为什么在此类型之前有加号？

Question

我正在浏览ocaml的标准库,并在map.ml文件中遇到了这段代码.

module type S =
  sig
    type key
    type +'a t
    val empty: 'a t'

我想知道为什么会这样type +'a t,为什么作者使用它而不是简单'a t.
它的行为很奇怪,我无法推断出它的用法.

# type +'a t = 'a list;;
type 'a t = 'a list
# type +'a t = +'a list;;
Characters 13-14:
  type +'a t = +'a list;;
               ^
Error: Syntax error

谢谢

Answer 1

为了建立Jeffrey的答案,开发人员在这里将抽象类型标记为协变的工作原因可能不会帮助您使用子类型(基本上没有人在OCaml中使用子类型,因为参数多态通常是首选),但要使用由于协变性抽象类型允许更多的多态性,所以类型系统的一个更为人熟知的方面称为"宽松值限制".

您可以安全地忽略这些微妙之处,直到有一天,您遇到的问题与您的抽象类型不同,并且您应该记住签名中的协方差注释可能会有所帮助.

我们几个月前在reddit/ocaml上讨论过这个问题:

请考虑以下代码示例:

module type S = sig
  type 'a collection
  val empty : unit -> 'a collection
end

module C : S = struct
  type 'a collection =
    | Nil
    | Cons of 'a * 'a collection
  let empty () = Nil
end

let test = C.empty ()

你得到的类型test是'_a C.collection,而不是'a C.collection你期望的类型.它不是多态类型('_a是一个尚未完全确定的单态推理变量),在大多数情况下你不会满意.

这是因为C.empty ()它不是一个值,所以它的类型不是一般化的(〜多态).要从宽松的值限制中受益,您必须标记抽象类型'a collection协变:

module type S = sig
  type +'a collection
  val empty : unit -> 'a collection
end

当然这只会发生,因为模块C是用签名密封的S:module C : S = ....如果模块C没有给出明确的签名,那么类型系统将推断出最一般的方差(这里是协方差),并且人们不会注意到这一点.

针对抽象接口进行编程通常很有用(当定义仿函数,或强制执行幻像类型规则或编写模块化程序时),因此这种情况肯定会发生,因此了解宽松值限制是有用的.

如果你想理解这个理论,价值限制及其放松在2004年的研究文章" 放宽雅克·加里格的价值限制"中进行了讨论,他的前几页是对主题和主要观点的一个相当有趣和易于理解的介绍.

Answer 2

这将类型标记为与模块类型相关的协变量.假设您有两个键,它们的键类型相同.这+表示如果一个地图A的值是另一个地图B的值的子类型,则地图A的整体类型是地图B的类型的子类型.我在Jane Street博客中找到了很好的描述.