首先，一些免责声明：
\nML 系列中的不同语言对模块系统的实现有些不同。就此而言，同一语言的不同实现是有差异的。在这个答案中，我将专门关注标准ML 的定义（修订版）中指定的标准 ML 。
\n同样，不同的依赖类型语言也有不同的特性。
\n我对依赖类型的了解并不多。我想我对这个答案的理解足够了，但是当然，我们并不总是知道我们不知道什么。:-)
\n这类问题比看起来更主观，因为你“得到”的东西实际上算什么并不总是显而易见的。
\n举个例子来说明我的意思：标准 MLfun ...通过展示如何将其转换为val rec .... 因此，您可以很容易地认为“fun”语法不会“得到”您任何东西，因为您可以使用“fun”语法编写的任何内容都可以使用“val rec”语法轻松编写；但显然语言设计者认为它确实给你带来了一些东西 \xe2\x80\x94 清晰、方便、干净，无论 \xe2\x80\x94 因为否则他们就不会费心去定义这种他们清楚理解是等价的形式。
对于模块系统尤其如此。标准 ML 模块的许多功能实际上只需使用标准 ML“核心”\xe2\x80\x94 即可实现，不需要依赖类型，甚至不需要 \xe2\x80\x94，只不过模块提供了更令人愉快的语法并鼓励模块化设计。即使是与记录上的函数进行比较的函子，也不太像常规函数，因为您不能在表达式内“调用”它们，因此它们不能出现在循环或条件中，它们不能调用自身递归地（这也好，因为递归必然是无限的），等等。这是函子的限制吗？可以通过更通用的方法来修复吗？或者更通用的方法是否会让按照预期方式使用函子变得不那么愉快？我认为无论哪种方式都可以立案。
\n因此，我只会列出一些使标准 ML 模块擅长其工作的功能，而据我有限的知识，当前的依赖类型语言并没有提供这些功能（即使它们是，也不会提供）是具有依赖类型的固有后果）。您可以自己判断哪些（如果有的话）真正“重要”。
\n值构造器
\n结构体不仅可以包含类型和值，还可以包含值构造函数，可用于模式匹配。例如，您可以这样写：
\nfun map f List.nil = List.nil\n | map f List.cons (h, t) = List.cons (f h, map f t)\n其中模式使用结构中的值构造函数。我不认为依赖类型系统不能支持这一点有本质原因，但这似乎很尴尬。
\n同样，结构可以包含异常，这也是同样的情况。
\n“开放”声明
\n声明open将结构体 \xe2\x80\x94 的全部值、类型、嵌套结构等复制到当前环境中，该环境可以是顶级环境，也可以是较小的范围（例如local或let)。
其用途之一是定义一个丰富另一个结构的结构（甚至是“相同”的结构，因为新的结构可以具有相同的名称，从而隐藏旧的绑定）。例如，如果我写：
\nstructure List = struct\n open List\n\n fun map f nil = nil\n | map f cons (h, t) = cons (f h, map f t)\nend\n那么 List 现在拥有它以前拥有的所有绑定，再加上一个新的 List.map （它可能会替换以前定义的 List.map）。（同样，我可以使用include规范来增强签名，尽管对于该签名我可能不会重复使用相同的名称。）
当然，即使没有这个功能，您也可以编写一系列声明，例如datatype list = datatype List.list、val hd = List.hd等，以将所有内容复制到结构体中；但我想你会同意，这样open List更清晰，更不容易出错，而且面对未来的变化也更稳健。
有些语言对记录 \xe2\x80\x94 具有这种操作，例如，从 ECMAScript 2018 开始，JavaScript 的扩展/休息语法允许您将所有字段从现有对象复制到新对象，并根据需要添加或替换\xe2\x80\x94 但我不确定是否有任何依赖类型的语言有它。
\n灵活搭配
\n在标准 ML 中，结构与签名匹配，即使它具有签名未指定的额外绑定，或者如果它具有比签名指定的绑定更具多态性的绑定等。
\n这意味着函子可以只需要它实际需要的东西，并且仍然可以与还有函子不关心的其他东西的结构一起使用。（这与常规函数相反；val first = # 1只关心元组的第一个元素，但其类型必须准确指定元组中有多少个元素。）
在依赖类型语言中，这相当于一种子类型关系。我不知道是否有任何依赖类型的语言有它 \xe2\x80\x94 它不会让我感到惊讶 \xe2\x80\x94 但肯定有些没有。
\n投影与抽象
\n继续上一点：当您将结构与签名匹配时，结果是（如果我可以简化一点）结构到签名指定的子空间的“投影”，即结构“减去”任何东西签名未指定。
\n这有效地“隐藏”了结构的各个方面，类似于在 C++ 或 Java 等语言中使用“私有”的方式。
\n您甚至可以通过最初更开放地定义结构，然后更窄地重新绑定相同的结构标识符来拥有“朋友”（在 C++ 意义上）：
\nstructure Foo = struct\n ...\nend\n\n... code with unfettered access to the contents of Foo ...\n\nstructure Foo = Foo :> FOO\n\n... code with access only to what's specified by FOO ...\n因为您可以非常精确地定义签名，所以您在公开内容和公开方式方面具有高度的粒度。该语法允许您即时优化签名（例如，FOO where type foo = int是一个有效的签名表达式），并且由于通常希望保留所有类型而不使它们抽象，因此有一个简单的语法（例如，Foo : FOO大致等效）到Foo :> FOO where type foo = Foo.foo and type bar = Foo.bar and ...）。
在通过子类型支持灵活匹配的依赖类型语言中（上面），其中一些可能会与此结合在一起；但我将其单独列出，并指出了语法上的便利性，以强调标准 ML 模块如何服务于其预期目的。
\n嗯，这可能已经足够说明这个想法了。如果您不认为上述任何一项真正“重要”，那么列出更多功能可能不会改变这一点。:-)
\n