                         HOOTS99 Preliminary Version

Object Closure Conversion

Neal Glew^{1}

Department of Computer Science Cornell University Ithaca, USA

Abstract

An integral part of implementing functional languages is closure conversion—the process of converting code with free variables into closed code and auxiliary data structures. Closure conversion has been extensively studied in this context, but also arises in languages with first-class objects. In fact, one variant of Java’s inner classes are an example of objects that need to be closure converted, and the transformation for converting these inner classes into Java Virtual Machine classes is an example of closure conversion.

This paper argues that a direct formulation of object closure conversion is interesting and gives further insight into general closure conversion. It presents a formal closure-conversion translation for a second-order object language and proves it correct. The translation and proof generalise to other object-oriented languages, and the paper gives some examples to support this statement. Finally, the paper discusses the well known connection between function closures and single-method objects. This connection is formalised by showing that an encoding of functions into objects, object closure conversion, and various object encodings compose to give various closure-conversion translations for functions.

1 Introduction

The process of closure conversion and the concept of closures are old and well studied ideas arising in any language with first-class functions. Briefly, if a function f nested within a function g has free variables that are defined in g, the compiler will need to propagate the values of these variables from the time they are computed in g to the times at which f executes. The usual solution is to compile functions to closures, which are data structures that pair closed

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

This is a preliminary version. The final version will be published in Electronic Notes in Theoretical Computer Science

                       URL: www.elsevier.nl/locate/entcs

Glew

code with the values of free variables. The application of a function f to an argument a becomes an expression that extracts the closed code for f from the closure and then applies the code to the original argument and a part of the closure containing the values of the free variables.

The necessity for closure conversion is not limited to functional languages. In particular, Abadi and Cardelli’s object calculi [AC96] have first-class objects, and an inner-nested object’s methods could refer to variables defined in an outer-nested object. It might seem that object closure conversion is less important to mainstream object-oriented languages, so first I shall argue that this is not the case. One objection is that mainstream object-oriented languages are class based, and because classes are typically second class, closure conversion is not needed. However, Java was recently extended with inner classes, including a form that requires closure conversion. In fact, this form was introduced to alleviate the tedium of manual closure conversion. Another objection is that the combination of an object encoding and functional closure conversion gives object closure conversion. While this indirect approach is adequate, the results of this paper show that this approach misses many important points that a direct account exposes.

First, the indirect approach, if implemented naively, misses opportunities for sharing. Since most object encodings produce separate functions for each method, the methods of an object will be closure converted separately and will not share their environments. A direct approach naturally shares the environments.

Second, the object closure-conversion translation presented here is simpler than typed functional closure-conversion translations. Objects combine code and data in a single construct, so the values of free variables are paired with closed code simply by adding extra fields. Instead of using existential types to hide the types of the environment, the translation uses subsumption, a natural feature of any object calculus.

Third, this paper shows that functional closure conversion is equivalent to the composition of an encoding of functions as objects, object closure conversion, and an object encoding. This result formalises the well known connection between closures and single method objects. We will see that standard choices in functional closure conversion correspond to choices in the object closure conversion and the object encoding.

A difficult and still open issue, even in the functional literature, is the correctness of closure conversion. Minamide et al. [MMH95] discuss closure conversion for simply-typed and polymorphically-typed lambda calculi. They describe both conversions as two-step translations, and prove both type preservation and operational correctness. Their notion of correctness is an observational equivalence defined inductively over source types, and their correctness argument is a logical-relations argument. However, this proof does not extend to recursive functions. Morrisett and Harper [MH99] have used a similar technique, but extended with an unwinding lemma, to prove correct a number of typed closure-conversion translations for recursive functions. Their unwinding lemma is proved by defining a model and proving the result there. Unfortunately, it is difficult to define models for languages with recursive types, and harder to prove results in models of languages with state and advanced control features. These proofs are unsatisfying since they do not scale well to real language features.

Steckler and Wand [SW96] describe an optimised closure-conversion process for a simple untyped lambda calculus. They also prove their analysis and transformation correct, and this is a harder task than other proofs described in this paper, as it shows correctness of the optimisations as well as the basic translation. They avoid some of the problems of the above proofs by carefully defining their source semantics and translation so that a simulation argument is possible. Their real contribution, however, is the analysis and optimisation of known closures, and the proof that this optimisation is correct. This proof probably could be used in other settings. As mentioned above, functional closure conversion is object closure conversion composed with an object encoding. Therefore, the proof of object closure conversion’s correctness should be simpler. However, it does retain the key difficulty that makes these proofs hard to construct. Thus defining a direct object closure-conversion translation allows us focus on this essential problem.

This paper makes three contributions: it defines a direct object closureconversion translation, it proves this translation correct using syntactic methods that extend to recursive types, and it relates object closure conversion to functional closure conversion, formalising the well known connection between closures and single-method objects. Because of space limitations, the correctness theorem is stated here, and the proof appears in a companion technical report [Gle99]. First, the basic ideas are explained in the setting of a very simple object calculus. The translation is formalised in Section 4, for a second-order object calculus with method parameters described in Section 3. Some extensions of the translation to other language constructs are discussed in Section 5, and the connection between closures and single-method objects is shown in Section 6.

2 The Basic Idea

This section describes the basic idea of a direct object closure-conversion translation. This translation will transform a simple object calculus to itself, taking arbitrary terms as input, and producing closed code as output.

The syntax of the language is:

Types τ, σ ::= [m_{i}:τ_{i}; f_{j}:σ_{j}]_{i∈I,j∈J}
Terms e, b ::= x | [m_{i} = x_{i}.b_{i}:τ_{i}; f_{j} = e_{j}]_{i∈I,j∈J} | e.m | e.f | e_{1}.f ← e_{2}

The only form of type is the object type [m_{i}:τ_{i}; f_{j}:σ_{j}]_{i∈I,j∈J}, which is for objects with methods m_{i} of type τ_{i} and fields f_{j} of type σ_{j}.^{2} Objects are created by an object constructor [m_{i} = x_{i}.b_{i}:τ_{i}; f_{j} = e_{j}]_{i∈I,j∈J}. The newly created object responds to method m_{i} by executing b_{i} with x_{i} bound to the object, and has e_{j} as its value for field f_{j}. Note that e_{j} is evaluated at the time the object is created, and its free variables do not need to be closed over. Method invocation is written e.m, field selection e.f, and field update e_{1}.f ← e_{2}. I defer the formal semantics and typing rules to the next section.

For functions, the variables that need to be closed over are the free variables of the function. For objects, however, the variables that need to be closed over are not the free variables of the object, but just the free variables of the object’s methods. Therefore, I define the notion of closure variables for object constructors:

cv([m_{i} = x_{i}.b_{i}:τ_{i}; f_{j} = e_{j}]_{i∈I,j∈J}) = ⋃_{i∈I}(fv(b_{i}) − {x_{i}})

The goal of object closure conversion is to eliminate all closure variables of all object constructors that appear in the program.

The idea behind object closure conversion is simple: In functional closure conversion, closed code is paired with the values of free variables. Since objects already pair code and data, we simply add new fields to the object to store the free variables of its methods, and access them through the self variable. For example, the expression

[apply = self_{1}.[me = self_{2}.(self_{1}.apply):τ; ]:τ; ].apply

where τ = [me:[; ]; ] is closure converted to [apply = self_{1}.[me = self_{2}.(self_{2}.f.apply):τ; f = self_{1}]:τ; ].apply

This idea leads directly to the following syntax-directed translation:

|x|  = x
|e.m|  = |e|.m
|e.f|  = |e|.f
|e_{1}.f ← e_{2}| = |e_{1}|.f ← |e_{2}|
|e|  = [m_{i} = x_{i}.b′_{i}:τ_{i}; f_{j} = |e_{j}|, g_{k} = y_{k}]_{i∈I,j∈J,1≤k≤n}
where e = [m_{i} = x_{i}.b_{i}:τ_{i}; f_{j} = e_{j}]_{i∈I,j∈J} cv(e) = {y_{1}, …, y_{n}} b′_{i} = |b_{i}|{y_{1}, …, y_{n} := x_{i}.g_{1}, …, x_{i}.g_{n}} g_{k} are fresh

2 The indices i and j range over index sets I and J. For the purposes of this paper, these index sets are unordered and object types and objects are considered equivalent up to reordering. Ordered index sets could also be considered, and the results apply in this case also. The translation defined preserves ordering.

The notation x{y := z} denotes capture-avoiding substitution of z for y in z. The translation is straightforward for all expression forms exception object constructors. In particular, notice that method invocation, the analogue of function application, has a trivial translation. For object constructors, the new object has the same methods and fields as the original objects, and some extra fields g_{k}. There is one extra field for each of the closure variables. After translating the method bodies, each closure variable is replaced by a selection from the self variable of the field that corresponds to the closure variable.

It is worth pointing out that the typing translation is the identity. In functional closure conversion a function type is translated into a more elaborate type, which usually employs an existential to hide the types of the closure variables. In this translation, the new object has the same methods and fields with the same types, and some extra fields. So its principle type is a subtype of the original object’s type, and subsumption is used to hide the types of the closure variables. As we shall see, this simplicity is due to the fact that this translation is only half of a functional closure-conversion translation. The other half is an object encoding that does considerable type level translation and further term translation.

Now I will formalise the developments of this section in a scaled up language. This more complex language includes features needed for a comparison with functional closure conversion, in particular, method parameters. Also it supports the claim that the ideas scale to real languages. In particular, the scaled up language will include polymorphism, as past attempts to scale closure conversion to include polymorphism have encountered difficulties.

3 The Object Language

This section formalises an object language. The next section will define a formal translation from this language to itself that takes arbitrary terms to closed terms. The language is a variant of Abadi and Cardelli’s second-order object calculus [AC96] with a distinction between methods and fields, variances on fields, method parameters, only unbounded polymorphism, and no method update (lifting the latter two restrictions will be discussed in Section 5). The syntax of the language is:

Types  τ, σ ::= α | [m_{i}:s_{i}; f_{j}:σ_{j}^{ϕ_{j}}]_{i∈I,j∈J} | ∀α.τ
Method Signature s ::= [α⃗](τ⃗) → τ
Variances  ϕ ::= + | − | ∘
Terms  e, b ::= x | [m_{i} = M_{i}; f_{j} = e_{j}]_{i∈I,j∈J} | e.m[τ⃗](e⃗) |

e.f | e_{1}.f ← e_{2} | Λα.b | e[τ]

Method Definition M ::= x[α⃗](x_{1}:τ_{1}, …, x_{n}:τ_{n}).b:τ

The notation X⃗ denotes a sequence of elements drawn from syntax category X. For example, α⃗ means α_{1}, …, α_{n}, and \overrightarrow{x:τ} means x_{1}:τ_{1}, …, x_{n}:τ_{n}.

The types include type variables α, object types [m_{i}:s_{i}; f_{j}:σ_{j}^{ϕ_{j}}]_{i∈I,j∈J}, and polymorphic types ∀α.τ. Methods now take both type and value parameters, so they have signatures s instead of types. The signature [α_{1}, …, α_{m}] (τ_{1}, …, τ_{n}) → τ specifies a methods that takes m type parameters α_{1} through α_{m} and n value parameters of types τ_{1} through τ_{n} and produces a result of type τ. Object types also specify variances ϕ for fields. A read only field has variance +; a write only field has variance −; a read write field has variance ∘.

The terms include variables x, object constructors [m_{i} = M_{i}; f_{j}=e_{j}]_{i∈I,j∈J}, method invocation e.m[τ⃗](e⃗), field selection e.f, field update e_{1}.f ← e_{2}, type abstraction Λα.b, and type application e[τ]. An object constructor gives each of its methods a method definition M. The method definition x[α_{1}, …, α_{m}] (x_{1}:τ_{1}, …, x_{n}:τ_{n}).b:τ takes type parameters α_{1} through α_{m} and value parameters x_{1} through x_{n} of types τ_{1} through τ_{n} and executes b with x bound to the object. A method invocation e.m[τ⃗](e⃗) includes both the actual type arguments τ⃗ and the actual value arguments e⃗. I intend a type-erasure interpretation of polymorphism. Consequently, Λα.b does not suspend the execution of b until type application but evaluates it immediately.

There are several syntactic restrictions that simplify the technical development. In particular, the m_{i} in an object type or an object constructor must be distinct, and similarly for the field names, type parameters, and value parameters. Syntactic objects are equal up to α-equivalence.

The operational semantics appears in Figure 1. The notation E⟨e⟩ denotes the substitution of e for the unique hole ⟨⟩ in E. The semantics is a deterministic, left to right, call by value, context based, reduction semantics. Again, note that fields are evaluated to values at object-creation time. The notation e↓ means that e ↦^{∗} v for some v; e↑ means that e starts an infinite reduction sequence.

The typing rules are standard and appear in Figure 2. The calculus has full breadth and depth subtyping, methods are contravariant in their arguments and covariant in their results, and the depth subtyping of fields is determined by their variance.^{3} The notation ϵ is used for an empty typing context. Note that applying a typing rule with Δ, α in a hypothesis, implicitly requires α ∉ Δ, and similarly for value contexts.

The typing rules are sound with respect to the operational semantics; this property can be proven by standard techniques. Type soundness and several related properties of the typing rules are used in the proof of correctness; details appear in the companion technical report [Gle99].

3 Abadi and Cardelli [AC96] provide a description of variances and the rules for variance subtyping.

Syntax:

Contexts E ::= ⟨⟩ | [m_{i} = M_{i}; \overrightarrow{f = v}, f = E, \overrightarrow{g = e}]_{i∈I} | E.m[τ⃗](e⃗) |
v.m[τ⃗](v⃗, E, e⃗) | E.f | E.f ← e | v.f ← E |
Λα.E | E[τ]
Values v, w ::= [m_{i} = M_{i}; f_{j} = v_{j}]_{i∈I,j∈J} | ∀α.v

Reduction rules:

E⟨ι⟩ ↦ E⟨e⟩

Where v = [m_{i} = M_{i}; f_{j} = v_{j}]_{i∈I,j∈J} and:

ι  e  Side Conditions
v.m_{k}[τ⃗](v_{1}, …, v_{n}) b{α⃗, x, x⃗ := τ⃗, v, v⃗}  k ∈ I, M_{k} =
x[α⃗](x_{1}:σ_{1}, …, x_{n}:σ_{m}).b
v.f_{k}  v_{k}  k ∈ J
v.f_{k} ← w  [m_{i} = M_{i}; f_{j} = v′_{j}]_{i∈I,j∈J} k ∈ J, v′_{j} = \{ \begin{matrix}v_{j} & j ≠ k \\ w & j = k \end{matrix}
(Λα.w)[τ]  w{α := τ}

Fig. 1. Operational Semantics

The free variables of an expression are:

fv(x)  = {x}
fv([m_{i} = M_{i}; f_{j} = e_{j}]_{i∈I,j∈J}) = ⋃_{i∈I} fv(M_{i}) ∪ ⋃_{j∈J} fv(e_{j})
fv(e.m[τ⃗](e_{1}, …, e_{n}))  = fv(e) ∪ ⋃_{1≤i≤n} fv(e_{i})
fv(e.f)  = fv(e)
fv(e_{1}.f ← e_{2})  = fv(e_{1}) ∪ fv(e_{2})
fv(Λα.b)  = fv(b)
fv(e[σ])  = fv(e)
fv(x[α⃗](x_{1}:τ_{1}, …, x_{n}:τ_{n}).b:τ) = fv(b) − {x, x_{1}, …, x_{n}}

The closure variables of an object constructor are:

cv([m_{i} = M_{i}; f_{j} = e_{j}]_{i∈I,j∈J}) = ⋃_{i∈I} fv(M_{i})

Again note that only the free variables of methods are included. An object constructor is code closed if and only if it has no closure variables. An arbitrary expression is code closed if and only if every object-constructor subexpression

Glew

Typing Contexts:

Δ ::= α_{1}, …, α_{n}  where α_{1}, …, α_{n} are distinct
Γ ::= x_{1}:τ_{1}, …, x_{n}:τ_{n} where x_{1}, …, x_{n} are distinct

Type well formedness, typing context well formedness, and subtyping:

Δ ⊢ τ (ftv(τ) ⊆ Δ) {Δ ⊢ τ_{i} \atop Δ ⊢ x_{1} : τ_{1}, …, x_{n} : τ_{n}} Δ ⊢ α ≤ α (α ∈ Δ)

\begin{aligned}i ∈ I_{2} : & Δ ⊢ s_{i} ≤ s′_{i} \\ j ∈ J_{2} : & Δ ⊢ σ_{j}^{ϕ_{j}} ≤ σ′_{j}^{ϕ′_{j}} \\ & Δ ⊢ [m_{i}:s_{i}; f_{j}:σ_{j}^{ϕ_{j}}]_{i∈I_{1},j∈J_{1}} \end{aligned} ; Δ ⊢ [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}} (I_{2} ⊆ I_{1}; J_{2} ⊆ J_{1})
{Δ, α ⊢ τ_{1} ≤ τ_{2} \atop Δ ⊢ ∀α.τ_{1} ≤ ∀α.τ_{2}}  \begin{matrix}Δ, α⃗ ⊢ σ_{i} ≤ τ_{i} & Δ, α⃗ ⊢ τ ≤ σ \\ Δ ⊢ [α⃗](τ_{1}, …, τ_{n}) → τ ≤ [α⃗](σ_{1}, …, σ_{n}) → σ \end{matrix}
{Δ ⊢ σ_{1} ≤ σ_{2} \atop Δ ⊢ σ_{1}^{ϕ} ≤ σ_{2}^{+}} (ϕ ∈ \{+, ∘\}) {Δ ⊢ σ_{2} ≤ σ_{1} \atop Δ ⊢ σ_{1}^{ϕ} ≤ σ_{2}^{−}} (ϕ ∈ \{−, ∘\}) {Δ ⊢ σ \atop Δ ⊢ σ^{∘} ≤ σ^{∘}}

Expression typing:

\begin{matrix}Δ; Γ ⊢ e : τ_{1} & ⊢ τ_{1} ≤ τ_{2} \\ Δ; Γ ⊢ e : τ_{2} \end{matrix} Δ; Γ ⊢ x : τ (Γ(x) = τ)
\begin{matrix}Δ ⊢ τ & Δ; Γ; τ ⊢ M_{i} : s_{i} & Δ; Γ ⊢ e_{j} : σ_{j} \\ Δ; Γ ⊢ [m_{i} = M_{i}; f_{j} = e_{j}]_{i∈I,j∈J} : τ \end{matrix} (τ = [m_{i}:s_{i}; f_{j}:σ_{j}^{∘}]_{i∈I,j∈J})

{Δ; Γ ⊢ e : [m:[α_{1}, …, α_{m}](τ_{1}, …, τ_{n}) → τ; ] Δ ⊢ σ_{i} Δ; Γ ⊢ e_{i} : τ_{i}\{α⃗ := σ⃗\} \atop Δ; Γ ⊢ e.m[σ_{1}, …, σ_{m}](e_{1}, …, e_{n}) : τ\{α⃗ := σ⃗\}}

{Δ; Γ ⊢ e : [; f:σ^{ϕ}] \atop Δ; Γ ⊢ e.f : σ_{k}} (ϕ ∈ \{+, ∘\})
\begin{aligned}Δ; Γ ⊢ e_{1} : τ & Δ ⊢ τ ≤ [; f:σ^{ϕ}] & Δ; Γ ⊢ e_{2} : σ \\ & Δ; Γ ⊢ e_{1}.f ← e_{2} : τ \end{aligned} (ϕ ∈ \{−, ∘\})
{Δ, α; Γ ⊢ b : τ \atop Δ; Γ ⊢ Λα.b : ∀α.τ}  \begin{matrix}Δ; Γ ⊢ e : ∀α.τ & Δ ⊢ σ \\ Δ; Γ ⊢ e[σ] : τ\{α := σ\} \end{matrix}

{Δ, α⃗; Γ, x:τ, x_{1}:τ_{1}, …, x_{n}:τ_{n} ⊢ b : σ \atop Δ; Γ; τ ⊢ x[α⃗](x_{1}:τ_{1}, …, x_{n}:τ_{n}).b:σ : [α⃗](τ_{1}, …, τ_{n}) → σ}

Fig. 2. Typing Rules

is code closed.

4 Object Closure Conversion

This section formalises the translation described in Section 2 for the object language in Section 3. Exactly the same ideas are used: An object constructor

|x|  = x
|e.m[τ⃗](e_{1}, …, e_{n})| = |e|.m[τ⃗](|e_{1}|, …, |e_{n}|)
|e.f|  = |e|.f
|e_{1}.f ← e_{2}|  = |e_{1}|.f ← |e_{2}|
|Λα.b|  = Λα.|b|
|e[σ]|  = |e|[σ]
|e|  = e′

where e  = [m_{i} = M_{i}; f_{j} = e_{j}]_{i∈I,j∈J}

e′ = [m_{i} = M′_{i}; f_{j} = |e_{j}|, g_{1} = y_{1}, …, g_{n} = y_{n}]_{i∈I,j∈J}
cv(e) = {y_{1}, …, y_{n}}
M_{i} = x_{i}[α⃗_{i}](\overrightarrow{x_{i}:τ_{i}}).b_{i}:τ_{i}
M′_{i} = x_{i}[α⃗_{i}](\overrightarrow{x_{i}:τ_{i}}).|b_{i}|\{y_{1}, …, y_{n} := x_{i}.g_{1}, …, x_{i}.g_{n}\}:τ_{i}

g_{1}, …, g_{n} are fresh

Fig. 3. Object Closure Conversion Translation

is extended with fields for its closure variables, and method bodies reference these closure variables by field selection of the self variable. The typing translation is the identity translation, and the term translation is defined inductively over the syntax of expressions and appears in Figure 3.

4.1 Observational Equivalence

An important aspect of the correctness of the translation is that it preserves the meaning of expressions. There are a number of ways to define notions of meaning preservation. Unfortunately, the simplest of these, simulation arguments, does not hold for this language. Consider the example given in Section 2. The source term makes this transition:

[apply = self_{1}.[me = self_{2}.(self_{1}.apply):τ; ]:τ; ].apply
↦ [me = self_{2}.([apply = self_{1}.[me = self_{2}.(self_{1}.apply):τ; ]:τ; ].apply):τ; ]

But the translated term makes this transition:

[apply = self_{1}.[me = self_{2}.(self_{2}.f.apply):τ; f = self_{1}]:τ; ].apply
↦ [me = self_{2}.(self_{2}.f.apply):τ;

f = [apply = self_{1}.[me = self_{2}.(self_{2}.f.apply):τ; f = self_{1}]:τ; ]]

The reduced source term is code closed and translates to itself not the reduced translated term. In particular, notice that the outer object is part of the method body of me in the reduced source term but an extra field in the reduced target term. In general, closure conversion shifts free variables to extra fields, but does not shift the values that get substituted for them to extra fields. In effect the environment is in the method bodies in the source term, but in extra fields in the target term. While this does not change the behaviour of terms, a simulation argument cannot prove correctness.

Instead, this paper uses contextual equivalence [Mor68,Plo77]: two terms are equivalent if they are indistinguishable in any context of the language. Following standard practice, termination behaviour is used as the primitive notion of observable difference. The formal definition of contextual equivalence, which I shall call observational equivalence, requires the definition of contexts.

Contexts C are an extension of the syntax category e with holes ⟨⟩. Holes may appear in a number of places in C and within type or term variable binders, and these binders capture the free type and term variables of the hole. The notation C⟨e⟩ denotes the expression that results from replacing the holes in C with e. A context C is typed by the judgement Δ_{1}; Γ_{1} ⊢ C : τ_{1}⟨Δ_{2}; Γ_{2}:τ_{2}⟩, and this holds exactly when Δ_{1}; Γ_{1} ⊢ C : τ_{1} is derivable with the extra rule Δ_{1}, Δ_{2}; Γ_{1}, Γ_{2} ⊢ ⟨⟩ : τ_{2}. Clearly if Δ_{1}, Δ_{2}; Γ_{1}, Γ_{2} ⊢ e : τ_{2} then Δ_{1}; Γ_{1} ⊢ C⟨e⟩ : τ_{1}.

Most previous work, which considered untyped languages, used an untyped version of equivalence. However, closure conversion is not correct under this version. A translated object constructor has extra fields, so a context that selects these extra fields will for the source term get stuck, and for the translated term converge. Therefore, the correctness criteria must rule out run-time type errors by using a typed version of equivalence. A term and its translation will be equivalent at the type of the source term.

Definition 4.1 (Observational Equivalence)

• e_{1} and e_{2} are Kleene equivalent, e_{1} ∼ e_{2}, iff: ^{4}

ϵ; ϵ ⊢ e_{1} : [; ] ∧ ϵ; ϵ ⊢ e_{2} : [; ] ∧ e_{1}↓ ⇔ e_{2}↓ ∧ e_{1}↑ ⇔ e_{2}↑

• e_{1} and e_{2} are Δ; Γ-observationally equivalent at τ, e_{1} ≡_{Δ;Γ:τ} e_{2}, iff:

\begin{matrix}Δ; Γ ⊢ e_{1} : τ ∧ Δ; Γ ⊢ e_{2} : τ ∧ \\ ∀C : ϵ; ϵ ⊢ C : [; ]⟨Δ; Γ:τ⟩ ⇒ C⟨e_{1}⟩ ∼ C⟨e_{2}⟩ \end{matrix}

The above relations are equivalence relations and observational equivalence is a congruence. These properties are proven in the companion technical report [Gle99], as part of a basic theory of observational equivalence. Some basic properties are proven: equivalence is preserved under equivalent substitutions and under reduction, and equivalence at a subtype is finer than equivalence at a supertype. Some principles for establishing equivalence are also proven.

4 The third and fourth clauses are redundant in a deterministic language, such as the one of this paper. I state the more general definition to be consistent with my scalability theme.

First, to show arbitrary open terms are equivalent it suffices to show that under all appropriate substitutions they are equivalent. Second, to show closed terms are equivalent it suffices to show that the values they evaluate to are equivalent.

Third, a coinduction principle is proven. To motivate this principle, consider proving v_{1} and v_{2} equivalent at [m:τ; ]. Placing v_{1} and v_{2} in arbitrary contexts results in arbitrary reductions, but such reductions will not observe a difference unless it includes a method invocation of m. Thus, most previous work includes a theorem of the form that v_{1} and v_{2} are equivalent if they are Kleene equivalent in all contexts of the form C⟨⟨⟩.m⟩. However, if v_{1}.m ↦ e_{1} and v_{2}.m ↦ e_{2} this still requires reasoning about e_{1} and e_{2} in arbitrary contexts. My coinduction principle goes further and considers just contexts of the form ⟨⟩.m. It requires showing that (v_{1}, v_{2}, [m:τ; ]) is a member of a set of triples that is closed under reduction. For this example, closed under reduction means that e_{1} and e_{2} are either equivalent or that (e_{1}, e_{2}, τ) is another triple in the set. In general the type at which v_{1} and v_{2} are to be equivalent determines the contexts that need to be considered, details are in the companion technical report [Gle99].

This coinduction principle is not enough. Consider proving [m = x.b_{1}; ] equivalent to [m = x.b_{2}; ] as part of a proof by induction on the structure of expressions. Using the coinduction principle this requires showing that b_{i}{x := [m = x.b_{i}; ]} for i ∈ {1, 2} are equivalent or in some set of triples. The induction hypothesis says that b_{1} and b_{2} are equivalent assuming x is substituted with equivalent values, but x is substituted by the values we are trying to prove equivalent. This is the fundamental problem with extending the proof of Minamide et al. [MMH95] to recursive functions. Morrisett and Harper [MH99] use an unwinding lemma to solve this problem. The 0th unwinding of [m = x.b_{i}; ] for i ∈ {1, 2} diverge when method m is invoked so they are clearly equivalent. The n + 1th unwinding reduces to b_{i} with the nth unwinding substituted for x, so by induction on n, we can establish that the nth unwindings of the objects are equivalent for all n. The unwinding lemma then tells us that the objects themselves are equivalent. The basic theory mentioned above proves an unwinding lemma for the object language, and a more powerful coinduction principle.

4.2 Correctness

There are three aspects to correctness: the translation produces code closed expressions, preserves types, and preserves the meaning of expressions.

Theorem 4.1 (Translation Correctness) If Δ ⊢ Γ and Δ; Γ ⊢ e : τ then:

• |e| is code closed

• Δ; Γ ⊢ |e| : τ

• e and |e| are Δ; Γ-observationally equivalent at τ The proof appears in the companion technical report [Gle99], and is by induction on the structure of e or its typing derivation. For all cases other than object constructors, the proof is straightforward, and uses the congruence property of equivalence. To prove operational correctness for object constructors requires two key lemmas. The first shows that an object is equivalent to itself with some extra fields. Intuitively this is true because the extra fields are just carried around, and contexts cannot see the extra fields at the original type. The proof uses the coinduction principle in a straightforward manner. The other lemma shows that one method body can be replaced with its translation. The coinduction principle is used again. The substitution y⃗ := \overrightarrow{x_{i}.g} preserves equivalence because x_{i}.g_{k} ↦ y_{k}, so one of the basic lemmas says that x_{i}.g_{k} and y_{k} are equivalent.

A couple of points are worth mentioning. First, the proof actually proves full abstraction. Full abstraction is the property that the target language cannot distinguish the translation of equivalent source terms, formally: e_{1} ≡_{Δ;Γ:τ} e_{2} implies |e_{1}| ≡_{Δ;Γ:τ} |e_{2}|. This holds for object closure conversion, for if e_{1} ≡_{Δ;Γ:τ} e_{2} then |e_{1}| ≡_{Δ;Γ:τ} e_{1} ≡_{Δ;Γ:τ} e_{2} ≡_{Δ;Γ:τ} |e_{2}|.

Second, the proof should extend to a number of other features. Consider recursive types. For equirecursive types, the definitions and proofs remain unchanged. For isorecursive types, the definition of closed under reduction needs to include unroll, but otherwise the proof goes through. The proof should also easily extend to cover all of the features mentioned in the next section, thus supporting my claim that the proof really does scale to real languages.

5 Some Extensions

The translation scales to a number of other language features and variations in the language semantics including an imperative semantics, right-extension subtyping, integers, products, sums, arrays, recursive types, and functions. Details appear in the companion technical report [Gle99].

On polymorphism, the translation already includes unbounded parametric polymorphism both as a separate construct and for methods. Extending this to ordinary-bounded, F-bounded, or matching-based parametric polymorphism is straightforward. It is worth noting that in implementing the object language, after converting objects to records of functions, and before lifting these functions to the top level, the free type variables must be closed over using the ideas of Morrisett et al. [MWCG98]. If a type-passing interpretation is desired, the translation must be changed to close over type variables as well. There are two approaches: The first uses the ideas of Crary, Weirich, and Morrisett [CWM98] to convert type variables to value variables and a type-erasure interpretation. This paper’s translation would then close over the value variables. The other approach involves adding type fields to an object constructor to store the free type variables. This would require a type system for objects with type fields, which likely would involve the complexity described by Minamide et al. [MMH96], Leroy [Ler94], and Harper and Lillibridge [HL94]. Otherwise, I believe the translation would look much the same, although the proof would be considerably more complicated.

The translation can also be extended to handle method update, field extension, and method extension. All of these require field extension, which interacts poorly with breadth subtyping. Thus, either a different operational semantics is required, such as the dictionary semantics [RS98], or a more complicated type system, such as described by Fisher [Fis96]. Details appear in the companion technical report [Gle99].

Finally, as well as extensions to other language features, the translation has variants that express other environment representations. The translation of method bodies is b′_{i} = |b_{i}|\{\overrightarrow{y := x_{i}.g}\}. It could also be b′_{i} = |b_{i}\{\overrightarrow{y := x_{i}.g}\}|, which would result in a different environment representation. The first choice leaves y_{1} through y_{p} free in all inner-nested object constructors and so these variables will be closed over in the inner objects, resulting in a flat environment representation. The second choice replaces the y_{p} in an inner-nested object constructor with a (free) reference to x_{i} which will be closed over, resulting in a linked environment representation.

6 Closures and Functional Closure Conversion

We are finally in a position to compare object closure conversion and functional closure conversion, and to formalise the well known connection between closures and single-method objects. This section will show this connection by providing a translation from a typed lambda calculus to the language of this paper, and show that the encoding composed with object closure conversion and some object encoding results in a functional closure conversion. I will demonstrate this for two particular object encodings, showing their equivalence to a closure passing and environment passing style of functional closure conversion.

Consider a simply-typed lambda calculus with recursive functions:

Types  τ, σ ::= int | τ_{1} → τ_{2}
Expressions e, b ::= x | i | fix f(x_{1}:τ_{1}):τ_{2}.b | e_{1} e_{2}

For the remainder of this section, assume an object language with integers. The lambda calculus can be encoded into the object language as follows:

|int|  = int
|τ_{1} → τ_{2}| = [apply:[ ](|τ_{1}|) → |τ_{2}|; ]

|x|  = x
|i|  = i
|fix f(x_{1}:τ_{1}):τ_{2}.b| = [apply = f[ ](x_{1}:|τ_{1}|).|b|:|τ_{2}|; ]
|e_{1} e_{2}|  = |e_{1}|.apply[ ](|e_{2}|)

If the object closure conversion translation is composed with the above encoding, the combined rule for functions is:

|fix f(x_{1}:τ_{1}):τ_{2}.b| = [apply = f[ ](x_{1}:|τ_{1}|).|b|{y_{i} := f.g_{i}}; g_{i} = y_{i}]
where fv(b) − {f, x_{1}} = {y_{i}}

Now, consider converting the object calculi back into a functional calculi via an object encoding. The notation ⟨\overrightarrow{f = e}⟩ denotes a record with fields f⃗ and values e⃗, e.f denotes field projection, and e_{1}.f ← e_{2} denotes field update. First, consider an encoding based on the self-application semantics [Kam88]. Ignoring typing, the interesting composed translation rules are:

|fix f(x_{1}:τ_{1}):τ_{2}.b| = ⟨apply = λ(f, x_{1}).|b|{y_{i} := f.g_{i}}, g_{i} = y_{i}⟩
where fv(b) − {f, x_{1}} = {y_{i}}
|e_{1} e_{2}|  = let x = |e_{1}| in x.apply(x, |e_{2}|)

These rules are just functional closure conversion with a closure-passing style and a flat environment representation.

Second, consider Pierce and Turner’s object encoding [PT94]. Ignoring typing, the interesting composed translation rules are:

|fix f(x_{1}:τ_{1}):τ_{2}.b| = let fix fcode(fenv, x_{1}) =

let f = ⟨⟨apply = fcode⟩, fenv⟩ in

|b|{y_{i} := fenv.g_{i}} in

⟨⟨apply = fcode⟩, ⟨g_{i} = y_{i}⟩⟩

where fv(b) − {f, x_{1}} = {y_{i}}

|e_{1} e_{2}|  = let x = |e_{1}| in x.1.apply(x.2, |e_{2}|)

These rules are just functional closure conversion with an environment-passing style and a flat environment representation.

Thus we see that closures and single method objects are equivalent, as witnessed by the translation given at the beginning of this section. We also see that functional closure conversion factors into this equivalence translation, object closure conversion, and an object encoding.

Other schemes mentioned in Morrisett and Harper [MH99] could also be described as specialised object encodings for single-method objects composed with object closure conversion. In fact, the ideas of this section suggest a general framework for explaining functional closure conversion, as follows. First, a closure language would be defined, which would be the object language of this paper restricted to single methods. Second, a closure-conversion translation would be defined on this language, and various choices for environment representation would be described as variations on this translation. Third, a closure-representation translation would be presented, and various passing styles would be described as various closure representations. This general framework then allows Java’s inner-class transformation to be explained as a generalisation to a full object language.

7 Related Work and Summary

Closure conversion has been studied extensively for functions [AJ89,Han95, KKR^{+}86,Lan64,MMH96,MWCG98,Rey72,Ste78,SW96]. To the best of my knowledge, object closure conversion has not been described before.

The connection between closures and objects is well known, and has been hinted at in the literature. As far as I am aware, this is the first paper to formalise the connection explicitly. Reddy [Red98] discuss objects as closures. Minamide et al. [MMH96] informally discuss closures as objects, but do not formalise the connection. Abadi and Cardelli [AC96] give several versions of an encoding of functional calculi into object calculi. Their encoding is different from the one here as they do not consider method parameters. Also they do not talk at all about closure conversion nor make connections between functional calculi and object calculi at the level of closures.

Correctness proofs for functional closure conversion are given by Minamide et al. [MMH95], Stekler and Wand [SW96], Morrisett and Harper [MH99], and possibly other authors. Only the latter considers recursive functions, and none of them consider recursive types. Observational equivalence has been studied and used to prove correctness in both functional settings (e.g., [Mor68,Plo77, MST96]) and in object settings (e.g., [GHL98]). My results use similar tools and similar proof techniques, further supporting the claim that my proof will scale to real languages.

This paper has presented an object language with first-class objects and a closure-conversion translation for it. This translation was used to show a formal connection between closures and single-method objects, and that functional closure conversion factors through object closure conversion. These results lend further insight into the general problem of closure conversion and foundations for the implementation of object-oriented languages.

References

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

[AJ89] Andrew Appel and Trevor Jim. Continuation-passing, closure-passing style. In 16th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 293–302, Austin, Texas, USA, January 1989.

[CWM98] Karl Crary, Stephanie Weirich, and Greg Morrisett. Intensional polymorphism in type-erasure semantics. In 1998 ACM SIGPLAN International Conference on Functional Programming, pages 301–312, Baltimore Maryland, USA, September 1998.

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

[GHL98] Andrew Gordon, Paul Hankin, and Søren Lassen. Compilation and equivalence of imperative objects. Technical Report RS-98-55, BRICS, Department of Computer Science, University of Aarhus, Ny Munkegade, building 540, DK-8000 Aarhus C, Denmark, December 1998. URL:

http://www.brics.dk/RS/98/55.

[Gle99] Neal Glew. Object closure conversion. Technical Report TR99-1763, Department of Computer Science, Cornell University, 4130 Upson Hall, Ithaca, NY 14853-7501, USA, August 1999. Available at http://

www.cs.cornell.edu/glew/paper-list.html.

[Han95] J. Hannan. A type system for closure conversion. In The Workshop on Types for Program Analysis, 1995.

[HL94] Robert Harper and Mark Lillibridge. A type-theoretic approach to higher-order modules with sharing. In 21st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 123–137, Portland Oregon, USA, January 1994.

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

[KKR^{+}86] David Kranz, R. Kelsey, J. Rees, P. R. Hudak, J. Philbin, and N. Adams. ORBIT: An optimizing compiler for Scheme. In Proceedings of the ACM SIGPLAN ’86 Symposium on Compiler Construction, pages 219–233, June 1986.

[Lan64] P. J. Landin. The mechanical evaluation of expressions. Computer Journal, 6(4):308–320, 1964.

[Ler94] Xavier Leroy. Manifest types, modules, and separate compilation. In 21st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 109–122, Portland, OR, USA, January 1994.

[MH99] Greg Morrisett and Robert Harper. Simply-typed closure conversion. Unpublished, authors contact: jgm@cs.cornell.edu, April 1999.

[MMH95] Yasuhiko Minamide, Greg Morrisett, and Robert Harper. Typed closure conversion. Technical Report CMU-CS-95-171, School of Computer Science, Carnegie Mellon University, Pittsburgh, PA 15213, USA, July 1995.

[MMH96] Yasuhiko Minamide, Greg Morrisett, and Robert Harper. Typed closure conversion. In 23rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 271–283, St. Petersburg, January 1996.

[Mor68] J. Morris. Lambda-Calculus Models of Programming Languages. PhD thesis, Massachuetts Institute of Technology, 1968.

[MST96] Ian Mason, Scott Smith, and Carolyn Talcott. From operational semantics to domain theory. Information and Computation, 128:26– 47, 1996.

[MWCG98] Greg Morrisett, David Walker, Karl Crary, and Neal Glew. From System F to typed assembly language. In 25th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 85–97, San Diego California, USA, January 1998. ACM Press.

[Plo77] Gordon Plotkin. LCF considered as a programming language. Theoretical Computer Science, 5:223–255, 1977.

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

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

[Rey72] John Reynolds. Definitional interpreters for higher-order programming languages. In Proceedings of the Annual ACM Conference, pages 717– 740, 1972.

[RS98] Jon Riecke and Christopher Stone. Privacy via subsumption. In 5th International Workshop on Foundations of Object Oriented Programming Languages, San Diego, CA, USA, January 1998.

[Ste78] Guy Steele Jr. Rabbit: A compiler for Scheme. Master’s thesis, MIT, 1978.

[SW96] Paul Steckler and Mitchell Wand. Lightweight closure conversion. ACM Transactions on Progamming Languages and Systems, pages 48–86, January 1996.