Haskell 中的类型历险记：GADT：为什么要进行以下类型检查？

Question

我在 GADT 上关注 Simon Peyton-Jones 的 this lecture。在那里，声明了以下数据类型：

data T a where
  T0 :: Bool -> T Bool
  T1 :: T a

然后问的问题是以下函数的类型是什么：

f x y = case x of
          T0 _ -> True
          T1   -> y

对我来说，似乎唯一可能的类型是：

f :: T a -> Bool -> Bool

但是，下面的类型：

f :: T a -> a -> a

也有效！事实上，您可以按如下方式使用 f：

 f (T1) "hello"

我的问题是为什么 f 的第二种签名有效？

Answer 1

在f的定义中有两种情况，都匹配你的第二种签名：

T0 _ -> True

此处您的参数是 T Bool 类型，您的结果是 Bool。所以这与 a ~ Bool.

的类型签名匹配

T1 ->  y

这里你的参数是 T a 类型，你的结果是 y，它是 a 类型。所以这与任何 a.

的签名匹配

要理解为什么这是类型安全的，只需问自己以下问题：有没有什么方法可以调用 f，从而使结果与类型签名不匹配？如果你传入 T a 和 a，你能取回 a 以外的任何东西吗？

答案是：没有。如果你传入一个 T0（意思是 a 是 Bool），你会得到一个 Bool。如果你传入一个 T1 你会得到第二个参数，它也保证是 a 类型。如果您尝试像 f (T1 :: T Int) "notAnInt" 那样调用它，它将无法编译，因为类型不匹配。换句话说：与类型签名匹配的函数的任何应用都将根据签名产生正确的结果类型。因此 f 是类型安全的。

Answer 2

通常，输入检查

case e of
  K1 ... -> e1
  K2 ... -> e2
  ...

要求所有表达式ei共享一个共同的类型。

这在使用 GADT 时仍然适用，除了在每个分支中，构造函数提供了一些已知在该分支中成立的类型相等方程 T ~ T'。因此，当检查所有 ei 是否共享一个公共类型时，我们不再要求它们的类型相同，而只是在类型等式成立时才相等。

特别是：

f :: T a -> a -> a
f x y = -- we know x :: T a , y :: a
   case x of
      T0 _ -> -- provides a ~ Bool
              True   -- has type Bool
      T1   -> -- provides a ~ a (useless)
              y      -- has type a

这里我们需要检查Bool ~ a，这在一般情况下是假的，但这里变成了真的，因为我们只需要在提供的相等性下检查a ~ Bool。而且，在这种情况下，它就变成了真的！

（老实说，类型系统做的事情略有不同，相反，检查两个分支是否等于在签名（在他们已知的平等条件下）——但让我保持简单。对于 GADT 模式匹配，始终需要某种形式的签名。）

请注意，这是 GADT 的全部要点——它们允许对分支显然涉及不同类型的模式匹配进行类型检查。

Haskell 中的类型历险记：GADT：为什么要进行以下类型检查？

Adventures with Types in Haskell: GADT's: why does the following typechecks?

haskell

functional-programming

type-inference

gadt