如何在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进行的处理是声明一个不是抽象的类型，而是empty，将其表示形式公开为根本没有构造函数。不幸的是，OCaml对此没有很好的支持。在本地定义一种类型的能力（编译器可以告诉它为空）的能力有点怪异，manual中并未真正提及。无法在模块签名中表达“此类型为空”。

Answer 2

正如Ben所说，问题在于签名type t是抽象的而不是空的。一种替代方法是定义一个无人居住的类型：

module One = struct
  type never = { impossible : 'a . 'a }
  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
end

module Two = struct
  let get1 : bool One.t1 -> bool = function One.B1 -> true
  let get2 : bool One.t2 -> bool = function One.B2 -> true
end

这不会给出任何详尽的警告。

Answer 3

我今天遇到了同样的问题，并花费了大量时间寻找解决方案。正如Ben和gsg所说，确实是由于type never是抽象的事实。我认为，最优雅的解决方案是将其定义为私有变体。

type never = private Never

这解决了详尽性警告，并且很明显，您消除了创建此类变量的可能性。