GADT（广义代数数据类型）

定义

广义代数数据类型（Generalized Algebraic Data Type，GADT）是代数数据类型的扩展：普通 ADT 的所有构造子必须返回同一形式的类型（如 Expr a），GADT 则允许每个构造子指定精确的返回类型（如 IntLit 返回 Expr Int、BoolLit 返回 Expr Bool）。

关键能力

模式匹配 GADT 时，编译器可从匹配到的构造子反推出类型参数的具体取值，即「类型精化」（type refinement）。这使类型系统能够跟踪值的内部不变量。

典型应用

最经典的例子是类型安全的表达式解释器：用 GADT 定义带类型索引的抽象语法树后，「对布尔值做加法」这类非法表达式在构造阶段就无法通过编译，eval 函数也无需任何运行时类型检查。GADT 还用于编码长度索引向量、状态机协议等。

语言支持

GHC Haskell（GADTs 扩展）、OCaml、Scala 3 均支持 GADT；Rust、TypeScript 只能部分模拟。