A Delegation-based Object Calculus with Subtyping

Kathleen Fisher^{⋆} and John C. Mitchell^{⋆⋆}

Computer Science Department, Stanford University, Stanford, CA 94305

                    {kfisher,mitchell}@cs.stanford.edu

Abstract. This paper presents an untyped object calculus that reflects the capabilities of so-called delegation-based object-oriented languages. A type inference system allows static detection of errors, such as message not understood, while at the same time allowing the type of an inherited method to be specialized to the type of the inheriting object. The main advance over previous work is the provision for subtyping in the presence of delegation primatives. This is achieved by distinguishing a prototype, whose methods may be extended or replaced, from an object, which only responds to messages for which it already has methods. An advantage of this approach is that we have full subtyping without restricting the “runtime” use of inheritance. Type soundness is proved using operational semantics and an analysis of typing derivations.

1 Introduction

There are two basic forms of object-oriented languages, the most common of which is class-based. In these languages, which include C++ [Str86, ES90], Smalltalk [GR83] and Eiffel [Mey92], an object is created by a class, which is a construct that creates objects that share a common representation but which may have different specific data values. In typed class-based languages, it is common for all objects created by a given class to have the same type. An alternate approach, advanced in the language Self [US91, CU89], allows objects to be created directly or by cloning (copying) existing objects. In class-based languages, inheritance is a mechanism for defining one class from another. In delegationbased languages, inheritance is a mechanism for reusing part of one object to define another.

Following our previous work [Mit90, FHM94], the object calculus presented in this paper is delegation-based. Initially, we regarded the delegation-based approach as a technically simpler method for analyzing the same underlying language concepts. This appeared correct for the study of method specialization carried out in [Mit90, FHM94], but in [FM94] we observed that there appeared to be a fundamental trade-off between delegation and subtyping. Specifically,

⋆ Supported in part by an NSF Graduate Fellowship, NSF Grant CCR-9303099, and

a Fannie and John Hertz Foundation Fellowship. ⋆⋆ Supported in part by NSF Grant CCR-9303099 and the TRW Foundation.

if an object may be extended with new methods, then it is important to know at compile-time that certain methods have not been defined already. This requirement conflicts with the usual motivation for subtyping, which is to allow code to operate uniformly over all objects having some minimum set of required methods. (Similar and related observations appear in [AC94]; see Section 3.1.)

In this paper, we present one way of resolving this conflict. Intuitively, the main idea is to distinguish between objects that may be extended with additional methods (or have existing methods redefined) and those that cannot. This distinction is achieved by giving different uses of objects different types. In other words, an object may be created, and then have new methods added or existing methods redefined. At this point, only trivial subtyping may be used because the type system must keep track of exactly the set of methods associated with the object. However, such an object may be “converted” to a different kind of object, whose methods can no longer be altered. This conversion is done by changing the type of the object to a form which has the expected subtyping properties. In this way, we allow both delegation and subtyping, at the cost of some increase in the complexity of the type system. An alternate way of extending our previous calculus with subtyping, developed in [BL95], is described in Section 6.

The two forms of object type used in this paper highlight the distinction between two interfaces: the inheritance-interface and the client-interface of an object. This distinction is essentially familiar from object-oriented languages and databases, but often not explicitly mentioned in language documentation. If we write a C++ class such as stack, then there are really two separate ways of using this class. The first is by calling the constructor of the class to create stack objects and then calling their member functions. The second use of the stack class is by defining a derived class. (This “reuse” of implementation is traditionally called inheritance.) One way to see that these are very different uses of a class is to notice that they induce very different notions of class equivalence. If we just want the objects constructed by a class to behave in the same way, then we can perform a number of optimizations and program transformations. However, some transformations that preserve the behavior of constructed objects would observably change the behavior of derived classes. A simple example occurs when a class has two mutually recursive member functions, say f and g. If we replace these functions by two equivalent non-recursive functions, we do not change the behavior of constructed objects. However, this transformation may radically alter the behavior of a derived class if both are virtual functions and one is redefined in the derived class. An innovation of our object calculus, when compared with other recent work such as [AC94, Bru93, FHM94, PT94] (summarized and compared in [FM94]), is the type distinction between these two uses of a class.

The distinction between inheritance and client interfaces leads us to distinguish prototypes and objects. Intuitively, a prototype is a collection of methods that may be used to implement one or more objects. The operations on prototypes are (i) sending a message (which results in the invocation of a method), (ii) adding a new method (method addition), and (iii) redefining an existing method without changing its type (method override). The type of a prototype is called a pro type. For the reasons described above, only trivial subtyping exists between pro types.

Intuitively, an object is created by “packaging” a prototype, an operation that does nothing except “seal” the prototype so that no methods can be added or redefined. In our calculus, the “sealing” operation only changes the type from a pro type to an object, or obj type. Although the only operations allowed on objects from the “outside” are message sends, the methods within an object can override the methods of their host object. This ability to override methods internally permits the existence of methods such as a setX method in a point object which replace the point’s x method with a new one storing a new location. Preventing external method override and method extension by sealing prototypes is sufficient, however, to make interesting subtyping sound for objects. The internal redefinitions do not cause an unsoundness in the type system because they are type-checked with precise knowledge of the pro type of the expression to which they were added.

In addition to subtyping, the distinction between prototypes and objects provides some useful insight into the two uses of classes mentioned above. Inheritance on classes is modeled in our system by operations on prototypes. Creating an object from a class is modeled by “sealing” a prototype to an object. The distinction between pro and obj types clearly illustrates the difference between a derived class’s interface to a class and a client program’s view of the objects created from that class. In particular, inheritance depends on the presence and absence of the methods in a prototype, whereas a client is only concerned with the presence of the methods it uses.

For simplicity, we work with a functional model of objects. Recent studies such as [AC95, Bv93, Pie93] confirm that imperative objects may be treated in essentially the same framework. In addition, our objects are collections of methods; we do not distinguish “member functions” from “member data” since data may be represented by functions that always return the same result. As in [FHM94], our object calculus provides method specialization. Intuitively, method specialization means that the types of methods in classes may be specialized when new classes are created from them via inheritance. Further discussion of method specialization may be found in [FHM94, FM94].

2 Untyped calculus of objects

This calculus is described in full detail in [FHM94]. We briefly summarize it here for presentational completeness.

2.1 The Objects

The untyped object calculus is the result of adding four new object-related syntactic forms to untyped lambda calculus:

⟨⟩  the empty object
e ⇐ m  send message m to object e
⟨e1 ←+ m=e2⟩ extend object e1 with new method m having body e2
⟨e1 ← m=e2⟩  replace e1’s method body for m by e2

We consider ⟨e1 ←+ m=e2⟩ meaningful only if e1 denotes an object that does not have an m method, and ⟨e1 ← m=e2⟩ meaningful only if e1 denotes an object that already has an m method. These conditions will be enforced by the type system. If a method is new, then no other method in the object could have referred to it, so it may have any type. On the other hand, if a method is being replaced, then we must be careful not to violate any typing assumptions in other methods that refer to it.

To simplify notation, we write ⟨m1 = e1, …, mk = ek⟩ for ⟨… ⟨⟨⟩ ←+ m1 = e1⟩ … ←+ mk = ek⟩, where m1, …, mk are distinct method names. Using this abbreviation, we may code a one-dimensional point object with field x and method move as follows:

p =^{def} ⟨ x = λself. 3,

              move = λself. λdx.⟨self ← x = λs.(self ⇐ x) + dx⟩⟩

We refer to x as a field because it does not use the self variable.

2.2 Message Send

Sending a message mi to an object containing such a method is modeled by extracting the corresponding method body ei from the object and applying it to the object itself:

⟨m1 = e1, …, mk = ek⟩ ⇐ mi ⟶^{eval} ei ⟨m1 = e1, …, mk = ek⟩

For example, sending the message move with a displacement of 2 to p, we get:

                 p ⇐ move2 = (λself. λdx.⟨ . . . ⟩) p 2

= ⟨p ← x = λs.(p ⇐ x) + 2⟩
= ⟨p ← x = λs. 3 + 2⟩

                          = ⟨p ← x = λself. 5⟩

Using a sound rule for object equality,

⟨⟨m1=e1, …, mk=ek⟩ ← mi=ei^{′}⟩ = ⟨m1=e1, …, mi=ei^{′}, …, mk=ek⟩

we may reach the conclusion

                p ⇐ move2 = ⟨ x = λself. 5,

move = λself. λdx.⟨…⟩⟩

showing that the result of sending a move message with an integer parameter is an object identical to p, but with an updated x-coordinate.

2.3 Inheritance

The inheritance mechanism of this calculus is very simple, although its typing is somewhat complex. To define colored points from points, we simply need to add a color method to our point object p.

                 cp =^{def} ⟨p ←+ myColor = λself. blue⟩

If we send the move message to cp with the same parameter, we may calculate the resulting object in exactly the same way as before:

                cp ⇐ move2 = (λself. λdx.⟨ . . . ⟩) cp 2

= ⟨cp ← x = λs.(cp ⇐ x) + 2⟩
= …

                          = ⟨cp ← x = λself. 5⟩

with the final conclusion that

                cp ⇐ move2 = ⟨ x = λself. 5,

move = λself. λdx.⟨…⟩,

                              myColor = λself. blue

⟩

The important feature of this computation is that the color of the resulting colored point is the same as the original one. While move was defined originally for points, the method body performs the correct computation when the method is inherited by an object with additional methods. Hence we have method specialization in the calculus.

2.4 Operational semantics

In defining the operational semantics for our calculus, we must give rules for extracting and applying the appropriate method of an object. A natural way to approach this would be to use a permutation rule

⟨⟨e1 ←∘ n=e2⟩ ←∘ m=e3⟩ = ⟨⟨e1 ←∘ m=e3⟩ ←∘ n=e2⟩

where m and n are distinct and each occurrence of ←∘ may be either ←+ or ←. This equational rule would let us treat objects as sets of methods, rather than ordered sequences. However, this rule would cause typing complications, since our typing rules only allow us to type object expressions when methods are added in an appropriate order. In particular, if we permute the methods of the object expression

⟨⟨⟨⟩ ←+ x = λself. 3⟩

                    ←+ x succ = λself.(self ⇐ x) + 1⟩

then the subexpression

                ⟨⟨⟩ ←+ x succ = λself.(self ⇐ x) + 1⟩

is not well-typed. Therefore, the entire expression cannot be typed.

We circumvent the problem of method order by using a more complicated “standard form” for object expressions, namely,

⟨⟨⟨m1=e1, … mk=ek⟩ ← m1=e1^{′}⟩ … ← mk=ek^{′}⟩

where each method is defined exactly once, using some arbitrary method body that does not contribute to the observable behavior of the object, and then redefined exactly once by giving the desired method body. Even if the two definitions of a method are the same, this form is useful since it allows us to permute the list of method redefinitions arbitrarily. More formally, in addition to the ⟶^{eval} relation that allows us to evaluate message sends and function applications, the operational semantics includes a subsidiary “bookkeeping” relation ⟶^{book}, which allows each object to be transformed into the “standard form” indicated above. The relation ⟶^{book} is the congruence closure of the first four clauses listed in Table 1. These rules also allow the method redefinitions to be permuted arbitrarily. An important property of ⟶^{book}, proved in Section 5, is that if e ⟶^{book} e′, then any type for e is also derivable for e′. This property would fail if we had the more general permutation rule discussed above.

(switch ext ov) ⟨⟨e1 ← n=e2⟩ ←+ m=e3⟩ ⟶^{book} ⟨⟨e1 ←+ m=e3⟩ ← n=e2⟩
(perm ov ov)  ⟨⟨e1 ← m=e2⟩ ← n=e3⟩ ⟶^{book} ⟨⟨e1 ← n=e3⟩ ← m=e2⟩
(add ov)  ⟨e1 ←+ m=e3⟩  ⟶^{book} ⟨⟨e1 ←+ m=e3⟩ ← m=e3⟩
(cancel ov ov) ⟨⟨e1 ← m=e2⟩ ← m=e3⟩ ⟶^{book} ⟨e1 ← m=e3⟩
(β)  (λx. e1)e2             ⟶^{eval} [e2/x]e1
(⇐)  ⟨e1 ←∘ m=e2⟩ ⇐ m      ⟶^{eval} e2⟨e1 ←∘ m=e2⟩

where ←∘ may either ←+ or ←.

Table 1. Bookkeeping and evaluation rules.

3 Static Type System

3.1 Subtyping and delegation

In general, there are two forms of subtyping that are applicable to object types: width and depth subtyping. If one object type provides all of the methods of another, with the same types, then every object of the first type should be safely substitutable in any context expecting an object with the second type. We call this form of subtyping width subtyping. It is also generally possible for one object type to restrict the type of one or more of its methods to a subtype. Again, any object with the more restricted type should be safely substitutable in any context expecting an object with the less restricted type. We call this form of subtyping depth subtyping.

As explained in [FM94], pure-delegation based languages, such as that described in [FHM94], do not permit either form of object subtyping. Consider the intuitive definition of a subtype: A is a subtype of B if we may use an object of type A in any context expecting an object of type B. If objects of type A are to be used as B’s, then A-objects must have all of the methods of B-objects. Because method addition is a legal operation on objects in delegation-based languages, objects with extra methods cannot be used in some contexts where an object with fewer methods may. As an example, a colored point object cannot be used in a context that will add color, but a point object can. For A to be a subtype of B then, A’s must contain exactly the same methods as B’s. Hence we do not get width subtyping.

We do not get depth subtyping either, as depth subtyping is unsound in the presence of method override. The following example, given in [AC94] illustrate the problem. Consider the object types A and B:

B =^{def} pro t ⟨⟨x : Int, y : Real⟩⟩

                   A =^{def} pro t ⟨⟨x : PosInt, y : Real⟩⟩

If we allow deep record/object subtyping, A <: B since PosInt <: Int. Now consider an object a defined as follows:

a =^{def}⟨x = 1, y = ln(self ⇐ x)⟩

We can see that a has type A. By the subsumption rule, we may consider a to have type B. With this typing, the expression ⟨a ← x = −1⟩ is legal. But then sending the message y to a produces a run-time type error.

In the remainder of this section, we give a type system for the object calculus described in Section 2 that is an extension of the one given in [FHM94]. The major change to the earlier system is the addition of obj types, which permit subtyping in both width and depth. In both the earlier system and the one we describe here, expressions with pro type (called class type in [FHM94]) may have new methods added via method addition (←+) and old methods replaced via method override(←). As described above, only trivial subtyping is sound for such types. In the system presented here, we may decide that we are no longer interested in modifying the methods of an expression with pro type. At this point, we may “seal” the expression by converting it to a value with an obj type. Since ← and ←+ are not valid operations on obj types, width and depth subtyping are sound for these types. We call expressions given pro type prototypes because they may either be sent messages or modified to create new kinds of prototypes. Expressions with obj type are called objects since such expressions may be sent messages or subtyped, but not extended or modified. In the following, we will use the meta-variable probj to denote either obj or pro.

3.2 The Type System

The type defined by the type expression

probj t ⟨⟨m1 : τ1, …, mk : τk⟩⟩

is a type t with the property that when we send the message mi for 1 ≤ i ≤ k to any element x of this type, the result has type τi . A significant aspect of this type is that the bound type variable t may appear in the types τ1, …, τk . Thus, when we say x ⇐ mi will have type τi , we mean type τi with any free occurrences of t in τi referring to the type probj t ⟨⟨m1 : τ1, …, mk : τk⟩⟩ itself. Thus, probj t ⟨⟨…⟩⟩ is a special form of recursively-defined type.

The typing rule for message send has the form

\frac{e : probj t ⟨⟨ … m : τ⟩⟩}{e ⇐ m : [probj t ⟨⟨ … m : τ⟩⟩/t]τ}

where the substitution for t in τ reflects the recursive nature of object types. This rule may be used in its pro form to give the point p with x and move methods type

                    pro t ⟨⟨ x : Int, move : Int → t⟩⟩

since p ⇐ x returns an integer and p ⇐ moven has the same type as p.

A subtle but very important aspect of the type system is that when an object is extended with an additional method, the syntactic type of each method does not change. For example, when we extended p with a color to obtain cp, we obtain an object with type

             pro t ⟨⟨ x : Int, move : Int → t, myColor : Color⟩⟩

The important change to notice here is that although the syntactic type of move is still Int → t, the meaning of the variable t has changed. Instead of referring to the type of p as it did originally, it now refers to the type of cp. This behavior is the method specialization discussed briefly in Section 1. For this kind of reinterpretation of type variables to be sound, the typing rules for object extension and object override must insure that every possible type for a new method will be correct. This check is done through a form of implicit higher-order polymorphism, which is explained more fully in [FHM94].

3.3 Adding subtyping

To insure that subtyping is sound for obj expressions, we disable object extension and object override on them, permitting them only to receive messages. Since the methods handling such messages are defined when the expression has a pro type, however, it is possible for these methods to redefine themselves or other methods of the host expression. (The polymorphism requirement for method bodies prevents them from adding new methods.) These redefinitions do not cause an unsoundness in the type system, however, because they were type-checked with precise knowledge of the pro type of the expression to which they were added. The unsoundness discussed above arises when the type of an expression is promoted via subsumption and then a method is replaced by another method with higher type. This scenario cannot occur in our system because once we seal an expression to a potentially imprecise obj type, methods cannot be overridden from the outside, where only the imprecise sealed type is available. Internal methods, type-checked with precise pro type information about the expression to which they were added, are type-safe.

Since sealing a prototype e requires no change to e, we would have liked to be able to use the following rule in conjunction with a subsumption rule to “seal” prototypes:

(seal-unsound)  \frac{Γ ⊢ obj t R : T}{Γ ⊢ pro t R <: obj t R}

where the judgement Γ ⊢ obj t R : T denotes that type obj t R is well formed. Unfortunately, this rule is unsound when the variable t appears contravariantly (or invariantly) in R. Hence we need a more complicated rule that has the same form as the rule for deriving subtyping judgements on obj types. Because of this similarity, we may combine the sealing rule and the obj subtyping rule to produce:

(<: object) \frac{Γ ⊢ probj s_{1} ⟨⟨\overrightarrow{m}: \overrightarrow{τ}, \overrightarrow{n}: \overrightarrow{σ}⟩⟩ : T Γ ⊢ obj s_{2} ⟨⟨\overrightarrow{m}: \overrightarrow{τ}′⟩⟩ : T Γ, s_{1} <: s_{2} ⊢ τ_{i} <: τ′_{i} s_{1} ∉ F V (τ′_{i}), s_{2} ∉ F V (τ_{i})}{Γ ⊢ probj s_{1} ⟨⟨\overrightarrow{m}: \overrightarrow{τ}, \overrightarrow{n}: \overrightarrow{σ}⟩⟩ <: obj s_{2} ⟨⟨\overrightarrow{m}: \overrightarrow{τ}′⟩⟩}

The meta-variable probj is pro when this rule is used to seal prototypes. When used simply for subtyping between object types, probj is obj. Notice that this rule gives us subtyping in both width and depth for obj types. This rule has the somewhat unfortunate consequence that we cannot seal prototypes to obj types containing methods that are contravariant (or invariant) in the bound type variable. However, this appears to be a fundamental trade-off and limitation.

The other rules in the type system are either routine or the same as those in [FHM94]. A complete list of the typing rules appears in Appendix A.

3.4 Rows, types, and kinds

More formally, the type expressions are given by:

Types

τ : : = t |s | τ_{1} → τ_{2} | pro t R | obj t R

Rows

R : : = r | ⟨⟨⟩⟩ | ⟨⟨R | m: τ⟩⟩ | λt. R | Rτ

Kinds

kind : : = T | κ
κ : : = T^{n} →[m_{1}, …, m_{k}]

The row expressions, which are essentially lists of method names and associated types, appear as subexpressions of type expressions. Types and rows are distinguished by kinds. As a notational simplification, we write [m_{1}, …, m_{k}] for T^{0} →[m_{1}, …, m_{k}] . Intuitively, the elements of kind [m_{1}, …, m_{k}] are rows that do not include method names m_{1}, …, m_{k}. The reason we must know statically that some method does not appear is to guarantee that methods are not multiply defined. Kinds of the form T^{n} →[m_{1}, …, m_{k}], for n ≥ 1, are used to infer a form of higher-order polymorphism of method bodies.

The environments, or contexts, of the system list term, type, and row variables.

Γ : : = ϵ | Γ , x: τ | Γ , t: T | Γ , r: κ | Γ , s_{1} <: s_{2}

Note that contexts are ordered lists, not sets.

The judgement forms are standard:

Γ ⊢ ∗  well-formed context
Γ ⊢ e: τ  term has type
Γ ⊢ τ : T  well-formed type
Γ ⊢ R: κ  row has kind
Γ ⊢ τ_{1} <: τ_{2} τ_{1} subtype of τ_{2}

4 Examples

To give some intuition for this calculus, we present two examples, neither of which is typable in the system of [FHM94]. Other examples, demonstrating the expressivity of the system, appear in [FHM94]. The first example below illustrates the use of subtyping for code reuse, while the second demonstrates its use for encapsulation.

4.1 Subtyping for code reuse

Consider the function

              average =^{def} λp1. λp2.((p1 ⇐ x) + (p2 ⇐ x))/2

We may give this expression type:

           average : obj t ⟨⟨x : int⟩⟩ → obj t ⟨⟨x : int⟩⟩ → int

(assuming integer division). Now consider the following two expressions:

p  =^{def} ⟨ x = λself. 3,

              move = λself. λdx. ⟨self ← x = λs.(self ⇐ x) + dx⟩⟩

       cp =^{def} ⟨ p ←+ c = λself. red ⟩

As in the system in [FHM94], we may give p and cp the following types:

              p : pro t ⟨⟨ x : int, move : int → t⟩⟩
             cp : pro t ⟨⟨ x : int, move : int → t, c : colors⟩⟩

In the new system, we may seal these expressions and give them both the following common supertype:

p, cp : obj t ⟨⟨x : int⟩⟩

Hence we may give the expression average p cp type int, allowing us to use the function average to calculate the average of colored points and points interchangeably.

4.2 Subtyping for encapsulation

Once we change the type of an expression from pro type to obj type, the methods of that prototype become “read-only”, including those methods that are effectively data fields. Hence if the designers of a prototype wish its users to be able to change the values of some of its methods after it is sealed, they must provide methods to change those values. This restriction provides a mechanism whereby prototype designers can guarantee invariants for the objects created from their prototypes.

Suppose, for example, we were interested in colored points whose color was guaranteed to be either blue or green. Then consider the expression:

cp2 =^{def} ⟨ x = …,

move = …,

                    c = λself. blue,
                    makeBlue = λself.⟨self ← c = blue⟩,
                    makeGreen = λself.⟨self ← c = green⟩,

⟩

As in the original system, we may give this expression type:

 cp2 : pro t ⟨⟨ x : int, move : int → t, c : colors, makeBlue : t, makeGreen : t⟩⟩

With this type, the user may override cp2 ’s c method to give cp2 any color. However, we may prevent this undesired change by sealing cp2 . We may use the rule (<: object) and subsumption to give cp2 the type:

 cp2 : obj t ⟨⟨ x : int, move : int → t, c : colors, makeBlue : t, makeGreen : t⟩⟩

With this type, users may no longer set the color of cp2 by overridding its value for c. Now they may only change its color by sending the messages makeBlue and makeGreen, which guarantees that the object only takes on legal colors.

5 Soundness

We prove the soundness of our type system with respect to the operational semantics given in Section 2.4. We first prove that evaluation preserves type; this property is traditionally called subject reduction. We then show that no typable expression evaluates to error using the evaluation rules given in [FHM94]. This fact guarantees that we have no message-not-understood errors for expressions with either pro or obj types.

The proof begins with two lemmas about substitution for row and type variables. We then prove a normal form lemma that allows us to restrict our attention to derivations of a certain form, simplifying later proofs. Lemmas 4 and 5 give us subject reduction for the bookkeeping rules and β -reduction, respectively. Lemma 6 implies subject reduction for (⇐)-reduction on expressions with pro type, while Lemmas 7 and 8 give us subject reduction for (⇐)-reduction on expressions with obj type.

The following two substitution lemmas are used in conjunction with row variables to specialize pro types to contain additional methods.

Lemma 1. If Γ, u_{2} : V_{2}, Γ′ ⊢ U_{1} : V_{1} and Γ ⊢ U_{2} : V_{2} are both derivable, then so is Γ, [U_{2}/u_{2}]Γ′ ⊢ [U_{2}/u_{2}]U_{1} : V_{1} , where U_{1} : V_{1} and U_{2} : V_{2} are either both τ : T or both R: κ.

Lemma 2. If Γ, r: T^{n} →[m_{1}, …, m_{k}], Γ′ ⊢ e : τ and Γ ⊢ R : T^{n} →[m_{1}, …, m_{k}] are both derivable, then so is Γ, [R/r]Γ′ ⊢ e : [R/r]τ.

The type and row equality rules introduce many non-essential judgement derivations, which unnecessarily complicate derivation analysis. We therefore restrict our attention to ⊢_{N} -derivations, which we define as those derivations in which the only appearance of a type or row equality rule is as (rowβ) immediately following an occurrence of (row fn app). The τnf of a type or row expression is its normal form with respect to ordinary β -reduction. The τnf of a term expression e is just e. Since we are only interested in types and rows in τnf, the following lemma shows we can find a ⊢_{N} -derivation for any judgement of interest.

Lemma 3. If Γ ⊢ A is derivable, then so is τnf(Γ) ⊢_{N} τnf(A).

The proof of this lemma is by induction on the derivation of Γ ⊢ A. Occurrences of equality rules may be eliminated in the ⊢_{N} -derivation because two row or type expressions related via β -reduction must have the same τnf.

From this point on, we will only concern ourselves with contexts and type or row expressions that are in τnf. This limitation is not severe, since any term that has a type has a type in τnf. Future analyses of derivations will consider only ⊢_{N} -derivations, since its restriction on equality rules greatly simplifies the proofs.

The next three lemmas show that the various components of the ⟶^{eval} relation preserve expression types. Lemma 4 is the first of these, showing that the (⟶^{book}) relation has the necessary property.

Lemma 4. If Γ ⊢ e : τ is derivable, and e ⟶^{book} e′, then Γ ⊢ e′ : τ is derivable.

The proof of Lemma 4 consists of two parts: the first shows that a derivation from Γ ⊢ e : τ can only depend on the form of τ, not on the form of e. More formally, if Γ ⊢ C[e] : τ is derived from Γ′ ⊢ e : σ and Γ′ ⊢ e′ : σ is also derivable, then so is Γ ⊢ C[e′] : τ. This fact is easily seen by an inspection of the typing rules. The second part shows that if Γ ⊢ e : τ is derivable, and e ⟶^{book} e′ by e matching the left-hand side of one of the (⟶^{book}) axioms, then Γ ⊢ e′ : τ is also derivable. This fact follows from a case analysis of the four (⟶^{book}) axioms. Row variables and Lemma 2 are essential for the (switch ext ov) case.

The fact that (β)-reduction preserves expression types is an immediate consequence of the following lemma:

Lemma 5. If Γ, x : τ_{1}, Γ′ ⊢ e2 : τ_{2} and Γ ⊢ e1 : τ_{1} are both derivable, then so is Γ, Γ′ ⊢ [e1/x]e2 : τ_{2} .

Lemma 5 is proved by induction on the derivation of Γ, x : τ_{1}, Γ′ ⊢ e2 : τ_{2} . The following three lemmas are useful in showing that (⇐)-reduction pre-

serves expression types.

Lemma 6. If Γ ⊢ ⟨⟨e ←∘ m1=e1⟩ … ←∘ mk=ek⟩ : pro t ⟨⟨R | m_{1} :τ_{1}, …, m_{k}:τ_{k}⟩⟩ is derivable, where m_{1}, …, m_{k} are distinct and are precisely the method names that occur consecutively to the right of e, then Γ ⊢ ei : [pro t ⟨⟨R | m_{1} : τ_{1}, …, m_{k} : τ_{k}⟩⟩/t](t → τ_{i}). is also derivable.

The proof of this lemma also has two parts. Part A gives a derivable type for each object obtained by stripping off some number of the ←∘ operations. The appropriate derivation is obtained by induction on the number of ←∘ operations removed. Part B gives the required type for each of the ei ’s. Row variables and Lemma 2 are critical to its proof, which is an analysis of the derivation of the type of ⟨⟨e ←∘ m1=e1⟩ … ←∘ mi=ei⟩, given by part A.

The key insight in the soundness of the subtyping of the calculus is that if we derive that an expression ob =^{def} ⟨⟨e ←∘_{1} m_{1}=e_{1}⟩ … ←∘_{k} m_{k}=e_{k}⟩ has obj type, then a series of lemmas about typing derivations show that we must have derived that ob had a related pro type. Furthermore, the methods of ob must have been typed checked under the assumption that ob had that pro type. Hence any ← or ←+ operations in the methods of ob were type checked with full knowledge of ob’s most general form and are thus type-safe. Technically, we may state this insight as:

Lemma 7. If we may derive Γ ⊢ ob : τ, then there exists some type pro t ⟨⟨R | \overrightarrow{m} : \overrightarrow{τ}⟩⟩ such that we may derive in no more steps Γ ⊢ ob : pro t ⟨⟨R | \overrightarrow{m} : \overrightarrow{τ}⟩⟩ and also Γ ⊢ pro t ⟨⟨R | \overrightarrow{m} : \overrightarrow{τ}⟩⟩ <: τ, where \overrightarrow{m} : \overrightarrow{τ} is shorthand for m_{1} : τ_{1}, …, m_{k} : τ_{k}.

To prove subject reduction for the operational semantics, we need to show that each of the basic evaluation rules preserves type. For the (⇐)-reduction rule, this corresponds to showing that if we may derive Γ ⊢ ⟨e1 ←∘ m = e2⟩ ⇐ m : τ then we may also derive Γ ⊢ e2⟨e1 ←∘ m = e2⟩ : τ. This fact is proved by induction on the derivation of Γ ⊢ ⟨e1 ←∘ m = e2⟩ ⇐ m : τ. The following lemma is important for the (object meth app) case of this proof:

Lemma 8. If Γ ⊢ probj s_{1} ⟨⟨R_{1} | m : τ_{1}⟩⟩ <: probj s_{2} ⟨⟨R_{2} | m : τ_{2}⟩⟩, is derivable, then Γ ⊢ [probj s_{1} ⟨⟨R_{1} | m : τ_{1}⟩⟩/s_{1}]τ_{1} <: [probj s_{2} ⟨⟨R_{2} | m : τ_{2}⟩⟩/s_{2}]τ_{2} is also derivable.

Theorem 9 Subject Reduction. If Γ ⊢ e : τ is derivable, and e ⟶^{eval} e′, then Γ ⊢ e′ : τ is also derivable.

The proof is similar in outline to that of Lemma 4; it reduces to showing that each of the basic evaluation steps preserves the type of the expression being reduced. The (⟶^{book}) case follows from Lemma 4, the (β) case from Lemma 5 and the (⇐) case from Lemmas 6, 7, and 8.

Theorem 10 Type Soundness. If the judgement ϵ ⊢ e : τ is derivable, then eval(e) ≠ error, where the function eval is as in [FHM94].

6 Related work

The authors of [BL95] approach the trade-off between delegation and subtyping in a very different way. Their system, which is an extension of [FHM94], permits a limited form of width subtyping on expressions with (what we call) pro type. In particular, they consider pro t R a subtype of pro t R′ so long as R contains all the methods of R′ (with matching types) and none of the “forgotten” methods are referred to in the methods listed in R′. This second condition guarantees that if we forget about the presence of some method m via subsumption and then re-add m with a potentially unrelated type, we cannot violate any typing assumptions the other methods of the object may have made about m. This guarantee is essential to the soundness of this approach to adding subtyping; however, its inability to “forget” methods referred to by “remembered” methods is somewhat unfortunate. In particular, it cannot type examples such as that given in Section 4.2, where desired invariants about an object are maintained by restricting access to certain methods via subsumption.

7 Conclusion

In this paper, we present a type system for an object calculus that extends previous work in [Mit90, FHM94]. The main additions to our previous object calculus are the distinction between prototypes and objects and the addition of subtyping. The distinction between prototypes, which allow method addition and override, and objects, which only receive messages, is essential for subtyping, since previous studies show an incompatibility between object extension, method override, and non-trivial subtyping [FM94]. We have devised a type soundness proof for our calculus of prototypes, objects, and subtyping based on a straightforward operational semantics.

References

[AC94] M. Abadi and L. Cardelli. A theory of primitive objects: untyped and firstorder systems. In Proc. Theor. Aspects of Computer Software, pages 296–320. Springer-Verlag LNCS 789, 1994.

[AC95] M. Abadi and L. Cardelli. An imperative object calculus: Basic typing and soundness. In SIPL ’95 - Proc. Second ACM SIGPLAN Workshop on State in Programming Languages. Technical Report UIUCDCS-R-95-1900, Department of Computer Science, University of Illinois at Urbana-Champaign, 1995.

[BL95] V. Bono and L. Liquori. A subtyping for the fisher-honsell-mitchell lambda calculus of objects. Berlin, June 1995. Springer LNCS 933. To appear.

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

[Bv93] K. Bruce and R. van Gent. TOIL: a new type-safe object-oriented imperative language. Manuscript, 1993.

[CU89] C. Chambers and D. Ungar. Customization: Optimizing compiler technology for Self, a dynamically-typed object-oriented programming language. In SIGPLAN ’89 Conf. on Programming Language Design and Implementation, pages 146–160, 1989.

[ES90] M. Ellis and B. Stroustrop. The Annotated C^{++} Reference Manual. Addison-Wesley, 1990.

[FHM94] K. Fisher, F. Honsell, and J.C. Mitchell. A lambda calculus of objects and method specialization. Nordic J. Computing (formerly BIT), 1:3–37, 1994. Preliminary version appeared in Proc. IEEE Symp. on Logic in Computer Science, 1993, 26–38.

[FM94] K. Fisher and J.C. Mitchell. Notes on typed object-oriented programming. In Proc. Theoretical Aspects of Computer Software, pages 844–885. Springer LNCS 789, 1994.

[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. Draft report; available electronically, June 1993.

[PT94] Benjamin C. Pierce and David N. Turner. Simple type-theoretic foundations for object-oriented programming. Journal of Functional Programming, 4(2):207–248, 1994.

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

[US91] D. Ungar and R.B. Smith. Self: The power of simplicity. Lisp and Symbolic Computation, 4(3):187–206, 1991. Preliminary version appeared in Proc. ACM Symp. on Object-Oriented Programming: Systems, Languages, and Applications, 1987, 227-241.

A Type System

Types τ : : = t |s | τ_{1} → τ_{2} | pro t R | obj t R

Rows R : : = r | ⟨⟨⟩⟩ | ⟨⟨R | m: τ⟩⟩ | λt. R | Rτ

Kinds kind : : = T | κ κ : : = T^{n} →[m_{1}, …, m_{k}]

Contexts:

Γ : : = ϵ | Γ , x: τ | Γ , t: T | Γ , r: κ | Γ , s_{1} <: s_{2}

The judgement forms are standard:

Γ ⊢ ∗  well-formed context
Γ ⊢ e: τ  term has type
Γ ⊢ τ : T  well-formed type
Γ ⊢ τ_{1} <: τ_{2} τ_{1} subtype of τ_{2}
Γ ⊢ R: κ  row has kind

A.1 Typing rules

General Rules

(start)  \overline{ϵ ⊢ ∗}

(projection)  \frac{\begin{matrix}Γ ⊢ ∗ \\ u : v ∈ Γ \end{matrix}}{Γ ⊢ u : v}

(weakening)  \frac{\begin{matrix}Γ ⊢ A \\ Γ, Γ′ & ⊢ & ∗ \end{matrix}}{Γ, Γ′ ⊢ A}

Rules for type expressions

(type var)  \frac{\begin{matrix}Γ ⊢ ∗ \\ t ∉ dom(Γ) \end{matrix}}{Γ , t : T ⊢ ∗}

(type arrow)  \frac{\begin{matrix}Γ ⊢ τ_{1} : T \\ Γ ⊢ τ_{2} : T \end{matrix}}{Γ ⊢ τ_{1} → τ_{2} : T}

(type pro)  \frac{Γ, t: T ⊢ R : [m_{1}, …, m_{k}]}{Γ ⊢ pro t R : T}

Type and Row Equality

Type or row expressions that differ only in names of bound variables or order of label : type pairs are considered identical. In other words, we consider α-conversion of type variables bound by λ, pro , or obj and applications of the principle

⟨⟨⟨⟨R | n : τ_{1}⟩⟩ | m : τ_{2}⟩⟩ = ⟨⟨⟨⟨R | m : τ_{2}⟩⟩ | n : τ_{1}⟩⟩

within type or row expressions to be conventions of syntax, rather than explicit rules of the system. Additional equations between types and rows arise as a result of β -reduction, written →_{β}, or β -conversion, written ↔_{β}.

(row β)  \frac{Γ ⊢ R : κ, R →_{β} R′}{Γ ⊢ R′ : κ}

(type β)  \frac{Γ ⊢ τ : T , τ →_{β} τ′}{Γ ⊢ τ′ : T}

(type eq)  \frac{Γ ⊢ e : τ, τ ↔_{β} τ′, Γ ⊢ τ′ : T}{Γ ⊢ e : τ′}

Rules for rows

(empty row)  \frac{Γ ⊢ ∗}{Γ ⊢ ⟨⟨⟩⟩ : [m_{1}, …, m_{k}]}

(row var)  \frac{\begin{matrix}Γ ⊢ ∗ \\ r ∉ dom(Γ) \end{matrix}}{Γ, r : T^{n} →[m_{1}, …, m_{k}] ⊢ ∗}

(row label)  \frac{\begin{matrix}Γ ⊢ R : T^{n} →[m_{1}, …, m_{k}] \\ \{n_{1}, …, n_{ℓ}\} ⊆ \{m_{1}, …, m_{k}\} \end{matrix}}{Γ ⊢ R : T^{n} →[n_{1}, …, n_{ℓ}]}

(row ext)  \frac{\begin{matrix}Γ ⊢ R : [m, m_{1}, …, m_{k}] \\ Γ ⊢ τ : T \end{matrix}}{Γ ⊢ ⟨⟨R | m: τ⟩⟩ : [m_{1}, …, m_{k}]}

(row fn abs)  \frac{Γ, t: T ⊢ R : T^{n} →[m_{1}, …, m_{k}]}{Γ ⊢ λt. R : T^{n+1} →[m_{1}, …, m_{k}]}

(row fn app)  \frac{\begin{matrix}Γ ⊢ R : T^{n+1} →[m_{1}, …, m_{k}] \\ Γ ⊢ τ : T \end{matrix}}{Γ ⊢ Rτ : T^{n} →[m_{1}, …, m_{k}]}

Rules for assigning types to terms

(exp var)  \frac{\begin{matrix}Γ ⊢ τ : T \\ x ∉ dom(Γ) \end{matrix}}{Γ, x: τ ⊢ ∗}

(exp abs)  \frac{Γ , x: τ_{1} ⊢ e : τ_{2}}{Γ ⊢ λx. e : τ_{1} → τ_{2}}

(exp app)  \frac{Γ ⊢ e_{1} : τ_{1} → τ_{2} Γ ⊢ e_{2} : τ_{1}}{Γ ⊢ e_{1} e_{2} : τ_{2}}

(empty object)  \frac{Γ ⊢ ∗}{Γ ⊢ ⟨⟩ : pro t ⟨⟨⟩⟩}

(pro meth app)  \frac{Γ ⊢ e : pro t ⟨⟨R | m: τ⟩⟩}{Γ ⊢ e ⇐ m : [pro t ⟨⟨R | m: τ⟩⟩/t]τ}

(obj ext) \frac{Γ ⊢ e_{1} : pro t ⟨⟨R | m_{1} : τ_{1}, …, m_{k} : τ_{k}⟩⟩ Γ, t: T ⊢ R : [m_{1}, …, m_{k}, n] Γ, r : T → [m_{1}, …, m_{k}, n] ⊢ e_{2} : [pro t ⟨⟨rt | \overrightarrow{m}: \overrightarrow{τ}, n: τ⟩⟩/t](t → τ)  r not in τ}{Γ ⊢ ⟨e_{1} ←+ n=e_{2}⟩ : pro t ⟨⟨R | \overrightarrow{m}: \overrightarrow{τ}, n: τ⟩⟩}

(obj over)  \frac{\begin{matrix}Γ ⊢ e_{1} : pro t ⟨⟨R | m_{1} : τ_{1}, …, m_{k} : τ_{k}⟩⟩ \\ Γ , r : T → [m_{1}, …, m_{k}] ⊢ \\ e_{2} : [pro t ⟨⟨rt | \overrightarrow{m}: \overrightarrow{τ}⟩⟩/t](t → τ_{i}) \end{matrix}}{Γ ⊢ ⟨e_{1} ← m_{i}=e_{2}⟩ : pro t ⟨⟨R | \overrightarrow{m}: \overrightarrow{τ}⟩⟩}

Here \overrightarrow{m}: \overrightarrow{τ} is used as an abbreviation for m_{1} : τ_{1}, …, m_{k} : τ_{k}. A.2 New Rules

(type object)  \frac{Γ, t: T ⊢ R : [m_{1}, …, m_{k}]}{Γ ⊢ obj t R : T}
(<: var)  \frac{\begin{matrix}Γ ⊢ ∗ \\ s_{1}, s_{2} ∉ dom(Γ) \\ s_{1} ≠ s_{2} \end{matrix}}{Γ, s_{1} <: s_{2} ⊢ ∗}
(<: proj)  \frac{\begin{matrix}Γ ⊢ ∗ \\ s_{1} <: s_{2} ∈ Γ \end{matrix}}{Γ ⊢ s_{1} <: s_{2}}
(<: var proj)  \frac{\begin{matrix}Γ ⊢ ∗ \\ s_{1} <: s_{2} ∈ Γ \end{matrix}}{Γ ⊢ s_{i} : T}
(<: refl)  \frac{Γ ⊢ τ : T}{Γ ⊢ τ <: τ}

(<: trans)  \frac{\begin{matrix}Γ ⊢ σ <: τ \\ Γ ⊢ τ <: ρ \end{matrix}}{Γ ⊢ σ <: ρ}

(<: arrow)  \frac{Γ ⊢ τ_{1} <: σ_{1} Γ ⊢ σ_{2} <: τ_{1}}{Γ ⊢ σ_{1} → σ_{2} <: τ_{1} → τ_{2}}

(<: object) \frac{Γ ⊢ probj s_{1} ⟨⟨\overrightarrow{m}: \overrightarrow{τ}, \overrightarrow{n}: \overrightarrow{σ}⟩⟩ : T Γ ⊢ obj s_{2} ⟨⟨\overrightarrow{m}: \overrightarrow{τ}′⟩⟩ : T Γ, s_{1} <: s_{2} ⊢ τ_{i} <: τ′_{i} s_{1} ∉ F V (τ′_{i}), s_{2} ∉ F V (τ_{i})}{Γ ⊢ probj s_{1} ⟨⟨\overrightarrow{m}: \overrightarrow{τ}, \overrightarrow{n}: \overrightarrow{σ}⟩⟩ <: obj s_{2} ⟨⟨\overrightarrow{m}: \overrightarrow{τ}′⟩⟩}

(subsumption)  \frac{\begin{matrix}Γ ⊢ σ <: τ \\ Γ ⊢ e : σ \end{matrix}}{Γ ⊢ e : τ}

(object meth app) \frac{Γ ⊢ e : obj t ⟨⟨R | m: τ⟩⟩}{Γ ⊢ e ⇐ m : [obj t ⟨⟨R | m: τ⟩⟩/t]τ}

This article was processed using the LaTEX macro package with LLNCS style