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 JAA17049 for caml-redistribution; Tue, 14 Sep 1999 09:23:24 +0200 (MET DST) Received: from nez-perce.inria.fr (nez-perce.inria.fr [192.93.2.78]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id XAA09328 for ; Mon, 13 Sep 1999 23:43:11 +0200 (MET DST) Received: from orion.williams.edu (orion.williams.edu [137.165.4.6]) by nez-perce.inria.fr (8.8.7/8.8.7) with ESMTP id XAA26173; Mon, 13 Sep 1999 23:43:09 +0200 (MET DST) Received: from bull.cs.williams.edu (bull.cs.williams.edu [137.165.8.2]) by williams.edu (PMDF V5.2-32 #39697) with ESMTP id <0FI00093JPNUD8@williams.edu>; Mon, 13 Sep 1999 17:43:07 -0400 (EDT) Received: from cs.williams.edu (santacruz [137.165.8.104]) by bull.cs.williams.edu (8.9.3/8.9.3) with ESMTP id RAA11405; Mon, 13 Sep 1999 17:43:06 -0400 (EDT) Date: Mon, 13 Sep 1999 17:43:06 -0400 From: Kim Bruce Subject: Re: Ocaml 2 object system origins Sender: weis To: John Prevost Cc: Didier.Remy@inria.fr, caml-list@inria.fr Message-id: <37DD6FEA.25A0386C@cs.williams.edu> Organization: Williams College MIME-version: 1.0 X-Mailer: Mozilla 4.51 [en] (X11; I; FreeBSD 3.2-RELEASE i386) Content-type: text/plain; charset=us-ascii Content-transfer-encoding: 7bit X-Accept-Language: en References: <19990913151557.26714@morgon.inria.fr> 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/