types - 如果有的话，您需要向依赖类型系统添加什么才能获得模块系统？

Question

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

模块~记录

签名~记录类型

仿函数 ~ 记录上的函数

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

我对它作为模块系统的工作情况感兴趣，以及是否以及如何集成应用仿函数和 mixin 等功能。

Answer 1

首先声明一些免责声明:

ML 系列中的不同语言对模块系统的实现有些不同。就此而言，同一语言的不同实现存在差异。在这个答案中，我将专门关注标准 ML 的定义(修订版)中指定的标准 ML。

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

我对依赖类型的了解并不多。我想我对这个答案的理解已经足够了，但是当然，我们并不总是知道我们不知道的东西。 :-)

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

例如我的意思:标准 ML 定义 fun ...通过展示如何将其转换为 val rec ... .所以你可以很容易地争辩说，'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声明将整个结构(所有值、类型、嵌套结构等)复制到当前环境中，该环境可以是顶级环境或较小的范围(例如 local 或 let )。
这样做的一个用途是定义一个结构来丰富另一个结构(甚至“相同”结构，因为新的结构可以具有相同的名称，从而影响旧的绑定(bind))。例如，如果我写:

structure List = struct
  open List

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

那么 List 现在拥有它之前的所有绑定(bind)，以及一个新的 List.map(它可以替换之前定义的 List.map)。 (同样，我可以使用 include 规范来增加签名，但对于那个我可能不会重复使用相同的名称。)
当然，即使没有这个特性，你也可以写一系列的声明，比如datatype list = datatype List.list , val hd = List.hd等，从结构中复制所有内容；但我想你会同意 open List更清晰，更不容易出错，并且在面对 future 的变化时更加健壮。
有些语言对记录进行了这种操作——例如，从 ECMAScript 2018 开始，JavaScript 的传播/休息语法允许您将现有对象中的所有字段复制到新对象，根据需要添加或替换——但我不确定是否有任何依赖类型的语言有它。

灵活搭配
在标准 ML 中，结构匹配签名，即使它具有签名未指定的额外绑定(bind)，或者它的绑定(bind)比签名指定的多态性，等等。
这意味着仿函数可以只需要它实际需要的东西，并且仍然可以与具有仿函数不关心的其他东西的结构一起使用。 (这与常规函数相反；val first = # 1 只关心元组的第一个元素，但其类型必须准确指定元组中有多少个元素。)
在依赖类型的语言中，这相当于一种子类型关系。我不知道是否有任何依赖类型的语言有它——这不会让我感到惊讶——但肯定有些语言没有。

投影和抽象
继续上一点:当你将一个结构与一个签名匹配时，结果是(如果我可以简化一点)结构到签名指定的子空间的“投影”，即结构“减去”无论什么不是由签名指定的。
这有效地“隐藏”了结构的各个方面，类似于在 C++ 和 Java 等语言中使用“私有(private)”的方式。
您甚至可以通过最初更公开地定义结构，然后更窄地重新绑定(bind)相同的结构标识符来拥有“ friend ”(在 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 模块如何满足其预期目的。

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