如果有的话，您需要向依赖类型系统添加啥来获得模块系统？

Posted 2023-03-16

【中文标题】如果有的话，您需要向依赖类型系统添加啥来获得模块系统？

【英文标题】：What, if anything, do you need to add to a dependent type system to get a module system?如果有的话，您需要向依赖类型系统添加什么来获得模块系统？

【发布时间】：2014-11-04 10:51:58

【问题描述】：

依赖类型系统似乎支持 ML 模块系统的某些用途。你从一个模块系统中得到了什么，而你没有从依赖记录中得到什么？

模块~记录

签名~记录类型

functor ~ 记录上的函数

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

我感兴趣的是它作为一个模块系统的工作情况，以及您是否以及如何集成应用函子和 mixins 等功能。

【问题讨论】：

我认为这是常见的翻译。我不记得具体例子和边缘案例的来源——如果有的话。

大多数依赖类型系统不支持子类型化，因此您需要添加。

您确定没有将存在类型与依赖类型混淆吗？

【参考方案1】：

首先，一些免责声明：

ML 系列中的不同语言对模块系统的实现有些不同。就此而言，相同语言的不同实现有区别。在这个答案中，我将只关注标准 ML 的定义（修订版）中指定的标准 ML。

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

我对依赖类型了解不多。我想我对他们的理解足以回答这个问题，但当然，我们并不总是知道我们不知道什么。 :-)

这类问题比看起来更主观，因为你“得到”的东西实际上算作什么并不总是很明显。

举个例子来说明我的意思：标准 ML 通过展示如何将其转换为 val rec ... 来定义 fun ...。所以你可以很容易地争辩说'fun'语法并没有给你任何东西，因为你可以用'fun'语法编写的任何东西都是你可以用'val rec'语法轻松编写的；但显然语言设计者认为它确实为你带来了一些东西——清晰、方便、干净等等——因为否则他们不会费心去定义这种他们清楚地理解为等价的形式。

对于模块系统尤其如此。标准 ML 模块的许多功能实际上只需标准 ML“核心”即可实现——甚至不需要依赖类型——除了模块提供了更令人愉快的语法并鼓励模块化设计。即使是与记录上的函数进行比较的仿函数，也不像常规函数，因为你不能在表达式中“调用”它们，所以它们不能出现在循环或条件中，它们不能调用自己递归地（这也很好，因为递归必然是无限的），等等。这是函子的限制，可能可以通过更通用的方法解决吗？或者更通用的方法是否会使按预期方式使用函子变得不那么愉快？我认为无论哪种方式都可以提出案例。

因此，我将仅介绍一些使标准 ML 模块能够胜任工作的功能，据我所知，这些功能并非由当前的依赖类型语言提供（即使它们是，不会是具有依赖类型的固有后果）。您可以自己判断哪些是真正“计数”的（如果有的话）。

---

值构造函数

一个结构不仅可以包含类型和值，还可以包含值构造函数，它们可以用于模式匹配。例如，你可以这样写：

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

模式使用结构中的值构造函数。我不认为依赖类型系统无法支持这一点的根本原因，但这似乎很尴尬。

同样，结构可以包含异常，同样的故事。

---

“开放”声明

open 声明将整个结构（所有值、类型、嵌套结构等）复制到当前环境中，该环境可以是***环境或较小的范围（例如 @987654325 @ 或 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 更清晰，更不容易出错，并且在面对未来的变化时更加稳健。

有些语言对记录有这种操作——例如，从 ECMAScript 2018 开始的 javascript 的扩展/剩余语法允许您将现有对象中的所有字段复制到新对象中，根据需要添加或替换——但是我不确定是否有任何依赖类型的语言。

---

灵活匹配

在标准 ML 中，结构匹配签名，即使它具有签名未指定的额外绑定，或者它具有比签名指定的更多多态的绑定等。

这意味着函子可以只需要它实际需要的东西，并且仍然可以与还具有函子不关心的其他东西的结构一起使用。 （这与常规函数相反；val first = # 1 只关心元组的第一个元素，但其类型必须准确指定元组中有多少元素。）

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

---

投影和抽象

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

这有效地“隐藏”了结构的各个方面，类似于在 C++ 或 Java 等语言中使用“私有”的方式。

您甚至可以通过更开放地定义结构，然后更严格地重新绑定相同的结构标识符来拥有“朋友”（在 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 模块如何服务于它们的预期目的。

---

嗯，这可能足以说明这个想法。如果您不觉得上述任何一项真正“重要”，那么列出更多功能可能不会改变这一点。 :-)