模块和存在之间的区别

Question

OCaml模块是"仅仅"存在类型的民间知识.两者之间有某种平等

module X = struct type t val x : t end

和

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

这并非完全不真实.

但正如我刚才所证明的那样,OCaml有模块和存在类型.我的问题是:

• 他们有什么不同？
• 有什么可以在一个而不是另一个中实现吗？
• 你什么时候使用一个(特别是比较一流模块和存在类型)？

Answer 1

它是具有存在类型的特定抽象类型。我认为，没有抽象类型的模块可以在没有存在主义的情况下进行解释。

模块具有抽象类型以外的功能：它们充当命名空间，它们是结构类型的，它们支持像includeand之类的操作module type of，它们允许私有类型等。

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

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

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

Answer 2

完成 gsg 对你的第三点的回答。

有两种使用模块的方式：

• 作为结构化构造，当您声明顶级模块时。在这种情况下，您并没有真正操纵存在变量。在 system-F 中对模块系统进行编码时，您可以通过存在变量有效地表示抽象类型，但从道德上讲，它更接近于新的单例类型。

• 作为一个值，当使用一流的模块时。在这种情况下，您显然是在操纵存在类型。

存在类型的其他表示是通过GADT和对象。（也可以用记录将存在性编码为通用的否定，但它的用法完全被一流的模块取代）。

在这 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)

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