Re: Overriding with subtypes

From: Didier.Remy@inria.fr
Date: Tue Aug 31 1999 - 15:48:08 MET DST


Date: Tue, 31 Aug 1999 15:48:08 +0200
From: Didier.Remy@inria.fr
To: Gert Smolka <smolka@ps.uni-sb.de>
Subject: Re: Overriding with subtypes
In-Reply-To: <37CAB746.950F452C@ps.uni-sb.de>; from Gert Smolka on Mon, Aug 30, 1999 at 06:54:30PM +0200

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.



This archive was generated by hypermail 2b29 : Sun Jan 02 2000 - 11:58:25 MET