广义代数数据类型

广义代数数据类型（GADT）是基本变量概念的扩展：

variant pair[T] =
| PUnit of unit => pair[unit]
| PInt[T] of int * pair[T] => pair[int * pair[T]]
| PFloat[T] of float * pair[T] => pair[float * pair[T]]
| PString[T] of string * pair[T] => pair[string * pair[T]]
;

这看起来像一个普通的变体，除了在RHS上有一个额外的术语，它总是带有一些下标的变体。

一个类型变量的普通变量 T 在本例中，RHS构造函数始终是变量类型 pair 使用它的通用量词，在本例中是类型变量 T .

对于GADT，下标可以是类型变量的任意类型函数，而不是 T .

鉴于上述GADT，以下是一些值：

var x1 : pair[unit] = #PUnit[unit];
var x2 : pair[int * pair[unit]] = PInt (1,x1);
var x3 = PFloat (42.33f, x2);

要使用GADT，您需要编写一个泛型函数：

fun show [W:GENERIC] (x:W):string=
{
 match x with
 | PUnit => return "PUnit";
 | PInt (head, tail) => return "PInt(" + head.str+", " + tail.show+ ")";
 | PString (head, tail) => return "PString(" + head+", " + tail.show+ ")";
 | PFloat (head, tail) => return "PFloat(" + head.str+", " + tail.show+ ")";
 endmatch;
}

println$ "x3=" + x3.show;

泛型函数的原因是它提供静态多态递归。

存在主义者

GAD构造函数可以引入一个称为存在变量的额外类型变量：

variant pair[T] =
| PUnit of unit => pair[unit]
| Pair[T,U] of U * pair[T] => pair[U * pair[T]]
;

var x1 = #PUnit[unit];
var x2 = Pair (22,x1);
var x3 = Pair (99.76,x2);

fun f[T:GENERIC] (x:T) = {
  match x with
  | Pair (a,b) => return a.str + ","+b.f;
  | PUnit => return "UNIT";
  endmatch;
}

println$ f x3;

这样做的好处 pair 比上一个更有效 any 输入U，而不仅仅是int、string或float。这个GADT实际上是递归地定义元组。

分析GADT的函数必须是泛型的，因为解码器需要多态递归。特别注意 b 在哪 f 调用的不等于 x .

另一个例子

这个例子来自维基百科：

variant Expr[T] =
  | EBool of bool => Expr[bool]
  | EInt of int => Expr[int]
  | EEqual of Expr[int] * Expr[int] => Expr[bool]
;

fun eval(e) => match e with
  | EBool a => a
  | EInt a => a
  | EEqual (a,b) => eval a == eval b
  endmatch
;

var expr1 = EEqual (EInt 2, EInt 3);
println$ eval expr1;

在这个例子中，我们有布尔值和整数值以及一个相等运算符。重要的是，等式只对整数有效，并返回bool：没有GADTs，就没有类型安全的方法来表示这个约束。