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

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几个月前:

Consider the following code example:

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 ()

The type you get for test is '_a C.collection, instead of the 'a C.collection that you would expect. It is not a polymorphic type ('_a is a monomorphic inference variable that is not yet fully determined), and you won't be happy with it in most cases.

This is because C.empty () is not a value, so its type is not generalized (~ made polymorphic). To benefit from the relaxed value restriction, you have to mark the abstract type 'a collection covariant:

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

Of course this only happens because the module C is sealed with the signature S : module C : S = .... If the module C was not given an explicit signature, the type-system would infer the most general variance (here covariance) and one wouldn't notice that.

Programming against an abstract interface is often useful (when defining a functor, or enforcing a phantom type discipline, or writing modular programs) so this sort of situation definitely happens and it is then useful to know about the relaxed value restriction.

如果你想了解这个理论，值(value)限制及其放宽在2004年的研究文章 Relaxing the value restriction中讨论过。来自 Jacques Garrigue，其前几页是对主题和主要思想的相当有趣且易于理解的介绍。