Comparing Object Encodings^{∗}

Kim B. Bruce  Luca Cardelli  Benjamin C. Pierce

June 8, 2001

Abstract

Recent years have seen the development of several foundational models for statically typed object-oriented programming. But despite their intuitive similarity, differences in the technical machinery used to formulate the various proposals have made them difficult to compare.

Using the typed lambda-calculus F_{<:}^{ω} as a common basis, we now offer a detailed comparison of four models: (1) a recursive-record encoding similar to the ones used by Cardelli [Car84], Reddy [Red88, KR94], Cook [Coo89, CHC90], and others; (2) Hofmann, Pierce, and Turner’s existential encoding [PT94, HP95]; (3) Bruce’s model based on existential and recursive types [Bru94]; and (4) Abadi, Cardelli, and Viswanathan’s type-theoretic encoding [ACV96] of a calculus of primitive objects.

1 Introduction

Over the last half decade, several authors have proposed foundational models for statically typed object-oriented programming. Although their motivating intuitions and technical machinery are all strongly related to typed lambda-calculi with subtyping [Car84, CW85, CG92], stylistic differences have made rigorous comparisons difficult. For example, some models are presented as translations from high-level object syntax into the syntax of a typed lambda-calculus; others map high-level syntax directly into a denotational model; still others focus on the object syntax as a primitive calculus in its own right.

In this paper we compare four of these models. The first of these, based on recursively-defined records, was introduced by Cardelli [Car84] and studied in many variations by Kamin and Reddy [Red88, KR94], Cook and Palsberg [CP89], and Mitchell [Mit90]. In its untyped form, this model was used rather effectively for the denotational semantics of untyped object-oriented languages. In its typed form, it was used to encode individual object-oriented examples, but had difficulties with uniform interpretations of typed object-oriented languages. The most successful effort in this direction was carried out by Cook et al. [CHC90, CCH^{+}89b].

In 1993, Pierce and Turner [PT94] introduced an encoding that relied only on a type system with existential types, but no recursive types. This led Hofmann and Pierce [HP95] to the first uniform, type-driven interpretation of objects in a functional calculus.

At the same conference in 1993, Bruce presented a paper [Bru94] on the semantics of a functional object-oriented language. This semantics was originally presented as a direct mapping into a denotational model of F_{<:}^{ω}, but has recently been reformulated as an object encoding that depends on both existential and recursive types.

∗Submitted to Information and Computation. Originally presented at TACS ’97, Sendai, Japan.

Meanwhile, frustrated by the difficulties of encoding objects in lambda calculi, Abadi and Cardelli introduced a calculus of primitive objects [AC96]. Later, however, Abadi, Cardelli, and Viswanathan [ACV96] discovered a faithful encoding of that object calculus in terms of bounded existentials and recursive types. (The encoding is simplified in this paper to facilitate comparisons with the other encodings; in particular, method update is only considered in Section 4.9).

In this paper we examine these object encodings and compare their strengths and weaknesses. Points of comparison include the expressiveness of the object-oriented constructs that can be encoded, the simplicity of the encoding, the uniformity of the encoding (e.g., independence of the encoding from the types of the objects and methods), and the power and proof-theoretic tractability of the underlying type theory used by the encoding.

We concentrate, throughout, on the lambda-calculus expressions that form the targets of the four encodings, eliding the associated “primitively object-oriented” source languages and the encoding functions mapping these into the lambda-calculus. (There are interesting comparisons to be made at this level too, but they are complicated by many inessential syntactic and stylistic differences between source languages.) Thus, the phrase “object encodings” in the title of the paper can be read as “object-oriented programming styles in typed lambda-calculus.”

We also stop short of considering classes and subclassing mechanisms. These are of course supported—in interestingly different ways—by all four encodings, but a detailed comparison falls outside the scope of this study.

Chapter 18 of [AC96] describes and compares several object encodings with respect to the object-oriented constructions that they can express and the properties that they enjoy. A main difference of approach in this paper is in the use of type operators to represent different encodings more uniformly. A paper by Fisher and Mitchell [FM96] (see also [FM94]) gives a general tutorial on type systems for object-oriented languages. It describes the origins and evolution of the recursive and existential encodings, and compares them with an axiomatic presentation of objects.

2 Technical Preliminaries

The “ambient type theory” in which our four encodings are expressed is the omega-order polymorphic lambda-calculus with subtyping, System F_{<:}^{ω} [Car90, CL91, PT94, HP95, PS97, Com94], extended with existential types [MP88], recursively defined types [AC93], recursive functions, and records. In the interest of brevity, we assume that readers have some prior familiarity with F_{<:}^{ω}, with recursive types, and with the use of existential types for information hiding à la Mitchell and Plotkin. (Prior familiarity with some of the encodings we discuss will also be helpful, but is not required.) In this section, we sketch the syntax of the language and briefly discuss a few technical points of particular relevance to what follows.

The sets of kinds, types, and terms are given by the following grammar:

K ::= Type  kind of types
| K->K  kind of type operators
T ::= X  type variable
| Fun(X:K)T  type operator
| T T  application of a type operator
| Top(K)  maximal type of kind K
| T->T  function type
| All(X)T  universally quantified type
| All(X<:T)T  bounded universal type
| Some(X)T  existentially quantified type
| Some(X<:T)T  bounded existential type
| Rec(X)T  recursive type

| {l:T...l:T}  record type

e ::= x  variable
| fun(x:T)e  abstraction
| e e  application
| fun(X<:T)e  type abstraction
| e T  type application
| pack [X,e] as T  existential package construction
| open e as [X,x] in e  existential package use
| {l=e...l=e}  record construction
| e.l  field selection
| let x=e in e  local definition
| letrec x(y:T):T = e in e  recursive local definition

We assume standard definitions of reduction and conversion, writing m=_{β}n to indicate that m and n are convertible. Although we shall perform conversion steps in whatever order is convenient for the sake of examples, we could just as well impose a call-by-name reduction strategy. (Most of the examples would diverge under a call-by-value strategy. This can be repaired, at the cost of some extra lambda-abstractions and applications to delay evaluation at appropriate points.)

We are informal about kinding throughout the paper. In particular, we omit kind declarations on type abstractions, writing Fun(X)T instead of Fun(X:K)T.

In the definitions of the encodings, we use pairs in addition to records; these can, of course, be encoded straightforwardly. We write (m,n) for the pair of m and n and use the selectors fst and snd to destruct pairs. S*T is the type of pairs of S and T.

Our formulation of existential types is standard, following (for example) Mitchell and Plotkin’s. If S is a type expression, then any element v with type of the form S[U/X] can be “packed” into

an element (pack [U,v] as Some(X)S) of type Some(X)S.

The expression (open o as [X,x] in b) unpacks the existential value o, yielding bindings for the type variable X and the term variable x, whose scope is the expression b. X represents the hidden, abstracted type, while x represents the term before it was packed. In particular, the

expression (open o as [X,x] in b) where o is (pack [U,v] as Some(X)S) will result in X being

bound to the type expression U and o to the expression v. In order to preserve type-safety, one may only apply operations to x that do not depend on knowing the actual hidden type bound to X.

The rules for introduction and elimination of existentials are the usual ones. Informally:

                          \frac{T=_{β}Some(X)S  ⊢ v : [X ↦ U]S}{(pack [U,v] as T) :  T}  (T-Pack)

                    \frac{⊢ o :  Some(X)S    x : S ⊢ b :  B    X∉ FV(B)}{(open o as [X,x] in b) :  B}  (T-Unpack)

Note the important side condition on the rule T-Unpack of existentials. If this side condition were dropped, then the hidden state X could “escape,” breaking the abstraction.

In examples, we use the informal pattern-matching notation

                             open o as [X,(s,m)] in b

to abbreviate

               open o as [X,x] in let s=fst(x) in let m=snd(x) in b.

For example the following defines a simple abstraction containing a value of type X and a function mapping type X to integers:

     abstr  =^{def} pack [{x:String},
                      ( {x="source"},
                        fun(s:{x:String}) length(s.x))]
                 as Some(X) X * (X -> Int)
             : OE(CellI)

We can use abstr by “opening” it and applying the second component to the first component:

     open abstr as [X,(x,f)] in f(x)

Because the type of f(x) does not involve X, this is legal according to T-Unpack. However, replacing f(x) by x or f(concat(x, "more")) is illegal according to T-Unpack as these changes would break the abstraction.

We can extend the subtyping relation to type functions (functions from types to types) by defining subtyping pointwise. Thus if F and G are type functions then F <: G iff for all types X,

F(X) <: G(X).

                             I(X)<:J(X) Fun(X) I(X)<:Fun(X) J(X)  (S-Abs)

Thus if G(X) = {bump:X, eq:X->Bool} and F(X) = {bump:X, eq:X->Bool, set:Int->X} then F
<: G.

The following folding and unfolding rules allow us to make use of recursive types:

                           Rec(X) I(X)<:I(Rec(X) I(X))  (S-Unfold)
                           I(Rec(X) I(X))<:Rec(X) I(X)  (S-Fold)

We will use these rules implicitly as needed rather than clutter the presentation.

The “Amber rule” is used to determine when recursively-defined types are subtypes:

                             \frac{X<:Y ⊢ I(X)<:J(Y)}{Rec(X) I(X)<:Rec(Y) J(Y)}  (S-Rec)

Note that this rule has a stronger premise than the pointwise subtyping rule for type operators above (S-Abs). Adopting a pointwise rule for recursive types (i.e., making Rec(X) I(X) a subtype of Rec(X) J(X) whenever I(X)<:J(X)) would render the type system unsound [AC93].

The letrec construct allows us to define terms using auxiliary functions (which may be defined recursively):

                        \frac{f:S->T, x : S ⊢ e : T    f:S->T ⊢ b :  B}{(letrec f(x:S):T = e in b) :  B}  (T-LetRec)

For subtyping quantifiers, we have a choice of rules. Some of our encodings will work fine with the kernel F_{<:} variant of the system; one needs the full F_{<:} rule. The following is the kernel rule for bounded polymorphic functions.

                              \frac{X<:A ⊢ D<:B}{All(X<:A)D<:All(X<:A)B}  (S-All-KFun)

Notice that the bounds on the parameters are identical for kernel F_{<:}. In the full F_{<:} system they are allowed to vary:

                              \frac{⊢ A<:C    X<:A ⊢ D<:B}{All(X<:C)D<:All(X<:A)B}  (S-All-Full-FSub)

The disadvantage of the full F_{<:} rule is that it makes the subtyping relation undecidable [Pie94] (as well as losing some other important properties, such as the existence of meets and joins).

3 The Encodings

Our running example throughout the paper will be (purely functional) integer reference cell objects.^{1} The interface of cell objects is represented by the following type operator:

    CellI(X)  =^{def} {get:Int, set:Int->X, bump:X}

Operationally, a cell object has three methods: get, which returns its current contents; set, which returns a new cell object (we intend that the contents of the resulting object should be set to the integer provided as a parameter, although of course the interface type doesn’t guarantee this); and bump, which returns a new cell (whose contents should be one greater than the current contents). The role of the parameter X varies between the encodings we consider, but it may be thought of intuitively as a placeholder for the “type of self.” Given an interface I, we write O(I) for the type of “objects with interface I.”

We are interested in the properties of O(I) for different values of O—i.e. for different ways of encoding objects with interface I. The four O’s that we consider in detail are:

1We concentrate here on the purely functional versions of each of the encodings. This choice aids both in formulating each of the systems (for example, it allows us to assume a call-by-name reduction strategy, avoiding some extra thunking for the corresponding call-by-value variants) and in later comparisons between systems.

              OR(I)    =^{def} Rec(X)                    I(X)
              OE(I)    =^{def}  Some(Y)    Y * (Y->I(Y))
              ORE(I)   =^{def} Rec(X) Some(Y)    Y * (Y->I(X))
              ORBE(I)  =^{def} Rec(X) Some(Y<:X) Y * (Y->I(Y))

OR is a “classical” recursive-record encoding. OE is the “existential encoding” of Hofmann, Pierce, and Turner [PT94, HP95]. ORE is a type-theoretic analog of Bruce’s denotational semantics for objects [Bru94]. ORBE is a variant of Abadi, Cardelli, and Viswanathan’s type-theoretic encoding [ACV96]. The names are designed to remind the reader of the main features of the encodings: R stands for recursive types, E for existential types, and BE for bounded existentials.

The use of type operators (rather than just types) to represent object interfaces is a way of capturing, uniformly, two different points of view about the types of the object’s methods: the “external view” of the object, in which the methods are abstract services that can only be invoked by an operation of “message sending,” and the “internal view” of the object when it is being created, in which the methods are concrete values. The internal view of the methods’ types varies from encoding to encoding (in two encodings I is applied to the recursively bound type variable X, while in the other two it is applied to the existentially bound variable Y.) On the other hand, the external view will always be the same:

    CellMessages  =^{def} O(CellI) -> CellI(O(CellI))
                  = O(CellI) -> {get:Int, set:Int->O(CellI),
                                   bump:O(CellI)}

That is, the messages supported by cell objects can be viewed as a collection of functions whose first parameter (the “self parameter”) is a cell object and whose results are described by CellI(O(CellI)). Of course, message sends will have to be interpreted differently in each of the object encodings in order to obtain this form.

It is technically convenient to write a single self parameter at the front of the whole collection of messages instead of abstracting each message individually on its self parameter. For example, for most of the paper we will assume that object interfaces are represented by covariant type operators, in which the bound variable appears only in positive positions. That is, each method of an object implicitly takes a single self parameter and can then return results of the self parameter type but not take any more arguments of this type. Section 4.7 discusses the implications of relaxing this restriction to allow “binary” methods with parameters of the same type as the receiver. See [BCC^{+}96] for a more extended discussion.

Note that all of these encodings need to be combined with some kind of higher-order bounded quantification to provide satisfactory typings for functions manipulating objects. For example, a function that accepts a cell object and sends it the bump message twice is given the type

    bumpTwice  :  All(I<:CellI) O(I) -> O(I)

capturing the fact that, if it is applied to a colored cell object, the result will also be colored.

We now develop each of the encodings in detail, using the example of cells to illustrate each one.

3.1 OR: Recursive records

The encoding of recursive records is fairly straightforward:

          OR(I)  =^{def} Rec(X) I(X)

In this case an object is simply a recursive record in which each occurrence of X stands for the type of the entire record. Thus if T = OR(I) then T = I(T).

We can encode a cell object as follows:

     mycell = letrec mkobj(s:{x:Int}) : OR(CellI) =
                  { get = s.x,
                    set = fun(n:Int) mkobj({x=n}),
                    bump = mkobj({x=s.x+1}) }
                in
                  mkobj({x=0})
             : OR(CellI)

The recursive function mkobj creates a new object of type OR(CellI), given a value for the internal state.^{2}

Let us introduce the informal syntax o<=l for sending a message l to an object o. Because objects in this encoding are simply recursively defined records, message sending is represented by field selection (after unfolding the recursive type):

      o<=l  =^{def} o.l

It is easy to see that (mycell<=bump)<=get reduces to 1 as follows:

     (mycell<=bump)<=get
            =_{β} (mkobj({x=0})<=bump)<=get
            =_{β} ({ get = {x=0}.x,
                   set = fun(n:Int) mkobj({x=n}),
                   bump = mkobj({x={x=0}.x+1}) }.bump)<=get
            =_{β} mkobj({x=({x=0}.x+1)})<=get
            =_{β} mkobj({x=1})<=get
            =_{β} {x=1}.x

=_{β} 1

Instead of implementing bump by manipulating the state directly, suppose we want to implement it in terms of the other methods. We can write:

     mycell  =^{def} letrec mkobj(s:{x:Int}) : OR(CellI) =
                  let self = mkobj s in
                  { get = s.x,
                    set = fun(n:Int) mkobj({x=n}),
                    bump = self<=set(self<=get + 1) }
                in
                  mkobj({x=0})
             : OR(CellI)

It is easy to see by reducing the messages sent to self that this is equivalent to the original definition, above.

2Note that, if we wanted to enforce a call-by-value reduction scheme, it would be necessary to change the encoding of the bump field, as otherwise a call to mkobj would always diverge. One solution would be to convert the bump field to a function of no arguments returning an object.

3.2 OE: Existentials

In the next encoding, we treat objects as pairs of state (with type Y) and methods (with type Y->I(Y)), in which the state component is hidden from the outside and methods are functions that depend on the state. Thus

          OE(I)  =^{def} Some(Y) Y * (Y->I(Y))

where the bound type variable Y represents the hidden state. We can define a cell object as follows:

     mycell  =^{def} pack [{x:Int},
                      ( {x=0},
                        fun(s:{x:Int})
                          {get = s.x,
                           set = fun(n:Int) {x=n},
                           bump = {x=s.x+1} })]
                 as OE(CellI)
             : OE(CellI)

It is now slightly more complex to send messages as we must “unpack” elements of existential type before we can access their components. Simple message sends like get are encoded as:

      o<=get  =^{def} open o as [X,(s,m)] in m(s).get

That is, we open the existential, apply the method suite to the state, and then extract the appropriate method.

However, messages like bump that return new objects with updated internal state require a bit more, since the resulting object must be re-packed.

      o<=bump  =^{def} open o as [X,(s,m)] in
                     pack [X,(m(s).bump,m)]
                     as OE(CellI)

The extra pack in the translation follows from the fact that the return type of the method has type Y, rather than the object type. In order to yield a fresh object as result, the state returned by the method must be re-packaged (with the original methods and state type) as an existential value. With this abbreviation it is easy to see that (mycell<=bump)<=get evaluates to 1:

  (mycell<=bump)<=get
      = (open mycell as [X,(s,m)] in pack [X,(m(s).bump,m)]
                                        as OE(CellI))<=get
      =_{β} (pack [{x:Int},
                  ((methfun {x=0}).bump,
                   methfun)]
           as OE(CellI))
           <=get
      =_{β} (pack [{x:Int},
                  ({get={x=0}.x, set=fun(n:Int){x=n},
                    bump={x={x=0}.x+1}}.bump,
                   methfun)]

           as OE(CellI))
           <=get
      =_{β} (pack [{x:Int},
                  ({x={x=0}.x+1},
                   methfun)]
           as OE(CellI))
           <=get
      =_{β} (pack [{x:Int},
                  ({x=1},
                  methfun)]
           as OE(CellI))
           <=get
      =_{β} open
             (pack [{x:Int},
                    ({x=1},
                     methfun)]
              as OE(CellI))
          as [X,(s,m)] in m(s).get
      =_{β} (methfun({x=1})).get
      =_{β} {get={x=1}.x, set=fun(n:Int){x=n},
            bump={x={x=1}.x+1}}.get
      =_{β} {x=1}.x

=_{β} 1

where

    methfun  =^{def} fun(s:{x:Int}) {get=s.x, set=fun(n:Int){x=n},
                                 bump={x=s.x+1}}

Because the message-sending code has to repack the object after the send in the case of bump, but not in the case of get, message-sending boilerplate must be generated from types, rather than being defined independently of types (as in the other encodings). On the other hand, the call to mkobj in the set method of the OR encoding of cells—which performs essentially the same “repackaging”—is omitted in the OE encoding, so the method bodies themselves are more uniform than in OR (and the other two encodings to follow).

This encoding technique is closely related to semantic models of Abstract Data Types. See [MP88] for details. This encoding has also been adopted in [MMH96] in order to represent closures as objects in compilers.

In the simple encoding, the “bump” method has no access to the “set” and “get” methods—it’s only passed the state as a parameter. But, as for OR, we can also build mycell in such a way that bump is defined in terms of get and set. This time, though, we have to do it a little differently. It doesn’t help to send get and set to the whole object, since the result of set is then a whole object, while the bump method is supposed to return just an element of the state type. Instead, we build just the set of methods recursively:

     mycell  =^{def} letrec m (s:{x:Int}) : CellI({x:Int}) =
                            let selfmeth = m s in
                            {get = s.x,
                             set = fun(n:Int) {x=n},

                             bump = selfmeth.set (selfmeth.get+1)}
                 in
                   pack [{x:Int}, ({x=0},m)]
                   as OE(CellI)
             : OE(CellI)

Note that this encoding can be refined by using a bounded existential to expose some of the instance variables. (This idea will come back later!)

          OBE(X,R)  =^{def} Some(Y<:R) Y * Y->I(Y)

In this encoding we are revealing that the state is a subtype of some “public instance variables interface” R, but are not specifying exactly what the type of the state is.

3.3 ORE: Recursion and Existentials

The intuition behind the ORE encoding is similar to OE except that any methods that return new objects do the repacking of internal state themselves, rather than requiring that the sender do it. This eliminates the need for different encodings of o<=m depending on the type of m.

          ORE(I)  =^{def} Rec(X) Some(Y) Y * (Y->I(X))

As with OE, Y represents the state of the object, while the methods are functions that depend on the current state. Notice that the types of methods now are expressed in terms of X, the type of the entire object, rather than just the type of the Y component. This will make it easier for us to encode message sends in a more uniform way. Thus a method returning a value of type X is returning an object, not just its state component. As we shall see in Section 4.7, this also provides support for “binary methods.”

For convenience, define:

     close  =^{def} fun(internalObj:
                           {x:Int} * ({x:Int}->CellI(ORE(CellI))))
                  pack [{x:Int}, internalObj]
                  as ORE(CellI)

The function close takes a pair representing the state and method definitions (in general, of type Y * (Y->I(X)) and creates an object of type ORE(I) by hiding the type of the state.

Now define mycell as:

    mycell  =^{def} letrec methfun(s:{x:Int}) : CellI(ORE(CellI)) =
                         {get = s.x,
                          set = fun(n:Int) close ({x=n},methfun),
                          bump = close ({x=s.x+1},methfun)}
                in
                   close ({x=0},methfun)
            : ORE(CellI)

The function methfun takes a value s representing the state of an object and creates a record of methods in which each method uses s as the current state. The close function packages up a new state with the method definitions given by methfun, producing a new object of type ORE(CellI).

The fact that the methods set and bump use close to return objects of type ORE(CellI) is a key difference from the existential encoding, where these methods simply returned the updated state.

As in OR, message sending is interpreted uniformly,

      o<=l  =^{def} open o as [X,(s,m)] in (m(s)).l

but each method that returns an object must explicitly call close to repackage the internal state before it returns. (The call to close here corresponds to the call to mkobj in the OR encoding.)

The expression (mycell<=bump)<=get evaluates to 1 as before.

     (mycell<=bump)<=get
            = ((close ({x=0},methfun))<=bump)<=get
            =_{β} ((pack [{x:Int}, ({x=0},methfun)]
                  as ORE(CellI))<=bump)<=get
            =_{β} ((methfun {x=0}).bump)<=get
            =_{β} (close ({x={x=0}.x+1},methfun))<=get
            =_{β} (close ({x=1},methfun))<=get
            =_{β} (pack [{x:Int}, ({x=1},methfun)]
                 as ORE(CellI))<=get
            =_{β} (methfun {x=1}).get
            =_{β} {x=1}.x

=_{β} 1

We can implement bump in terms of set as follows:

    mycell  =^{def} letrec methfun(s:{x:Int}) : CellI(ORE(CellI)) =
                  let self = close (s,methfun) in
                     {get = s.x,
                      set = fun(n:Int) close ({x=n},methfun),
                      bump = self<=set (self<=get + 1)}
               in
                  close ({x=0},methfun)
            : ORE(CellI)

In this definition, s, with type {x:Int}, represents the state while self, with type ORE(CellI), represents an object with that state. As before, the methods set and bump both return values of

type ORE(CellI).

It is useful to compare this definition with the corresponding one for OR. The main difference is the splitting of the function mkobj of the earlier definition into two separate functions methfun and close. In essence, close allows the creation of new objects by simply packing a new state with an existing method suite rather than requiring the creation of a new recursively-defined record. Thus ORE makes an explicit distinction between the state component of the object—the part that changes in response to message-sends—and the methods themselves, which are constant. (Of course, OE makes the same distinction. In ORBE, on the other hand, it becomes somewhat blurred, especially in the variant with method update discussed in Section 4.9.)

3.4 ORBE: Recursion and Bounded Existentials

We can understand the ORBE encoding by starting with the OE encoding and working our way up to the more complex one.

The OE encoding makes no public commitment about the type of the state: we can choose the state to be a record of instance variables, as we have done so far, or an element of any other type, so long as we can write methods that operate on this state in the appropriate way. In particular, we can choose the state type to be the type of the object itself! This may seem a slightly strange thing to do, but note that it allows us to use the o<=l syntax in the definition of bump:

      mycell  =^{def} letrec mkobj(s:{x:Int}) : OE(CellI) =
                   let self = mkobj s in
                     pack [OE(CellI),
                       (self,
                        fun(self':OE(CellI))
                          {get = s.x,
                           set = fun(n:Int) mkobj {x=n},
                           bump = self'<=set (self'<=get + 1)
                          }
                       )]
                     as OE(CellI)
                 in mkobj {x=0}

It would be nice if we could use the more uniform encoding of message sending in OR and ORE. We can do this if we add a recursive definition of X while revealing only some of the information about the actual type of the object. Define:

          ORBE(I)  =^{def} Rec(X) Some(Y<:X) Y * (Y->I(Y))

In the implementation of mycell, Y will be the actual type ORBE(I) of the entire object, but we do not reveal this publicly. We can now define an object as follows:

    mycell  =^{def} letrec mkobj(s:{x:Int}) : ORBE(CellI) =
                  let self = mkobj s in
                     pack [ORBE(CellI),
                       (self,
                        fun(self':ORBE(CellI))
                          {get = s.x,
                           set = fun(n:Int) mkobj {x=n},
                           bump = self'<=set (self'<=get + 1)
                          }
                         )]
                      as ORBE(CellI)
                 in
                    mkobj({x=0})
      : ORBE(CellI)

With this more refined encoding we can now define message sends uniformly (with the same definition as in the ORE encoding):

            o<=l  =^{def} open o as [X,(s,m)] in (m(s)).l

As in ORE and OR, this external uniformity comes at the price of having to call mkobj at the end of each method that returns an updated object.

For example:

            mycell<=set
                  = open mycell as [X,(s,m)] in (m(s)).set
                  =_{β} fun(n:Int) mkobj {x=n}

Note that the assumption Y<:X is critically used in the typing of o<=bump: the body (m(s)).bump has minimal type Y, but in order to satisfy the side condition on the open rule for existential types, this has to be promoted to a Y-free supertype—i.e. ORBE(CellI). This subsumption works as long as Y appears in only positive positions.

4 Comparisons

Having presented these four models as encodings in a common notational framework, we are now in a position to begin comparing them along a number of dimensions.

4.1 Treatment of the self parameter

The four encodings represent four strategies for encoding objects. In OR, methods do not take an explicit self argument on invocation. Instead, self is implicitly bound by a recursive declaration when the object is constructed. In the other three encodings, an argument representing self is explicitly passed to the methods. In OE and ORE, the argument is just the “internal state” of the object, while in ORBE the argument is the whole object. In OE, methods that return a modified version of self (such as bump), return just the state part, while in ORE and ORBE, such methods return a whole object. Summarizing, we can say that, viewed from outside, self-returning methods in OR map unit to whole objects, in OE they map states to states, in ORE they map states to whole objects, and in ORBE they map whole objects to whole objects.

4.2 Protection of instance variables

A related point concerns the treatment of instance variables. In mainstream object-oriented language designs, there have been two quite distinct points of view about instance variables:

1. Instance variables are hidden internal state of the object, not available to outside meddling unless the object explicitly provides access/update functions to do so.

2. Instance variables are members of an object just like its methods, therefore accessible externally unless explicitly protected (via subsumption, etc.).

The first view is exemplified by Smalltalk [GR83], by the “objects as closures” line of objectoriented Scheme extensions [AR88, etc.], and by the “objects as greatest fixed points” school of specification and verification [Rei95, Jac96, etc.]. The second is characteristic of Simula [BDMN79], Beta [KMMPN87], C++ [Str86], and Java [AG96].

This dichotomy in the design space us another dimension for comparison between the four encodings.

In all four cases, one can choose the convention that the encoding from a high-level language should generate access/update functions for all the instance variables of an object, and then use subsumption to hide these as appropriate[Probably too cryptic — maybe we need an example? –Benli]. In other words, all four representations of objects can support #2.

As for #1, the OE and ORE encodings include an explicit account of hidden instance variables, while OR and ORBE do not—OR makes no mention of anything hidden at all, while ORBE makes explicit the fact that what’s hidden is the whole object, not just instance variables.

So, even though all the encodings can support #2, only two of them (OR and ORBE) are intended to support #2, while OE and ORE were designed with #1 in mind.

4.3 Same information, different packaging

The four encodings “represent the same kind of objects,” in the sense that an object in one of the encodings can be wrapped up into an object in any other encoding that reacts to messages in exactly the same way as the original. In two cases, the “wrapping procedure” is actually trivial:

           ORBE(I) <: OE(I)
           ORBE(I) <: ORE(I)

This shows that ORBE is the most revealing of the three encodings involving existential types, in the sense that OE and ORE can be viewed as variants of ORBE that make fewer public commitments about their implementation.

4.4 Full abstraction

A more subtle—and arguably less important—difference between the OR encoding and the encodings based on existentials is that, in the latter three, an “observing context” can perform operations on an object that do not correspond to sending messages and, in some cases, obtain some information about the internal implementation of the methods. With the OR encoding, the only test that an observing context can make of an object is to look at the results that are returned by its methods. In the existential encodings, the observer can also apply the methods to a divergent argument, giving it the power to discriminate between objects that cannot be told apart just by sending messages in the ordinary way. This represents a kind of failure of full abstraction for the existential encodings.

To see this, consider two very simple OE-objects

       a  =^{def} pack [Int, (0, l=fun(s:Int)5)] as OE(J)
       b  =^{def} pack [Int, (5, l=fun(s:Int)s)] as OE(J)

where

       J(X)  =^{def} {l:Int}.

The x messages of both objects yield the result 5. But internally, the code for x in a is a constant function, while the code for x in b is an identity function. This fact can be detected by the observer

       obs  =^{def} fun(o:OE(J))

                 unpack o as [X,(s,m)] in
                   m.x(bottom(X))

where bottom(X) is a divergent computation of type X, such as:

       bottom(X)  =^{def} letrec f(n:Int) : X = f(n)
                       in f(0)

Then the test obs(a) yields 5 (assuming a call-by-name reduction strategy), whereas obs(b) diverges. On the other hand, if we construct OR-objects analogous to a and b, this difference disappears, since the observer can only see the result of the x method: it cannot test it by applying its internal implementation to divergent arguments. Similar examples can be constructed for ORE and

ORBE.

Thus, OR has a claim to being the tightest encoding of the four, in the sense that the type OR(I) does not allow an observer to test the behavior of an object’s methods directly by applying them to arguments other than the intended self parameter.

Note that the failure of full abstraction described here applies only in the case of a call-by-name evaluation strategy, since, with call-by-value, applying the methods to bottom always diverges. Since all common object-oriented languages use call-by-value, the difference is probably not significant in practice.

4.5 Uniform methods vs. uniform message sending

Another difference between the encodings is whether they choose to impose the burden of repackaging states into whole objects on the code that sends messages to objects (OE) or on the bodies of methods inside objects (OR, ORE, and ORBE).

In ORE and ORBE, every message is sent by opening the packed object, applying the second (method) component to the first (state) component, and then extracting the appropriate field of the result. It is even easier in OR, since no existential unpacking is needed.

In OE, the encoding of message sending depends on the type of the method. If there is no occurrence of the “self type variable” (the bound variable of the type operator representing the interface signature) in the result type, then message sends are encoded as for ORE and ORBE. However if the return type is the self type variable, then the result of the method must be repackaged as a new existential value (of type OE(I)).

However, in OR, ORE, and ORBE, methods that yield updated objects must repackage the objects before returning, while methods returning other values such as numbers do not package their results.

In either case, this repackaging introduces some non-uniformity in the encoding, since methods that return objects must be treated differently from those that do not. For all of the encodings, it appears that the required packaging code can be generated automatically, based on the type of the method [HP95, Bru94]. For the extension of the ORBE encoding discussed in Section 4.9, a more uniform treatment is possible, in which the repackaging code is identical in all methods [ACV96].

4.6 Strength of underlying type theory

OE works in the “most elementary” type theory—F_{<:}^{ω} with the kernel F_{<:} subtyping rule. If classes and inheritance are omitted, the underlying calculus is even strongly normalizing.

All the other models require recursive types, which entail recursion and loss of strong normalization. All the models (including OE) use recursive values when adapted to allow method invocation through self—or, more generally, when extended with classes. In the presence of recursive values, the semantics of the type system becomes more challenging; recursive types also complicate the metatheory.

OR, OE, and ORE work fine with the kernel F_{<:} subtyping rule for quantifiers. ORBE requires the full F_{<:} rule, leading to a substantial increase in the theoretical complexity of the calculus [Ghe95, Ghe93] and the loss of some pragmatically desirable properties such as decidability [Pie94]. See [PS97] for more discussion of variants of this rule.

The stronger rule is needed in ORBE to validate the usual subtyping rule for object types. Recall that, in F_{<:}^{ω}, bounded existential are encoded in terms of bounded universals. When comparing two ORBE object types, the Amber rule must be used first on the recursive types, followed by a comparison of existential types where the existential bounds are different type variables. Therefore, a general rule for subtyping existential types with different bounds is needed. This rule is derivable from the full F_{<:}^{ω} rule for universals, but not from weaker rules.

Even if existentials are taken as primitive, with a strong subtyping rule, the resulting system has undecidable typing. Karl Crary has observed [personal communication] that it may be possible to ameliorate this deficiency in ORBE by introducing a single type constructor combining the behaviors

of Rec and Some.

4.7 Binary Methods

Another difference between the encodings concerns the treatment of binary methods—methods taking an argument of the same type as the receiver object. Consider the following object interfaces:

   CellI(X)      =^{def} {get:Int, set:Int->X, bump:X}
   EqCellI(X)    =^{def} {get:Int, set:Int->X, bump:X, eq:X->Bool}
   EqClrCellI(X) =^{def} {get:Int, set:Int->X, bump:X, eq:X->Bool, color:Color}

CellI is our running example of cells; EqCellI adds a method eq that takes a cell and compares its contents with the contents of the cell to which the eq message is sent; EqClrCell adds one more method (whose behavior is unimportant). The crucial difference between CellI and the other two operators is that CellI is covariant—that is, S<:T implies CellI(S)<:CellI(T)—which is not the case for EqCellI or EqClrCellI, which both contain occurrences of the bound variable X in contravariant positions. This section and the next explore the consequences of non-covariant operators as object signatures.

Unfortunately, neither the OE nor the ORBE encoding handles non-covariant interfaces satisfactorily. For example, consider the object type OE(EqCellI)—simple existential cell objects with equality methods:

     EqCell  =^{def} OE(EqCellI)
             = Some(Y) Y * (Y -> {get:Int, set:Int->Y, bump:Y,
                                    eq:Y->Bool})

We can create objects with this type exactly as we did in Section 3.2.

     myeqcell  =^{def} pack [{x:Int},
                        ( {x=0},
                          fun(s:{x:Int})
                            {get = s.x,
                             set = fun(n:Int) {x=n},
                             bump = {x=s.x+1},
                             eq = fun(s':{x:Int}) s.x = s'.x })]
                   as OE(CellI)
               : OE(CellI)

However, it is not possible to send eq messages to such objects in a way we would expect. Having unpacked the existential, applied the methods to the state, and projected out the eq field of the resulting record, we are left with a function that expects a parameter of the same state type. But the second cell object that we want to pass as argument has its own—possibly different—internal state type, so its internal state is not an appropriate argument. The same observation applies to ORBE(EqCellI) (even though the state type is partially known).

This defect can be repaired to some extent by manually introducing a recursion in the interface signatures, binding the contravariant occurrences of the “self variable,” and adding explicit object constructors:

   REqCellI       =^{def} Rec(J) Fun(X) {get:Int, set:Int->X, bump:X,
                                     eq:OE(J)->Bool}
   REqClrCellI    =^{def} Rec(J) Fun(X) {get:Int, set:Int->X, bump:X,
                                     eq:OE(J)->Bool, color:Color}

This step allows binary messages to be sent to objects, but involves a nontrivial extension to the ambient type theory, since it relies on a recursively defined type operator. Moreover, it destroys the important property of pointwise subtyping between interfaces: REqClrCellI is not a subtype

of REqCellI (whereas EqClrCellI is a subtype of EqCellI).

By contrast, with OR and ORE we can create objects with interfaces like EqCellI and EqClrCellI and send them messages exactly as before: support for binary methods is “built in.” We illustrate with the ORE encoding:

     myeqcell  =^{def} letrec methfun(s:{x:Int}): CellI(ORE(EqCellI)) =
                         {get = s.x,
                          set = fun(n:Int) close ({x=n},methfun),
                          bump = close ({x=s.x+1},methfun),
                          eq = fun(other:ORE(EqCellI))
                                               s.x = other <= get}
                in
                   close ({x=0},methfun)
            : ORE(EqCellI)

The type of myeqcell is

     EqCell  =^{def} ORE(EqCellI)
             = Rec(X) Some(Y) Y * (Y -> {get:Int, set:Int->X,
                                           bump:X, eq:X->Bool})
             = Some(Y) Y * (Y -> {get:Int, set:Int->EqCell,
                                    bump:EqCell, eq:EqCell->Bool})

Thus the message send myeqcell <= eq(othereqcell) will be well typed as long as othereqcell has type EqCell. No changes are required to the definition of message sending in either OR or ORE in order to support these binary methods.

Thus the recursively-bound type variable in ORE (and OR) enables the definition and use of messages whose types involve both covariant and contravariant occurrences of the object type being defined. Because the ORBE encoding does not use the recursively-bound type variable in method types, it has the same difficulties as OE with binary methods.

Furthermore, since EqClrCellI is (pointwise) a subtype of EqCellI, we can write functions that manipulate both cells and colored cells with equality, by abstracting over subtypes of EqCellI:

    test5  =^{def} fun(I<EqCellI)
                 fun(o:ORE(I))
                   if o<=eq (o<=set(5)) then "o contains 5"
                                        else "doesn't"

4.8 Subtyping of Object Types

Unfortunately, the previous example would not work if we simply wrote

    test5'  =^{def} fun(C<OR(EqCellI))
                  fun(o:C)
                    if o<=eq (o<=set(5)) then "o contains 5"
                                         else "doesn't"

using an abstraction over types bounded by the object type OR(EqCellI) instead of the abstraction over type operators I bounded by EqCellI. While this simpler version is well typed as it stands, it is not very useful because OR(EqCellI) does not have any nontrivial subtypes!

In general, the pointwise subtyping relation I<:J between object interfaces does not imply that the corresponding object types OR(I) and OR(J) are in the subtype relation. (Nor, similarly, does it follow that ORE(I)<:ORE(J).) On the other hand, it does always follow that OE(I)<:OE(J) and ORBE(I)<:ORBE(J). The built-in support for binary methods in OR and ORE comes at the price of subtyping between object types in some cases. In particular, it will only be the case that I<:J

implies OR(I)<:OR(J) and ORE(I)<:ORE(J) when J is covariant.

This may or may not be viewed as a serious problem, since we can always write functions in the form of test5 instead of test5'. Indeed, variations on this style of “polymorphic programming by bounded abstraction over interfaces” have been proposed in several languages under the names matching, F-bounded quantification, and where clauses [BHJ^{+}87, CCH^{+}89a, BSvG95, AC95, BFP97, DGLM95].

4.9 Method Update

Method update can be added to encodings of the ORBE flavor, by extending the encoding with a collection of method updaters. These updaters take a sufficiently polymorphic new method and return an object with the new method in it [ACV96]. Forms of method update can be added also to encodings of the OR flavor. See [AC96, p. 268], and [San96].

These techniques work for certain presentations of the encodings, but do not adapt trivially to our presentation. However, there is hope of finding a systematic treatment of method update for all of our encodings. We leave this topic for further work.

5 Conclusions

Table 1 summarizes the major points of comparison between the four encodings we have considered. Interestingly, none of the columns completely dominates all of the others. However, we can make some broad comparisons.

There are two basic encoding techniques and two hybrids. The principal advantage of the basic techniques is straightforward intuition: OR represents the most naive view of objects as data values that can be interrogated by named messages; OE gives a lower-level picture, showing explicitly that objects consist of state and methods, with the state inaccessible except via the methods. The hybrid encodings—both of which can be viewed as deriving from OE—are more powerful, each offering a useful refinement: ORE adds support for binary methods, while a variation of ORBE was the first to support method update.

This paper is the beginning of a uniform treatment of most known encodings, but more work needs to be done. In particular, we intend to extend this treatment to method update and classes.

                              OR              OE           ORE            ORBE

responsibility for repackaging results method message sender method

method

internal access to “self methods” built-in can be added built-in

built-in

default protection of instance variables public private private

public

“fully abstract” yes no no

no

ambient type theory

F_{<:}^{ω} + Rec

pure F_{<:}^{ω}

F_{<:}^{ω} + Rec

F_{<:}^{ω} + Rec

quantifier subtyping Kernel F_{<:}

Kernel F_{<:}

Kernel F_{<:}

full F_{<:}

     \begin{matrix}I<:J ⇒ \\ O(I)<:O(J)? \end{matrix}

if J is covariant yes if J is covariant

yes

support for noncovariant interfaces yes limited, using extra Rec yes limited, using extra Rec

method update no no no

in a variant

Table 1: Summary of comparisons

It would also be useful to develop a simple object-oriented language supporting the constructs treated here and present its translation using each of these encodings.

6 Acknowledgments

Peter O’Hearn and Ramesh Viswanathan joined us in early discussions of the material presented here. O’Hearn was particularly helpful in understanding the circumstances under which “full abstraction” of the encodings will fail (cf. Section 4.4). Viswanathan contributed valuable insight into method update. Comments from Paul Steckler, Martín Abadi, and four anonymous referees helped us improve our presentation from an earlier draft.

Bruce was partially supported by NSF grant CCR-9424123. Pierce was partially supported by EPSRC grant GR/K 38403 and by NSF grant CCR-9701826.

References

[AC93] Roberto Amadio and Luca Cardelli. Subtyping recursive types. ACM Transactions on Programming Languages and Systems, 15(4):575–631, 1993.

[AC95] Martín Abadi and Luca Cardelli. On subtyping and matching. In Proceedings ECOOP ’95, pages 145–167, 1995.

[AC96] Martín Abadi and Luca Cardelli. A Theory of Objects. Springer-Verlag, 1996.

[ACV96] Martín Abadi, Luca Cardelli, and Ramesh Viswanathan. An interpretation of objects and object types. In Principles of Programming Languages, pages 396–409, 1996.

[AG96] Ken Arnold and James Gosling. The Java Programming Language. Addison Wesley, [AR88] Norman Adams and Jonathan Rees. Object-oriented programming in scheme. In

Proceedings of the 1988 ACM Conference on Lisp and Functional Programming, pages 277–288. ACM, ACM, July 1988.

[BCC^{+}96] Kim B. Bruce, Luca Cardelli, Giuseppe Castagna, the Hopkins Objects Group (Jonathan Eifrig, Scott Smith, Valery Trifonov), Gary T. Leavens, and Benjamin Pierce. On binary methods. Theory and Practice of Object Systems, 1(3):221–242, 1996.

[BDMN79] Graham M. Birtwistle, Ole-Johan Dahl, Bjorn Myhrhaug, and Kristen Nygaard. Simula Begin. Studentlitteratur (Lund, Sweden), Bratt Institut fuer neues Lernen (Goch, FRG), Chartwell-Bratt Ltd (Kent, England), 1979.

[BFP97] Kim B. Bruce, Adrian Fiech, and Leaf Petersen. Subtyping is not a good “match” for object-oriented languages. In ECOOP ’97, pages 104–127. LNCS 1241, Springer-Verlag, 1997.

[BHJ^{+}87] A. P. Black, N. Hutchinson, E. Jul, H. M. Levy, and L. Carter. Distribution and abstract types in Emerald. IEEE Transactions on Software Engineering, SE-13(1):65– 76, 1987.

[Bru94] Kim B. Bruce. A paradigmatic object-oriented programming language: Design, static typing and semantics. Journal of Functional Programming, 4(2), April 1994. A preliminary version appeared in POPL 1993 under the title “Safe Type Checking in a Statically Typed Object-Oriented Programming Language”.

[BSvG95] Kim B. Bruce, Angela Schuett, and Robert van Gent. PolyTOIL: A type-safe polymorphic object-oriented language, extended abstract. In ECOOP ’95, pages 27–51. LNCS 952, Springer-Verlag, 1995.

[Car84] Luca Cardelli. A semantics of multiple inheritance. In G. Kahn, D. MacQueen, and G. Plotkin, editors, Semantics of Data Types, volume 173 of Lecture Notes in Computer Science, pages 51–67. Springer-Verlag, 1984. Full version in Information and Computation 76(2/3):138–164, 1988.

[Car90] Luca Cardelli. Notes about F_{<:}^{ω}. Unpublished manuscript, October 1990.

[CCH^{+}89a] P. Canning, W. Cook, W. Hill, J. Mitchell, and W. Olthoff. F-bounded quantification for object-oriented programming. In Functional Prog. and Computer Architecture, pages 273–280, 1989.

[CCH^{+}89b] Peter Canning, William Cook, Walter Hill, Walter Olthoff, and John Mitchell. Fbounded quantification for object-oriented programming. In Fourth International Conference on Functional Programming Languages and Computer Architecture, pages 273–280, September 1989.

[CG92] Pierre-Louis Curien and Giorgio Ghelli. Coherence of subsumption: Minimum typing and type-checking in F_{≤}. Mathematical Structures in Computer Science, 2:55–91, 1992. Also in Carl A. Gunter and John C. Mitchell, editors, Theoretical Aspects of Object-Oriented Programming: Types, Semantics, and Language Design (MIT Press, [CHC90] William R. Cook, Walter L. Hill, and Peter S. Canning. Inheritance is not subtyping.

In Proc. 17th ACM Symp. on Principles of Programming Languages, pages 125–135, January 1990.

[CL91] Luca Cardelli and Giuseppe Longo. A semantic basis for Quest. Journal of Functional Programming, 1(4):417–458, 1991.

[Com94] Adriana B. Compagnoni. Decidability of higher-order subtyping with intersection types. In Computer Science Logic, September 1994. Kazimierz, Poland. Springer Lecture Notes in Computer Science 933, June 1995. Also available as University of Edinburgh, LFCS technical report ECS-LFCS-94-281, titled “Subtyping in F_{∧}^{ω} is decidable”.

[Coo89] William Cook. A Denotational Semantics of Inheritance. PhD thesis, Brown University, 1989.

[CP89] W. Cook and J. Palsberg. A denotational semantics of inheritance and its correctness. In Proc. ACM Conf. on Object-Oriented Programming: Systems, Languages and Applications, pages 433–444, 1989.

[CW85] Luca Cardelli and Peter Wegner. On understanding types, data abstraction, and polymorphism. Computing Surveys, 17(4), December 1985.

[DGLM95] Mark Day, Robert Gruber, Barbara Liskov, and Andrew C. Meyers. Subtypes vs. where clauses: Constraining parametric polymorphism. In Proc. ACM Symp. on Object-Oriented Programming: Systems, Languages, and Applications, pages 156– 168, 1995.

[FM94] Kathleen Fisher and John Mitchell. Notes on typed object-oriented programming. In Proceedings Theoretical Aspects of Computer Software, pages 138–150. Springer LNCS 789, 1994.

[FM96] Kathleen Fisher and John Mitchell. The development of type systems for objectoriented languages. Theory and Practice of Object Systems, 1(3):189–220, 1996.

[Ghe93] Giorgio Ghelli. Recursive types are not conservative over F_{≤}. In Typed Lambda Calculus and Applications, March 1993.

[Ghe95] Giorgio Ghelli. Divergence of F_{≤} type checking. Theoretical Computer Science, 139(1,2):131–162, 1995.

[GR83] Adele Goldberg and David Robson. Smalltalk-80: The Language and Its Implementation. Addison-Wesley, Reading, MA, 1983.

[HP95] Martin Hofmann and Benjamin Pierce. A unifying type-theoretic framework for objects. Journal of Functional Programming, 5(4):593–635, October 1995. Previous versions appeared in the Symposium on Theoretical Aspects of Computer Science, 1994, (pages 251–262) and, under the title “An Abstract View of Objects and Subtyping (Preliminary Report),” as University of Edinburgh, LFCS technical report ECS-LFCS-92-226, 1992.

[Jac96] Bart Jacobs. Inheritance and cofree constructions. In P. Cointe, editor, European Conference on Object-Oriented Programming (ECOOP96), number 1098 in Lecture Notes in Computer Science, pages 210–231. Springer-Verlag, 1996.

[KMMPN87] Bent Bruun Kristensen, Ole Lehrmann Madsen, Birger Møller-Pedersen, and Kristen Nygaard. The BETA programming language. In Bruce Shriver and Peter Wegner, editors, Research Directions in Object-Oriented Programming. The MIT Press, Cambridge, MA, 1987.

[KR94] Samuel N. Kamin and Uday S. Reddy. Two semantic models of object-oriented languages. In Carl A. Gunter and John C. Mitchell, editors, Theoretical Aspects of Object-Oriented Programming: Types, Semantics, and Language Design, pages 464– 495. The MIT Press, 1994.

[Mit90] John C. Mitchell. Toward a typed foundation for method specialization and inheritance. In Proceedings of the 17th ACM Symposium on Principles of Programming Languages, pages 109–124, January 1990. Also in Carl A. Gunter and John C. Mitchell, editors, Theoretical Aspects of Object-Oriented Programming: Types, Semantics, and Language Design (MIT Press, 1994).

[MMH96] Yasuhiko Minamide, Greg Morrisett, and Robert Harper. Typed closure conversion. In Proc. 23rd ACM Symp. on Principles of Programming Languages, pages 271–283, January 1996.

[MP88] J.C. Mitchell and G.D. Plotkin. Abstract types have existential type. ACM Trans. on Programming Languages and Systems, 10(3):470–502, 1988. Preliminary version appeared in Proc. 12th ACM Symp. on Principles of Programming Languages, 1985.

[Pie94] Benjamin C. Pierce. Bounded quantification is undecidable. Information and Computation, 112(1):131–165, July 1994. Also in Carl A. Gunter and John C. Mitchell, editors, Theoretical Aspects of Object-Oriented Programming: Types, Semantics, and Language Design (MIT Press, 1994). A preliminary version appeared in POPL ’92.

[PS97] Benjamin Pierce and Martin Steffen. Higher-order subtyping. Theoretical Computer Science, 1997. To appear. A preliminary version appeared in IFIP Working Conference on Programming Concepts, Methods and Calculi (PROCOMET), June 1994, and as University of Edinburgh technical report ECS-LFCS-94-280 and Universität Erlangen-Nürnberg Interner Bericht IMMD7-01/94, January 1994.

[PT94] Benjamin C. Pierce and David N. Turner. Simple type-theoretic foundations for object-oriented programming. Journal of functional programming, 4:207–247, 1994. An earlier version appeared in Proc. of POPL ’93, pp. 299-312.

[Red88] Uday S. Reddy. Objects as closures: Abstract semantics of object oriented languages. In Proceedings of the 1988 ACM Symposium on Lisp and Functional Programming, pages 289–297, Snowbird, Utah, July 1988.

[Rei95] Horst Reichel. An approach to object semantics based on terminal co-algebras. Mathematical Structures in Computer Science, 1995. To appear.

[San96] Davide Sangiorgi. Interpreting typed objects into typed pi-calculus (invited lecture). Available electronically through http://www.cs.williams.edu/∼kim/FOOL/

Abstracts.html, July 1996.

[Str86] Bjarne Stroustrup. The C++ Programming Language. Addison-Wesley, Reading, Mass, 1986.