依赖类型系统似乎支持一些ML模块系统的用途。使用模块系统可以得到什么,而使用依赖记录则得不到呢?
模块 ~ 记录
签名 ~ 记录类型
函数子 ~ 记录上的函数
带有抽象类型组件的模块 ~ 带有类型字段的依赖记录
我对这个作为模块系统的表现很感兴趣,以及如何集成可应用函子和混入等功能。
依赖类型系统似乎支持一些ML模块系统的用途。使用模块系统可以得到什么,而使用依赖记录则得不到呢?
模块 ~ 记录
签名 ~ 记录类型
函数子 ~ 记录上的函数
带有抽象类型组件的模块 ~ 带有类型字段的依赖记录
我对这个作为模块系统的表现很感兴趣,以及如何集成可应用函子和混入等功能。
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
include
规范来增强签名,但对于这个签名,我可能不会重复使用相同的名称。)datatype list = datatype List.list
,val hd = List.hd
等,以将结构中的所有内容复制出来; 但我认为您会同意open List
更清晰,更少出错,并且在未来的变化面前更加强大。灵活匹配
在标准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 ...
)。好的,这已经足够的例子来展示这个想法了。如果你觉得上面列举的任何一个都不算,那么再列举更多的功能也不会改变这一点。 :-)