理解涉及到模式匹配的索引在用户定义的种类上的数据类型所涉及的转换

Question

理解涉及到模式匹配的索引在用户定义的种类上的数据类型所涉及的转换

haskellcastingghctype-familiesdata-kinds

12

我在Haskell中尝试使用和，并开始查看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函数生成的核心内容。

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)
    }

我完全理解这个，但是示例中让我困扰的是这一部分：

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

第二行真的让我感到困惑。分号在这里做什么？它似乎有点不合适，还是我漏掉了什么？是否有一个地方可以阅读相关资料（如果您能推荐一篇论文，我会非常感激）。

此致敬礼，

raichoo

- raichoo

1个回答

网页内容由stack overflow 提供, 点击上面的

可以查看英文原文，
原文链接

- Lambdageek · Accepted Answer

分号是强制类型转换的语法。

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

特别地，在该论文的第3图中，我们看到了强制类型转换的语法。"γ₁;γ₂"是强制类型转换的传递性。如果γ₁是证明"τ₁ ~ τ₂"的强制类型转换，γ₂是证明τ₂ ~ τ₃的强制类型转换，那么"γ₁;γ₂"就是证明τ₁ ~ τ₃的强制类型转换。

在这个例子中，当你写eval (I i) = i时，编译器在右侧看到的是一个类型为Int的值，而它需要（从函数的返回类型中）得到InterpTy a的东西。所以现在它需要构造一个证明，证明Int ~ InterpTy a。

非正式地说（从右向左阅读并忽略角色 - 角色的细节请参见链接的论文）：

通过进行GADT模式匹配，我们了解到“a ~ Int”（这是dt_dLh）。
因此，我们将Sym应用于它，得到“Int ~ a”。
然后应用InterpTy家族，得到“InterpTy Int ~ InterpTy a”（这是/congruence/的一个实例）
然后我们将其与“Sym InterpTyTyInt”组合，以获取我们想要的强制转换：“Int ~ InterpTy a”。