在OCaml中，用冒号声明其标记的变体

Question

看下面的代码:

type z = Z of z
type 'a s = Z | S of 'a
type _ t = Z : z t | S : 'n t -> 'n s t

最后一行包含一个通用的变体，或者看起来像一个，但是没有使用关键字of，而是使用冒号:。为什么呢?我该怎么读这种字体呢?

查看类型声明的OCaml语法:https://ocaml.org/manual/types.html它似乎不太明显，如果这真的是一个变体，它甚至看起来像是一个标签和一个变体的混合。

Answer 1

这是广义代数数据类型(GADT)的定义。这个语言特性是在OCaml的4.0版本中引入的，并且正则代数数据类型(ADT)的语法被扩展为这个列变体，以启用特定于构造函数的约束。

常规ADT语法<Constr> [of <args>]用于引入具有指定参数的构造函数<Constr>，例如，

type student = Student of string * int

通用语法，<Constr> : [<args>] -> <constr>使用:而不是of，但增加了一个额外的位置来指定类型约束，例如，

type student = Student : string * int -> student

约束必须是已定义类型的实例。当定义的类型或构造函数参数(或两者)是多态的，即引用类型变量时，它是有用的。一个更好的例子是表达式语言的类型安全抽象语法树，例如

type _ exp = 
| Int : int -> int exp
| Str : string -> string exp
| Cat : string exp * string exp -> string exp
| Add : int exp * int exp -> int exp

使用这种表示，我们可以编写一个静态类型解释器，其中我们不必处理Add (Str "foo", Int 42)的情况，因为Cat构造函数的约束要求两个参数都具有string类型，因此不可能构造这样的值。

GADT的另一个用例是启用存在类型，这些存在类型可用于实现动态类型和ad-hoc多态性，例如Haskell类型类。在存在构造函数中，在构造函数参数类型中出现的某些类型变量在约束类型中不存在，例如

type show = Show : {data : 'a; show : 'a -> string} -> show
let show (Show {show; data}) = show data

这样我们就有了异构容器，

let entries = [
Show {data=42; show=string_of_int};
Show {data="foo"; show=fun x -> x};
]

我们可以显示，

# List.map show entries;;
- : string list = ["42"; "foo"]