了解与通过用户定义的类索引的数据类型匹配的模式中涉及的强制类型转换

Question

所以,我正在DataKinds和TypeFamiliesHaskell 一起玩,并开始关注生成的Core GHC.

这是一个小TestCase来激发我的问题:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}

module TestCase where

data Ty = TyBool | TyInt

type family InterpTy (t :: Ty) :: *
type instance InterpTy TyBool = Bool
type instance InterpTy TyInt  = Int

data Expr (a :: Ty) where
  I :: Int  -> Expr TyInt
  B :: Bool -> Expr TyBool

eval :: Expr a -> InterpTy a
eval (I i) = i
eval (B b) = b

我们来看看为eval函数生成的Core

TestCase.eval =
  \ (@ (a_aKM :: TestCase.Ty)) (ds_dL3 :: TestCase.Expr a_aKM) ->
    case ds_dL3 of _ [Occ=Dead] {
      TestCase.I dt_dLh i_as6 ->
        i_as6
        `cast` (Sub (Sym TestCase.TFCo:R:InterpTyTyInt[0])
                ; (TestCase.InterpTy (Sym dt_dLh))_R
                :: GHC.Types.Int ~# TestCase.InterpTy a_aKM);
      TestCase.B dt_dLc b_as7 ->
        b_as7
        `cast` (Sub (Sym TestCase.TFCo:R:InterpTyTyBool[0])
                ; (TestCase.InterpTy (Sym dt_dLc))_R
                :: GHC.Types.Bool ~# TestCase.InterpTy a_aKM)
    }

显然,我们需要携带有关a特定分支中可能存在的信息.如果我没有对Datakind进行索引并且不使用TypeFamilies,那么转换更容易理解.

它会是这样的:

Main.eval =
  \ (@ a_a1hg) (ds_d1sQ :: Main.Simpl a_a1hg) ->
    case ds_d1sQ of _ [Occ=Dead] {
      Main.I' dt_d1to i_aFa ->
        i_aFa
        `cast` (Sub (Sym dt_d1to) :: GHC.Integer.Type.Integer ~# a_a1hg);
      Main.B' dt_d1tk b_aFb ->
        b_aFb `cast` (Sub (Sym dt_d1tk) :: GHC.Types.Bool ~# a_a1hg)
    }

这个我能完全理解,在这个TypeFamilies例子中让我烦恼的是这部分:

(Sub (Sym TestCase.TFCo:R:InterpTyTyInt[0])
      ; (TestCase.InterpTy (Sym dt_dLh))_R
      :: GHC.Types.Int ~# TestCase.InterpTy a_aKM);

第二行真的让我很困惑.分号在那里做什么？这里似乎有点不合适或者我错过了什么？有没有我可以阅读的地方(如果你能推荐一个,我很乐意拿文件)

亲切的问候,

raichoo

Answer 1

分号是强制传递的语法.

关于System FC的最新(截至2014年9月)论文是来自ICFP 2014的"Haskell中的安全零成本强制".

特别是,在该论文的图3中,我们看到了强制的语法."γ1;γ2"是强制传递性.如果γ1是一个强迫,证明"τ1~τ2"和γ2是一个强迫,证明τ2~τ3那么"γ1;γ2"是一个强迫τ1~τ3.

在这个例子中,当你编写eval (I i) = i编译器在右侧看到的是一个类型的值,Int它需要什么(从函数的返回类型)是什么InterpTy a.所以现在需要构建一个证明Int ~ InterpTy a.

非正式地,(从右到左阅读并忽略角色 - 有关详细信息,请参阅链接的论文):

1. 从做GADT模式匹配我们学到了" a ~ Int"(那是dt_dLh)
2. 所以我们申请Sym它,以获得" Int ~ a".
3. 然后应用该InterpTy族来获取" InterpTy Int ~ InterpTy a"(这是/同余/的一个实例)
4. 然后我们用" Sym InterpTyTyInt"(这是说明" InterpTy TyInt ~ Int" 的公理的翻转版本)来传递,以获得我们所追求的强制:" Int ~ InterpTy a"