types - 如何在 OCaml 中跨模块使用 GADT 而不会发出警告？

Question

我有两个文件:gadt1.ml 和 gadt2.ml，第二个取决于第一个。

gadt1.ml:

type never
type _ t1 = A1 : never  t1 | B1 : bool t1
type _ t2 = A2 : string t2 | B2 : bool t2
let get1 : bool t1 -> bool = function B1 -> true
let get2 : bool t2 -> bool = function B2 -> true

gadt2.ml:

let get1 : bool Gadt1.t1 -> bool = function Gadt.B1 -> true
let get2 : bool Gadt1.t2 -> bool = function Gadt.B2 -> true

当我使用 ocaml 4.02.3 ( ocamlbuild gadt2.native ) 进行编译时，我收到关于 Gadt2.get1 函数不详尽的警告 8。我很困惑 Gadt2.get1在 Gadt1.get1 时发出警告和 Gadt2.get2不。

我的假设是空类型 never不能等于 bool所以 Gadt2.get1不应发出警告。另一方面，如果我调用 Gadt2.get1带参数 A1 ，我得到一个类型错误(根据需要)。警告是预期的行为还是错误？我错过了什么？

顺便加个 -principal编译标志不会改变任何东西。

Answer 1

Gadt2只能看到Gadt1的界面，而不是它的实现。界面看起来像这样:

type never
type _ t1 = A1 : never  t1 | B1 : bool t1
type _ t2 = A2 : string t2 | B2 : bool t2
val get1 : bool t1 -> bool
val get2 : bool t2 -> bool

请注意 type never是抽象的——没有什么可以阻止一个实现给它一个 RHS。特别是，您可以在 gadt1.ml 中写入 type never = bool ，此时通过 A1 变得合理至 get1 ，等等 get1需要为这种可能性做好准备。

相比之下， string是一个非抽象类型:它有一个已知的表示，所以它不可能等于 bool ，等等 A2永远不能传递给 get2 .

你似乎想用 never 做什么is 声明了一个非抽象但为空的类型，将其表示暴露为根本没有构造函数。不幸的是，OCaml 并没有很好地支持它。定义本地编译器可以判断为空的类型的能力有点怪癖， manual 中没有真正提到。 .没有办法在模块签名中表达“这种类型是空的”。

更新:我相信这已经改变了，你现在可以写:

type never = |

表示 never确实是一个空类型，而不是抽象类型。