ocaml, inheritance vs. subtyping?

ocaml, inheritance vs. subtyping?

[Ian T Zimmerman]

Hi, I am just starting with ocaml, so please have mercy on a newbie
:-)

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.  It even seems that not having such an
overlap defeats the purpose of having OO features in the first place.
How is the programmer to predict where a subtype relation actually
exists?

Now the manual goes on to say that this occurs because `the self type
appears in contravariant position in the type of method leq'.  First,
am I right in decoding this as `the types of the argument of
int_comparable#leq and int_comparable2#leq are in covariant relation,
but they would have to be in contravariant relation for a subtyping
relation to exist between int_comparable and int_comparable2'?
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?

If these are stupid questions, I apologize again.  Maybe it's a sign
that the OO features need more explanation in the manual, though.

Best,

-- 
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      +-------------------------------------------+

Re: ocaml, inheritance vs. subtyping?

[Didier Remy]

> 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, the two relations are 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. 

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.

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;;

> 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.

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.

> 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]. 

> Now the manual goes on to say that this occurs because `the self type
> appears in contravariant position in the type of method leq'.  First,
> am I right in decoding this as `the types of the argument of
> int_comparable#leq and int_comparable2#leq are in covariant relation,
> but they would have to be in contravariant relation for a subtyping
> relation to exist between int_comparable and int_comparable2'?

You should rather read:

In order for the type of int_comparable2 to be a subtype of int_comparable,

    1/ int_comparable2#leq must be a subtype of int_comparable#leq, i.e. 
    (int_comparable2 -> bool) must be a subtype of (int_comparable -> bool)

    2/ by contra-variant propagation on the left side of the arrow, 
    int_comparable must be a subtype of int_comparable2

    3/ since set_x is a method of int_comparable2, 
    set_x must be a method of int_comparable

    4/ which is not the case.
    
Therefore, int_comparable2 is not a subtype of int_comparable. 


> 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:

        #class virtual comparable () : 'a =
        #  virtual leq : 'a -> bool
        #end;;
        class virtual comparable (unit) : 'a =
          virtual leq : 'a -> bool
        end

In this particular case, if you define, as you suggest:
                                                                        ;;
    class virtual 'a comparable () =
      constraint 'a = < x : int; .. > 
      virtual leq : 'a -> bool
    end;;

and leave int_comparable and int_comprable2 classes unchanged, then 
int_comparable2 would be a subtype of int_comparable. 

> that the OO features need more explanation in the manual, though.

Presently, the chapter on objects in the "Introduction in Objective Caml"
part of the manual is more a safety kit than an extended course on
objects. Still, it will probably be extended in a future release.

    -Didier.

[1] @incollection  (
  author       =   "William R. Cook and Walter L. Hill and Peter S. Canning",
  title        =   "Inheritance is not Subtyping",
  booktitle =    "Theoretical Aspects Of Object-Oriented Programming. 
                  Types, Semantics and Language Design",
  publisher =    "MIT Press",
  year =         1993,
  editor =    "Carl A. Gunter and John C. Mitchell")


[2] @inproceedings   (
author       =   "Roberto M. Amadio and Luca Cardelli",
title        =   "Subtyping Recursive Types",
booktitle    =   "Proceedings of the Eighteenth ACM Symposium on
                  Principles of Programming Languages", 
address      =   "Orlando, FL",
month        =   "January",
year         =   "1991",
pages        =   "104--118",
note         =   "Also available as DEC Systems Research Center
                  Research Report number 62, August 1990.  
                  To appear in TOPLAS")

[3] 
@inproceedings{Kozen-Palsberg/efficient-recursive-subtyping,
        author =        "Dexter Kozen and Jens Palsberg",
        title =         "Efficient Recursive Subtyping",
        booktitle =     "Proc. 20th symp. Principles of Programming Languages",
        year =          "1993",
        pages =         "419--428",
        publisher =     "ACM press"}

Re: ocaml, inheritance vs. subtyping?

[Ian T Zimmerman]

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      +-------------------------------------------+