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

[Alain Frisch <frisch@clipper.ens.fr>]

On Sun, 18 Nov 2001, Clemens Hintze wrote:

> - If you believe that contravariance isn't generally particularly
>   useful, as you stated in the mail before, why can I flag some type
>   with (-'a) stating this is contravariant? What sense does this make?

> - What exactly are types and subtypes in OCaml? You know, I am coming
>   mainly from the imperative world. There I use languages that makes
>   no distinction between classes and types. Is 'int' a subtype of
>   'float'? How can I decide if something is a subtype of another one?
>   I do not ask in sense of OO inheritance but in OCaml terminology.

If you don't do OO, you can live with OCaml without knowing what 'subtype'
means.

Types in Caml are syntactical expressions, whose full syntax is
given in section 6.4 of OCaml user's manual. As types may contain type
variables, there is a natural order 'less general' induced by
instantiating type variables. The type inference algorithm allows to
take instances, that is to use an expression of a more general type where
a less general type is expected. (this is an unaccurate description of the
algorithm).

What about objects ?  Let's have a look at:

# let f x = (x # value) + 1;;
val f : < value : int; .. > -> int = <fun>

The function f accepts any object with a method value (returning an int)
and possible others: the ".." really denotes a type variable that can
be instantiated to a row of other methods.

# class o = object method value = 2  method str = "abc" end;;
class o : object method str : string method value : int end
# f (new o);;
- : int = 3

Here ".." is instantiated with (str : string). This kind of type matching
allows to use objects with extra methods in a context that expects only
some methods. More precisely, it is the context that accepts more methods.

What you can't do with that is for instance:

# class o = object method x = 2  method y = "abc" end;;
class o : object method x : int method y : string end
# class p =  object method x = 3 end;;
class p : object method x : int end
# [new o; new p];;
This expression has type p = < x : int > but is here used with type
  o = < x : int; y : string >
Only the second object type has a method y


A list in OCaml is homogeneous: all the elements must have the _same_
type; you could say that [new o; new p] has type < x : int; .. > list,
but then ".." has to be unified with (y : string) and ()  [the empty
row of methods], which is impossible.

Here you have to help the type system, and coerce both objets
to a common supertype:

# type t = < x : int >;;
type t = < x : int >
# [(new o :> t); (new p :> t)];;
- : t list = [<obj>; <obj>]

Coercing to a supertype amounts to forget some methods (which is safe,
but never done automatically).

Now there is a subtyping relation on object types. But it is handy to have
it also on constructed types:

# let l1 = [new o; new o] and l2 = [new p; new p];;
val l1 : o list = [<obj>; <obj>]
val l2 : p list = [<obj>; <obj>]
# (l1 :> t list) @ (l2 :> t list);;
- : t list = [<obj>; <obj>; <obj>; <obj>]

To make l1 and l2 compatible, we again use a coercion, but now, we use
the subtyping relation over lists:  "o list is a subtype of
t list _because_ o is a subtype of t". This express the covariance
of the list type constructor.

Some constructors are contravariant. For instance, the arrow constructor
t->s is contravariant in t and covariant in s. This means that:
t1->s1 is a subtype of t2->s2 if and only if t2 is a subtype
of t1 and s1 is a subtype of s2. If the arrow constructor was
considered covariant in both arguments, it would be easy to break
the type system (runtime type error) with a coercion.


And some constructors are invariant, such as:
type 'a inv = A of 'a | B of 'a -> unit

t1 inv is a subtype of t2 inv if and only if t1 and t2 are equal
(modulo the subtyping relation).


Now, if you don't have the definition of a type constructor - say
it is an abstract type from your point of view -
you can't tell what its variance is w.r.t one of its arguments.
So OCaml allows to specify this information in module interface;
for instance, in map.mli:

module type S =
  sig
    type key
          (* The type of the map keys. *)
    type (+'a) t
          (* The type of maps from type [key] to type ['a]. *)
...


The '+' means that type t is covariant: a map from type key to type
t1 can be coerced to a map from type key to type t2 if and only
if t1 is a subtype of t2.

(I don't know why other modules such as Queue do not give variance
information ...)


So, the subtyping relation is only raised from object types to
all types using variance information for each type constructor
(actually, subtyping can also appears with polymorphic variants).
There is no subtyping between basic types: int is not a subtype of float.

One reason for it is that in OCaml, coercion to a super type does not
require any computation, thanks to the concrete representation of objects.
So coercing a list does not involve walking through all its elements.
As int representation is not compatible with float one, int is not a
subtype if float.



-- 
  Alain

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