OCaml中定义无构造函数的类型有何含义？如何构造其值？

你在Coq代码库中看到的type ('a, 'b, 'c) tag是OCaml里非常典型的抽象类型定义，这类定义几乎都出现在模块的签名文件（.mli）中，核心作用是实现模块层面的封装：

• 这类定义不会对外暴露类型的内部结构、构造函数，签名作用域之外的代码完全不知道这个类型的具体实现形式，自然无法直接通过构造函数生成该类型的值，也无法通过模式匹配拆解该类型的值。
• 这种设计可以强制外部代码只能通过模块官方暴露的接口操作该类型，从根源上避免外部代码随意构造非法值、破坏类型内部约束的问题。
• 这个定义上的三个类型参数属于典型的*幻影类型（Phantom Type）*参数：这三个类型不会出现在类型值的运行时存储结构里，纯粹是编译期用来做类型校验的标记，对应Coq通用参数在语法解析、预处理、内核校验三个阶段的对应类型，靠OCaml的类型检查器在编译阶段拦住参数类型不匹配的错误，运行时不会带来额外开销。

这类类型的值构造方式 #

你不需要（也没有权限）直接通过构造函数生成tag类型的值，唯一合法的构造方式是调用所属模块对外暴露的专用构造接口。
以Coq Genarg模块中的tag类型为例：

• 模块内部对tag类型有完整的GADT实现，但所有构造函数都不对外暴露
• 模块本身预定义了对应三类内置通用参数的tag值，比如对应常规参数的rarg_tag、对应命名参数的narg_tag等，可以直接使用
• 如果需要自定义通用参数，调用模块提供的参数注册接口即可，接口会返回对应类型的合法tag值，全程不需要接触类型的内部结构。

补充说明：如果无构造函数的类型定义直接出现在实现文件（.ml）的顶层而非模块签名中，属于OCaml语法错误，编译器会直接报错——只有出现在签名里、将内部实现隐藏在对应模块中的抽象类型才是合法用法。

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