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

Question

所以，我在 Haskell 中玩弄 DataKinds 和 TypeFamilies 并开始查看生成的 Core GHC。

这里有一个小测试用例来激发我的问题：

{-# 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);

第二行真正让我感到困惑。分号在那里做什么？这里似乎有点不合适，或者我错过了什么？有没有地方可以读到这个（如果你能推荐的话，我很乐意拿论文）

亲切的问候，

瑞秋

Answer 1

分号是强制传递性的语法。

关于 System FC 的最新（截至 2014 年 9 月）论文是来自 ICFP 2014 的"Safe Zero-Cost Coercions in Haskell"。

特别是，在那篇论文的图 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”（这是/congruence/ 的一个实例）
4. 然后我们将它与“Sym InterpTyTyInt”（这是声明“InterpTy TyInt ~ Int”的公理的翻转版本）传递组合以获得我们所追求的强制：“Int ~ InterpTy a”