TOIL: A new Type-safe Object-oriented Imperative Language ^{∗}^{†}

Kim B. Bruce  Robert van Gent^{‡}

Williams College October 13, 1993

1 Introduction

In [Bru93b], the first author introduced a statically-typed, functional, object-oriented language, TOOPLE. The goal behind the design of TOOPLE was to create a type-safe object-oriented programming language, whose design would be firmly based on the formal semantics for object-oriented programming languages which have been developed over the last several years.

Work to date on TOOPLE (see also [Bru93a, BCK93, BCD^{+}93]), has resulted in a denotational and operational semantics for the language, and a series of results have been proven which include the relatively consistency of the operational and denotational semantics, a subject-reduction theorem, the type safety of the type-checking rules, and the decidability of the type-checking problem. TOOPLE was designed as a functional language because it was believed to be simpler to approach these problems for a functional rather than an imperative language.

At the end of the presentations of the papers, [Bru93b] and [PT93], in POPL ’93, David MacQueen challenged the authors to extend their work to imperative languages, since functional languages only provided an approximation to common object-oriented languages. This paper is a response to that challenge. (Pierce has also extended his language to include imperative features in [Pie93]).

An imperative object-oriented language has several advantages over functional languages. Most importantly, an imperative language is typically significantly more efficient than a functional language, especially when large data structures (e.g., arrays) are updated. Moreover, more programmers are comfortable with imperative than functional languages. Finally, almost all contemporary object-oriented programming languages are imperative, leading many programmers to be suspicious of any functional language which purports to be object-oriented.

The design of TOOPLE built on the work of many researchers, especially the work of Cardelli, Cook et al., and Mitchell. See, for example, [CHC90, Mit90, Car88, BM92]. It was designed to provide a model design for a safe static type system of a very expressive object-oriented language.

∗Both authors were partially supported by NSF grant CCR-9121778.

†Corresponding author: Kim B. Bruce, Department of Computer Science, Williams College, Williamstown, MA 01267. kim@cs.williams.edu,(413) 597-2273, FAX: (413) 597-4116.

‡Many of the results in this paper are included in the second author’s senior honors thesis [vG93].

However there are clearly extra problems that have to be solved for imperative languages that do not arise in functional languages.

In this paper, we present the language TOIL (for “Typed Object-oriented Imperative Language”), an extension of TOOPLE in which instance variables represent locations, and updates are executed in place, rather than by a copy semantics. TOIL (like TOOPLE) contains all of the important features of class-based object-oriented languages, including classes, objects, methods, hidden instance variables, subclasses, subtypes, dynamic method invocation, and references to self (with its public type, MyType) and super, the record of methods of the superclass.

As with TOOPLE, the subclass hierarchy only depends on class implementations, while the subtype hierarchy is based only on the public interface or type of object and other expressions. In particular, there may be several classes with different implementations which generate objects of the same type. As before, subclasses need not generate subtypes.

Interestingly, while the type system of TOIL is provably safe, it is also significantly more flexible than such typed object-oriented languages as C++ ([Str86]), Object Pascal ([Tes85]), and Modula-3 ([CDG^{+}88]). Moreover, TOIL programs are designed to be type checked modularly. That is, if a class type checks correctly, inherited methods in subclasses do not need to be typed checked again. This provides better support for the provision of reusable libraries than languages which require access to the bodies of methods in superclasses in order to repeatedly type check the code of inherited methods.

As noted earlier, instance variables are implemented as references (locations in most implementations). In order to provide better support for the use of subtypes, objects are also implemented as references. One happy consequence of this decision is that recursive data types can be defined directly in TOIL, eliminating the need for explicit pointers in implementing complex data types.

Methods can be either functions or procedures. As with Eiffel ([Mey92]), parameters are passed only by constant value. As a result, the programmer may not assign new values to formal parameters. However, the programmer may send messages to object parameters, which may result in changes to the instance variables of actual parameters. These design decisions provide for a very flexible use of subtypes. In particular, if a formal parameter, p, of a procedure is declared with type τ, and σ ≤ τ, then an actual parameter, a, of type σ may be passed for p. Languages like C++ and Object Pascal do not generally support this subtyping because of a different set of design decisions.

In our research on TOIL, we have developed type-checking rules, denotational and natural (operational) semantics, and have proved several important theorems about the type-checking rules and semantics. We also have a prototype implementation of an interpreter for TOIL, which is based on its natural semantics. Because of space limitations, we cannot describe all of these aspects of the language. Instead we concentrate here on the type-checking rules and natural semantics, proving a subject-reduction theorem in order to demonstrate the safety of the type system.^{1} One consequence of the subject-reduction theorem is that the computation of a well-typed term will never result in sending a message to an object that it does not understand.

In Section 2 of this paper we present an informal introduction to TOIL. In the following section we discuss the difficulties in type checking object-oriented programming languages. In Section 4 we provide the formal syntax and type-checking rules for TOIL. In Section 5 we then introduce a natural (operational) semantics and prove the subject-reduction theorem for TOIL. Finally, in Section 7 we compare TOIL with other statically-typed imperative object-oriented programming languages, provide a summary of the paper, and discuss work in progress on extensions. We also compare our results with similar work reported in [ESTZ93].

1In [Bru93b] we concentrated on the denotational semantics. The approach taken here is more similar to that of [BCK93].

2 An informal introduction to TOIL

We presume that the reader is familiar with the basic notions of object-oriented languages, including object, class, subclass, method, and instance variable. Recall that one type is a subtype of another if an element of the first type can be used in any context expecting an element of the second.

A TOIL program consists of a sequence of type abbreviations, constant definitions, and variable declarations, followed by a sequence of executable statements. A sample TOIL program which defines and uses a stack is given in Appendix A.

Class definitions (e.g., for stack class) provide initial values for instance variables of the class and provide the definitions of methods. The types of classes^{2} (written in the form ClassType(σ, τ)) describe the types of both instance variables (σ) and methods (τ), while the types of objects (written in the form ObjectType τ) only mention the types of methods. This corresponds to the fact that instance variables are not accessible outside of the methods of an object. The types of procedures are written in the form proc(τ_{1}, …, τ_{k}), while those of functions are written as func(τ_{1}, …, τ_{k}): σ.

Method bodies in classes can refer to the receiving object using the term self. The type of the receiving object is denoted MyType. In TOOPLE, the user was required to choose a name for self and MyType. This was useful since class definitions could be nested, and hence required the selection of distinct names. Since TOIL includes explicit provisions for defining and naming classes, we have omitted the requirement of providing these names. Instead, self and MyType will be considered reserved words.

An instance variable, x, of an object can be accessed inside one of its methods as self .x. Instance variables may be either evaluated or assigned to. A message, m, can be sent to an object, o, by writing o ⇐ m. For this term to be well-typed, the type of o must contain a method with the same name, m. It is also possible for an object to send a message to itself (though the user must first “close” self in order to hide the instance variables – see section 4 for details).

Because of the use of subtyping, the type of an expression at run-time may be a subtype of the statically determined type of the expression. When a message is sent to an object, the method body invoked depends on the class which created the object rather than on the statically-determined type of the object. This dynamic method binding is the same as that used in languages like Smalltalk ([GR83]) and Eiffel, and is that used with “virtual” methods in C++.

The types of methods and instance variables can involve the term MyType, allowing the implicit recursive definition of object types. For instance, the type node class type in the Appendix has an instance variable of type MyType, while methods get next and attach right respectively return a value of type MyType and take a parameter of type MyType. When a message is sent to an object, all occurrences of MyType in the method body and its type are replaced by the type of the object. Thus if n is an object of type node type from Appendix A, the type of n ⇐ get next is func(): node type, while the type of n ⇐ attach right is proc(node type).

Because the instance variable, next, in node class type has type MyType, each object generated from a class with that type also contains a (hidden) instance variable of type node type. This instance variable is only accessible to the methods of the class. We will see below that using MyType in the types of the instance variables and methods will also provide us with greater flexibility in defining subclasses.

2Recall from TOOPLE that classes are values, not types.

Objects are treated as references. Thus assignment of objects represents sharing rather than copying. A nil reference is denoted by the constant nil, which can be treated as an element of any object type. In particular, it may be assigned to a variable of type MyType.

Parameter passing is done using call-by-constant value. It is illegal to assign to a formal parameter in a procedure or function. Of course, it is legal to send a message to such a parameter, requesting it to perform an action (which may result in a change to that object’s instance variables). Because of this, and the fact that an object is represented as a reference, parameter passing can actually have behavior similar to that of call-by-name.

New objects are created by applying new to a class. The instance variables of the new object are initialized to the values specified in the class. In the sample program in Appendix A, generate node class is a function from numbers to node class type. A new node with value 3 is created and stored in variable x by executing

x: = new (generate node class(3)).

Subclasses of classes can be defined either by adding new methods and instance variables or changing existing methods and (initial values of) instance variables. Instance variables and methods of the original class not mentioned in the subclass definition are inherited.

At the end of Appendix A, we define a subclass of nodes which also have associated colors.^{3} This is accomplished by adding a new color instance variable and a method to retrieve that value. All of the instance variables and methods of generate node class(n) are inherited by generate color node class(n, c). Note that because the types are specified using MyType, we retain fine control over the types of methods. Thus, if n is of type node type and cn is of type color node type, the value returned from n ⇐ getnext() has type node type, while the value returned from cn ⇐ getnext() has type color node type.

3 Issues in type checking object-oriented programming languages

There are many places in the design of object-oriented programming languages where the designer can fall into traps which compromise the safety of the type system. In this section we illustrate a few which have to do with the imperative features of TOIL. Several other problems were discussed in [Bru93b]. For the most part, we do not repeat those discussions here. The problems discussed in this section have to do with subclasses which fail to generate subtypes (an issue that was discussed in the earlier paper), difficulties with reference parameters, and implementation difficulties in preserving subtyping.

We begin by illustrating the problems which can arise by conflating subclasses with subtypes. In the previous section, we defined a class to generate objects of type color node type via inheritance from one that generated objects of type node type. Nevertheless, color node type is not a subtype of node type. Thus objects of type color node type may not be used in places where an object of type node type is expected. The following program fragment (which uses the program segments defined in the Appendix) illustrates why this is not allowed.

3Technically, we define a new function which returns a subclass of the class returned by evaluating generate node class(n).

const add_it = procedure(node:node_type; n:num)
                var
                  new_node:node_type
                begin
                  new_node := new(generate_node_class(n));
                  node <= attach_right(new_node)
                end:proc(node_type,num);
...
var color_node:color_node_type;
    nu_color_node:color_node_type;
begin
  color_node = new(generate_color_node_class(2,red));
  add_it(color_node);
  nu_color_node := get_next(color_node);
  nu_color := nu_color_node <= get_color
end.

If color node type were a subtype of node type then the procedure call add it(color node) would be legal. However, this program results in a run-time error, since add it puts a non-color node in the next field of color node. Hence get next(color node) actually returns a node of type node type which has no color field.

As we shall see later, the reason that color node type fails to be a subtype of node type is the occurrence of a parameter of type MyType in the method attach right of node type. Thus, while the class which generates objects of type color node type is obtained as a subclass of the one generating objects of type node type, they do not represent subtypes.

A problem can arise with subtyping if the language supports call-by-reference parameters. For instance, a procedure might take a formal parameter of type T and assign it a new object of that type. If an actual parameter, u which is of type U ≤ T is passed in to the procedure, it will be assigned a value of type T. If objects of type U have a method, m, which does not exist in T, then, after the procedure is executed, u will not be able to respond to message m. (This problem is related to the fact that reference types do not have subtypes, as discussed in the next section.) Because call-by-reference parameters do not interact well with subtyping, we only support call-by-value parameters in TOIL.

In support of subtyping, one would normally wish to allow assignment of subtype expressions to supertype variables. That is, if T ≤ U, e is an expression of type T, and x is a variable of type U, one would like to allow the assignment x: = e. However there is the practical problem that a value of type T may take up considerably more storage space than a value of type U (for instance, T may have several more instance variables). In order to make such an assignment feasible we need to have an upper bound on the amount of space required for the variable x. Our solution to this problem is to require objects to be implemented as references. This is the same solution adopted by Eiffel, Clu, and Modula-2 for objects or elements of opaque types (i.e., those whose implementation is not known at compile time).^{4} Thus object variables are always allocated the same amount of space (no matter what the object type), enough space to hold a reference to a descriptor which itself specifies the location of instance variables and the values of methods.

4We would also need to require records to be implemented as references if they were supported by the language.

Here they are simply provided as degenerate objects.

4 A formal definition of TOIL syntax

In this section we present the formal definitions of types and terms and provide type-checking rules for TOIL. The language is presented here with an abstract syntax, which differs in inessential ways from that used in the earlier examples.

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 ∪ {COMMAND, UNIT, PROGRAM, ⊥} then t is a type expression.

2. If τ is a type expression, and τ ∉ {COMMAND, UNIT, PROGRAM, ⊥} then ref τ is a type expression.

3. If σ_{1} … σ_{n} and τ are type expressions, then so is func(σ_{1}, …, σ_{n}): τ.

4. If m_{1}, …, m_{n} ∈ L and τ_{1}, …, τ_{n} are type expressions, then {m_{1}: τ_{1}; …; m_{n}: τ_{n}} is a (record) type expression.

5. Let σ and τ be record type expressions. Then VisObjType(σ, τ), ClassType(σ, τ), and ObjectType τ are type expressions.

The type constant COMMAND is the type of an imperative command expression. UNIT is a type whose only value is written (), and is used when typing parameterless functions. Reference types are simply the types of variables, so X: ref τ implies that X is a variable containing data of type τ. Record types are included above, even though they may not be used independently in TOIL. Nevertheless, they are useful in the construction of classes and objects since collections of methods and instance variables can easily be modelled as records.

The type ⊥ is a subtype of all object types. Its main importance is that it contains the element nil, used in our sample programs. Sending a message to nil produces an error result.

The type ClassType(σ, τ) is the type of classes in which the record of initial values for instance variables has type σ and record of methods has type τ. ObjectType τ and VisObjType(σ, τ) represent the types of objects generated from a class with type ClassType(σ, τ). The former represents the type as seen from outside the object (in which instance variables are hidden), while the latter represents the type as seen from the inside (where the instance variables are visible).

Like TOOPLE, TOIL uses the relation ≤_{Meth} as well as the subtyping relation, ≤, in order to type-check terms. The relation ≤_{Meth} on object types corresponds to a pointwise ordering on the method types. It is defined so that if ObjectType τ′ is the type of objects generated from a subclass, c′, of a class, c, which itself generates objects of type ObjectType τ, then ObjectType τ′≤_{Meth}ObjectType τ. We saw in the node example in Section 3, that it need not follow that ObjectType τ′ ≤ ObjectType τ.

The rules for ≤, ≤_{Meth}, and type-checking are given with respect to a set, C, of simple type constraints.

Definition 4.2 Relations of the form t ≤ τ and t ≤_{Meth} τ, where t is a type variable and τ is a type expression, are said to be simple type constraints. 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 ≤ τ is a simple type constraint such that the type variable t does not appear in C or τ, then C ∪ {t ≤ τ} is a type constraint system.

3. If C is a type constraint system, τ is of the form ObjectType σ, and t ≤_{Meth} τ is a type constraint such that the type variable t does not appear free in C or τ, then C ∪ {t ≤_{Meth} τ} is a type constraint system.

The axioms and rules for ≤ and ≤_{Meth} are similar to those for TOOPLE and can be found in Appendix B. Notice that neither class nor reference types have subtypes. The example in Section 3 showing the problems with the mix of call-by-reference and subtypes provides the justification for not allowing reference types to have subtypes.

In the examples presented earlier, we used a concrete syntax which is understood by our interpreter. Here we use an abstract syntax which is somewhat more primitive. In particular the key words var and method separating instance variable and method definitions are dropped in favor of a pair of record expressions, and val must be used to obtain the value of a variable. Procedures are not directly supported, but are modelled by functions which return the unique value, command, of type COMMAND.

Variables have types of the form ref τ. The value stored in a variable, x, is denoted by the expression, val x. These types and expressions are not necessary in the concrete syntax since they are inferred by the parser. In particular the implemented TOIL does not support keywords ref and val.

For simplicity, in this conference paper we omit the definition of declarations. (For more details see [vG93].) The expressions and commands of the language are given as follows:

Definition 4.3 The pre-expressions and pre-commands of TOIL are given by the following contextfree grammar:

E  : : = x | c | val x |function(v_{1}: σ_{1}; …; v_{n}: σ_{n}) Block |
E(E_{1}, …, E_{n}) | {m_{1} = E_{1}, …, m_{n} = E_{n}} | E.m_{i} | class(E_{1}: σ, E_{2}: τ) |
new E | E ⇐ m_{i} | E.v_{i} | update E by({v_{1} = E_{1}}, {m_{1} = E′_{1}}) |
update E with({v_{k+1} = E_{k+1}}, {m_{n+1} = E′_{n+1}})
S  : : = x: = E | if E then E_{1} else E_{2} | while E do S | S; S′
Block : : = begin S return M: σ; end

The intended meaning of these terms should be clear from our previous discussion. The typechecking axioms and rules for TOIL are given in terms of a type constraint system, C, as defined earlier, and a variable type assignment, E, as defined below:

Definition 4.4 A variable type assignment E is a finite set of associations between variables and type expressions of the form x: τ, where each x is unique in E. If the relation x: τ ∈ E, then we write E(x) = τ.

The collection of terms of TOIL with respect to C, E is the set of pre-terms which can be assigned types with respect to the type assignment axioms and rules in Appendix C. The rules for the commands and non-object-oriented expressions should be relatively clear, while those for the object-oriented expressions may require some extra explanation.

The type-assignment rule, Class, involves several new features. As suggested earlier, the reserved word self may be used inside the methods of a class to refer to the object which is executing the method. Because instance variables are not visible outside of an object’s methods, the object actually has two types, an internal type, SelfType, in which the instance variables are visible, and an external type, MyType, which hides the instance variables. The reserved word self represents an internal view of the object and has type SelfType. The reserved word close: SelfType → MyType is used to convert a term (usually self) from the internal type to the external type of the object executing the method. Since SelfType is the internal type of the object, it cannot appear in the type of any instance variable or method of the object.

Recall that the class merely contains initial values for the instance variables, while the objects contain locations at which those initial values are stored. The function RecToMem is used to convert a record type into one in which the type of each field is a reference to the type in the original. Thus

RecT oMem({v_{1}: σ_{1}; …; v_{n}: σ_{n}}) = {v_{1}: ref σ_{1}; …; v_{n}: ref σ_{n}}.

Finally, let us recall from TOOPLE that values of instance variables and method bodies should be type checked so that they are guaranteed to be type-correct when inherited in a subclass. Thus we must type-check these terms only under relatively weak assumptions on the possible values of SelfType and MyType.

With this background we can now understand the type-assignment rule, Class, as indicating that to type-check a class term one must ensure that the records of initial values of instance variables and of methods have the desired types, when type-checking is done only assuming that SelfType ≤ (RecT oMem(σ), τ) and MyType≤_{Meth}ObjectType τ, since any subclass of the class being type-checked will satisfy these constraints. Notice that since RecT oMem(σ) is a record of reference types, subtypes may not change the type of any instance variable, but may only add new instance variables.

The type-assignment rules for other object-oriented terms are similar to Class or are like the corresponding rules for TOOPLE.

5 An operational semantics for TOIL

In this section we provide a natural (operational) semantics for TOIL. This semantics is similar to that given in [BCK93] for TOOPLE. We also prove a subject reduction theorem, which indicates that our type-assignment rules are safe.

There are a number of semantic decisions involving binding time that must be made carefully in order to provide a useful language. For instance, in order for new to create new objects each time it is invoked, it is important that locations for instance variables are not allocated when their initial values are declared in a class. Instead, they can only be allocated when a new object is created.

Suppose the initial values of instance variables or method bodies depend on global variables. When should they be evaluated? In TOOPLE, we waited until a new object was created, but, because it was a functional language, it made no real difference. In TOIL, we employ eager evaluation in computing the initial values of instance variables specified in classes, while method bodies (since they are protected by function or procedure abstraction) do not evaluate variables until they are actually invoked by a message.

Another complication is that methods may refer to self and super. Yet the values of these reserved words are not known at the time a method body is provided in a class definition. Thus the instantiation of the corresponding values must be postponed until the new object is created.

We introduce two new terms, obj(a, e) and close_{(σ,τ)}, in order to write the natural semantics of the language. The term obj(a, e) represents an object whose instance variables are in the locations specified in a and whose methods are given in e. The type of obj(a, e) is of the form VisObjType(σ, τ) if the type of a is RecT oMem(σ) and the type of e is τ. The term close_{(σ,τ)} designates a specialization of the term close, with type VisObjType(σ, τ) → ObjectType τ. It takes an object whose instance variables are visible to one whose instance variables are hidden. The typing rules for these terms (and for closures, introduced below) may be found at the end of Appendix C.

The semantic rules reduce a term with associated environment and current store to a pair consisting of an irreducible value and an updated store. The environment is a (finite) mapping of names to irreducible values, while the store is a (finite) mapping of locations to irreducible values.

The irreducible values in TOIL are numbers, Booleans, locations, functions (represented as closures, which are pairs of terms and environments), records with irreducible components, classes whose record of initial values of instance variables and record of methods are irreducible, and object values whose record of instance variables and record of methods are irreducible. For technical reasons we allow environments to map the keywords self and close to themselves. The environment paired with a term in a closure must include interpretations of all free variables of the term.

We use a store, s, to represent the state of the machine. The store is modelled as a finite function mapping locations to irreducible values. For simplicity we presume that each location is associated with a fixed type. We write Loc_{τ} for the collection of locations holding values of type τ. Thus we will interpret the type ref τ as an abbreviation for Loc_{τ}. We note that it would be possible instead to have a single collection of locations and simply keep lists of the intended types of allocated locations, but the approach used here seemed more straightforward. We will also understand ObjectType τ as an abbreviation for ⋃_{σ} Loc_{VisObjType(σ,τ)}, where σ ranges over record types. If we think of terms of the form obj(a, e) as terms representing objects whose instance variables are visible, objects with hidden instance variables are interpreted as references to those with visible instance variables.

The store is infinitely extensible – the function GetNewLoc takes a store, s, and a type, τ, and returns an unused location l ∈ Loc_{τ}, along with a new store, s′. The new store is the same as s, except that l is mapped to a location holding a (default) value of type τ. The notation s[l ↦ V] is used to denote the updating of the store. The store s is updated so that the location l now contains the value V , but is otherwise unchanged. Note that for all l ∈ Loc_{τ}, s(l) has type τ.

The natural semantics rules for TOIL can be found in Appendix D. Note that functions reduce to closures. The most complex rules are for new c and close_{(σ,τ)} e.

In new c, the expression c is first reduced to an irreducible class value of the form class(IV, Methods). New space is allocated for each of the instance variables of the object, and a new location is allocated to hold the object the object. The value returned is that new location, into which is stored a term of the form obj(newIV, newMethods) where newIV is defined to be the record of locations for the instance variables. NewMethods is obtained from Methods by replacing all free occurrences of self by obj(newIV, Methods), close by the specialized close_{(σ,τ)}, and the types SelfType and MyType by the types VisObjType(σ, τ) and ObjectType τ.

The operation close_{(σ,τ)}e is interpreted similarly, except that the locations for instance variables need not be allocated since they were already allocated when the obj term was evaluated.

Note that since new c and close_{(}σ, τ)e are the only ways of constructing terms of type ObjectType τ, no irreducible values of these types will have free occurrences of self or close. As a result, the natural semantics of sending a message to an object is trivial. Just look up the value stored in the location corresponding to the object and extract the appropriate method value. ^{5} The object nil responds to all messages with the value error of the appropriate type. Extracting the value of instance variables from (visible) objects also involves simply extracting the location from the record of instance variables.

6 Subject Reduction Theorem

In this section we prove the subject reduction theorem for TOIL, and use it to prove the type safety of the language.

In the following, it will be useful to have the following abbreviations: For any C, E, define

1. E^{MET H} = E ∪ {self : SelfType, close: (func(SelfType): MyType)},

2. C^{IV} = C ∪ {MyType≤_{Meth}ObjectType τ}, and

3. C^{MET H} = C^{IV} ∪ {SelfType ≤ VisObjType(σ, τ)}.

4. E_{0} = \{ \begin{matrix}∅^{MET H}, & if self : SelfType ∈ E \\ ∅, & otherwise. \end{matrix}

We say that an environment, ρ, is consistent with C, E iff whenever (x: τ) ∈ E then C, E_{0} ⊢ ρ(x): τ. A state s is consistent with C iff for all l ∈ Loc_{τ}, C, ∅ ⊢ s(l): τ. Note that in the definitions of both consistent environments and consistent states, the minimum types of ρ(x) and s(l) may be subtypes of the given type τ. It follows from the definition of consistent state that irreducible values stored in locations may not include either free variables or the terms self or close.

We now have enough definitions to state our result.

Theorem 6.1 (Subject Reduction) If C, E ⊢ M: σ, ρ is consistent with C, E, s is consistent with C, and (M, ρ, s) ↓ (V, s′), then s′ is consistent with C, and C, E_{0} ⊢ V: σ. Moreover, if σ is of the form ObjectType τ, then V ∈ Loc_{VisObjType(σ,τ)} for some σ, and s′(V) = obj(a, e) for some a, e such that e contains no free occurrences of self, close, SelfType, or MyType.

The proof of subject reduction is given in Appendix E.

This result shows that our type assignment rules are sound in that all subterms which arise in the computation of a term must be typable.

We now wish to prove something a bit stronger - that computations of well-typed terms never get stuck. In particular, a computation of a well-typed term will never result in sending a message, m, to an object which does not have m as a method. We say a computation from (e, ρ, s) becomes stuck if there is a term in the computation tree of the form (e′, ρ′, s′) ↓ (V′, s′′) which must be satisfied, yet there is no semantic rule applicable to (e′, ρ′, s′).

5Interestingly, the semantics of message sending is more straightforward here than in TOOPLE.

In order to prove this we must make a few changes to our natural semantics, and ensure that we have appropriate computation rules for all constants. We must add computation rules for error values to ensure that computations in which errors arise will terminate with an error value. We accomplish this by simply assuming that extra natural semantics rules are added for each term construction which indicate that if any of the subterms needed in the computation evaluate to error_{σ} for some σ, then the term evaluates to error_{τ} for appropriate τ. We do not bother to write down this extended set of rules, but simply term the system of old and new rules the extended natural semantics of TOIL and use the notation ↓^{+} for its computation. Except for terms of the form error_{τ} and close_{(σ,τ)}, we presume that all other constants of the language have a base type (e.g., Bool), and the only constants of type Bool are true, false, and error_{Bool}. It would also be possible, for instance, to add new computation rules for all constants of functional types (e.g., arithmetic operators on numbers), but we satisfy ourselves with this simplified version here.

Theorem 6.2 Let e be a term with no free variables. Suppose that C, ∅ ⊢ e: τ, ρ is consistent with C, ∅, and s is consistent with C. Then under the assumptions stated above, either (e, ρ, s) ↓^{+} (V, s′), for V an irreducible value, or the computation diverges.

Proof. It is sufficient to show that for every well-typed term e, there is an applicable axiom or rule. The proof is a simple induction on the proof of the minimum typing of the term (expressed as a proof by contradiction based on the ”shortest” counter-example). Because we have already proved the subject reduction theorem above, we can be assured that the results of the computations which are hypotheses will be of the correct type.

Of course, we cannot assure that those computations will actually terminate. Simple examples of non-terminating computations include while statements with true as the Boolean guard, and expressions involving sending a message to an object whose corresponding method body sends the same message to close(self ).

The key to the proof is that with the exception of error and close terms, there is only one kind of irreducible value of each non-base type. We illustrate the proof with a few cases. As stated above, the proof is by contradiction. Suppose e is a well-typed term with the shortest proof of typing for which there exist ρ and s such that the computation gets stuck.

Function Application Let e = M N and suppose C, E ⊢ M N: τ. Thus C, E ⊢ M: σ → τ, and C, E ⊢ N: σ′ for C ⊢ σ′ ≤ σ. Since the typing proofs for M and N are shorter than that of M N, the computations on (M, ρ, s) and (N, ρ, s) do not get stuck. Since that of (M N, ρ, s) does get stuck, the computations for M and N must terminate (otherwise that of M N diverges rather than getting stuck). Suppose (M, ρ, s) ↓^{+} (V, s′) and (N, ρ, s) ↓^{+} (V′, s′′). By the subject reduction theorem, C, ∅ ⊢ V: σ → τ. By assumption the only irreducible terms of those types are error and close constants, and closures. But there are computation rules for each of these cases. Thus the computation on M N cannot get stuck.

Message sending Suppose e = o ⇐ m_{i}, and suppose C, E ⊢ o ⇐ m_{i}: τ_{i}[ObjectType τ/MyType] follows from C, E ⊢ o: ObjectType τ, for τ = {m_{1}: τ_{1}, …, m_{n}: τ_{n}}. (Note that by the corresponding case of the subject reduction theorem, the type of o must be of the form ObjectType τ.)

Suppose (o, ρ, s) ↓^{+} (V, s′). By the subject reduction theorem, C, E ⊢ V: ObjectType τ. But the only irreducible values of this type are an error constant and locations (since ObjectType τ = ⋃_{σ} Loc_{VisObjType(σ,τ)}). There is a rule for the case in which V is an error term. Moreover if V ∈ Loc_{VisObjType(σ,τ)}, then by the consistency of s′, C, ∅ ⊢ s′(l): VisObjType(σ, τ). The only irreducible values of type VisObjType(σ, τ) are an error constant (which triggers one of the added “error” rules), and terms of the form obj(a, e), and there is a rule handling this case. Thus the computation does not get stuck.

The other cases are similar.

7 Summary and comparison with other work

An important difference between TOIL and other typed object-oriented languages such as C++, Object Pascal, and Eiffel are that the subtype and subclass hierarchies are no longer identified. If they are identified then one is either left with an unsafe language (either by design, or with conventions that require many type casts – essentially by-passing the type system), a language with limited expressibility, or a language which requires either extra run-time or link-time checks in order to preserve type safety.

TOIL’s type system allows much greater flexibility than C++, Object Pascal, and Modula-3, none of which support a special name for the type of self or allow the modification of types of methods in subclasses. The lack of these features greatly limits the expressibility of these languages, particularly in defining subclasses.

In TOIL the types of instance variables and methods may be given in terms of MyType. Thus, when a subclass is defined (such as our color node type example), the types of the instance variables and methods automatically change to reflect that of the new object type.

On the other hand, TOIL does not allow the degree of flexibility found in Eiffel, a language which does provide a version of MyType, written as “like Current”. Eiffel’s type checking system considers color node type to be a subtype of node type in the example in section 3. This results from the identification in Eiffel of classes with types and the rejection of the (correct) subtyping rule for functions given here. Eiffel 3.0 copes with the resulting difficulties by introducing a link-time global analysis of a program to identify those places where type-related errors could arise.

We feel the TOIL approach is more straightforward. Moreover we gain the flexibility of having multiple classes generating objects of the same type.

In summary, the features of TOIL which provide extra expressibility are

1. A name for the (external) type of self, MyType (similar to Eiffel’s “like Current”);

2. The ability to replace the types of methods by subtypes when redefining methods;

3. The separation of the definitions of type and subtype from implementation details. This allows:

• the definition of multiple classes generating objects of the same type,

• the definition of subclasses which do not generate subtypes.

Another important feature of TOIL is that it may be type checked modularly. That is, in order to type check a subclass, we only need to know the type of the superclass and the new or modified instance variable values and methods. It is not necessary to repeatedly type check inherited features. Moreover, by the subject reduction theorem, we are guaranteed that these inherited features can only be used in a type-safe way.

Though not included here, there is also a denotational semantics for TOIL, along with a proof of the soundness of type-checking with respect to the denotational semantics (similar to that in [Bru93b] and [Bru93a]). (See [vG93] for further information.) The second author has also written a prototype interpreter for TOIL which is based on the natural semantics provided here.

The paper [ESTZ93] presents similar results for an object-oriented language, LOOP, with state. However there are considerable differences between TOIL and LOOP. LOOP identifies the inheritance and subtype hierarchies, and has no type expressions corresponding to our use of MyType and SelfType, thus limiting its expressiveness. However, LOOP does allow the programmer to use self in the initialization of instance variables, adding expressiveness (and corresponding complexity of semantics) in a different direction than that taken with TOIL. The approach taken in [ESTZ93] also differs from that taken here since LOOP is first translated into a simple imperative language, SOOP. A proof of type-soundness is given for SOOP, which then carries over via translation to LOOP.

Pierce, [Pie93], has also extended his encoding of object-oriented languages to include references. As he points out, the change was more or less straightforward, with the only complication being that the shift from call-by-name to call-by-value semantics limited the availability of fixedpoint operators to function types. Nevertheless, a few simple changes led to a system supporting references. Like [ESTZ93], Pierce’s strategy is to encode object-oriented languages in terms of a lower-level language, in this case an extension of the bounded second-order lambda calculus. This encoding is similar to the denotational semantics of TOIL. It is somewhat simpler than the semantics of TOIL, requiring one fewer fixed-point operator in creating types of objects. However, as with the corresponding functional language, there is a corresponding loss of expressibility with regard to expressing binary methods like the attach right method in node class type in Appendix A.

Current work on TOIL is proceeding with examining extensions to support bounded polymorphism (what Eiffel calls “bounded genericity”). As long as the type-assignment rules are relatively conservative, we expect this extension to be relatively straightforward and easy to implement.

We hope to see TOIL as the core of a new generation of object-oriented programming languages which offer both increased expressibility and a safe type system. We recently learned of the development of the language Strongtalk [BG93], which has adopted essentially the typing rules for TOIL (along with a few extensions) in order to type check a subset of Smalltalk. We hope to see other language designers adopting similar systems.

References

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

[BCK93] K. Bruce, J. Crabtree, and G. Kanapathy. An operational semantics for TOOPLE: A statically-typed object-oriented programming language. To appear in Proceedings of MFPS IX, 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.

[BM92] Kim B. Bruce and J. Mitchell. PER models of subtyping, recursive types and higherorder polymorphism. In Proc. ACM Symp. on Principles of Programming Languages, pages 316–327, 1992.

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

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

[CDG^{+}88] L. Cardelli, J. Donahue, L. Galssman, M. Jordan, B. Kalsow, and G. Nelson. Modula-3 report. Technical Report SRC-31, DEC systems Research Center, 1988.

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

[ESTZ93] J. Eifrig, S. Smith, V. Trifonov, and A. Zwarico. A simple interpretation of OOP in a language with state. Technical Report YALEU/DCS/RR-968, Yale University, 1993. Proceedings of the Workshop on State in Programming Languages.

[GR83] A. Goldberg and D. Robson. Smalltalk–80: The language and its implementation. Addison Wesley, 1983.

[Mey92] B. Meyer. Eiffel: the language. Prentice-Hall, 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.

[Pie93] Benjamin C. Pierce. Mutable objects. Technical report, University of Edinburgh, 1993.

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

[Str86] B. Stroustrop. The C^{++} Programming Language. Addison-Wesley, 1986.

[Tes85] L. Tesler. Object Pascal report. Technical Report 1, Apple Computer, 1985.

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

A Sample TOIL program

program stacker;
abbrev  node_class_type = ClassType({value:num;next:MyType},
    {get_value:func():num;
     get_next:func():MyType;
     attach_right:proc(MyType)});
node_type = ObjectType{get_value:func():num;
get_next:func():MyType;
attach_right:proc(MyType)};
stack_class_type = ClassType({top:node_type},
     {push:proc(num);
      pop:func():num;
      is_empty:func():bool});
stack_type = ObjectType{push:proc(num);
pop:func():num;
is_empty:func():bool}
const   generate_node_class = function(n:num):node_class_type
begin
return
class
var
value = n : num;
next = nil : MyType
methods
get_value = function():num
begin
return self.value;
end : func():num;
get_next = function():MyType
begin
return self.next;
end : func():MyType;
attach_right =  procedure(n:MyType)
begin
self.next:=n;
end : proc(MyType)
end;
end : func(num):node_class_type;

stack_class =
class
var
top=nil : node_type
methods
push =  procedure(n:num)
var
temp:node_type
begin
temp:=self.top;
self.top := new (generate_node_class(n));
self.top <= attach_right(temp);
end : proc(num);
pop =   function():num
var
answer : num
begin
answer:=self.top <= get_value();
self.top := self.top <= get_next();
return answer;
end : func():num;
is_empty =  function():bool
 begin
    return (self.top =OBJ= nil);
 end : func():bool
end : stack_class_type
var   test_stack: stack_type;
val: num
begin
test_stack := new(stack_class);
test_stack <= push(2);
test_stack <= push(3);
while (not (test_stack <= is_empty())) do
val:=test_stack <= pop();
printNum(val);
end;
end.

A subclass of node class, formed by adding a color to each node, can easily be defined. We assume that a type ColorType has been defined elsewhere.

abbrev  color_node_class_type = ClassType
          ({value:num; color: ColorType; next:MyType},
           {get_value:func():num;

get_color:func():ColorType;
get_next:func():MyType;
attach_right:proc(MyType)});
color_node_type = ObjectType{get_value:func():num;
get_color:func():ColorType;
get_next:func():MyType;
attach_right:proc(MyType)};
const   generate_color_node_class = function(n:num; c:color):color_node_class_type
begin
return
extend generate_node_class(n) by
var
color = c : ColorType
methods
get_color = function():ColorType
begin
return self.color
end: func():ColorType
end;
end : func(num):color_node_class_type;

B Subtyping and ≤_{Meth} axioms and rules

Axioms and rules for ≤

Refl(≤) C ⊢ τ ≤ τ,

V ar(≤) C ∪ {t ≤ τ} ⊢ t ≤ τ,

T rans(≤)  \frac{C ⊢ γ ≤ σ, C ⊢ σ ≤ τ}{C ⊢ γ ≤ τ} ,

F unc(≤)  \frac{C ⊢ σ′_{i} ≤ σ_{i} for 1 ≤ i ≤ n, C ⊢ τ ≤ τ′}{C ⊢ F unc(σ_{1}, …, σ_{n}) : τ ≤ F unc(σ′_{1}, …, σ′_{n}) : τ′} ,

Rec(≤)  \frac{C ⊢ σ_{j} ≤ τ_{j}, for 1 ≤ j ≤ k ≤ n}{C ⊢ \{m_{1}: σ_{1}; …; m_{k}: σ_{k}; …; m_{n}: σ_{n}\} ≤ \{m_{1}: τ_{1}; …; m_{k}: τ_{k}\}} ,

P air(≤)  \frac{C ⊢ RecT oMem(σ) ≤ RecT oMem(σ′), C ⊢ τ ≤ τ′}{C ⊢ VisObjType(σ, τ) ≤ VisObjType(σ′, τ′)} ,
Obj(≤),  \frac{C ∪ \{s ≤ t\} ⊢ τ[s/MyType] ≤ τ′[t/MyType]}{C ⊢ ObjectType τ ≤ ObjectType τ′} .

where neither s nor t may occur free in C, τ, or τ′, Bot(≤) C ⊢⊥ ≤ ObjectType τ,

Axioms and Rules for ≤_{Meth}

V ar(≤_{Meth}) C ∪ {t≤_{Meth}τ} ⊢ t≤_{Meth}τ,

Refl(≤_{Meth}) C ⊢ ObjectType τ≤_{Meth}ObjectType τ,

T rans(≤_{Meth})  \frac{C ⊢ γ≤_{Meth}ObjectType τ, C ⊢ τ ≤ τ′}{C ⊢ γ≤_{Meth}ObjectType τ′} ,

C Type Assignment Axioms and Rules

Type Assignment Rules (Blocks)

Block  \frac{C, E ⊢ S: COMMAND, C, E ⊢ M: σ}{C, E ⊢ begin S return M; end : σ}

Type Assignment Rules (Commands)

Assn  \frac{C, E ⊢ X: ref τ, C, E ⊢ M: τ}{C, E ⊢ X: = M: COMMAND}
Cond  \frac{C, E ⊢ B: Bool, C, E ⊢ S: COMMAND, C, E ⊢ T: COMMAND}{C, E ⊢ if B then S else T end : COMMAND}
W hile  \frac{C, E ⊢ B: Bool, C, E ⊢ S: COMMAND}{C, E ⊢ while B do S end : COMMAND}
StmtList  \frac{C, E ⊢ S: COMMAND, C, E ⊢ T: COMMAND}{C, E ⊢ S; T: COMMAND}

Type Assignment Rules (Expressions)

Nil C, E ⊢ nil: ⊥

V ar C, E ⊢ X: τ, if E(X) = τ

Ref  \frac{C, E ⊢ X: ref τ}{C, E ⊢ val X: τ}

F unction \frac{C, E ∪ \{v_{1}: σ_{1}, …, v_{n}: σ_{n}\} ⊢ Block: τ}{C, E ⊢ function (v_{1}: σ_{1}; …; v_{n}: σ_{n}) Block: (func(σ_{1}, …, σ_{n}): τ)}

F uncAppl \frac{C, E ⊢ M: func(σ_{1}, …, σ_{n}): τ, C, E ⊢ N_{i}: σ_{i} for all 1 ≤ i ≤ n}{C, E ⊢ M(N_{1}, …, N_{n}): τ}

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

P roj  \frac{C, E ⊢ e: \{m_{1}: τ_{1}; …; m_{n}: τ_{n}\}}{C, E ⊢ e.m_{i}: τ_{i} for all 1 ≤ i ≤ n}

Class  \frac{C^{IV} , E ⊢ e_{1}: σ, C^{MET H}, E^{MET H} ⊢ e_{2}: τ}{C, E ⊢ class(e_{1}, e_{2}): ClassType(σ, τ)}

where C^{IV} = C ∪ {MyType≤_{Meth}ObjectType τ}, C^{MET H} = C^{IV} ∪ {SelfType ≤ VisObjType(σ, τ)}, and E^{MET H} = E ∪ {self : SelfType, close: (func(SelfType): MyType)}.

Object  \frac{C, E ⊢ c: ClassType(σ, τ)}{C, E ⊢ new c: ObjectType τ}

Message  \frac{C ⊢ γ≤_{Meth}ObjectType \{m: τ\}, C, E ⊢ o: γ}{C, E ⊢ o ⇐ m: τ[γ/MyType]}

InstV ar  \frac{C ⊢ γ ≤ VisObjType(\{v_{1}: σ_{1}; …; v_{n}: σ_{n}\}, τ), C, E ⊢ o: γ}{C, E ⊢ o.v_{i}: ref σ_{i}}

Update \frac{C, E ⊢ c: ClassType(\{v_{1}: σ_{1}; …; v_{m}: σ_{m}\}, \{m_{1}: τ_{1}; …; m_{n}: τ_{n}\}), C ⊢ τ′_{1} ≤ τ_{1}, C^{IV} , E ⊢ a′_{1}: σ_{1}, C^{MET H}, E^{MET H} ⊢ e′_{1}: τ′_{1}}{C, E ⊢ update c by (\{v_{1} = a′_{1}: σ_{1}\}, \{m_{1} = e′_{1}: τ′_{1}\}): ClassType(\{v_{1}: σ_{1}; …; v_{m}: σ_{m}\}, \{m_{1}: τ′_{1}; m_{2}: τ_{2}; …; m_{n}: τ_{n}\})}

where C^{IV} = C ∪ {MyType≤_{Meth}ObjectType {m_{1}: τ′_{1}; m_{2}: τ_{2}; …; m_{n}: τ_{n}}}

C^{MET H} = C^{IV} ∪

{SelfType ≤ VisObjType({v_{1}: σ_{1}; …; v_{m}: σ_{m}}, {m_{1}: τ′_{1}; m_{2}: τ_{2}; …; m_{n}: τ_{n}})}

E^{MET H} = E ∪ {self : SelfType, close: func(SelfType): MyType,

super: SelfType → {m_{1}: τ_{1}; …; m_{n}: τ_{n}}}

Extend \frac{C, E ⊢ c: ClassType(\{v_{1}: σ_{1}; …; v_{m}: σ_{m}\}, \{m_{1}: τ_{1}; …; m_{n}: τ_{n}\}), C^{IV} , E ⊢ a_{m+1}: σ_{m+1}, C^{MET H}, E^{MET H} ⊢ e_{n+1}: τ_{n+1}}{C, E ⊢ extend c with (\{v_{m+1} = a_{m+1}: σ_{m+1}\}, \{m_{n+1} = e_{n+1}: τ_{n+1}\}): ClassType(\{v_{1}: σ_{1}; …; v_{m+1}: σ_{m+1}\}\{m_{1}: τ_{1}; …; m_{n+1}: τ_{n+1}\})}

where C^{IV} = C ∪ {MyType≤_{Meth}ObjectType {m_{1}: τ_{1}; …; m_{n+1}: τ_{n+1}}},

C^{MET H} = C^{IV} ∪

{SelfType ≤ VisObjType({v_{1}: σ_{1}; …; v_{m+1}: σ_{m+1}}, {m_{1}: τ_{1}; …; m_{n+1}: τ_{n+1}})}
E^{MET H} = E ∪ {self : SelfType, close: func(SelfType): MyType,

super: SelfType → {m_{1}: τ_{1}; …; m_{n}: τ_{n}}}

Neither MyType nor SelfType may occur free in C, E in the rules for class, extend, and update.

Subsump  \frac{C ⊢ σ ≤ τ, C, E ⊢ e: σ}{C, E ⊢ e: τ}

Type Assignment Rules for Extra Terms in Natural Semantics

Close C, E ⊢ close_{(σ,τ)}: VisObjType(σ, τ) → ObjectType τ

Obj  \frac{C, E ⊢ (a: RecT oMem(σ))[ObjectType τ/MyType] C, E ∪ \{self : VisObjType(σ, τ)\} ⊢ e′: τ′}{C, E ⊢ obj(a, e): VisObjType(σ, τ)}

where e′ = e[close_{(σ,τ)}/close, ObjectType τ/MyType, VisObjType(σ, τ)/SelfType]

τ′ = τ[ObjectType τ/MyType]. Let ρ be an environment. Define ρ_{C}^{T} to be a syntactic type environment such that ρ^{T} (x) = τ

iff C, {self : SelfType, close: SelfType → MyType} ⊢ ρ(x): τ. Note that if ρ is consistent with C, E, then C, E ⊢ M: τ implies that C, ρ_{C}^{T} ⊢ M: τ.

Closure  \frac{C, ρ_{C}^{T} ⊢ f: τ}{C, E_{0} ⊢ ⟨f, ρ⟩: τ}

D The natural semantics of TOIL

Blocks

\frac{(S, ρ, s) ↓ (Command, s′), (R, ρ, s′) ↓ (V, s′′)}{(begin S return R; end, ρ, s) ↓ (V, s′′)} ,

Commands

\frac{(X, ρ, s) ↓ (Loc, s′), (M, ρ, s′) ↓ (V, s′′)}{(X: = M, ρ, s) ↓ (Command, s′′[Loc ↦ V])} ,
\frac{(B, ρ, s) ↓ (true, s′), (M, ρ, s′) ↓ (Command, s′′)}{(if B then M else N end, ρ, s) ↓ (Command, s′′)} ,
\frac{(B, ρ, s) ↓ (false, s′), (N, ρ, s′) ↓ (Command, s′′)}{(if B then M else N end, ρ, s) ↓ (Command, s′′)} ,

\frac{(B, ρ, s) ↓ (true, s′), (S, ρ, s′) ↓ (Command, s′′), (while B do S end, ρ, s′′) ↓ (Command, s′′′)}{(while B do S end, ρ, s) ↓ (Command, s′′′)} ,
\frac{(B, ρ, s) ↓ (false, s′)}{(while B do S end, ρ, s) ↓ (Command, s′)} ,

\frac{(C_{1}, ρ, s) ↓ (Command, s′), (C_{2}, ρ, s′) ↓ (Command, s′′)}{(C_{1}; C_{2}, ρ, s) ↓ (Command, s′′)}

Expressions

(c, ρ, s) ↓ (c, s), where c is a constant

(x, ρ, s) ↓ (ρ(x), s), where x is a variable

\frac{(x, ρ, s) ↓ (Loc, s′), s′(Loc) = V}{(val x, ρ, s) ↓ (V, s′)} ,

(function(v_{1}: σ_{1}, …, v_{n}: σ_{n})B, ρ, s) ↓ (⟨function(v_{1}, …, v_{n})B, ρ⟩, s),

\frac{\begin{matrix}(M, ρ, s^{0}) ↓ (⟨function(v_{1}: σ_{1}, …, v_{n}: σ_{n})B, ρ_{f}⟩, s^{1}), (N_{i}, ρ, s^{i}) ↓ (V_{i}, s^{i+1}), \\ (B, ρ_{f}[V_{i}/v_{i}], s^{n+1}) ↓ (V, s^{n+2}) \end{matrix}}{(M(N_{1}, …, N_{n}), ρ, s^{0}) ↓ (V, s^{n+2})} ,

\frac{(e_{i}, ρ, s^{i}) ↓ (V_{i}, s^{i+1}), 1 ≤ i ≤ n}{(\{m_{1} = e_{1}: τ_{1}, …, m_{n} = e_{n}: τ_{n}\}, ρ, s^{1}) ↓ (\{m_{1} = V_{1}: τ_{1}, …, m_{n} = V_{n}: τ_{n}\}, s^{n+1})} ,

\frac{(e, ρ, s) ↓ (\{m_{1} = V_{1}: τ_{1}, …, m_{n} = V_{n}: τ_{n}\}, s′)}{(e.m_{i}, ρ, s) ↓ (V_{i}, s′)} ,

\frac{(a, ρ, s) ↓ (V_{a}, s′), (e, ρ[self /self , close/close], s′) ↓ (V_{e}, s′′)}{(class(a, e), ρ, s) ↓ (class(V_{a}, V_{e}), s′′)} ,

\frac{(a, ρ, s) ↓ (V_{a}, s′), (e, ρ[self /self , close/close], s′) ↓ (V_{e}, s′′)}{(obj(a, e), ρ, s) ↓ (obj(V_{a}, V_{e}), s′′)} ,

\frac{(c, ρ, s) ↓ (class(\{iv_{1} = V_{1}: σ_{1}, …, iv_{n} = V_{n}: σ_{n}\}, Methods), s^{0}), (newLoc_{i}, s^{i}) = (GetNewLoc s^{i−1} σ_{i}), 1 ≤ i ≤ n, (newLoc_{n+1}, s^{n+1}) = GetNewLoc s^{n} VisObjType(σ, τ)}{\begin{matrix}(new c, ρ, s) ↓ (newLoc_{n+1}, s^{i}[newLoc_{1} ↦ V_{1}, …, newLoc_{n} ↦ V_{n}, \\ newLoc_{n+1} ↦ obj(newIV, newMethods)]) \end{matrix}} ,

where newIV = {iv_{1} = newLoc_{1}: ref σ_{1}, …, iv_{n} = newLoc_{n}: ref σ_{n}}, o′ = obj(newIV, Methods), newMethods = Methods[o′/self, close_{(σ,τ)}/close,

VisObjType(σ, τ)/SelfType, ObjectType τ/MyType]

\frac{(e, ρ, s) ↓ (o′, s′), (newLoc, s′′) = (GetNewLoc s′VisObjType(σ, τ))}{(close_{(σ,τ)} e, ρ, s) ↓ (newLoc, s′′[newLoc ↦ obj(a, newMethods)])} ,

where o′ = obj(a, Methods),

newMethods = Methods[o′/self, close_{(σ,τ)}/close, VisObjType(σ, τ)/SelfType, ObjectType τ/MyType]

\frac{(o, ρ, s) ↓ (Loc, s′), s′(Loc) = obj(a, \{m_{1} = V_{1}: τ_{1}, …, m_{n} = V_{n}: τ_{n}\})}{(o ⇐ m_{i}, ρ, s) ↓ (V_{i}, s′)} ,

\frac{(e, ρ, s) ↓ (nil, s′)}{(e ⇐ m_{i}, ρ, s) ↓ (error, s′)} ,

\frac{(o, ρ, s) ↓ (obj(\{iv_{1} = V_{1}: σ_{1}, …, iv_{n} = V_{n}: σ_{n}\}, e), s′)}{(o.iv_{i}, ρ, s) ↓ (V_{i}, s′)} ,

\frac{(P, ρ, s) ↓ (class(\{iv_{1} = V_{1}: σ_{1}, …, iv_{upd} = V_{old}: σ_{upd}, …, iv_{n} = V_{n}: σ_{n}\}, e), s′), (u, ρ, s′) ↓ (V_{new}, s′′)}{\begin{matrix}(update P by (\{iv_{upd} = u: σ_{upd}\}, \{\}), ρ, s) ↓ \\ (class(\{iv_{1} = V_{1}: σ_{1}, …, iv_{upd} = V_{new}: σ_{upd}, …, iv_{n} = V_{n}: σ_{n}\}, e), s′′) \end{matrix}} ,

\frac{(P, ρ, s) ↓ (class(a, \{m_{1} = V_{1}: τ_{1}, …, m_{upd} = V_{old}: τ_{upd}, …, m_{n} = V_{n}: τ_{n}\}), s′), (u, ρ′, s′) ↓ (V_{new}, s′′)}{\begin{matrix}(update P by (\{\}, \{m_{upd} = u: τ′_{upd}\}), ρ, s) ↓ \\ (class(a, \{m_{1} = V_{1}: τ_{1}, …, m_{upd} = V_{new}: τ′_{upd}, …, m_{n} = V_{n}: τ_{n}\}), s′′) \end{matrix}} ,

where ρ′ = ρ[self /self , close/close, (function(self : SelfType).{m_{1} = V_{1}: τ_{1}, …, m_{upd} = V_{old}: τ_{upd}, …, m_{n} = V_{n}: τ_{1}})/super]

\frac{(P, ρ, s) ↓ (class(\{iv_{1} = V_{1}: σ_{1}, …, iv_{n} = V_{n}: σ_{n}\}, e), s′), (u, ρ, s′) ↓ (V_{n+1}, s′′)}{\begin{matrix}(extend p with (\{iv_{n+1} = u: σ_{n+1}\}, \{\}), ρ, s) ↓ \\ (class(\{iv_{1} = V_{1}: σ_{1}, …, iv_{n} = V_{n}: σ_{n}, iv_{n+1} = V_{n+1}: σ_{n+1}\}, e), s′′) \end{matrix}} ,

\frac{(P, ρ, s) ↓ (class(a, \{m_{1} = V_{1}: τ_{1}, …, m_{n} = V_{n}: τ_{n}\}), s′), (u, ρ′, s′) ↓ (V_{n+1}, s′′)}{\begin{matrix}(extend p with (\{\}, \{m_{n+1} = u: τ_{n+1}\}), ρ, s) ↓ \\ (class(a, \{m_{1} = V_{1}: τ_{1}, …, m_{n} = V_{n}: τ_{n}, m_{n+1} = V_{n+1}: τ_{n+1}\}), s′′) \end{matrix}} ,

where ρ′ = ρ[self /self , close/close, (function(self: SelfType).{m_{1} = V_{1}: τ_{1}, …, m_{n} = V_{n}: τ_{n}})/super]

E The proof of Subject Reduction

Before beginning the proof, we note that by a simple induction on proofs, it can be shown that C^{IV} , E ⊢ a: σ implies that C, E[ObjectType τ/MyType] ⊢ (a: σ)[ObjectType τ/MyType] and C^{MET H}, E^{MET H} ⊢ e: τ implies that

C, E[ObjectType τ/MyType, VisObjType(σ, τ)/SelfType] ∪ {self : VisObjType(σ, τ)} ⊢ e′: τ′

for e′ = e[close_{(σ,τ)}/close, ObjectType τ/MyType, VisObjType(σ, τ)/SelfType]

and τ′ = τ[ObjectType τ/MyType].

Theorem E.1 (Subject Reduction) If C, E ⊢ M: σ, ρ is consistent with C, E, s is consistent with C, and (M, ρ, s) ↓ (V, s′), then s′ is consistent with C, and C, E_{0} ⊢ V: σ. Moreover, if σ is of the form ObjectType τ, then V ∈ Loc_{VisObjType(σ,τ)} for some σ, and s′(V) = obj(a, e) for some a, e such that e contains no free occurrences of self, close, SelfType, or MyType.

Proof. The proof is by induction on the length of the computation. Any time typing of terms are given, they correspond to a minimum type for the term.

Commands (i) Suppose (X: = M, ρ, s) ↓ (Command, s′′[l ↦ V]) because (X, ρ, s) ↓ (l, s′) and (M, ρ, s′) ↓ (V, s′′). Therefore by induction, both s′ and s′′ are consistent with C.

Suppose also that C, E ⊢ X: ref τ and C, E ⊢ M: τ. By induction, C, E ⊢ V: τ and l ∈ Loc^{τ}. Therefore s′′[l ↦ V]) is also consistent.

(ii) Suppose (while B do S end, ρ, s) ↓ (Command, s′) because (B, ρ, s) ↓ (false, s′). By induction, s′ is consistent with C.

Suppose, on the other hand, that (while B do S end, ρ, s) ↓ (Command, s′′′) because (B, ρ, s) ↓ (true, s′), (S, ρ, s′) ↓ (Command, s′′), and (while B do S end, ρ, s′′) ↓ (Command, s′′′). By induction (on the length of the computation), s′, s′′, and s′′′ are all consistent.

The arguments for if … then … else … and sequencing are similarly easy.

Blocks Suppose (begin S return R; end, ρ, s) ↓ (V, s′′) because (S, ρ, s) ↓ (Command, s′) and (R, ρ, s′) ↓ (V, s′′). Suppose also that C, E ⊢ begin S return R; end: τ follows from C, E ⊢ S: COMMAND and C, E ⊢ R: τ. By induction, s′ and s′′ are consistent with C and C, E_{0} ⊢ V: τ.

Expressions (i) Suppose c is a constant such that C, E ⊢ c: σ. Then (c, ρ, s) ↓ (c, s), clearly satisfying the Theorem.

(ii) Suppose x is a variable such that E(x) = σ. Then C, E ⊢ x: σ and (x, ρ, s) ↓ (ρ(x), s). Since ρ is consistent with C, E, it follows that C, E_{0} ⊢ ρ(x): τ.

(iii) Suppose C, E ⊢ val x: σ. Therefore, C, E ⊢ x: ref σ. Suppose also that (x, ρ, s) ↓ (l, s′) where s′(l) = V. By induction, C, E_{0} ⊢ l: ref σ. (Recall ref σ = Loc_{σ}.) Since by induction s′ is consistent with C, it follows that C, E_{0} ⊢ V: σ, as desired.

(iv) Suppose C, E ⊢ function(v_{1}: σ_{1}, …, v_{n}: σ_{n})B: (func(σ_{1}, …, σ_{n}): τ). Recall that

(function(v_{1}: σ_{1}, …, v_{n}: σ_{n})B, ρ, s) ↓ (⟨function(v_{1}, …, v_{n})B, ρ⟩, s).

Then by the type-checking rules for closures and the consistency of ρ with C, E,

C, E_{0} ⊢ ⟨function(v_{1}, …, v_{n})B, ρ⟩: (func(σ_{1}, …, σ_{n}): τ).

(v) Suppose C, E ⊢ M(N_{1}, …, N_{n}): τ. Thus C, E ⊢ M: (func(σ_{1}, …, σ_{n}): τ), and for all 1 ≤ i ≤ n, C, E ⊢ N_{i}: σ_{i}. If (C, E ⊢ M(N_{1}, …, N_{n}): τ, ρ, s) ↓ (V, s′), then

(M, ρ, s) ↓ (⟨function(v_{1}, …, v_{n})B, ρ_{f}⟩, s^{1}),
(N_{i}, ρ, s^{i}) ↓ (V_{i}, s^{i+1}),

and

(B, ρ_{f}[V_{i}/v_{i}], s^{n+1}) ↓ (V, s′).

By induction, all s^{i} and s′ are consistent with C,

C, E_{0} ⊢ ⟨function(v_{1}, …, v_{n})B, ρ⟩: (func(σ_{1}, …, σ_{n}): τ),

and for all 1 ≤ i ≤ n, C, E_{0} ⊢ V_{i}: σ_{i}.

By the type-checking rules for closures and functions, C, (ρ_{f}[V_{i}/v_{i}])^{T} ⊢ B: τ. Clearly ρ_{f}[V_{i}/v_{i}] is consistent with (ρ_{f}[V_{i}/v_{i}])^{T}, so by induction, C, E_{0} ⊢ V: τ.

(vi) Suppose C, E ⊢ {m_{1} = e_{1}: τ_{1}, …, m_{n} = e_{n}: τ_{n}}: {m_{1}: τ_{1}; …; m_{n}: τ_{n}} and

({m_{1} = e_{1}: τ_{1}, …, m_{n} = e_{n}: τ_{n}}, ρ, s) ↓ {m_{1} = V_{1}: τ_{1}, …, m_{n} = V_{n}: τ_{n}}, s′).

Then for 1 ≤ i ≤ n, (e_{i}, ρ, s^{i}) ↓ (V_{i}, s^{i+1}) (where s = s^{1} and s′ = s^{n+1}). By induction, C, E_{0} ⊢ V_{i}: τ_{i} and all s^{i} are consistent with C. Thus, C, E_{0} ⊢ {m_{1} = V_{1}: τ_{1}, …, m_{n} = V_{n}: τ_{n}}: {m_{1}: τ_{1}; …; m_{n}: τ_{n}} and s′ is consistent with C.

(vii) Suppose C, E ⊢ e.m_{i}: τ_{i} and (e.m_{i}, ρ, s) ↓ (V_{i}, s′). Then C, E ⊢ e: {m_{1}: τ_{1}; …; m_{n}: τ_{n}} and (e, ρ, s) ↓ {m_{1} = V_{1}: τ_{1}, …, m_{n} = V_{n}: τ_{n}}, s′). By induction,

C, E_{0} ⊢ {m_{1} = V_{1}: τ_{1}, …, m_{n} = V_{n}: τ_{n}}: {m_{1}: τ_{1}; …; m_{n}: τ_{n}}.

Thus, C, E_{0} ⊢ V_{i}: τ_{i}, as desired.

(viii) Suppose C, E ⊢ class(a, e): ClassType(σ, τ) and (class(a, e), ρ, s) ↓ (class(V_{a}, V_{e}), s′′). Then C^{IV} , E ⊢ a: σ and C^{MET H}, E^{MET H} ⊢ e: τ. Also, (a, ρ, s) ↓ (V_{a}, s′) and

(e, ρ[self /self , close/close], s′) ↓ (V_{e}, s′′).

By induction, C^{IV} , ∅ ⊢ V_{a}: σ and

C^{MET H}, {self : SelfType, close: (func(SelfType): MyType)} ⊢ V_{e}: τ

(this last because ρ[self /self , close/close] is consistent with E^{MET H}).

Thus C, ∅ ⊢ class(V_{a}, V_{e}): ClassType(σ, τ). By induction s′ and s′′ are consistent with C.

(ix) Suppose C, E ⊢ new c: ObjectType τ, and thus that C, E ⊢ c: ClassType(σ, τ). Suppose moreover that (new c, ρ, s) ↓ (newLoc_{n+1}, s′n + 1 where

(c, ρ, s) ↓ (class({iv_{1} = V_{1}: σ_{1}, …, iv_{n} = V_{n}: σ_{n}}, Methods), s^{0}),

for 1 ≤ i ≤ n,

(newLoc_{i}, s^{i}) = (GetNewLoc s^{i−1} σ_{i}[ObjectType τ/MyType] V_{i}[ObjectType τ/MyType]),
newIV = {iv_{1} = newLoc_{1}: ref σ_{1}, …, iv_{n} = newLoc_{n}: ref σ_{n}},
o′ = obj(newIV, Methods),

newMethods = Methods[o′/self, close_{(σ,τ)}/close, VisObjType(σ, τ)/SelfType, ObjectType τ/MyType], and

(newLoc_{n+1}, s^{n+1}) = GetNewLoc s^{n} VisObjType(σ, τ) obj(newIV, newMethods).

If we show that C, E_{0} ⊢ V_{i}: τ_{i} and C, E_{0} ⊢ obj(newIV, newMethods): VisObjType(σ, τ), then we will be done since then each s^{i} will be consistent with C, and C, ∅ ⊢ newLoc_{n+1}: ObjectType τ since ObjectType τ = ∪_{σ∈RecordT ype}Loc_{VisObjType(σ,τ)}.

By induction,

C, ∅ ⊢ class({iv_{1} = V_{1}: σ_{1}, …, iv_{n} = V_{n}: σ_{n}}, Methods): ClassType(σ, τ).

Thus

C^{IV} , ∅ ⊢ {iv_{1} = V_{1}: σ_{1}, …, iv_{n} = V_{n}: σ_{n}}: σ

and

C^{MET H}, ∅^{MET H} ⊢ Methods: τ,

where ∅^{MET H} = {self : SelfType, close: (func(SelfType): MyType)}.

Thus, for 1 ≤ i ≤ n, C^{IV} , ∅ ⊢ V_{i}: σ_{i}. By the remarks before the statement of the theorem, it follows that C, ∅ ⊢ V_{i}[ObjectType τ/MyType]: σ_{i}[ObjectType τ/MyType]. Thus the applications of GetNewLoc resulting in s^{i} are type-correct, and thus the s^{i} for 1 ≤ i ≤ n are consistent with C.

To finish the proof of this case we need only show

C, E_{0} ⊢ obj(newIV, newMethods): VisObjType(σ, τ).

Clearly C^{IV} , ∅ ⊢ newIV: RecT oMem(σ)[ObjectType τ/MyType]. Again using the remarks before the theorem and C^{MET H}, ∅^{MET H} ⊢ Methods: τ, it follows that

C, {self : VisObjType(σ, τ)} ⊢ Methods[close_{(σ,τ)}/close, ObjectType τ/MyType, VisObjType(σ, τ)/SelfType]: τ[ObjectType τ/MyType]

Thus C, ∅ ⊢ o′: VisObjType(σ, τ). It follows easily by induction on the length of the typing proof that C, ∅ ⊢ newMethods: τ[ObjectType τ/MyType].

It follows immediately that

C, ∅ ⊢ obj(newIV, newMethods): VisObjType(σ, τ),

(note that obj(newIV, newMethods) contains no free occurrences of self). Thus s^{n+1} is consistent with C.

(x) Suppose C, E ⊢ close_{(σ,τ)} e: ObjectType τ. Therefore C, E ⊢ e: VisObjType(σ, τ). Suppose (e, ρ, s) ↓ (o′, s′), for

o′ = obj(a, Meth)

and

(l, s′′) = GetNewLoc s′VisObjType(σ, τ) obj(a, newMethods)

where

newMethods = Methods[o′/self, close_{(σ,τ)}/close,

VisObjType(σ, τ)/SelfType, ObjectType τ/MyType].

By the natural semantics rules,

(close_{(σ,τ)} e, ρ, s) ↓ (l, s′′).

By induction, s′ and s′′ are consistent with C and C, ∅ ⊢ l: ObjectType τ, as long as

C, ∅ ⊢ obj(a, newMethods): VisObjType(σ, τ).

By induction, C, E_{0} ⊢ obj(a, Methods): VisObjType(σ, τ), and hence

C, {self : VisObjType(σ, tau)} ⊢ (Methods: τ)[close_{(σ,τ)}/close, VisObjType(σ, τ)/SelfType, ObjectType τ/MyType].

As in the previous case,

C, ∅ ⊢ newMethods: τ[ObjectType τ/MyType],

and hence, C, ∅ ⊢ obj(a, newMethods): VisObjType(σ, τ).

(xi) Suppose (o ⇐ m_{i}, ρ, s) ↓ (V_{i}, s′) follows from (o, ρ, s) ↓ (l, s′) where

s′(l) = o′ =_{def} obj(a, {m_{1} = V_{1}: τ_{1}, …, m_{n} = V_{n}: τ_{n}}).

Suppose C, E ⊢ o: γ. By induction, s′ is consistent and C, ∅ ⊢ l: γ. It then follows from the structure of o′ = s′(l) that there exist σ and τ such that γ = ObjectType τ and C, E_{0} ⊢ o′: VisObjType(σ, τ). Thus C, E ⊢ o ⇐ m_{i}: τ_{i}[ObjectType τ/MyType].

From the type-checking rule for obj terms it follows that

C, {self : VisObjType(σ, τ)} ⊢ (V_{i}: τ_{i})[close_{(σ,τ)}/close, ObjectType τ/MyType, VisObjType(σ, τ)/SelfType].

However, by the hypotheses of the theorem, since o has an object type, V_{i} contains no free occurrences of self, close, SelfType, or MyType. Therefore,

C, ∅ ⊢ V_{i}: τ_{i}[ObjectType τ/MyType].

(xii) Suppose (o ⇐ m_{i}, ρ, s) ↓ (error_{τ} , s′) because (o, ρ, s) ↓ (nil, s′). By the definition of the natural, semantics, C, E ⊢ o ⇐ m_{i}: τ, and C, ∅ ⊢ error_{τ}: τ by definition. Moreover, s′ is consistent by induction.

(xiii) Suppose (o′.iv_{i}, ρ, s) ↓ (V_{i}, s′) via (o′, ρ, s) ↓ (obj({iv_{1} = V_{1}: ref σ_{1}, …, iv_{n} = V_{n}: ref σ_{n}}, e), s′). If C, E ⊢ o′: VisObjType(σ, τ), it follows by induction that

C, E_{0} ⊢ obj({iv_{1} = V_{1}: ref σ_{1}, …, iv_{n} = V_{n}: ref σ_{n}}, e): VisObjType(σ, τ).

Clearly σ = {iv_{1}: σ_{1}, …, iv_{n}: σ_{n}}. Thus C, E ⊢ o′.iv_{i}: ref σ_{i}. By the typing rules for obj terms, C, ∅ ⊢ V_{i}: ref σ_{i}, as desired.

The cases for update and extend are similar to those for class.