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