An Ef�cient Class and Object Encoding ^{∗}

Neal Glew

Department of Computer Science Cornell University

aglew@acm.org

ABSTRACT

An object encoding translates a language with object primitives to one without. Similarly, a class encoding translates classes into other primitives. Both are important theoretically for comparing the expressive power of languages and for transferring results from traditional languages to those with objects and classes. Both are also important foundations for the implementation of object-oriented languages as compilers typically include a phase that performs these translations.

This paper describes a language with a primitive notion of classes and objects and presents an encoding of this language into one with records and functions. The encoding uses two techniques often used in compilers for single-inheritance class-based object-oriented languages: the self-application semantics and the method-table technique. To type the output of the encoding, the encoding uses a new formulation of self quantifiers that is more powerful than previous approaches.

1. INTRODUCTION

An object encoding is a translation from a language with a primitive notion of objects to one without, typically one that has functions and records instead. Object encodings are important theoretically for comparing the expressive power of object-oriented languages versus functional languages and for transferring results proven about functional languages to object-oriented languages. Object encodings are also important for building solid foundations for the implementation of object-oriented languages as known implementation techniques typically involve a phase that turns objects into records and functions.

∗This paper is based on work supported in part by the NSF grant CCR-9708915, AFOSR grant F49620-97-1-0013, and ARPA/RADC grant F30602-1-0317. Any opinions, findings, and conclusions or recommendations expressed in this publication are those of the author and do not reflect the views of these agencies.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for pro�t or commercial advantage and that copies bear this notice and the full citation on the �rst page. To copy otherwise, to republish, to post on servers or to redistribute to lists, requires prior speci�c permission and/or a fee. OOPSLA 2000, Minneapolis, MN, USA Copyright 2000 ACM 0-89791-88-6/97/05 ..$5.00

A typical implementation of an object-oriented language uses a translation that corresponds to the self-application semantics [Kam88] (this paper uses the term self-application semantics to refer to both the implementation technique and the semantics). In the self-application semantics, an object becomes a record with entries for the object’s fields and methods. Methods become functions which take an extra argument, and the object itself is always passed as this extra argument—because part of the object is applied to the object itself, the terminology “self application” is used.

Similarly, a class encoding is a translation from a language with a primitive notion of classes into one without. A class encoding might target a pure object language or might be combined with an object encoding to produce records and functions. Class encodings are important for the same reason as object encodings: they illuminate the additional expressiveness of classes and provide foundations for the implementation of class-based languages.

A typical implementation of a class-based language uses the method-table technique in addition to the self-application semantics. In this refinement, objects become records with entries for the object’s fields and an entry for a method table, which is another record with entries for the object’s methods. Only one method table is constructed per class and is shared amongst all the class’s instances.

It is important to distinguish between typed and untyped encodings. An untyped encoding translates into a language without a static typing discipline. A typed encoding translates a statically typed language into a statically typed language and must, if given type-correct input, produce typecorrect output. Typed encodings provide foundations for type-directed compilers, which in addition to translating code also maintain and translate type information. There are several benefits to type-directed compilers: They can be debugged by turning on intermediate language type checkers (e.g., [MTC^{+}96]). They can use type information to guide or enable optimisation or better run-time systems (e.g., [TMC^{+}96]). They can produce certificates of safety for target code [NL98, MCG^{+}99]. Typed object and class encodings describe how to produce the necessary type information for an intermediate language based on records and functions.

The search for object and class encodings is also an attempt to tease apart the various aspects of objects: packaging of code and data, self reference, information hiding, et cetera. Teasing these aspects apart breaks the object construct into a number of separate concepts. Many of these concepts match well with traditional records, functions, and type systems. Indeed, the self-application semantics and method-tables are easily expressed as untyped object encodings. But one concept does not: the type of self, and this mismatch makes it difficult to extend these encodings to produce type correct output in some typed language. Typed encodings must somehow capture the type of self using existing type constructors or by inventing new ones.

The extensive previous work on typed object and class encodings, is discussed in detail with references in Section 5. These encodings have used a combination of recursive types and some flavour of existential types to capture the type of self. Recursive types are used because objects can refer to themselves. Existential types are used to try to capture the information hiding aspect of objects. Unfortunately, these combinations of recursive and existential types do not quite capture self’s type, forcing these encodings to include work arounds: extra data structures, extra indirections, and extra operations. For theoretical purposes, these work arounds are no problem, and these encodings answer important theoretical questions such as the comparative expressiveness of object-oriented languages versus functional languages and how to transfer results about functional languages to objectoriented languages. But for practical purposes, implementations based directly on these encodings are not efficient, and so these encodings cannot be considered foundations for language implementation.

This paper tackles the type of self directly by introducing a new type constructor, the self quantifier, to capture it. To explain what a self quantifier does, consider some object and the static types assigned to it at various program points. In general the static types will not be the actual run-time type of the object, but rather a supertype of the run-time type. Self quantifiers allow the supertype to refer to the actual, but unknown, run-time type of the object. This paper uses self quantifiers to devise a new typed object and class encoding that is faithful to the self-application semantics and methodtable techniques. In particular, methods become functions which require an argument of the actual run-time type, and self quantifiers are used to capture this requirement.

The main contribution of this paper is a new typed object and class encoding based on a new formulation of self quantifiers. The key to understanding object encodings is the typing of self, and self quantifiers naturally capture this type. The new formulation of self quantifiers avoids certain problems with previous typed encodings and allows the self-application semantics and method-table techniques to be used as the term translation. Since these techniques are used in real compilers, the new encoding provides a formal foundation for implementations. A minor contribution of this paper is a new object language with primitive notions of classes and objects.

1.1 Roles of Classes

In typical class-based object-oriented languages, classes play a number of roles. Primarily, a class provides a template for the creation of objects, specifying which fields the objects will have and how they will respond to methods. But classes play other roles as well. For example, in Java [GJS96] a class provides a template, a named type, an explicit subtyping relationship between this named type and the named type of the superclass, constructors that allow for the controlled creation and initialisation of objects, and the ability to downcast objects based on the class from which they were

                                                        class Window {
                                                          Rectangle extent;
                                                          boolean handleEvent(Event) {· · · };
                                                          boolean contains(Point) {· · · };
                                                        }
                                                        class ContainerWindow extends Window {
                                                          Window[] children;
                                                          boolean handleEvent(Event) {· · · };
                                                          void addChild(Window) {· · · };
                                                        }

Figure 1: Example Class Hierarchy

created. This paper just concentrates on the role of classes as templates for objects. The role of classes in downcasting is addressed in another paper [Gle99b]. The other roles, while important, are beyond the scope of this paper and are left to future work.

2. OBJECT TEMPLATE LANGUAGE

To begin, this section defines a language with primitive notions of objects and object templates. Object templates capture the role of classes as templates for objects. Consider the example class hierarchy shown in Figure 1 that includes classes from a hypothetical GUI toolkit. The class Window represents windows on the user’s screen and the class ContainerWindow represents windows that are the composition of a number of child windows. Class Window has a field containing the current position and size of the window and methods for handling user events and for determining if a pixel is within the window. Class ContainerWindow has a field containing the current children and a new method for adding children. Additionally, it overrides handleEvent perhaps to distribute the event to one of children according to screen location.

Class Window provides a template for objects with a field

                                                        extent and methods handleEvent and contains. Similarly,

ContainerWindow provides a template for objects with fields

                                                        extent and children and methods handleEvent, contains,

and addChild. One way to construct these templates is to start with the superclass’s template and then apply operations that add fields, add methods, and override methods. Since adding a field is not dependent upon the other fields or methods, adding a single field could be a basic operation. Adding or overriding methods, however, is not independent, because the new methods may refer to other methods being added. Therefore, the addition and overriding of several methods is the most basic operation. Using et to denote the empty template, + to denote field addition, and ← + to denote method addition and overriding, templates for Window and ContainerWindow are constructed as follows:

                                                           let Window_{t} =
                                                             et + extent : Rectangle
                                                               ← +[handleEvent = · · · , contains = · · ·] in
                                                           let ContainerWindow_{t} =
                                                             Window_{t} + children : array(Window)
                                                                    ← +[handleEvent = · · · , addChild = · · ·] in

Objects are created by instantiating classes, or more precisely, their templates. The new object will have all the fields and methods in the template and will respond to the methods according to the code given in the template. The instantiation operation must provide initial values for the fields as the template only lists the fields and their types. (Most object-oriented languages provide more sophisticated creation and initialisation mechanisms; these mechanisms are beyond the scope of this paper.) Writing instantiation as new template[field = initial value], objects from Window and ContainerWindow are created as follows:

let w1 = new Window_{t}[extent = r1] in

      let w2 = new ContainerWindow_{t}

[extent = r2, children = array()] in

where r1 and r2 are rectangles.

Objects are manipulated using the operations of method invocation, field selection, and field update. For example, the operation w2.addChild(w1) adds w1 as a child of w2.

The language informally described so far captures the key features of a single-inheritance class-based language such as Java. The rest of this section formalises an object template language called O, and the next section shows how to encode it into a language with records and functions. The term language of O is:

Expressions e ::= x |
et | e + f : σ | e ← +[m_{i} = M_{i}]_{i∈I} |
new e[f_{j} = e_{j}]_{j∈J} |
e.m | e.f | e_{1}.f := e_{2}
Methods  M ::= x.e:τ

Metavariable x ranges over term variables, m over method names, and f over field names.

In O, templates are values distinct from the objects that are created from them, and are built from the empty template by the operations of field addition and method addition/override. The empty template is written et; its instances have no fields and no methods. The operation e+f : σ adds field f with type σ to template e producing a new template. The template e must not have field f, and the new template has all the methods, method implementations, and fields of e, as well as field f with type σ. The operation e ← +[m_{i} = M_{i}]_{i∈I} adds or overrides methods m_{i} of template e with implementations M_{i}, producing a new template. The new template will have methods m_{i} with implementation M_{i} plus all the methods in e not in {m_{i}|i ∈ I}, as well as all fields of e. A method implementation M has the form x.e:τ. Unlike Java, O does not have an explicit keyword for self, but instead the programmer chooses a variable x and uses this variable to refer to self in the method body. In x.e:τ, x is the variable chosen to stand for self, e is the method body, and τ is the return type. If object o has x.e:τ as its implementation of method m then the method invocation o.m will result in the execution of e with x replaced by o. Note that methods are parameterless, Section 4 describes extensions of O with method parameters.

Objects are created by instantiating templates and can be manipulated by method invocation, field selection, and field update. Instantiation is written new e[f_{j} = e_{j}]_{j∈J}, where e is the template to be instantiated and e_{j} is the initial value of field f_{j}. The new object will respond to methods as dictated by template e. Method invocation is written e.m, field selection e.f, and field update e_{1}.f := e_{2}.

The type language of O is:

Types  τ, σ ::= tempt r | objt r
Rows r ::= [m_{i} : s_{i}; f_{j} : σ_{j}]_{i∈I,j∈J}
Signatures s  ::= τ

As templates are distinct from objects, they have their own types, which are different from the types for objects. Templates are given the type tempt r where r, called a row, describes the objects that result from instantiating the template. The row [m_{i}:s_{i}; f_{j}:σ_{j}]_{i∈I,j∈J} describes objects with methods m_{i} of signature s_{i} and fields f_{j} of type σ_{j}. The order of the methods and fields matters,^{1} so I and J can be thought of as ordered index sets. Methods in O are parameterless and just compute a result, so a signature is a type, the type of the result. Section 4 describes extensions of O with more complicated signatures. There is no interesting subtyping for template types as the operations on templates have conflicting subtyping requirements.

Objects have type objt r where r is a row as above. Object types have right-extension breadth subtyping: an object type with more methods on the right end and more fields on the right end is a subtype of an object type with less. Objects types also have depth subtyping for methods: methods of the subtype may have subsignatures of the methods of the supertype. Because fields are mutable, they have no depth subtyping. The following rule captures these properties:

k ∈ I_{2} : ⊢_{O} s_{k} ≤ s′_{k}

⊢_{O} objt[m_{i}:s_{i}; f_{j}:σ_{j}]_{i∈I_{1},j∈J_{1}} ≤ objt[m_{i}:s′_{i}; f_{j}:σ_{j}]_{i∈I_{2},j∈J_{2}}

where I_{2} is a prefix of I_{1} and J_{2} is a prefix of J_{1}.

Type checking terms is separated into two judgements: one for expressions and one for methods. (This separation along with the distinct syntactic classes for signatures and methods will facilitate later extensions of O with method arguments, type arguments, and self types.) Judgement Γ ⊢_{O}^{M} M : τ ⊳ s asserts that method implementation M has signature s when self has type τ or one of its subtypes. Type checking the template operations is fairly straightforward. The empty template has the empty template type tempt[; ]. The operation e+f:σ requires e to have a template type without field f, and the result type is the same template type but with f added. Method addition/override is more complicated. This operation is type checked by first computing the row for the new template, then checking that the method implementations are correct assuming self has the new row, and finally checking that any overridden methods have compatible signatures, that is, the overriding method has a subsignature of the overridden method. Formally, the typing rule is:

Γ ⊢_{O} e : tempt[m_{i}:s_{i}; f_{j}:σ_{j}]_{i∈I,j∈J}
k ∈ K :  Γ ⊢_{O}^{M} M_{k} : objt r′ ⊳ s′_{k}
k ∈ I ∩ K : ⊢_{O} s′_{k} ≤ s_{k}
Γ ⊢_{O} e ← +[m_{i} = M_{i}]_{i∈K} : tempt r′

where r′ = [m_{i}:s′′_{i}; f_{j}:σ_{j}]_{i∈(I,K−I),j∈J}, s′′_{i} = s_{i} if i ∈ I − K, and s′′_{i} = s′_{i} if i ∈ K.

Instantiation new e[f_{j} = e_{j}]_{j∈J} requires e to have a template type, {f_{j}|j ∈ J} to be exactly the fields in e’s type,

1The encoding is also correct if the order of methods and fields is unimportant, so long as the order of record fields in the target language is unimportant. and e_{j} to have the type of field f_{j}:

Γ ⊢_{O} e : tempt r Γ ⊢_{O} e_{j} : σ_{j}

Γ ⊢_{O} new e[f_{j} = e_{j}]_{j∈J} : objt r (r = [m_{i}:s_{i}; f_{j}:σ_{j}]_{i∈I,j∈J})

Method invocation e.m requires e to have an object type with method m and the result type is m’s signature. Field selection e.f requires e to have an object type with field f and the result type is f’s type. Field update e_{1}.f := e_{2} requires e_{1} to have an object type with field f, e_{2} to have f’s type, and the result type is e_{1}’s type.

Appendix A gives an operational semantics and a full set of typing rules for O. O could be given either a functional or an imperative semantics, and so long as the target language in the next section has the same kind of semantics, the encoding in the next section will be correct. Since a functional semantics is more concise, it is used in this paper. The typing rules are sound with respect to the operational semantics [Gle00a].

3. ENCODING O

This section presents a typed encoding of O into a language with records and functions, using the self-application semantics and the method-table technique. Before getting into formal details, this part of the section informally spells out the self-application semantics and method-table technique in more detail and discusses the issues that arise in trying to type them. These typing issues motivate a new type constructor, the self quantifier, as well as other features needed in the target language. Section 3.1 formalises the target language and Section 3.2 formalises the encoding.

This section informally describes the encoding, and sometimes uses the the formal translation syntax to refer to other parts of the encoding. Unfortunately, it is necessary to refer to some parts of encoding before they are defined. To ease the burden, here is a summary of the parts of the encoding, the formal translation syntax, and their intended meanings.

[[τ]]_{type}  The translation of type τ
[[r]]_{mt}(τ)  The record type of the method table

of a translated object where τ is the type of self

[[r]]_{full}(τ)  The record type of the translation of

an object where τ is the type of self

[[s]]_{sig}(τ)  The translation of signature s
[[e]]_{exp}  The translation of expression e
[[M]]_{mth}(τ) The translation of method body M where

τ is the type of self

Two of these deserve a little elaboration. Objects are translated into records, one of whose fields is the method table, also a record. The types [[r]]_{full}(τ) and [[r]]_{mt}(τ) are the respective record types for these records where τ is the type of self. The translation of object and template types use these types, but also have quantifiers to introduce self’s type as described later.

Under the self-application semantics, a method is compiled into a function taking an extra argument, and during method invocation the object itself is always passed as the extra argument. Thus, the method handleEvent in the class Window is compiled to a function of the following form,

named say Window::handleEvent:

λ(x:α, y:Event).b

where x is the extra self parameter, b is the body of the method, and α is, for now, a type variable that stands for the type of self. This function has type (α, Event) → bool. In a class-based language, all instances of a class have the same methods. In order to save space, objects share a structure with other instances of the class, the method table. A method table is a record with one field for each method the object responds to. For example, the Window class has a method table, named say Window::mt:

                                                                ⟨handleEvent = Window::handleEvent,
                                                                  contains = Window::contains⟩

and ContainerWindow has method table:

                                                            ⟨handleEvent = ContainerWindow::handleEvent,
                                                              contains = Window::contains,
                                                              addChild = ContainerWindow::addChild⟩

Using the suggested typing of Window::handleEvent, the method table Window::mt has type:

                                                         [[Window]]_{mt}(α) = ⟨handleEvent:(α, Event) → bool,

contains:(α, Point) → bool⟩ (1)

However, this type has a free α, and the encoding must somehow introduce this α. Abadi and Cardelli [AC96] observe that the methods in these method tables are polymorphic in the final object type, and so can be given an Fbounded polymorphic type [CCH^{+}89]. Using the [[r]]_{full}(α) type, Window’s method table gets type:

⟨handleEvent : ∀α ≤ [[Window]]_{full}(α).(α, Event) → bool,

contains : ∀α ≤ [[Window]]_{full}(α).(α, Point) → bool⟩

My encoding will use this idea with one twist. Instead of polymorphic methods, the method table itself is polymorphic. Thus Window’s method table has type:

∀α ≤ [[Window]]_{full}(α).⟨handleEvent : (α, Event) → bool,

                                                                              contains : (α, Point) → bool⟩

This means that a method table can be installed into an object simply by instantiating it at an appropriate type. In general [[temp r]]_{type} = ∀α ≤ [[r]]_{full}(α) . [[r]]_{mt}(α) and [[r]]_{mt}(α) is a record type with one entry for each method in r, which is a function taking an α to the result of that method:

[[[m_{i}:α.τ_{i}; f_{j}:σ_{j}]_{i∈I,j∈I}]]_{mt}(α) = ⟨m_{i}:α → [[τ_{i}]]_{type}⟩_{i∈I}

An object is a record with an entry for its class’s method table and an entry for each of its fields. For example, instances of Window and ContainerWindow would have the forms

                                                                    ⟨mt=Window::mt, extent=r_{1}⟩
                                                          ⟨mt=ContainerWindow::mt, extent=r_{2}, children=a⟩

respectively, where r_{1} and r_{2} are some rectangles and a is some array of Windows.

The type of an instance of Window has the form:

[[Window]]_{full}(α) = ⟨mt : [[Window]]_{mt}(α),

                                                                                 extent : Rectangle⟩

Again the issue is how to introduce α. Naively, this is the object type itself, so a recursive type should be used:

rec α.⟨mt : [[Window]]_{mt}(α), extent : Rectangle⟩ (2)

Unfortunately this does not work for the following reason. Consider a ContainerWindow instance, which also has type Window, it would have the following target type:

rec α.⟨mt : [[ContainerWindow]]_{mt}(α), extent : Rectangle,
children : array(Window)⟩

Since ContainerWindow is a subtype of Window, its translation must be a subtype of Window’s translation. This means that the above type should be a subtype of (2), but it is not. Type (2)’s body has a contravariant occurance of α (see (1)), so has no subtypes other than itself.

The problem is that the recursive type makes α, the type of self, equal to Window instead of the actual run-time type of the object. The solution is to somehow make α refer to this actual run-time type. To achieve this, I introduce a new^{2} type constructor, a self quantifier, instead of the recursive quantifier.

A self quantifier allows a type to refer to the actual runtime type of the value inhabiting it. The type self α.τ contains values v of type τ where α is the actual type of v. Using this quantifier, Window’s instances have type:

self α.⟨mt : [[Window]]_{mt}(α), extent : Rectangle⟩

In general [[obj r]]_{type} = self α.[[r]]_{full}(α) and [[r]]_{full}(α) is a record type with an entry for the method table and an entry for each field of r:

[[r]]_{full}(α) = ⟨mt:[[r]]_{mt}(α), f_{j}:[[σ_{j}]]_{type}⟩_{j∈J} where r = [m_{i}:τ_{i}; f_{j}:σ_{j}]_{i∈I,j∈I}

The only remaining issue is formalising self quantifiers. Abadi and Cardelli [AC96] provide a formulation of self quantifiers, but their formulation leads to the need for “recoup” fields and the inefficiencies of an extra field and an extra projection.^{3} The encoding needs a new formulation of self quantifiers that avoids the problems of recoup fields.

Abadi and Cardelli’s formulation involves two operations: one to introduce self quantifiers and one to eliminate them. The introduction form is pack e, σ as self α.τ (they call it “wrap”), and it produces an expression e packaged up with its actual self type σ. The typing rule is:

Δ; B; Γ ⊢_{F} e : σ Δ; B ⊢_{F} σ ≤ τ{α := σ}

Δ; B; Γ ⊢_{F} pack e, σ as self α.τ : self α.τ

where capture avoiding substitution of x for y in z is written z{y := x}. For σ to actually be e’s self type, e must have type σ. In addition e also must have type τ with α replaced by e’s self type, that is, e must have type τ{α := σ}. The latter is achieved by requiring that σ ≤ τ{α := σ}. Using pack, the translation of new Window_{t}[extent = r1] is:

pack ⟨mt = Window :: mt, extend = [[r1]]_{exp}⟩, rec α.[[Window]]_{full}(α) as self α.[[Window]]_{full}(α)

Here, the object’s run-time is rec α.[[Window]]_{full}(α). For this type to satisfy the requirements for packing into a self type, the condition Δ; B ⊢_{F} σ ≤ τ{α := σ} above, it must be

2Strictly speaking, self quantifiers were introduced by Abadi and Cardelli [AC96], but, as explained in this section, their formulation of self quantifiers is insufficient for the purposes of this paper, so a new formulation is needed. 3Note that the translation of objects given in this section under the interpretation of self quantifiers used by Abadi and Cardelli leads directly to Abadi, Cardelli, and Viswanathan’s encoding for an imperative calculus. the case that rec α.τ ≤ τ{α := rec α.τ}. This is true under an equirecursive interpretation of recursive types, that is, where rec α.τ = τ{α := rec α.τ}. The target language has this interpretation.

The elimination form is unpack α, x = e_{1} in e_{2} (they call it “use as”). Intuitively, the expression e_{1} is a value packaged with its self type, and unpack unpacks the value into x and the self type into α, and executes e_{2}. The typing rule is:

Δ; B; Γ ⊢_{F} e_{1} : self α.τ_{1}
Δ, α; B, α ≤ self α.τ_{1}; Γ, x : τ_{1} ⊢_{F} e_{2} : τ_{2}
Δ ⊢_{F} τ_{2}
Δ; B; Γ ⊢_{F} unpack α, x = e_{1} in e_{2} : τ_{2}

Notice that x is assumed to have type τ_{1}, but will be bound to a value whose actual run-time type could be a strict subtype of τ_{1}. For this reason, this unpack typing rule is too weak to type check method invocation. Consider the method invocation e.m where e has type obj r and m has signature τ in r. It is translated into unpack α, x = [[e_{1}]]_{exp} in x.mt.m x. Under the above rule, x.mt.m has type α → [[τ]]_{type}, but x has type [[r]]_{full}(α), which is a strict supertype of α.

The solution is to make a stronger assumption about x— that it has type α. This is sound because α is bound to the actual run-time type of the value bound to x. This stronger assumption leads to the rule:

Δ; B; Γ ⊢_{F} e_{1} : self α.τ_{1}
Δ, α; B, α ≤ τ_{1}; Γ, x : α ⊢_{F} e_{2} : τ_{2}
Δ ⊢_{F} τ_{2}
Δ; B; Γ ⊢_{F} unpack α, x = e_{1} in e_{2} : τ_{2}

Note, however, that the bound α ≤ τ_{1} has α on both the left and the right sides, that is, it is an F bound rather than an ordinary bound. Since the system must already deal with F-bounded polymorphism, these F bounds add no additional complexity. In fact, this use of F bounds brings a nice symmetry to the system, as F bounds are used in the typing of methods, and F bounds are used in the typing of method invocation.

Using this new rule, reconsider the translation of e.m:

unpack α, x = [[e]]_{exp} in x.mt.m x

During type checking of x.mt.m x, x has type α and α has bound [[r]]_{full}(α). Thus x.mt.m type checks and has type α → [[τ]]_{type}. Since x has type α, the application type checks.

Finally consider method addition/override. The translation of this operation needs to create a new method table that is a combination of an old method table and some new method implementations. There are two approaches: create a new record and copy the relevant entries from the old record, or have record operations for updating a field and for extending a record with a new field. Either approach would work, but I have chosen the second approach. Overridden methods translate into a record update operation that needs to produce a new record. Field update also translates into a record update operation. If the source language has applicative field update then this operation needs to produce a new record. If the source language has imperative field update then this operation needs to update in place. Even if the source language has applicative field update, the typing requirements for the translation of field update and the translation of method override are different and require different record update operations. Therefore, the target language has record extension and two record update operations in addition to projection and record formation.

Most class-based object-oriented language, unlike O, do not have first-class templates. In these languages, a method table is completely determined at compile time (link time in dynamic languages like Java) and the method tables can be built by the compiler and included in the static-data segment. In O this amounts to statically reducing template expressions to template values, which can then be translated into statically determined records and functions. Since O has first-class values, the translation presented in this paper treats the more general case.

3.1 Target Language

The target language, F_{self}, is a variant of the second-order typed lambda calculus with records, F-bounded polymorphism, self quantifiers, and recursive types. The syntax is:

Types  τ, σ ::= α | τ_{1} → τ_{2} | ⟨ℓ_{i} : τ_{i}^{ϕ_{i}}⟩_{i∈I}^{φ} |

∀α ≤ τ_{1}.τ_{2} | self α.τ | rec α.τ

Variances ϕ ::= + | ∘
φ ::= ∘ | →
Expressions e  ::= x | λx : τ.e | e_{1} e_{2} |

⟨ℓ_{i} = e_{i}⟩_{i∈I} | e.ℓ | e_{1}.ℓ ← e_{2} |

e_{1}.ℓ := e_{2} | e_{1} + ℓ = e_{2} |
Λα ≤ τ.e | e[τ] |
pack e, τ as self α.σ |
unpack α, x = e_{1} in e_{2}

The unusual features of F_{self} are its records, F-bounded polymorphism, self quantifiers, and equirecursive types. F_{self} contains an extensive set of record operations including projection, update, and extension. In order to have all these operations as well as breadth and depth subtyping, which is necessary for the encoding, record types must have a number of variances to keep everything straight. A record type ⟨ℓ_{i}:τ_{i}^{ϕ_{i}}⟩_{i∈I}^{φ} contains records with fields ℓ_{i} of type τ_{i}. The variance ϕ_{i} specifies the allowable operations on that field, + means projection only and ∘ allows both projection and update. The record variance φ specifies whether the type lists all of the fields of the value or just some of them. A record is in the type ⟨ℓ_{i}:τ_{i}^{ϕ_{i}}⟩_{i∈I}^{∘} only when it has exactly the fields ℓ_{i∈I}, but is in the type ⟨ℓ_{i}:τ_{i}^{ϕ_{i}}⟩\overrightarrow{i∈I} when it has at least the fields ℓ_{i∈I} and possibly more.

There are two record update operations. The operation e_{1}.ℓ := e_{2} can be interpreted imperatively or applicatively depending upon whether the source language has an imperative or applicative field update. Its typing rule is structural [AC96] (see also [HP98]), that is, the type of the result is the same as the type of e_{1}, which is required to be a subtype of a record type with a field ℓ that is mutable and e_{2} must have the type corresponding to ℓ:

\begin{matrix}Δ; B; Γ ⊢_{F} e_{1} : σ_{1} \\ Δ; B ⊢_{F} σ_{1} ≤ ⟨ℓ_{i}:τ_{i}^{ϕ_{i}}⟩_{i∈I}^{φ} \\ Δ; B; Γ ⊢_{F} e_{2} : τ_{k} \end{matrix} ; Δ; B; Γ ⊢_{F} e_{1}.ℓ_{k} := e_{2} : σ_{1} (k ∈ I; ϕ_{k} = ∘)

The operation e_{1}.ℓ ← e_{2}, on the other hand, always produces a new record, which is a copy of e_{1} with the ℓ field replaced by e_{2}. Its typing rule ignores the old type and variance of ℓ and the result type is a record type obtained from e_{1}’s by replacing the field ℓ with the type of e_{2}:

\begin{matrix}Δ; B; Γ ⊢_{F} e_{1} : ⟨ℓ_{i}:τ_{i}^{ϕ_{i}}⟩_{i∈I}^{φ} & Δ; B; Γ ⊢_{F} e_{2} : σ \\ Δ; B; Γ ⊢_{F} e_{1}.ℓ_{k} ← e_{2} : ⟨ℓ_{i}:τ′_{i}^{ϕ′_{i}}⟩_{i∈I}^{φ} \end{matrix} (k ∈ I)

where τ′_{i}^{ϕ′_{i}} = τ_{i}^{ϕ_{i}} if i ≠ k and τ′_{k}^{ϕ′_{k}} = σ^{∘}. Finally, the operation e_{1} + ℓ = e_{2} adds a new field ℓ with initial value e_{2} to record e_{1}. Record e_{1} must not contain a field ℓ, and the typing rule ensures this by using the exact record variance ∘:

\begin{matrix}Δ; B; Γ ⊢_{F} e_{1} : ⟨ℓ_{i}:τ_{i}^{ϕ_{i}}⟩_{i∈I}^{∘} & Δ; B; Γ ⊢_{F} e_{2} : σ \\ Δ; B; Γ ⊢_{F} e_{1} + ℓ = e_{2} : ⟨ℓ_{i}:τ_{i}^{ϕ_{i}}, ℓ:σ^{∘}⟩_{i∈I}^{∘} \end{matrix} (ℓ ∉ ℓ_{i∈I})

Polymorphic types ∀α ≤ τ_{1}.τ_{2} are F bounded [CCH^{+}89]. This means that α binds in both τ_{1} and τ_{2}, and that a type σ satisfies the bound if σ is a subtype of τ_{1}{α := σ}. Otherwise, they follow the standard rules for polymorphic types with the kernel-fun subtyping rule:

\begin{matrix}Δ, α ⊢_{F} τ & Δ, α; B, α ≤ τ; Γ ⊢_{F} e : σ \\ Δ; B; Γ ⊢_{F} Λα ≤ τ.e : ∀α ≤ τ.σ \end{matrix}

\begin{matrix}Δ; B; Γ ⊢_{F} e : ∀α ≤ τ_{1}.τ_{2} & Δ; B ⊢_{F} σ ≤ τ_{1}\{α := σ\} \\ Δ; B; Γ ⊢_{F} e[σ] : τ_{2}\{α := σ\} \end{matrix}

Recursive types rec α.τ contain values that have type τ where α refers to the recursive type rec α.τ. This is formalised by making a recursive type equal to its unrolling:

Δ ⊢_{F} rec α.τ = τ{α := rec α.τ}

The most novel aspect of F_{self} is its self quantifiers. A self quantified type is written self α.τ, and has a covariant subtyping rule:

Δ, α; B ⊢_{F} τ ≤ σ
Δ; B ⊢_{F} self α.τ ≤ self α.σ

Self quantified types are introduced by the pack operation and eliminated by the unpack operation. These operations have the semantics and typing rules discussed above.

Appendix B gives an operational semantics and a full set of typing rules for F_{self}. The typing rules are sound with respect to the operational semantics [Gle00a]. An alternative formulation of the target language with explicit coercions for recursive types is described in my dissertation [Gle00b]. Equirecursive types and F-bounds make decision procedures for subtyping far from obvious. However, there are algorithms for first and second-order systems with recursive types [AC93, KPS95, CG99]. I believe these results can be extended to F_{self}, but am still working out the details. Alternatively, a variation of F_{self} where recursive types and F-bounds are mediated by explicit coercions [Gle00b] is definitely decidable and practical. Also, the calculus of coercions [Cra99] could also be used to get a decidable version of F_{self}. F_{self} does not have a minimal types property because of the variances on fields. If the introduction form for records were ⟨ℓ_{i} = e_{i}:τ_{i}⟩_{i∈I} with a rule that required e_{i} to have type τ_{i} then F_{self} would have a minimal types property. The self quantifier developed in this paper could also be used in lower-level typed languages including typed target languages such as TAL [MWCG99, MCG^{+}99].

3.2 The Translation

The translation appears in Figure 2. Technically it is a type-directed translation and is defined by induction over an

[[tempt r]]_{type}  = ∀α ≤ [[r]]_{full}(α).[[r]]_{mt}(α, ∘)
[[objt r]]_{type}  = self α.[[r]]_{full}(α)
[[r]]_{mt}(τ, φ)  = ⟨m_{i}:[[s_{i}]]_{sig}(τ)^{+}⟩_{i∈I}^{φ}
[[r]]_{full}(τ)  = ⟨mt:[[r]]_{mt}(τ, →)^{+}, f_{j}:[[σ_{j}]]_{type}^{∘}⟩\overrightarrow{j∈J}
[[σ]]_{sig}(τ)  = τ → σ
[[x]]_{exp}  = x
[[et]]_{exp}  = ∀α ≤ ⟨mt:⟨⟩^{→+}⟩^{→}.⟨⟩
[[e + f:τ]]_{exp}  = ∀α ≤ [[r′]]_{full}(α).[[e]]_{exp}[α]
where e has type tempt[m_{i}:s_{i}; f_{j}:σ_{j}]_{i∈I,j∈J} and r′ is [m_{i}:s_{i}; f_{j}:σ_{j}, f:τ]_{i∈I,j∈J}
[[e ← +[m_{i} = M_{i}]_{i∈K}]]_{exp} = ∀α ≤ [[r′]]_{full}(α).([[e]]_{exp}[α].m_{i} ←_{i∈I∩K} [[M_{i}]]_{mth}(α) +_{i∈K−I} m_{i} = [[M_{i}]]_{mth}(α))
where e has type tempt[m_{i}:s_{i}; f_{j}:σ_{j}]_{i∈I,j∈J}, r′ is [m_{i}:s′′_{i}; f_{j}:σ_{j}]_{i∈(I,K−I),j∈J},
s′′_{i} = s′_{i} if i ∈ K, and s′′_{i} = s_{i} if i ∉ K
[[new e[f_{j} = e_{j}]_{j∈J}]]_{exp} = pack ⟨mt = [[e]]_{exp}[rec α.[[r]]_{full}(α)], f_{j} = [[e_{j}]]_{exp}⟩_{j∈J}, rec α.[[r]]_{full}(α) as [[objt r]]_{type}

where e has type tempt r

[[e.m]]_{exp}  = unpack α, x = [[e]]_{exp} in x.mt.m x

where α and x are fresh

[[e.f]]_{exp}  = unpack α, x = [[e]]_{exp} in x.f

where α and x are fresh

[[e_{1}.f := e_{1}]]_{exp}  = unpack α, x = [[e_{1}]]_{exp} in pack x.f := [[e_{2}]]_{exp}, α as [[objt r]]_{type}

where e_{1} has type objt r and α and x are fresh

[[x.e:σ]]_{mth}(τ)  = λx′:τ.let x = pack x′, τ as τ′ in [[e]]_{exp}

where x.e:σ has type τ′ ⊳ σ and x′ is fresh

Figure 2: The Translation

O typing derivation. However, I present it as a function of O expression syntax and indicate the typing assumptions. The proof of correctness contains a kind of coherence argument for the translation [Gle00a].

The translation uses the ideas developed in the introduction of this section. For a row r there are two important target types: [[r]]_{mt}(τ, φ) for method tables, and [[r]]_{full}(τ) for the objects. The record type of a method table is [[r]]_{mt}(τ, φ) where τ is the type of self and φ is the desired record variance. Exact record variance is used for object templates, because adding methods requires using the record extension operation, which requires exact record variance. Extensible record variance is used for objects in order to get depth subtyping. The record type of an object is [[r]]_{full}(τ) where τ is the type of self. As discussed, a template type is polymorphic over self, so is translated to ∀α ≤ [[r]]_{full}(α).[[r]]_{mt}(α, ∘). An object type uses a self quantifier, so is translated to self α.[[r]]_{full}(α).

At the term level, notice that field extension translates into a term with no operational effect. The effect of the type abstraction and application is to change the type to reflect the new bound on the self type. Method update and addition translates into a series of record extensions and ← updates. Note that these are done sequentially, and the mutual dependencies in the source language are resolved by the type application [[e]]_{exp}[α], where the new bound for α has the necessary type information about the other methods. Template instantiation is translated into record formation followed by packing into the appropriate self type. The method table is installed by instantiating it with a recursive type for the actual self type. The method invocation, field selection, and field update operations use unpack to open the self quantifier and then apply the appropriate record operations. Note that field update unpacks the object, updates, and then repacks it back into the appropriate self type.

The translation is both type preserving and operationally correct [Gle00a].

4. EXTENSIONS

The previous section presented an object and class encoding for a very simple object template language. This allowed the key ideas to be presented without being cluttered by extraneous source-language features. However, it begs the question of whether the ideas generalise to more advanced object-oriented constructs. In fact, they do and, except for self types, they generalise without requiring any new ideas. This section will demonstrate this by sketching a number of extensions.

It is worth noting that the encoding, as presented, works for either imperative or functional objects so long as the operation := in F_{self} is interpreted in the same way. Also note that any number of nonobject-oriented constructs could be added to the source and target languages and the translation extended to deal with them. Since the target language already has F-bounded polymorphism and recursive types, these could also be added to the source language and translation.

Now consider more object-oriented constructs. Method parameters could be added to O as follows:

\begin{aligned}s & ::= & (τ_{1}, …, τ_{n}) → τ \\ e & ::= & ⋯ | e.m(e_{1}, …, e_{n}) \\ M & ::= & x(x_{1} : τ_{1}, …, x_{n} : τ_{n}).b : τ \end{aligned}

To encode these method parameters F_{self} is extended with multiargument functions.^{4} Using (τ_{1}, …, τ_{n}) → τ for mul-

4Multiargument functions are theoretically equivalent to curried functions, but the implementations are vastly different, especially if closure conversion is done earlier than object encoding as I have suggested elsewhere [Gle99a]. tiargument function types, λ(x_{1} : τ_{1}, …, x_{n} : τ_{n}).b for multiargument functions, and e(e_{1}, …, e_{n}) for multiargument application the revised encoding is:

[[(τ_{1}, …, τ_{n}) → τ]]_{sig}(σ) =

(σ, [[τ_{1}]]_{type}, …, [[τ_{n}]]_{type}) → [[τ]]_{type} [[e.m(e_{1}, …, e_{n})]]_{exp} =

unpack α, x = [[e]]_{exp} in x.mt.m(x, [[e_{1}]]_{exp}, …, [[e_{n}]]_{exp})

[[x(x_{1} : τ_{1}, …, x_{n} : τ_{n}).b : τ]]_{mth}(σ) = λ(x′ : σ, x_{1} : [[τ_{1}]]_{type}, …, x_{n} : [[τ_{n}]]_{type}). let x = pack x′, σ as τ′ in [[b]]_{exp}

Type parameters can also be incorporated by encoding methods as polymorphic functions:

\begin{aligned}s & ::= & [α_{1} ≤ τ_{1}, …, α_{n} ≤ τ_{n}]τ \\ e & ::= & ⋯ | e.m[τ_{1}, …, τ_{n}] \\ M & ::= & x[α_{1} ≤ τ_{1}, …, α_{n} ≤ τ_{n}].b : τ \end{aligned}

[[[α_{1} ≤ τ_{1}, …, α_{n} ≤ τ_{n}]τ]]_{sig}(σ) =

∀α_{1} ≤ [[τ_{1}]]_{type}…. ∀α_{n} ≤ [[τ_{n}]]_{type}.σ → τ [[e.m[τ_{1}, …, τ_{n}]]]_{exp} =

unpack α, x = [[e]]_{exp} in x.mt.m[[[τ_{1}]]_{type}] ⋯ [[[τ_{n}]]_{type}] x

[[x[α_{1} ≤ τ_{1}, …, α_{n} ≤ τ_{n}].b : τ]]_{mth}(σ) = Λα_{1} ≤ [[τ_{1}]]_{type}…. Λα_{n} ≤ [[τ_{n}]]_{type}.λx′ : σ. let x = pack x′, σ as τ′ in [[b]]_{exp}

Covariant self types could be added to O by allowing signatures of the form α.τ where α may occur only positively in τ. Method bodies would have the form α, x.b : τ where α is a type variable that binds in b and stands for the type of self. The rule for method invocation would become:

{Δ; B ⊢_{O} e : τ \atop Δ; B ⊢_{O} e.m_{k} : τ_{k}\{α_{k} := τ\}}

where τ = objt[m_{i}:s_{i}; f_{j}:σ_{j}]_{i∈I,j∈J}, k ∈ I, and s_{k} = α_{k}.τ_{k}. To encode this variant of O into F_{self}, a deeper form of pack is needed. The deeper form of pack is written pack e, τ′[α := τ] as self α.σ and coerces an expression of type τ′{α := τ} into τ′{α := self α.σ} when α occurs only positively in τ′ and τ ≤ σ{α := τ}. The details are messy, but the essence of the new translation is:

[[α.τ]]_{sig}(σ) = σ → ([[τ]]_{type}{α := σ})
[[e.m]]_{exp}  = unpack α, x = [[e]]_{exp} in

pack x.mt.m x, [[σ]]_{type}[α := α] as [[τ]]_{type}

Where e has type τ and m’s signature in τ is α.σ. The translation could probably be extended to a structural rule for method invocation given a structural rule for unpack, details appear elsewhere [Gle00a]. The above type translation for self types is compatible with contravariant self types, but it is unclear what to do at the term level. This is unsurprising, since formulating object languages with contravariant self types and subsumption is problematic [Coo89b][AC96, §2.8 and §3.5].

O allows no depth subtyping in fields. O could use variances, as in F_{self}, to lift this restriction. Rows would have the form [m_{i} : s_{i}; f_{j} : σ_{j}^{ϕ_{j}}]_{i∈I,j∈J} and subtyping would now be:

\begin{aligned}i ∈ I_{2} : & ⊢_{O} s_{i} ≤ s′_{i} \\ j ∈ J_{2} : & ⊢_{O} σ_{j}^{ϕ_{j}} ≤ σ′_{j}^{ϕ′_{j}} \end{aligned} ; \begin{matrix}⊢_{O} [m_{i} = s_{i}; f_{j} = σ_{j}^{ϕ_{j}}]_{i∈I_{1},j∈J_{1}} ≤ \\ [m_{i} = s′_{i}; f_{j} = σ′_{j}^{ϕ′_{j}}]_{i∈I_{2},j∈J_{2}} \end{matrix}

where I_{1} is a prefix of I_{2} and J_{1} a prefix of J_{2}. The field extension operation would now have a variance e + f : σ^{ϕ}, and a field override operation is now possible: e.f := σ^{ϕ} where σ^{ϕ} is a subtype/variance of the current type and variance of f in e. The translation then becomes:

[[r = [m_{i}:s_{i}; f_{j}:σ_{j}^{ϕ_{j}}]_{i∈I,j∈J}]]_{full}(τ) =
⟨mt:[[r]]_{mt}(τ, →)^{+}, f_{j}:[[σ_{j}]]_{type}^{ϕ_{j}}⟩_{j∈J}
[[e.f := σ^{ϕ}]]_{exp} =
∀α ≤ [[r′]]_{full}(α).[[e]]_{exp}[α]

where e.f := σ^{ϕ} has type tempt r′.

In a similar way, O could have variances on methods and allow method override on objects. Method override on objects is incompatible with the method-table technique. However, a version of the encoding that just uses the selfapplication semantics and not the method-table technique could easily incorporate method override. In fact, any of Abadi and Cardelli’s pure object languages [AC96] can be encoded into suitable variants of O and thus be encoded using ideas in this paper. I believe that method extension on objects could also be incorporated, but initial investigation has revealed the need for some unusual structural rules for record extension. I leave for future work a full investigation of this possibility.

It is worth remarking that the encoding can be combined with object closure conversion [Gle99a] and an encoding of functions as objects to provide a typed translation of closure-passing-style closure conversion. In particular, a function of type τ_{1} → τ_{2} translates into a closure of type self α.⟨(α, [[τ_{1}]]_{type}) → [[τ_{2}]]_{type}⟩.

The templates in O allow only single inheritance and concrete methods. To finish this section, I will sketch a couple of generalisations that would allow abstract methods and multiple inheritance. The first generalisation separates the assumptions a template makes from what it provides. In this version, template values consist of a row that specifies the assumptions the template makes about the eventual object and a list of methods and methods bodies, thus a form like temp(r; m_{i} = M_{i})_{i∈I}. Template types would mention both the assumptions and list of provided methods and signatures, as in tempt(r; m_{i}:s_{i})_{i∈I}. There would be a template operation for strengthening the assumptions made, say e := r, where e has type tempt(r′; m_{i} = M_{i})_{i∈I} and r is a subtype of r′. The method override and addition operations would be broken into operations to add single methods, e + m = M, and override single methods, e.m := M. The instantiation operation would check that all assumptions made about methods are provided by the template being instantiated. The following rule ensures this where r = [m_{i}:s_{i}; f_{j}:σ_{j}]_{i∈I,j∈J}:

Γ ⊢_{O} e : tempt(r; m_{i}:s′_{i})_{i∈I} ⊢_{O} s′_{i} ≤ s_{i} Γ ⊢_{O} e_{j} : σ_{j}
Γ ⊢_{O} new e[f_{j} = e_{j}]_{j∈J} : objt r

The translation could probably be revised based on the following type translation:

[[tempt(r; m_{i} : s_{i})_{i∈I}]]_{type} = ∀α ≤ [[r]]_{full}(α).⟨m_{i} : [[s_{i}]]_{sig}(α)^{+}⟩_{i∈I}^{∘}

I leave it to future work to flesh out these ideas.

The second generalisation is to introduce a template combining operation e_{1} + e_{2}. There are two possible interpretations for this operation, one could require e_{1} and e_{2} to provide disjoint sets of methods, the other could allow e_{2} to override e_{1}. Taking the disjoint approach, a typing rule for this operation might be, where m_{i∈I} ∩ m′_{j∈J} = ∅:

Γ ⊢_{O} e_{1} : tempt(r; m_{i}:s_{i})_{i∈I} Γ ⊢_{O} e_{2} : tempt(r; m′_{j}:s′_{j})_{j∈J}

Γ ⊢_{O} e_{1} + e_{2} : tempt(r; m_{i}:s_{i}, m′_{j}:s′_{j})_{i∈I,j∈J}

Translating this operation requires a record combining operation with similar properties. Again, I leave to future work the exploration of these ideas. Note that right-extension breadth subtyping limits the usefulness of these combining operations and should be abandoned in favour of arbitrary breadth subtyping. The translation, as stated in the previous section, works for O with arbitrary breadth subtyping so long as F_{self} also has arbitrary breadth subtyping.

5. PREVIOUS WORK

5.1 Object Encodings

An object encoding should preserve the meaning of programs, and for typed translations must preserve both typing and subtyping. For use as foundations for language implementation, an encoding should also be efficient, and for use in certifying compilers, full abstraction is a useful property. In addition to these requirements, object encodings can be compared according to the features of the source language that they can encode. Bruce et al. [BCP99] provide an excellent comparison of most of the known object encodings.

Cardelli [Car88] proposed the first typed object encoding. In his encoding, an object is a record that can recursively refer to itself, often called a recursive record interpretation. At the type level, an object type is the fixed point of a record type whose elements are the methods’ types. The encoding preserves meaning, typing, and subtyping, but it cannot encode method update, which is used to encode inheritance. The recursive records interpretation was pursued by Reddy [Red98, KR94], Cook [Coo89a, CHC90], the Hopkins Object Group [ESTZ95], and others.

Pierce and Turner [PT94] proposed a simple object and class encoding that requires existential types but not recursive types. At the term level, an object has two parts: a private state component and a public method suite. The functions that encode methods are passed the state of self but not self’s method suite. Calls to other methods of self must be hardwired at the time the object is created, and the class encoding arranges this. Furthermore, if a method’s return type is the self type, then the function returns only the state component, and the method invocation sites must repackage the object. This encoding is the only encoding with a nonuniform translation of method invocation. The encoding preserves meaning, typing, and subtyping, but it cannot encode method update. The lack of method update is not a concern because a separate class encoding deals with inheritance. Finally, methods can be both private and public, but mutable fields can only be private, as public fields would not be passed to the methods’ functions. Thus, in a sense, the encoding is for a different object model than Cardelli considered.

Bruce et al. [Bru94, BSvG95] designed a functional and an imperative class-based object-oriented language, and the denotational semantics for these languages can be seen as an object and class encoding. Like Pierce and Turner’s encoding, the encoding has a complementary class encoding for dealing with inheritance. The encoding is very similar to Pierce and Turner’s, but methods whose result type is the self type return the whole object not just the state component. Thus, the translation of an object type is like Pierce and Turner’s but wrapped with an extra fixed point. Bruce et al. also argue for the use of matching rather than subtyping, which has many advantages, but leads to a different object and class model than Cardelli or Pierce and Turner’s.

Rémy [Rém94, RV97] uses a variant of Pierce and Turner’s encoding with row variables. Row variables are used to specify polymorphism over the type of self, and enable a natural extension of ML that includes objects and classes without sacrificing type inference. However, this system does not include subsumption: an object must be explicitly coerced from a subtype to a supertype.

In 1996, Abadi, Cardelli, and Viswanathan discovered an adequate typed object encoding for objects with method invocation and method update [ACV96]. This encoding uses bounded existential types and recursive types to effectively encode self’s type. However, the technique requires, purely for typing purposes, an additional projection and an additional field.

Abadi et al.’s encoding is also not fully abstract; in particular, the translation of method update allows the target language to distinguish objects that were indistinguishable in the source language. Viswanathan [Vis98] fixed this problem, but by introducing considerably more computation.

Concurrently with the work of this paper, Hickey, Crary, and League et al. have proposed typed encodings of the self-application semantics. Hickey [Hic] shows how to type the self-application semantics in the Nuprl type theory, using an intersection type to make methods polymorphic over the type of self. However, the Nuprl type theory is undecidable, so it is not clear how to use this encoding in a type-directed compiler. Crary [Cra99] shows how to use unbounded existential and binary intersection types to type the self application semantics. League et al. [LST99] show how to type the self application semantics using existentially quantified row variables and recursive types. They also show how to deal with classes, as described below. Both Crary and League et al.’s ideas can be seen as encodings of the self quantifier introduced in this paper.

5.2 Class Encodings

Abadi and Cardelli [AC96] show informally how to encode classes into their pure object calculi. In the encoding, a class becomes an object with premethods^{5} for each of the instance’s methods and a new method for instantiating the class. The new method copies the premethods into a newly created object. Subclasses copy the premethods of the superclass that they inherit and provide their own premethods for overridden or addition methods. F-bounded polymorphism is used to type the premethods. This encoding shows

5A premethod for a method is a function that takes self as an argument and computes the methods. that classes add no expressiveness to a pure object calculus, but does not faithfully encode the efficient method-table technique.

Fisher and Mitchell with others [Fis96, Mit90, FHM94, FM95a, FM95b, FM96, BF98, FM98] have pursued a line of research into encoding classes as extensible objects. The object calculi they consider have a method extension operation for adding a new method to an already existing object. This construct does not appear in the object calculi usually considered for object encodings. Method extension interacts poorly with breadth subtyping, and so extensible object calculi need to have complicated type systems for tracking the absence of methods. Often a distinction is made between prototype objects, which are extensible but do not have breadth subtyping, and proper objects, which are not extensible but do have breadth subtyping. Like Abadi and Cardelli’s class encoding, these encodings show that classes do not add expressiveness, and also provide a good basis for the design and definition of languages. However, also like Abadi and Cardelli’s encoding, they do not lead directly to efficient implementations. In particular, class instantiation involves creating an empty object, and then adding all its methods to the object.

Pierce and Turner’s class encoding [PT94], unlike the previous two approaches, encodes classes directly into records and functions and not into objects. Recall that in their encoding, an object consists of a public method suite and a private state component. A class is encoded as a function f that returns the public method suite for objects in that class. The public methods may want to invoke other public methods of self, so f takes another method suite s as an argument, and uses s to do method invocations on self. To instantiate a class, the fixed point of f is used as the public method suite of the new object along with an appropriate initial state component. However, subclasses may have more fields than superclasses, so f is parameterised by functions that convert between the final representation and the one the current class defines. Unfortunately, these conversion functions persist beyond class instantiation time and in general are evaluated every time a method is invoked, making this encoding particularly inefficient. Later work [HP95] shows how to avoid some of these problems.

Bruce et al.’s class encoding [Bru94, BSvG95] essentially encodes a class as a pair containing both the initial values of the private fields of the class and a function for the public methods. Additionally the pair is polymorphic in the final object type and the type of the private fields. The function for the public methods takes the final object and returns a record of the results of each method. Similarly to Pierce and Turner, class instantiation requires taking the fixed point of the function for the public methods to produce a function from the private state to the method suite, and then packaging this function with the initial private state. This encoding also results in inefficiencies.

Concurrently with the work of this paper, League et al. show how to encode a subset of the Java class model into a variant of F_{ω} [LST99]. A class is encoded as a method table (they call it a dictionary), a function to initialise the class’s private fields, and a function to instantiate the class. Using a combination of row polymorphism and existential types, they are able to encode class private fields and their work can probably be extended to handle most of Java’s protection modifiers.

Reppy and Reicke [RR96a] show how to encode classes as modules in the SML module system extended with objects in the core language [RR96b]. Their encoding is essentially the same as Abadi and Cardelli’s, but with some twists for handling protection. Vouillon [Vou98] shows how to combine the classes and modules of Objective ML [RV97] into a single construct.

6. CONCLUSION

This paper presented a small language with the key features of a class-based object-oriented language and a typed encoding of this language into a language with records and functions. The encoding uses the self-application semantics and method-table techniques, providing a typed formalisation for both. Section 4 showed how to incorporate a number of extensions and variants into the template language and the encoding. This provides evidence that the ideas of this paper provide a nice framework for the description of classbased languages and their implementation and that the use of self quantifiers is the right way to type self application.

7. REFERENCES

[AC93] Roberto Amadio and Luca Cardelli. Subtyping recursive types. ACM Transactions on Progamming Languages and Systems, 15(4):575–631, September 1993.

[AC96] Martín Abadi and Luca Cardelli. A Theory Of Objects. Springer-Verlag, 1996.

[ACV96] Martín Abadi, Luca Cardelli, and Ramesh Viswanathan. An interpretation of objects and object types. In 23rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 396–409, January 1996.

[BCP99] Kim Bruce, Luca Cardelli, and Benjamin Pierce. Comparing object encodings. Information and Computation, 155(1/2):108–133, 1999.

[BF98] Viviana Bono and Kathleen Fisher. An imperative, first-order calculus with object extension. In 5th International Workshop on Foundations of Object Oriented Programming Languages, pages 8–1 to 8–13, San Diego, California, USA, January 1998.

[Bru94] Kim Bruce. A paradigmatic object-oriented programming language: Design, static typing and semantics. Journal of Functional Programming, 4(2):127–206, April 1994.

[BSvG95] Kim Bruce, Angela Schuett, and Robert van Gent. PolyTOIL: A type-safe polymorphic object-oriented language. In 1995 European Conference on Object-Oriented Programming, volume 952 of Lecture Notes in Computer Science, pages 27–51. Springer-Verlag, 1995.

[Car88] Luca Cardelli. A semantics of multiple inheritance. Information and Computation, 76(2/3):138–164, 1988. Also published in volume 173 of Lecture Notes in Computer Science, pages 51–67, 1984. [CCH^{+}89] Peter Canning, William Cook, Walter Hill,

John Mitchell, and Walter Olthoff. F-bounded quantification for object-oriented programming. In 4th ACM Conference on Functional Programming and Computer Architecture, pages 273–280, London, UK, September 1989. ACM Press.

[CG99] Dario Colazzo and Giorgio Ghelli. Subtyping recursive types in kernel fun. In 1999 Symposium on Logic in Computer Science, pages 137–146, Trento, Italy, July 1999.

[CHC90] William Cook, Walter Hill, and Peter Canning. Inheritance is not subtyping. In 17th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 125–135. ACM Press, January 1990.

[Coo89a] William Cook. A Denotational Semantics of Inheritance. PhD thesis, Brown University, 1989.

[Coo89b] William Cook. A proposal for making Eiffel type-safe. In 3rd European Conference on Object-Oriented Programming, pages 57–72, Nottingham, UK, July 1989. Cambridge University Press.

[Cra99] Karl Crary. Simple, efficient object encoding using intersection types. Technical Report CMU-CS-99-100, Carnegie Mellon University, Pittsburgh, PA 15213, USA, 1999.

[ESTZ95] Jonathan Eifrig, Scott Smith, Valery Trifonov, and Amy Zwarico. An interpretation of typed oop in a language with state. Lisp and Symbolic Computation, 8(4):357–397, 1995.

[FHM94] Kathleen Fisher, F. Honsell, and John Mitchell. A lambda calculus of objects and method specialization. Nordic Journal of Computing, 1:3–37, 1994. Preliminary version appeared in IEEE Symposium on Logic in Computer Science, 1993, 26–38.

[Fis96] Kathleen Fisher. Type Systems for object-oriented programming languages. PhD thesis, Stanford University, California 94305, USA, 1996.

[FM95a] Kathleen Fisher and John Mitchell. A delegation-based object calculus with subtyping. In 10th International Conference on Fundamentals of Computation theory, volume 965 of Lecture Notes in Computer Science, pages 42–61. Springer-Verlag, 1995.

[FM95b] Kathleen Fisher and John Mitchell. The development of type systems for object-oriented languages. Theory and Practice of Object Systems, 1(3):189–220, 1995.

[FM96] Kathleen Fisher and John Mitchell. Classes = objects + data abstraction. Technical Report STAN-CS-TN-96-31, Stanford University, California 94305, USA, 1996.

[FM98] Kathleen Fisher and John Mitchell. On the relationship between classes, objects, and data abstraction. Theory and Practice of Object Systems, 1998. To appear.

[GJS96] James Gosling, Bill Joy, and Guy Steele. The Java Language Specification. Addison-Wesley, 1996.

[Gle99a] Neal Glew. Object closure conversion. In Andrew Gordon and Andrew Pitts, editors, 3rd International Workshop on Higher Order Operational Techniques in Semantics, volume 26 of Electronic Notes in Theoretical Computer Science, Paris, France, September

1999. Elsevier. http://www.elsevier.nl/
locate/entcs/volume26.html.

[Gle99b] Neal Glew. Type dispatch for named hierarchical types. In 4th ACM SIGPLAN International Conference on Functional Programming, Paris, France, September 1999.

[Gle00a] Neal Glew. An efficient class and object encoding. Technical Report STAR-TR-00.07-02, STAR Lab, InterTrust Technologies Corporation, 4750 Patrick Henry Drive, Santa Clara, CA 95054-1851, USA, July 2000.

[Gle00b] Neal Glew. Low-Level Type Systems for Modularity and Object-Oriented Constructs. PhD thesis, Cornell University, 4130 Upson Hall, Ithaca, NY 14853-7501, USA, January 2000.

[Hic] Jason Hickey. Predicative type-theoretic interpretation of objects. Unpublished,

author’s contact: jyh@cs.cornell.edu.

[HP95] Martin Hoffman and Benjamin Pierce. Positive subtyping. In 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 186–197, San Francisco, CA, USA, January 1995. ACM Press.

[HP98] Martin Hofmann and Benjamin Pierce. Type destructors. In 5th International Workshop on Foundations of Object Oriented Programming Languages, pages 3–1 to 3–11, San Diego, CA, USA, January 1998.

[Kam88] Samuel Kamin. Inheritance in smalltalk-80: A denotational definition. In 15th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 80–87, San Diego, CA, USA, January 1988.

[KPS95] Dexter Kozen, Jens Palsberg, and Michael Schwartzbach. Efficient recursive subtyping. Mathematical Structures in Computer Science, 5(1):113–125, March 1995.

[KR94] Samuel Kamin and Uday Reddy. Two semantic models of object-oriented languages. In Carl Gunter and John Mitchell, editors, Theoretical Aspects of Object-Oriented Programming: Types, Semantics, and Language Design, pages 464–495. MIT Press, Cambridge, MA 02142, 1994.

[LST99] Christopher League, Zhong Shao, and Valerey Trifonov. Representing java classes in a typed intermediate language. In 1999 ACM SIGPLAN International Conference on Functional Programming, Paris, France, September 1999. ACM Press.

[MCG^{+}99] Greg Morrisett, Karl Crary, Neal Glew, Dan Grossman, Richard Samuels, Frederick Smith, David Walker, Stephanie Weirich, and Steve Zdancewic. TALx86: A realistic typed assembly language. In ACM SIGPLAN Workshop on Compiler Support for System Software, volume 0228 of INRIA Research Reports, Atlanta, GA, USA, May 1999.

[Mit90] John Mitchell. Toward a typed foundation for method specialization and inheritance. In 17th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 109–124. ACM Press, January 1990.

[MTC^{+}96] Greg Morrisett, David Tarditi, Perry Cheng, Christopher Stone, Robert Harper, and Peter Lee. The TIL/ML compiler: Performance and safety through types. In ACM SIGPLAN Workshop on Compiler Support for System Software, Tucson, AZ, USA, February 1996.

[MWCG99] Greg Morrisett, David Walker, Karl Crary, and Neal Glew. From System F to typed assembly language. ACM Transactions on Progamming Languages and Systems, 21(3):528–569, May 1999.

[NL98] George Necula and Peter Lee. The design and implementation of a certifying compiler. In ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 333–344, Montreal, Canada, June 1998.

[PT94] Benjamin Pierce and David Turner. Simple type-theoretic foundations for object-oriented programming. Journal of Functional Programming, 4(2):207–247, April 1994. An early version appeared in POPL’93, pages 299–312.

[Red98] Uday Reddy. Objects as closures: Abstract semantics of object-oriented languages. In ACM Symposium on LISP and Functional Programming, pages 289–297. ACM, July 1998.

[Rém94] Didier Rémy. Programming objects with ML-ART, an extension to ML with abstract and record types. In Masami Hagiya and John Mitchell, editors, International Symposium on Theoretical Aspects of Computer Science, volume 789 of Lecture Notes in Computer Science, pages 321–346, Sendai, Japan, April 1994. Springer-Verlag.

[RR96a] John Reppy and Jon Riecke. Classes in Object ML via modules. In 3rd International Workshop on Foundations of Object Oriented Programming Languages, New Brunswick, NJ, USA, July 1996.

[RR96b] John Reppy and Jon Riecke. Simple objects for Standard ML. In 1996 ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 171–180. ACM Press, 1996.

[RV97] Didier Rémy and Jérôme Vouillon. Objective ML: A simple object-oriented extension of ML. In 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 40–53, Paris, France, January 1997.

[TMC^{+}96] David Tarditi, Greg Morrisett, Perry Cheng, Christopher Stone, Robert Harper, and Peter Lee. TIL: A type-directed optimizing compiler for ML. In 1996 ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 181–192, Philadelphia, PA, USA, May 1996. ACM Press.

[Vis98] Ramesh Viswanathan. Full abstraction for first-order objects with recursive types and subtyping. In 13th Symposium on Logic in Computer Science, 1998.

[Vou98] Jérôme Vouillon. Using modules as classes. In 5th International Workshop on Foundations of Object Oriented Programming Languages, pages 4–1 to 4–10, San Diego, CA, USA, January 1998.

APPENDIX

A. O SEMANTICS

The operational semantics for the template language appears in Figure 3. Capture avoiding substitution of x for y in z is written z{y := x}.

A.1 Subtyping rules

⊢_{O} tempt r ≤ tempt r
i ∈ I_{2} : ⊢_{O} s_{i} ≤ s′_{i}

⊢_{O} objt[m_{i}:s_{i}; f_{j}:σ_{j}]_{i∈I_{1},j∈J_{1}} ≤ objt[m_{i}:s′_{i}; f_{j}:σ_{j}]_{i∈I_{2},j∈J_{2}}

where I_{1} is a prefix of I_{2} and J_{1} is a prefix of J_{2}.

A.2 Expression Typing

A typing context Γ is a list of variables and their types, x_{1}:τ_{1}, …, x_{n}:τ_{n}, where the variables are distinct.

\begin{matrix}Γ ⊢_{O} e : τ_{1} & ⊢_{O} τ_{1} ≤ τ_{2} \\ Γ ⊢_{O} e : τ_{2} \end{matrix}  Γ ⊢_{O} x : τ (Γ(x) = τ)

Γ ⊢_{O} et : tempt[; ]
Γ ⊢_{O} e : tempt[m_{i}:s_{i}; f_{j}:σ_{j}]_{i∈I,j∈J}

Γ ⊢_{O} e + f : σ : tempt[m_{i}:s_{i}; f_{j}:σ_{j}, f:σ]_{i∈I,j∈J} (f ∉ f_{j∈J})

Γ ⊢_{O} e : tempt[m_{i}:s_{i}; f_{j}:σ_{j}]_{i∈I,j∈J}
i ∈ K :  Γ ⊢_{O}^{M} M_{i} : objt r′ ⊳ s′_{i}
i ∈ I ∩ K : ⊢_{O} s′_{i} ≤ s_{i}
Γ ⊢_{O} e ← +[m_{i} = M_{i}]_{i∈K} : tempt r′

where r′ = [m_{i}:s′′_{i}; f_{j}:σ_{j}]_{i∈(I,K−I),j∈J}, s′′_{i} = s_{i} if i ∈ I − K, and s′′_{i} = s′_{i} if i ∈ K.

Γ ⊢_{O} e : tempt r Γ ⊢_{O} e_{j} : σ_{j}

Γ ⊢_{O} new e[f_{j} = e_{j}]_{j∈J} : objt r (r = [m_{i}:s_{i}; f_{j}:σ_{j}]_{i∈I,j∈J})

{Γ ⊢_{O} e : objt[m_{i}:s_{i}; f_{j}:σ_{j}]_{i∈I,j∈J} \atop Γ ⊢_{O} e.m_{k} : s_{k}} (k ∈ I)

{Γ ⊢_{O} e : objt[m_{i}:s_{i}; f_{j}:σ_{j}]_{i∈I,j∈J} \atop Γ ⊢_{O} e.f_{k} : σ_{k}} (k ∈ J)

\begin{matrix}Γ ⊢_{O} e_{1} : τ_{1} & Γ ⊢_{O} e_{2} : σ_{k} \\ Γ ⊢_{O} e_{1}.f_{k} := e_{2} : τ_{1} \end{matrix} (k ∈ J)

Additional syntactic constructs:

Values  v, w ::= temp[m_{i} = M_{i}; f_{j}:σ_{j}]_{i∈I,j∈J} | obj[m_{i} = M_{i}; f_{j} = v_{j}]_{i∈I,j∈J}
Contexts E ::= \{\} | E + f : σ | E ← +[m_{i} = M_{i}]_{i∈I} | new E[f_{j} = e_{j}]_{j∈J} | new v[\overrightarrow{f = v}, f = E, \overrightarrow{f′ = e}] |
E.m | E.f | E.f := e | v.f := E

Reduction rules:

E{ι} ↦ E{e} where:

ι e Side Conditions
et  temp[; ]
temp[m_{i} = M_{i}; f_{j}:σ_{j}]_{i∈I,j∈J} + f : σ  temp[m_{i} = M_{i}; f_{j}:σ_{j}, f:σ]_{i∈I,j∈J}  f ∉ f_{j∈J}
temp[m_{i} = M_{i}; f_{j}:σ_{j}]_{i∈I,j∈J} ← +[m_{k} = M′_{k}]_{k∈K} temp[m_{l} = M′′_{l}; f_{j}:σ_{j}]_{l∈(I,K−I),j∈J} M′′_{l} = \{ \begin{matrix}M_{l} & l ∈ I − K \\ M′_{l} & l ∈ K \end{matrix}
new temp[m_{i} = M_{i}; f_{j}:σ_{j}]_{i∈I,j∈J}[f_{j} = w_{j}]_{j∈J} obj[m_{i} = M_{i}; f_{j} = w_{j}]_{i∈I,j∈J}
obj[m_{i} = M_{i}; f_{j} = w_{j}]_{i∈I,j∈J}.m_{k}  e_{k}{x_{k} := v_{2}}  k ∈ I
obj[m_{i} = M_{i}; f_{j} = w_{j}]_{i∈I,j∈J}.f_{k}  w_{k}  k ∈ J, M_{k} = x_{k}.e_{k}:τ_{k}
obj[m_{i} = M_{i}; f_{j} = w_{j}]_{i∈I,j∈J}.f_{k} := v  obj[m_{i} = M_{i}; f_{j} = w′_{j}]_{i∈I,j∈J}  k ∈ J; w′_{j} = \{ \begin{matrix}w_{j} & j ≠ k \\ v & j = k \end{matrix}

Figure 3: Object Template Language Operational Semantics

where τ_{1} = objt[m_{i}:s_{i}; f_{j}:σ_{j}]_{i∈I,j∈J}.

{Γ, x : σ ⊢_{O} e : τ \atop Γ ⊢_{O}^{M} x.e:τ : σ ⊳ τ}

B. F_{self} SEMANTICS

The operational semantics for the target language appears in Figure 4.

B.1 Type well formedness

Δ ⊢_{F} τ (ftv(τ) ⊆ Δ)

where ftv(τ) are the free type variables of τ.

B.2 Equality Rules

Along with the usual reflexivity, transitivity, and congruence rules, F_{self} has the following equality rules.

{Δ ⊢_{F} τ \atop Δ ⊢_{F} τ = σ\{α := τ\}} (τ = rec α.σ)

\begin{matrix}Δ ⊢_{F} τ\{α := σ_{1}\} = σ_{1} & Δ ⊢_{F} τ\{α := σ_{2}\} = σ_{2} \\ Δ ⊢_{F} σ_{1} = σ_{2} \end{matrix} (τ ↓ α)

Where τ ↓ α means that τ is syntactically contractive in α, that is, there is a function, record, polymorphic type constructor, or self quantifier before any occurrences of α.

B.3 Subtyping Rules

{Δ; B ⊢_{F} τ_{1} = τ_{2} \atop Δ; B ⊢_{F} τ_{1} ≤ τ_{2}}  \begin{matrix}Δ; B ⊢_{F} τ_{1} ≤ τ_{2} & Δ; B ⊢_{F} τ_{2} ≤ τ_{3} \\ Δ; B ⊢_{F} τ_{1} ≤ τ_{3} \end{matrix}

Δ; B ⊢_{F} α ≤ τ (α ∈ Δ; α ≤ τ ∈ B)

\begin{matrix}Δ; B ⊢_{F} σ_{1} ≤ τ_{1} & Δ; B ⊢_{F} τ_{2} ≤ σ_{2} \\ Δ; B ⊢_{F} τ_{1} → τ_{2} ≤ σ_{1} → σ_{2} \end{matrix}

\begin{matrix}j ∈ I_{2} : Δ; B ⊢_{F} τ_{j}^{ϕ_{j}} ≤ τ′_{j}^{ϕ′_{j}} & k ∈ I_{1} − I_{2} : Δ ⊢_{F} τ_{k} \\ Δ; B ⊢_{F} ⟨ℓ_{i}:τ_{i}^{ϕ_{i}}⟩_{i∈I_{1}}^{φ_{1}} ≤ ⟨ℓ_{j}:τ′_{j}^{ϕ′_{j}} ⟩_{j∈I_{2}}^{φ_{2}} \end{matrix}

where I_{2} is prefix of I_{1} if φ_{2} =→, otherwise I_{1} = I_{2} and

φ_{1} = ∘.

\begin{matrix}Δ, α ⊢_{F} τ_{11} = τ_{21} & Δ, α; B, α ≤ τ_{11} ⊢_{F} τ_{12} ≤ τ_{22} \\ Δ; B ⊢_{F} ∀α ≤ τ_{11}.τ_{12} ≤ ∀α ≤ τ_{21}.τ_{22} \end{matrix}

Δ, α; B ⊢_{F} τ_{1} ≤ τ_{2}

Δ; B ⊢_{F} self α.τ_{1} ≤ self α.τ_{2}

Δ, α_{1}, α_{2}; B, α_{1} ≤ α_{2} ⊢_{F} τ_{1} ≤ τ_{2}

Δ; B ⊢_{F} rec α_{1}.τ_{1} ≤ rec α_{2}.τ_{2} (α_{1} ≠ α_{2})

{Δ; B ⊢_{F} τ_{1} ≤ τ_{2} \atop Δ; B ⊢_{F} τ_{1}^{ϕ} ≤ τ_{2}^{+}} (ϕ ∈ \{+, ∘\})

{Δ ⊢_{F} τ_{1} = τ_{2} \atop Δ; B ⊢_{F} τ_{1}^{∘} ≤ τ_{2}^{∘}}

B.4 Expression Typing

\begin{matrix}Δ; B; Γ ⊢_{F} e : τ_{1} & Δ; B ⊢_{F} τ_{1} ≤ τ_{2} \\ Δ; B; Γ ⊢_{F} e : τ_{2} \end{matrix}

Δ; B; Γ ⊢_{F} x : τ (Γ(x) = τ)

\begin{matrix}Δ ⊢_{F} τ_{1} & Δ; B; Γ, x : τ_{1} ⊢_{F} e : τ_{2} \\ Δ; B; Γ ⊢_{F} λx : τ_{1}.e : τ_{1} → τ_{2} \end{matrix}

\begin{matrix}Δ; B; Γ ⊢_{F} e_{1} : τ_{2} → τ_{1} & Δ; B; Γ ⊢_{F} e_{2} : τ_{2} \\ Δ; B; Γ ⊢_{F} e_{1} e_{2} : τ_{1} \end{matrix}

Additional syntactic constructs:

Values  v, w ::= λx:τ.e | ⟨ℓ_{i} = v_{i}⟩_{i∈I} | Λα ≤ τ.v | pack v, τ as self α.σ
Contexts E ::= \{\} | E e | v E | ⟨\overrightarrow{ℓ = v}, ℓ = E, \overrightarrow{ℓ′ = e}⟩ | E.ℓ | E.ℓ ← e | v.ℓ ← E | E.ℓ := e | v.ℓ := E |
E + ℓ = e | v + ℓ = E | Λα ≤ τ.E | E[τ] | pack E, τ as self α.σ | unpack α, x = E in e

Reduction rules:

E{ι} ↦ E{e}

Where:

ι  e  Side Conditions
(λx:τ.e) v  e{x := v}
⟨ℓ_{i} = v_{i}⟩_{i∈I}.ℓ_{k}  v_{k}  k ∈ I
\{ \begin{matrix}⟨ℓ_{i} = v_{i}⟩_{i∈I}.ℓ_{k} ← v \\ ⟨ℓ_{i} = v_{i}⟩_{i∈I}.ℓ_{k} := v \end{matrix} \}  ⟨ℓ_{i} = v′_{i}⟩_{i∈I}  k ∈ I; v′_{i} = \{ \begin{matrix}v_{i} & i ≠ k \\ v & i = k \end{matrix}
⟨ℓ_{i} = v_{i}⟩_{i∈I} + ℓ = v  ⟨ℓ_{i} = v_{i}, ℓ = v⟩_{i∈I} ℓ ∉ ℓ_{i∈I}
(Λα ≤ τ.v)[σ]  v{α := σ}
unpack α, x = pack v, τ as self α.σ in e e{α, x := τ, v}

Figure 4: Target Language Operational Semantics

{Δ; B; Γ ⊢_{F} e_{i} : τ_{i} \atop Δ; B; Γ ⊢_{F} ⟨ℓ_{i} = e_{i}⟩_{i∈I} : ⟨ℓ_{i}:τ_{i}^{∘}⟩_{i∈I}^{∘}}

{Δ; B; Γ ⊢_{F} e : ⟨ℓ_{i}:τ_{i}^{ϕ_{k}}⟩_{i∈I}^{φ} \atop Δ; B; Γ ⊢_{F} e.ℓ_{k} : τ_{k}} (k ∈ I; ϕ_{k} ∈ \{+, ∘\})

\begin{matrix}Δ; B; Γ ⊢_{F} e_{1} : ⟨ℓ_{i}:τ_{i}^{ϕ_{i}}⟩_{i∈I}^{φ} & Δ; B; Γ ⊢_{F} e_{2} : σ \\ Δ; B; Γ ⊢_{F} e_{1}.ℓ_{k} ← e_{2} : ⟨ℓ_{i}:τ′_{i}^{ϕ′_{i}}⟩_{i∈I}^{φ} \end{matrix} (k ∈ I)

where τ′_{i}^{ϕ′_{i}} = τ_{i}^{ϕ_{i}} if i ≠ k and τ′_{k}^{ϕ′_{k}} = σ^{∘}.

\begin{matrix}Δ; B; Γ ⊢_{F} e_{1} : σ_{1} \\ Δ; B ⊢_{F} σ_{1} ≤ ⟨ℓ_{i}:τ_{i}^{ϕ_{i}}⟩_{i∈I}^{φ} \\ Δ; B; Γ ⊢_{F} e_{2} : τ_{k} \end{matrix} ; Δ; B; Γ ⊢_{F} e_{1}.ℓ_{k} := e_{2} : σ_{1} (k ∈ I; ϕ_{k} = ∘)

\begin{matrix}Δ; B; Γ ⊢_{F} e_{1} : ⟨ℓ_{i}:τ_{i}^{ϕ_{i}}⟩_{i∈I}^{∘} & Δ; B; Γ ⊢_{F} e_{2} : σ \\ Δ; B; Γ ⊢_{F} e_{1} + ℓ = e_{2} : ⟨ℓ_{i}:τ_{i}^{ϕ_{i}}, ℓ:σ^{∘}⟩_{i∈I}^{∘} \end{matrix} (ℓ ∉ ℓ_{i∈I})

\begin{matrix}Δ, α ⊢_{F} τ_{1} & Δ, α; B, α ≤ τ_{1} ⊢_{F} e : τ_{2} \\ Δ; B; Γ ⊢_{F} Λα ≤ τ_{1}.e : ∀α ≤ τ_{1}.τ_{2} \end{matrix}

\begin{matrix}Δ; B; Γ ⊢_{F} e : ∀α ≤ τ_{1}.τ_{2} & Δ; B ⊢_{F} σ ≤ τ_{1}\{α := σ\} \\ Δ; B; Γ ⊢_{F} e[σ] : τ_{2}\{α := σ\} \end{matrix}

Δ; B; Γ ⊢_{F} e : τ Δ; B ⊢_{F} τ ≤ σ{α := τ}
Δ; B; Γ ⊢_{F} pack e, τ as self α.σ : self α.σ

Δ; B; Γ ⊢_{F} e_{1} : self α.τ_{1}
Δ, α; B, α ≤ τ_{1}; Γ, x : α ⊢_{F} e_{2} : τ_{2}
Δ ⊢_{F} τ_{2}
Δ; B; Γ ⊢_{F} unpack α, x = e_{1} in e_{2} : τ_{2}