第 7 章 广义代数数据类型

广义代数数据类型或 GADTs 以两种方式扩展了常见的总和类型：类型参数上的约束可能会根据值构造函数而变化，并且某些类型变量可能会被存在量化。添加约束是通过给出显式返回类型来完成的，其中类型参数被实例化。

type _ term = | Int : int -> int term | Add : (int -> int -> int) term | App : ('b -> 'a) term * 'b term -> 'a term

此返回类型必须使用与正在定义的类型相同的类型构造函数，并且具有相同数量的参数。当变量出现在构造函数的参数内部，但不在其返回类型中时，它们就会变成存在的。由于返回类型的使用通常消除了在类型定义的左侧命名类型参数的需要，因此在这种情况下可以用匿名类型 _ 替换它们。

与每个构造函数关联的约束可以通过模式匹配恢复。也就是说，如果模式匹配的被匹配项的类型包含一个局部抽象类型，那么此类型可以根据使用的构造函数进行细化。这些额外的约束仅在模式匹配的相应分支内部有效。如果一个构造函数有一些存在变量，则会生成新的局部抽象类型，并且它们不能超出此分支的范围。

1 递归函数

我们写一个 eval 函数

let rec eval : type a. a term -> a = function | Int n -> n (* a = int *) | Add -> (fun x y -> x+y) (* a = int -> int -> int *) | App(f,x) -> (eval f) (eval x) (* eval 在类型 (b->a) 和 b 上被调用，用于新的 b *)

并使用它

let two = eval (App (App (Add, Int 1), Int 1))
val two : int = 2

重要的是要注意，函数 eval 正在使用局部抽象类型的多态语法。当定义一个操作 GADT 的递归函数时，通常应该使用显式多态递归。例如，以下定义会导致类型错误

let rec eval (type a) : a term -> a = function | Int n -> n | Add -> (fun x y -> x+y) | App(f,x) -> (eval f) (eval x)
错误: 此表达式类型为 ($b -> a) term，但预期为 'a 类型 类型构造函数 $b 将超出其范围 提示：$b 是由 App 构造函数绑定的存在类型。

在没有显式多态注释的情况下，将为递归函数推断出单态类型。如果递归调用在定义中发生在一个涉及存在 GADT 类型变量的类型上，则此变量会流向递归函数的类型，从而超出其范围。在上面的例子中，当 eval 以 f 作为参数调用时，这会发生在 App(f,x) 分支中。在此分支中，f 的类型为 ($App_'b -> a) term。 $ 前缀在 $App_'b 中表示编译器命名的存在类型（参见 ‍7.5）。由于 eval 的类型是 'a term -> 'a，因此调用 eval f 使存在类型 $App_'b 流向类型变量 'a 并超出其范围。这将触发上述错误。

2 类型推断

GADTs 的类型推断非常困难。这是因为当类型从一个分支中逃逸时，某些类型可能会变得模棱两可。例如，在上面的 Int 情况下，n 可能是 int 或 a 类型，并且它们在该分支之外并不等效。作为一种初步近似，如果模式匹配用不包含自由类型变量的类型（在被匹配项和返回类型上）进行注释，则类型推断将始终有效。这在上面的示例中是有效的，因为类型注释仅包含局部抽象类型。

实际上，类型推断比这要聪明一些：类型注释不需要直接在模式匹配上，并且类型也不需要始终是封闭的。因此，通常只注释函数就足够了，如上面的示例所示。类型注释以两种方式传播：对于被匹配项，它们遵循类型推断的流程，类似于多态方法；对于返回类型，它们遵循程序的结构，它们在函数上被分割，传播到模式匹配的所有分支，并通过元组、记录和总和类型。此外，使用的歧义概念更强：只有当类型与不兼容类型（由约束等效）混合，并且它们之间没有类型注释时，才认为类型是模棱两可的。例如，以下程序类型正确。

let rec sum : type a. a term -> _ = fun x -> let y = match x with | Int n -> n | Add -> 0 | App(f,x) -> sum f + sum x in y + 1
val sum : 'a term -> int = <fun>

这里，返回类型 int 从未与 a 混合，因此被视为非模棱两可的，可以被推断出来。当使用这种部分类型注释时，我们强烈建议指定 -principal 模式，以检查推断是否是主要的。

穷举检查了解 GADT 约束，可以自动推断出某些情况不可能发生。例如，以下模式匹配被正确地视为穷举（Add 情况不可能发生）。

let get_int : int term -> int = function | Int n -> n | App(_,_) -> 0

3 反证情况

通常，穷举检查只尝试检查模式匹配中省略的那些情况是否可类型化。但是，可以通过添加反证情况来强制它更努力地尝试，写成一个句号。在存在反证情况的情况下，穷举检查将首先计算模式与之前情况补集的交集。然后，它通过尝试对其进行类型检查来检查生成的模式是否真的可以匹配任何具体的值。生成的模式中的通配符以特殊方式处理：如果它们的类型是仅包含 GADT 构造函数的变体类型，则模式将被拆分为不同的构造函数，以检查它们中的任何一个是否可能（这不会对这些构造函数的参数进行拆分，以避免非终止）。我们还拆分元组和仅包含一个情况的变体类型，因为它们可能在内部包含 GADTs。例如，以下代码被认为是穷举的

type _ t = | Int : int t | Bool : bool t let deep : (char t * int) option -> char = function | None -> 'c' | _ -> .

也就是说，推断出的剩余情况是 Some _，它被拆分为 Some (Int, _) 和 Some (Bool, _)，它们都不可类型化，因为 deep 期望一个不存在的 char t 作为元组的第一个元素。注意，这里可以省略反证情况，因为它在模式匹配中只有一个情况时会自动添加。

另一个补充是，冗余检查现在了解 GADTs：如果一个情况可以用相同的模式替换为一个反证情况，那么它将被检测为冗余。

4 进阶示例

我们上面定义的 term 类型是一个索引类型，其中一个类型参数反映了值内容的属性。GADTs 的另一个用途是单例类型，其中一个 GADT 值代表一个确切的类型。此值可以用作此类型的运行时表示，并且接收它的函数可以具有多态行为。

这是一个多态函数的示例，它获取一些类型 t 的运行时表示和相同类型的值，然后将值漂亮地打印为字符串

type _ typ = | Int : int typ | String : string typ | Pair : 'a typ * 'b typ -> ('a * 'b) typ let rec to_string: type t. t typ -> t -> string = fun t x -> match t with | Int -> Int.to_string x | String -> Printf.sprintf "%S" x | Pair(t1,t2) -> let (x1, x2) = x in Printf.sprintf "(%s,%s)" (to_string t1 x1) (to_string t2 x2)

GADTs 的另一个常见应用是等式见证。

type (_,_) eq = Eq : ('a,'a) eq let cast : type a b. (a,b) eq -> a -> b = fun Eq x -> x

这里类型 eq 只有一个构造函数，通过匹配它，可以添加一个本地约束，允许在 a 和 b 之间进行转换。通过构建这样的等式见证，可以使语法上不同的类型相等。

以下是一个使用单例类型和等式见证来实现动态类型的示例。

let rec eq_type : type a b. a typ -> b typ -> (a,b) eq option = fun a b -> match a, b with | Int, Int -> Some Eq | String, String -> Some Eq | Pair(a1,a2), Pair(b1,b2) -> begin match eq_type a1 b1, eq_type a2 b2 with | Some Eq, Some Eq -> Some Eq | _ -> None end | _ -> None type dyn = Dyn : 'a typ * 'a -> dyn let get_dyn : type a. a typ -> dyn -> a option = fun a (Dyn(b,x)) -> match eq_type a b with | None -> None | Some Eq -> Some x

5 错误消息中的存在类型名

在存在 GADTs 的情况下，模式匹配的类型推断可能会生成许多存在类型。必要时，错误消息使用编译器生成的名称来引用这些存在类型。当前，编译器根据以下命名法生成这些名称

如最后一项所示，当前行为并不完美，可能在未来版本中得到改进。

6 显式命名存在类型

如上所述，对 GADT 构造函数进行模式匹配可能会引入存在类型。语法已被引入，允许它们被显式命名。例如，以下代码命名了 f 的参数类型，并使用此名称。

type _ closure = Closure : ('a -> 'b) * 'a -> 'b closure let eval = fun (Closure (type a) (f, x : (a -> _) * _)) -> f (x : a)

构造函数的所有存在类型变量都必须通过 (type ...) 结构引入，并在构造函数参数外部进行类型标注。

7 非局部抽象类型上的方程

GADT 模式匹配也可以为非局部抽象类型添加类型方程。行为与局部抽象类型相同。重用上面的 eq 类型，可以写

module M : sig type t val x : t val e : (t,int) eq end = struct type t = int let x = 33 let e = Eq end let x : int = let Eq = M.e in M.x

当然，并非所有抽象类型都可以被细化，因为这将与穷举性检查相矛盾。也就是说，内置类型（由编译器本身定义的类型，例如 int 或 array），以及由局部模块定义的抽象类型，是不可实例化的，因此会导致类型错误而不是引入方程。

版权所有 © 2024 法国国家信息与自动化研究所