在Haskell中使用类型的冒险:GADT:为什么以下的类型检查？

Question

我正在接受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,结果与类型签名不匹配？就像a你通过一个T a和一个a？

答案是:不,没有.如果你传入T0(意思a是Bool),你会得到一个Bool.如果你传入了一个T1你将得到第二个参数,这也保证是类型的a.如果你试图调用它f (T1 :: T Int) "notAnInt",它将无法编译,因为类型不匹配.换句话说:与类型签名匹配的函数的任何应用程序将根据签名生成正确的结果类型.因此f是类型安全的.