Re: Ocaml 2 object system origins

[Kim Bruce <kim@cs.williams.edu>]

Thanks for including me on the message list for this discussion of
O'Caml and LOOM.  Itn order to better understand the relationship
between the two, it might help to see how matching can be
defined in terms of higher-order subtyping.

Originally, matching was interpreted on the basis of F-bounded
polymorphism, but Abadi and Cardelli pointed out that it could
also be interpreted with higher-order subtyping.  Here is the basic
idea.

Suppose we have an object type of the form
    ObjectType{mi:Ti(MyType)}
where MyType is a keyword which stands for the type of self (or
this).  Form the record type of the methods where we replace all
occurrences of MyType by the parameter MT.
    M(MT) = {mi:Ti(MT)}
Thus M is a function from types to a record type.  This provides a
convenient notation for writing object types, as we can now write
them in the form ObjectType M(MyType).

Now we can give a simple definition of matching as
    ObjectType M'(MyType) <# ObjectType M(MyType)
iff
    for all MT, M'(MT) <: M(MT)
iff
    M' <: M
where we define subtyping on functions from types to types pointwise.
Thus one object type matches another iff if has all the methods of
the first (and perhaps more) plus the types of corresponding methods
are in the subtype relation.

This was the definition of matching in PolyTOIL (see my web page
at http://www.cs.williams.edu/~kim/  for links to papers).  My
impression is that this is more general than O'Caml because it allows
subtyping in types of existing methods.

In LOOM, we decided to simplify the language by omitting subtyping
altogether in favor of just using matching, and introducing something
called hash types (written #T) to provide the flexibility similar to
subtyping where desired.  Because subtyping was not defined in the
language it no longer made sense to allow subtyping of individual
methods.  At one point we had an elaborate scheme allowing
matching of corresponding method types, we abandoned this both
because it seemed too complex, and because we discovered that
in a language with MyType and match-bounded polymorphism,
this flexibility was rarely needed.  Hence the definition of matching
was restricted in LOOM, to simply mean extension.  Thus
    ObjectType M'(MyType) <# ObjectType M(MyType)
iff
    M(MyType) extends M(MyType)
(though the semantics is still given in terms of higher-order
subtyping).  Of course it is important to remember that if MyType
occurs in a negative position, then matching is not the same
as subtyping.  Thus if
    Node = ObjectType{setNext:MyType -> void;
                      getNext: void -> MyType}
and DoubleNode is the obvious extension with getPrevious and
setPrevious, then DoubleNode <# Node, but they are not subtypes
because of the occurrence of MyType as a parameter in setNext.

As Didier remarked, the two systems are similar, but we don't
know the exact relation between them.  Clearly the type inference
system makes a big difference.  On the one hand, they need to
explicitly indicate coercions with subtyping (though in fairness
we must indicate where we wish to allow subtyping by using hash
types), on the other hand, because types don't need to be written
down, their system has an easier time with tricky systems that
otherwise seem to require a mechanism to handle subclassing systems
where types are mutually recursive.  [Not being an expert in O'Caml,
I might have messed up the comparison - I'm sure Didier will
correct me if I'm wrong.]

I'd be interested if anyone successfully investigates the
relative expressiveness of the two systems.  I find it interesting
(and encouraging) that both groups came to somewhat similar
designs from very different origins.

    Kim

--

        Kim Bruce
        Department of Computer Science
        Williams College, Williamstown, MA 01267
        Kim@cs.williams.edu,   http://www.cs.williams.edu/~kim/