The Equivalence of Two Semantic Definitions for Inheritance in Object-Oriented Languages

Kim B. Bruce^{∗} Williams College kim@cs.williams.edu

Abstract

A simple language is presented which supports inheritance in object-oriented languages. Using this language, the definitions for the semantics of inheritance given in [CHC90] and [Mit90] are compared and shown to be equivalent. The equivalence is shown by presenting and comparing two denotational semantics of the simple language which capture the essence of each of the earlier semantics.

1 Introduction

The semantics of object-oriented programming languages appears to be much more subtle than might have originally been expected. In particular, the combination of inheritance, subtyping, and what is sometimes referred to as dynamic binding^{1} often lead to unexpected results, especially in the context of a strongly-typed language.

[CHC90] and [Mit90] have each provided slightly different explanations of inheritance within a typed framework. Each proceeds by translating constructs in object-oriented languages expressing inheritance into higher-order extensions of the typed lambda calculus. Computation takes place by rewriting terms according to the rewrite rules of the calculi.

While these translations are complex, they allow the authors to illustrate seemingly paradoxical results which arise when using inheritance. For example, [CHC90] is able to show that inherited types need not be subtypes of the starting types, highlighting problems with languages which confuse the notions of inheritance and subtyping.

An example given in [Mit90] illustrates the complexity of inheritance by presenting an example in which a user defines a subclass of a given class by inheriting from the parent class and then redefining one of the inherited methods. Depending on the internal (and often hidden) definitions of the remaining methods in the parent, the meanings of other methods inherited from the parent class may or may not themselves change (the key is whether the redefined method’s name is used in the definition of the other methods). This interaction of dynamic binding and inheritance must be handled rather carefully in specifying the semantics of object-oriented languages if the result is to reflect the desires of the language designers.

∗Part of this work was done while the author was on leave at the Computer Science Department, Stanford University and at the DEC Systems Research Center in Palo Alto, California. The author was partially supported by NSF grant CCR - 9105316 and a grant from the Williams College Division 3 & P Research Funding Committee.

1We realize that the name dynamic binding is not quite correct here. It has been described more accurately as “late binding” or “dynamic message dispatch”. We use “dynamic binding” throughout this paper since it is the more commonly used term.

In each of the above cited cases, the primary difficulty follows from the use of self (or equivalent features) in conjunction with dynamic binding. When self occurs in the body of a method which has been invoked on an object, self refers to that object. This self-reference gives rise to objects which are created as the fixed point of a function of self (i.e., self = F (self ) where F is the definition of the class whose methods may refer to self).

For example, suppose P oint is a class which includes the method move which is defined in terms of self. Let pt be an object generated from class P oint and suppose the message move is sent to pt. When the body of move is executed, self will refer to pt, a point. Now suppose the class ColorP oint is defined as inheriting from P oint, making no modifications to the method move. Now if c pt is an object generated from class ColorP oint and the message move is sent to c pt then all occurrences of self in the body of move will refer to c pt, a colored point, not a point. It is thus necessary to ensure that any operations on self which are legal for a point are also legal for a colored point (or for any other potential subclass of class P oint).

In dynamic binding, if a method is inherited in constructing a subclass, all method names referred to in that method’s body are resolved and interpreted in the context of the subclass, not the class where they were originally defined. In our example, suppose method eq is inherited by ColorP oint and then redefined. Then any occurrences of eq in move must be interpreted with the new meaning of eq when applied to an object which is a colored point.

Because the definitions of inheritance given in [CHC90] and [Mit90] are quite complex, it is difficult to see whether they provide equivalent semantics for inheritance. Both authors use second-order concepts in their definitions in order to capture the subtleties involved in inheriting methods. In [CHC90] the semantics of classes is defined using a variant of bounded abstraction over types, while Mitchell uses bounded abstraction over functions from types to records.

Mitchell’s semantics provides an interpretation of self via an indirect self-application during method invocation. [CHC90] has a straightforward definition of method invocation, but the meaning of objects is provided by the solution of a fixed point equation. In the following, we show the equivalence of these definitions of semantics for typed objectoriented languages.

We proceed in a way somewhat different from each of the previous papers. We will define a very simple “core” language which allows us to write expressions which represent classes and objects and computations on them. We hope that this language will be easier to understand since all fixed points and self-application are eliminated from the syntax. Once the language and its type-checking rules are presented, we provide two versions of a denotational semantics for the language. One is similar to the style of [Mit90] and the other is in the style of [CHC90].

We note that it would also have been possible to provide a translation of our core language into the second-order lambda calculus with F-bounded quantification (see [CCH^{+}89] for a description of this language). It would then be possible to show that the translations were equivalent via a proof based on the reduction rules of an operational semantics for the translated language. We have chosen the denotational semantics rather than a translation and operational semantics since we feel it gives the meaning of the language at a more appropriate level of abstraction, and hopefully allows the reader to continue to think about the language at the level of the core language, rather than its translation.

Once we have given these two versions of the semantics, a relatively straightforward argument shows that they are equivalent. (Finding a “core” language with which to compare the languages and then reformulating the two semantic definitions to apply to this language was more challenging than actually finding the proof.)

This paper is organized as follows. In section 2 we discuss the differences in the formal languages chosen by [Mit90]and [CHC90] and relate these to our choices of core language and the presentation of semantics. In section 3 we provide an informal description of our language in preparation for the more formal introduction to the syntax and type-checking rules found in section 4. In section 5 we then provide the two different denotational semantics for the core language, and show that the two semantics are equivalent in section 6. In section 7 we discuss previous work in this area and directions for further work. Because our semantics in the style of [Mit90] appears on the surface to be different from the one given in that paper, we provide a more detailed comparison of the two in an appendix.

2 The Languages of Cook et al. and Mitchell

One problem which arises in comparing the two semantic definitions of inheritance is that the languages that the different authors used are conceptually somewhat different.

Mitchell’s language has no classes – objects are defined by extending (or changing) other objects (i.e., by “delegation”), while Cook’s language does provide classes and a mechanism to generate objects from classes. The language described here provides classes and the “new” operator to construct objects from classes. Mitchell provides mechanisms for updating and extending objects while Cook et al. provide a mechanism for updating and extending classes. We provide these mechanisms for classes.

Both languages support the constant “self”, which refers to the object to which the method is applied. Cook et al. supports “super” while Mitchell does not. We follow Mitchell in omitting “super”, but including “self ” in our language.

As noted earlier, both authors use higher-order quantification in order to support the inheritance of methods in subclasses. However, the two semantics describe the types of subclasses with different notation. In Mitchell’s system one extends classes to form subclasses via the use of a function G from types to records which represents the possible extensions to the original object type. Cook et al., on the other hand, use F-bounded quantifiers (see [CW85] and [CCH^{+}89] for comprehensive discussions of the use of bounded quantifiers to express inheritance) to express similar relations between types. We adopt terminology which is based on F-bounded quantification, but adopt some of the features of Mitchell’s notation.

Finally, Mitchell has a relatively simple definition of objects, but a relatively complex definition of method invocation. We have rewritten his definitions so that the definition of classes is essentially the same as his definition of objects , but put much of the work that used to be involved in message passing into the definition of “new” (which was not included in his language) which creates an object from a class.^{2} The meaning of method invocation then becomes much simpler, and identical to that of Cook et al.. This redistribution of complexity makes it easier to show that the two systems are equivalent. (In Appendix 1, we provide a more detailed argument that our modification of Mitchell’s semantics is in the same spirit as his original semantics.)

As a result of these modifications, the languages and semantics used in this paper differ somewhat from those given in [CHC90] and [Mit90]. However we believe that the semantics provided preserves the essential features (and mutual differences) of the semantics given in the original papers.

3 An Informal Description of the Language

Before presenting the formal syntax and semantics of our language, we provide an informal description. We begin with a description of classes, objects, and their types. We presume that the reader is familiar with the syntax of the typed lambda calculus. In particular, λx: σ.M stands for a function which takes a parameter of type σ and returns the value of M (where the value of the actual parameter is used as the value of x in M).

Classes provide templates for the creation of objects. A typical class is written as

class (self : MyType){m_{1} = e_{1},…, m_{n} = e_{n}},

where the m_{i} are the names of its methods and the e_{i} are terms representing the bodies of the methods. (We explain the role of self:MyType in the notation later.)

T class (MyType){m_{1}: τ_{1},…, m_{n}: τ_{n}}

is the type of class (self : MyType){m_{1} = e_{1},…, m_{n} = e_{n}}, if each e_{i} has type τ_{i}. If c is a class,

new c

is a new object which responds to messages by evaluating the corresponding term in the definition of the class c. If c has type T class(MyType){m_{1}: τ_{1},…, m_{n}: τ_{n}}, then the type of the object created by new c will be written as

T obj(MyType){m_{1}: τ_{1},…, m_{n}: τ_{n}}.

The essential difference is that objects are involved in computations as targets of messages, while classes can only be instantiated to objects (through the new command) or modified as described below. Messages cannot be sent to classes.

If o is an object which has a method with name m, then we write

o ⇐ m

2We also eliminated the dependence on the order in which methods are added to objects since this often required “pre-processing” objects before a message could be sent to it.

for the result of evaluating the method m on o (some authors write this as o.m instead). This is often described as “sending the message m to o”.

The variable self which occurs in the definition of the class is used in the body of a method to stand for the object that the method is being invoked on. Thus, if in the definition of a method m, one wishes to send the message m′ to the current object, one writes self ⇐ m′. The other variable MyType which occurs in class definitions and in Tclass and Tobj definitions stands for the type of the current object. Thus the type of each occurrence of self in a method is always given by MyType (hence the notation self:MyType in the header of the class).

The following simple example of a class should help clarify these ideas. Let

P ointClass = class(self : MyType){x = 47, y = 13, eq = λp: MyType.

([(p ⇐ x) = (self ⇐ x)]and [(p ⇐ y) = (self ⇐ y)])}.

Then the type of P ointClass is

T class(MyType){x: Num, y: Num, eq: MyType → Bool}

where the type A → B represents the type of all functions from A to B. Let

MyP oint = new P ointClass.

Then MyP oint is an object with type

P ointT ype = T obj(MyType){x: Num, y: Num, eq: MyType → Bool}.

In particular, MyP oint ⇐ eq is a function with type P ointT ype → Bool. That is, it takes an argument whose type is the same as that of MyP oint (namely P ointT ype), returning either true or false depending on whether its x and y components are equal to those of MyPoint. (Note that we replace the keyword MyType by the actual type of MyPoint, i.e. PointType, when we form MyP oint ⇐ eq.)

As a consequence of our definitions, there may be many classes with the same class type, and objects of a particular object type may have been generated by several different classes (though all of the generating classes must have had the same class type).

Classes can be modified in two ways. First, a class may be updated by modifying the value of a method. If c is a class with method m_{i}, we write

update c by (self : MyType){m_{i} = e′_{i}}

for the new class whose m_{i} component is replaced by e′_{i} (e′_{i} must have the same type as the original body, e_{i}, of m_{i}). For example we can define

DiffPointClass = update P ointClass by (self : MyType){x = 17}

Objects generated from this new class will have an x value of 17 rather than 47. We write update c by (self : MyType){m′_{1} = e′_{1},…, m′_{k} = e′_{k}} as an abbreviation for the obvious series of updates of single methods.

Second, a class may be extended by adding new methods. If c is a class then we write

extend c with (self : MyType){m′_{1} = e′_{1},…, m′_{n} = e′_{n}}

for the new class obtained from c which contains all of the methods of c plus new methods m′_{i} with corresponding bodies e′_{i}. (Note that the simultaneous addition of multiple new methods is essential because of the possibility of mutually recursive methods.) For example, we can define

ColorP ointClass = extend P ointClass with (self : MyType){c = red}

If s and t are both object types then we write s ≤_{X} t if s is obtained from t by adding new methods (while leaving the types of the original methods alone). As one example, if a class d is obtained by inheriting from class c, then the type of objects generated from d will be ≤_{X} to the type of objects generated from c.

Remark 3.1 As explained in [CHC90], this notion is not the same as subtype. (See that paper for a definition of subtype. It involves the possibility of using an item of one type where another is expected.) The failure of subtyping results from the occurrence of MyType (and complications due to contravariance). For example, the type of objects generated from ColorP ointClass is not a subtype of P ointT ype because of the occurrence of MyType in the domain of the eq method.

Because ≤_{X} does not designate subtyping, this paper does not consider the “subsumption” rule or other rules commonly derived from that rule. Thus a function can only be applied to a parameter whose type matches exactly that of the formal parameter - a type which is ≤_{X} to that specified will not do.

We can summarize our language as follows. The language contains expressions which denote classes and objects and their corresponding types as well as the normal elements of traditional types found commonly in programming languages. Classes can be used to generate objects via the new construct, and can be changed (via the update construct) and extended (via the extend construct). Objects, on the other hand, are immutable. The only operation available on objects is to send them messages (o ⇐ m).

While an extension to this language supporting subtypes, super, and updateable instance variables is not that difficult (see the last section of this paper), we chose to keep the language very simple here in order to simplify the comparison of the two styles of semantics.

In the next section we provide a formal definition of the language and a formal specification of the types of terms.

4 Syntax and Type Checking

The rules and axioms given in this section provide a formal definition of the syntax for type expressions and ordinary expressions in our core language. We also provide typing rules for expressions. We begin by defining the type expressions.

Rather than giving a complete (and complex) definition of types in terms of expressions of higher types, we give a more informal definition here. It is an easy exercise to convert this to the more complete specification given in [BMM90] and [BL90]

Definition 4.1 Let V be an infinite collection of type variables, L be an infinite collection of labels, and C be a collection of type constants which includes at least the type constants Bool and Num. The type expressions with respect to V and C are defined as follows:

1. If t ∈ V ∪ C then t is a type expression.

2. If σ and τ are type expressions, then so is σ → τ.

3. If m_{1},…, m_{n} ∈ L and τ_{1},…, τ_{n} are type expressions and MyType ∈ V, then T obj(MyType){m_{1}: τ_{1},…, m_{n}: τ_{n}} and T class(MyType){m_{1}: τ_{1},…, m_{n}: τ_{n}} are type expressions. MyType is considered to be a bound variable in the Tobj and Tclass type expressions.

In the above definition, the bound variable MyType in object and class types stands for the type of self, that is, the type of the current object which is executing the method. We will consider two type expressions to be the same if they are the same up to renaming of bound variables. Thus

T obj(MyType){m_{1}: τ_{1},…, m_{n}: τ_{n}} = T obj(MyType′){m_{1}: τ′_{1},…, m_{n}: τ′_{n}}

if MyType′ does not occur in the type expression on the left, and, for 1 ≤ i ≤ n, τ′_{i} = τ_{i}[MyType′/MyType].

As noted in the previous section, σ ≤_{X} τ is only used between type expressions which are intended to denote object types, and indicates that the methods of σ include all of those in τ and the corresponding types associated with each of those methods are identical as well.

Definition 4.2 An inequality of the form σ ≤_{X} τ, where σ and τ are type expressions, is said to be a type constraint. If, moreover, t is a type variable and τ is of the form T obj(MyType){m_{1}: σ_{1}, ..., m_{k}: σ_{k}} then we say t ≤_{X} τ is a simple type constraint which declares t. If for some τ, t ≤_{X} τ is included in a set C of simple type constraints, then we say t is declared in C. A type constraint system is defined as follows:

1. The empty set is a type constraint system.

2. If C is a type constraint system and t ≤_{X} τ is a simple type constraint such that t is not declared in C and such that every free variable in τ is declared in C, then C ∪ {t ≤_{X} τ} is a type constraint system.

For example, if MyType and u are type variables, then

C = {MyType ≤_{X} T obj(MyType){x: Num, add: MyType → MyType},
u ≤_{X} T obj(MyType′){p: MyType, r: MyType′ → Bool}}

is a type constraint system.

We define type constraint derivations of the form C ⊢ σ ≤_{X} τ, for C a type constraint system and σ, τ type expressions, via the following set of axioms and rules:

Type Constraint Axioms and Rules:

C∪{t ≤_{X} τ}⊢ t ≤_{X} τ

C ⊢ τ ≤_{X} τ, for τ an object type or type variable declared in C

\frac{C ⊢ ρ ≤_{X} σ, C ⊢ σ ≤_{X} τ}{C ⊢ ρ ≤_{X} τ} ,

C ⊢ T obj(MyType){m_{1}: σ_{1}, ..., m_{k}: σ_{k}, ..., m_{n}: σ_{n}} ≤_{X} T obj(MyType){m_{1}: σ_{1}, ..., m_{k}: σ_{k}}

In types of the form T obj(MyType){m_{1}: σ_{1}, ..., m_{k}: σ_{k}}, the ordering of the method names (the m_{i}) are not important. Thus the ≤_{X} relation holds between T obj types if all of the larger type’s methods (and corresponding types) are included in those in the smaller type.

The above axioms and rules are simpler than those typically used in object-oriented languages. The simplicity results from the fact that we are only dealing with class extensions and updates which do not change the types of pre-existing methods. Future work will include the notion of subtyping, which is not considered here.

Definition 4.3 A syntactic type assignment, E, is a finite set of the form:

E = {x_{1}: τ_{1}, ..., x_{n}: τ_{n}}

with no variable x_{i} appearing more than once in E. We write E(x) = τ if x: τ ∈ E.

Type assignment derivations of the form C, E ⊢ M: σ, for C a type constraint system, E a syntactic type assignment, M a term of our language, and σ a type, define the terms of the language and their typing. They are given by the following set of axioms and rules for typing assertions. In the syntax below, decorations of the form (self : MyType) and (MyType) indicate the regular and type variables which stand for the current object, self, and its type, MyType. Variables included in such decorations are considered bound variables.

Type Assignment Axioms and Rules:

C, E ⊢ x: τ if E(x) = τ

\frac{C, E ⊢ B: Bool, C, E ⊢ M: τ, C, E ⊢ N: τ}{C, E ⊢ if B then M else N: τ}

\frac{C, E ∪ \{v: σ\} ⊢ M: τ}{C, E ⊢ λv: σ.M: σ → τ}

\frac{C, E ⊢ M: σ → τ, N: σ}{C, E ⊢ M N: τ}

\frac{C, E ⊢ M, N: Num}{C, E ⊢ M = N: Bool}

\frac{C ∪ \{MyType ≤_{X} T obj(MyType)\{m_{1}: τ_{1},…, m_{n}: τ_{n}\}\}, E ∪ \{self : MyType\} ⊢ e_{i}: τ_{i} for all 1 ≤ i ≤ n}{C, E ⊢ class(self : MyType)\{m_{1} = e_{1},…, m_{n} = e_{n}\}: T class(MyType)\{m_{1}: τ_{1},… m_{n}: τ_{n}\}}

\frac{C, E ⊢ c: T class(MyType)\{m_{1}: τ_{1},…, m_{n}: τ_{n}\}}{C, E ⊢ new c: T obj(MyType)\{m_{1}: τ_{1},…, m_{n}: τ_{n}\}}

\frac{C ⊢ σ ≤_{X} T obj(MyType)\{m: τ\}, C, E ⊢ o: σ}{C, E ⊢ o ⇐ m: τ[σ/MyType]}

\frac{C, E ⊢ c: T class(MyType)\{m_{1}: τ_{1},…, m_{n}: τ_{n}\}, C ∪ \{MyType ≤_{X} T obj(MyType)\{m_{1}: τ_{1},…, m_{i}: τ_{i},…, m_{n}: τ_{n}\}\}, E ∪ \{self : MyType\} ⊢ e′_{i}: τ_{i}}{C, E ⊢ update c by (self : MyType)\{m_{i} = e′_{i}\}: T class(MyType)\{m_{1}: τ_{1},…, m_{n}: τ_{n}\}} , if 1 ≤ i ≤ n

\frac{C, E ⊢ c: T class(MyType)\{m_{1}: τ_{1},…, m_{n}: τ_{n}\}, C ∪ \{MyType ≤_{X} T obj(MyType)\{m_{1}: τ_{1},…, m_{n}: τ_{n}, m′: τ′\}\}, E ∪ \{self : MyType\} ⊢ e′: τ′}{C, E ⊢ extend c with (self : MyType)\{m′ = e′\}: T class(MyType)\{m_{1}: τ_{1},…, m_{n}: τ_{n}, m′: τ′\}}

In the last rule, we require that m ∉ {m_{1},…, m_{n}}. Also as noted in section 3, the last rule should allow for the addition of multiple new methods. We have written it with only one for simplicity here. As indicated earlier, the variables self and MyType are considered bound in the class, update, and extend expressions. Terms which agree up to bound variables are considered to be identical.

Remark 4.4 We have cheated a bit in several of the rules in an attempt to make them easier to understand. In particular, we have presumed that the bound MyType’s are the same in each of the hypotheses of a rule as well as reused MyType as a free variable. For instance, the typing rule for classes should actually read:

\frac{C ∪ \{MyType ≤_{X} T obj(MT)\{m_{1}: τ′_{1},…, m_{n}: τ′_{n}\}\}, E ∪ \{self : MyType\} ⊢ e_{i}: τ_{i} for all 1 ≤ i ≤ n}{C, E ⊢ class(self : MyType)\{m_{1} = e_{1},…, m_{n} = e_{n}\}: T class(MyType)\{m_{1}: τ_{1},… m_{n}: τ_{n}\}}

where MT does not occur in any of the τ_{i} and τ′_{i} = τ_{i}[MT/MyType].

The update and extend rule are worse because of the complexity arising from the multiple hypotheses. The concerned reader is urged to rewrite these in their more complex form.

Note also that since

C ∪ {MyType ≤_{X} T obj(MyType){m_{1}: τ_{1},…, m_{n}: τ_{n}, m′: τ′}}

is illegal if C already defines MyType, it will occasionally be necessary to replace the names of bound variables (e.g. self and MyType) by fresh variables, and later convert back to the desired bound variable names. (This is similar to what is routinely required in dealing with bound variables in typing λ-abstraction terms.)

5 Semantic Definitions

In this section we provide semantic definitions for our language. We provide two somewhat different versions, one of which provides semantic definitions similar to that given by [Mit90], and the other of which is similar to that given in [CHC90]. In the next section we show that the two definitions are equivalent. Both definitions are based on the existence of a model of the second-order polymorphic lambda calculus fitting the definition given in [BMM90] with extensions as suggested in [CCH^{+}89] for handling what is described there as “F-Bounded quantification.” We present the definition under the assumption that a model exists which provides all of the features needed for the definition, including all necessary least fixed points for both types and elements.

Let A be an extensional model of the second-order polymorphic lambda calculus with records, and for each type σ, let A^{σ} represent the set of elements of type σ. For simplicity we assume that A^{Bool} = {true, false}. If ρ is a type environment mapping type variables to types, then we define the meanings of types as follows:

[[t]]ρ = ρ(t)

[[A → B]]ρ = [[A]]ρ ⇒ [[B]]ρ

[[T obj(MyType){m_{1}: τ_{1},…, m_{n}: τ_{n}}]]ρ = F IX(λ τ. ∏_{m_{i}∈{m_{1},...,m_{n}}}[[τ_{i}]]ρ[τ/MyType])

FIX is an operator which provides the least fixed point of a function. Thus

[[T obj(MyType){m_{1}: τ_{1},…, m_{n}: τ_{n}}]]ρ = ∏_{m_{i}∈{m_{1},...,m_{n}}}[[τ_{i}]]ρ[[[T obj(MyType){m_{1}: τ_{1},…, m_{n}: τ_{n}}]]ρ/MyType] ^{3}

The meaning of the class types will depend on which of the semantics we are discussing, and thus will be given separately with each.

For simplicity in exposition, we presume that

A^{σ⇒τ} = A^{σ} → A^{τ}

[[{m_{1}: τ_{1},…, m_{n}: τ_{n}}]]ρ = ∏_{m_{i}∈{m_{1},...,m_{n}}}[[τ_{i}]]ρ

3While our language does not include record types, it may be useful to note that if records were supported, the semantics would be:

Thus object types are essentially treated as recursively defined records.

and similarly for products (as in the definition of object types). It is straightforward to replace this by the more complex (but more flexible) definition given in [BMM90] and [BL90].

We must now provide a semantics for ≤_{X} which will be appropriate for types (as opposed to type expressions). The difficulty is that we will be trying to interpret inequalities of the form t ≤_{X} T obj(MT)F (MT) where F is a function from types to types. We essentially want types t such that t is an extension of F(t). We cannot simply take the collection of all types less than or equal to some fixed type in a given ordering of types, since F (t) depends on t. The solution given in [CCH^{+}89] is to define the collection of types

F Bound(F) = {τ|τ ≤_{T} F (τ)}

where ≤_{T} is the obvious ordering on product types. We provide a similar solution below.

Definition 5.1 Let τ and τ′ be types. Define τ′ ≤_{T} τ iff there are L′ ⊇ L finite collections of labels from L and a collection {τ_{l}}_{l∈L′} of types such that τ′ = ∏_{l∈L′} τ_{l} and τ = ∏_{l∈L} τ_{l}.

We now need to provide a definition of the set of types satisfying a type constraint which involves the type being bounded.

Definition 5.2 Let τ_{1},…, τ_{n} be type expressions, m_{1},…, m_{n} be labels, t a type variable, and ρ a type environment. We define

F Bound({m_{1}: τ_{1},…, m_{n}: τ_{n}}, t, ρ) = {τ|τ is a type & τ ≤_{T} ∏_{m_{i}∈{m_{1},...,m_{n}}}[[τ_{i}]]ρ[τ/t]}.

(Since the definitions of the meaning of type expressions involving class types will differ between the Mitchell and Cook semantics, there will actually be two such notions of FBound — one for each semantics. We will write the term with a superscript M or C to designate which of the two we mean.)

Lemma 5.3 F Bound({m_{1}: τ_{1},…, m_{n+1}: τ_{n+1}}, t, ρ) ⊆ F Bound({m_{1}: τ_{1},…, m_{n}: τ_{n}}, t, ρ)

Proof. This follows easily from the fact that ∏_{m_{i}∈{m_{1},...,m_{n+1}}}[[τ_{i}]]ρ′ ≤_{T} ∏_{m_{i}∈{m_{1},...,m_{n}}}[[τ_{i}]]ρ′ for all ρ′.

Let ρ be a type environment mapping type variables to types and C be a type constraint system. We need to determine when ρ is consistent with C.

Definition 5.4 The following inductive definition determines when a type environment ρ is consistent with a type constraint system C:

1. If C is empty then ρ is consistent with C.

2. Suppose C′ = C ∪ {t ≤_{X} T obj(MyType){m_{1}: σ_{1}, ..., m_{k}: σ_{k}}} is a type constraint system. If ρ is consistent with C and

ρ(t) ∈ F Bound({m_{1}: σ_{1}, ..., m_{k}: σ_{k}}, MyType, ρ)

then ρ is consistent with C′.

(As was the case with FBound above, there are two notions of consistency here and in the following definition — one for each semantics. It will usually be clear from context which of the two we mean.)

Definition 5.5 Let ρ be a semantic environment mapping type variables to types and regular variables to elements of A. We say ρ is consistent with respect to C, E, if ρ is consistent with C and, for all x in the domain of ρ, if E(x) = σ then ρ(x) ∈ [[σ]]ρ.

The meaning of terms of the simple typed lambda calculus and of message passing are identical for the two semantic definitions. As a result, we present these first. In all cases we assume that the semantic environment is consistent with the corresponding sets C and E. We shall show later that for all cases, [[C, E ⊢ M: τ]]ρ ∈ A^{[[τ]]ρ}

Common Semantics:

[[C, E ⊢ x: τ]]ρ = ρ(x)

[[C, E ⊢ if B then M else N: τ]]ρ = \{ \begin{matrix}[[C, E ⊢ M: τ]]ρ, & if [[C, E ⊢ B: Bool]]ρ \\ [[C, E ⊢ N: τ]]ρ, & otherwise \end{matrix}

[[C, E ⊢ λv: σ.M: σ → τ]]ρ = λd ∈ A^{σ}.[[C, E ⊢ M: τ]]ρ[d/v]

[[C, E ⊢ MN: τ]]ρ = ([[C, E ⊢ M: σ → τ]]ρ)([[C, E ⊢ N: σ]]ρ)

[[C, E ⊢ M = N: Bool]]ρ = \{ \begin{matrix}true, & if [[C, E ⊢ M: τ]]ρ = [[C, E ⊢ N: τ]]ρ \\ false, & otherwise \end{matrix}

[[C, E ⊢ o ⇐ m: τ_{i}[σ/MyType]]]ρ = [[C, E ⊢ o: σ]]ρ m

The semantics of classes and objects differ in the two systems. We will write [[N]]^{M}ρ for the meaning of the term N in the Mitchell semantics and [[N]]^{C}ρ for the meaning of N in the semantics given by Cook et al. We first present the Mitchell semantics, followed by that given by Cook et al. (We suggest that the reader keep the type assignment axioms and rules at hand when reading the definitions of semantics.)

Mitchell Semantics:

Types

[[T class(MyType){m_{1}: τ_{1},…, m_{n}: τ_{n}}]]^{M}ρ

= ∏_{m_{i}∈{m_{1},...,m_{n}}} ∏_{τ∈F Bound({m_{1}:τ_{1},...,m_{n}:τ_{n}},MyType,ρ)^{M}} (τ ⇒ [[τ_{i}]]^{M}ρ[τ/MyType])

Note that the τ_{i} occurring at the end of the above formula has a subscript i which matches the m_{i} chosen in the outer product.

Terms

[[C, E ⊢ class(self : MyType){m_{1} = e_{1},…, m_{n} = e_{n}}:

T class(MyType){m_{1}: τ_{1},…, m_{n}: τ_{n}}]]^{M}ρ

= f where for m_{i} ∈ {m_{1},…, m_{n}},

f(m_{i}) = λτ ∈ F Bound({m_{1}: τ_{1},…, m_{n}: τ_{n}}, MyType, ρ)^{M}.λσ ∈ A^{τ}.

[[C ∪ {MyType ≤_{X} T obj(MyType){m_{1}: τ_{1},…, m_{n}: τ_{n}}},

E ∪ {self : MyType} ⊢ e_{i}: τ_{i}]]^{M}ρ[σ/self , τ/MyType]

[[C, E ⊢ new c: T obj(MyType){m_{1}: τ_{1},…, m_{n}: τ_{n}}]]^{M}ρ

= F IX(λo ∈ A^{[[T obj(MyType){m_{1}:τ_{1},...,m_{n}:τ_{n}}]]^{M} ρ}.λm ∈ {m_{1},…, m_{n}}.

([[C, E ⊢ c: T class(MyType){m_{1}: τ_{1},…, m_{n}: τ_{n}}]]^{M}ρ) m ([[T obj(MyType){m_{1}: τ_{1},…, m_{n}: τ_{n}}]]^{M}ρ) o)

[[C, E ⊢ update c by(self : MyType){m_{i} = e′_{i}}: T class(MyType){m_{1}: τ_{1},…, m_{n}: τ_{n}}]]^{M}ρ = f where f(m_{i}) = λτ ∈ F Bound({m_{1}: τ_{1},…, m_{n}: τ_{n}}, MyType, ρ)^{M}.λσ ∈ A^{τ}.

[[C ∪ {MyType ≤_{X} T obj(MyType){m_{1}: τ_{1},…, m_{n}: τ_{n}}}, E ∪ {self : MyType} ⊢ e′_{i}: τ_{i}]]^{M}ρ[σ/self , τ/MyType]

and for m_{j} ∈ {m_{1},…, m_{n}}, m_{j} ≠ m_{i}, f(m_{j}) = [[C, E ⊢ c: T class(MyType){m_{1}: τ_{1},…, m_{n}: τ_{n}}]]^{M}ρ m_{j}

[[C, E ⊢ extend c with(self : MyType){m′ = e′}:

T class(MyType){m_{1}: τ_{1},…, m_{n}: τ_{n}, m′: τ′}]]^{M}ρ

= f

where f(m′) = λτ ∈ F Bound({m_{1}: τ_{1},…, m_{n}: τ_{n}, m′: τ′}, MyType, ρ)^{M}.λσ ∈ A^{τ}.

[[C ∪ {MyType ≤_{X} T obj(MyType){m_{1}: τ_{1},…, m_{n}: τ_{n}, m′: τ′}},

E ∪ {self : MyType} ⊢ e′: τ′]]^{M}ρ[σ/self , τ/MyType]

and for m_{i} ∈ {m_{1},…, m_{n}}, f(m_{i}) = [[C, E ⊢ c: T class(MyType){m_{1}: τ_{1},…, m_{n}: τ_{n}}]]^{M}ρ m_{i}

The meaning of a class given above is a function which takes an appropriate method name (i.e. one mentioned in its type) as its first argument. It then takes as parameter a type (which is an extension of the type of objects generated by the class) as the interpretation of MyType, and an object of that type as the interpretation of self . With those interpretations, it then evaluates the body of the method whose name corresponds to the one provided. It is crucial that the meaning of the class can be applied to any extension of the type of the given class. Thus, in the definition of the meaning of extend c with (self : MyType){m′ = e′}, if m is a method name of c, the meaning of c is applied to m and a type τ which is an extension of the type of objects generated by c and which also contains a field m’ with appropriate type.

The meaning of a class seems to have too many parameters to be directly useful in responding to messages, and that is so. In order to make it useful in responding to messages, we must create an object. The meaning of an object given by new c is found by taking a fixed point of the class c. The meaning of self in each of the messages defined in c is bound to that fixed point. By unrolling the fixed point one level, we can write the meaning in a slightly different way from that given above,

[[C, E ⊢ new c: T obj(MyType){m_{1}: τ_{1},…, m_{n}: τ_{n}}]]^{M}ρ = f

where for m ∈ {m_{1},…, m_{n}}.

f(m) = ([[C, E ⊢ c: T class(MyType){m_{1}: τ_{1},…, m_{n}: τ_{n}}]]^{M}ρ) m

([[T obj(MyType){m_{1}: τ_{1},…, m_{n}: τ_{n}}]]^{M}ρ)

[[C, E ⊢ new c: T obj(MyType){m_{1}: τ_{1},…, m_{n}: τ_{n}}]]^{M}ρ

If, moreover, c = class(self : MyType){m_{1} = e_{1},…, m_{n} = e_{n}} then [[C, E ⊢ new c: T obj(MyType){m_{1}: τ_{1},…, m_{n}: τ_{n}}]]^{M}ρ m_{i}

= [[C ∪ {MyType ≤_{X} T obj(MyType){m_{1}: τ_{1},…, m_{n}: τ_{n}}}, E ∪ {self : MyType}

⊢ e_{i}: τ_{i}]]^{M}ρ[[[C, E ⊢ new c: T obj(MyType){m_{1}: τ_{1},…, m_{n}: τ_{n}}]]^{M}ρ/self ,

[[T obj(MyType){m_{1}: τ_{1},…, m_{n}: τ_{n}}]]^{M}ρ/MyType]

Thus the body of each method is interpreted in an environment in which self is interpreted as the entire object (i.e., the meaning of new c) and MyType is interpreted as the type of new c.

See Appendix 1 for a comparison of this definition with that given in [Mit90].

Cook Semantics:

Types

[[T class(MyType){m_{1}: τ_{1},…, m_{n}: τ_{n}}]]^{C}ρ = ∏_{τ∈F Bound({m_{1}:τ_{1},...,m_{n}:τ_{n}},MyType,ρ)^{C}}(τ ⇒ ∏_{m_{i}∈{m_{1},...,m_{n}}}[[τ_{i}]]^{C}ρ[τ/MyType])

Terms

[[C, E ⊢ class(self : MyType){m_{1} = e_{1},…, m_{n} = e_{n}}:

T class(MyType){m_{1}: τ_{1},…, m_{n}: τ_{n}}]]^{C}ρ

= λτ ∈ F Bound({m_{1}: τ_{1},…, m_{n}: τ_{n}}, MyType, ρ)^{C}.λσ ∈ A^{τ}.f_{τ,σ}

where for m_{i} ∈ {m_{1},…, m_{n}},

f_{τ,σ}(m_{i}) = [[C ∪ {MyType ≤_{X} T obj(MyType){m_{1}: τ_{1},…, m_{n}: τ_{n}}},

E ∪ {self : MyType} ⊢ e_{i}: τ_{i}]]^{C}ρ[σ/self , τ/MyType]

[[C, E ⊢ new c: T obj(MyType){m_{1}: τ_{1},…, m_{n}: τ_{n}}]]^{C}ρ

= F IX([[C, E ⊢ c: T class(MyType){m_{1}: τ_{1},…, m_{n}: τ_{n}}]]^{C}ρ ([[T obj(MyType){m_{1}: τ_{1},…, m_{n}: τ_{n}}]]^{C}ρ))

[[C, E ⊢ update c by(self : MyType){m_{i} = e′_{i}}: T class(MyType){m_{1}: τ_{1},…, m_{n}: τ_{n}}]]^{C}ρ = λτ ∈ F Bound({m_{1}: τ_{1},…, m_{n}: τ_{n}}, MyType, ρ)^{C}.λσ ∈ A^{τ}.f_{τ,σ} where f_{τ,σ}(m_{i}) = [[C ∪ {MyType ≤_{X} T obj(MyType){m_{1}: τ_{1},…, m_{n}: τ_{n}}},

E ∪ {self : MyType} ⊢ e′_{i}: τ_{i}]]^{C}ρ[σ/self , τ/MyType]

and for m_{j} ∈ {m_{1},… m_{n}}, m_{j} ≠ m_{i}, f_{τ,σ}(m_{j}) = C, E ⊢ c: T class(MyType){m_{1}: τ_{1},…, m_{n}: τ_{n}} τ σ m_{j}

[[C, E ⊢ extend c with(self : MyType){m′ = e′}:

T class(MyType){m_{1}: τ_{1},…, m_{n}: τ_{n}, m′: τ′}]]^{C}ρ

= λτ ∈ F Bound({m_{1}: τ_{1},…, m_{n}: τ_{n}, m′: τ′}, MyType, ρ)^{C}.λσ ∈ A^{τ}.f_{τ,σ} where f_{τ,σ}(m′) = [[C ∪ {MyType ≤_{X} T obj(MyType){m_{1}: τ_{1},…, m_{n}: τ_{n}, m′: τ′}},

E ∪ {self : MyType} ⊢ e′: τ′]]^{C}ρ[σ/self , τ/MyType]

and for m_{i} ∈ {m_{1},…, m_{n}}, f_{τ,σ}(m_{i}) = [[C, E ⊢ c: T class(MyType){m_{1}: τ_{1},…, m_{n}: τ_{n}}]]^{C}ρ τ σ m_{i}

As stated earlier, for the above definitions to make sense we need a model A in which all of the necessary least fixed points (on both types and elements) exist. The models by [Ama91, Car89, BM91] all suffice for this purpose. For the remainder of the paper we presume that we are working in such a model.

Notice that the main difference between the two sets of definitions is in the order in which the parameters occur in the definition of the meaning of class constructs. This can most easily be seen by examining the interpretation of class types (i.e. type expressions of the form T class(MyType){…}). We show in the next section that the two definitions are equivalent.

We end this section with a theorem stating that our definitions are consistent with our typing rules.

Theorem 5.6 (Soundness of semantics with respect to the typing rules) For each of the Cook and Mitchell semantics given above, if C, E ⊢ M: σ then [[C, E ⊢ M: σ]]ρ ∈ [[σ]]ρ.

Proof. The proof is by induction on the complexity of terms. The case for M = new c depends on the fact that the meaning of an object type is a fixed point, and the case for M = extend c with (self : MyType){m′: e′} depends on Lemma 5.3. All other cases are straightforward.

6 Semantic Equivalence

In this section we show the equivalence of the two semantic definitions for our language. Some complications arise because of the differences of meaning for class types in the two systems. Thus we will restrict our attention to a well-behaved subset of the collection of all term expressions.

Definition 6.1 We say a type expression is restricted if no proper subexpression is a class type expression (i.e. is of the form T class(MyType){…}). We say a term M is a restricted term (with respect to C,E) iff there is a derivation of C, E ⊢ M: τ, such that for all statements of the form C′, E′ ⊢ M′: τ′ occurring in that derivation, τ′ is a restricted type.

Note that a class type T class(MyType){m_{1}: τ_{1},…, m_{n}: τ_{n}} is restricted if none of the τ_{i} are class type expressions and the τ_{i} are all are themselves restricted. Similarly, new c is restricted if c is.

The following lemma is obvious from the semantic definitions given in the previous section.

Lemma 6.2 Let τ, τ_{1},…, τ_{n} be restricted type expressions which are not class type expressions, t a type variable, and ρ a type environment. Then

1. [[τ]]^{M}ρ = [[τ]]^{C}ρ.

2. F Bound({m_{1}: τ_{1},…, m_{n}: τ_{n}}, t, ρ)^{M} = F Bound({m_{1}: τ_{1},…, m_{n}: τ_{n}}, t, ρ)^{C}.

Definition 6.3 We say that an environment ρ is simple with respect to the Mitchell semantics if, for all restricted type expressions, τ′, if [[τ′]]^{M}ρ = [[T class(MyType){m_{1}: τ_{1},…, m_{n}: τ_{n}}]]^{M}ρ then

τ′ = T class(MyType′){m_{1}: τ′_{1},…, m_{n}: τ′_{n}} and

F Bound({m_{1}: τ_{1},…, m_{n}: τ_{n}}, MyType, ρ)^{M} =

F Bound({m_{1}: τ′_{1},…, m_{n}: τ′_{n}}, MyType′, ρ)^{M}.

A similar definition holds for the Cook semantics.

This restriction will allow us to define an equivalence relation on types and be assured that it will be well-defined.

The definition of ≃ below is similar to that of a specialized logical relation on our two ways of interpreting A as a model of the language.

Definition 6.4 Let A be a model and let ρ be a simple environment. We define an equivalence relation ≃ on domains of restricted types A^{[[τ]]^{M} ρ} and A^{[[τ]]^{C}ρ} as follows.

1. If τ is a class type expression of the form T class(MyType){m_{1}: τ_{1},…, m_{n}: τ_{n}}, Ξ^{M} ∈ A^{[[τ]]^{M} ρ} and Ξ^{C} ∈ A^{[[τ]]^{C}ρ}, then define Ξ^{M} ≃ Ξ^{C} iff for all 1 ≤ i ≤ n, for all τ′ ∈ F Bound({m_{1}: τ_{1},…, m_{n}: τ_{n}}, MyType, ρ), and for all σ ∈ A^{τ′},

Ξ^{M} m_{i} τ′ σ = Ξ^{C} τ′ σ m_{i}. ^{4}

2. If τ is not a class type expression, then A^{[[τ]]^{M} ρ} = A^{[[τ]]^{C}ρ} and for all a ∈ A^{[[τ]]^{M} ρ}, a′ ∈ A^{[[τ]]^{C}ρ}, define a ≃ a′ iff a = a′.

Finally, we need to define ≃ on environments.

Definition 6.5 Let C, E be given and suppose ρ^{M} and ρ^{C} are simple environments for A and suppose each is consistent with C, E (with respect to each of the Mitchell and Cook semantics). Then ρ^{M} ≃ ρ^{C} iff for all x ∈ Domain(E) such that E(x) is a restricted type, ρ^{M}(x) ≃ ρ^{C}(x)

We now show that the meanings of restricted terms in the two semantics are related by ≃.

Theorem 6.6 Let A be a model with the necessary least fixed points, N be a restricted term, C, E ⊢ N: τ, and ρ^{M} ≃ ρ^{C} consistent with C and E with respect to the Mitchell and Cook semantics, respectively. Then

[[C, E ⊢ N: τ]]^{M}ρ^{M} ≃ [[C, E ⊢ N: τ]]^{C}ρ^{C}.

Proof. The proof is by induction on the proof of the typing of N. The induction hypothesis is that the theorem is true for all expressions in the proof of the typing of N and for all appropriate C, E, τ, and ρ^{M} and ρ^{C}. The cases for variables, if..then..else.., M N, M = N, and o ⇐ m are straightforward. The proof for λv: σ.M depends on the fact that σ is restricted and not a class type expression, but is otherwise straightforward.

Case i: N = class(self : MyType){m_{1} = e_{1}, ..., m_{n} = e_{n}} .

[[C, E ⊢ N: τ]]^{M}ρ^{M}

= [[C, E ⊢ class(self : MyType){m_{1} = e_{1},…, m_{n} = e_{n}}:

T class(MyType){m_{1}: τ_{1},…, m_{n}: τ_{n}}]]^{M}ρ^{M}
= f

where for m_{i} ∈ {m_{1},…, m_{n}}, f(m_{i}) = λτ ∈ F Bound({m_{1}: τ_{1},…, m_{n}: τ_{n}}, MyType, ρ^{M})^{M}.λσ ∈ A^{τ}.

4Note that by the previous lemma, we need not specify whether we are interpreting FBound in the Mitchell or Cook semantics.

[[C ∪ {MyType ≤_{X} T obj(MyType){m_{1}: τ_{1},…, m_{n}: τ_{n}}},
E ∪ {self : MyType} ⊢ e_{i}: τ_{i}]]^{M}ρ^{M}[σ/self , τ/MyType]

[[C, E ⊢ N: τ]]^{C}ρ^{C}

= [[C, E ⊢ class(self : MyType){m_{1} = e_{1},…, m_{n} = e_{n}}:

T class(MyType){m_{1}: τ_{1},…, m_{n}: τ_{n}}]]^{C}ρ^{C}

= λτ ∈ F Bound({m_{1}: τ_{1},…, m_{n}: τ_{n}}, MyType, ρ^{C})^{C}.λσ ∈ A^{τ}.f_{τ,σ} where for m_{i} ∈ {m_{1},…, m_{n}}

f_{τ,σ}(m_{i}) = [[C ∪ {MyType ≤_{X} T obj(MyType){m_{1}: τ_{1},…, m_{n}: τ_{n}}},

E ∪ {self : MyType} ⊢ e_{i}: τ_{i}]]^{C}ρ^{C}[σ/self , τ/MyType]

By induction, for all i, [[C ∪ {MyType ≤_{X} T obj(MyType){m_{1}: τ_{1},…, m_{n}: τ_{n}}},

E ∪ {self : MyType} ⊢ e_{i}: τ_{i}]]^{M}ρ^{M}[σ/self , τ/MyType]

= [[C ∪ {MyType ≤_{X} T obj(MyType){m_{1}: τ_{1},…, m_{n}: τ_{n}}},
E ∪ {self : MyType} ⊢ e_{i}: τ_{i}]]^{C}ρ^{C}[σ/self , τ/MyType]

Thus [[C, E ⊢ N: τ]]^{M}ρ m_{i} τ σ

= [[C ∪ {MyType ≤_{X} T obj(MyType){m_{1}: τ_{1},…, m_{n}: τ_{n}}},

E ∪ {self : MyType} ⊢ e_{i}: τ_{i}]]^{M}ρ^{M}[σ/self , τ/MyType]
= [[C ∪ {MyType ≤_{X} T obj(MyType){m_{1}: τ_{1},…, m_{n}: τ_{n}}},
E ∪ {self : MyType} ⊢ e_{i}: τ_{i}]]^{C}ρ^{C}[σ/self , τ/MyType]
= [[C, E ⊢ N: τ]]^{C}ρ^{C} τ σ m_{i}

So by the definition of ≃, [[C, E ⊢ N: τ]]^{M}ρ^{M} ≃ [[C, E ⊢ N: τ]]^{C}ρ^{C}. Case ii: N = new c Let Ξ^{M} = [[C, E ⊢ c: T class(MyType){m_{1}: τ_{1},…, m_{n}: τ_{n}}]]^{M}ρ^{M} Let

σ^{M} = [[C, E ⊢ N: τ]]^{M}ρ^{M}
= [[C, E ⊢ new c: T obj(MyType){m_{1}: τ_{1},…, m_{n}: τ_{n}}]]^{M}ρ^{M}
= λm ∈ {m_{1},…, m_{n}}.Ξ^{M}m ([[T obj(MyType){m_{1}: τ_{1},…, m_{n}: τ_{n}}]]^{M}ρ^{M}) σ^{M}

Let Ξ^{C} = [[C, E ⊢ c: T class(MyType){m_{1}: τ_{1},…, m_{n}: τ_{n}}]]^{C}ρ^{C}. Let

σ^{C} = [[C, E ⊢ N: τ]]^{C}ρ^{C}
= [[C, E ⊢ new c: T obj(MyType){m_{1}: τ_{1},…, m_{n}: τ_{n}}]]^{C}ρ^{C}
= Ξ^{C}([[T obj(MyType){m_{1}: τ_{1}, ..., m_{n}: τ_{n}}]]^{C}ρ^{C}) σ^{C}

By induction Ξ^{M} ≃ Ξ^{C}. Thus

Ξ^{M}m ([[T obj(MyType){m_{1}: τ_{1}, ..., m_{n}: τ_{n}}]]^{M}ρ) σ

= Ξ^{C}([[T obj(MyType){m_{1}: τ_{1}, ..., m_{n}: τ_{n}}]]^{M}ρ^{M}) σ m

for all m ∈ {m_{1}, ..., m_{n}}, and all σ ∈ A^{τ}. Note also that [[T obj(MyType){m_{1}: τ_{1}, ..., m_{n}: τ_{n}}]]^{M}ρ^{M}

= [[T obj(MyType){m_{1}: τ_{1}, ..., m_{n}: τ_{n}}]]^{C}ρ^{C} since it is a restricted type.

Therefore

σ^{M} = λm ∈ {m_{1},…, m_{n}}.Ξ^{M}m ([[T obj(MyType){m_{1}: τ_{1},…, m_{n}: τ_{n}}]]^{M}ρ^{M}) σ^{M}
= λm ∈ {m_{1},…, m_{n}}.Ξ^{C}([[T obj(MyType){m_{1}: τ_{1},…, m_{n}: τ_{n}}]]^{C}ρ^{C}) σ^{M}m

and hence, by extensionality, σ^{M} = Ξ^{C}([[T obj(MyType){m_{1}: τ_{1}, ..., m_{n}: τ_{n}}]]^{C}ρ^{C}) σ^{M}.

Similarly, σ^{C} = λm ∈ {m_{1},…, m_{n}}.Ξ^{M}m ([[T obj(MyType){m_{1}: τ_{1},…, m_{n}: τ_{n}}]]^{M}ρ^{M})σ^{C}).

Since σ^{C} is a fixed point of σ^{M}’s defining equation (and vice-versa), and each is the least solution of their own defining equation, σ^{C} and σ^{M} must be the same. I.e.

[[C, E ⊢ N: τ]]^{M}ρ^{M} = σ^{M} = σ^{C} = [[C, E ⊢ N: τ]]^{C}ρ^{C}.

Case iii: N = update c by (self : MyType){m_{i} = e′_{i}}

[[C, E ⊢ N: τ]]^{M}ρ^{M}

= [[C, E ⊢ update c by (self : MyType){m_{i} = e′_{i}}:

T class(MyType){m_{1}: τ_{1},…, m_{n}: τ_{n}}]]^{M}ρ^{M}
= f

where f(m_{i}) = λτ ∈ F Bound({m_{1}: τ_{1},…, m_{n}: τ_{n}}, MyType, ρ^{M})^{M}.

λσ ∈ A^{τ}.[[C ∪ {MyType ≤_{X} T obj(MyType){m_{1}: τ_{1},…, m_{n}: τ_{n}}},

E ∪ {self : MyType} ⊢ e′_{i}: τ_{i}]]^{M}ρ^{M}[σ/self , τ/MyType]

and for m_{j} ∈ {m_{1},…, m_{n}}, m_{j} ≠ m_{i}, f(m_{j}) = [[C, E ⊢ c: T class(MyType){m_{1}: τ_{1},…, m_{n}: τ_{n}}]]^{M}ρ^{M} m_{j}

[[C, E ⊢ N: τ]]^{C}ρ^{C}

= [[C, E ⊢ update c by(self : MyType){m_{i} = e′_{i}}:

T class(MyType){m_{1}: τ_{1},…, m_{n}: τ_{n}}]]^{C}ρ^{C}
= λτ ∈ F Bound({m_{1}: τ_{1},…, m_{n}: τ_{n}}, MyType, ρ^{C})^{C}.λσ ∈ A^{τ}.f_{τ,σ}

where f_{τ,σ}(m_{i}) = [[C ∪ {MyType ≤_{X} T obj(MyType){m_{1}: τ_{1},…, m_{n}: τ_{n}}},

E ∪ {self : MyType} ⊢ e′_{i}: τ_{i}]]^{C}ρ^{C}[σ/self , τ/MyType]

and for m_{j} ∈ {m_{1},…, m_{n}}, m_{j} ≠ m_{i}, f_{τ,σ}(m_{j}) = [[C, E ⊢ c: T class(MyType){m_{1}: τ_{1},…, m_{n}: τ_{n}}]]^{C}ρ^{C} τ σ m_{j}

To show [[C, E ⊢ N: τ]]^{M}ρ^{M} ≃ [[C, E ⊢ N: τ]]^{C}ρ^{C} :

For m_{i}, [[C, E ⊢ N: τ]]^{M}ρ^{M} m_{i} τ σ

= [[C ∪ {MyType ≤_{X} T obj(MyType){m_{1}: τ_{1},…, m_{n}: τ_{n}}},

E ∪ {self : MyType} ⊢ e′_{i}: τ_{i}]]^{M}ρ^{M}[σ/self , τ/MyType]

[[C, E ⊢ N: τ]]^{C}ρ^{C} τ σ m_{i}

= [[C ∪ {MyType ≤_{X} T obj(MyType){m_{1}: τ_{1},…, m_{n}: τ_{n}}},

E ∪ {self : MyType} ⊢ e′_{i}: τ_{i}]]^{C}ρ^{C}[σ/self , τ/MyType]

By induction, these two are equal.

Now for m_{j} ≠ m_{i}, [[C, E ⊢ N: τ]]^{M}ρ^{M} m_{j} τ σ = [[C, E ⊢ c: T class(MyType){m_{1}: τ_{1},…, m_{n}: τ_{n}}]]^{M}ρ^{M} m_{j} τ σ [[C, E ⊢ N: τ]]^{C}ρ^{C} τ σ m_{j} = [[C, E ⊢ c: T class(MyType){m_{1}: τ_{1},…, m_{n}: τ_{n}}]]^{C}ρ^{C} τ σ m_{j} which are also equal by induction. Since for all m the corresponding terms are equal,

[[C, E ⊢ N: τ]]^{M}ρ^{M} ≃ [[C, E ⊢ N: τ]]^{C}ρ^{C}.

Case iv: extend c with (self : MyType){m′ = e′} [[C, E ⊢ N: τ]]^{M}ρ^{M}

= [[C, E ⊢ extend c with (self : MyType){m′ = e′}:

T class(MyType){m_{1}: τ_{1},…, m_{n}: τ_{n}, m′: τ′}]]^{M}ρ^{M}
= f

where f(m′) = λτ ∈ F Bound({m_{1}: τ_{1},…, m_{n}: τ_{n}, m′: τ′}, MyType, ρ^{M})^{M}.λσ ∈ A^{τ}.

[[C ∪ {MyType ≤_{X} T obj(MyType){m_{1}: τ_{1},…, m_{n}: τ_{n}, m′: τ′}},

E ∪ {self : MyType} ⊢ e′: τ′]]^{M}ρ^{M}[σ/self , τ/MyType]

and for m_{i} ∈ {m_{1},…, m_{n}},

f(m_{i}) = [[C, E ⊢ c: T class(MyType){m_{1}: τ_{1},…, m_{n}: τ_{n}}]]^{M}ρ^{M} m_{i} [[C, E ⊢ N: τ]]^{C}ρ^{C}

= [[C, E ⊢ extend c with (self : MyType){m′ = e′}:

T class(MyType){m_{1}: τ_{1},…, m_{n}: τ_{n}, m′: τ′}]]^{C}ρ^{C}
= λτ ∈ F Bound({m_{1}: τ_{1},…, m_{n}: τ_{n}, m′: τ′}, MyType, ρ^{C})^{C}.λσ ∈ A^{τ}.f_{τ,σ}

where f_{τ,σ}(m′) = [[C ∪ {MyType ≤_{X} T obj(MyType){m_{1}: τ_{1},…, m_{n}: τ_{n}, m′: τ′}},

E ∪ {self : MyType} ⊢ e′: τ′]]^{C}ρ^{C}[σ/self , τ/MyType]

and for m_{i} ∈ {m_{1},…, m_{n}},

f_{τ,σ}(m_{i}) = [[C, E ⊢ c: T class(MyType){m_{1}: τ_{1},…, m_{n}: τ_{n}}]]^{C}ρ^{C} τ σ m_{i} To show [[C, E ⊢ N: τ]]^{M}ρ^{M} ≃ [[C, E ⊢ N: τ]]^{C}ρ^{C} : [[C, E ⊢ N: τ]]^{M}ρ^{M} m′ τ σ

= [[C ∪ {MyType ≤_{X} T obj(MyType){m_{1}: τ_{1},…, m_{n}: τ_{n}, m′: τ′}},

E ∪ {self : MyType} ⊢ e′: τ′]]^{M}ρ^{M}[σ/self , τ/MyType]

[[C, E ⊢ N: τ]]^{C}ρ^{C} τ σ m′

= [[C ∪ {MyType ≤_{X} T obj(MyType){m_{1}: τ_{1},…, m_{n}: τ_{n}, m′: τ′}},

E ∪ {self : MyType} ⊢ e′: τ′]]^{C}ρ^{C}[σ/self , τ/MyType]

By induction, these two are equal. Now for m_{i} ≠ m′, [[C, E ⊢ N: τ]]^{M}ρ^{M} m_{i} τ σ = [[C, E ⊢ c: T class(MyType){m_{1}: τ_{1},…, m_{n}: τ_{n}}]]^{M}ρ^{M} m_{i} τ σ [[C, E ⊢ N: τ]]^{C}ρ^{C} τ σ m_{i} = [[C, E ⊢ c: T class(MyType){m_{1}: τ_{1},…, m_{n}: τ_{n}}]]^{C}ρ^{C} τ σ m_{i} which are also equal by induction. Since, for all m, the corresponding terms are equal,

[[C, E ⊢ N: τ]]^{M}ρ^{M} ≃ [[C, E ⊢ N: τ]]^{C}ρ^{C}.

We note here that the restrictions in the hypothesis of this theorem to restricted terms could be dropped if we were willing to presume the existence of a model which would preserve the relation ≃ under the taking of fixed points (i.e., preserving ⊥ and sups of increasing chains under ≃). This would allow us to push the above proof through without restriction for the new c case.

Corollary 6.7 Suppose N is a restricted term, C, E ⊢ N: τ where τ is not a class type, and ρ^{M} ≃ ρ^{C} are consistent with C and E with respect to the Mitchell and Cook semantics, respectively. Then

[[C, E ⊢ N: τ]]^{M}ρ^{M} = [[C, E ⊢ N: τ]]^{C}ρ^{C}.

7 History and Future Work

The starting point for this paper was the pair of papers by [CHC90] and [Mit90], which presented the semantics of typed languages with inheritance. A semantics for untyped languages had already been given in Cook’s thesis [Coo89]. Similar denotational definitions for untyped languages were also given in [Kam88], [Red88], and [Yel89]. Mitchell’s semantics apparently reflect the way that some object-oriented languages are actually implemented.

Bounded quantification is described in [CW85], and is based on ideas from [Mit84].

[CM89] presented the record operations (including higher-order function abstraction) used in describing Mitchell’s semantics. While there is still much to be done in completing the work described here, it is relatively straightforward to make several improvements.

For instance, we can extend the language to support the keyword “super” which refers to the parent class of the one being defined. This can be included in the semantics by adding the meaning of “super” to the environment (as we did for “self”). The associated meaning can be obtained by applying the meaning of the superclass to the type of the current object and to the current object itself.

For simplicity, this paper has totally ignored instance variables. Objects as treated here are immutable. Real object-oriented programming languages also support instance variables, which are essentially attributes of objects that can be modified at the object level. Terms representing these values do not involve “self” or “MyType.” In order to have the current values of instance variables used when a method is executed, it is important that their values not be locked in when the values of methods are obtained by taking a fixed point (when a new object is constructed). Instead, objects can be modelled as a pair, where the first component is essentially the meaning as given in this paper (encompassing only the meaning of the methods), while the second component represents the current values of the instance variables. Method application is obtained by essentially passing in the values of the instance variables as an extra parameter to each method call. This is reminiscent of the technique used in [Mit90]. The main difference is that he passed in the entire object as an argument. We only pass in the instance variable values. With this set-up, instance variables can be updated in objects (or classes), while methods can only be updated or added in classes. This also has important consequences when subtyping is added to the language (see below). This solution can be further improved by the use of existential types to hide the instance variables from users of the object.

The current presentation makes no direct use of subtypes. Rather “≤_{X}” provides information on object types which form extensions of others. The addition of subtyping allows a more expressive language for methods. Related to this is the generalization of the update operator to one which allows the user to replace a method with one whose type is a subtype of the original. This extension causes no serious problems. We have omitted it here in order to avoid the confusion of working with two different ≤’s simultaneously.

All of these extensions will be included in future work. They were omitted in order to allow a simpler exposition of the results on the equivalence of the semantic definitions. The paper [BM91] will also discuss mathematical models which will support all of these features.

Acknowledgements

Thanks to William Cook, John Mitchell, and Luca Cardelli for many interesting conversations and insights about object-oriented programming languages. Jon Riecke provided many valuable comments based on his presentation of an earlier version of this paper to a seminar at MIT. Gary Leavens also made several helpful suggestions which improved the exposition of the paper. Special thanks to Todd Lowe, Williams ’91, for helping me to really understand the [CHC90] and [Mit90] papers, making this work possible. Finally, thanks to John Mitchell and the Stanford University Computer Science Department and to Luca Cardelli and DEC SRC for their hospitality during my sabbatical leave in the Spring of 1991.

References

[Ama91] R.M. Amadio. Recursion over realizability structures. Information and Computation, 91(1):55–85, March 1991.

[BL90] K. Bruce and G. Longo. A modest model of records, inheritance and bounded quantification. Information and Computation, 87(1/2):196–240, 1990.

[BM91] K. B. Bruce and J. C. Mitchell. A per model of subtypes, polymorphism, and recursive types. 1991. in preparation.

[BMM90] K. B. Bruce, A. R. Meyer, and J. C. Mitchell. The semantics of secondorder lambda calculus. Information and Computation, 85(1):76–134, 1990. Reprinted in Logical Foundations of Functional Programming, ed. G. Huet, Addison-Wesley (1990) 213–273.

[Car89] F. Cardone. Relational semantics for recursive types and bounded quantification. In ICALP, pages 164–178. Springer LNCS 372, 1989.

[CCH^{+}89] 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.

[CHC90] William R. Cook, Walter L. Hill, and Peter S. Canning. Inheritance is not subtyping. In Proc. 17-th ACM Symp. on Principles of Programming Languages, pages 125–135, January 1990.

[CM89] L. Cardelli and J.C. Mitchell. Operations on records. In Math. Foundations of Prog. Lang. Semantics, pages 22–52. Springer LNCS 442, 1989.

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

[CW85] L. Cardelli and P. Wegner. On understanding types, data abstraction, and polymorphism. Computing Surveys, 17(4):471–522, 1985.

[Kam88] S. Kamin. Inheritance in smalltalk-80: a denotational definition. In ACM Symp. Principles of Programming Languages, pages 80–87, 1988.

[Mit84] J.C. Mitchell. Coercion and type inference (summary). In Proc. 11-th ACM Symp. on Principles of Programming Languages, pages 175–185, January 1984.

[Mit90] J.C. Mitchell. Toward a typed foundation for method specialization and inheritance. In Proc. 17-th ACM Symp. on Principles of Programming Languages, pages 109–124, January 1990.

[Red88] U.S. Reddy. Objects as closures: Abstract semantics of object-oriented languages. In Proc. ACM Symp. Lisp and Functional Programming Languages, pages 289–297, July 1988.

[Yel89] P.M. Yelland. First steps towards fully-abstract semantics for object-oriented languages. In European Conf. on Object-Oriented Programming, pages 347– 367, 1989.

A Comparison with Original Mitchell Semantics

In [Mit90], there are no classes in the sense defined here. The use of the expression “class MyT ype.{m_{1}: τ_{1}, ..., m_{n}: τ_{n}}” in that paper corresponds to a combination of our types T class(MyT ype){m_{1}: τ_{1}, ..., m_{n}: τ_{n}} and T obj(MyT ype){m_{1}: τ_{1}, ..., m_{n}: τ_{n}}. Instead, objects are defined directly, and an object inherits from another object via a form of “delegation.” Nevertheless it is relatively easy to show that the definition of semantics of objects and message passing given there corresponds well to that given here.

In Mitchell’s paper, the operator new is unnecessary because of the identification of objects and classes. We have simulated his system by separating objects and classes (by the introduction of new to the language) as well as providing the corresponding types T class(MyT ype){m_{1}: τ_{1}, ..., m_{n}: τ_{n}} and T obj(MyT ype){m_{1}: τ_{1}, ..., m_{n}: τ_{n}}.

In Mitchell’s definition, if C, E ⊢ c: σ (where σ is of the form T class(MyT ype){m_{1}: τ_{1}, ..., m_{n}: τ_{n}} in our notation) then

[[C, E ⊢ c ⇐ m_{i}: τ_{i}[σ/MyT ype]]]ρ = ([[C, E ⊢ c: σ)]]ρ)m_{i}([[σ]]ρ)([[C, E ⊢ c: σ]]ρ).

Because the language used in this paper requires the use of the operator new to create objects before messages can be sent to them, we would evaluate (new c) ⇐ m_{i} rather than c ⇐ m_{i}. Let σ′ = T obj(MyT ype){m_{1}: τ_{1}, ..., m_{n}: τ_{n}} (the object type corresponding to the class type σ). In the system given in this paper for Mitchell semantics:

[[C, E ⊢ (new c ⇐ m_{i}: τ_{i}[σ′/MyT ype]]]^{M}ρ = ([[C, E ⊢ new c: σ′)]]^{M}ρ) m_{i}

= o m_{i} where

\begin{aligned}o & = & [[C, E ⊢ new c: σ′)]]^{M}ρ \\ & = & λm ∈ \{m_{1},…, m_{n}\}.([[C, E ⊢ c: σ]]^{M}ρ) m ([[σ′]]^{M}ρ) o \end{aligned}

= ([[C, E ⊢ c: σ]]^{M}ρ) m_{i} ([[σ′]]^{M}ρ) o)
= ([[C, E ⊢ c: σ]]^{M}ρ) m_{i} ([[σ′]]^{M}ρ) ([[C, E ⊢ new c: σ′)]]^{M}ρ)

Clearly this expression differs from Mitchell’s only in the replacement of the second occurrence of c by new c. As a result of this correspondence we believe it is fair to say that the definition given here is a faithful reflection of the spirit of the definition given in [Mit90], modified to correspond to a somewhat different language.