From mboxrd@z Thu Jan  1 00:00:00 1970
Received: (from weis@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id TAA26345 for caml-redistribution; Tue, 31 Aug 1999 19:15:59 +0200 (MET DST)
Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id PAA19627 for <caml-list@pauillac.inria.fr>; Tue, 31 Aug 1999 15:39:02 +0200 (MET DST)
Received: from morgon.inria.fr (morgon.inria.fr [128.93.8.33])
	by concorde.inria.fr (8.8.7/8.8.7) with ESMTP id PAA28444;
	Tue, 31 Aug 1999 15:39:01 +0200 (MET DST)
Received: (from remy@localhost)
	by morgon.inria.fr (8.8.7/8.8.7) id PAA20556;
	Tue, 31 Aug 1999 15:48:09 +0200
Message-ID: <19990831154808.63182@morgon.inria.fr>
Date: Tue, 31 Aug 1999 15:48:08 +0200
From: Didier.Remy@inria.fr
To: Gert Smolka <smolka@ps.uni-sb.de>
Cc: caml-list@inria.fr
Subject: Re: Overriding with subtypes
Reply-To: Didier.Remy@inria.fr
References: <37CAB746.950F452C@ps.uni-sb.de>
Mime-Version: 1.0
Content-Type: text/plain; charset=us-ascii
X-Mailer: Mutt 0.85e
In-Reply-To: <37CAB746.950F452C@ps.uni-sb.de>; from Gert Smolka on Mon, Aug 30, 1999 at 06:54:30PM +0200
Organization: INRIA, BP 105, F-78153 Le Chesnay Cedex
Phone: (33) 1 3963 5317 -- Sec: (33) 1 3963 5570 -- Fax: (33) 1 3963 5684
Web: http://cristal.inria.fr/~remy
Sender: weis

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.