为什么这个类型前面有一个加号？

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 中使用子类型作为参数通常首选多态性），但要使用类型系统的一个鲜为人知的方面，称为“松弛值限制”，这要归功于协变抽象类型允许更多的多态性。

您可以放心地忽略这些细微之处，直到有一天您遇到了一个抽象类型的问题，该类型不像您希望的那样具有多态性，然后您应该记住，签名中的协方差注释可能会有所帮助。

几个月前我们讨论过这个on 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 没有给出明确的签名，那么类型系统会推断出最普​​遍的方差（这里是协方差），而人们不会注意到这一点。

针对抽象接口进行编程通常很有用（在定义函子、执行幻像类型规则或编写模块化程序时），所以这种情况肯定会发生，然后了解放宽的值限制很有用。

如果您想了解该理论，价值限制及其放松在 Jacques Garrigue 的 2004 年研究文章Relaxing the value restriction 中进行了讨论，其前几页是对该主题和主要思想的相当有趣且易于理解的介绍。

Answer 2

这会将类型标记为与模块类型相关的协变。假设您有两个键是相同类型的映射。 + 表示如果一个映射 A 的值是另一个映射 B 的值的子类型，则映射 A 的整体类型是映射 B 的类型的子类型。我在Jane Street blog 中找到了一个很好的描述。