OCaml自定义类型定义中冒号:与箭头->的语法含义

你看到的是OCaml语言中**广义代数数据类型（GADT）**的定义语法，和你之前掌握的普通代数数据类型（ADT）语法属于同个类型系统下的不同书写形式，因此会出现你没见过的冒号、箭头位置。

• 构造器后的冒号:：用于显式标注构造器本身的完整类型签名。你熟悉的of写法是普通ADT的语法糖，GADT写法直接把构造器的类型完整展开书写。
• 签名中的箭头->：就是OCaml标准的函数类型箭头，含义为「接收箭头左侧类型的参数，返回箭头右侧类型的结果」。代数数据类型的构造器本质是特殊的构造函数，输入对应参数就返回该类型的实例，GADT只是把这个函数的类型直接写了出来，和你平时写普通函数类型签名的箭头语义完全一致。

你已经掌握普通列表的ADT定义：

type 'a list =
  | Nil
  | Cons of 'a * ('a list)

把它改写成完全等价的GADT写法，形式如下，可以直接对照理解对应关系：

type 'a list =
  | Nil : 'a list
  | Cons : 'a * ('a list) -> 'a list

对照就能发现：无参数构造器Nil不需要接收参数，所以签名直接写返回类型'a list，没有箭头；带参数的构造器Cons接收一个'a * 'a list类型的二元组参数，返回'a list类型的列表实例，所以签名用箭头连接参数类型和返回类型，和你看到的Coq文档里的写法结构完全一致。

你看到的代码：

type 'l generic_argument =
| GenArg : ('a, 'l) abstract_argument_type * 'a -> 'l generic_argument

逐部分拆解语义：

1. 这是一个带类型参数'l的GADT类型，类型名为generic_argument
2. 该类型只有一个构造器GenArg
3. GenArg是一个构造函数：接收一个二元组作为入参，二元组第一个元素是('a, 'l) abstract_argument_type类型的值，第二个元素是和第一个元素共享类型变量'a的值，最终返回'l generic_argument类型的实例

这个定义用到了GADT独有的存在类型特性：类型变量'a没有出现在最终返回的类型'l generic_argument的参数中，是构造器内部隐藏的局部类型。这个特性允许构造器封装任意类型的参数值，外层使用generic_argument类型时只需要按'l标记做分类，不需要感知内部存储的'a具体是什么类型，Coq用这个结构实现了通用参数的类型安全封装。

内容的提问来源于stack exchange，提问作者Charlie Parker