如果要获得一个模块系统，您需要向依赖类型系统添加什么？

Question

依赖类型系统似乎支持一些ML模块系统的用途。使用模块系统可以得到什么，而使用依赖记录则得不到呢？

模块 ~ 记录

签名 ~ 记录类型

函数子 ~ 记录上的函数

带有抽象类型组件的模块 ~ 带有类型字段的依赖记录

我对这个作为模块系统的表现很感兴趣，以及如何集成可应用函子和混入等功能。

- Jules

---

我认为这是常见的翻译。如果有的话，我无法回忆起特定示例和边缘情况的来源。 - nlucaroni

大多数依赖类型系统不支持子类型，因此您需要添加该功能。 - Leo White

你确定你没有混淆存在类型和依赖类型吗？ - ivg

Answer 1

首先，有几点免责声明：

• ML家族中的不同语言在模块系统方面有着略微不同的实现。同样，相同语言的不同实现也存在差异。在本答案中，我将专注于《标准ML定义（修订版）》中规定的标准ML。

• 同样地，不同的依赖类型语言具有不同的特性。

• 我对依赖类型并不像我应该了解的那么多。我认为我理解它们足够回答这个问题，但是当然，我们并不总是知道我们不知道什么。:-)

• 这种问题比看起来更加主观，因为你“得到”的东西并不总是很明显。

  • 举个例子：标准ML通过展示如何将fun ...转换为val rec ...来定义它。因此，你可以轻松地争论'fun'语法并没有给你带来任何东西，因为你用'val rec'语法编写的任何内容都可以轻松地用'fun'语法编写；但显然，语言设计者认为它确实给你带来了一些东西——清晰度、方便性、整洁性等等——否则他们不会费心定义这个他们明显理解为等价的形式。

  • 对于模块系统来说，情况尤其如此。标准ML模块的许多特性实际上可以通过仅使用标准ML“核心”来实现——甚至不需要依赖类型——只是模块提供了更加愉悦的语法并鼓励模块化设计。即使是functors，你将它们与记录上的函数进行比较，也不完全像普通函数，因为你不能在表达式中“调用”它们，所以它们不能出现在循环或条件中，它们不能递归调用自己（这是很好的，因为递归必然是无限的），等等。这是functors的一个限制，可能通过更一般的方法修复吗？或者更一般的方法会使得使用functors的方式变得不那么愉快？我认为两种情况都可以成立。

  所以，我只会列出一些使标准ML模块在其工作中表现良好的特性，而根据我的有限知识，这些特性目前没有被当前的依赖类型语言提供（即使它们被提供了，也不会是具有依赖类型的固有后果）。你可以自己判断哪些，如果有的话，真正“重要”。

---

值构造函数

一个结构体不仅可以包含类型和值，还可以包含值构造函数，这些函数可以在模式匹配中使用。例如，您可以编写以下代码：

fun map f List.nil = List.nil
  | map f List.cons (h, t) = List.cons (f h, map f t)

当模式使用结构中的值构造函数时。我认为依赖类型系统并没有必要不支持这一点，但它似乎很别扭。

同样地，结构可以包含异常，也是如此。

---

'open'声明

open声明将一个结构的所有值、类型、嵌套结构等完全复制到当前环境中，可以是顶级环境或更小的范围（如local或let）。

其中一个用途是定义一个结构，以丰富另一个结构（甚至是“相同”的结构，因为新结构可以有相同的名称，从而遮蔽旧绑定）。例如，如果我写：

structure List = struct
  open List

  fun map f nil = nil
    | map f cons (h, t) = cons (f h, map f t)
end

然后，List现在拥有之前所有的绑定，加上一个新的List.map（可能会替换先前定义的List.map）。 （同样，我可以使用include规范来增强签名，但对于这个签名，我可能不会重复使用相同的名称。）

当然，即使没有这个功能，您也可以编写一系列声明，例如datatype list = datatype List.list，val hd = List.hd等，以将结构中的所有内容复制出来; 但我认为您会同意open List更清晰，更少出错，并且在未来的变化面前更加强大。

有一些语言对于记录具有此类操作 - 例如，JavaScript的spread / rest语法从ECMAScript 2018开始，允许您将所有字段从现有对象复制到一个新对象中，根据需要添加或替换 - 但我不确定是否有任何依赖类型的语言具有此功能。

---

灵活匹配

在标准ML中，一个结构即使有额外的绑定没有在签名中指定，或者它具有比签名指定的更多态的绑定等情况，也可以与签名匹配。

这意味着一个函数器只需要它实际需要的东西，就可以与也有其他函数器不关心的东西的结构一起使用。(这与常规函数不同;val first = # 1只关心元组的第一个元素，但它的类型必须明确指定元组中有多少个元素。)

在一个依赖类型的语言中，这将成为一种子类型关系。我不知道是否有任何依赖类型的语言有它——这不会让我感到惊讶——但肯定有一些没有。

---

投影和抽象

继续上一点：当您将一个结构与一个签名匹配时，结果是（如果我可以简化一下）该结构“投影”到由签名指定的子空间上，即结构“减去”签名未指定的任何内容。

这有效地“隐藏”了结构的某些方面，类似于您可能在像C++或Java这样的语言中使用“private”的方式。

您甚至可以通过最初更公开地定义结构，然后更窄地重新绑定相同的结构标识符来拥有“朋友”（在C++意义上）：

structure Foo = struct
  ...
end

... code with unfettered access to the contents of Foo ...

structure Foo = Foo :> FOO

... code with access only to what's specified by FOO ...

由于您可以非常精确地定义签名，因此在暴露内容和方式方面具有很高的细粒度。语法允许您即时完善签名（例如，FOO where type foo = int 是一个有效的签名表达式），并且因为通常希望保留所有类型而不使它们抽象化，所以有一个简单的语法（例如，Foo : FOO 大致相当于 Foo :> FOO where type foo = Foo.foo and type bar = Foo.bar and ...）。

在支持通过子类型进行灵活匹配的依赖类型语言中（如上所述），其中一些可能会与此结合起来；但我将其单独列出，并强调了语法上的便利之处，以突显标准ML模块如何服务于其预期目的。

---

好的，这已经足够的例子来展示这个想法了。如果你觉得上面列举的任何一个都不算，那么再列举更多的功能也不会改变这一点。 :-)

- ruakh