Safe Type Checking in a Statically-Typed Object-Oriented Programming Language

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

Abstract

In this paper we introduce a statically-typed, functional, object-oriented programming language, TOOPL, which supports classes, objects, methods, instance variables, subtypes, and inheritance.

It has proved to be surprisingly difficult to design statically-typed object-oriented languages which are nearly as expressive as Smalltalk and yet have no holes in their typing systems. A particular problem with statically type checking object-oriented languages is determining whether a method provided in a superclass will continue to type check when inherited in a subclass. This problem is solved in our language by providing type checking rules which guarantee that a method which type checks as part of a class will type check correctly in all legal subclasses in which it is inherited. This feature enables library providers to provide only the interfaces of classes with executables and still allow users to safely create subclasses.

The design of TOOPL has been guided by an analysis of the semantics of the language, which is given in terms of a sufficiently rich model of the F-bounded second-order lambda calculus. This semantics supported the language design by provided a means of proving that the type-checking rules for the language are sound, ensuring that well-typed terms produce objects of the appropriate type. In particular, in a welltyped program it is impossible to send a message to an object which lacks a corresponding method.

1 Introduction

Two very influential papers on the foundations of object-oriented programming languages were presented at the 1990 POPL conference. The first, [CHC90], argued that subtyping and inheritance were distinct concepts, providing examples showing that subclasses did not always result in subtypes. It then demonstrated that many object-oriented features could be modeled in the “F-bounded” second order lambda calculus, an extension of the bounded secondorder lambda calculus. (See also [CCH^{+}89] for more discussion and examples in this language.)

The second paper, [Mit90], showed how delegation, a variant of inheritance, could be modeled in a record calculus which supported record extensions (but not full subtyping) and bounded quantification over functions from types to types.

In each case, a term could be determined to be typesafe if the translation of the term into the higher-order language type-checked. Moreover this type checking of the translation ensured that methods of the original language remained well-typed when inherited.

While both papers represented important progress in the foundations of object-oriented programming languages, both simulated features of object-oriented languages in higher-order languages which included quantification over types or functions from types to types. This made each rather difficult to relate directly to languages that a programmer would recognize as object-oriented.

This paper is an attempt to extend the work in these two papers by presenting a statically-typed object-oriented language, TOOPL (for Typed Object-Oriented Programming Language), which is based on a firm semantic foundation. Unlike the languages in the papers referred to earlier, TOOPL is a firstorder (functional) object-oriented programming language which directly supports all of the common features of the object-oriented paradigm, including classes, objects, methods, updatable instance variables, subtypes, and inheritance. It supports the use of an identifier, usually written self, which refers to the current object, and its type, usually written My-Type. It also provides a mechanism to refer to methods of the superclass of a class being defined.

∗Part of this work was done while the author was on leave at the Computer Science Department, Stanford University, at the DEC Systems Research Center in Palo Alto, California, and at the Département de Mathématiques et d’Informatique, Ecole Normale Supérieure, in Paris. This research was partially supported by NSF grants CCR - 9105316 and CCR-9121778, and, at Stanford, the Powell Foundation.

We also provide static type-checking rules for the language. The rules for type-checking classes are based on those presented in [Mit90], extended to support subtyping rather than only simple type extensions.

Following [CHC90], we separate the subtype and inheritance hierarchies. This results in a more flexible language while preserving type safety. One advantage of this separation of classes and types is that objects generated from distinct classes can have the same type. For example, Point objects represented using Cartesian coordinates can be defined so as to have the same type as point objects represented using polar coordinates.

In order to make possible a proof that the typechecking system is safe, we have provided a denotational semantics of the language, which is presented in terms of a model of the F-bounded second-order lambda calculus which contains fixed points at both the type and element level. Using this semantics we are able to prove that the type-checking rules are sound.

Since TOOPL is functional, updating an instance variable results in a new object which differs from the original only in the value of the instance variable which was changed. Instance variables are hidden outside of an object. The semantics of the hidden instance variables are given in terms of existential types, as presented in [MP88].

While the semantics is presented in terms of a model of the F-bounded second-order lambda calculus, the user has no need to understand this more complex language, since our type-checking rules are all presented in terms of first-order constructs. The same is true of the operational semantics of the language, which is not, however, discussed in this paper.

The major focus of this paper is the design of safe static type-checking rules for object-oriented languages, as illustrated in TOOPL. Type-checking problems arise when methods are redefined in subclasses. A key question we will answer is what changes to the types of methods are allowed in subclasses. However, equally severe problems can occur when methods are inherited (i.e., without change) in subclasses. Suppose we have type checked a method in the context of the class in which it is defined. If its body includes sending messages to self, and those messages may be modified in the subclass, how can we be assured that this method will continue to type check when inherited? We would like to have type-checking rules which guarantee that, once a method is type checked, it will be type correct in all subclasses in which it is inherited. This is certainly necessary if vendors are going to provide libraries of classes in compiled form only.

Our understanding is that in Trellis/Owl [SCB^{+}86] and Typed Smalltalk [GJ90], for example, method bodies are type checked again when they are inherited in subclasses. This is unsatisfactory from our point of view, since the source code of the original class will generally not be available at the time the subclass is compiled.

In the language described in this paper, we will provide type-checking rules which will allow us to inherit methods in subclasses with the assurance that they are type correct without the necessity of type checking them again in the context of the definition of the subclass.

Thus TOOPL satisfies the following conditions:

1. If we can prove that a term of TOOPL 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.

2. If a class has a type, then we provide rules for deriving subclasses which guarantee that all inherited methods continue to have the types specified in the superclass. In particular, only the types of the instance variables and methods of the superclass need be known in order to type check the subclass.

In the next two sections we provide a very brief explanation of the fundamental concepts and terminology commonly used in object-oriented languages and give an example of a program which causes problems with most object-oriented languages. We then describe the syntax and type-checking rules for our language. In section 5 we give a brief sketch of a denotational semantics for this language. This semantics provides the basis for our proof of a soundness theorem which shows that our type-checking rules are correct with respect to the semantics.

Because of space limitations, we concentrate on the language without instance variables. However in section 6 we provide a brief sketch of the changes necessary in order to include instance variables. The addition of instance variables provides significant added complications in both type-checking and specifying the denotational semantics of object-oriented languages. (A more detailed presentation of the full language can be found in [Bru92b].) Finally we compare our work with that of other researchers in the area and discuss other recent results on TOOPL.

2 Fundamental concepts of object-oriented languages

We presume the reader is familiar with object-oriented languages and simply provide a quick description of the terminology used in the rest of the paper.

The language described in this paper offers full support for object-oriented features including objects, classes, methods, instance variables, dynamic method dispatch, subclasses, and subtypes. We provide mechanisms to allow the programmer to refer to the current object (self) and the record of methods of its superclass (super). Moreover the language provides a term which refers to the type of the current object (MyType), which can be used in type-checking terms. These concepts are described briefly below.

An object consists 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 type safety. A subclass inherits those methods of its superclass which are not redefined in the subclass. These methods can then be used as though they were part of the subclass definition.

All terms of the language, including both classes and objects, have associated types. In the language described in this paper, instance variables are not visible outside of objects. Since types describe only the public interfaces of objects, neither the instance variable names nor their types are referred to in object 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 inheritance depends upon their implementations.

Virtually all object-oriented languages provide programmers with a mechanism for sending a message from an object to itself. We will use the keyword self in methods as a name for the object which is currently executing the method. Since our language is statically typed, it will be necessary to assign a type to all occurrences of self. While one could simply give self the same type as the object being defined, complications involving subclasses lead us to find a different solution.

The complications arise when a method whose body involves self is inherited in a subclass. In the inherited method, self will now refer to objects generated from the subclass rather than from the original class. Because the meaning of self will change in subclasses, its type will change as well. Thus we will use the keyword MyType as the type of self. (Technically, both self and MyType are bound variables, rather than key words, in TOOPL. This allows for the possibility of nested class definitions. A language designed for serious software production would probably make these reserved words of the language.)

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 the keyword super to refer to the record of methods of the superclass.

3 Problems with type-checking object-oriented languages

Statically-typed object-oriented programming languages are notorious for the holes in their typing systems or their reliance on type casting in order to support a style of programming nearly as flexible as weakly typed languages like Smalltalk. Since one of the goals of this research is to produce a language whose type system is safe, we present an example here which gives most statically-typed object-oriented languages problems, though it is easily expressed in Smalltalk. The example is presented in a variant of TOOPL without instance variables.

In the following, p <= m denotes sending the message m to the object p.

PointClass = class(self:MyType)

                                                      {x = 0,
                                                       y = 0,
                                                       eq = fun(p:MyType)((self<=x) = (p<=x))
                                                                       & ((self<=y) = (p<=y))}

PointClass has three methods named x, y, and eq. The method eq takes a parameter, p, with the same type as self and compares the results of sending messages x and y to p and the results of sending the same messages to self. (In Section 6 we exhibit another version of this example in which x and y are instance variables, rather than methods.)

The operator new applied to a class returns a new object of that class.

                                                  PtObj = new PointClass

The type of PtObj is the type PointType:

PointType = ObjectType(MyType)

{x,y:Int;
eq:MyType -> Bool}

Next we modify PointClass by adding a color field, c, and updating method eq in ColorPointClass so that it calls the inherited eq from PointClass (using the keyword super) and then checks “c” components for equality.

ColorPointClass = modify PointClass by

(self:MyType,

super:{x,y:Int;eq:MyType->Bool})
{c = Red,
eq= fun(p:MyType)super.eq(p) &
((self <= c) = (p <= c))}

(We have taken a few liberties with TOOPL here and combined “update” and “extend” operations in forming ColorPointClass. The formal language would require us to define this in two steps.) ColorPointClass inherits the definitions of x and y

from PointClass.

As before we can create new objects from this class.

ColorPtObj = new ColorPointClass
ColorPtObj has type ColorPointType:
ColorPointType = ObjectType(MyType)
{c:ColorType;
x,y:Int;
eq:MyType -> Bool }

The definition of the subclass ColorPointClass from PointClass is a very natural one and typechecks without problem in TOOPL. However problems may arise if we make the incorrect assump-

tion that ColorPointType is a subtype of PointType.

Consider the following function:

BreakIt = fun(p:PointType)
p <= eq (new PointClass)

This is a perfectly reasonable function which takes a point p as a parameter and checks to see if it is equal to a new object formed from PointClass. In particular, it checks to see if its x and y components are both 0. This program type-checks without problem in TOOPL.

Suppose for a moment that ColorPointType is a subtype of PointType. If so, then a term of type ColorPointType may be used in any context which expects a term of type PointType. Thus it would be

legal to write BreakIt(ColorPtObj).

However, this function call breaks the type sys-

tem since ColorPtObj <= eq (new PointClass) is

not well-typed. ColorPtObj <= eq expects a pa-

rameter of type ColorPointType, not PointType.

If the system attempted to evaluate the term BreakIt(ColorPtObj) it would crash since it would execute the code for eq which is associated with ColorPointClass and collapse when it tried to call the (non-existent) color method of new PointClass. Thus ColorPointType can not be a subtype of PointType. (In fact this argument shows that PointType can have no proper subtypes in which eq has type MyType -> Bool!)

This example creates serious problems for most well-known statically-typed object-oriented languages, since they typically identify the notions of subtype and subclass. More precisely, they presume that any legal subclass must be a subtype. The original versions of Eiffel allowed the definition of the subclass

ColorPointClass of PointClass, and then crashed if

the function BreakIt were applied to an object generated by ColorPointClass. Version 3.0 of Eiffel works around this problem by adding an extra level of type checking at link time. This system-wide type checking essentially performs a data flow analysis of all classes of the program in order to ensure that only type-safe message sends are performed (see [Mey92] for more details). Classes defined like ColorPointClass and PointClass would type check, but programs which included a class in which BreakIt were applied to an object generated by ColorPointClass would result in a type error during the link-time type check. We consider this solution unsatisfactory since individually correct classes may combine to produce an incorrect system. Moreover, this type-checking system requires access to the source code (or some close approximation) for all classes in the system. Since we would like our language to support the provision of libraries which could be provided in compiled form only, this solution will not meet our needs.

Other languages avoid this problem by declaring the subclass ColorPointClass to be illegal. Trellis/Owl declares it to be illegal since it only allows subclasses which are also subtypes. C++ [Str86], Object Pascal [Tes85], and Modula-3 [CDG^{+}88] do not allow the user to redefine the types of parameters in subclasses, so the proposed redefinition of eq in ColorPointClass is illegal (though in C++ and Object Pascal it can be hacked together by by-passing the type system and coercing the argument of eq to be an object of ColorPointType in the body of eq). Sather [Omo91] (a variant of Eiffel) allows redefinition of types of parameters, but they must be redefined to be supertypes rather than subtypes.

TOOPL allows us to define ColorPointClass in a type-safe way by allowing it to be a subclass, without insisting that ColorPointType be a subtype of PointType. TOOPL thus combines expressibility with type-safety.

4 TOOPL - a statically-typed object-oriented language

In this section we introduce TOOPL (Typed Object-Oriented Programming Language), a functional, statically-typed object-oriented language. We provide an informal definition in this section, leaving the formal definition to Appendix A. Because of space limitations, we describe only the subset of the full language with methods but no instance variables here. In section 6 we provide a sketch of some of the changes neccessary to include updatable instance variables.

4.1 Types, ≤, and ≤_{meth}

We begin by defining the types of our language. A type is either a type variable, a constant, or of the form σ → τ (for functions), {m_{1}: τ_{1};…;m_{n}: τ_{n}} (for records), ObjectType(MyType)τ (for object types), or ClassType(MyType)τ (for classes). In the last two expressions, MyType is considered to be a bound type variable, while τ must be a record type. The bound type variable MyType occurring in ObjectType and ClassType types will be used as the type of self in definitions of methods associated with these objects and classes.

Because we are distinguishing between subtype and subclass, it will be convenient to define two different orders on type expressions. The first, ≤, is the subtype ordering, which effectively determines when elements of one type may be used in place of elements of another type. The second ordering, ≤_{meth}, will only be defined on object types, and will correspond to a pointwise ordering on the types of corresponding methods. We will see that this ordering is very useful in type checking classes as it is related to the types of objects generated by subclasses.

A type constraint system is a finite sequence of statements of the form t ≤ τ or t ≤_{meth} τ where t is a type variable and τ is a type expression. (See the formal definition in Appendix A.)

The axioms and rules for ≤ and ≤_{meth} are given in Appendix A and are the familiar ones for function and record types. (See [Car88a] for justifications.) Note that rule (S →) for subtyping function types is contravariant in the domain and covariant in the range. Rule SRec for record types is as usual, with subtypes possibly containing more fields than the supertypes, while the types of record components may be replaced by subtypes of those found in the supertype.

The subtyping rule for object types is the only new rule here. It is derived from the rule in [AC90] for recursive types. The complexity is due to the inherently recursive meaning of MyType. The intuition behind the rule is that if ObjectType(MyType)τ ≤ ObjectType(MyType′)τ′, then MyType represents a type which is less than that represented by MyType’. Thus if we can show that τ ≤ τ′, assuming only that MyType ≤ MyType’, then the conclusion follows. (We refer the reader to [AC90] for more details and a more rigorous justification of this rule.)

On the other hand, the “obvious” subtyping rule for objects is essentially the one given for ≤_{meth}. However, our earlier example of ColorPointType and PointType in Section 3 shows that this rule fails. In particular,

                                                  {c:ColorType;x,y:Int;eq:MyType->Bool} ≤
                                                                  {x,y:Int;eq:MyType->Bool} ,
                                                  but ColorPointType is not a subtype of PointType.

Instead this more obvious rule is the basis for the ordering ≤_{meth}. It is an ordering of object types only. The following rule is derivable from rules MRefl and MT rans.

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

While the conclusion fails for subtypes, it reflects exactly the way in which subclasses are formed. That is, one object type will be ≤_{meth} to another if it has more methods or if types of some methods in the larger have been replaced by their subtypes in the smaller. We use the notation ≤_{meth} in order to remind us that this ordering depends only on comparisons of the types of methods. If C' is a subclass of C such that C' generates objects of type T', and C generates objects of type T, then T' ≤_{meth} T. In particular ColorPointType

                                                  ≤_{meth} PointType.

4.2 Terms and type assignment

The syntax of pre-terms is given in Figure 1. A preterm of the form class(self:MyType)e represents a class with e as the record of method definitions. Inside those methods, self is used to refer to the object itself, while MyType designates its type. The extend and update pre-terms represent subclasses of c which are formed by either adding a new method (in the case of extend) or updating a method of c. In either of these cases, self and MyType are used as in class terms, while super is used to refer to the record of methods of the superclass. A pre-term of the form new c represents a new object whose methods are those specified in c. Finally o <= m designates the result of sending the message m to object o.

The terms of TOOPL are given with respect to a type-constraint system, C, and a syntactic type assignment, E. The terms with respect to C, E are those pre-terms which can be assigned a type by the type assignment axioms and rules in appendix A. C

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

class(self:MyType) e | update c by(self:MyType;super: {m_{1}: τ_{1};…;m_{n}: τ_{n}}){m_{1} = e′_{1}} | extend c with(self:MyType;super: {m_{1}: τ_{1};…;m_{n}: τ_{n}}) {m_{n+1} = e_{n+1}} | new c | o <= m.

Figure 1: Pre-terms of TOOPL without instance variables

describes any assumptions that we may have on supertypes of type variables, while E describes the intended type of term variables. In the rest of this section we explain the intuition behind these rules and axioms.

The type-assignment rules for variables, if-then-else, function abstractions and applications, and records are similar to those for ordinary programming languages, and are omitted here. The last rule, Subsump, reflects exactly our intuition for subtypes. That is, an element of a subtype can be treated as an element of its supertype.

We focus on those rules which are specific to objectoriented languages. We urge the reader to examine briefly all type assignment rules in Appendix A before proceeding with the explanations in this section.

As discussed earlier, we wish to type check methods in classes so that they need not be type checked again when inherited in subclasses. Because an inherited method may depend on yet another method which may be redefined in a subclass, it is important to know how that redefined method might be changed.

Suppose D is a class with method m = … self <= n … where n is a method of D with type τ. If Dsub is a subclass of D in which m is inherited, but in which n is redefined to have type τ′, we have to ensure that m still type checks. We will be able to assign m the same type as before if self <= n can be assigned the same type in Dsub as in D. Since self <= n has type τ inside D and has type τ′ inside Dsub, we can use subsumption to assign self <= n the type τ in Dsub as long as τ′ ≤ τ.

Note that the type of a method m may involve the type MyType. In this case the meaning of MyType in class D will likely be different from its meaning in a subclass Dsub. However, if m is inherited in Dsub, all occurrences of self (and other expressions of type MyType) will now have a type corresponding to objects generated from Dsub rather than D. If the only assumption we make about MyType when we type check m in D is that MyType is a type of objects generated from a subclass of D (not necessarily exactly D), then the type-checking proof for m could be carried out in exactly the same way for Dsub as for D.

The preceding discussion can be summarized as follows:

1. If we redefine a method m from a class D in a subclass, the type of the redefined m should be a subtype of that in D.

2. If we can successfully type check a method, while only assuming that MyType is the type of objects generated by some unspecified subclass of D, then the body of m will type check properly if copied into any subclass of D.

Of course, subclasses can also be formed by adding new methods to a class. The two ways of forming subclasses correspond exactly to having the type of the record of methods of the subclass be a subtype of the record of methods of the superclass. As discussed at the end of the previous section, this corresponds exactly to our ordering ≤_{meth} on object types.

At this point we have sufficient information to explain the type assignment rule, Class. In order to show class(self:MyType)e has type ClassType(MyType)τ, it is sufficient to show that e has type τ under the assumption that self has type MyType. In this derivation one is only allowed to assume that MyType ≤_{meth} ObjectType(MyType)τ. That is, we may only assume that MyType is the type of an object generated by a subclass of class(self:MyType)e. The discussion above on assuring the type correctness of inherited methods provides the intuition behind this rule.

We next discuss the typing rules for subclasses. Rule Update determines when a term

update c by(self:MyType; super: {m_{1}: τ_{1};…;m_{n}: τ_{n}}){m_{1} = e′_{1}}

has type

ClassType(MyType)

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

It is sufficient to show that the new body e′_{1} of m_{1} has a type, τ′_{1}, which is a subtype of the type τ_{1} of m_{1} in c. As with classes, we type check the new body of m_{1} under the assumption that self has type MyType, which is a type of objects generated by an undetermined subclass of the updated class. (This ensures that the new body of m_{1} will remain type correct in all subclasses of the updated class.) The new body e′_{1} of method m_{1} may also refer to the record super of the methods of the superclass. Thus the assumption that the type of super is that of the record of methods of c can be used in type checking e_{1}.

The rule, Extend, for subclasses formed by adding new methods is similar, and will not be discussed further here.

The type-assignment rule for objects of the form new c is straightforward. The new object has a type of the same shape as the class, c, except that it is an ObjectType rather than a ClassType.

Finally we come to the rule for type checking a message sent to an object. It is possible that when a message is sent to an object, we may not have exact information about the type of its methods. The most common way this arises is in sending a message to self. In a method all we know is that the type of self, MyType, is ≤_{meth} to the type of objects generated by the class being defined (see the type assignment rule for class terms). Thus the type assignment rule, Message, must take this into consideration. Message determines that o <= m has type τ[γ/MyType] if o has type γ and γ is an object type corresponding to a subclass of a class with method m of type τ (i.e., γ ≤_{meth} ObjectType(MyType){m: τ}). Notice that γ is substituted in for MyType in the final type since MyType stands for the type of self, which is γ at the time the message is sent.

The careful reader might worry at this point that there may be several choices for the τ in the relation γ ≤_{meth} ObjectType(MyType){m: τ} in the previous paragraph. We hope it will be somewhat reassuring to point out that

γ ≤_{meth} ObjectType(MyType){m: τ′}

≤_{meth} ObjectType(MyType){m: τ}

only if τ′ ≤ τ, and hence if τ′[γ/MyType] ≤ τ[γ/MyType]. (Of course, the ultimate reassurance is the proof of Theorem 5.1).

5 The soundness of type assignment in TOOPL

In this section we discuss some of the ideas behind the proof of the soundness theorem for our type assignment rules. The soundness theorem states that in a denotational model for TOOPL, for all terms M of TOOPL, all type-constraint systems, C, and all syntactic type assignments, E, if the assignment of variables to values in the model satisfies C and E, and if C, E ⊢ M: τ, then the value of M in the model is an element in the set of values corresponding to type τ.

Other soundness theorems of this sort can be provided by analyzing the operational semantics of a language and showing that types are preserved under computations. (Such a “subject reduction” theorem is true in TOOPL and will be presented in a future paper).

Another alternative is to provide a semantics in terms of an untyped model and then show that all terms with a particular type lie in that part of the model corresponding to the set of elements of its type.

In our case, the meaning of a term is given by induction on its typing proof. Hence untyped terms are not given meanings at all.

Since we do not have to provide meanings for untyped terms, our semantics can be given in a simpler form than might otherwise be possible, since we will not need to put in checks that values have the appropriate forms. Our soundness theorem essentially says that these checks can be omitted because an element which has type τ can be shown to be in the set of elements corresponding to the meaning of τ. This makes life much easier for us since we know, for instance, that if M has type σ → τ, we can be guaranteed that its meaning is a function. Hence we will not need to check this in a semantic definition before applying it to the meaning of an element of type σ. Of course if this theorem failed, then our semantics of terms of TOOPL would not necessarily be well-defined.

In order to present our soundness theorem, we need to know something about the possible models of our language, and how to find the meaning of terms in this model.

One class of models which will satisfy our needs is the collection of models of F_{≤} described in [BM92]. The types in these models are partial equivalence relations over a model of the untyped lambda calculus. These models can be used to interpret terms of the bounded second-order lambda calculus [Gir71, Rey74], and thus support a subtype ordering which corresponds to our ≤. These models also contain solutions to all relevant fixed-point type and value equations. A model having these features is sufficient to interpret TOOPL. For instance the solutions to fixed-point equations allow us to find meanings for self-referential terms of TOOPL like self and MyType.

In [Bru92b] we give a detailed description of the semantics of TOOPL. In what follows we simply provide a sketch of these semantics in order to motivate the soundness theorem. Readers are referred to [Bru92b] for more details.

Let ρ be an environment assigning type and term variables to appropriate types and values of the model. We write [[τ]]ρ for the meaning of type τ in environment ρ, and [[M]]ρ for the meaning of M in ρ. Functions and their types are interpreted as usual, while records are interpreted as functions from field names to elements of the appropriate fields. The interpretations of objects and their types are more complex because of the inherently recursive meaning of self and My-Type.

We begin by discussing object types. If τ is a record type, then

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

That is, the meaning of the object type is simply the meaning of the type of the record of methods in an environment in which MyType has been replaced everywhere by the meaning of the type itself. While this is a recursively defined type, our model allows us to find recursive types by using fixed point operators. Objects themselves are defined recursively so that self is interpreted as the entire object, and MyType is interpreted as its type. Sending a message then simply corresponds to extracting the corresponding field from the record of methods of the receiving object. (In the full language including hidden instance variables, the semantics of message sending is more complex.)

Classes and their types are more complex, because the meaning of a class must specify the meaning of methods not only for objects generated from the class, but also for objects generated from any subclass which inherits those methods. As a result, classes are interpreted as functions which take as a parameter a type which is a possible meaning for MyType. Such a type could arise as the type of an object generated by a subclass of the class being defined. Since we also need to have an interpretation of self in order to obtain the meaning for the methods, the meaning of the class will take a second parameter which is an element of the type passed in as the first parameter.

A simple example should help illustrate this. Let

c = class(self:MyType) {x=2,

       eqX = fun(newx:Int)(self <= x) = newx}.

The type of c is ClassType(MyType){x:Int; eqX:Int -> Bool}. Suppose o = [[new c]]ρ and

T = [[ObjectType(MyType)

                    {x: Int; eqX: Int− > Bool}]]ρ.

Then [[c]]ρ = f, and f(T)(o) is a record with a component x with value 2, and a component eqX which is a function which takes an integer parameter and returns true iff that parameter has value 2. Let T′ be the meaning of a type σ′ such that σ′ ≤_{meth} ObjectType(MyType){x:Int; eqX:Int -> Bool} and let o′ be an object from T′ whose x component is 17. Then f(T′)(o′) is a record with two components, in which the x component is 2 and the eqX component is a function which returns true iff the parameter it is applied to is 17.^{1}

Once the meaning of classes is understood, it is easy to see that the meaning of ClassType(MyType)τ is a collection of functions, each of which takes a type T (constrained as above), and an element of that type, and returns a record with type [[τ]]ρ[T/MyType].

Finally we note that it is possible to interpret the ordering ≤_{meth} in this model. The relation γ ≤_{meth} ObjectType(MyType)τ will be true in the model iff [[γ]]ρ ≤ [[τ]]ρ[[[γ]]ρ/MyType].^{2}

Having given an intuitive description of our model and its semantics, we now state the soundness theorem for the type assignment rules of TOOPL. We say that an environment ρ is consistent with C, E iff when all variables are interpreted in the model according to ρ, all inequalities in C are true, and variables are assigned values in the types specified in E.

Theorem 5.1 (Soundness of semantics with respect to the typing rules) Suppose there is a model as described in this section. For all typing derivations, C, E ⊢ M: σ, if ρ is consistent with C, E, then [[C, E ⊢ M: σ]]ρ will be an element of type [[σ]]ρ. In particular, no term which is well-typed with respect to C, E will ever fail to have a meaning because a message is not understood by an object.

The proof of this theorem can be given by induction on typing derivations.

6 Updateable instance variables

The key difference between methods and instance variables is that methods are frozen when an object is created, while instance variables of an object may be updated. Values of instance variables are specified in class definitions, providing initial values for these instance variables when new objects are created from classes (using the new operator). However it is possible to make a new copy of an object with a different value for an instance variable using the “gets” expression. In TOOPL we provide different notation for accessing instance variables than for sending messages. We write q.x to access the instance variable x of q and p <= getx to send the message getx to p. We update an instance variable x of object p by writing p gets {x = e}. The value of this expression is a new object identical to p but with the value of e replacing the old value of x.

The addition of updatable instance variables to our language adds considerable complexity. One problem is that when defining subclasses, we may not replace the type of an instance variable by a subtype since that may break the typing system.

Suppose class c has instance variable x with type T and has a method m whose body includes the expression self gets {x = e} where e is an expression of type T. If we define a subclass of c which differs only by changing the type of x to be some T' which is a proper subtype of T (and of course providing a new initial value for x), then the inherited method m will break since we can no longer assign e to x. To be legal, we would need T ≤ T' when the reverse is true. Similarly a method which uses the value of x can be used to show that redefining instance variables in a subclass using supertypes rather than subtypes also has problems. Thus no changes are allowed to types of instance variables in subclasses.

1Notice that o′ itself may have more than two fields, and that the value of o′ only affects the meaning of eqX (and not x)

because only the body of eqX in c refers to self.

2See [Bru92b] for an explanation of why ≤_{meth} should be interpreted in this way.

A second complicating factor is that we do not wish to have instance variables visible outside of an object. Thus, we will have two different views of an object: the view from inside the object in which all instance variables are visible, and that from without, in which all instance variables are hidden. We will continue to refer to the type of an object from the outside using MyType, but we will now refer to the type from the inside using SelfType. Inside a method, the type of self will now be SelfType. Often we will need to “close up” an object to hide the instance variables from the outside world. The function “close” with type SelfType -> MyType will perform this action. The following example of a movable point in the full TOOPL should get across the basic idea. (We take the liberty of adding keywords var and methods to make the syntax more readable.)

PointClass =

class(self:SelfType,

close:SelfType->MyType)

(var

{x = 0,
y = 0},

methods

{mv(dx,dy:Int)=
close(self gets {x = self.x + dx,
y = self.y + dy}),
getx = self.x,
gety = self.y,

eq = fun(p:MyType)

(self.x = (p <= getx))
& (self.y = (p <= gety))}})

Notice that there is no way to directly access the instance variables of the parameter p of eq. The type of this class is

PointClassType =

ClassType(MyType)

(var

{x,y:Int},

methods

{mv:Int -> Int -> MT;
getx,gety:Int;
eq:MyType -> Bool})

While the instance variables are visible in the type of PointClass, they are not visible in the correspond-

ing object types. If MyPoint = new PointClass then

the type of MyPoint is:

PointType =

ObjectType(MyType)

      {mv:Int -> Int -> MyType;
       getx,gety:Int;
       eq:MyType -> Bool}

Thus only the types of methods are visible in object types. We also restrict the types of methods to exclude any mention of SelfType, since that information should not be visible outside of the object.

As well as adding some complexity to the subtyping and type-checking rules, the addition of instance variables raises the complexity of the semantics of the language as well. For the moment let us ignore the fact that instance variables are hidden outside object. Then objects are interpreted as pairs where the first component is a record containing the current values of its instance variables, while the second component consists of a function which, when applied to a set of values of the instance variables, returns the meaning of the record of methods.

Recall that the meanings of methods are fixed at object creation time (via taking a fixed point so that each occurrence of self in its methods refers to the object as a whole), while the instance variables can be changed at any time. While we could take a new fixed point every time an object’s instance variable is updated, we prefer to simply make a change to the record of current values of instance variables. As a result we will have to go to a bit more work when we send a message to an object.

When we wish to extract the value of an instance variable of an object, we simply look it up in the first component of the object. However, when we send a message to an object we must now apply the second component of the object to the current value of the record of instance variables before looking up the appropriate method.

Going back to our example, if MyPoint = new

PointClass, then [[MyPoint]]ρ = ({x = 0, y = 0}, f),

where for v a record value of the form {x = a, y = b},

f(v) = {mv = g, getx = a, gety = b, eq = h}

in which, for actual parameters c and d, g(c, d) is ({x = a+c, y = b+d}, f), while h takes another object value, p, from type PointType as a parameter, and returns true iff the results of sending getx and gety to p return the values a and b, respectively.

To evaluate [[MyPoint <= mv(2, 3)]]ρ, we calculate f({x = 0, y = 0}) (since {x = 0, y = 0} is the current value of MyPoint‘s instance variables), extract the meaning of mv and apply it to the parameters 2 and 3, getting as an answer an object with value ({x = 2, y = 3}, f), where f is as above.

If a mv message were sent to this new object, f would now be applied to {x = 2, y = 3} before extracting the meaning of mv and applying it to the actual parameters.

The fact that we wish to hide the instance variables from outside the object brings in one more complicating factor. Fortunately, existential types (see [MP88]) provide exactly what we need. SelfType will be of the form (σ, σ → τ). The function close hides the record of instance variables of an object by converting a pair with type (σ, σ → τ) to an element with the existential type, ∃v.(v, v → τ). Thus MyType and all object types are “existential” types of this form. Since a method only has access to its own instance variables and self has type SelfType, there is no difficulty accessing the needed instance variables.

As in the example with mv above, before a new object is returned as the value of a method, it must be closed so that the outside world has no access to the instance variables. This is enforced by a typechecking requirement that the types of methods not involve SelfType. When a method is sent to an object, one can “open” the existential type to apply the function in the second component to the current value of the instance variables. Since this does not require knowledge of the exact value of v, this is a type-safe operation which provides the appropriate abstraction.

A more complete discussion of the full TOOPL language with instance variables may be found in [Bru92b].

7 Comparison with previous work

As we indicated in the introduction, the language presented in this paper builds on the important papers [CHC90, Mit90]. In a previous paper, [Bru92a], we compared the definitions of inheritance given in the those papers and showed that they were essentially equivalent. While we have chosen to give the semantics of TOOPL using the F-bounded second-order lambda calculus, which is closer to the approach taken in [CHC90], the rules for type-checking are based on those given in [Mit90], modified to handle classes and inheritance rather than delegation, and extended to handle their interactions with subtypes.

While these earlier papers handled only methods, this paper also includes a treatment of instant variables. Instance variables differ primarily from methods in that they can be updated in objects, whereas once an object is created, the methods are frozen.^{3} We also include specific mechanisms for referring to the object receiving a message, self, its type, My-Type, and the methods of the superclass, super. We also have provided a proof that type-checked terms of the language will not encounter type-errors, in particular, those related to sending a message to an object that it does not understand.

This paper differs from most earlier theoretical analyses of statically-typed object-oriented languages by working with a first-order language with primitives for object-oriented notions like class, object, and message sending, rather than simulating them within another, usually higher-order language. We hope the reader has found that our primitives and resulting language are closer to those of real object-oriented programming languages.

There has been considerable interest in the theoretical community in designing object-oriented languages with clean semantical designs. The major influences on the design work described in this paper have come from Cook and his collaborators in the (late and lamented) ABEL project at HP Labs ([CCH^{+}89, Coo89, CCHO89, CHC90]) and the work of Luca Cardelli, John Mitchell and their collaborators ([Car88a, CW85, Car88b, CL91, CM90, Car92a]).

The research closest in spirit to this paper is that of [Car92b]. Cardelli’s goal was slightly different than that of this paper. He wished to find a minimal language which was sufficient for expressing the key concepts of object-oriented programming language. Thus he provides a translation of a language similar to that given here into a simpler language with constructs for subtyping, bounded quantification, and powerful record operations.

A recent series of papers by Pierce and his coworkers [PT92a, PT92b, PH92] represent an alternative approach to that of Cardelli and this paper. Their goal is to model object-oriented languages using secondorder bounded lambda calculus, but using existential types to replace the use of F-bounded lambda calculus (as used in this paper and the work of Cook et al) or higher-order fixed points (as used in the work of Cardelli and Mitchell). While their language seems slightly less expressive (they have difficulty modelling our Point with eq method), their approach allows them to avoid some of the complexity which arises through the proliferation of fixed points in determining the meaning of object-oriented constructs.

8 Conclusion

In this paper we have described a functional, objectoriented programming language, TOOPL, and a set of type assignment rules for performing a static type analysis of terms of the language. More importantly, we have shown that the type assignment rules are sound with respect to a semantics for the language. To our knowledge this is the first statically-typed objectoriented language to be proved to have a sound type system.

3In the case of Mitchell’s language, which is based on delegation, there seems to be no advantage to separating instance variables from methods.

Our language includes all of the standard features of object-oriented programming languages, including objects, classes, methods, updatable instance variables, subtypes, and subclasses. While the full language including instance variables was only sketched here, the instance variables are an important part of the language. In order to support information hiding, objects only have access to their own instance variables. The semantics of objects with instance variables is given using existential types ([MP88]). Because the semantics of TOOPL is given in terms of a model of F_{≤} supporting parametric polymorphism and recursion, it is easy to add these and other features to the language without compromising the static type checking.

It is not uncommon for users to be provided with libraries in the form of compiled code along with information on the types of all accessible routines. The type-checking rules for TOOPL are designed to be especially useful in this circumstance, since access to the source code of a class is not necessary in type checking a subclass. All that is needed is the type information for the methods of the superclass, and the code for all method bodies added or modified in the subclass.

It is worth noting that the subtype relation given in this paper is not as powerful as it could be. Since object types are really just recursively defined types, it is possible to add a Fold/Unfold rule for them that would allow an object type to be replaced by a record type in which all occurrences of MyType would be replaced by the object type. We have chosen not to include such a rule at this point because we are not convinced of its usefulness (even though it is clearly sound). If recursive types (which clearly are useful) were added to TOOPL, one would certainly wish to add such a rule for them.

We have not discussed an algorithm for type checking in this paper. The recent paper [Pie92] showed that the type-checking problem for F_{≤} is undecidable. Since the semantics of TOOPL is based on models of an extension of F_{≤}, one might suspect that the typechecking problem for this language might be undecidable as well.

The undecidability of type checking F_{≤} results from the undecidability of determining if one type is a subtype of another. In contrast, [DM92] have recently shown that the subtype problem is decidable for TOOPL.^{4} Building on this, Bruce, Crabtree, Murtagh, and van Gent have created a simple variant of TOOPL, called TOOPLE (for TOOPL with Extra information). The only differences in syntax between TOOPL and TOOPLE are that class, extend, and update terms must be labeled with their intended types. Then, applying techniques suggested in [CG92], it can be shown (under very natural restrictions on C) that every term which is typeable with respect to C, E has a minimum type. From this an algorithm can be derived which solves the type-checking problem for TOOPLE. Thus this language has useful practical as well as theoretical properties.

Acknowledgements

Thanks to the following for helpful comments on TOOPL and this entire project: Luca Cardelli, John Mitchell, Benjamin Pierce, Giuseppe Longo, the Harvard University Object-Oriented Languages Seminar (including Peter Wegner and Andrew Black), Jon Riecke, and the Williams College TOOPL research group (Tom Murtagh, Jon Crabtree, Gerald Kanapathy, and Robert van Gent).

References

[AC90] Roberto Amadio and Luca Cardelli. Subtyping recursive types. Technical Report 62, Digital Systems Research Center, 1990.

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

[Bru92a] K. Bruce. The equivalence of two semantic definitions of inheritance in objectoriented languages. In S. Brookes, M. Main, A. Melton, M. Mislove, and D. Schmidt, editors, Proceedings of the 7th International Conference on Mathematical Foundations of Programming Semantics, pages 102–124. LNCS 598, Springer-Verlag, 1992.

[Bru92b] K. Bruce. A paradigmatic object-oriented programming language: design, static typing and semantics. Technical Report CS-92-01, Williams College, 1992.

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

4Kozen et al.[KPS93], have shown that subtyping for the extension of TOOPL obtained by adding the Fold/Unfold rule suggested above has an O(n^{2}) algorithm. While their paper does not discuss record types, an addition to handle this seems relatively straight-forward.

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

[Car92b] Luca Cardelli. Typed foundations of object-oriented programming, 1992. Tutorial given at POPL ’92.

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

[CCHO89] P. Canning, W. Cook, W. Hill, and W. Olthoff. Interfaces for strongly-typed object-oriented programming. In Proc. ACM Conf. on Object-Oriented Programming: Systems, Languages and Applications, pages 457–467, 1989.

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

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

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

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

[Coo89] W.R. Cook. A proposal for making Eiffel type-safe. In European Conf. on Object-Oriented Programming, pages 57–72, 1989.

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

[DM92] Allyn Dimock and Robert Muller. Private communication, 1992.

[Gir71] J.-Y.

Girard. Une extension de l’interpretation de Gödel à l’analyse, et son application à l’élimination des coupures dans l’analyse et la théorie des types. In J.E. Fenstad, editor, 2nd Scandinavian Logic Symposium, pages 63–92. North-Holland, 1971.

[GJ90] J. Graver and R. Johnson. A type system for smalltalk. In ACM Symp. Principles of Programming Languages, pages 136–150, 1990.

[KPS93] Dexter Kozen, Jens Palsberg, and Michael I. Schwartzbach. Efficient recursive subtyping. In 20th ACM Symp. Principles of Programming Languages, 1993.

[Mey92] B. Meyer. Eiffel: the language. Prentice-Hall, 1992.

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

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

[Omo91] Stephen M. Omohundro. The Sather language. Technical report, International Computer Science Institute, 1991.

[PH92] Benjamin C. Pierce and Martin Hoffman. An abstract view of objects and subtyping (preliminary report). Technical Report to appear, 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.

[PT92a] Benjamin C. Pierce and David N. Turner. Object-oriented programming without recursive types. Technical Report ECS-LFCS-92-226, University of Edinburgh, 1992.

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

[Rey74] J.C. Reynolds. Towards a theory of type structure. In Paris Colloq. on Programming, pages 408–425. Springer-Verlag LNCS 19, 1974.

[SCB^{+}86] C. Schaffert, T. Cooper, B. Bullis, M. Kilian, and C Wilpolt. An introduction to Trellis/Owl. In OOPSLA ’86 Proceedings, pages 9–16. ACM SIGPLAN Notices,21(11), November 1986.

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

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

A The formal definition of TOOPL

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

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

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

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

4. If τ is a record type expression and MyType ∈ V, then each of ObjectType(MyType)τ and ClassType(MyType)τ are type expressions. MyType is considered to be a bound variable in these two type expressions.

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

As explained in the body of the paper, ≤ represents the subtype relation between types, while ≤_{meth} is an ordering relating types of objects whose classes could have been defined using inheritance.

Definition A.2 Relations of the form σ ≤ τ and σ ≤_{meth} τ, where σ and τ are type expressions, are said to be type constraints. If, moreover, t is a type variable then we say t ≤ τ and t ≤_{meth} τ are simple type constraints. If for some τ, t ≤ τ or t ≤_{meth} τ are included in a set C of simple type constraints, then we say t is declared in C. A type constraint system is defined as follows:

1. The empty sequence, ϵ, is a type constraint system.

2. If C is a type constraint system and t ≤ τ is a simple type constraint such that 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(MyType)σ, and t ≤_{meth} τ is a simple type constraint such that t does not appear in C or τ, then C; t ≤_{meth} τ is a type constraint system.

We define type constraint derivations of the form C ⊢ σ ≤ τ and C ⊢ σ ≤_{meth} τ, for C a type constraint system, and σ, τ type expressions, via the following sets of axioms and rules given below. Note that τ[σ/t] denotes the expression obtained by replacing all free occurrences of variable t in τ by σ.

Axioms and Rules for subtypes:

SRefl C ⊢ τ ≤ τ,

SV ar C; t ≤ τ ⊢ t ≤ τ,

ST rans \frac{C ⊢ γ ≤ σ, C ⊢ σ ≤ τ}{C ⊢ γ ≤ τ} ,

SEq  \frac{C ⊢ σ = τ}{C ⊢ σ ≤ τ} ,

ST rans \frac{C ⊢ γ ≤ σ, C ⊢ σ ≤ τ}{C ⊢ γ ≤ τ} ,

S →  \frac{C ⊢ σ′ ≤ σ, C ⊢ τ ≤ τ′}{C ⊢ σ → τ ≤ σ′ → τ′} ,

SRec \frac{C ⊢ σ_{j} ≤ τ_{j}, for 1 ≤ j ≤ k ≤ n}{\begin{matrix}C ⊢ \{m_{1}: σ_{1}; …; m_{k}: σ_{k}; …; m_{n}: σ_{n}\} \\ ≤ \{m_{1}: τ_{1}; …; m_{k}: τ_{k}\} \end{matrix}} ,

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

In the SObj rule, neither s nor t may occur free in C, τ, or τ′.

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

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

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

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

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

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

Figure 2: Type Assignment Rules

Axioms and Rule for ≤_{meth}:

MV ar C; t ≤_{meth} τ ⊢ t ≤_{meth} τ,

MRefl

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

ObjectType(MyType)τ,

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

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

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

with no variable x_{i} appearing more than once in E.

The standard type assignment rules for the objectoriented terms of the language appear in Figure 2. The type assignment rules for the other terms are as usual.