我下面这个讲座由西蒙·佩顿-琼斯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有效？
通常，要输入检查
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一般情况下哪个是假的，但在这里变为真，因为我们只需要在提供的equals下检查即可a ~ Bool。而且，在这种情况下，它成为事实！
（说实话，类型系统所做的事情略有不同，而是检查两个分支是否都等于签名中声明的类型（在已知的相等性下），但是让我保持简单。对于GADT模式匹配，这种签名是总是需要某种形式的。）
请注意，这就是GADT的重点-它们允许类型检查其分支显然涉及不同类型的模式匹配。
本文收集自互联网，转载请注明来源。
如有侵权，请联系 [email protected] 删除。
我来说两句