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

["Marcin 'Qrczak' Kowalczyk" <qrczak@knm.org.pl>]

Disclaimer: I have no experience in OCaml's object system.

Sun, 18 Nov 2001 10:16:36 +0100, Clemens Hintze <cle-ocaml@qiao.in-berlin.de> pisze:

> - In the context you have mentioned above: 'invariant' means the two
>   types have *no* relationship to each other, yes?

Yes.

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

For a concrete type you have little choice: either the type definition
allows covariant changes of the parameter type (list is an example of
such type), or it allows contravariant changes (type 'a f = 'a -> unit
is an example), or it doesn't allows any changes (array is an example).
It follows either from type definition (in the case of algebraic types)
or from primitive operations provided (for primitive types).

The compiler infers variance of concrete types itself. Explicit
annotations are useful for concrete types where it's not yet known
which type will be substituted. Abstract types are invariant by
default and in such case any type can be substituted (you will be
able to make use of its variance only in places where it's known
which concrete type is used).

You can mark an abstract type as covariant and then only covariant
concrete types can be substituted when matching a module to a module
type. Similarly - contravariant.

A concrete type can also allow both variances (if the type variable
of its parameter is not used in its body). AFAIK there is no syntax
to mark abstract types as such - it has little use anyway.

> - What exactly are types and subtypes in OCaml?

Subtypes are generated by object types (by including more methods,
or having the same method names with subtypes as their types),
by using a subtype as a parameter to a covariant type, by using a
supertype as a parameter to a contravariant type, and from making
this relation reflexive and transitive.

I don't know if that's all. I'm not sure how polymorphic variant types
interact with this. They are surely covariant wrt. argument types,
but coercions which extend the type by including more variants can
be implicit - they don't need the :> operator.

-- 
 __("<  Marcin Kowalczyk * qrczak@knm.org.pl http://qrczak.ids.net.pl/
 \__/
  ^^
QRCZAK

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