什么是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类型的值来检测它是橙色还是苹果但是在编译时/类型检查时自己强制执行此操作不是很好,所以这个函数只有与袋苹果一起工作不能通过橘子袋.

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

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

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

现在我可以定义一个仅适用于苹果袋的功能.

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

Answer 2

GADT允许您让类型包含有关它们所代表的值的更多信息.他们通过拉伸哈斯克尔做这个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表达式.如果不使用GADTs我们就需要使用金额类型来表示我们的条款的价值和处理类型的错误.

>>> 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"