GADTs

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

 placeholderCopydata 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:

 placeholderCopydata 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 编写一个评估器,如下所示:

 placeholderCopycrazyEval::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(同样对于 notif_then_else_a ~ Bool)。