Overriding with subtypes

Overriding with subtypes

[Gert Smolka]

It should be ok to override a method of type t
with a method of a subtype of  t.  In fact,
that happens in

class c  = object(self) method a = self end
class c' = object(self) inherit c method a = self method b = 1 end

since c' is a proper subtype of c.  This is accepted by
Ocaml.  However,

class d  = object method a = new c end
class d' = object inherit d method a = new c' end

is rejected.  Why?  I would expect that this is a
limitation that is due to the type inferencer.

Gert Smolka

Re: Overriding with subtypes

[Didier.Remy]

Hi Gert,

> It should be ok to override a method of type t
> with a method of a subtype of  t.  

Yes, but this would require a form of bounded quantification.
The parent class should be typed with a class scheme of the form

        parent : Forall 'a < t. classtype ... t ...

so that the code is also correct when t is replaced by a subtype of t.

For simplicity, and because it is not essential, we don't have bounded
quantification in Ocaml but only ML-style polymorphism. 

> In fact, that happens in
> 
> class c  = object(self) method a = self end
> class c' = object(self) inherit c method a = self method b = 1 end
> 
> since c' is a proper subtype of c.  This is accepted by Ocaml.  

Yes it is accepted, but not for the reason you think.  Class c has type:

        class c : object ('a) method a : 'a end

This is a polymorphic in the row variable .. that appears in the implicit
type constraint 'a == < a : 'a; .. >

> However,
> 
> class d  = object method a = new c end
> class d' = object inherit d method a = new c' end
> 
> is rejected.  Why?  

Because the type of "new c'" is not an instance of the type of
"new c".  Indeed, "new c" has a closed type 'a == < a : 'a > without the
"..". This is a ground (recursive) type with no other instance but itself.

> I would expect that this is a
> limitation that is due to the type inferencer.

With explicit subtyping, you can type:

        class d'' = object inherit d method a = (new c' :> c) end

Class d' and d'' are operationally equivalent. However, d'' has type

        class d'' : object method a : c end

while you expected

        class d' : object method a : c' end

The later is be sound and should be typable with a form of bounded
quantification. This does not mean to be explicitly typed.  Extending Ocaml
with subtyping constraints is possible *in principle* and would preserve
type inference. Then, the above example could be accepted.  

    Didier.