Re: co(ntra)-variant subtyping

[Didier Remy <remy@morgon.inria.fr>]

>    Objective Caml's subtyping algorithm does not subtype under type
>    constructors (but it does it under abbreviations), for the sake of
>    efficiency. That is, eventhough colored_point :> point, you don't have
>    colored_point option :> point option. This equation would be needed to
>    check the subtyping in method move of example 2.
>    
> I must say I am really surprised.  
> 
> How about object types? Do they support co(ntra)-variant
> subtype rules?

As Jacques said, subtyping sees through abbreviations.
Object types are abbreviations. 
They are covariant except when self-type occurs negatively, in
which case they are non-variant.

> I would suggest to include a section about the subtype relation
> in the ocaml documentation. 

We are aware that the documentation is too succinct. 
We will keep improving it. 

> Because IMHO anybody how knows
> something about formal models for oo languages would expect
> co(ntra)-variant subtype rules. 

I leave you this opinion.

Traditionally, people have heavily relied on subtyping polymorphism; they
run into serious difficulties because of the bad interaction between
recursion, late-binding and contra-variance. This lead to some mistakes
(some languages got it wrong). Moreover they still have difficulties with
binary methods.  For instance, even though Java is explicitly typed, it
fails to type binary methods: the type of self is weakened to the current
type of the class, which forces later useless and unsafe coercions (they may
fail, dynamically).

Instead, Objective Caml relies on parametric polymorphism.  This is easier to
explain, often more powerful (here, binary methods are not a problem) and
allows simple type inference. This is really what makes Objective Caml work.
Actually, Objective Caml does work with no subtyping at all, i.e.  polymorphic
message invocation, inheritance, binary methods, etc. all work without
subtyping.  Indeed, many examples do not use subtyping at all.

Still, Objective Caml allows subtyping because they are a few situations
when it is  convenient. Typically, when storing a collection of
objects of different subclasses of a common parent class into a bag.  Then,
only the operations of the parent class can be directly invoked on the
objects of the collection. (Actually, subtyping is independent from the
class hierarchy and objects do not need to be in an inheritance relation to
be put in the same collection.)

> In summary I think the lack of these subtype rules are a major
> restriction of the ocaml language. 

I am not convinced that the current restriction is such a burden. 
You are one of the first person to complain...

> Now it is not possible to mix
> class types and (algebraic) data types in an application. Instead
> a user has to decide beforehand what is more important for him:
> algebraic data types and parametric polymorphism or object types
> with code reuse and stepwise refinement.

Maybe you could detail your examples.

> Are there any plans to add the missing subtype rules to the type
> system of ocaml?

In fact, there is no real difficulty to allow subtyping through
user-declared type constructors.  However, when types are abstract (e.g. in
module interfaces) the user would need to declare the variances of the
constructors in their arguments.

We did not want to add yet another notion in the language, and therefore 
we prefered to make all non-primitive type constructors non variant.

   Didier