haskell - Haskell 中的类型冒险 : GADT's: why does the following typechecks?

Question

我正在关注this lecture作者:西蒙·佩顿·琼斯 (Simon Peyton-Jones) 关于 GADT 的文章。在那里，声明了以下数据类型:

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 是类型安全的。