Ocaml 2 object system origins

Ocaml 2 object system origins

[John Prevost]

I just came across the paper "Typing in object-oriented languages:
Achieving expressiveness and safety" by Kim Bruce, and was struck,
once I referred back to the O'Caml documentation on the new object
system, by the similarities.

So, I was just wondering whether the features of the new object system
are based on this paper, a predecessor of this paper, or perhaps the
language LOOM, which apparently shares syntax with the examples in the
paper.

(The presence of # types seems too much to be chance.)

Thanks,

John Prevost.

Re: Ocaml 2 object system origins

[Jerome Vouillon]

On Mon, Sep 06, 1999 at 06:38:32AM -0400, John Prevost wrote:
> I just came across the paper "Typing in object-oriented languages:
> Achieving expressiveness and safety" by Kim Bruce, and was struck,
> once I referred back to the O'Caml documentation on the new object
> system, by the similarities.
> 
> So, I was just wondering whether the features of the new object system
> are based on this paper, a predecessor of this paper, or perhaps the
> language LOOM, which apparently shares syntax with the examples in the
> paper.

The two object systems was designed independently and are actually
very different, even though they seem to have roughly the same
expressive power.  For instance, O'Caml has no notion of "MyType" and
does not use a matching relation (<#). But these two notions can more
or less be expressed using recursive types and type instantiation.

> (The presence of # types seems too much to be chance.)

Indeed, I chose this syntax because the # abbreviations have
(very) roughly the same meaning as the # types of Kim Bruce.

-- Jérôme

Re: Ocaml 2 object system origins

[Didier.Remy]

> I just came across the paper "Typing in object-oriented languages:
> Achieving expressiveness and safety" by Kim Bruce, and was struck,
> once I referred back to the O'Caml documentation on the new object
> system, by the similarities.
> 
> So, I was just wondering whether the features of the new object system
> are based on this paper, a predecessor of this paper, or perhaps the
> language LOOM, which apparently shares syntax with the examples in the
> paper.

Dear John,

Not at all. You might read [3,4] (the Ocaml home page lists those under
"Related papers"). In particular [4] provides theoretical foundations for
O'Caml objects and a very brief comparison with LOOM.

More precisely, the design of O'Caml finds its origins in some of my earliest
works on type inference for extensible records [1, etc] and especially in an
experimental prototype called MLART described in [3].

In MLART, objects were not primitive but encoded, and a small OO in a
library was provided.  The OO library of MLART was about as expressive as
the OO constructs of O'Caml. It included multiple inheritance, binary
methods, etc. , and of course full type inference.  However, the lack of
syntactic sugar for classes and of an abbreviation mechanism made both
object types and typing errors unreadable.

Hence, an essential part of the design of O'Caml is its sophisticated use and
propagation of automatic abbreviations to keep type expressions relatively
small.  O'Caml also cut down a little on the expressiveness of the class
language of MLART, so as to improve readability of both types and typing
errors.  The OO layer of O'Caml is formally described in [4] except for the
recent redesign of the class language, which is inspired by [5].

The type system of O'Caml entirely relies on ML polymorphism.  The only
insignificant difference with ML is that types are taken modulo an
equational theory, and hence do not form a free algebra.  On the other hand,
the language LOOM uses a new notion called matching (<#) and primitive
self-types. It is folklore (but I don't think it has ever been checked
formally) that matching does not accomplish more than polymorphism over
row-variables.  As a result of this correspondence, the core languages
of LOOM and O'Caml have similar expressiveness. In particular, they both
handle binary methods, correctly.

However, there are several situations where O'Caml does much better than
LOOM.  An important difference is that O'Caml uses structural types, and
treats the type of self (almost) as any other type (and therefore classes
can abstract over the type of self). On the contrary, the type of self is a
primitive notion in LOOM, called "Mytype".  Some advanced examples such as
virtual types (that can be naturally defined in O'Caml ---see for instance
the subject/observer example in the documentation and in [7]) cannot be
written in LOOM. (However, a recent extension of LOOM with a notion of group
has been introduced to solve virtual types [6].)

Also, LOOM does not have multiple inheritance, but this could be added quite
easily.  LOOM does not have type-inference, which is, of course a major
difference.

> (The presence of # types seems too much to be chance.)

As Jerome said, we choice the same symbol as the one used for hash-types in
LOOM because of the resemblance. However, O'Caml #-types are regular types
(this is just a notation for an implicit row-variable) while hash-types are
a primitive notion in LOOM.

Best regards,

        -Didier

----------------

See <http://cristal.inria.fr/~remy/publications.html> for details.

[1] Type Inference for Records in a Natural Extension of ML. 

[3] Programming Objects with ML-ART: An extension to ML with Abstract and
Record Types.

[4] Objective ML: An effective object-oriented extension to ML.  (with
Jérôme Vouillon).

[5] Using modules as classes by Jérôme Vouillon.
<http://cristal.inria.fr/~vouillon/publi.html>

[6] Semantics-Driven Language Design: Statically type-safe virtual types in
object-oriented languages by Kim B. Bruce and Joseph Vanderwaart.
<http://www.cs.williams.edu/~kim/README.html>

[7] The reality of virtual types for free! (with Jérôme Vouillon).

Re: Ocaml 2 object system origins

[John Prevost]

Ahh.  Thanks very much--I recalled that there were some papers about
this, but poked around the web page a bit ineffectually.

On the topic of folklore and matching, you say:

> On the other hand, the language LOOM uses a new notion called
> matching (<#) and primitive self-types. It is folklore (but I don't
> think it has ever been checked formally) that matching does not
> accomplish more than polymorphism over row-variables.

Hmm.  My intuition on looking at the two systems is to believe that,
if anything, polymorphism over row-variables *might* be more powerful.

Unfortunately, the comparison is complicated, since LOOM allows
variables of type #foo, and in O'Caml #foo is a synonym for a
type-expression with an unbound type variable (implying that this type
must be unified to a single type except in polymorphic function
types.)  (It's so worrying when intuition can be confused in this
way.)

In any case, I'll have to do more reading and comparison now that I
have descriptions of both systems available to me.

Thanks very much for the excellent explanation.

John

Re: Ocaml 2 object system origins

[Kim Bruce]

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/