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
(同样对于 not
和 if_then_else_
当 a ~ Bool
)。