什么是GADT？

Question

我当时正在Haskell上阅读假人用GADT页面，我仍然不明白如何以及为什么应该使用它们。作者举了一个令人振奋的例子：

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类型就能给你任何指示，无论是橙色的袋子还是苹果的袋子。嗯，不是静态的，我的意思是，在运行时，一个函数可以对Bag类型的值进行模式匹配，以检测它是橘子还是苹果，但是在编译时/类型检查本身强制执行这一点不是很好，这样一个只适用于一袋苹果的函数就不能传递一袋橘子了。

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

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

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

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

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

Answer 2

GADT允许您的类型包含关于它们所代表的值的更多信息。他们通过将Haskell data声明扩展到依赖类型语言中的归纳类型家族来做到这一点。

典型的示例是类型化的高阶抽象语法，表示为GADT。

{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeOperators #-} -- Not needed, just for convenience of (:@) below

module HOAS where

data Exp a where
  Lam  :: (Exp s -> Exp t) -> Exp (s -> t)
  (:@) :: Exp (s -> t) -> Exp s -> Exp t
  Con  :: a -> Exp a

intp :: Exp a -> a
intp (Con a)      = a
intp (Lam f)      = intp . f . Con
intp (fun :@ arg) = intp fun (intp arg)

在本例中，Exp是一个GADT。注意，Con构造函数是非常正常的，但是App和Lam构造函数非常自由地引入了新的类型变量。这些是存在量化的类型变量，它们代表了Lam和App的不同参数之间相当复杂的关系。

特别是，它们确保任何Exp都可以被解释为一个类型良好的Haskell表达式。在不使用GADT的情况下，我们需要使用sum类型来表示术语中的值，并处理类型错误。

>>> intp $ Con (+1) :@ Con 1
2

>>> Con (+1) :@ Con 'a'
<interactive>:1:11: Warning:
    No instance for (Num Char) arising from a use of `+'
    Possible fix: add an instance declaration for (Num Char)
    In the first argument of `Con', namely `(+ 1)'
    In the first argument of `App', namely `(Con (+ 1))'
    In the expression: App (Con (+ 1)) (Con 'a')

>>> let konst = Lam $ \x -> Lam $ \y -> x
>>> :t konst
konst :: Exp (t -> s -> t)

>>> :t intp $ konst :@ Con "first"
intp $ konst :@ Con "first" :: s -> [Char]

>>> intp $ konst :@ Con "first" :@ Con "second"
"first"