1 / 2
16 / 17 · GADTs
GADT：构造器携带类型等式
普通变体做不到：同一条 expr，有的求值出 int，有的出 bool。
如果 expr 只有 Int 和 Bool 两种构造器，而你写 eval : expr -> int，那么遇到 Bool 分支就无路可走。把返回类型改成一个大变体，又把「这棵树其实是 int」的信息扔掉了。
GADT 让构造器决定类型参数。Lit : int -> int expr，IsZero : int expr -> bool expr。match 到 Lit 时，编译器知道整棵树的参数就是 int。书桌的解释器不会做这种细化，所以这段只读、不跑。
书里的形状
utop
type _ expr =
| Lit : int -> int expr
| IsZero : int expr -> bool expr
| If : bool expr * 'a expr * 'a expr -> 'a expr
let rec eval : type a. a expr -> a = function
| Lit n -> n
| IsZero e -> eval e = 0
| If (c, t, e) -> if eval c then eval t else eval e这一课只读。GADT 会在匹配时细化类型参数，书桌的解释器做不到，硬跑会把这个要点盖住。
先预测，再对照
2 / 2