A lambda calculus of objects and method specialization

Kathleen Fisher ^{∗} Computer Science Dept.

Stanford University

   kfisher@cs.stanford.edu

Furio Honsell ^{†} Dipartimento di Informatica Universitá di Udine

                                 honsell@uduniv.cineca.it

John C. Mitchell ^{‡} Computer Science Dept. Stanford University

                                                                  jcm@cs.stanford.edu

June 14, 1994

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 is proved using operational semantics 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 class-based and delegation-based languages. In class-based languages such as Smalltalk [GR83] and C^{++} [ES90], each object is created by a class and inheritance is determined by the class. In delegation-based languages such as Self [US87, CU89], an object may be created from another object, inheriting properties from the original. 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.

In our calculus, the 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].

∗Supported in part by an NSF Graduate Fellowship, an NSF PYI Award and NSF CCR-9303099.

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

‡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 NSF CCR-9303099 and the Wallace F. and Lucille M. Davis Faculty Scholarship.

The main goal of this paper is to develop a type system that allows methods to be specialized appropriately as they are inherited. Briefly, suppose p is a point object with x and y methods returning the integer x- and y-coordinates of p, and a move method with type int × int → point. Method move has this type because if we send the message move to p, we obtain a function which given distances to move in the x and y directions, returns a point identical to p, but with updated x− and 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. If the inherited method had its original type int × int → point, then whenever we moved a colored point, we would 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.

The phenomenon we are concerned with is called “method specialization” in [Mit90], which describes a precursor to the calculus used here. The earlier paper 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. 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 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. A preliminary version of this work appeared in [MHF93].

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 | e_{1}e_{2} | ⟨⟩ | e ⇐ m | ⟨e_{1} ←+ m=e_{2}⟩ | ⟨e_{1} ← m=e_{2}⟩

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 e_{1}e_{2} 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
⟨e_{1} ←+ m=e_{2}⟩ extend object e_{1} with new method m having body e_{2}
⟨e_{1} ← m=e_{2}⟩ replace e_{1}’s method body for m by e_{2}

We consider ⟨e_{1} ←+ m=e_{2}⟩ meaningful only if e_{1} denotes an object that does not have an m method and ⟨e_{1} ← m=e_{2}⟩ meaningful only if e_{1} 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 existing method with 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 general, we attempt to convey the essential properties by the examples of points and colored points given below.

To simplify notation, we write ⟨m_{1} = e_{1}, …, m_{k} = e_{k}⟩ for ⟨… ⟨⟨⟩ ←+ m_{1} = e_{1}⟩ … ←+ m_{k} = e_{k}⟩, where m_{1}, …, m_{k} 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,

⟨m_{1} = e_{1}, …, m_{k} = e_{k}⟩ ⇐ m_{i} ⟶^{eval} e_{i} ⟨m_{1} = e_{1}, …, m_{k} = e_{k}⟩

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. In particular, we may represent the record ⟨l_{1} = e_{1}, …, l_{k} = e_{k}⟩ by the object ⟨m_{1} = Ke_{1}, …, m_{k} = Ke_{k}⟩, where K = λself. λx. x.

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- and 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 to the object p:

                        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,

⟨⟨m_{1}=e_{1}, …, m_{k}=e_{k}⟩ ← m_{i}=ei^{′}⟩ = ⟨m_{1}=e_{1}, …, m_{i}=ei^{′}, …, m_{k}=e_{k}⟩

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 as above, 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 xcoordinate, 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 method. 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 it 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 illustrative object calculus, 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

⟨⟨e_{1} ←∘ n=e_{2}⟩ ←∘ m=e_{3}⟩ = ⟨⟨e_{1} ←∘ m=e_{3}⟩ ←∘ n=e_{2}⟩

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

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

where ←∘ may either ←+ or ←.

Table 1: Bookkeeping and evaluation rules.

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,

⟨⟨⟨m_{1}=e_{1}, … m_{k}=e_{k}⟩ ← m_{1}=e1^{′}⟩ … ← m_{k}=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 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 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 4, 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.

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 e of this type is an object such that for 1 ≤ i ≤ k, the result of e ⇐ 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 e ⇐ 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 ⇐ 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 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 uses 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 and 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 Smalltalk 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, which are discussed below, are those associated with objects. The complete type system appears in Appendix A.

The empty object ⟨⟩ has the object type class t ⟨⟨⟩⟩, as specified in the rule:

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

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 below, 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 Appendix A. Consequently, there is no loss of generality in assuming m is the last method listed in the type.

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

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

(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: τ⟩⟩}

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⟩⟩,

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} − dx − self ⊢ λ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 2: Example typing derivation.

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 2. 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 type system captures the desired form of method specialization.

4 Soundness of the Type System

We prove the soundness of the type system in several steps. The first is subject reduction, i.e., if e has type τ and e → →^{eval} e′, then e′ also has type τ, where the symbol → →^{eval} denotes the transitive closure of the ⟶^{eval} relation. We then define an evaluation strategy eval that reduces expressions of the object calculus to values, a special “value” error, or is undefined if the expression in question fails to terminate. We then use subject reduction to show that if we may derive a type for a closed expression e, then eval(e) ≠ error. Since the evaluator returns error if it fails to find a required method, this fact justfies the claim that our type system prevents “message not understood” errors.

The subject reduction proof begins with a collection of lemmas about substitution for row and type variables. These lemmas allow us to specialize polymorphic object types to include additional methods. In Section 4.2, we introduce a normal form for our typing derivations to permit us to restrict our attention to derivations where the only occurrences of equality rules are as (row β) immediately following an occurrence of (row fn app). This restriction greatly simplifies later proofs. We then prove a series of technical lemmas in Section 4.3. The first of these allows us to treat contexts, which are lists, more like sets. The remaining lemmas in the section provide tools for constructing row expressions to generalize polymorphic object types. The lemmas in Section 4.4 then show that the (⟶^{book}), (β), and (⇐) components of the (⟶^{eval}) relation preserve expression types. The subject reduction theorem then follows. In Section 4.5, we define the eval function and show that typable closed expressions do not evaluate to error, a fact which guarantees that we do not get dynamic message-not-understood errors.

4.1 Substitution Lemmas

The first two lemmas are used to prove that if we may derive a type or row judgement containing a type or row variable, then substituting a type or row expression of the appropriate kind produces a derivable judgement. Lemma 4.1 is the desired property, except it has the additional hypothesis that we may derive the judgement Γ, [U_{2}/u_{2}]Γ′ ⊢ ∗. This extra assumption is required for the (projection), (weakening), and (empty row) cases. Lemma 4.2 then uses Lemma 4.1 to show that the additional hypothesis is in fact unnecessary.

Lemma 4.1 If the judgement Γ, u_{2} : V_{2}, Γ′ ⊢ U_{1} : V_{1} , the judgement Γ ⊢ U_{2} : V_{2} , and the judgement Γ, [U_{2}/u_{2}]Γ′ ⊢ ∗ are all 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 of the form τ : T or R: κ.

Proof The proof is by induction on the derivation of Γ, u_{2} : V_{2}, Γ′ ⊢ U_{1} : V_{1} . Most of the cases are either vacuous or follow immediately from the inductive hypothesis. The (projection) case requires a case analysis on whether or not u_{2} is the projected variable. The (row β) and (type β) cases follow from the fact that if U_{1} →_{β} U_{2} , then [U/u]U_{1} →_{β} [U/u]U_{2} , where U_{1} and U_{2} are either both row expressions or both type expressions, U is either a row or type expression, and u is either a row or type variable, to match U. The (weakening) case requires the fact that Γ ⊢ ∗ is derivable if Γ ⊢ A is. The (class) and (row fn abs) cases follow from the fact that bound variables may be consistently renamed as necessary.

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

Proof The proof of Lemma 4.2 is by induction on the length of Γ′. Lemma 4.1 is needed for the case where Γ′ is extened via (exp var).

Using the fact that Γ ⊢ ∗ is derivable if Γ ⊢ A is, we may combine Lemmas 4.1 and 4.2 to give the desired substitution property on type and kind derivations.

Lemma 4.3 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} may be either τ : T or R: κ.

The following lemma is used in conjunction with Lemma 4.3 to specialize class types to contain additional methods.

Lemma 4.4 If Γ, r: T^{n} →[m⃗], Γ′ ⊢ e : τ and Γ ⊢ R : T^{n} →[m⃗] are both derivable, then so is Γ, [R/r]Γ′ ⊢ e : [R/r]τ.

Proof Lemma 4.4 follows by induction on the derivation of Γ, r: T^{n} →[m⃗], Γ′ ⊢ e : τ. Lemma 4.2 is used in the (projection), (weakening), and (empty object) cases. Lemma 4.3 with U_{2} as a row expression is needed for the (obj ext) case.

4.2 Normal Form

The equality rules in the proof system introduce many non-essential judgement derivations, which unnecessarily complicate derivation analysis. We therefore restrict our attention to derivations in which the only appearance of an equality rule is as (row β) immediately following an occurrence of (row fn app). We will call these derivations ⊢_{N} -derivations. Although not all judgements derivable in the full system are derivable by ⊢_{N} -derivations, we will see below that all judgements whose row and type expressions are in a particular form, which we will call τnf (for type normal form), are derivable via ⊢_{N} -derivations. Since every expression that has a type at all will have a type in τnf, we may prove soundness using only ⊢_{N} -derivations.

The τnf of a type or row expression is its normal form with respect to β -reduction, applied to the row function application redexes within it. This notion is well-defined since the row and type portion of our calculus is strongly normalizing and confluent. We prove this fact by giving a translation function tr into λ^{→}(Σ), where λ^{→}(Σ) denotes the typed lambda calculus with function types over signature Σ, which is defined as:

Type Constants : typ, meth
Term Constants : er : meth

ar : typ → typ → typ cl : (typ → meth) → typ br_{m} : meth → typ → meth for each method name m.

Let the variables of λ^{→}(Σ) contain all of the row and type variables of our calculus. Then define the translation tr by:

tr(t) = t
tr(τ_{1} → τ_{2}) = ar tr(τ_{1}) tr(τ_{2})
tr(class t R) = cl (λt: typ.tr(R))
tr(r) = r
tr(⟨⟨⟩⟩) = er
tr(⟨⟨R | m : τ⟩⟩) = br_{m} tr(R) tr(τ)
tr(λt.R) = λt: typ.tr(R)
tr(Rτ) = tr(R) tr(τ)

We extend tr to the kinds and contexts of our system as follows:

tr(T) = typ
tr(T^{n} →[m⃗]) = typ^{n} → meth
tr(ϵ) = ∅
tr(Γ, x : τ) = tr(Γ)
tr(Γ, t : T) = tr(Γ) ∪ {tr(t) : tr(T)}
tr(Γ, r : κ) = tr(Γ) ∪ {tr(r) : tr(κ)}

Note that tr preserves both bound and free variables of expressions, i.e., BV (U) = BV (tr(U)) and F V (U) = F V (tr(U)) for all row and type expressions U. Furthermore, if U_{1} =_{α} U_{2} , then tr(U_{1}) =_{α} tr(U_{2}) under the same renaming of bound variables.

To show that strong normalization for our system follows from strong normalization for λ^{→}(Σ), we need to establish two properties of tr. We need to show that the translations of any two terms related via →_{β} in our system are related via →_{β} in λ^{→}(Σ) and that the translation of every well-kinded term in our system is a well-typed λ^{→}(Σ) term. Lemma 4.5 proves the first of these properties.

Lemma 4.5 If U_{1} →_{β} U_{2} , then tr(U_{1}) →_{β} tr(U_{2}), where U_{1} and U_{2} are either both row or both type expression in our system.

Proof The proof of Lemma 4.5 is by induction on the structure of U_{1} . Each inductive case is a case analysis of the possible forms of U_{2} . The only case which does not follow routinely is when U_{1} = (λt.R)τ and U_{2} = [τ/t]R. This case follows from the subsidiary lemma that [tr(τ)/t]tr(U) = tr([τ/t]U) for all type and row expressions U, which is proved by induction on the structure of U.

Lemma 4.6 establishes that tr produces typable λ^{→}(Σ) terms.

Lemma 4.6 If Γ ⊢ U : V is derivable in our system, then tr(Γ) > tr(U) : tr(V) is derivable in λ^{→}(Σ), where we use > to distinguish λ^{→}(Σ)-derivations from derivations in our system.

Proof The proof of Lemma 4.6 is by induction on the derivation of Γ ⊢ U : V . The cases for (row β) and (type β) require Lemma 4.5 and Subject Reduction for λ^{→}(Σ).

Combining Lemmas 4.5 and 4.6 we get that the row and type portion of our calculus is strongly normalizing:

Lemma 4.7 (Strong Normalization for Row and Type Portion) If Γ ⊢ U : V is derivable, where U is either a row or type expression, then there is no infinite sequence of →_{β} reductions from U.

The following lemma is crucial to showing that confluence for λ^{→}(Σ) implies confluence for the row and type portion of our calculus.

Lemma 4.8 If tr(U) →_{β} W, then there is a unique expression U′ such that U →_{β} U′ and tr(U′) = W, where U is either a row or type expression and W is an expression of λ^{→}(Σ).

Proof The proof of Lemma 4.8 is by induction on the structure of U. It is similar in outline to the proof of Lemma 4.5.

The confluence of the row and type portion of our system now follows.

Lemma 4.9 (Confluence for Row and Type Portion) If Γ ⊢ U_{1} : V_{1} is derivable and U_{1} → →_{β} U_{2} and U_{1} → →_{β} U_{3} , then there exists a U_{4} such that U_{2} → →_{β} U_{4} and U_{3} → →_{β} U_{4} .

Since each row and type expression has a unique normal form, the τnf of row and type expressions is a well-defined notion. Because any term expression that has a type has a type in normal form, we may restrict our attention to types and rows in τnf. To this end, we need to extend the definition of τnf to term expressions and contexts. The τnf of a term expression e is just that expression e. The τnf of a context Γ is the context listing the τnf ’s of the elements of Γ. The following lemma then shows we can find a ⊢_{N} -derivation for any judgement in τnf.

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

Proof 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. Most of the other cases follow immediately from the inductive hypothesis. We give the (row fn app) case in detail, since it is the most interesting.

If Γ ⊢ A is derived via (row fn app), then Γ ⊢ A must be of the form

Γ ⊢ Rτ : T^{n} →[m⃗].

By the hypotheses for (row fn app), we must have previously derived

Γ ⊢ R : T^{n+1} →[m⃗]

and

Γ ⊢ τ : T .

By the inductive hypothesis, we know that

τnf(Γ) ⊢_{N} τnf(R : T^{n+1} →[m⃗])

and

τnf(Γ) ⊢_{N} τnf(τ : T)

are both derivable. Applying (row fn app) to these two judgements produces

τnf(Γ) ⊢_{N} τnf(R)τnf(τ) : T^{n} →[m⃗].

There are two cases to consider: either τnf(R) is a λ-abstraction or it is not.

Case 1: τnf(R) = λt.τnf(R′). In this case, we have that

τnf(Γ) ⊢_{N} (λt.τnf(R′))τnf(τ) : T^{n} →[m⃗].

Now

(λt.τnf(R′))τnf(τ) →_{β} [τnf(τ)/t]τnf(R′),

so applying (row β) to the last judgement produces

τnf(Γ) ⊢_{N} [τnf(τ)/t]τnf(R′) : T^{n} →[m⃗],

which is still a ⊢_{N} -derivation. Note that

[τnf(τ)/t]τnf(R′) = τnf(Rτ)

since substituting types in normal form for variables cannot introduce new β -reductions. (Substituting a row expression for a row variable could introduce a new β -reduction, but we do not allow abstraction over row variables so we need not worry about this case.) Thus the following judgement is derivable:

τnf(Γ) ⊢_{N} τnf(Rτ : T^{n} →[m⃗]).

Case 2: τnf(R) is not a λ-abstraction. In this case, the desired result follows immediately from the inductive hypothesis.

From this point on, we will only concern ourselves with 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.

4.3 Technical Lemmas

The following lemma is useful because it allows contexts, which are in fact lists, to be treated more like sets.

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

Proof The proof of Lemma 4.11 is by induction on the derivation of Γ, Γ′ ⊢ A. The (obj ext) and (obj over) cases require a subsidiary lemma that permits the consistent renaming of the row variables in a judgement. This renaming is necessary to avoid naming-clashes.

The remaining lemmas in this section are used to build well-formed row expressions that can be substituted for row variables in typing derivations. This ability is crucial to the proofs of Lemmas 4.15 and 4.17.

Lemma 4.12 If Γ ⊢_{N} λt_{1}, …, t_{n}.⟨⟨R | m⃗: τ⃗⟩⟩ : T^{n} →[l⃗] is derivable, then so are Γ, t_{1} : T, …, t_{n} : T ⊢_{N} τ_{i} : T for each τ_{i} in τ⃗ and Γ, t_{1} : T, …, t_{n} : T ⊢_{N} R : [m⃗, l⃗].

Proof The proof of Lemma 4.12 is by induction on the derivation of Γ ⊢_{N} λt_{1}, …, t_{n}.⟨⟨R | m⃗: τ⃗⟩⟩ : T^{n} →[l⃗]. Most of the cases follow routinely from the inductive hypothesis. The (weakening) case follows from repeated applications of Lemma 4.11. The (row β) case is worked out here, since it is the most difficult.

If Γ ⊢_{N} λt_{1}, …, t_{n}.⟨⟨R | m⃗: τ⃗⟩⟩ : T^{n} →[l⃗] is derived via (row β), then the previous step must have been (row fn app) by the definition of a ⊢_{N} -derivation. Furthermore, its hypotheses must have been of the form:

Γ ⊢_{N} λt.λt_{1}, …, t_{n}.⟨⟨R^{∗} | m⃗: τ^{∗}⟩⟩ : T^{n} →[l⃗]

and

Γ ⊢_{N} τ′ : T

where

λt_{1}, …, t_{n}.⟨⟨R | m⃗: τ⃗⟩⟩ = [τ′/t]λt_{1}, …, t_{n}.⟨⟨R^{∗} | m⃗: τ^{∗}⟩⟩.

Without loss of generality, t_{1}, … t_{n} ∉ F V (τ′) ∪ {t}, so

λt_{1}, …, t_{n}.⟨⟨R | m⃗: τ⃗⟩⟩ = λt_{1}, …, t_{n}.⟨⟨[τ′/t]R^{∗} | m⃗: [τ′/t]τ^{∗}⟩⟩,

which implies that τ⃗ = [τ′/t]τ^{∗} and R = [τ′/t]R^{∗}. By the inductive hypothesis, for each τ_{i}^{∗} in τ^{∗}

Γ, t: T, t_{1} : T, …, t_{n} : T ⊢_{N} τ_{i}^{∗} : T

and

Γ, t: T, t_{1} : T, …, t_{n} : T ⊢_{N} R^{∗} : [m⃗, l⃗]

are derivable. By Lemma 4.3, for each τ_{i}^{∗} in τ^{∗},

Γ, t_{1} : T, …, t_{n} : T ⊢ [τ′/t]τ_{i}^{∗} : T

and

Γ, t_{1} : T, …, t_{n} : T ⊢ [τ′/t]R^{∗} : [m⃗, l⃗]

are derivable. Since τ⃗ = [τ′/t]τ⃗^{∗} and R = [τ′/t]R^{∗}, these are just:

Γ, t_{1} : T, …, t_{n} : T ⊢ τ_{i} : T

and

Γ, t_{1} : T, …, t_{n} : T ⊢ R : [m⃗, l⃗].

The original derivation is in τnf, so Γ, τ⃗, and R are all in τnf. Hence by Lemma 4.10, we get for each τ_{i} in τ⃗

Γ, t_{1} : T, …, t_{n} : T ⊢_{N} τ_{i} : T

and

Γ, t_{1} : T, …, t_{n} : T ⊢_{N} R : [m⃗, l⃗]

are derivable.

Lemma 4.13 If Γ ⊢_{N} class t ⟨⟨R | m⃗: τ⃗⟩⟩ : T is derivable, then so are Γ, t: T ⊢_{N} τ_{i} : T for each τ_{i} in τ⃗ and Γ, t: T ⊢_{N} R : [m⃗].

The proof of Lemma 4.13 is by induction on the derivation of Γ ⊢_{N} class t ⟨⟨R | m⃗: τ⃗⟩⟩ : T to handle the (weakening) case. Most of the cases are vacuous, since they could not have been the last step in the derivation of the form Γ ⊢_{N} class t ⟨⟨R | m⃗: τ⃗⟩⟩ : T. The (type β) case follows vacuously because it cannot appear in a ⊢_{N} -derivation. The (class) case follows immediately from Lemma 4.12.

Lemma 4.14 If Γ ⊢_{N} e : τ is derivable, then so is Γ ⊢_{N} τ : T.

Proof The proof of Lemma 4.14 is by induction on the derivation of Γ ⊢_{N} e : τ. Below is the case for (obj ext), which is the most difficult. The other cases follow for similar reasons or directly from the inductive hypothesis.

If Γ ⊢_{N} e : τ is derived via (obj ext), then the judgement must have the form:

Γ ⊢_{N} ⟨e_{1} ←+ n=e_{2}⟩ : class t ⟨⟨R | m⃗: τ⃗, n: τ⟩⟩.

By the hypotheses for (obj ext), we must have previously derived

Γ ⊢_{N} e_{1} : class t ⟨⟨R | m⃗: τ⃗⟩⟩.

Applying the inductive hypothesis to this produces the judgement:

Γ ⊢_{N} class t ⟨⟨R | m⃗: τ⃗⟩⟩ : T .

By Lemma 4.13 then, we have that for all τ_{i} in τ⃗

Γ, t: T ⊢_{N} τ_{i} : T

is derivable. The hypotheses for (obj ext) also give us that

Γ, t: T ⊢_{N} R : [m⃗, n]

is derivable. By |m⃗| applications of (row ext), we may derive

Γ, t: T ⊢_{N} ⟨⟨R | m⃗: τ⃗⟩⟩ : [n].

The final hypothesis for (obj ext) tells us that the judgement:

Γ, r : T → [m⃗, n] ⊢_{N} e_{2} : [class t ⟨⟨rt | m⃗: τ⃗, n: τ⟩⟩/t](t → τ)

is derivable. Applying the inductive hypothesis produces the judgement:

Γ, r : T → [m⃗, n] ⊢_{N} [class t ⟨⟨rt | m⃗: τ⃗, n: τ⟩⟩/t](t → τ) : T .

It then follows from an easily proved property of derivations that

Γ, r : T → [m⃗, n] ⊢_{N} class t ⟨⟨rt | m⃗: τ⃗, n: τ⟩⟩ : T

is also derivable. Lemma 4.13 gives us that

Γ, r : T → [m⃗, n], t : T ⊢_{N} τ : T

is also derivable. By the side condition for (row ext), r ∉ F V (τ), so as a consequence of Lemma 4.3 we may derive

Γ, t : T ⊢_{N} τ : T .

Applying row extension, we may derive the judgement

Γ, t : T ⊢_{N} ⟨⟨R | m⃗: τ⃗, n : τ⟩⟩ : ∅.

Applying (class) to this judgement produces

Γ ⊢_{N} class t ⟨⟨R | m⃗: τ⃗, n : τ⟩⟩ : T ,

which is the judgement we wished to derive.

4.4 Type Preservation Lemmas

The next three lemmas show that the various components of the (⟶^{eval}) relation preserve expression types.

Lemma 4.15 If Γ ⊢_{N} e : τ is derivable, and e ⟶^{book} e′, then Γ ⊢_{N} e′ : τ is also derivable.

Proof The proof of Lemma 4.15 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 may be 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 4.4, 4.13, and 4.14 are essential for the (switch ext ov) case.

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

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

Proof The proof of Lemma 4.16 is by induction on the derivation of Γ, x: τ_{1}, Γ′ ⊢ e_{2} : τ_{2} . Several of the cases require a lemma of the form that if Γ, x: τ, Γ′ ⊢ A is derivable with x not in A, then the judgement Γ, Γ′ ⊢ A is also derivable. The proof of this sub-lemma is similar in structure to the proof of Lemma 4.3.

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

Lemma 4.17 If Γ ⊢_{N} ⟨⟨e ←∘_{1} m_{1}=e_{1}⟩ … ←∘_{k} m_{k}=e_{k}⟩ : 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 Γ ⊢ e_{i} : [class t ⟨⟨R | m_{1} : τ_{1}, …, m_{k} : τ_{k}⟩⟩/t](t → τ_{i}) is derivable.

Proof Suppose that Γ ⊢_{N} ⟨⟨e ←∘_{1} m_{1}=e_{1}⟩ … ←∘_{k} m_{k}=e_{k}⟩ : class t ⟨⟨R | m_{1} : τ_{1}, …, m_{k} : τ_{k}⟩⟩ is derivable. The proof then has two parts. The first part, which establishes Claim 4.18 below, gives a derivable type for each object obtained from ⟨⟨e ←∘_{1} m_{1}=e_{1}⟩ … ←∘_{k} m_{k}=e_{k}⟩ by stripping off some number of the ←∘ operations. Names for these “subobjects” are introduced below. The second part, establishing Claim 4.19, shows that we may derive the required type for each of the e_{i} ’s. Claim 4.19 follows from an analysis of the typing judgements given by Claim 4.18.

To represent the subobjects of ⟨⟨e ←∘_{1} m_{1}=e_{1}⟩ … ←∘_{k} m_{k}=e_{k}⟩, we introduce the following notation:

\begin{matrix}O_{0} & =^{def} & e \\ O_{j} & =^{def} & ⟨O_{j−1} ←∘_{j} m_{j}=e_{j}⟩. \end{matrix}

Note that the object in the assumption of the lemma is just O_{k}. We also need to be able to name particular collections of the methods defined in O_{k} and their associated types. To this end, let M_{j} = [m_{j+1}, …, m_{k}] and M_{j}^{−} be the subsequence of M_{j} such that m_{i} ∈ M_{j}^{−} if and only if ←∘_{i} = ←+. Similarly, let Σ_{j} = [τ_{j+1}, …, τ_{k}] and Σ_{j}^{−} be the subsequence of Σ_{j} such that τ_{i} ∈ Σ_{j}^{−} if and only if m_{i} ∈ M_{j}^{−}. Note that M_{k} = M_{k}^{−} = ϵ, M_{0} = [m_{1}, …, m_{k}], and M_{0}^{−} = [m_{i}| ←∘_{i} = ←+]. Thus M_{0}^{−} is the sequence of all methods in O_{k} that are not defined in O_{0} . It follows that the methods in (M_{0}−M_{0}^{−}) are those methods that are overridden in O_{k}. Similarly, M_{j}^{−} is the sequence of all methods in O_{k} that are not defined in O_{j}, and the methods in (M_{j} −M_{j}^{−}) are those methods defined in O_{j} that are later overridden in O_{k}.

Lemma 4.17 follows immediately from the following two claims, written using the notation just defined:

Claim 4.18 If Γ ⊢_{N} O_{k} : class t ⟨⟨R | m_{1} : τ_{1}, …, m_{k} : τ_{k}⟩⟩ is derivable, then

Γ ⊢_{N} O_{k−n} : class t ⟨⟨R | m_{1} : τ_{1}, …, m_{k−n} : τ_{k−n}, (M_{k−n} − M_{k−n}^{−}) : (Σ_{k−n} − Σ_{k−n}^{−})⟩⟩

is also derivable for all 0 ≤ n ≤ k.

Claim 4.19 If Γ ⊢_{N} O_{k} : class t ⟨⟨R | m_{1} : τ_{1}, …, m_{k} : τ_{k}⟩⟩ and

Γ ⊢_{N} O_{i} : class t ⟨⟨R | m_{1} : τ_{1}, …, m_{i} : τ_{i}, (M_{i} − M_{i}^{−}) : (Σ_{i} − Σ_{i}^{−})⟩⟩

are derivable, where 1 ≤ i ≤ k, then

Γ ⊢_{N} e_{i} : [class t ⟨⟨R | m_{1} : τ_{1}, …, m_{k} : τ_{k}⟩⟩/t](t → τ_{i})

is also derivable.

The proof of Claim 4.18 is by induction on n. Claim 4.19 follows by an induction on the derivation of the typing for O_{i}. (An induction is necessary to handle the (weakening) case. Otherwise a simple case analysis would suffice.) The only cases besides (weakening) that need to be considered are (obj ext) and (obj over). Both of these rules have a hypothesis of the form:

Γ′, r : T → [m_{1}, …, m_{i}, (M_{i} − M_{i}^{−})] ⊢_{N}
e_{i} : [class t ⟨⟨rt | m_{1} : τ_{1}, …, m_{i} : τ_{i}, (M_{i} − M_{i}^{−}) : (Σ_{i} − Σ_{i}^{−})⟩⟩/t](t → τ_{i}).

Lemmas 4.13 and 4.14 are used to build a row expression that is substituted via Lemma 4.4 for the row variable r in the above judgement to give the desired type to e_{i}.

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

Proof The proof is similar in outline to that of Lemma 4.15; 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.15, the (β) case from Lemma 4.16 and the (⇐) case from Lemma 4.17.

4.5 Type Soundness

Now that we have subject reduction, we need to formalize the notion of message-not-understood errors to show that our type system prevents them. Intuitively, a message-not-understood error occurs when a message m is sent to an expression that does not define an object with an m-method. To formalize this notion, we define mutually recursive functions eval and get_{m} via proof rules in the style of structured operational semantics. The ideas behind this proof system are discussed below. The full system is given in Appendix B

The eval function is the standard lazy evaluator from lambda calculus, extended to our object calculus in the following way. Object expressions other than message sends evaluate to themselves. On expressions of the form e ⇐ m, eval uses the function get_{m} to extract the m method from e. This behavior is specified in the (eval ⇐) proof rule:

(eval ⇐)  \frac{\begin{matrix}get_{m}(e) = ⟨e_{1} ← m = e_{2}⟩ \\ eval(e_{2}⟨e_{1} ← n = e_{2}⟩) = z \end{matrix}}{eval(e ⇐ m) = z}

which we may read as follows. Once get_{m} has extracted the m method from e by returning an expression of the form ⟨e_{1} ← m = e_{2}⟩, we “send” the message m to this expression by applying e_{2} to the object. This resulting expression is then recursively evaluated to z, which is then returned as the value of the original message send. Meta-variable z is either an expression or the special “value” error.

How does get_{m} extract an m-method from its expression? There are two different forms of expressions from which get_{m} may immediately extract an m method: ⟨e_{1} ← m = e_{2}⟩ and ⟨e_{1} ←+ m = e_{2}⟩. The corresponding axioms are:

(getm ←) get_{m}(⟨e_{1} ← m = e_{2}⟩) = ⟨e_{1} ← m = e_{2}⟩

(getm ←+) get_{m}(⟨e_{1} ←+ m = e_{2}⟩) = ⟨⟨e_{1} ←+ m = e_{2}⟩ ← m = e_{2}⟩

The second of these rules converts its object ⟨e_{1} ←+ m = e_{2}⟩to the equivalent object ⟨⟨e_{1} ←+ m = e_{2}⟩ ← m = e_{2}⟩ so that get_{m} returns objects in a standard form.

To extract an m method from more complicated expressions, we recursively use the eval and get_{m} functions. The (getm ⇐) rule is representative of these cases:

(getm ⇐)  \frac{\begin{matrix}get_{n}(e) = ⟨e_{1} ← n = e_{2}⟩ \\ get_{m}(e_{2}⟨e_{1} ← n = e_{2}⟩) = z \end{matrix}}{get_{m}(e ⇐ n) = z}

To find an m-method in an expression of the form e ⇐ n, we first find an n-method in the expression e by calling get_{n}(e), which returns an expression of the form ⟨e_{1} ← n = e_{2}⟩. We then “send” the object ⟨e_{1} ← n = e_{2}⟩ the message n by extracting the n method and applying it to ⟨e_{1} ← n = e_{2}⟩. We return the result of recursively looking for an m-method in the resulting expression.

How could get_{m} fail to find an m method? There are three different ways in which get_{m} may immediately “realize” that its object does not have the required method m. Its object could be a variable, a lambda abstraction, or the empty object ⟨⟩. These possibilities are described by the following three axioms:

(getm var) get_{m}(x) = error

(getm ⟨⟩) get_{m}(⟨⟩) = error

(getm λ) get_{m}(λx. e) = error

When called on more complicated expressions, get_{m} fails to find its desired method if one of its recursive calls fails. The (getm ⇐ err) and (getm ⇐) rules are representative of these cases:

(getm ⇐ err)  \frac{get_{n}(e) = error}{get_{m}(e ⇐ n) = error}

(getm ⇐)  \frac{\begin{matrix}get_{n}(e) = ⟨e_{1} ← n = e_{2}⟩ \\ get_{m}(e_{2}⟨e_{1} ← n = e_{2}⟩) = z \end{matrix}}{get_{m}(e ⇐ n) = z}

These rules reflect the fact that there are two ways we could fail to find an m-method in an expression of the form e ⇐ n. The first, described by (getm ⇐ err), occurs when we cannot find an n-method in e. The second, described by the same (getm ⇐) rule that we saw above, occurs when we cannot find an m method in the expression obtained by invoking e’s n-method.

We need to define these mutually recursive functions instead of using a single eval function because the notion of a value changes within the context of a message send. In particular, when we are not looking for a method, any object expression of the form ⟨e ←∘ m = e′⟩ is a value. If we are looking for an m method, then expressions of the form⟨e ← m = e′⟩ are still values. However, if we are looking for an n method, ⟨e ←∘ m = e′⟩ is not a value and must be evaluated further.

Our specific eval and get_{m} functions are designed so that we may demonstrate that our type system prevents message-not-understood errors in programs. The same technique would allow us to show that terms typed as function expressions in programs either diverge or reduce to lambda abstractions. To do this, we would need to add a third evaluation function, get_{λ}, that “looks” for lambda abstractions and returns a tagged error value function − error when called on an expression that cannot reduce to a lambda abstraction. To simplify the presentation, we only consider message-not-understood errors here.

Using the proof rules, we may show formally that typable programs of our object calculus do not produce message-not-understood errors.

Lemma 4.21 If ev(e_{1}) = e_{2} , then e_{1}→ →^{eval}e_{2} , where ev is either get_{m} or eval.

Proof The proof is by induction on the derivation of ev(e_{1}) = e_{2} . The base case for the (getm ←+) axiom follows from the (add ov) bookkeeping rule. The other base cases are either vacuous, since error is not an expression, or immediate.

The inductive case for the (getm ⇐) proof rule is given below since it is representative of the non-vacuous inductive cases. If we have derived get_{m}(e ⇐ n) = e′ via (getm ⇐), then we must previously have derived that

get_{n}(e) = ⟨e_{1} ← n = e_{2}⟩

and

get_{m}(e_{2}⟨e_{1} ← n = e_{2}⟩) = e′.

Note that get_{m}(e_{2}⟨e_{1} ← n = e_{2}⟩) cannot equal error, since we know that get_{m}(e ⇐ n) = e′ and e′ is an expression, not error. Thus

e ⇐ n → →^{eval} ⟨e_{1} ← n = e_{2}⟩ ⇐ n
→^{eval} e_{2}⟨e_{1} ← n = e_{2}⟩
→^{eval} e′

The first step above follows from the inductive hypothesis and fact that the reduction rules are a congruence relation. The second step follows from the (⇐)-reduction rule, and the final one via the inductive hypothesis.

It remains to show that if we may derive ∅ ⊢ e : τ, then eval(e) ≠ error. Because there are two ways in which eval(e) could not equal error, either by returning an expression or being undefined (which happens when e diverges under lazy evaluation), it is simpler to prove the contrapositive:

Lemma 4.22 If ev(e) = error, then

• if ev = get_{m}, then ∅ ⊬ e : class t ⟨⟨R | m : τ⟩⟩ for any row R and type τ, and

• if ev = eval, then ∅ ⊬ e : τ for any type τ, where Γ ⊬ A indicates that the judgment Γ ⊢ A is not derivable.

Proof The proof is by induction on the derivation of ev(e) = error. The base cases are either vacuous or follow by inspection of the typing rules. We give the inductive cases for the (getm ⇐ err) and (getm ⇐) rules, since they are representative of the non-vacuous inductive cases.

(getm ⇐ err) If we derive ev(e) = error via (getm ⇐ err), then ev is get_{m}, e must be of the form e′ ⇐ n, and we must have previously derived that get_{n}(e′) = error. Applying the inductive hypothesis, we get that

∅ ⊬ e′ : class t ⟨⟨R′ | n : τ′⟩⟩

for any row R′ and any type τ′. Then an inspection of the typing rule for message send (meth app) reveals that

∅ ⊬ e′ ⇐ n : τ′′

for any type τ′′. A fortiori,

∅ ⊬ e′ ⇐ n : class t ⟨⟨R | m: τ⟩⟩

for any row R and type τ, which is what we needed to show.

(getm ⇐) If we derive ev(e) = error via (getm ⇐), then ev is get_{m} and e must be of the form e′ ⇐ n. Also, we must have previously derived that get_{n}(e′) = ⟨e_{1} ← n = e_{2}⟩ and get_{m}(e_{2}⟨e_{1} ← n = e_{2}⟩) = error. Applying the inductive hypothesis to the second of these equations, we get

∅ ⊬ e_{2}⟨e_{1} ← n = e_{2}⟩ : class t ⟨⟨R | m : τ⟩⟩.

By Lemma 4.21, e′ → →^{eval} ⟨e_{1} ← n = e_{2}⟩, so

\begin{aligned}e′ ⇐ n & → →^{eval} & ⟨e_{1} ← n = e_{2}⟩ ⇐ n \\ & →^{eval} & e_{2}⟨e_{1} ← n = e_{2}⟩. \end{aligned}

Since ∅ ⊬ e_{2}⟨e_{1} ← n = e_{2}⟩ : class t ⟨⟨R | m : τ⟩⟩, we get by Subject Reduction (Theorem 4.20) that

∅ ⊬ e′ ⇐ n : class t ⟨⟨R | m : τ⟩⟩,

which is what we needed to show.

Theorem 4.23 (Type Soundness) If the judgement ∅ ⊢ e : τ is derivable, then eval(e) ≠ error.

5 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 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 fixedpoint 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 σ that does not contain t.

Γ ⊢ 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}x, 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 being 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 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 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 may 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.

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

[MHF93] J.C. Mitchell, F. Honsell, and K. Fisher. A lambda calculus of objects and method specialization. In Proc. IEEE Symp. on Logic in Computer Science, pages 26–38, 1993.

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

A Typing rules

General Rules

(start1)  \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}

(class)  \frac{Γ, t: T ⊢ R : [m_{1}, …, m_{k}]}{Γ ⊢ class 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 λ 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 : τ′}

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{Γ ⊢ ∗}{Γ ⊢ ⟨⟩ : 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}.

B Definition of evaluation strategy

Axioms In the following, meta-variable z represents either an expression or error. (getm var) get_{m}(x) = error (getm ⟨⟩) get_{m}(⟨⟩) = error (getm λ) get_{m}(λx. e) = error (getm ←) get_{m}(⟨e_{1} ← m = e_{2}⟩) = ⟨e_{1} ← m = e_{2}⟩ (getm ←+) get_{m}(⟨e_{1} ←+ m = e_{2}⟩) = ⟨⟨e_{1} ←+ m = e_{2}⟩ ← m = e_{2}⟩ (eval var) eval(x) = x (eval ⟨⟩) eval(⟨⟩) = ⟨⟩ (eval λ) eval(λx. e) = λx. e (eval ←) eval(⟨e_{1} ← m = e_{2}⟩) = ⟨e_{1} ← m = e_{2}⟩ (eval ←+) eval(⟨e_{1} ←+ m = e_{2}⟩) = ⟨e_{1} ←+ m = e_{2}⟩ Inference Rules

(getm app err)  \frac{eval(e_{1}) = error}{get_{m}(e_{1}e_{2}) = error}
(getm app)  \frac{\begin{matrix}eval(e_{1}) = λx. e′_{1} \\ get_{m}([e_{2}/x]e′_{1}) = z \end{matrix}}{get_{m}(e_{1}e_{2}) = z}
(getm ⇐ err)  \frac{get_{n}(e) = error}{get_{m}(e ⇐ n) = error}
(getm ⇐)  \frac{\begin{matrix}get_{n}(e) = ⟨e_{1} ← n = e_{2}⟩ \\ get_{m}(e_{2}⟨e_{1} ← n = e_{2}⟩) = z \end{matrix}}{get_{m}(e ⇐ n) = z}

(getm ← err)  \frac{\begin{matrix}n ≠ m \\ get_{m}(e_{1}) = error \end{matrix}}{get_{m}(⟨e_{1} ← n = e_{2}⟩) = error}^{(getm ←)  \frac{\begin{matrix}n ≠ m \\ get_{m}(e_{1}) = ⟨e_{3} ← m = e_{4}⟩ \end{matrix}}{get_{m}(⟨e_{1} ← n = e_{2}⟩) = ⟨⟨e_{3} ← n = e_{2}⟩ ← m = e_{4}⟩}}^{(getm ←+ err)  \frac{\begin{matrix}n ≠ m \\ get_{m}(e_{1}) = error \end{matrix}}{get_{m}(⟨e_{1} ←+ n = e_{2}⟩) = error}}^{(getm ←+)  \frac{\begin{matrix}n ≠ m \\ get_{m}(e_{1}) = ⟨e_{3} ← m = e_{4}⟩ \end{matrix}}{get_{m}(⟨e_{1} ←+ n = e_{2}⟩) = ⟨⟨e_{3} ←+ n = e_{2}⟩ ← m = e_{4}⟩}}^{(eval app err)  \frac{eval(e_{1}) = error}{eval(e_{1}e_{2}) = error}}^{(eval app)  \frac{\begin{matrix}eval(e_{1}) = λx. e′_{1} \\ eval([e_{2}/x]e′_{1}) = z \end{matrix}}{eval(e_{1}e_{2}) = z}}^{(eval ⇐ err)  \frac{get_{n}(e) = error}{eval(e ⇐ n) = error}}^{(eval ⇐)  \frac{\begin{matrix}get_{n}(e) = ⟨e_{1} ← n = e_{2}⟩ \\ eval(e_{2}⟨e_{1} ← n = e_{2}⟩) = z \end{matrix}}{eval(e ⇐ n) = z}}

30