Re: ocaml, inheritance vs. subtyping?

Ian T Zimmerman (itz@rahul.net)
Mon, 3 Jun 1996 23:51:30 -0700

Date: Mon, 3 Jun 1996 23:51:30 -0700
Message-Id: <199606040651.XAA04258@kronstadt.rahul.net>
From: Ian T Zimmerman <itz@rahul.net>
To: Didier.Remy@inria.fr
Subject: Re: ocaml, inheritance vs. subtyping?

In article <199606031649.SAA14505@pauillac.inria.fr>
Didier.Remy@inria.fr (Didier Remy) writes:

> I (itz) wrote this...:

> > I am somewhat perplexed by the passage in the manual on virtual
> > methods (pp. 29-30). Let's start with the first paragraph on p.30: it
> > says that int_comparable2 is not a subtype of int_comparable, even
> > though the former inherits from the latter! Now for a person with an
> > experience in a non-functional OO language (C++ or Eiffel or Sather)
> > it seems _very strange_ that the subtype and inheritance (derivation)
> > relations aren't the same.
>

> No their are intendedly not the same. This is one of the main
> problem with object orientation: subtyping and subclassing should
> not be identified. The are different notions. Inheritance is the
> ability to build a class from some older ones, and in particular to
> share its source and compiled code. The subclassing relation is
> defined between classes, and is purely syntactic. On the opposite,
> the subtyping relation is defined between types, and the coercions
> are defined between values, usually objects. The subtyping relation
> tells wether an object of some type can safely be considered as an
> object of another type. This is a more semantic concept.

OK, I now see that this is mainly a matter of terminology. What
you're saying is that subtyping and subclassing _as used by ocaml_ are
distinct. I already knew that when I wrote my post :-) But ocaml's
notion of subclassing is different from the one in C++ and Sather, and
the latter two simply DON'T HAVE this extra notion. So, the question
really is, what advantage is there in having it? Please read on
before responding.

> There is *no* relation between sub-classing and sub-typing as illustrated by
> the two following examples (You may read [1] for a longer discussion of
> this problem):
>
> Let first see an example of subclassing were subtyping fails: ;;
>
> class point x as self : 'mytype =
> val x = (x:int)
> method getx = x
> method equal (q:'mytype) = (self#getx = q#getx)
> end;;
>
> class color_point x c as self =
> inherit point x as super
> val c = (c : string)
> method getc = c
> method equal q = super#equal q && (self#getc = q#getc)
> end;;
>
> let p = new point 1;;
> let cp = new color_point 1 "color";;
>
> But, ;;
>
> (cp : color_point :> point);;
>
> complains with the error message:
>
> color_point is not a subtype of point
>
> Indeed, point is not a subtype of point_color. Otherwise, you could send the
> message equal to cp seen as a point and then pass it a point as argument, as
> in the following program:
> ;;
> (cp : color_point :> point)#equal p;;
>
> where the execution of method equal of cp would attempt to access the c
> field of the point p.
>

In C++ and Sather, a class _is a type_. The type of an object is
determined by its declaration, which mentions the class name. The
situation above cannot arise, because the class=type notion is
_enforced_ by the language semantics and you cannot override a method
by one with the wrong variance: this is done differently in each
language. Sather will just flag such a construction as erroneous,
which IMHO is by far the least error-prone way. C++ on the other side
will silently accept it, but will consider the method in the derived
class (the analogue of color_point#equal above) a completely _new_ and
semantically unrelated method (not an override). I can't say that I
like this way :-( but it does the job of keeping type safety.

> Conversely, you can easily define two classes that are not in a subclass
> relation, while the types of objets of those classes are always
> in a subtype relation: For example, define
> ;;
> class very_efficient_point x as self : 'mytype =
> val x = string_of_int x
> method getx = int_of_string x
> method equal (q:'mytype) = (self#getx = q#getx)
> end;;
>
> let q = new very_efficient_point 1;;
>
> Then the two classes point and very_efficient_point are unrelated.
> However, objects of those classes always have the very same type, and
> a fortiori have types in a subtype relation! Indeed, you can safely test
> them for equality:
>
> p # equal q;;
>

Hmmmm...strange...strange :-) I guess my misgivings are caused by
being used to _explicit_ typing and considering it The Good Thing, and
therefore also considering explicit _sub_typing Another Good Thing.
For a language based on type inference, other ehtics may be
appropriate :-)

> > It even seems that not having such an
> > overlap defeats the purpose of having OO features in the first place.

> I would rather say that identifying the two notions fools the user.
> In the past, the identification of the two notions resulted in big
> holes in some type systems of languages that were widely used (in
> the industry), generally by accepting the above incorrect example.

Like which languages? Not C++, as I noted above (although of course
C++ is full of other holes, so to speak :-))

> More recently, other languages choose to weaken their type system,
> thus forcing the user touse dynamic type cases (i.e. allowing a
> runtime failure) on examples that can be statically typed in O'caml.

Eiffel allows the example of covariant override above. I am not aware
of others. Sather, on the contrary, _tightened_ typing by disallowing
the renaming trap of C++ and permitting only real contravariant
overrides.

> > How is the programmer to predict where a subtype relation actually
> > exists?

> The subtyping relation in ocaml is quite standard [2]. A simple
> and efficient algorithm can be found in [3].

I have actually read [2]. But my point is not whether subtyping is
abstractly definable or mechanizable, but whether it is obvious and
explicit. If it isn't, programmers will rely on the compiler to
typecheck their code, instead of trying to get it right before
submitting it for compilation.

> > Second, and this may be the heart of the issue, _WHY_ is type 'a ->
> > bool inferred for leq, and not < x: unit -> int; .. > -> bool , as
> > it surely would for a global function?
>

> the type 'a -> bool was not inferred. It was a constraint put in the
> source code:

Of course, you're right here. My whole rave was based on an
oversight.

To finish let me return to the first paragraph. My question (and it's
just that, not a start of a language war) is what ocaml gains by
having a separate `structural' (as in structural vs. name equivalence)
notion of subtyping. You can allow covariant overrides like
color_point#equal. Is that good? The C++ person in me screams, NO
WAY! But one of these days, I'll kill him and become a happy ocamler.

-- 
Ian T Zimmerman           +-------------------------------------------+
Box 13445                 I When the dead are left to bury the dead,  I
Berkeley CA 94712 USA     I the living remain alone.  Arthur Koestler I
mailto:itz@rahul.net      +-------------------------------------------+