OCaml类型定义中冒号的含义解析——equality witness相关疑问

问题背景 #

在学习高阶类型（higher-kinded types）时接触到**equality witness（等价见证）**术语，查到如下OCaml类型定义：

type ('a, 'b) eq = | Eq : ('a, 'a) eq

原本以为它等同于：

type ('a, 'b) eq = | Eq of ('a, 'a) eq

但两者在顶层环境的输出不同。请问该冒号的作用是什么？这个类型的定义逻辑是怎样的？

补充猜测 #

我猜测Eq是('a, 'a) eq类型而非类型构造器，符号Eq可被解读为('a, 'a) eq，是否正确？

解答 #

1. 冒号的作用：GADT语法标记 #

OCaml里，:在数据构造器定义中是**广义代数数据类型（GADT）**的专属语法，用来明确指定该构造器对应的具体类型实例，而非让编译器默认根据参数推导类型。

对比两种写法的本质差异：

• 用of的版本是普通代数数据类型：Eq是构造器，需要接收一个('a, 'a) eq类型的值作为参数，才能返回('a, 'b) eq类型的值（这里'b是自由类型参数，会导致递归定义的逻辑矛盾）。
• 用:的版本是GADT定义：Eq是无参数构造器，它的类型直接就是('a, 'a) eq——只有当类型参数'a和'b完全相同时，这个构造器才能生成合法的('a, 'b) eq类型值。

2. 类型定义逻辑：等价见证的核心 #

这个eq类型的作用是在类型层面证明两个类型等价：

• 当你持有一个('a, 'b) eq类型的值时，OCaml类型检查器会认定'a和'b是同一类型，允许后续代码中进行安全的类型转换。
• 唯一能生成eq类型值的构造器是Eq，且它只能产出('a, 'a) eq实例——这就从根源保证了：只有真正等价的类型，才能生成合法的见证值。

举个实用例子，借助这个类型可以写出安全的类型转换函数：

let cast (type a b) (eq : (a, b) eq) (x : a) : b =
  match eq with
  | Eq -> x

匹配Eq时，类型检查器会自动推导a和b是同一类型，因此允许直接返回x作为b类型的值。

3. 补充猜测的验证 #

你的猜测完全正确：Eq不是类型构造器，而是一个值构造器，它的类型就是('a, 'a) eq。换句话说，Eq本身就是'a等于'a的见证值——不需要传入任何参数，它直接代表了两个类型相等的证据。

而用of的版本中，Eq是需要接收('a, 'a) eq参数的构造器，会形成无意义的递归定义，根本无法起到等价见证的作用，因为你需要先有一个见证值才能创建另一个，陷入逻辑循环。

内容的提问来源于stack exchange，提问作者Rawley Fowler