An operational semantics for TOOPLE: A statically-typed object-oriented programming

language ^{∗}

Kim B. Bruce  Jonathan Crabtree^{†} Gerald Kanapathy^{‡}

Department of Computer Science Williams College Williamstown, MA 01267 kim@cs.williams.edu

Abstract

In this paper we present an operational semantics for the language TOOPLE, a staticallytyped functional object-oriented programming language which has a number of desirable properties. The operational semantics, given in the form of a natural semantics, is significantly simpler than the previous denotational semantics for the language. A “subject reduction” theorem for the natural semantics provides a proof that the language is type-safe. We also show that the natural semantics is consistent with the denotational semantics of the language. Computing Review categories: D3.2 Object Oriented Languages, F3.2 Operational Semantics, F3.3 Type structure.

1 Introduction

Object-oriented languages promise to provide support for reusability and modularity of program code. Reusability is achieved by inheritance, which allows subclasses to be created easily from classes, and by subtyping, which allows elements of a subtype to be used in contexts which expect elements of the supertype. Modularity is achieved by the encapsulation of methods, which gives programs independence from the implementation details of the classes they use.

Static typing has clear advantages for programming languages as long as it does not interfere with expressibility in the language. Unfortunately, most extant statically-typed object-oriented languages are either type-unsafe or are unduly restrictive in the programs accepted by the type checker. For example, the holes in the type system for Eiffel are wellknown, while C++, Object Pascal, and Modula-3 are unduly restrictive in not allowing changes in the types of methods in subclasses (derived classes). The design of the language TOOPLE^{1} (see [Bru93a, Bru93b]) represents progress in solving both of these problems by ensuring type-safety while providing greater expressibility than other statically-typed object-oriented languages which are type-safe. The introduction to [Bru93b] includes an extensive comparison with other statically-typed object-oriented programming languages. We simply remark here that a key to the combination of safety and greater expressibility in TOOPLE is the separation of the subclass and subtype hierarchies, as suggested in [CHC90].

∗This research was partially supported by NSF grant CCR - 9121778.

†Current address: Department of Computer and Information Science, University of Pennsylvania.

‡Current address: Department of Computer Science, Rice University.

An important design goal of TOOPLE was to provide a modular type-checking system for the language. In most current object-oriented languages, the inheritance mechanism creates problems for the type checker. While a program that merely uses a class can be written and checked independently of the class code (assuming that an interface and corresponding type specification are given), to type check a class which inherits from another class, one often needs to go back and repeat the process of type checking the bodies of inherited methods from the superclass. This is necessary in order to ensure that overriding other methods from the superclass (in particular, changing their types) does not affect the types of inherited methods.

In an ideal object-oriented language, the inheritance mechanism itself will be modular. That is, one should be able to write and check programs, and find errors, looking only at the types of the superclass and the code of the modifications. For instance, a typechecking mechanism with these properties will be necessary if vendors are to be able to distribute libraries in compiled form only. The type-checking rules for TOOPLE do provide this modularity. The user need only know the type of a class in order to define and type check any subclass of that class.

We can summarize these important properties of TOOPLE as follows:

• Type safety: If a term has a type, τ, then the result of evaluating that term will be an element of type τ. In particular, no error messages of the form “message not understood” will arise during the evaluation of a well-typed term.

• Modularity of type-checking: If a class has a type, then methods inherited in a subclass continue to have the types specified in the superclass. Moreover, in order to type-check a subclass we need not have access to the bodies of methods inherited from the superclass. Only the types of the inherited methods are needed from the superclass.

Earlier papers on TOOPL provided a denotational semantics of the language. Building on earlier work of Cook et al. ([CHC90]) and Mitchell ([Mit90]) on the semantics of inheritance in typed programming languages, the denotational semantics is based on a higher-order extension of F_{≤}, the bounded second-order lambda calculus. The denotational semantics involves fixed points at both the element and type level, making the semantics more complex than might be desired.

For some purposes, such as implementation or program verification, a natural semantics is more useful. Thus, in this paper, we present an operational semantics for the language. This semantics is significantly less complex than the denotational semantics, as it involves no higher order concepts and no fixed points. The operational semantics is given in the form of a natural semantics (see [NN92] or [Gun92] for more details on natural semantics).

1TOOPLE is a minor modification of TOOPL (Typed Object-Oriented Programming Language) in which class terms are required to include slightly more typing information as part of their syntax. This change was necessary in order to provide an algorithm for type-checking terms and ensure that each term has a minimal type.

In [Bru93a, Bru93b], the first author showed that the language is type-safe by showing that the meaning of a term is included in the set of values corresponding to its type. Here we provide an alternative proof of this fact by proving a “subject reduction” theorem for the operational semantics. This theorem states that if a term has a type, then the term which results from fully reducing (evaluating) the original term also has the same type.

Of course when one provides a different style of semantics for a language, one is in danger of creating a semantics which is no longer consistent with the original one. Thus we prove that the operational semantics is consistent with the earlier denotational semantics. In particular if a term e reduces to a term v in the operational semantics, we show that e and v have the same denotational semantics.

In section 2 of this paper, we provide a very brief description of the syntax of TOOPLE, along with a few simple sample programs. In section 3, we present the operational and denotational semantics of TOOPLE as well as some preliminary lemmas which are necessary for the results in the rest of the paper. This includes a statement of the minimal typing theorem for TOOPLE, which was proved in [BCD^{+}93]. In section 4, the subject reduction theorem is proved. As noted above, this leads to an alternative proof of the type safety of the language. In section 5, the natural semantics of TOOPLE is shown to be consistent with the denotational semantics of the language. Finally, in the last two sections we provide a brief comparison with other attempts at modeling object-oriented programming languages, and conclude with a discussion of other results on TOOPLE.

Because of space restrictions, this version of the paper only discusses the restriction of TOOPLE to a language in which classes have no instance variables.

2 A brief introduction to TOOPLE

TOOPLE is a statically-typed functional object-oriented programming language. It offers full support for object-oriented features including objects, classes, methods, hidden instance variables, dynamic method invocation, subclasses, and subtypes. Moreover, TOOPLE provides mechanisms to allow the programmer to refer to the current object (self ), its type (MyType), and the record of methods of its superclass (super). We presume the reader is familiar with the fundamental concepts of object-oriented languages, though they are described briefly below.

Objects consist of a collection of instance variables, representing the state of the object, and a collection of methods, which are routines for manipulating the object. When a message is sent to an object, the corresponding method of the object is executed. Classes are extensible templates for creating objects. In particular, classes contain initial values for instance variables and the bodies for methods. All objects generated from the same class share the same methods, but may contain different values for their instance variables. A subclass may be defined from a class by either adding to or modifying the methods and instance variables of the original class. (Restrictions on the modification of the types of methods and instance variables in subclasses are necessary in order to preserve typesafety.) Methods which are not modified in subclasses are said to be inherited from their superclass.

All terms of the language, including both classes and objects, have associated types. We say type T is a subtype of U if a value of type T can be used in any context in which a value of type U is expected. Note that subtyping depends only on the type of values, while subclasses and inheritance depends upon their implementations. It was pointed out in [CHC90] that if one class is a subclass of another, the type of the objects generated by the subclass need not be a subtype of the type of the objects generated by the original class.

A bound variable, usually written as self , may be used in methods as a name for the current object. Since our language is statically typed, it will be necessary to assign a type to all occurrences of self . Because the meaning of self will change when methods are inherited in subclasses, its type will change as well. Thus we will use a bound variable, usually written as MyType, as the type of self .

Finally, when new definitions are given to methods in a subclass, it is useful to be able to refer to the methods of the superclass. For instance, one often wishes to apply the method body from the superclass and then perform a few more operations before returning from the redefined method. We provide a bound variable, usually written as super, to refer to the record of methods of the superclass.

We note that instance variables are omitted in this conference paper to keep the language as simple as possible. The addition of instance variables raises no serious complications in the development of the technical results.

The types for TOOPLE are defined as follows:

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

1. If t ∈ V^{T p} ∪ C^{T p} 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 , then {m_{1} : τ_{1}; …; m_{n} : τ_{n}} is a (record) type expression.

4. If τ is a record type expression and MyType ∈ V^{T p}, then ObjectT ype(MyType)τ and ClassT ype(MyType)τ are type expressions. MyType is considered to be a bound variable in these two type expressions, and binds all free occurrences of MyType in τ.

Types of the form σ → τ represent function spaces. Object types are written in the form ObjectType(MyType)τ, where τ is the type of the record of methods of the object. Similarly, class types are of the form ClassType(MyType)τ.

Definition 2.2 The pre-terms of TOOPLE are as follows:

M ::= x | if B then M else N | fun(v : σ) M | M N | M = N | e.m_{i} |

{m_{1} = e_{1}, …, m_{n} = e_{n}} | class(self : MyType ≤_{meth} ObjectType(MyType)τ)e |

new c | o ⇐ m | obj (self : MyType ≤_{meth} ObjectType(MyType)τ)e |
update c by(self : MyType ≤_{meth} ObjectType(MyType)τ′; super){m_{1} = e′_{1}} |

extend c with(self : MyType ≤_{meth} ObjectType(MyType)τ′; super){m_{n+1} = e_{n+1}}.

In the above grammar, B, M, N, c, o, e, and the various e_{i} refer to pre-terms.

Most of the pre-terms should be self-explanatory. A pre-term of the form class(self : MyType ≤_{meth} ObjectType(MyType)τ)e represents a class whose method bodies are contained in the record e with type τ.^{2} As discussed earlier, self can be used in the body of a method to refer to the object executing the method. MyType represents the type of self .

A pre-term of the form obj (self : MyType ≤_{meth} ObjectType(MyType)τ)e represents an object with method bodies in e.^{3} If c is a class then new c represents an object generated from c. “Update” and “extend” pre-terms provide ways of modifying or adding new methods to a class. A pre-term of the form o ⇐ m represents sending the message m to object o. Sample TOOPLE code is given at the end of this section.

Aside from the subtyping relation (≤) discussed above, we need another ordering on object types which is related to types obtained via subclasses. This ordering, ≤_{meth}, is a pointwise ordering on method types. If o is an object of type ObjectType(MyType)τ, generated from class c, and ObjectType(MyType)τ′ is the type of an object generated from a subclass of c, then ObjectType(MyType)τ′ ≤_{meth} ObjectType(MyType)τ. The axioms and rules for ≤ and ≤_{meth} are given in Appendix A. The subtyping rules and axioms are given with respect to a collection, C, of simple type constraints of the form t ≤ τ and t ≤_{meth} τ. See [Bru93b] or [Bru93a] for further explanation. Note that C ⊢ ObjectType(MyType)τ′ ≤_{meth} ObjectType(MyType)τ iff C ⊢ τ′ ≤ τ.

Most rules should be familiar with the possible exception of the subtyping rule for object types. This rule arises from the fact that object types are defined recursively (in order for MyType to stand for the type of the object in its type definition).

The actual terms of TOOPLE are those which can be type checked with respect to a collection, C, of simple type constraints, and an assignment, E, of types to variables. The type-checking rules for TOOPLE can be found in [Bru93b] or [Bru93a], where they are explained in some detail. Note that it is possible to redefine a method in a subclass in such a way that the type of the new method is a subtype of the type in the superclass.

The following restrictions on type constraint systems will allow us to show that each term has a minimum type.^{4}

Definition 2.3 Let C be a type constraint system. We say that C is manageable if the following conditions hold, where s and t range over type variables:

2The addition of ≤_{meth} ObjectType(MyType)τ after MyType in class definitions is necessary in order to obtain a minimal type for all terms of TOOPLE. This addition for class, update, and extend terms is the only difference between the language TOOPL described in previous papers and the language presented here.

3Obj terms are not actually in the source language. However they are used as an intermediate form of a term in the natural semantics. As a result, we include them here.

4In [BCD^{+}93] we restrict type constraints systems even further. However the definition of manageable type constraints given here is sufficient to prove minimum types for terms.

1. If (t ≤_{meth} ObjectType(MyType)τ) ∈ C, then there is no term of the form (s ≤ t) ∈ C.

2. There are no terms of the form (t ≤ ObjectType(MyType)τ) ∈ C.

These two rules essentially disallow introducing a type variable which is a subtype of an object type.

A collection of type-checking rules for computing the minimal types of terms of TOOPLE can be found in Appendix B. These rules represent an algorithm for computing the minimal type of a term of TOOPLE as long as C is a manageable type constraint system. Note that there are two rules for each of function application (MAppl and MAppl’), record field extraction (MProj and MProj’), and message passing (MMsg and MMsg’). These are necessary since these operations may be applied to items whose minimum types are type variables. The most important place where this arises is when a message is sent to self , whose type is MyType.

The following theorem from [BCD^{+}93] gives the relation between the type-checking rules given in [Bru93a, Bru93b] and the minimal typing rules given in Appendix B.

Theorem 2.4 Suppose that C is manageable. Then C, E ⊢ e : τ according to the typechecking rules in [Bru93b] or [Bru93a] iff there is a type τ′ such that C, E ⊢_{M} e : τ′ and C ⊢ τ′ ≤ τ.

As a result, it will be sufficient to use the rules for deriving minimum types given in Appendix B. This will be useful later in the paper after we have introduced the natural (operational) semantics of TOOPLE. We will show that the minimum types of terms generated in the evaluation of a TOOPLE term are all subtypes of the minimum type of the original term.

We end this brief introduction with the inclusion of a few examples of terms and their types from [Bru93b].

PointClass =

class(self : MyType ≤_{meth} ObjectType(MyType){x, y : Int; eq : MyType → Bool}) {x = 0, y = 0, eq = fun(p : MyType)((self ⇐ x) = (p ⇐ x))&((self ⇐ y) = (p ⇐ y))}

has type PointClassType = ClassType(MyType){x, y : Int; eq : MyType → Bool}, and represents points with x, y, and eq methods.

PtObj = new PointClass is an object generated from PointClass. Its type is

PointType = ObjectType(MyType){x, y : Int; eq : MyType → Bool}.

Let

ColorPointType = ObjectType(MyType){x, y : Int; c : ColorT ype; eq : MyType → Bool}.

We can add a color method to PointClass using the “extend” term:

ColorPointClass = extendPointClass by(self :MyType≤_{meth} ColorPointType; super) {c = Red}

If we wish to change the method eq so that it now also checks the color components of two records, we define NuColorPtClass = update ColorPointClass with (self :MyType ≤_{meth} ColorPointType;

super) {eq = fun(p:MyType) super.eq(p) & ((self ⇐ c) = (p ⇐ c)) }.

Notice the use of super in the updated eq method to perform the old eq body, before testing the equality of colors.

Finally we note that by rule (MMsg) the term PtObject ⇐ eq has type PointType → Bool. On the other hand, if ColorPtObject is an object generated from NuColorPointClass having type ColorPointType, then ColorPtObject ⇐ eq has type ColorPointType → Bool. This illustrates the flexibility obtained by the use of self and its type MyType.

3 Semantic definitions and preliminary lemmas

In this section we present some fundamental definitions and lemmas which will be useful in the proofs in the following sections. We also present the natural and denotational semantics for TOOPLE. We begin with a description of some of our notation.

Definition 3.1 We write a ≡ b to denote that a and b are syntactically identical, up to renaming of bound variables.

Definition 3.2 We write e[a/x] to denote the substitution of a for x in e, where we first rename bound variables as necessary to avoid capture of free variables.

The natural semantics and denotational semantics for terms of TOOPLE can be found in Appendices C and D. In the natural semantics we will use C, E ⊢ e : τ ↓ v as an abbreviation for C, E ⊢ e : τ, and e ↓ v. We read this as e is a term with type τ which reduces to v, which is an irreducible term.

The irreductible terms are constants, function abstractions, records, classes, and objects. Most rules for non-object-oriented features should be familiar. By RRecord, RClass, RAppl, and RNew, the evaluation strategy is “lazy.” That is, subterms are not evaluated until necessary.

The most interesting rule is RMsg, for sending a message to an object. When a term of the form o ⇐ m is evaluated, o is reduced to a term of the form, o′ = obj (self : MyType ≤_{meth} γ′)e, where e is its record of methods. Then self is replaced by o′ and MyType by γ′ in e, which is then evaluated to a record term. Finally, the record component corresponding to m is evaluated and returned as the final answer.

While self is an irreducible value, it should be noted that when a message is sent to an object, all occurrences of self are replaced by the object, so self no longer occurs in the method body when it is actually evaluated.

The subject reduction theorem, presented in section 4, will show that the reduced term, v, will have a minimal type that is a subtype of the type of the original term e. It follows that, in the original typing system, if C, E ⊢ e : τ ↓ v, then C, E ⊢ v : τ.

The substitution lemma for types is necessary to prove the subject reduction theorem. It ensures that substitution is a well-behaved operation with respect to the subtyping relation. More formally:

Lemma 3.3 Let C be manageable and let x be a variable. Assume that there exist terms and types such that C, E ⊢_{M} e : τ, C, E ⊢_{M} x : σ, C, E ⊢_{M} a : σ′, and C ⊢ σ′ ≤ σ. Then there exists some τ′ such that C, E ⊢_{M} e[a/x] : τ′ and C ⊢ τ′ ≤ τ. Furthermore, if τ is a class type, then τ′ ≡ τ.

Proof. The proof is by induction on the proof of minimum typing. The base case is straightforward. We present only a few of the inductive cases.

Inductive assumption. For all C, E, if C, E ⊢_{M} e′ : ρ in fewer than n steps and x and a are as described above, then there exists some ρ′ such that C, E ⊢_{M} e′[a/x] : ρ′, where C ⊢ ρ′ ≤ ρ. Furthermore, if ρ is a ClassType type, then ρ′ = ρ.

MClass. C, E ⊢_{M} class(self : MyType ≤_{meth} ObjectType(MyType)τ)e :

ClassType(MyType)τ.

Case 1: x = self . In this case the expression is unchanged by the substitution as self is a bound variable of the term. As a result the type of the term is unchanged by the substitution.

Case 2: x ≠ self . Thus, (class(self : MyType ≤_{meth} ObjectType (MyType)τ)e)[a/x] ≡ class(self : MyType ≤_{meth} ObjectType(MyType)τ)e′, where e′ ≡ e[a/x]. By induction, C, E ⊢_{M} e′ : τ′, where C ⊢ τ′ ≤ τ. Since classes have unique types, the class typing rule allows us to prove that C, E ⊢_{M} (class(self : MyType ≤_{meth} ObjectType(MyType)τ)e)[a/x] : ClassType(MyType)τ.

MMsg. C, E ⊢_{M} o ⇐ m_{i} : τ_{i}[γ/MyType].

We may assume that C, E ⊢_{M} o : γ, where γ = ObjectType(MyType){…; m_{i} : τ_{i}; …}, by the typing rules. By induction, C, E ⊢_{M} o[a/x] : γ′, where γ′ = ObjectType(MyType) {…; m_{i} : τ′_{i}; …}, and C ⊢ γ′ ≤ γ. Note that the minimum type of o[a/x] must be an ObjectType type, since, by the second part of the definition of manageability, there can be no expressions of the form (t ≤ ObjectType(MyType)τ) ∈ C. By the object subtyping rule, C ∪ {s ≤ t} ⊢ {…; m_{i} : τ′_{i}; …}[s/MyType] ≤ {…; m_{i} : τ_{i}; …}[t/MyType], and it follows that C ∪ {s ≤ t} ⊢ τ′_{i}[s/MyType] ≤ τ_{i}[t/MyType]. Finally, because s and t do not occur in C, substitution of the types of the γ′ and γ for s and t gives us that C ⊢ τ′_{i}[γ′/MyType] ≤ τ_{i}[γ/MyType].

MMsg’. C, E ⊢_{M} o ⇐ m_{i} : τ_{i}[t/MyType].

C, E ⊢_{M} o : t, where t is a type variable. Thus (t ≤_{meth} ObjectType(MyType){…; m_{i} : τ_{i}; …}) ∈ C. Note that (o ⇐ m_{i})[a/x] ≡ o[a/x] ⇐ m_{i}. Now, by induction, C, E ⊢_{M} o[a/x] : t′, where C ⊢ t′ ≤ t. But the first part of the definition of C being manageable asserts that there can be nothing of the form (r ≤ t) ∈ C, and, since t is a variable, no other proof can exist which shows that t′ is a subtype of t. Therefore, t = t′, and so C, E ⊢_{M} o[a/x] ⇐ m_{i} : τ_{i}[t/MyType].

MUpdate. C, E ⊢_{M} update c by (self : MyType ≤_{meth} ObjectType(MyType)γ′; super)

{m_{1} = e′_{1}} : ClassType(MyType) γ′.

where γ′ = {m_{1} : τ′_{1}; m_{2} : τ_{2}; …; m_{n} : τ_{n}}.

By the observations in the (MClass) case, we may assume that x ≠ self , as no change will take place otherwise. Now note that

(update c by (self : MyType ≤_{meth} ObjectType(MyType) γ′; super){m_{1} = e′_{1}})[a/x]

≡ update c[a/x] by (self : MyType ≤_{meth} ObjectType(MyType) γ′′; super) {m_{1} = e′_{1}[a/x]}).

By the typing rules, c has some ClassType type, and so by induction, c[a/x] must have the same type. Thus C, E ⊢_{M} c[a/x] : ClassType(MyType){m_{1} : τ_{1}; …; m_{n} : τ_{n}}. Also, by induction, C, E ⊢_{M} e′_{1}[a/x] : τ′′_{1}, where C ⊢ τ′′_{1} ≤ τ′_{1}. Thus we can use (MUpdate) to prove that C, E ⊢_{M} update c[a/x] by (self : MyType ≤_{meth} ObjectType(MyType)γ′; super){m_{1} = e′_{1}[a/x]}) : ClassType γ′. Thus the update expression after performing substitution has exactly the same type as it did before the substitution.

4 Subject reduction theorem

The subject reduction theorem shows that types are preserved under the reductions of our natural semantics. This can be used to show that TOOPLE is type-safe, since no computation on a well-typed term can ever result in a term which is ill-typed.

Theorem 4.1 Subject Reduction Theorem Assume that C, E ⊢_{M} e : τ ↓ e′. Then there is a type τ′ such that C, E ⊢_{M} e′ : τ′, where C ⊢ τ′ ≤ τ. Furthermore, if τ is a class type then τ′ ≡ τ.

Proof. The proof is by induction on the number of steps used in the reduction.

Base case. If any of the rules RAbs, RConst, RRecord, RClass, or RObj apply, then e′ ≡ e, so the theorem holds trivially.

Inductive cases. Suppose that for all C, E, and for all e′ such that e′ ↓ e′′ in fewer than n steps, if C, E ⊢_{M} e′ : τ′ ↓ e′′ then there is some τ′′ such that C, E ⊢_{M} e′′ : τ′′ and C ⊢ τ′′ ≤ τ′. Furthermore, if τ′ is a class type then τ′ ≡ τ′′.

The proof proceeds by cases on the last semantic rule applied. In each case we assume that e is typable and that there is some v such that e ↓ v, in n steps. We begin each case by specifying the form of e and the minimum type of e.

We include only a few interesting cases in this conference paper. We note that Lemma 3.3 is needed in the (omitted) case for function application.

RNew. C, E ⊢_{M} new c : ObjectType(MyType)τ.

By the typing rules, C, E ⊢_{M} c : ClassType(MyType)τ, and by the semantic rule, c ↓ class(self : MyType ≤_{meth} ObjectType(MyType)τ)e′. By induction, C, E ⊢_{M} class(self : MyType ≤_{meth} ObjectType(MyType)τ)e′ : ClassType(MyType)τ, as the types of classes are invariant. By the semantic rule v ≡ obj(self : MyType ≤_{meth} ObjectType(MyType)τ)e′, and we can prove that C, E ⊢_{M} obj(self : MyType ≤_{meth} ObjectType(MyType)τ)e′ : ObjectType(MyType)τ.

RMsg. C, E ⊢_{M} o ⇐ m_{i} : τ_{i}[γ/MyType].

It is clear that o is typable, as the entire expression is typable, and we proceed by cases on the last rule of the proof of minimum type for o ⇐ m_{i}.

MMsg. C, E ⊢_{M} o : ObjectType(MyType){…; m_{i} : τ_{i}; …}.

Note that γ = ObjectType(MyType){…; m_{i} : τ_{i}; …}. Since o ↓ obj(self : MyType ≤_{meth} γ′)e for γ′ = ObjectType{…; m_{i} : τ′_{i}; …}, then, by induction,

C, E ⊢_{M} obj(self : MyType ≤_{meth} γ′)e : ObjectType(MyType)γ′,  (1)
where C ⊢ γ′ ≤ γ.  (2)

By the subtyping rules, the only way (2) could hold is if C ∪{s ≤ t} ⊢ τ′_{i}[s/MyType] ≤ τ_{i}[t/MyType]. It follows that

C ⊢ τ′_{i}[γ′/MyType] ≤ τ_{i}[γ/MyType].  (3)

By (1) and our typing rule for obj terms,

C ∪ {MyType ≤_{meth} γ′}, E ∪ {self : MyType} ⊢_{M} e : {…; m_{i} : τ′′_{i}; …},  (4)

where

C ∪ {MyType ≤_{meth} γ′} ⊢ τ′′_{i} ≤ τ′_{i}.  (5)

Let e′ = e[obj (self : MyType ≤_{meth} γ′)e/self , γ′/MyType]. By Lemma 3.3, it follows that

C, E ⊢_{M} e′ : {…; m_{i} : τ′′′_{i}; …}  (6)

where C ⊢ τ′′′_{i} ≤ τ′′_{i}[γ′/MyType].

By (5), it follows that

C ⊢ τ′′_{i}[γ′/MyType] ≤ τ′_{i}[γ′/MyType].  (7)

Furthermore, since e′ ↓ {…, m_{i} = e_{i}, …}, it follows by induction that C, E ⊢_{M} e_{i} : ρ, where

C ⊢ ρ ≤ τ′′′_{i}.  (8)

Since e_{i} ↓ v, by induction,

C, E ⊢_{M} v : ρ′, where C ⊢ ρ′ ≤ ρ ≤ τ′′′_{i} ≤ τ′′_{i}[γ′/MyType].  (9)

Thus, by (3), (7), (9), and transitivity,

C ⊢ ρ′ ≤ τ_{i}[γ/MyType].

In summary, if (e ⇐ m_{i}) ↓ v, where C, E ⊢_{M} e ⇐ m_{i} : τ_{i}[γ/MyType], then C, E ⊢_{M} v : ρ′, with C ⊢ ρ′ ≤ τ_{i}[γ/MyType], as desired.

MMsg’. C, E ⊢_{M} o : t, where t is a type variable.

Note that γ = t. The other hypothesis of the (MMsg’) rule must be

(t ≤_{meth} ObjectType(MyType){…; m_{i} : τ_{i}; …}) ∈ C.

By the semantic rule (RMsg), o ↓ obj(self : MyType ≤_{meth} {…; m_{i} : τ′_{i}; …})e. Thus, by induction, C, E ⊢_{M} obj(self : MyType ≤_{meth} {…; m_{i} : τ′_{i}; …})e : t′, where C ⊢ t′ ≤ t. However, any proof of minimum type for an obj expression must end in the (MObj) typing rule. Thus t′ is of the form ObjectType(MyType)τ, and so C ⊢ ObjectType(MyType)τ ≤ t. But this implies something of the form (r ≤ t) ∈ C, which is impossible due to the first part of the definition of manageability. Thus it cannot be the case that C, E ⊢_{M} e : t, where t is a type variable.

The subject reduction theorem ensures that our programming language is type-safe, by showing that all intermediate terms in a computation can be typed (with a subtype of the type of the original term). In particular, this implies that no term of the form f(e) occurs in the computation of a well-typed term if the types of f and e do not match. Similarly no object will be sent a message that it cannot handle in a computation on a well-typed term (since such a subterm would be ill-typed).

Thus, if we begin with a term with no free variables, a computation will proceed in a type-safe way to a value or may loop. However, it will never become stuck at a non-value since each well-typed term corresponds to a computation rule in the natural semantics.

5 Consistency of the natural semantics with the denotational semantics

The theoretical results about TOOPL in [Bru93a] are given in terms of the denotational semantics presented in Appendix D. Of course, we would like to be able to claim that any results using the natural semantics presented here actually refer to the same language as the one Bruce described.

We will prove that the natural semantics presented in appendix C is sound with respect to the denotational semantics. To do this, we must show that, whenever a term M reduces to a term v in the natural semantics, their meanings are the same according to the denotational semantics.

We first need the following substitution lemma for terms.

Lemma 5.1 Suppose s is not free in C or E, C ∪ {s ≤ τ}, E ∪ {x : s} ⊢ M : γ, C, E ⊢ a : σ, and C ⊢ σ ≤ τ. Then

1. C, E ⊢ M[a/x, σ/s] : γ[σ/s], and

2. [[C ∪ {s ≤ τ}, E ∪ {x : s} ⊢ M : γ]]ρ[[[C, E ⊢ a : σ]]ρ/x, [[σ]]ρ/s] = [[C, E ⊢ M[a/x, σ/s] : γ[σ/s]]]ρ.

We now prove the correctness of the natural semantics with respect to the denotational semantics.

Theorem 5.2 If C, E ⊢ M : τ ↓ v, then [[C, E ⊢ M : τ]]ρ = [[C, E ⊢ v : τ]]ρ

Proof. We will prove the natural semantics correct by induction on the number of steps in the reduction.

Base Cases. For terms that can be reduced by one of the rules RAbs, RConst, RRecord, RClass, or RObj , the theorem is clearly true, since each of these rules states that M ↓ M.

Inductive Cases. We prove the consistency of the natural semantics for all terms whose reduction is of length n, where n > 1, assuming that the semantics are correct for all terms whose reductions are of length less than n. We provide only a few of the more interesting cases.

Function application. The natural semantics rule for function application is RAppl, which gives us, by the induction hypothesis, that

\begin{aligned}[[C, E ⊢ e : σ → τ]]ρ & = [[C, E ⊢ λx : σ.M : σ → τ]]ρ \\ & = λd ∈ A^{σ}.[[C, E ∪ \{x : σ\} ⊢ M : τ]]ρ[d/x]. \end{aligned}

Then

[[C, E ⊢ e e′ : τ]]ρ = ([[C, E ⊢ e : σ → τ]]ρ)([[C, E ⊢ e′ : σ]]ρ)
= (λd ∈ A^{σ}.[[C, E ∪ {x : σ} ⊢ M : τ]]ρ[d/x])([[C, E ⊢ e′ : σ]]ρ)
= [[C, E ∪ {x : σ} ⊢ M : τ]]ρ[[[C, E ⊢ e′ : σ]]ρ/x]
= [[C, E ⊢ M[e′/x] : τ]]ρ

where the final step follows from Lemma 5.1, part 2.

Because C, E ⊢ M[e′/x] : τ ↓ v by induction, we obtain

[[C, E ⊢ M[e′/x] : τ]]ρ = [[C, E ⊢ v : τ]]ρ.

Thus

[[C, E ⊢ e e′ : τ]]ρ = [[C, E ⊢ v : τ]]ρ.

Objects. The rule for creation of an object from a class is RNew. The corresponding denotational rule is:

[[C, E ⊢ new c : ObjectType(MyType)τ]]ρ = FIX (([[C, E ⊢ c : ClassType(MyType)τ]]ρ)([[ObjectType(MyType)τ]]ρ)).

Now, by the induction hypothesis,

[[C, E ⊢ c : ClassType(MyType)τ]]ρ = [[C, E ⊢ class(self : MyType)e : ClassType(MyType)τ]]ρ.

Substituting and using the semantics of objects we get:

[[C, E ⊢ new c : ObjectType(MyType)τ]]ρ

= FIX (([[C, E ⊢ class(self : MyType)e : ClassType(MyType)τ]]ρ)

([[ObjectType(MyType)τ]]ρ))

= [[C, E ⊢ obj (self : MyType)e : ObjectType(MyType)τ]]ρ.

Message passing. The next case to consider is an expression that sends a message to an object. The natural semantics rule for this is RMsg. Without loss of generality we presume that C, E ⊢_{M} o ⇐ m_{i} : τ_{i}[γ/MyType]. We proceed by cases on the last typing rule applied: \underline{Case i.} C, E ⊢_{M} o : γ for γ = ObjectType(MyType)\{m_{1} : τ_{1}; …; m_{n} : τ_{n}\}.

The denotational definition for message passing is Msg:

[[C, E ⊢ o ⇐ m_{i} : τ_{i}[γ/MyType]]]ρ = (convert[[[{m_{i} : τ_{i}}]]ρ[[[γ]]ρ/MyType]][[[γ]]ρ][[C, E ⊢ o : γ]]ρ) (m_{i}).

By the convert rules for records in [BL90], if σ ≤_{A} [[{s_{1} : σ_{1}; …, s_{k} : σ_{k}; …; s_{n} : σ_{n}}]]ρ, and r ∈ A^{[[σ]]ρ}, then

(convert[[[{s_{1} : σ_{1}; …; s_{n} : σ_{n}}]]ρ][σ]r)(s_{k}) = (convert[[[{s_{k} : σ_{k}}]]ρ][σ]r)(s_{k}).

By the semantics of object types,

[[γ]]ρ = [[{m_{1} : τ_{1}; …; m_{n} : τ_{n}}]]ρ[[[γ]]ρ/MyType].

Thus,

(convert[[[{m_{i} : τ_{i}}]]ρ[[[γ]]ρ/MyType]][[[γ]]ρ][[C, E ⊢ o : γ]]ρ) (m_{i})

= (convert[[[{m_{1} : τ_{1}; …; m_{n} : τ_{n}}]]ρ[[[γ]]ρ/MyType]][[[γ]]ρ][[C, E ⊢ o : γ]]ρ) (m_{i})

= (convert[[[γ]]ρ][[[γ]]ρ][[C, E ⊢ o : γ]]ρ) (m_{i})

= [[C, E ⊢ o : γ]]ρ(m_{i}).

Hence [[C, E ⊢ o ⇐ m_{i} : τ_{i}[γ/MyType]]]ρ = [[C, E ⊢ o : γ]]ρ(m_{i}).

Since o ⇐ m_{i} ↓ v, if follows that

o ↓ obj(self : MyType ≤_{meth} γ′)e  (10)

for some γ′ = ObjectType(MyType)τ′, and some record e such that

e′ = e[obj(self : MyType ≤_{meth} γ′)e/self , γ′/MyType] ↓ {m_{1} = e_{1}, …, m_{k} = e_{k}}, (11)

and

e_{i} ↓ v.  (12)

By the subject-reduction theorem and (10), C ⊢ γ′ ≤ γ.

Let C′ = C ∪ {MyType ≤_{meth} ObjectType(MyType)τ′} and E′ = E ∪ {self : MyType}. By the denotational rule for objects, Obj ,

[[C, E ⊢ obj (self : MyType)e : γ′]]ρ = FIX (([[C, E ⊢ class(self : MyType)e : ClassType(MyType)τ′]]ρ)([[γ′]]ρ)). = FIX ((λξ ≤ [[τ′]]ρ[ξ/MyType].λo ∈ A^{ξ}.[[C′, E′ ⊢ e : τ′]]ρ[ξ/MyType, o/self ])([[γ′]]ρ)) = FIX (λo ∈ A^{[[γ′]]ρ}.[[C′, E′ ⊢ e : τ′]]ρ[[[γ′]]ρ/MyType, o/self ]).

Therefore,

[[C, E ⊢ obj (self : MyType)e : γ′]]ρ = [[C′, E′ ⊢ e : τ′]]ρ[[[γ′]]ρ/MyType, [[C, E ⊢ obj (self : MyType)e : γ′]]ρ/self ], = [[C, E ⊢ e′ : τ′[γ′/MyType]]]ρ, by Lemma 5.1. = [[C, E ⊢ {m_{1} = e_{1}, …, m_{i} = e_{i}, …, m_{n} = e_{n}} : τ′[γ′/MyType]]]ρ, by induction.

Because C ⊢ γ′ ≤ γ and both are object types, it follows that C ⊢ τ′[γ′/MyType] ≤ {m_{1} : τ_{1}; …; m_{n} : τ_{n}}[γ/MyType]. By induction, (10) and the above expansion of [[obj (self : MyType)e]]ρ,

[[C, E ⊢ o : γ]]ρ = [[C, E ⊢ {m_{1} = e_{1}, …, m_{n} = e_{n}} : τ[γ/MyType]]]ρ,

so

([[C, E ⊢ o : γ]]ρ)(m_{i}) = [[C, E ⊢ e_{i} : τ_{i}[γ/MyType]]]ρ = [[C, E ⊢ v : τ_{i}[γ/MyType]]]ρ

by the Rec rule and the induction hypothesis, respectively. We conclude, then, that

[[C, E ⊢ o ⇐ m_{i} : τ_{i}[γ/MyType]]]ρ = [[C, E ⊢ v : τ_{i}[γ/MyType]]]ρ.

\underline{Case ii.} C, E ⊢_{M} o : γ for t a type variable.

By assumption, o ↓ obj(self : MyType ≤_{meth} γ′)e where γ′ (which is also the type of the object expression) is an object type. By the subject reduction theorem, C ⊢ γ′ ≤ t. However, by the definition of manageable type constraint system, a type variable may not be shown to be a subtype of an object type. Thus this case will never arise!

Class update. Classes are updated according to the rule RUpdate.

Let τ = {m_{1} : τ_{1}; …; m_{n} : τ_{n}} and τ′ = {m_{1} : τ′_{1}; m_{2} : τ_{2}; …; m_{n} : τ_{n}}. The denotational rule, Update, is:

[[C, E ⊢ update c by (self : MyType ≤_{meth} ObjectType(MyType)τ′; super){m_{1} = e′_{1}} : ClassType(MyType)τ′]]ρ = λξ ≤ [[τ′]]ρ[ξ/MyType].λo ∈ A^{ξ}.f,

where

C′  = C ∪ {MyType ≤_{meth} ObjectType(MyType)τ′},
E′  = E ∪ {self : MyType},
dom(f) = {m_{1}, …, m_{n}},
f(m_{1}) = [[C′, E′ ⊢ e′_{1} : τ′_{1}]]ρ[ξ/MyType, o/self , s/super],
f(m_{j}) = s(m_{j}), ∀j : 2 ≤ j ≤ n,
s  = [[C, E ⊢ c : ClassType(MyType)τ]]ρ(ξ)(o).

Since

C, E ⊢ c : ClassType(MyType)τ ↓ class(self : MyType ≤_{meth} ObjectType(MyType)τ)e,

it follows by induction and the semantics of classes that

s = [[C′, E′ ⊢ e : τ]]ρ[ξ/MyType, o/self ].

Let e′ = {m_{1} = e′′_{1}, m_{2} = e.m_{2}, …, m_{n} = e.m_{n}}, where e′′_{1} = e′_{1}[e/super]. By Class:

[[C, E ⊢ class(self : MyType ≤_{meth} ClassType(MyType)τ′; super)e′ : ClassType(MyType)τ′]]ρ = λξ ≤ [[τ′]]ρ[ξ/MyType].λo ∈ A^{ξ}.[[C′, E′ ⊢ e′ : τ′]]ρ[ξ/MyType, o/self ]

To complete the proof we must show that

f(m_{i}) = ([[C′, E′ ⊢ e′ : τ′]]ρ[ξ/MyType, o/self ])(m_{i})

for all ξ ≤ [[τ′]]ρ[ξ/MyType],o ∈ A^{ξ}, and i from 1 to n.

Case: i = 1. We can say, by the denotational rule for records, Proj , that

([[C′, E′ ⊢ e′ : τ′]]ρ[ξ/MyType, o/self ])(m_{1})
= [[C′, E′ ⊢ e′′_{1} : τ′_{1}]]ρ[ξ/MyType, o/self ]
= [[C′, E′ ⊢ e′_{1} : τ′_{1}]]ρ[ξ/MyType, o/self , s/super]
= f(m_{1}).

Case: i ≥ 2. By the definition of f above,

f(m_{i})= [[C, E ⊢ c : ClassType(MyType)τ]]ρ(ξ)(o)(m_{i})

= ([[C, E ⊢ class(self : MyType ≤_{meth} ObjectType(MyType)τ)e :

ClassType(MyType)τ]]ρ)(ξ)(o)(m_{i}) by induction

= ([[C^{+}, E′ ⊢ e : τ]]ρ[ξ/MyType, o/self ])(m_{i}) by Class

= ([[C′, E′ ⊢ e′ : τ′]]ρ[ξ/MyType, o/self ])(m_{i}) by Rec.

where C^{+} = C ∪ {MyType ≤_{meth} ObjectType(MyType)τ}.

Thus, the two functions are equal for all m_{i} in either domain. Since the functions were equal to the denotational meanings of the respective expressions, we can say that the two are equivalent.

The case for class extensions is similar.

6 Comparison with previous work

As indicated earlier, the work on TOOPLE grew out of work in [CHC90] and [Mit90] on the semantics of inheritance in typed object-oriented languages. We have also been greatly influenced by the work of Luca Cardelli.

The most interesting comparable work to ours is that of Cardelli and of Benjamin Pierce. In their papers, both alone and with collaborators (see [Car88a, CW85, Car88b, CL91, CM90, Car92] and [PT93, PT92, PH92]), both authors have been striving to find a core language which can be used to model all of the common features of object-oriented programming languages. Each uses extensions of F_{≤}, the bounded second-order lambda calculus. While we have preferred to use the F-bounded second-order lambda calculus (see [CCH^{+}89]) as a basis for the denotational semantics of our language, they have preferred a different variant which involves taking fixed points of higher order functions from types to types. As indicated by [Aba92], these extensions of F_{≤} are essentially identical.

A major difference between both Cardelli and Pierce and our work is that they adopt a mainly syntactic point of view of translating object-oriented features into extensions of the second-order lambda calculus. We have adopted a more semantic approach, originally giving the denotational semantics of TOOPLE in a model of the second-order lambda calculus. We have continued this approach here, treating our object-oriented programming language features as primitive and providing an operational semantics in terms of these constructs.

Pierce’s approach eliminates the need for fixed points at the type level in his language (though they are still required at the element level to model objects). The price to be paid for this is not being able to express classes with binary methods like eq which take parameters of type MyType, as in PointClass in section 2. While our denotational semantics for TOOPLE requires fixed points at both the term and type levels, the natural semantics provided here is significantly simpler.

Castagna, Ghelli, and Longo (see [CGL92]) have proposed an interesting new approach to providing the features of object-oriented programming languages. They propose replacing inheritance by a disciplined use of overloading of operations. When combined with subtyping, the resulting language has many interesting features, including a mechanism for dealing with multi-methods, methods whose execution depends on the types of several parameters rather than just the type of the receiver of the message, as in most objectoriented programming languages.

Each of these approaches to modeling object-oriented programming languages has its strengths and weaknesses, many of which will be apparent only with time and experience. It is already clear that each of these approaches represents significant progress toward the ultimate understanding of object-oriented programming languages.

7 Summary and further work on TOOPLE

In this paper we presented a natural semantics (a form of operational semantics) for the statically-typed, functional, object-oriented language, TOOPLE. The natural semantics has the advantage of being easier to understand than the denotational semantics, since the denotational semantics requires fixed points at both the element and type levels. The major results in the paper were proofs of a subject reduction theorem for the natural semantics, and a consistency theorem for the natural semantics relative to the denotational semantics.

The language presented in this conference paper does not include instance variables. The language with only methods is extremely limited in expressibility, but we decided that it was much easier to present this simpler language in the limited space available here. We urge the reader to see [Bru93a] for a full discussion of TOOPLE with instance variables. The natural semantics presented here can be extended easily to the full language, and the theorems and proofs carry over fairly directly to this more complex language.

The subject reduction theorem shows that the natural semantics preserves the type system for the language. Thus a well-typed term can never go “wrong”. In particular, it shows that a well-typed term will never result in a computation in which a message is sent to an object which cannot handle it. The earlier papers [Bru93b] and [Bru93a] included other results with respect to a denotational semantics which indicated that the language was type-safe.

The proofs of the subject reduction theorem and the type safety of the denotational semantics helped us discover and eliminate errors in the type-checking rules that might have remained had we not built the language on this theoretical base. It is our hope that this deeper understanding of object-oriented programming languages will provide the basis for a careful analysis of the pros and cons of each of their individual features. This should lead to the design of safe languages which are easy to reason about, and whose expressiveness is similar to that found in today’s popular object-oriented languages.

Since earlier papers presented the semantics of the language as a denotational semantics, we showed here that the natural semantics is consistent with those earlier semantics.

The paper, [BCD^{+}93], presents further results on TOOPLE. It shows that type checking TOOPLE is decidable and that every term of TOOPLE has a minimal type. The decidability of type checking was in some doubt since Pierce [Pie92] showed that type checking F_{≤} was undecidable and the denotational semantics of TOOPLE is expressed in an extension of F_{≤}.

R. van Gent at Williams College has built a TOOPLE type checker and interpreter which is based on the type-checking algorithm presented in [BCD^{+}93] and the natural semantics presented in this paper. More recently, Bruce and van Gent [vG93, BvG93] have designed an imperative language, TOIL, with a type system extending that of TOOPLE. Similar results about the safety and decidability of type-checking hold for TOIL. An interpreter has been written which is being used to further investigate the language. Work is currently proceeding on extending the type system of TOIL to include explicit polymorphism. We are also investigating the development of proof axioms and rules for reasoning about TOOPLE and TOIL programs.

While TOOPLE is missing many of the important features necessary to provide a truly useful language, we believe that TOOPLE can serve as the core of a statically-typed object-oriented language which combines type-safety with expressiveness approaching or even exceeding that of languages which fail to be strongly typed.

As this paper was going to press, we learned of the development of the language Strongtalk [BG93], which has adopted essentially the typing rules for TOOPLE (along with a few extensions) in order to type check a subset of Smalltalk. We look forward to learning of the efficacy of this typing system in large programming projects.

Acknowledgements

Thanks to the following for helpful comments on TOOPL and this entire project: Luca Cardelli, Giuseppe Longo, John Mitchell, Benjamin Pierce, the Harvard University Object-Oriented Languages Seminar (including Peter Wegner, Andrew Black, Allyn Dimock, and Robert Muller), and the other members of the Williams College TOOPL research group: Tom Murtagh and Robert van Gent. Special thanks go to Jon Riecke, who originally suggested that a structured operational semantics might be significantly simpler than the original denotational semantics, and introduced us to modern treatments of operational semantics.

References

[Aba92] M Abadi. Doing without F-bounded quantification. Message to Types electronic mail list, February, 1992.

[BCD^{+}93] K. Bruce, J. Crabtree, A. Dimock, R. Muller, T. Murtagh, and R. van Gent. Safe and decidable type checking in an object-oriented language. In Proc. ACM Symp. on Object-Oriented Programming: Systems, Languages, and Applications, pages 29–46, 1993.

[BG93] Gilad Bracha and David Griswold. Strongtalk: Typechecking Smalltalk in a production environment. In Proc. ACM Symp. on Object-Oriented Programming: Systems, Languages, and Applications, pages 215–230, 1993.

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

[Bru93a] K. Bruce. A paradigmatic object-oriented programming language: design, static typing and semantics. Technical Report CS-92-01, revised, Williams College, 1993. To appear in Journal of Functional Programming.

[Bru93b] K. Bruce. Safe type checking in a statically typed object-oriented programming language. In Proc. ACM Symp. on Principles of Programming Languages, pages 285–298, 1993.

[BvG93] Kim B. Bruce and Robert van Gent. TOIL: A new type-safe object-oriented imperative language. to appear, 1993.

[Car88a] L. Cardelli. A semantics of multiple inheritance. Information and Computation, 76:138–164, 1988. Special issue devoted to Symp. on Semantics of Data Types, Sophia-Antipolis (France), 1984.

[Car88b] L. Cardelli. Structural subtyping and the notion of powertype. In Proc 15th ACM Symp. Principles of Programming Languages, pages 70–79, 1988.

[Car92] Luca Cardelli. Extensible records in a pure calculus of subtyping. Technical Report 81, DEC Systems Research Center, 1992.

[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.

[CG92] P.L. Curien and G. Ghelli. Coherence of subsumption, minimum typing and type-checking in F_{≤}. Mathematical Structures in Computer Science, 2:55–91, 1992.

[CGL92] G. Castagna, G. Ghelli, and G. Longo. A calculus for overloaded functions with subtyping. In Proc. ACM Symp. Lisp and Functional Programming Languages, pages 182–192, 1992.

[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.

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

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

[Gun92] Carl A. Gunter. Semantics of Programming Languages: Structures and Techniques. MIT Press, 1992.

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

[NN92] Hanne Riis Nielson and Flemming Nielson. Semantics with applications: A formal introduction. John Wiley & Sons, 1992.

[PH92] Benjamin C. Pierce and Martin Hoffman. An abstract view of objects and subtyping (preliminary report). Technical Report ECS-LFCS-92-226, University of Edinburgh, 1992.

[Pie92] Benjamin C. Pierce. Bounded quantification is undecidable. In Proc 19th ACM Symp. Principles of Programming Languages, pages 305–315, 1992.

[PT92] Benjamin C. Pierce and David N. Turner. Simple type-theoretic foundations for object-oriented programming. Technical report, University of Edinburgh, 1992.

[PT93] Benjamin C. Pierce and David N. Turner. Object-oriented programming without recursive types. In Proc 20th ACM Symp. Principles of Programming Languages, pages 299–312, 1993.

[vG93] Robert van Gent. TOIL: An imperative type-safe object-oriented language. Williams College Senior Honors Thesis, 1993.

A Subtyping Rules for TOOPLE

SRefl

C ⊢ τ ≤ τ

SVar

C ∪ {t ≤ τ} ⊢ t ≤ τ

STrans

\frac{\begin{matrix}C ⊢ γ ≤ σ, \\ C ⊢ σ ≤ τ \end{matrix}}{C ⊢ γ ≤ τ}

SAbs

\frac{\begin{matrix}C ⊢ σ′ ≤ σ, \\ C ⊢ τ ≤ τ′ \end{matrix}}{C ⊢ σ → τ ≤ σ′ → τ′}

SRec

\frac{C ⊢ σ_{j} ≤ τ_{j}, ∀j : 1 ≤ j ≤ k ≤ n}{C ⊢ \{m_{1} : σ; …; m_{k} : σ_{k}; …; m_{n} : σ_{n}\} ≤ \{m_{1} : τ_{1}; …; m_{k} : τ_{k}\}}

SObj

\frac{C ∪ s ≤ t ⊢ τ[s/MyType] ≤ τ′[t/MyType]}{C ⊢ ObjectType(MyType)τ ≤ ObjectType(MyType)τ′}

IRefl

C ⊢ ObjectType(MyType)τ ≤_{meth} ObjectType(MyType)τ

IVar

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

ITrans

\frac{C ⊢ γ ≤_{meth} ObjectType(MyType)τ, C ⊢ τ ≤ τ′}{C ⊢ γ ≤_{meth} ObjectType(MyType)τ′}

B Minimum Typing Rules for TOOPLE

Definition B.1 The following are used in the minimum typing rules and axioms below.

1. (Fzrom [CG92]) We write C ⊢ t ≪ τ, if t is a type variable, and C ⊢ t ≤ τ is provable using only (SVar) and (STrans).

2. The type lub(τ, τ′) is the least upper bound of τ and τ′ according to the subtyping ordering. The least upper bound of two types exists as long as they have any upper bound. See [BCD^{+}93] for details.

MVar

C, E ⊢_{M} x : τ, if E(x) = τ

Mcond

\frac{\begin{matrix}C, E ⊢_{M} B : ρ, \\ C ⊢ ρ ≤ Bool, \\ C, E ⊢_{M} M : τ′, \\ C, E ⊢_{M} N : τ′′ \end{matrix}}{C, E ⊢_{M} if B then M else N : lub(τ′, τ′′)}

MAbs

\frac{C, E ∪ \{v : σ\} ⊢_{M} M : τ}{C, E ⊢_{M} fun(v : σ) M : σ → τ}

MAppl

\frac{\begin{matrix}C, E ⊢_{M} M : σ → τ, \\ C, E ⊢_{M} N : σ′, \\ C ⊢ σ′ ≤ σ \end{matrix}}{C, E ⊢_{M} M N : τ}

MAppl’

\frac{\begin{matrix}C, E ⊢_{M} M : t, \\ C, E ⊢_{M} N : σ′, \\ C ⊢ t ≪ σ → τ, \\ C ⊢ σ′ ≤ σ \end{matrix}}{C, E ⊢_{M} M N : τ}

MEq?

\frac{\begin{matrix}C, E ⊢_{M} M : τ, \\ C, E ⊢_{M} N : τ′, \\ C ⊢ τ ≤ Num, \\ C ⊢ τ′ ≤ Num \end{matrix}}{C, E ⊢_{M} M = N : Bool}

MRec

\frac{C, E ⊢_{M} e_{i} : τ_{i}, ∀i : 1 ≤ i ≤ n}{C, E ⊢_{M} \{m_{1} = e_{1}, …, m_{n} = e_{n}\} : \{m_{1} : τ_{1}; …; m_{n} : τ_{n}\}}

MProj

\frac{C, E ⊢_{M} e : \{m_{1} : τ_{1}; …; m_{n} : τ_{n}\}}{C, E ⊢_{M} e.m_{i} : τ_{i}, ∀i : 1 ≤ i ≤ n}

MProj’

\frac{\begin{matrix}C, E ⊢_{M} e : t, \\ C ⊢ t ≪ \{m_{1} : τ_{1}; …; m_{n} : τ_{n}\} \end{matrix}}{C, E ⊢_{M} e.m_{i} : τ_{i}, ∀i : 1 ≤ i ≤ n}

MClass

\frac{C ∪ \{MyType ≤_{meth} ObjectType(MyType)τ\}, E ∪ \{self : MyType\} ⊢_{M} e : τ′, C ∪ \{MyType ≤_{meth} ObjectType(MyType)τ\} ⊢ τ′ ≤ τ}{C, E ⊢_{M} class(self : MyType ≤_{meth} ObjectType(MyType)τ)e : ClassType(MyType)τ} MObj

\frac{C ∪ \{MyType ≤_{meth} ObjectType(MyType)τ\}, E ∪ \{self : MyType\}\} ⊢_{M} e : τ′, C ∪ \{MyType ≤_{meth} ObjectType(MyType)τ\} ⊢ τ′ ≤ τ}{C, E ⊢_{M} obj (self : MyType ≤_{meth} ObjectType(MyType)τ)e : ObjectType(MyType)τ} MNew

\frac{C, E ⊢_{M} c : ClassType(MyType)τ}{C, E ⊢_{M} new c : ObjectType(MyType)τ}

MMsg

\frac{C, E ⊢_{M} o : ObjectType(MyType)\{m_{1} : τ_{1}; …; m_{n} : τ_{n}\}}{C, E ⊢_{M} o ⇐ m_{i} : τ_{i}[ObjectType(MyType)\{m_{1} : τ_{1}; …; m_{n} : τ_{n}\}/MyType]}

MMsg’

\frac{C, E ⊢_{M} o : t, (t ≤_{meth} ObjectType(MyType)\{m_{1} : τ_{1}; …; m_{n} : τ_{n}\}) ∈ C}{C, E ⊢_{M} o ⇐ m_{i} : τ_{i}[t/MyType]}

MUpdate \frac{C, E ⊢_{M} c : ClassType(MyType)τ, C ⊢ τ′_{1} ≤ τ_{1}, C ∪ \{MyType ≤_{meth} ObjectType(MyType)τ′\}, E ∪ \{self : MyType, super : τ\} ⊢_{M} e′_{1} : τ′′_{1}, C ∪ \{MyType ≤_{meth} ObjectType(MyType)τ′\} ⊢ τ′′_{1} ≤ τ′_{1}}{C, E ⊢_{M} update c by (self : MyType ≤_{meth} ObjectType(MyType)τ′, super)\{m_{1} = e′_{1}\} : ClassType(MyType)τ′}

where τ = {m_{1} : τ_{1}; …; m_{n} : τ_{n}} and τ′ = {m_{1} : τ′_{1}; …; m_{n} : τ_{n}}. MExtend

\frac{C, E ⊢_{M} c : ClassType(MyType)τ, C ∪ \{MyType ≤_{meth} ObjectType(MyType)τ′\}, E ∪ \{self : MyType, super : τ\} ⊢_{M} e_{n+1} : τ′_{n+1}, C ∪ \{MyType ≤_{meth} ObjectType(MyType)τ′\} ⊢ τ′_{n+1} ≤ τ_{n+1}}{C, E ⊢_{M} extend c with (self : MyType ≤_{meth} ObjectType(MyType)τ′, super) \{m_{n+1} = e_{n+1}\} : ClassType(MyType)τ′} where τ = {m_{1} : τ_{1}; …; m_{n} : τ_{n}} and τ′ = {m_{1} : τ_{1}; …; m_{n+1} : τ_{n+1}}.

C Natural Semantics for TOOPLE

RAbs

C, E ⊢ fun(x : σ) M : σ → τ ↓ fun(x : σ) M

RConst

C, E ⊢ true : Bool ↓ true,
C, E ⊢ false : Bool ↓ false,

C, E ⊢ n : Num ↓ n, if n is a constant of type Num C, E ⊢ self : MyType ↓ self RRecord

C, E ⊢ {r_{1} = e_{1}, …, r_{n} = e_{n}} : {r_{1} : τ_{1}; …; r_{n} : τ_{n}} ↓ {r_{1} = e_{1}, …, r_{n} = e_{n}}

RClass

C, E ⊢ class(self : MyType ≤_{meth} ObjectType(MyType)τ)e : ClassType(MyType)τ ↓ class(self : MyType ≤_{meth} ObjectType(MyType)τ)e

RObj

C, E ⊢ obj (self : MyType ≤_{meth} ObjectType(MyType)τ)e : ObjectType(MyType)τ ↓ obj (self : MyType ≤_{meth} ObjectType(MyType)τ)e

REq

\frac{\begin{matrix}C, E ⊢ e_{1} : Num ↓ v, \\ C, E ⊢ e_{2} : Num ↓ v \end{matrix}}{C, E ⊢ e_{1} = e_{2} : Bool ↓ true}

RNeq

\frac{\begin{matrix}C, E ⊢ e_{1} : Num ↓ v_{1}, \\ C, E ⊢ e_{2} : Num ↓ v_{2}, \\ v_{1} ≢ v_{2} \end{matrix}}{C, E ⊢ e_{1} = e_{2} : Bool ↓ false}

RTrue

\frac{C, E ⊢ B : Bool ↓ true, C, E ⊢ e_{1} : τ ↓ v, C, E ⊢ e_{2} : τ}{C, E ⊢ if B then e_{1} else e_{2} : τ ↓ v}

RFalse

\frac{C, E ⊢ B : Bool ↓ false, C, E ⊢ e_{2} : τ ↓ v, C, E ⊢ e_{1} : τ}{C, E ⊢ if B then e_{1} else e_{2} : τ ↓ v}

RAppl

\frac{\begin{matrix}C, E ⊢ e : σ → τ ↓ fun(x : σ) M, \\ C, E ⊢ M[e′/x] : τ ↓ v \end{matrix}}{C, E ⊢ e e′ : τ ↓ v}

RProj

\frac{\begin{matrix}C, E ⊢ e : τ ↓ \{r_{1} = e_{1}, …, r_{i} = e_{i}, …, r_{n} = e_{n}\}, \\ C, E ⊢ e_{i} : τ_{i} ↓ v \end{matrix}}{C, E ⊢ e.r_{i} : τ_{i} ↓ v}

RNew

\frac{C, E ⊢ c : ClassType(MyType)τ ↓ class(self : MyType ≤_{meth} ObjectType(MyType)τ)e}{C, E ⊢ new c : ObjectType(MyType)τ ↓ obj (self : MyType ≤_{meth} ObjectType(MyType)τ)e}

RMsg

\frac{C, E ⊢ o : γ ↓ obj (self : MyType ≤_{meth} γ′)e, C, E ⊢ (e[obj (self : MyType ≤_{meth} ObjectType(MyType)τ)e/self , γ′/MyType] : \{m_{1} : τ_{1}; …; m_{n} : τ_{n}\})[γ′/MyType] ↓ \{m_{1} = e_{1}, …, m_{n} = e_{n}\} C, E ⊢ e_{i} : τ_{i}[γ′/MyType] ↓ v}{C, E ⊢ o ⇐ m_{i} : τ_{i}[γ/MyType] ↓ v}

where 1 ≤ i ≤ n, and γ′ = ObjectType(MyType){m_{1} : τ_{1}; …; m_{n} : τ_{n}} RUpdate \frac{C, E ⊢ c : ClassType(MyType)τ ↓ class(self : MyType ≤_{meth} ObjectType(MyType)τ)e}{C, E ⊢ update c by (self : MyType ≤_{meth} ObjectType(MyType)τ′, super)\{m_{1} = e′_{1}\} : ClassType(MyType)τ′ ↓ class(self : MyType ≤_{meth} ObjectType(MyType)τ′)\{m_{1} = e′′_{1}, m_{2} = e.m_{2}, …, m_{n} = e.m_{n}\}}

where e′′_{1} = e′_{1}[e/super], τ = {m_{1} : τ_{1}; …; m_{n} : τ_{n}}, and τ′ = {m_{1} : τ′_{1}; …; m_{n} : τ_{n}}. RExtend \frac{C, E ⊢ c : ClassType(MyType)τ ↓ class(self : MyType ≤_{meth} ObjectType(MyType)τ)e}{C, E ⊢ update c by (self : MyType ≤_{meth} ObjectType(MyType)τ′, super)\{m_{n+1} = e_{n+1}\} : ClassType(MyType)τ′ ↓ class(self : MyType ≤_{meth} ObjectType(MyType)τ′) \{m_{1} = e.m_{1}, …, m_{n} = e.m_{n}, m_{n+1} = e′_{n+1}\}}

where e′_{n+1} = e_{n+1}[e/super], τ = {m_{1} : τ_{1}; …; m_{n} : τ_{n}}, and τ′ = {m_{1} : τ_{1}; …; m_{n+1} : τ_{n+1}}.

D Denotational Semantics for TOOPL

ObjectType [[ObjectType(MyType)τ]]ρ = F IX(λξ.[[τ]]ρ[ξMyType] ClassType

[[ClassType(MyType)τ]]ρ = ∏_{ξ≤_{A}[[τ]]ρ[ξ/MyType]}(ξ → [[τ]]ρ[ξ/MyType])

Var

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

Cond

[[C, E ⊢ if B then e_{1} else e_{2} : τ]]ρ = \{ \begin{matrix}[[C, E ⊢ e_{1} : τ]]ρ, if [[C, E ⊢ B : Bool]]ρ = true \\ [[C, E ⊢ e_{2} : τ]]ρ, if [[C, E ⊢ B : Bool]]ρ = false \\ ⊥, otherwise \end{matrix}

Abs

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

Appl

[[C, E ⊢ e e′ : τ]]ρ = ([[C, E ⊢ e : σ → τ]]ρ)([[C, E ⊢ e′ : σ]]ρ)

Eq?

[[C, E ⊢ e_{1} = e_{2} : Bool]]ρ = \{ \begin{matrix}true, if [[C, E ⊢ e_{1} : τ]]ρ = [[C, E ⊢ e_{2} : τ]]ρ \\ false, otherwise \end{matrix}

Rec

[[C, E ⊢ {r_{1} = e_{1}, …, r_{n} = e_{n}} : τ]]ρ = f,

where

\begin{aligned}dom(f) & = & \{r_{1}, …, r_{n}\} \\ ∀i : 1 ≤ i ≤ n, f(r_{i}) & = & [[C, E ⊢ e_{i} : τ_{i}]]ρ \end{aligned}

Proj

[[C, E ⊢ e.r_{i} : τ_{i}]]ρ = ([[C, E ⊢ e : τ]]ρ)(r_{i})

Class [[C, E ⊢ class(self : MyType ≤_{meth} ObjectType(MyType)τ)e : ClassType(MyType)τ]]ρ =

λξ ≤ [[τ]]ρ[ξ/MyType].λo ∈ A^{ξ}.[[C ∪ {MyType ≤_{meth} ObjectType(MyType)τ},

E ∪ {self : MyType} ⊢ e : τ]]ρ[ξ/MyType, o/self ]

New

[[C, E ⊢ new c : ObjectType(MyType)τ]]ρ = FIX (([[C, E ⊢ c : ClassType(MyType)τ]]ρ)([[ObjectType(MyType)τ]]ρ))

Obj

[[C, E ⊢ obj (self : MyType ≤_{meth} ObjectType(MyType)τ)e : ObjectType(MyType)τ]]ρ =

FIX (([[C, E ⊢ class(self : MyType ≤_{meth} ObjectType(MyType)τ)e : ClassType(MyType)τ]]ρ)([[ObjectType(MyType)τ]]ρ))

Msg

[[C, E ⊢ o ⇐ m_{i} : τ_{i}[γ/MyType]]]ρ
= (convert[[[{m_{i} : τ_{i}}]]ρ[[[γ]]ρ/MyType]][[[γ]]ρ][[C, E ⊢ o : γ]]ρ) (m_{i})

Update

[[C, E ⊢ update c by (self : MyType ≤_{meth} ObjectType(MyType)τ, super){m_{1} = e′_{1}} : ClassType(MyType)τ′]]ρ = λξ ≤ [[τ′]]ρ[ξ/MyType].λo ∈ A^{ξ}.f,

where

dom(f) = {m_{1}, …, m_{n}},
f(m_{1}) = [[C ∪ {MyType ≤_{meth} ObjectType(MyType)τ′},
E ∪ {self : MyType} ⊢ e′_{1} : τ′_{1}]]ρ[ξ/MyType, o/self , s/super],
f(m_{j}) = s(m_{j}), ∀j : 2 ≤ j ≤ n,
s  = ([[C, E ⊢ c : ClassType(MyType){m_{1} : τ_{1}; …; m_{n} : tau_{n}}]]ρ)(ξ)(o).

Extend

[[C, E ⊢ extend c with (self : MyType ≤_{meth} ObjectType(MyType)τ, super) {m_{n+1} = e_{n+1}} : ClassType(MyType)τ′]]ρ = λξ ≤ [[τ′]]ρ[ξ/MyType].λo ∈ A^{ξ}.f,

where

dom(f) = {m_{1}, …, m_{n+1}},
f(m_{n+1}) = [[C ∪ {MyType ≤_{meth} ObjectType(MyType)τ′},
E ∪ {self : MyType} ⊢ e_{n+1} : τ_{n+1}]]ρ[ξ/MyType, o/self , s/super],
f(m_{j}) = s(m_{j}), ∀j : 1 ≤ j ≤ n,
s  = ([[C, E ⊢ c : ClassType(MyType){m_{1} : τ_{1}; …; m_{n} : tau_{n}}]]ρ)(ξ)(o).