Why there is a plus sign before this type?

Question

I was browsing ocaml's standard library, and came across this code in the map.ml file.

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

I'm wondering why there is type +'a t, and why the author use it instead of simply 'a t.
Its behaviour is strange and I can't deduce the usage of it.

# 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

Thanks

Answer 1

To build up on Jeffrey's answer, the reason the developers did the work of marking the abstract type as covariant here is likely not to help you use subtyping (essentially nobody uses subtyping in OCaml, as parametric polymorphis is generally preferred), but to use an even-less-well-known aspect of the type system called the "relaxed value restriction", thanks to which covariant abstract types allow more polymorphism.

You may safely ignore those subtleties until, someday, you hit a problem with an abstract type of yours that is not as polymorphic as you would like, and then you should remember than a covariance annotation in the signature may help.

We discussed this on reddit/ocaml a few months ago:

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.

If you want to understand the theory, the value restriction and its relaxation are discussed in the 2004 research article Relaxing the value restriction from Jacques Garrigue, whose first few page are a rather interesting and accessible introduction to the topic and main idea.