广义代数数据类型
广义代数数据类型(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,就没有类型安全的方法来表示这个约束。