haskell - 什么是 GADT？

Question

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

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类型的值进行模式匹配以检测它是橙子还是苹果，但是在编译时/类型检查时强制执行这一点不是很好，所以只有一个函数与 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] -> ...

Answer 2

GADT 允许您让您的类型包含有关它们所代表的值的更多信息。他们通过将 Haskelldata声明稍微延伸到依赖类型语言中的归纳类型族来做到这一点。

典型示例是类型化的高阶抽象语法，表示为 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。

特别是，它们确保 anyExp可以解释为类型良好的 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"