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

Learning
1

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
2

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 σ.

4 Likes
3

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

4 Likes
4

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
5

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?

6

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
7

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
9

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

10

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