Re: [Caml-list] [Q]: Co(ntra)variance and subtyping?

["Andreas Rossberg" <AndreasRossberg@web.de>]

> - What does subtyping exactly mean in OCaml resp. functional
>   programming?

OCaml has two separate notions of subtyping:

- in the core language, to support objects
- in the module language, for signature matching

While subtyping for module types is rather standard from a superficial point
of view, OCaml's treatment of subtyping in the core language is somewhat
special because it does not provide so-called subsumption. Subsumption means
that wherever a value of type t is expected you may freely provide a value
of some subtype t'. This is not the case in OCaml: you have to explicitly
coerce the value to the required supertype first. This is necessary to make
type inference feasible.

Note however that OCaml's object system rarely requires the use of
subtyping, because it mainly relies on row polymorphism, which is more or
less superior (although it admittedly complicates things to have both).

> - What means covariance and contravariance of types and subtypes?

Variance is a property of type constructor arguments. Take the "list" type
constructor for example: it is said to be covariant in its argument because
it comes with the following subtyping rule:

    t' < t     =>     t' list < t list

where "<" stands for "is subtype of". This means that you can use a t' list
as a t list - the list type "varies" in the same direction as its argument,
thus the term "covariance".

The most important type constructor is "->", which has the following
subtyping rule:

    t' < t and u' < u    =>    (t -> u') < (t' -> u)

Note the order of t and t' here: it goes in the opposite direction!
Functions are covariant in their result type, but contravariant in their
argument type. This may seem a bit funny at first (and in fact there are
major programming languages that still insist on getting it plainly wrong -
you already know one ;-) but it is the only sound rule. Intuitively it means
that a function type is a subtype of another function type if it produces a
more specific result while putting less requirements on its argument.

In general, you have covariance for type components that are "produced" or
"readable", and contravariance for components that are "consumed" or
"writable". Another example of contravariance would be a polymorphic output
channel.

Of course, you cannot have both co- and contravariance for the same
argument. So if some type component is both readable and writable then it
has to be invariant. Consider arrays for example: there is no subtyping
relation between any two array types t array and u array, no matter what
relation t and u are in (with the only exception of t=u, then of course you
trivially have `subtyping' in either direction). In fact, mutable types
always have to be invariant (another thing that many popular OO languages do
wrong - some at least do runtime checks for compensation, some just crash).

> OTOH, these terms seem to be very important in dealing with OCaml or
> functional programming.

I hope my explanations clarified that these terms are mainly important if
you do OO in the presence of polymorphic types. Functional programming in
its purer forms usually does not use nor require subtyping, so need not
bother with them ;-)

Cheers,

    - Andreas


-------------------
Bug reports: http://caml.inria.fr/bin/caml-bugs  FAQ: http://caml.inria.fr/FAQ/
To unsubscribe, mail caml-list-request@inria.fr  Archives: http://caml.inria.fr