# What is meaning of 'type +'a t' and 'type -'a u'

I have often seen type declaration of the form
`'type +'a t'` and `'type -'a u'` in ocaml .mli files. What does `+` and `-` in front of the generic parameter do. From my little experiment, I am unable to discern any difference if `+/-` is removed from the from type declaration. I am unable to find the explanation in the manual.

Thanks.
B.

3 Likes

From the manual page on type declarations:

The type variables appearing as type parameters can optionally be prefixed by + or - to indicate that the type constructor is covariant or contravariant with respect to this parameter. This variance information is used to decide subtyping relations when checking the validity of :> coercions (see section 7.7.6).

For instance, type +'a t declares t as an abstract type that is covariant in its parameter; this means that if the type τ is a subtype of the type σ, then τ t is a subtype of σ t. Similarly, type -'a t declares that the abstract type t is contravariant in its parameter: if τ is a subtype of σ, then σ t is a subtype of τ t. If no + or - variance annotation is given, the type constructor is assumed non-variant in the corresponding parameter. For instance, the abstract type declaration type 'a t means that τ t is neither a subtype nor a supertype of σ t if τ is subtype of σ.

3 Likes

There’s also this blog post which explains things in more details.

4 Likes

It expresses how the type constructor `t` behaves respect to the subtyping relation. If you have a `+` then it preserves the subtyping relation, i.e. if `a <: b` then `a t <: b t`; but if you have a `-` then it reverses it, i.e. if `a <: b` then `b t <: a t`. You can see it also in this way: with a `+` the type constructor is an increasing function (from type to type) respect to subtyping ordering; with a `-` it is a decreasing function.

2 Likes

Is the variant type annotation (+/-) only useful if one uses polymorhpic variants? Is there any other way to establish subtype/parent relationship in ocaml - besides the OO features of course?

Yes, with the `private` keyword in module signature:

``````(* M.t is a subtype of int *)
module M : sig type t = private int val i : t end = struct type t = int let i = 1 end

M.i;;
- : M.t = 1

(M.i :> int);;
- : int = 1
``````
1 Like

In fact, covariance `+` annotation are also very useful outside of objects, plymorphics variants and private types due to the relaxed value restriction: if a type constructor is covariant in a type parameter, it is always safe to generalize it. There is a manual section on the subject. Note there is also a succinct description of variance there, but this part should be expanded and moved to a better place at some point in the future.

2 Likes

Ah, interesting. I use private type as an abstraction/encapsulation and data structure construction invariant mechanism but not to establish subtype relation. Thanks.

You’re right. A simple example where the covariance annotation matter for generalization:

``````module A : sig
type +'a t
val inject : 'a -> 'a t
end = struct
type 'a t = 'a
let inject x = x
end

module B = (A : sig type 'a t val inject : 'a -> 'a t end)

(* the type is generalized *)
A.inject [];;
- : 'a list A.t = <abstr>

(* the type is not generalized *)
B.inject [];;
- : '_a list B.t = <abstr>
``````

This is how the staged type is implemented in base with the right annotation in the interface.

2 Likes