在 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 的另一个用例是启用可用于实现动态类型和临时多态性（ala 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"]