什么是 Haskell 中的 GADT（广义代数数据类型）？

先看看没有 GADT 的时候我们在做啥。最简单的，比如定义一个列表：

List a = Nil | Cons a (List a)

它是在做啥呢？

• 先看等号左边，它首先定义了一个叫 List 的 type constructor，它接受一个类型，并返回一个新的类型。其实就是类型的函数。
• 再看右边，它告诉我们有两种方式获得一个类型为 List a 的值，一个叫 Nil，一个叫 Cons a (List a)。
  • Nil 的话，你直接写 Nil，它就是一个 List a 类型的值，至于这个 a 具体是啥，需要结合上下文推导才知道。
  • 而 Cons a (List a) 呢，它是接受两个参数，一个类型是 a，一个类型是 List a，然后返回一个 List a 类型的值。至于这个 a 是啥，我们同样是需要推导才能知道的，不过是这里的推导比较显著罢了，因为直接就是第一个参数的类型。

那么我们可以用函数形式给这俩表示出来：

Nil :: List a
Cons :: a -> List a -> List a

可以看到它们接受一些参数，但返回类型都是 List a。GADT 唯一改的就是返回类型这个地方，我们不一定必须写 a，而是可以把 a 替换为另外的类型。比如说我们可以有一个只能作为 Int 列表的头的构造函数：

IntNil :: List Int

我们可以试验一下（这个就是 GADT 的写法了）：

data List a where
  IntNil :: List Int
  Nil :: List a
  Cons :: a -> List a -> List a

a :: List Int
a = IntNil

-- 会报错，因为类型不相容
-- c_ :: List Char
-- c_ = IntNil

-- 这个就是相容的
c :: List Char
c = Nil

当然左边不一定得是 List Int 这样直白的类型，只要是一个形如 List 的类型就可以了，你甚至可以把自己嵌套进去：

data Pair a b where Pair :: a -> b -> Pair a b

data List a where IntListNil :: List (List Int)
  ListNil :: List (List a)
  IntNil :: List Int
  Nil :: List a
  Cons :: a -> List a -> List a
  -- 这个就不行，因为形如 Pair 而不是 List
  -- Bad :: a -> List a -> Pair a (List a)

那么它可以干啥用呢？我所知道的有这么一些（都不超出网上的 wiki 的范畴）：

一种就是最有名的，嵌入一种语言（的语法树）。比如这么一种简单的表达式语言：

data Expr = 
    ILit Int
  | BLit Bool
  | Add Expr Expr
  | Eq Expr Expr

这样是足够表达了，但是存在一些问题——比如我们不希望 Bool 被 Add（就是说我们要嵌入的语言，它本身也是有类型的，有些运算不能对某些对象做），但这个定义无法避免我们写：

addBool :: Expr
addBool = Add (BLit True) (BLit False)

一个想法是把这个 Expr 的「返回值」类型记录下来，就像我们对 List 做的那样（在那里我们记录的是成员类型）：

data Expr a = 
    ILit Int
  | BLit Bool
  | Add (Expr Int) (Expr Int)
  | Eq (Expr a) (Expr a)

这个看起来很美好，但是行不行呢？

实际上是不行的！你不要以为 BLit True 就是 Expr Bool 类型，从而会不能作为 Add 的参数了。其实，这里的 BLit True 还是 Expr a 类型，其中 a 是任意类型，就像之前的 Nil 是 List a 类型、a 是任意的一样。

这个时候就体现出 GADT 的重要性了——只有透过 GADT 才能限定一个「构造函数」的返回类型：

data Expr a where
  ILit :: Int -> Expr Int
  BLit :: Bool -> Expr Bool
  Add :: Expr Int -> Expr Int -> Expr Int
  -- 对 Eq 我们可以放宽要求，只用 typeclass 来限制，不必指定具体类型
  Eq :: Eq a => Expr a -> Expr a -> Expr Bool

这时候它就能分辨是非了：

-- 报错，因为 Expr Bool 和 Expr Int 不兼容
-- addBool =  Add (BLit True) (BLit False)
addInt = Add (ILit 1) (ILit 2)
eqBool = Eq (BLit True) (BLit False)

很美妙，是不是？

这就是所谓的 initial embedding of a language，而我们最后得到的用 GADT 的版本，叫 tagless initial embedding。为什么是 tagless 呢？因为原始的 ADT 是所谓的 “tagged union”。我们现在抛弃了它，所以叫 tagless。

这个 Expr 是很简单的语言。实际上你完全可以将 simply typed lambda calculus 给这样嵌入进去。

相对于 initial embedding，我们还可以有所谓 final embedding，不过跟 GADT 关系不大了。

我们还可以玩点更风骚的。比如这里假如有一种简单的、描述栈操作的语言，Push 表示推入一个数，Add 表示弹出两个数，把它们的和推回去：

data StackLang where
  Begin :: StackLang
  Push :: Int -> StackLang -> StackLang
  Add :: StackLang -> StackLang

bug = Add (Push 1 Begin)

这里的 bug 语句实际上是有 bug 的，因为你刚推进去一个 1，没有人和它相加。那么能不能从类型层面来消除这种 bug呢？

我们想，要是 StackLang 的类型里面，带上栈里有多少个数该多好啊！但是这时候 Begin 就不能返回一般的 StackLang 类型了，而是带有 0 个数的 StackLang 类型，同理，Push 接受带有 n 个数的 StackLang 类型，返回带有 n+1 个数的 StackLang 类型，Add 则是 n+2 -> n+1。此时 GADT 就可以派上用场了：

data Z
data S n

data SStackLang t where
  SBegin :: SStackLang Z
  SPush :: Int -> SStackLang t -> SStackLang (S t)
  SAdd :: SStackLang (S (S t)) -> SStackLang (S t)

这里 Z 和 S 就是对自然数的 0 和后继（successor）的模拟。这时候你会发现：

sBug = SAdd (SPush 1 SBegin)

会报错

• Couldn’t match type ‘Z’ with ‘S t’
Expected type: SStackLang (S (S t))
Actual type: SStackLang (S Z)

非常安全。

其实这就是对所谓的「依赖类型」(dependent type) 的模拟。仿照这个你还可以造出「长度为 n」的列表的概念，并对其定义安全的操作。这就是后话了。

GADT 还可以把 type 转化为 value。把类型保存在一个值里，本来你固然是可以：

data Witness a = Witness a

但这样你得提供一个 a 类型的值才能把类型记录进去。一方面很多时候没法构造这个值，另一方面可能有的类型就没有值，最后要求提供值的做法根本就是不科学的。

但是有 GADT 你就可以为所欲为——我不一定要接受一个值，才能得到这个类型了：

data Witness a where
  IntWitness :: Witness Int
  BoollWitness :: Witness Bool

这就是所谓的 “type witness”。至于这个有什么用，怎么用，为什么要这么用，（待续）。