模块和存在之间的区别

Question

众所周知，OCaml 模块是 "just" 存在类型。

之间存在某种对等

module X = struct type t val x : t end

和

data 'a spec = { x : 'a }
data x = X : 'a spec

这并不完全是假的。

但正如我刚才所证明的，OCaml 既有模块又有存在类型。我的问题是：

它们有何不同？
有什么可以在一个中实现而另一个不能实现的吗？
你什么时候会使用一个而不是另一个（特别是比较 first-class 模块与存在类型）？

Answer 1

它是具有存在类型的具体抽象类型。我认为没有抽象类型的模块可以在没有存在主义的情况下得到解释。

模块具有抽象类型以外的特性：它们充当命名空间，它们是结构类型的，它们支持像 include 和 module type of 这样的操作，它们允许私有类型等。

一个显着的区别是函子允许在任何（固定）元数的类型上进行范围，这对于类型变量是不可能的，因为 OCaml 缺少更高种类的类型：

module type M = sig
  type 'a t
  val x : 'a t
end

我不太确定如何回答你的最后一个问题。模块和存在主义在实践中非常不同，以至于何时用一个代替另一个的问题还没有出现。

Answer 2

完成 gsg 对第三点的回答。

有两种使用模块的方式：

作为结构构造，当您声明顶层模块时。在那种情况下，您并不是真正在操纵存在变量。在 system-F 中编码模块系统时，您可以通过存在变量有效地表示抽象类型，但从道德上讲，它更接近于新的单例类型。
作为一个值，当使用 first class modules 时。在那种情况下，您显然是在操纵存在类型。

存在类型的其他表示是通过 GADT's 和对象。（也可以将 existential 编码为 universal with records 的否定，但它的用法完全被第一个 class 模块取代）。

在这 3 种情况之间做出选择在一定程度上取决于上下文。如果你想为你的类型提供很多功能，你会更喜欢模块或对象。如果只有少数，您可能会发现模块或对象的语法太重，并且更喜欢 GADT。 GADT 还可以揭示您的类型的结构，例如：

type _ ty =
  | List : ty -> ty list
  | Int : int list

type exist = E : 'a ty * 'a -> exist

如果您处于那种情况，则不需要传播在该类型上工作的函数，因此您最终会得到一些使用 GADT 存在性的更轻量级的东西。对于模块，这看起来像

module type Exist = sig
  type t
  val t : t ty
end
module Int_list : Exist = struct
  type t = int list 
  let t = List Int
end
let int_list = (module Int_list:Exist)

如果您需要子类型化或后期绑定，请寻找对象。这通常可以用模块编码，但这往往很乏味。

模块和存在之间的区别

Difference between modules and existentials

module

ocaml

existential-type