GADTs

传统的代数数据类型在其类型变量中是参数化的。例如，如果我们定义 ADT 之类的

data Expr a = IntLit Int 
            | BoolLit Bool 
            | If (Expr Bool) (Expr a) (Expr a)

希望这将静态排除非良好类型的条件，这将不会像预期的那样表现，因为 IntLit::Int -> Expr a 的类型是普遍量化的：对于 a 的任何选择，它产生 Expr a 类型的值。特别是对于 a ~ Bool，我们有 IntLit::Int -> Expr Bool，允许我们构造类似 If (IntLit 1) e1 e2 的东西，这是 If 构造函数试图排除的类型。

广义代数数据类型允许我们控制数据构造函数的结果类型，使它们不仅仅是参数化的。我们可以像这样重写我们的 Expr 类型作为 GADT：

data Expr a where
  IntLit::Int -> Expr Int
  BoolLit::Bool -> Expr Bool
  If::Expr Bool -> Expr a -> Expr a -> Expr a

这里，构造函数 IntLit 的类型是 Int -> Expr Int，因此 IntLit 1 :: Expr Bool 不会进行类型检查。

GADT 值上的模式匹配会导致返回的术语类型的细化。例如，可以为 Expr a 编写一个评估器，如下所示：

crazyEval::Expr a -> a
crazyEval (IntLit x) = 
   -- Here we can use `(+)` because x::Int
   x + 1 
crazyEval (BoolLit b) = 
   -- Here we can use `not` because b::Bool
   not b
crazyEval (If b thn els) = 
  -- Because b::Expr Bool, we can use `crazyEval b::Bool`.
  -- Also, because thn::Expr a and els::Expr a, we can pass either to 
  -- the recursive call to `crazyEval` and get an a back
  crazyEval $ if crazyEval b then thn else els 

请注意，我们可以在上面的定义中使用 (+)，因为当 IntLit x 模式匹配时，我们也会知道 a ~ Int（同样对于 not 和 if_then_else_ 当 a ~ Bool）。