haskell - 什么是 GADT？

Question

我正在阅读 GADTs for dummies Haskell Wiki 上的页面，我仍然不明白如何以及为什么应该使用它们。作者举了一个励志的例子:

data T a where
    D1 :: Int -> T String
    D2 :: T Bool
    D3 :: (a,a) -> T [a]

这段代码究竟做了什么，为什么有用？

如果这个问题有点太模糊，也许一个相关的问题是:GADT 可以用来实现成员函数吗？

Answer 1

假设您想为一个水果袋建模。这个袋子可以有苹果或橘子。因此，作为一个好的哈斯克勒，你定义:

data Bag = Oranges Int | Apples Int

看起来不错。让我们看看 Bag单独键入而不查看数据构造函数。是否 Bag仅 type 就可以告诉您它是橙色包还是苹果包。不是静态的，我的意思是在运行时，函数可以模式匹配 Bag 的值type 来检测它是橘子还是苹果，但在编译时/类型检查时强制执行这个不是很好，所以一个只适用于 Bag of apples 的函数根本不能传递 bag of oranges。

这就是 GADT 可以帮助我们的地方，基本上可以让我们更准确地了解我们的类型:

data Orange = ...
data Apple = ....

data Bag a where
    OrangeBag :: [Orange] -> Bag [Orange]
    AppleBag :: [Apple] -> Bag [Apple]

现在我可以定义一个只适用于苹果袋的函数。

giveMeApples :: Bag [Apple] -> ...