OCaml, meaning of `!+` in `type `!+'a t`

Question

I'm currently learning about OCaml, and especially functors. I looked at map.mli from the standard library, and around line 70, there is :

type key
(** The type of the map keys. *)

type !+'a t
(** The type of maps from type [key] to type ['a]. *)

val empty: 'a t
(** The empty map. *)

I understand that key is the type of the key used in the map (or rather its signature, since we are in a .mli file), and 'a t is the (polymorphic/abstract) type of the map itself. However I am wondering what !+ is used for. I tried looking for some documentation about it but didn't found any unfortunately.

I would appreciate explanations regarding this, and/or a link to relevant documentation/tutorial if possible.

Thanks in advance.

Answer 1

Variance and injectivity annotations give back some information about the relationship between an abstract type constructor type 'a t and its argument. For instance, a type constructor could either

• produce or contain an 'a:

type 'a t = 'a * 'a

• consume an 'a

type 'a t = 'a -> unit

• ignore its argument all together:

type 'a t = int

• contain a viewable and mutable reference to 'a

type 'a t = { get: unit -> 'a; store: 'a -> unit }

All those type constructors can be abstracted away with a signature to:

module Any: sig
  type 'a t
end = struct
   type 'a t = 'a * 'a
end 

with this level of abstraction, we end up knowing nothing about 'a t in the outside world. However, sometimes it is useful to know a little more than nothing. For instance, if I have a producer type constructor 'a t, for instance

type 'a t = 'a * 'a

, and two types that are a related by a subtyping relation, let's say type x = < x:int > and type xy = <x:int; y:int > t. I can deduce from xy <: x that xy t <: y t because it is fine to pretend that the stored object has fewer methods than the one that was really produced. Since the order of the relation <: is preserved from xy :> x to xy t :> x t, we say that the type constructor t is covariant in its type parameter. And I can expose the fact that the type constructor is covariant in an interface by adding a variance annotation:

type xy = <x:int; y:int>
type x = < x:int >

module Covariant: sig
  type +'a t
  val xy: xy t
end = struct
  type +'a t = 'a * 'a
  let xy = let c = object method x = 0 method y = 1 end in c, c
end

let xy = (Covariant.xy: xy Covariant.t :> x Covariant.t)

In a dual way, if I have a type that consumes an object with a method x, for instance

type 'a t = 'a -> int
let x: x t = fun arg -> arg#x

it is fine to pretend that it requires in fact more methods. In other words, I can coerce a x t into a xy t reversing the relationship from xy:>x to x t :> xy t. And I can expose this information with a contravariant annotation

module Contravariant: sig
  type -'a t
  val x: x t
end = struct
  type -'a t = 'a -> int
  let x c = c#x
end

let xy = (Contravariant.x: x Contravariant.t :> xy Contravariant.t)

The use of + and - for contravariant reflects the rules that multiplying by a positive number preserve the ordinary order x < y implies that 2 x <2 y whereas multiplying by a negative number reverse the order: x < y implies that -2 y < -2x.

Thus the variance annotation allows us to expose how the type constructor t behaves with respect to subtyping. For concrete type definitions, the typechecker will infer the variance by itself and there is nothing to do. However, for abstract type constructor, it is the role of the author to expose (or not) the variance information.

This variance information is useful when dealing with objects, polymorphic variants or private types. But one may wonder if that matters much in OCaml, since objects are not used that much. And in fact, the main use for covariance annotation is relied to polymorphism and the value restriction.

The value restriction is a consequence of a destructive interference between polymorphism and mutability. The simplest example would be a function that generates a pair of functions to store or get some value from a reference

type 'a t = { get: unit -> 'a; store: 'a -> unit }
let init () =
  let st = ref None in
  let store x = st := Some x in
  let get () = match !st with None -> raise Not_found | Some x -> x
  in
  {store; get}

Typically, I can use like this:

let st = init ()
let () = st.store 0
let y = st.get ()

However, what is the type of st on the first line of the previous example. The type of init is unit -> 'a t because I can store any kind of value in the generated reference. However, the type of the concrete value st cannot be polymorphic, because I should not be able to store an integer and retrieve a function for instance:

let wrong = st.get () 0

Thus, the type of st is a weakly polymorphic type : '_weak1 t' where '_weak1 is a placeholder for a concrete type that can be replaced only once. Thus at line 2, the type of st, we learn that 'weak1=int and the type of t is updated to int t. This is the value restriction at play, it tells us that we cannot generally infer that the result of a computation is polymorphic. However, the issue only appear because with a store, we could both read and write a value of type 'a. If we can only read (or produce) a value of type 'a, it is fine to generalize a polymorphic value produced from a computation. For instance, in this example,

let gen_none () = None
let none = gen_None () 

surprisingly the inferred type for none is the fully polymorphic type 'a option'. Indeed, an option type 'a option is immutable container type that can only produce a value of type 'a. It is thus fine to generalize the type of the computation none is a from '_weak1 option to 'a option. And this where we meet again the variance annotation: being a container type that can only produce an 'a is one way to describe a covariant type parameter. And it is possible to prove more generally that if a type variable only appears in covariant position, it is always fine to generalize the type of that computation. This is the relaxed value restriction.

However, this happens because for a covariant type constructor 'a t', the only possible way to produce a polymorphic value is to have some kind of empty container. It can be quite fun to check that with OCaml type system :

type 'a maybe = Nothing | Just of 'a
type empty = |
type poly_maybe = { x: 'a. 'a maybe}
let a_polymorphic_maybe_is_nothing {x} = match (x:empty maybe) with
| Nothing -> ()
| _ -> .

To conclude on variance annotation, they are useful for container libraries to give their user the ability to

• coerce the whole container to a subtype with no-runtime cost
• compute polymorphic "empty" values

The use case of injectivity is a lot more subtle. In brief, they only matter when checking the exhaustiveness of some pattern matching in presence of GADTs (which explains why they were only introduced in OCaml 4.12).

Indeed, if variance annotations are concerned with the preservation of subtyping relationship, injectivity annotation are concerned with the preservation of inequality. Imagine that I have two distinguishable types, for instance int and float. Can I always distinguish an int t or float t? If I look at sum types

type !'a sum = A

or records

type !'a product = { x: 'a}

the answer is always yes. In other words, if I have 'a != 'b then both 'a sum != 'b sum and 'a product !='b product . This preservation of inequality is called injectivity. And I can add an injectivity annotation to check that the typechecker agrees with me (like variance annotations, injectivity annotations are inferred for concrete type definitions).

However, if the type parameter was in fact a phantom type parameter,

type 'a t = float

then I cannot guarantee that int t != float t (because _ t is always a float). For an example of a type constructor with a phantom parameter, I can define a type of float numbers with units with

type m = M
type s = S

module SI: sig
  type 'a t
  val m: m t
  val s: s t
end = struct
  type 'a t = float
  let m = 1.
  let s = 1.
end

Here, the type 'a SI.t represents a real number with a unit encoded in the type. So with this example, I have both injective and non-injective types. When does injectivity matters? And the answer is that for injectivity to matter I need to deal with explicit type equations. And explicit types equations are the domain of GADTs. The quintessential GADT is indeed the proof of equality witness

type ('a,'b) eq = Refl: ('a,'a) eq
let conv (type a b) (Refl: (a,b) eq) (x:a) = (x:b) 

having a value eq of type ('a,'b) t is a proof that two types are equal. For instance, I can use this type to export the fact that m SI.t and s SI.t are secretly the same type

module SI: sig
  type 'a t
  val m: m t
  val s: s t
  val magic: (s t, m t) eq
end = struct
  type 'a t = float
  let m = 1.
  let s = 1.
  let magic = Refl
end

and I can then use this secret equality to convert seconds to meters (which is bad)

let wrong_conversion (x:s SI.t) : m SI.t = 
  conv SI.magic x

Thus, I can use GADTs to expose the fact that a type constructor was not injective. Similarly, I can use an injectivity annotation to prove the other equivalent definition of injectivity: if 'a t = 'b t and t is injective in its first parameter then 'a = 'b:

module Inj(T: sig type !'a t end) = struct
  open T
  let conv (type a b) (Refl: (a t, b t) eq): (a,b) eq = Refl
end

All this is rather theoretical, but this issue of injectivity appears on more practical problem. Imagine that I have a container type vec

module Vec: sig
  type 'a t
  val v2: 'a -> 'a -> 'a t
end = struct
  type 'a t = 'a * 'a
  let v2 x y = x, y
end
type 'a vec = 'a Vec.t

(Note the missing injectivity annotation for now) With GADTs, I can define functions that work with either , int vec or float vec by defining the right GADT

type 'a monoid =
  | Int_vec: int vec monoid
  | Float_vec: float vec monoid 

For instance, I can define a zero function monoid by monoid:

let zero (type a) (kind:a monoid): a = match kind with
| Int_vec -> Vec.v2 0 0
| Float_vec -> Vec.v2 0. 0.

This works as expected. The trouble starts, once I want to define a function that works only on one of the possible monoids. For instance, only integer vectors have a finite number of elements of radius 1

let unit_circle (monoid:int vec monoid) = match monoid with
| Int_vec -> Vec.[v2 1 0; v2 (-1) 0; v2 0 1; v2 0 (-1)]

But then, we get an unexpected warning:

Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: Float_vec

This warning may seem strange at a first look Float_vec has type float vec monoid, which does not match with the int vec monoid type , and trying to apply unit_circle to Float_vec yields

let error = unit_circle Float_vec

Error: This expression has type float vec monoid but an expression was expected of type int vec monoid Type float is not compatible with type int

Thus the typechecker knows that a float vec is not compatible with an int vec. Why it is thus warning us about missing case in the pattern matching case? This issue is a question of context: when analyzing the pattern matching for exhaustiveness, the typechecker sees that the type 'a vec is not injective, and thus it cannot assume that there is not some hidden equations lying around that prove that in fact a float vec is the same as an int vec. Contrarily, in the application case, the typechecker knows that there is no such equation in the current context, and thus it ought to reject the application (even if there is such equation lying around somewhere).

The easy solution in our case is thus to add the missing injectivity annotation (we can add the missing variance too)

module Vec: sig
  type +!'a t
  val v2: 'a -> 'a -> 'a t
end = struct
  type 'a t = 'a * 'a
  let v2 x y = x, y
end
type 'a vec = 'a Vec.t
type 'a monoid =
  | Int_vec: int vec monoid
  | Float_vec: float vec monoid 

With this missing piece of information, the typechecker can conclude that an int vec is always different from a float vec and thus we don't have a warning anymore with

let unit_circle (monoid:int vec monoid) = match monoid with
| Int_vec -> Vec.[v2 1 0; v2 (-1) 0; v2 0 1; v2 0 (-1)]
| _ -> .

Indeed, since 'a vec is injective, we know that we can deduce int vec != float vec from the inequation int != float

To conclude on injectivity, an injectivity annotation is a way for a library to let its user know that even if a type constructor is abstract it does preserve inequalities. This is quite small piece of information, that doesn't leak much information. At the same time, it is only useful for clients that manipulate explicitly type equations through the use of GADTs.