If you’ve ever wondered what it means in OCaml when there is a + or - in front of a type variable, read on.

OCaml has subtyping, which is a binary relation on types that says roughly, if type t1 is a subtype of type t2, then any value of type t1 can be used anywhere a value of type t2 was expected. In OCaml, subtyping arises from polymorphic variants. For example, [ A ] is a subtype of [ A | B ] (typographical note: in this post, polymorphic variants are written without the leading grave accent (backtick) due to formatting issues). Why? Because if you have a piece of code that knows how to deal with A and B, well then surely it can deal with just A.

One can ask OCaml to check subtyping using a coercion expression:

(e : t1 :> t2)

For example:

let f x = (x : [ A ] :> [ A | B ])

A coercion expression actually does two things; it verifies that t1 is a subtype of t2, and causes the type of the entire expression to be t2.

Just as the OCaml typechecker has rules for deciding when a let expression or a function call typechecks, it has rules for deciding when the subtyping in a coercion expression is allowed. The subtyping rule for polymorphic variant types is clear – one polymorphic variant t1 is a subtype of another polymorphic variant t2 if every constructor in t1 also appears in t2 (and with the same type argument). OCaml then has rules to extend the subtyping relation to more complex types. E.g. for tuples the rule is

if t1 :> t1' and t2 :> t2' then (t1, t2) :> (t1', t2')

For example:

let f x = (x : [ A ] * [ B ] :> [ A | C ] * [ B | D ])

The rule for subtyping on tuples makes intuitive sense if you think about what code could do with a tuple – it can take apart the pieces and look at them. So, if a tuple has fewer kinds of values in both its first and second components, then code dealing with the tuple would still be fine.

For arrow types the subtyping rule is:

if ta' :> ta and tr :> tr' then ta -> tr :> ta' -> tr'

For example:

let f x = (x : [ A | B ] -> [ C ] :> [ A ] -> [ C | D ])

Again, the rule makes sense if you think about what code can do with a function that it has. It can feed the function arguments, and observe the results. So, if a function can accept more kinds of inputs or returns fewer kinds of outputs, then the code dealing with the function would still be fine.

For types in OCaml like tuple and arrow, one can use + and -, called “variance annotations”, to state the essence of the subtyping rule for the type – namely the direction of subtyping needed on the component types in order to deduce subtyping on the compound type. For tuple and arrow types, one can write:

type (+'a, +'b) t = 'a * 'b
type (-'a, +'b) t = 'a -> 'b

One sometimes hears the term “covariant” to describe to a type variable annotated with a + and “contravariant” to describe to a type variable annotated with a -. For example, the tuple type is covariant in all its arguments. The arrow type constructor is contravariant in its first argument and covariant in its second argument.

If you don’t write the + and -, OCaml will infer them for you. So, why does one need to write them at all? Because module interfaces are designed to express the contract between implementor and user of a module, and because the variance of a type affects which programs using that type are type correct. For example, suppose you have the following:

module M : sig
  type ('a, 'b) t
end = struct
  type ('a, 'b) t = 'a * 'b
end

Should the following typecheck or not?

let f x = (x : ([ A ], [ B ]) M.t :> ([ A | C ], [ B | D ]) M.t)

If one knows that ('a, 'b) M.t = 'a * 'b, then yes, it should type check. But the whole point of an interface is that a user only knows what the interface says. And it does not say that ('a, 'b) M.t = 'a * 'b. So in fact it does not type check.

Variance annotations allow you to expose the subtyping properties of your type in an interface, without exposing the representation. For example, you can say:

module M : sig
  type (+'a, +'b) t
end = struct
  type ('a, 'b) t = 'a * 'b
end

This will give enough information to the OCaml type checker to typecheck uses of M.t for subtyping so that the following will type check.

let f x = (x : ([ A ], [ B ]) M.t :> ([ A | C ], [ B | D ]) M.t)

When you use variance annotations in an interface, OCaml will check that the implementation matches the interface, as always. For example the following will fail to typecheck:

module M : sig
  type (+'a, +'b) t
end = struct
  type ('a, 'b) t = 'a -> 'b
end

Whereas the following will typecheck:

module M : sig
  type (-'a, +'b) t
end = struct
  type ('a, 'b) t = 'a -> 'b
end

Hopefully this sheds some light on a somewhat obscure corner of the language.