A lambda calculus of objects and method specialization

John C. Mitchell ^{∗} Computer Science Dept.

Stanford University

jcm@cs.stanford.edu

Furio Honsell ^{†} Dipartimento di Informatica

Universitá di Udine

honsell@uduniv.cineca.it

Kathleen Fisher ^{‡} Computer Science Dept. Stanford University

                    kfisher@cs.stanford.edu

Abstract

This paper presents an untyped lambda calculus, extended with object primitives that reflect 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. Type soundness, in the form of a “subject-reduction” theorem, is proved and examples illustrating the expressiveness of the pure calculus are presented.

1 Introduction

There are several forms of object-oriented languages. One of the major lines of difference is between classbased languages, such as Smalltalk [GR83] and C^{++} [ES90], where each object is created by a class and inheritance is determined by the class, and delegationbased languages such as Self [US87, CU89], where an object may be created from another object, inheriting properties of the original object. In this paper, we use an untyped lambda calculus of objects with a functional form of delegation as a tool for studying typing issues in object-oriented programming languages. Our main interests lie in (i) understanding how the functionality of a method may change as it is inherited, intuitively due to reinterpretation of the special symbol self (or this in C^{++} ), and (ii) setting the stage for equational reasoning about method bodies, apart from the particular context in which they first occur. The second goal seems a necessary precurser to understanding the effects of optimization or program transformations on method bodies or inheritance hierarchies. The main reason for using a delegation based language in this study is its relative simplicity, when compared with class-based languages.

Our main operations on objects are to send a message m to an object e, written e ⇐ m, and two forms of method definition. If expression e denotes an object without method m, then ⟨e ←+ m = e′⟩ denotes an object obtained from e by adding the method body e′ for m. When ⟨e ←+ m = e′⟩ is sent the message m, the result is obtained by applying e′ to ⟨e ←+ m = e′⟩. This form of “self-application” allows us to model the special symbol self of object-oriented languages directly by lambda abstraction. Intuitively, the method body e′ must be a function, and the first actual parameter of e′ will always be the “object itself.” To reinforce this intuition, we often write method bodies in the form λself.(…). The final method operation on objects is to replace one method body by another. This provides a functional form of update. As in the language Self, we do not distinguish instance variables from methods, since this does not seem essential. The untyped lambda calculus we use bears a strong resemblance to the T object system [RA82, AR88] (although it was originally developed without prior knowledge of T) and the untyped part of the calculus used in [Aba93] to model a fragment of Modula 3 [CDG^{+} 88, CDJ^{+} 89].

The main goal of this paper is to develop a type system that allows methods to be specialized appropriately as they are inherited. This is illustrated in the motivating examples given in the next section. Briefly, suppose p is a point object, with x, y methods returning the integer x- and y -coordinates of p, and a move method, with type int × int → point. The reason why move has this type is that if we send the message move to p, then we obtain a function which, given distances to move in the x and y directions, returns a point identical to p, but with new x, y -coordinates. If we create a colored point cp from p by the object extension operation, then cp inherits the x, y and move methods from p. In an untyped object-oriented language such as Smalltalk, the inherited move method will change the position of a colored point, leaving the color unchanged. Therefore, in a typed language, we want the move method of cp to have the “specialized” type int × int → colored point. Otherwise, if the inherited method has its original type, int × int → point, then whenever we move a colored point, we will obtain an ordinary point without color, making the inherited move function largely useless. While an imperative version of move would bypass this difficulty by returning type unit (as it is called in ML, or void in C^{++} ), the same issue arises when we attempt to define a function that must return a value. The construct like Current in Eiffel [Mey92], analyzed in [Coo89], illustrates the value of specializing the type of a method in an imperative language. While C^{++} does not include such a construct, the widespread use of C^{++} is not counter-evidence to the usefulness of method specialization. In fact, it appears to be common for novice C^{++} programmers to attempt to specialize the types of methods in derived classes. More experienced C^{++} programmers appear to use “down casts” to approximate the effects described in this paper.

∗Supported in part by an NSF PYI Award, with matching funds from AT&T, Digital Equipment Corporation, the Powell Foundation and Xerox Corporation; and by the Wallace F. and Lucille M. Davis Faculty Scholarship.

†Supported in part by a CNR grant, and Mitchell’s funding at Stanford spring 1992.

‡Supported in part by an NSF Graduate Fellowship.

The phenomenon we are concerned with is called “method specialization” in [Mit90], which describes a calculus similar to the one used here. However, the earlier paper, whose main intent was to identify a problem rather than solve it, suffered from several shortcomings that are repaired here. Specifically, [Mit90] describes method specialization and explains its usefulness, but only presents a tentative type system by extending the already complicated record calculus of [CM91]. In addition, no analysis of the type system is given. In contrast, the current paper presents a calculus of objects alone, without recourse to record calculi (although we owe a substantial debt to previous studies of record calculi), simplifies the typing rules substantially, and proves a form of type soundness. In addition, we show that equality of typable terms is undecidable by showing how to encode numerals as objects and how to define all partial recursive function. Objects play an essential role here, since the function part of our calculus is simply typed, and therefore only sufficient to express total recursive functions.

2 Untyped objects and inheritance by delegation

2.1 Untyped calculus of objects

We extend the untyped lambda calculus with four object-related syntactic forms,

e :: = x | c | λx. e | e1e2 | ⟨⟩ | e ⇐ m
| ⟨e1 ←+ m=e2⟩ | ⟨e1 ← m=e2⟩

In this grammar, x may be any variable, c is a constant symbol (such as a “built-in” function), λx. e is a lambda abstraction (function expression) and e1e2 is function application. The object forms are described in tabular form for easy reference:

⟨⟩  the empty object
e ⇐ m  send message m to object e
⟨e1 ←+ m=e2⟩ extend object with new method

m having body e2

⟨e1 ← m=e2⟩ replace 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. The reason for distinguishing extension from method replacement is that these two operations will have different typing rules. 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. If we were not concerned with static typing, then we could use a single operation that adds a method to an object, replacing any method that had the same name.

2.2 Examples of objects, inheritance and method specialization

To provide some intuition for this calculus, we give a few short examples. The first shows how records may be encoded as objects, while the second and third illustrate method specialization. The latter examples may be regarded as the motivating examples for this paper; rather than try to define method specialization in the abstract, we attempt to convey the essential properties by the examples of points and colored points given below.

To simplify notation, we write ⟨m1 = e1, …, mk = ek⟩ for ⟨… ⟨⟨⟩ ←+ m1 = e1⟩ … ←+ mk = ek⟩, where m1, …, mk are distinct method names. We illustrate the computational behavior of objects in this section using a simplified evaluation rule that reflects the operational semantics defined precisely below,

⟨m1 = e1, . . . , mk = ek⟩ ⇐ mi

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

This allows us to evaluate a message send by retrieving the appropriate method body from the object and applying it to the entire object itself. Note that the relation ⟶^{eval} represents one evaluation step, not full evaluation of an expression.

Record with two components. The first example is a form of “point” object that has constant x, y - coordinates:

r =^{def} ⟨x = λself. 3, y = λself. 2⟩

If we send the message x to r, we may calculate the result by

r ⇐ x ⟶^{eval} (λself. 3) r ⟶^{eval} 3

where the second evaluation step is ordinary β - reduction from lambda calculus. This example may be generalized to show how any record may be represented as an object whose methods are constant functions.

One-dimensional point with move function. A more interesting object, which we will refer to again, is the following “point” object with an x-coordinate and move method. We could easily give a similar two-dimensional point with x, y -coordinates, but the one-dimensional case illustrates the same ideas more simply.

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

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

⟩

The move method, when applied to the object itself and a displacement dx, replaces the x method by one returning a coordinate incremented by dx. This is illustrated in the following example calculation, where we send the message move with parameter 2:

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 integer parameter, is an object identical to p, but with an updated x-coordinate.

Inherit move from point to colored point. Our third introductory example shows how x and move are inherited when a colored point is defined from p by adding a color method.

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

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.⟨…⟩,

                     color = λself. red

⟩

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, which only have an x-coordinate, the method body performs the correct computation when the method is inherited by a more complicated object with additional methods.

In many cases, it is also useful to redefine an inherited method to exhibit more specialized behavior. This may be accomplished in our calculus by a combination of inheritance and method redefinition. For example, if we want an object to change to a darker color when moved, we could first define colored points from points as above, obtaining a colored point with the right type of move function. Then, move could be redefined (without changing its type) to have the right behavior.

Mutually recursive methods. As a technical simplification, our system is formulated so that methods are added to an object one at a time. This leads us to formulate our typing rules in a manner that makes it difficult to write object expressions with mutually recursive functions. More specifically, the static type system will only allow a method body to be added if all the other methods it refers to are already available from the object. For example, we cannot type the object expression

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

which has a method referring to x, but does not have an x method. The reason this object expression is not typable is that if we send the message x plus1, the object will then send the message x to itself. But since the object does not have an x method, this is an error; it is precisely the error we aim to prevent with our type system. On the other hand, we may type the object expression

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

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

which is formed by first extending the empty object with an x method, then the x plus1 method that refers to x.

The typing restriction that no method may refer to a method that the object does not have is inconvenient if we wish to add mutually-recursive methods m and n to some object. However, there is a standard idiom for adding mutually recursive methods. Specifically, we first extend the object by giving some method body for m that has the correct type, but does not depend on n. Then, the object may be extended with the desired method body for n, referring to m. Finally, we replace the “dummy” method body for m with the desired method body referring to n. While this is a programming inconvenience, it is not a limitation in expressiveness. It therefore does not seem serious enough to merit complicating the typing rules in a way that alleviates the difficulty. In any “real” programming language based on our “kernel language”, we would expect there to be convenient syntactic sugar for simultaneously adding several, possibly mutually recursive, methods to an object.

2.3 Operational semantics

In defining the operational semantics of our calculus, we must give rules for extracting and applying the appropriate method of an object. A natural way to approach this is 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 would let us treat objects as sets of methods, rather than ordered sequences. However, this equational 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 plus1 = λself.(self ⇐ x) + 1⟩

then the subexpression

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

is not well-typed, as described in the previous section. Therefore, the entire expression cannot be typed.

We circumvent the problem of method order 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 “dummy” method body that does not contribute to the observable behavior of the object, and redefined exactly once by giving the desired method body. More formally, in addition to the ⟶^{eval} relation that allows us to evaluate object and function expressions, 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 3.5, is that if e ⟶^{book} e′, then any type for e is also derivable for e′. This would fail if we had the more general permutation rule discussed above.

The evaluation relation is the congruence closure of the union of ⟶^{book} and the two evaluation clauses, (β) and (⇐), at the bottom of Table 1. In other words, e ⟶^{eval} e′ if we may obtain e′ from e by applying a bookkeeping or basic evaluation step to one subterm.

3 Static type system

3.1 Class types and message send

The type of an object will be called a class type. This is in part a misuse of the word “class,” since classes in object-oriented languages generally determine the representations as well as the interfaces, or types, of objects. However, “class” seems the best standard term from object-oriented programming that suggests the type of an object.

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

The type defined by the type expression

class t ⟨⟨m_{1} : τ_{1}, …, m_{k} : τ_{k}⟩⟩

is a type t with the property that any element x of this type is an object such that for 1 ≤ i ≤ k, the result of x ⇐ m_{i} is a value of 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 ⇐ m_{i} will have type τ_{i}, we mean type τ_{i} with any free occurrences of t in τ_{i} referring to the type class t ⟨⟨m_{1}:τ_{1}, …, m_{k}:τ_{k}⟩⟩ itself. Thus, class t ⟨⟨ … ⟩⟩ is a special form of recursively-defined type.

The typing rule for message send has the form

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

where the substitution for t in τ reflects the recursive nature of class types. This rule may be used to give the point p with x and move methods considered in Section 2.2 type

class t ⟨⟨ x : int, move : int → t⟩⟩

since p ⇐ x returns an integer and p ⇐ move n 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 extend p with a color to obtain cp, also given in Section 2.2, we obtain an object with type

class t ⟨⟨ x : int, move : int → t, color : colors⟩⟩

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 is the effect that we have called method specialization – the type of a method may change when the method is inherited. For this kind of reinterpretation of type variables to be sound, the typing rule for object extension must insure that every possible type for a new method will be correct. This is done through a form of implicit higher-order polymorphism.

Another subtle aspect of the type system is that objects which behave identically when we send either any sequence of messages may have different types. This is because adding and redefining methods are also considered operations on objects. A simple example is given by the following two objects.

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

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

⟩

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

           move = λself. λdx. (p ⇐ movedx)

⟩

It is not hard to see that p and q return the same results for any sequence of message sends. (Either we send x, which clearly gives the same result for p or q, or we send the message move. But since q ⇐ move returns p ⇐ move, any sequence of subsequent messages will produce identical results.) However, p and q are not equivalent if we extend them with additional methods. The reason is that the first move method will preserve any additional methods added by object extension, but the second will not. This distinction shows up in the type system, where we can give p the first type below, give q the second, but it is unsound to give q the first type.

point  = class t ⟨⟨ x : int, move : int → t⟩⟩
q point = class t ⟨⟨ x : int, move : int → point⟩⟩

A similar situation arises in Smalltalk, for example, where it is possible to have two classes that generate equivalent objects, but behave differently when we inherit from them. In adapting our type system to Smalltalk, we might expect to distinguish two such classes by type. The reason is that we wish the type of a class to not only give information about the behavior of objects, but also about the types of methods when they are inherited by other classes.

3.2 Types, rows and kinds

The type expressions include type variables, function types and class types. It would not change the system in any substantial way to add type constants, but we will not need them in this paper.

Types τ : : = t | τ_{1} → τ_{2} | class t R

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

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

The row expressions appear as subexpressions of type expressions, with rows and types 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: κ

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

3.3 Typing rules

For the most part, the formulation of the type system is routine. The most novel rules are those associated with objects. These are listed in Table 2. The remaining rules are listed in tables at the end of the paper.

The empty object, ⟨⟩ has the object type class t ⟨⟨⟩⟩, as specified in rule (empty object). The empty object has no methods, and therefore cannot respond to any messages. However, this object can be extended with methods to obtain objects of other types.

The typing rule (meth app) for sending a message to an object has the form described in the last section. However, in the more precise rule listed in Table 2, the row occurring in the class type of the object may have any form, as long as the method name being used occurs explicitly. Type equality allows the order of method names to be permuted, as described in Table 6. Consequently, there is no loss of generality in assuming m is the last method listed in the type.

The most subtle and complicated rule of the system is the (obj ext) typing rule for adding methods to objects. In this rule, we assume e1 is a object of some class type, and that e1 does not include a method n, to be added. The final assumption is a typing for e2 , the expression to be used as the method body for n. The first thing to notice about the typing for e2 is that it contains a row variable, r, which is implicitly universally quantified. Because of this quantification, e2 will have the indicated type for any substitution of row expression R for r, provided R has the correct kind. (See Lemma 3.2 below.) This is essential, since it implies that e2 will have the required functionality for any possible future extension of ⟨e1 ←+ n = e2⟩. The second important property of the typing for e2 is that the type has the form t → τ, with a class type substituted for t. While t is hidden in the class type of ⟨e1 ←+ n = e2⟩, it is necessary in the hypothesis since sending the message n to ⟨e1 ←+ n = e2⟩ will result in the application of e2 to this object. To simplify notation, we will use m⃗:τ⃗ as an abbreviation for m_{1} : τ_{1}, …, m_{k} : τ_{k}.

The rule for redefining, or overriding, a method body has the same form, but is slightly simpler.

3.4 Example typing derivations

We claimed earlier that we should be able to prove the following two typings

p : class t ⟨⟨ x : int, move : int → t⟩⟩
q : class t ⟨⟨ x : int, move : int → point⟩⟩

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

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

(obj ext)  \frac{Γ ⊢ e_{1} : class 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} : [class t ⟨⟨rt | m⃗: τ⃗, n: τ⟩⟩/t](t → τ)  r not in τ}{Γ ⊢ ⟨e_{1} ←+ n=e_{2}⟩ : class t ⟨⟨R | m⃗: τ⃗, n: τ⟩⟩}

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

Here m⃗: τ⃗ is used as an abbreviation for m_{1} : τ_{1}, …, m_{k} : τ_{k}.

Table 2: Typing rules for object expressions

and argued that it is unsound to give q the first type. To illustrate the use of the typing rules, we prove the first of these in Table 3. The second is proved similarly. In addition, we can prove that the object expression

cp = ⟨p ←+ color = λself. red⟩

has type

class t ⟨⟨ x : int, move : int → t, color : colors⟩⟩

by similar means. These examples are intended to demonstrate that the system captures the desired form of method specialization.

3.5 Soundness of typing rules

We prove the soundness of the type system by showing that if e has a type and e → →^{eval} e′, then e′ has the same type. This fact, combined with the observation that erroneous expressions are untypable, guarantees type soundness.

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 3.4, 3.5, and 3.6 provide useful tools for proving the last three lemmas, which show that the (⟶^{book}), (β), and (⇐) components of the (⟶^{eval}) relation all preserve expression types.

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

Lemma 3.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 3.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]τ.

These two lemmas follow from two more detailed lemmas, which we omit.

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 Contexts

Γ_{1} = r : T → [x, move],

self : class t ⟨⟨rt | x : int, move : int → t⟩⟩, dx : int

Γ_{2} = Γ_{1}, r′ : T → [x, move],

p : class t ⟨⟨r′t | x : int, move : int → t⟩⟩

Derivation (assuming ϵ ⊢ ⟨x= λself. 3⟩ : class t ⟨⟨x : int⟩⟩)

Γ_{2} ⊢ (self ⇐ x) + dx : int
Γ_{2} − p ⊢ λp.(self ⇐ x) + dx : class t ⟨⟨r′t | x : int, move : int → t⟩⟩ → int
Γ_{1} ⊢ ⟨self ← x= λp.(self ⇐ x) + dx⟩ : class t ⟨⟨rt | x : int, move : int → t⟩⟩

        Γ_{1} − self − dx ⊢ λself. λdx.⟨self ← x= λp.(self ⇐ x) + dx⟩

: [class t ⟨⟨rt | x : int, move : int → t⟩⟩/t](t → int → t)

                    ϵ ⊢ ⟨⟨x= λself. 3⟩ ←+ move= λself. λdx.⟨self ← x= λp.(self ⇐ x) + dx⟩⟩

: class t ⟨⟨x : int, move : int → t⟩⟩

Table 3: Example typing derivation.

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.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 following technical lemma is useful because it allows contexts, which are in fact lists, to be treated more like sets.

Lemma 3.4 If Γ, Γ′ ⊢ A and Γ, y : Z, Γ′ ⊢ ∗ are both derivable, then so is Γ, y : Z, Γ′ ⊢ A, where y : Z can be r: κ, t: T, or x : τ.

The next two lemmas are used to build rows that may be substituted for row variables by the substitution lemmas above. This substitution allows class types to be specialized with additional methods.

Lemma 3.5

If Γ ⊢_{N} class t ⟨⟨R | m_{1} : τ_{1}, …, m_{k} : τ_{k}⟩⟩ : T is derivable, then so is Γ, t: T ⊢ R : [m_{1} … m_{k}].

The proof of Lemma 3.5 is by induction on the derivation to handle the (weakening) case. For (class), a subsidiary lemma that if Γ ⊢_{N} λt_{1}, …, t_{n}.⟨⟨R | m⃗: τ⃗⟩⟩ : T^{n} →[l⃗] is derivable, then so is Γ, t_{1} : T, …, t_{n} : T ⊢_{N} R : [m⃗, l⃗] is helpful.

Lemma 3.6 If Γ ⊢ e : τ is derivable, then so is Γ ⊢ τ : T.

This lemma is proved by induction on the derivation of Γ ⊢_{N} e : τ. The hardest case is (obj ext) since it adds a method to a class type. For this rule, a helpful subsidiary lemma is that Γ, t_{1} : T, …, t_{n} : T ⊢_{N} τ : T is derivable if Γ ⊢_{N} λt_{1}, …, t_{n}.⟨⟨R | m: τ⟩⟩ : T^{n} →[m_{1}, …, m_{k}] is. The next three lemmas show that the various components of the ⟶^{eval} relation preserve expression types. Lemma 3.7 is the first of these, showing that the (⟶^{book}) relation has the necessary property.

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

The proof of Lemma 3.7 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 Lemmas 3.2 and 3.6 are essential for the (switch ext ov) case.

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

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

The proof of Lemma 3.8 is by induction on the derivation of Γ, x : τ_{1}, Γ′ ⊢ e2 : τ_{2} . Several of the cases require a lemma of the form that if Γ, x : τ, Γ′ ⊢ A is derivable with x not in A, then so is Γ, Γ′ ⊢ A.

An immediate consequence of the next lemma is that (⇐)-reduction preserves expression types.

Lemma 3.9 If Γ ⊢ ⟨⟨e ←∘ m1=e1⟩ … ←∘ mk=ek⟩ : class 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 : [class t ⟨⟨R | m_{1} : τ_{1}, …, m_{k} : τ_{k}⟩⟩/t](t → τ_{i}). is 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 Lemmas 3.2 and 3.6 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.

Theorem 3.10 (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 3.7; 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 3.7, the (β) case from Lemma 3.8 and the (⇐) case from Lemma 3.9.

We define “faulty” expressions to be those of the form: ⟨… ⟨⟨⟩ ←∘ m1=e1⟩ … ←∘ mk=ek⟩ ⇐ n where n ∉ {m1, …, mk}. An easy induction on k shows that faulty expressions are not typable.

Theorem 3.11 (Type Soundness) If Γ ⊢ e : τ and e → →^{eval} e′, then e′ is not faulty.

This theorem follows immediately from Theorem 3.10 and the observation above.

4 Expressive power

Since the function part of our calculus is simply typed, every typable expression that does not contain object operations is strongly normalizing. It follows that using only function expressions, only a subset of the total recursive functions are representable. In contrast, we show that all partial recursive functions are representable in the calculus of functions and objects. Intuitively, this is because class types are a form of recursive type that allows self application. We begin with a simple example of a nonterminating expression, illustrating the failure of strong normalization for typable object expressions. Divergent Computation

The object Ω has one method, m, which only sends the message m to the object itself. Consequently, the evaluation of Ω ⇐ m produces an infinite sequence of message sends.

Ω  =^{def} ⟨m = λself.(self ⇐ m)⟩
:  class t ⟨⟨m : t⟩⟩
Ω ⇐ m  ⟶^{eval} (λself.(self ⇐ m)) Ω
⟶^{eval} Ω ⇐ m

Fixed-point Operator

Before considering natural numbers and their basic operations, we show how to define a fixed-point operator on any type. The main idea is illustrated by the following object,X, whose rec (for “recurse”) method causes the function f to be applied to X ⇐ rec.

                                                    X       =^{def} ⟨rec = λself. f(self ⇐ rec)⟩
                                                    X ⇐ rec  ⟶^{eval} f(X ⇐ rec)

We define a general fixed point operator by treating the object X above as a function of f. Using the context

Γ = f : σ → σ,
r : T → [rec],
x : class t ⟨⟨rt | rec : σ⟩⟩

the following typing derivation shows that the resulting function has type (σ → σ) → σ, for any σ.

Γ ⊢ f(x ⇐ rec) : σ
Γ − x ⊢ λx. f(x ⇐ rec)

: class t ⟨⟨rt | rec : σ⟩⟩ → σ

Γ − x − r ⊢ ⟨rec= λx. f(x ⇐ rec)⟩

: class t ⟨⟨rec : σ⟩⟩

Γ − x − r ⊢ ⟨rec= λx. f(x ⇐ rec)⟩ ⇐ rec : σ

ϵ ⊢ λf.⟨rec= λx. f(x ⇐ rec)⟩ ⇐ rec

: (σ → σ) → σ

Object Numerals

The representation of natural numbers by object expressions is more complicated than the preceding examples. The main idea is to represent the natural number n by an object \underline{n} with a method that sends its formal parameter the message m a total of n times. This is similar in spirit to the Church numeral λf. λx. f^{n}, where the number n is represented using a function that does n function applications. The differences are that the numeral for n involves n message sends instead of n function applications, and that since message/method names cannot be parameters, the message that is sent n times must be fixed, rather than a formal parameter. While it is possible to type the Church numerals in our calculus, we have not been able to type a predecessor or equality function on Church numerals.

The “representation” of a number is “stored” as the rep method of the numeral. In addition to the rep method, it is also convenient to include successor and predecessor as methods. This gives us numerals with three methods: S, for successor, P, for predecessor, and rep, for “representation.” Numerals have type

nat  =^{def} class t ⟨⟨S : t, P : t,

rep : test(t) → test(t)⟩⟩

test(t) =^{def} class s ⟨⟨m : s, b : t → t → t⟩⟩

where the type of rep is chosen to make it easy to test whether a number is zero and evaluate one of two argument expressions accordingly.

The numeral for n is defined as follows, using the combinator K =^{def} λx. λy. x and postponing the full definition of predecessor until after zero test is defined.

\underline{n} =^{def} ⟨ rep=K(λx. x ⇐ \overbrace{m ⇐ m ⇐ … ⇐ m}^{n}),

S= λself.⟨self ←
rep=K(λx.(self ⇐ repx) ⇐ m)⟩,
P= λself.⟨self ← rep=K(λx. . . . )⟩

⟩ It is easy to see that successor increments the number of times m is sent by rep, without relying on the predecessor method. For each n, we will be able to show \underline{n}: nat .

Zero test

The function IFZ, for zero test, has the property that IFZ\underline{n} yields true =^{def} λx. λy. x : nat → nat → nat if n = 0 and false =^{def} λx. λy. y : nat → nat → nat otherwise. As a result, IFZ \underline{n} e_{1} e_{2} is e_{1} if n = 0 and e_{2} otherwise. The functions true and false are used in the objects

         F  =^{def} ⟨m= λx. x, b=Kfalse⟩
         T  =^{def} ⟨m=KF, b=Ktrue⟩

with the properties that T ⇐ m ⟶^{eval} F, F ⇐ m ⟶^{eval} F, T ⇐ b ⟶^{eval} true and F ⇐ b ⟶^{eval} false. Using these objects, we define zero test as follows.

IFZ    =^{def} λx.((x ⇐ rep) T) ⇐ b
IFZ\underline{n} ⟶^{eval} T\overbrace{⇐ m … ⇐ m}^{n} ⇐ b
⟶^{eval} \{ \begin{matrix}true & if n = 0 \\ false & if n > 0 \end{matrix}

Predecessor

In rough terms, the main idea for predecessor is to pass an object of the form ⟨m=x, b=K(…)⟩ to the rep method of the object. (The b method is not used, so any function of the right type will do.) If rep sends this object the message m n times, the net effect will be to send x the message m n − 1 times. This gives us a way of decrementing the number of times m is sent to the formal parameter of a function. Zero test, IFZ, is used to take care of the special case n = 0, where the result would otherwise be the object ⟨m=x, b=K(…)⟩, rather than the numeral for 0. The predecessor method of each numeral is defined as follows.

 P= λself.⟨self ← rep=K(λx.(
       (IFZself \underline{1} self) ⇐ rep ⟨m=x, b=K(. . .)⟩))⟩

Since the function (IFZself \underline{1} self) ⇐ rep sends m to ⟨m=x, b=K(…)⟩ a total of min{1, self} times, the predecessor method works as follows.

P\underline{n} ⟶^{eval} ⟨\underline{n} ← rep=K(λx.

(IFZ\underline{n} \underline{1} \underline{n}) ⇐ rep

⟨m=x, b=K(…)⟩)⟩

⟶^{eval} ⟨\underline{n} ← rep=K(λx.

⟨m=x, b=K(…)⟩ \underbrace{⇐ m ⇐ m … ⇐ m}_{min\{1,n\}})⟩

⟶^{eval} ⟨\underline{n} ← rep=K(λx. x\underbrace{⇐ m … ⇐ m}_{min\{1,n\}−1})⟩

This concludes the set of basic functions on natural numbers that are needed to represent all partial recursive functions.

5 Conclusion

We have given a computationally expressive, typed calculus of functions and objects with a sound type system. In this “kernel language,” we define objects and their interfaces (called “classes” here) directly instead of through some subsidiary calculus of records. This gives an axiomatic presentation of a simple object-oriented language and its type system, in a form that we hope is conducive to further work. A feature of the calculus is method specialization: using method redefinition (expressions of the form ⟨e ← n=e′⟩), we may define functions whose type and behavior change in a natural and useful way as a result of inheritance. This capability seems very difficult to achieve directly with any calculus of records. While it seems too early to claim that we have captured “the essence of inheritance in a simple form,” it seems that some progress has been made in this direction.

There are many technical open problems, including development of a denotational model, a proof system for equivalence that is sufficiently powerful to derive nontrivial equations between method bodies, and the investigation of subtyping and substitutivity in this language. Hopefully, the calculus presented here will provide a basis for studying these mathematical problems in a manner that is faithful to substantial uses of object-oriented programming in practice.

References

[Aba93] M. Abadi. Baby Modula-3 and a theory of objects. Technical Report 95, DEC Systems Research Center, 1993. To appear in J. Functional Prog.

[AR88] N. Adams and J. Rees. Object-oriented programming in Scheme. In Proc. ACM Symp.

Lisp and Functional Programming Languages, pages 277–288, July 1988.

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

[CDJ^{+} 89] L. Cardelli, J. Donahue, M. Jordan, B. Kalsow, and G. Nelson. The Modula-3 type system. In Sixteenth ACM Symp. Principles of Programming Languages, pages 202– 212, 1989.

[CM91] L. Cardelli and J.C. Mitchell. Operations on records. Math. Structures in Computer Science, 1(1):3–48, 1991. Summary in Math. Foundations of Prog. Lang. Semantics, Springer LNCS 442, 1990, pp 22–52.

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

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

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

[RA82] J. Rees and N. Adams. T, a dialect of Lisp, or lambda: the ultimate software tool. In Proc. ACM Symp. Lisp and Functional Programming Languages, pages 114–122, August 1982.

[US87] D. Ungar and R.B. Smith. Self: The power of simplicity. In Proc. ACM Symp. on Object-Oriented Programming: Systems, Languages, and Applications, pages 227–241, 1987.

(start)  \overline{ϵ ⊢ ∗}

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

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

Table 4: General Rules

(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}

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

Table 5: Rules for type expressions

Type or row expressions that differ only in the names of bound variables or in the order of label : type pairs are considered identical. In other words, we consider α-conversion of type variables bound by λ or class 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 : τ′}

Table 6: Type equality and associated rules

(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}]}

Table 7: Rules for rows

(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}}

Table 8: Rules for assigning types to terms Page 13