Typed Closure Conversion
Yasuhiko Minamide yGreg Morrisett

Robert Harper

Research Institute for Mathematical Sciences
Kyoto University
Kyoto 606{01, Japan

School of Computer Science
Carnegie Mellon University
Pittsburgh, PA 15213{3891

School of Computer Science
Carnegie Mellon University
Pittsburgh, PA 15213{3891

nan@kurims.kyoto-u.ac.jp

jgmorris@cs.cmu.edu

rwh@cs.cmu.edu

Abstract
Closure conversion is a program transformation used bycompilers to separate code from data. Previous accountsof closure conversion use only untyped target languages. Recent studies show that translating to typed target languages
is a useful methodology for building compilers, because acompiler can use the types to implement ecient data representations, calling conventions, and tag-free garbage collection. Furthermore, type-based translations facilitate security and debugging through automatic type checking, as
well as correctness arguments through the method of logicalrelations.
We present closure conversion as a type-directed, andtype-preserving translation for both the simply-typed andthe polymorphic -calculus. Our translations are based ona simple \closures as objects" principle: higher-order functions are viewed as objects consisting of a single method(the code) and a single instance variable (the environment).
In the simply-typed case, the Pierce-Turner model of object typing where objects are packages of existential typesuces. In the polymorphic case, more careful tracking oftype sharing is required. We exploit a variant of the HarperLillibridge \translucent type" formalism to characterize thetypes of polymorphic closures.

1 Introduction
Closure conversion 29, 34, 5, 17, 16, 1, 39, 9] is a programtransformation that achieves a separation between code andThis research was sponsored in part by the Advanced Research
Projects Agency CSTO under the title \The Fox Project: Advanced
Languages for Systems Software", ARPA Order No. C533, issued
by ESC/ENS under Contract No. F19628-95-C-0050, and in partby the National Science Foundation under Grant No. CCR-9502674,
and in part by the Isaac Newton Institute for Mathematical Sciences,
Cambridge, England. The views and conclusions contained in thisdocument are those of the authors and should not be interpreted as
representing ocial policies, either expressed or implied, of ARPAor the U.S. Government. Any opinions, ndings, and conclusions
or recommendations expressed in this material are those of the authors and do not necessarily reect the views of the National Science
Foundation.
y This research was performed while the rst author was visiting
the Fox Project at Carnegie Mellon University.

data. Functions with free variables are replaced by code abstracted on an extra environment parameter. Free variablesin the body of the function are replaced by references to theenvironment. The abstracted code is partially applied to an
explicitly constructed environment providing the bindings
for these variables. This partial application of the code toits environment is in fact suspended until the function is actually applied to its argument the suspended application,
called a closure, is a data structure consisting of a piece ofpure code and a representation of its environment.
A critical decision in closure conversion is the choiceof representation for the environment | whether to use a
at FAM-like 4], linked CAM-like 5], or hybrid representation 30]. The choice of representation is inuenced by a desire to minimize closure creation time, the space consumed
by the environment, and the time to access a variable in
the environment 39, 30]. An important property of closure
conversion is that the representation of the environment isprivate to the closure. This aords considerable exibility
in the representation of environments and is thus exploited
to good advantage by Shao and Appel 30] and Wand andSteckler 39].
Previous accounts consider closure conversion as a transformation to untyped terms, even if the source language istyped 34, 17, 1, 39, 9]. This is adequate for compilers thatmake little or no use of types in the back end or at run
time. However, when compiling typed languages, it is often
advantageous to propagate type information through eachstage of the compiler, and to make use of types at link- or
even run time. For example, Leroy's representation analysis 18, 31] uses types to determine procedure calling conventions, and Ohori's record compilation 25] uses a representation of types at run time to access components of a record.
Compilation strategies for polymorphic languages, such as
those proposed by Morrison et al. 24] and Harper and Morrisett 14], rely on analyzing types at run time to support
unboxed representations and non-parametric operators, including printing and structural equality. Tag-free garbage
collection 3, 37, 23] for both monomorphic and polymorphic programming languages relies on analyzing types at
run time to determine the size and layout of objects in theheap. To support any of these implementation strategies,
it is necessary to propagate type information through closure conversion and into the generated code. The purposeof this paper is to demonstrate how this can be done in botha simply-typed and a polymorphic setting.
We present closure conversion as an example of a typedirected and type-preserving translation. In general, suchtranslations transform both a term and its type, possibly
relying on type information to guide the translation. Thus
each stage of the compiler can be viewed as a type-preserving
translation between typed intermediate languages. Examples of such translations have been given by Leroy 18],
Ohori 25], Harper and Lillibridge 10], and Harper and Morrisett 14]. In contrast to type-free compilation strategies,
these translations make essential use of type information
during translation to increase the time or space eciency of
programs. In addition to the practical advantages of this approach, type-directed translation also facilitates the work of
the compiler writer. In particular, the typing properties of
the intermediate code may be exploited to give clear, concise
proofs of compiler correctness through the method of logicalrelations 35, 6, 27, 32, 33]. Furthermore, the intermediate
code of the compiler can be mechanically typed-checked,
an important debugging tool for the compiler writer. Finally, checkable typed intermediate languages are a promising technique for ensuring safety properties of programs ina distributed environment 8, 38].
We describe closure conversion for the simply-typed calculus and the predicative fragment of the polymorphic-calculus. In each case we present closure conversion in
two stages. The rst stage, called abstract closure conversion, is a type-directed translation to an intermediate language with a primitive notion of closures. We describe thetranslation as a deductive system where the choice of environment representations may be independently made foreach closure. We argue that various representations considered in the literature (such as the FAM 4] or CAM 5]), as
well as hybrid representations 30], can all be explained inthis uniform framework. We establish the correctness of thetranslation once for all environment representations.
The second stage, called closure representation, is another type-directed translation where closures are implemented in terms of generic typed -calculus primitives. The
main idea is to represent closures as objects consisting ofa single method (the code) and a single instance variable(the environment). We show that, in the simply-typed case,
Pierce and Turner's type discipline for object-oriented programming 26] may be used to characterize the types of closures. In particular, we use existential type abstraction toensure the privacy of environment representation in muchthe same way that Pierce and Turner hide the representation types of instance variables. In the polymorphic case,
we must use a more sophisticated type discipline in order
to track critical type sharing relationships within the closure. To this end, we exploit a variant of the translucent
type 11] (or manifest type 19]) formalism. Our \closures asobjects" model provides an interesting counterpoint to themore familiar \objects as closures" proposal introduced by
Reddy 28].
We prove the correctness of both the abstract closure
conversion and the closure representation stages using themethod of logical relations. The main idea is to dene a
type-indexed family of simulation relations that establish acorrespondence between the source and target terms of thetranslation. Once a suitable system of relations has beendened, it is relatively straightforward to prove by induction
on the denition of the compilation relation that the source
and target of the translation are related. From this, we may
conclude that a closed program and its translation evaluate
to the same result. Due to lack of space, we omit the proofsof correctness here. However, full details may be found in

the companion technical report 21].
Closure conversion is discussed in descriptions of various
functional language compilers 34, 17, 2, 1, 30]. It is similar to -lifting 15] in that it eliminates free variables inthe bodies of -abstractions but diers by making the representation of the environment explicit as a data structure.
Making the environment explicit is important because it exposes environment construction and variable lookup to an
optimizer. Furthermore, Shao and Appel show that not allenvironment representations are \safe for space" 30], andthus choosing a good environment representation is an important part of compilation. Wand and Steckler 39] haveconsider two optimizations of the basic closure conversion
strategy, called selective and lightweight closure conversion,and provide a correctness proof for each of these in an untyped setting. Hannan 9] recasts Wand's work into a typed
setting and provides correctness proofs for one of Wand's
optimizations. Hannan's translation, like ours, is given as adeductive system, but he does not consider the important
issue of environment representation (preferring an abstract
account instead), nor does he consider the typing propertiesof the closure-converted code. Finally, neither Wand nor
Hannan consider closure conversion under a type-passing
interpretation of polymorphism.
The remainder of this paper is organized as follows. In
Section 2, we give an overview of closure conversion andthe typing issues involved for the simply-typed -calculus.
In Section 3, we provide the details of our type-preserving
transform for the simply-typed case. In Section 4, we give an
overview of closure conversion and the typing issues involved
for the predicative fragment of the polymorphic -calculus.
The formal development of this conversion is given in Section
5.

2 Overview of Simply-Typed Closure Conversion
The main ideas of closure conversion are illustrated by considering the following ML program:let val x = 1
val y = 2
val z = 3
val f = w. x + y + w
in
f 100
end.

The function f contains free variables x and y. We may
eliminate references to these variables from the body of f
by abstracting an environment env and replacing x and y byreferences to the environment. In compensation, a suitableenvironment containing the bindings for x and y must be
passed to f before it is applied. This leads to the following
translation:
let val x = 1
val y = 2
val z = 3
val f = ( env. w. (#x env) + (#y env) + w)
x=x, y=y
in
f 100
end.

f

g

References to x and y in the body of f are replaced byprojections (eld selections) #x and #y that access the corresponding component of the environment. Since the code forf is closed, it may be hoisted out of the enclosing denitionand dened at the top-level. We ignore this \hoisting" phaseand instead concentrate on the process of closure conversion.
In the preceding example the environment contains bindings only for x and y, and is thus as small as possible. Since z
is in scope, it is also sensible to include z in the environmentof f, resulting in the following code:
let val x = 1
val y = 2
val z = 3
val f = ( env. w. (#x env) + (#y env) + w)
x=x, y=y, z=z
in
f 100
end.

f

g

In the examples above, we used a at FAM-like 4] representation of the environment as a record with one eld foreach variable. Alternatively we could choose a linked CAMlike 5] representation in which each binding is a separate
frame attached to the front of the remaining bindings. Thisidea leads to the following translation:
let val x = 1
val y = 2
val z = 3
val f = ( env. w.
(#x(#link(#link env))) +(#y(#link env)) + w)
z=z, link= y=y, link= x=x
in
f 100
end.

f

f

f ggg

The linked representation facilitates environment sharing,
but accessing a variable requires link traversals proportional
to the nesting depth of the variable in the environment. The
linked representation also supports constant-time closure
creation, but this requires reusing the current environment.
Reusing the current environment can result in unnecessary
bindings in the environment (such as z above), leading tospace leaks.
These simple translations fail to delay the application of
the code to its environment under call-by-value evaluation.
A natural representation of a delayed application or closure
is an ordered pair (code, env) consisting of the code together with its environment. Application of a closure toan argument proceeds by projecting the code part from theclosure and then applying it simultaneously to both the environment and the argument according to some calling convention. For example,
let val x = 1
val y = 2
val z = 3
val code = env. w. #x(env) + #y(env) + w
val env = x=x, y=yval f = (code, env)
in(#1 f) (#2 f) 100
end.

f

g

But since code has a type of the form ve ! 1 ! 2 , whereve is the type of the environment env, the closure as a whole
would have type (ve ! 1 ! 2 )  ve, exposing the type ofthe environment. As a result, this translation does not, ingeneral, preserve types. For example, consider the following
ML source program with type int ! int:
let val y = 1
in
if true thenx. x+y
else
z. z
end.

Closure converting this expression and representing the closures as pairs yields
let val y = 1
in
if true then( env. x. x + #y(env),
else( env. z. z,
)
end.

fg

fy=yg)

This program fails to type-check because the then-clause of
the conditional has type (fy:intg ! int ! int)  fy:intg,
whereas the else-clause has type (fg ! int ! int)  fg.
If types are to be preserved by closure conversion, therepresentation of the environment must be hidden. Thismay be achieved through the use of existential types 22],
whose typing rules are given in Figure 1. Briey, the packconstruct packages a type  with a term e, abstracting certain occurrences of  in the type of e as the type variable t.
The open operation extracts the contents of a package foruse within a xed scope, holding the type component of the
package abstract. (See Mitchell and Plotkin's article 22] forfurther discussion of existential types.)
Using existentials, we may hide the type of the environment by abstracting it from the type of the closure itself.
Specically, a closure of type 1 ! 2 is represented by apackage of the formpack ve with (code env) as 9tve :(tve ! 1 ! 2 )  tve
with type 9tve :(tve ! 1 ! 2 )  tve . Applying this to theexample of the conditional expression given above, we obtainthe translation
let val y = 1
in
if true thenpack y:int with ( env. x. x+#y(env), y=y )
as
int
int)
ve ( ve
ve
else
pack
with ( env. z. z,
)
as
int
int)
ve ( ve
ve
end.

f g
9t : t !
fg
9t : t !

!
!

t
fg
t

f g

It is easy to see that the types of the clauses of the conditional agree, and that the translation has type 9tve :(tve !
int ! int)  tve .
With closures represented as packages of existential type,applications of the form e e' are translated as follows: ; ` e1 : 9t: ] ftg ; ] fx: g ` e2 :  ; ` e : =t]0

 ; ` pack  with e as 9t: : 9t:(t 62 FTV () t 62 )0 ; ` open e1 as t with x in e2 : 

Figure 1: Typing Rules for Existentialsttopen e as ve with z : ( vein(#1 z) (#2 z) e'end.

!  !  )t
1

2

ve

That is, the package e is opened, holding the environment
representation abstract, and the code part is simultaneously
applied to both the environment and the argument of theapplication.

3 A Formal Account of Simply-Typed Closure Conversion
In this section we present the details of closure conversion forthe call-by-value, simply-typed -calculus. We break the fulltransformation into two stages, as outlined in the introduction. To simplify the presentation, we begin with a versionof abstract closure conversion that does not admit sharingof environments and then consider the general, shared environment case separately. Next, we give the representationof closures in terms of existential types as sketched in thepreceding section. Finally, we prove the correctness of thetranslations using a logical relations argument.
We dene the syntax of the source language, , as follows:Types ::= b j 1 ! 2
Expressions e ::= c j x j x:: e j e1 e2
Valuesv ::= c j x:: eTypes consist of base types (b) and function types1 . Expressions consist of constants (c) of base type, variables, abstractions, and applications. We use ; to denote a sequence oftype bindings of the form fx1 :1  : : :  xn :n g (n 0) where
the xi 's are distinct variables. The judgement ; ` e : asserts that the expression e has type  under the type assignment ;, and is derived from the standard typing rulesof the simply-typed -calculus. The dynamic semantics ofthe language is dened by judgements of the form e ,! v
asserting that the closed expression e evaluates to the value
v. The judgement is dened by the following standard inference rules for call-by-value evaluation:
e1 ,! x:1 : e e2 ,! v2 ev2 =x] ,! v
v ,! v!

e1 e2 ,! v

3.1 Abstract Closure Conversion

We denethe target language for abstract closure conversion, cl , as follows:
Types  ::= b j 1 ! 2 j h1  : : :  n i j code(ve  1  2 )Exp's e ::= c j x j e1 e2 j he1  : : :  en i j i (e) j
xve :ve : x:1 : e j hhe1  e2 ii
Values v ::= c j xve :ve : x:1 : e j hv1  : : :  vn i j hhv1 v2 ii
1 The results of this paper easily extend to other source types including products and sums.

In the introduction we informally presented a closure as apartial application of code to an environment, with the intention that this application is delayed until the closure isapplied to an argument. To make this precise we introduce an explicit closure form, written hheeve ii, where e isthe code of the closure and eve is its environment. Noticethat closures are distinguished from applications of functions to arguments, which are written in the usual way byjuxtaposition. To capture the restriction that the code partof a closure should be closed, we introduce a special code
type, code(ve  1  2 ), consisting of closed terms of the form
xve :ve : x:1 :e, which abstract both an environment andan argument2 .
The typing rules for cl are standard except for code andclosures, whose rules are given as follows:
fxve:ve x:1g ` e : 2
; ` xve :ve : x:1 :e : code(ve 1  2 ); ` e : code(ve  1  2 ) ; ` eve : ve; ` hhe eveii : 1 ! 2

The evaluation rules governing closures are given as follows:

e1 ,! v1 e2 ,! v2
hhe1 e2ii ,! hhv1 v2ii
e1 ,! hh xve:ve : x:1 :e vveii e2 ,! v2evve=xve  v2 =x] ,! v
e1 e2 ,! v

When a closure is applied to an argument, the environment
and the argument are substituted for the corresponding variables and the body of the code is evaluated.
We dene abstract closure
conversion as the type-directedtranslation fromto cl given in Figure 2. We formulate
the translation as a deductive system with judgements ofthe form ; x: . e e and ; x: . ;eve, where ;and ; are source type assignments,  is a source type, e isa source expression, and e and eve are target expressions.
The distinguished variable x is used to represent the argument of the nearest enclosing -abstraction the variables in; include this -abstraction's free variables.
The judgement ; x: . e e asserts that e is thetranslation of e under the assumption that ; ] fx: g ` e : for some  . The judgement ; x: . ; eve assertsthat eve is an expression that evaluates to the environment
corresponding to ; , under the assumption that each binding
in ; occurs in ; ] fx: g. The order of bindings in ; isimportant, because this determines the translation of both
environments and free variables.
!

0

0

0

0

0

0

0

0

0

0

0

0

0

0

0

2 In practice, a multi-argument -abstraction is used for code in
the target language. However, the polymorphic case requires a more
complicated construct that abstracts both values ( ) and types ().
For uniformity we use a curried presentation to abstract multiple
arguments.

(const) ; x: . cc(arg) ; x: . x

x : . ;(abs) ; x ;: . x::e000eve ;  x: . e

0

0

x
e

0

hh x :j; j: x:: e  e ii

0

ve

0

0

ve

(env) fx1 :1  : : :  xn :n g x: . xi

i (xve )(app) ; x: ;. ex1: . ee11 e;2 x:e. ee2
001

x: . xn en(context) ;;xx::..fxx11 :1  e: 1: : :x: n: :;n g he1  : : :  en i

0

e2
0

2

(; ] fx: g ` xi : i )Figure 2: Simply-Typed Abstract Closure Conversion
We use the variable xve to hold the environment argument of the current code body. Thus, we translate free variables to projections of xve . More precisely, according torule (env), we translate a reference to the free variable xi
found in the ith position of the type assignment ; to the ith
projection of the variable xve . On the other hand, according
to rule (arg), we translate a reference to the argument of thecurrent code body to the distinguished argument variable x.
Under the assumptions ; x : , we translate an abstraction x::e to a closure according to the (abs) rule. To construct the environment of the closure, we choose a type assignment ; such that ; x : . ;eve is derivable via
the (context) rule and ;  x: . e e . In eect, these rules
require that every binding in the closure's environment must
be in scope (i.e., in ; ] fx : g) and the environment is required to contain bindings for all of the free variables in
the original function x:: e. However, ; may also containbindings for variables that are in scope but do not occur freein the function. Consequently, there are many choices for; , with the exact choice being inuenced by time and spaceconsiderations.
We construct the environment of a closure via the (context)
rule by translating each of the variables occurring in ;(namely x1   xn ) to the target expressions e1   en . We
place the resulting expressions in a tuple he1  : : :  en i, toform the environment data structure of the closure. This
representation of the environment has type h1   n i,
which we summarize by writing j; j.
To produce the code of the closure, we translate the bodyof the source function under the strengthened assumptions;  x : , producing the body of the code, e . We then abstract the environment and argument, yielding the translation xve :j; j: x:: e .
Using a dummy \current argument" to translate an entire closed program, it is easy to prove by induction on thederivation of the translation that the translation preserves
the type of a program.
Theorem 1 If ` e: and  x:b . e e , then ` e :  .
To prove the correctness of the translation, we use a typeindexed family of logical relations relating closed source expressions to closed target expressions ( ) and closed source
values to closed target values ( ). The relations are dened
by induction on source types as follows:e ei e ,! v and e ,! v and v  v
0

0

0

0

0

0

0

0

0

0

0

0

0

0

0

0

0

v

c

0

0

bc

1 2 v

0

0

0

0

0

i for all v1 1 v1 , v v1 2 v v1 .
We extend the relation to nite source ( ) and target substitutions ( ), mapping variables to their respective class of
!

0

0

0

0

0

values. These relations are dened as follows:
x1 :1 :::xn :n x: hv1  : : :  vn i=xve  v=x]i (xi ) i vi for 1  i  n and (x)  v.
Theorem 2 Let ;x0 : 0 . If ; ] fx : g ` e :  and; x : . e e , then (e)  (e ).
Thus, for a closed program of base type, evaluating the
program and its translation yields syntactically equivalentvalues.
f

g

0

0

0

0

0

0

0

0

3.2 Sharing Environments

Some implementations of functional programming languages
share portions of an environment among closures in an eort
to decrease space and closure creation time. In this section
we extend the treatment of abstract closure conversion toallow for shared environments. We achieve this by imposing additional structure on environments to allow for nested
representations.
The type assignments in the previous section (;) consistof a at sequence of variable declarations. To provide forshared environment representations, we enrich the structureof type assignments to support nested type assignments asfollows:! ::= fx: g j h!1  : : :  !m i
A nested type assignment is either a single type binding
or a sequence of nested type assignments. The environment
corresponding to the type assignment ! has target language
type j!j, where jfx: gj =  and jh!1  : : :  !m ij = hj!1j : : :  j!m ji. We can obtain a non-nested type assignment(;) from a nested type assignment (!) simply by dropping
the extra structure.
We give the most important translation rules for closure
conversion with nested environments in Figure 3 the remaining rules may be obtained from those in Figure 2 byreplacing ; with ! throughout.
We use the (env-tuple) rule to construct a nested environment he1   en i corresponding to the type assignments!1   !n , if ! x: . !i ei , for 1  i  n. We obtain each of the !i and ei from the (arg), (env), (subenv),and (env-tuple) rules. We use the (arg) rule to translate theargument of the nearest enclosing -abstraction as an environment, and we use the (env) rule to translate the freevariables of this abstraction as an environment. As before,
we use the distinguished variables x and xve to hold thesetwo values in the translation. We use the (subenv) rule totranslate access to a type assignment nested within ! to a(arg) fx : g x: . fx: g
00!i  x: . !

h!  : : :  !ni x: . !

(subenv)1x(env) ! x: . !

xve

x: . fx : g e(var) !!x: . x e000! x: . !1 e1! x: . !n eneei(xve )=xve ] (env-tuple)! x: . h!1  : : :  !n i he1  : : :  en i

Figure 3: Simply-Typed Closure Conversion using Nested Environments
projection of the environment corresponding to !. Finally,
we translate access to a variable within a type assignment
via the (var) rule.
As an example, consider the translation
hfx1:intg fx2:intgi x :int . ( x:int:x + x1 + x2)
hh xve:: x:int:1(xve) + 1 (2(xve)) + 2(2 (xve))
00hx  x iii
where  is hint  hint  intii. We construct the new envi0

veronment for the closure by pairing the current argument x
and the current environment xve according to the (env-tuple)
rule. If we used the at translation given in Figure 2, thenwe would have to project the values for x1 and x2 out of thecurrent environment and place these values and the current
argument into a newly allocated tuple.
Nested type assignments are suciently exible to handle many commonly-used environment representations. For
example, the Categorical Abstract Machine, or CAM 5],
uses a linked list to represent the environment. This is reected in our framework by restricting the shape of nested
type assignments and by restricting the (env-tuple) rule to\cons" the current argument onto the current environment,
as follows:(CAM context) !c ::= fx: g j hfx: g !c i(env-tuple) !c  x: . hx: !c i hx xve i:
The advantage of the CAM strategy is that the cost of theconstruction of a new environment is constant. However,in the worst case, accessing values in the environment takes
time proportional to the length of the environment.
In contrast, the FAM 4] uses at environments with nosharing. The closure conversion of Figure 2 accurately models the environment strategy of the FAM if we choose a specic strengthening strategy in the (abs) rule where only thefree variables of the function are preserved in the resulting
closure's environment. The advantage of the FAM environment representation is that the cost of variable lookup isalways constant and the representation is \safe for space"
1] according to Appel's denition. However, constructing
the environment for a closure takes time proportional to thenumber of free variables in the function, and closures cannot
share portions of their environment.
Clearly, there are a variety of other strategies for forming environments. For example, the shared closure strategy described by Appel and Shao 30] that is also safe forspace can also be formulated in our framework. However,to determine a good representation for each closure's environment requires a good deal more information including
an estimate as to how many times each variable is accessed,
when garbage collection can occur, what garbage collection
algorithm is used, etc.
03.3 Closure Representation

The purpose of abstract closure conversion is to choose anenvironment representation for each closure and to make theconstruction of closures explicit. By making environments
explicit, we expose operations that are implicit at the source
level to an optimizer at the target level. In particular, an
optimizer can eliminate redundant constructions of environments or redundant projections from environments.
However, the process of extracting the code and environment of a closure remains an implicit, atomic operation of
the operational semantics. Hence, we cannot optimize theseclosure operations. For instance, if the same closure is repeatedly applied in a loop, it is not possible to extract thecode and environment once, repeating only the application
to the environment and argument within the loop.
To make such optimizations possible, we choose a representation of closures in terms of generic primitives thatwould, in practice, already be present in the intermediate
language. Specically, we consider a target languagewith existential types, dened by the following grammar:
Types  ::= b j t j h1  : : :  n i jcode(ve  1  2 ) j 9t:
9Exp's e ::= c j e1 (e2  e3 ) j xve :ve : x:1 :e jhe  : : :  eni j i e j
1

pack
open

 with e as  j
e1 as t with x: in e2This language includes existential types and code types,
but not function types we show how to dene function types
in terms of these primitive constructs. We restrict applications to the form e1 (e2  e3 ) in order to preclude a partial
application of code to its environment this can be seen asa specialized use of multi-argument functions.
Typing judgements for are of the form  ; ` e : 
where  is a list of type variables in scope and ; is a typeassignment for variables in scope. We assume that the free
type variables of the types in the range of ; and the free typevariables of e and  are contained in . The typing rules
and evaluation rules of the language are standard (see 22]
and Figure 1).
We describe the closure representation phase in two parts.
We begin by dening a translation from cl to types, denoted j j, as follows:
jbj = bjh1  : : :  n ij = hj1j  : : :  jnji
jcode(ve 1 2 )j = code(jvej j1j j2j)j1 ! 2 j = 9tve:hcode(tve j1j j2j)  tvei:
We translate an arrow type to a pair consisting of code andan environment, with the environment type held abstract
using an existential quantier.
99; . e : code(ve  1  2 ) e ; . eve : ve eve(closure) ; . hheepack jve j with he  eve i as j1 ! 2 jve ii : 1 ! 20

00

; . e1 : 1 ! 2 e1 ; . e2 : 1 e2; . e1 e2 : 2
(x 62 Dom(;))
open e1 as tve with x:hcode(tve  j1 j j2 j)  tve i in (1 x)(2 x e2 )
0

(app)

0

0

0

0

Figure 4: Important Rules of Simply-Typed Closure Representation
Next, we dene the translation of cl terms to terms
in Figure 4. The judgements of the translation clare of theform ; . e :  e , where ;, e, and  are a type assignment, expression, and type respectively, and e is a
expression. The interesting rules are (closure) and (app).
The other rules (not shown) simply map the other cl constructs to their counterparts. We translate a closure to apair of the code and the environment packed with the typeof the environment. We translate an application to an open,
extract from a package the pair of a code and an environment, and then apply the code to the environment and theargument.
It is easy prove that the translation preserves the typeof a program up to the translation of the type. We do soby rst extending the type translation to type assignments,
setting
jfx1:1  : : :  xn:ngj = fx1:j1j: : :  xn:jnjg:
Theorem 3 If ; ` e :  and ; . e :  e , then  j;j `e : j j.
Correctness of the translation is proven using logical relationsclbetween cl and expressions, cl and values,
andand substitutions. The denition of the relations and the proof of the correctness can be found in our
technical report 21].
9

0

0

9

9

0

0

9

9

9

4 Overview of Polymorphic Closure Conversion
Closure conversion for a language with ML-style (i.e., predicative 13]) explicit polymorphism follows a similar pattern
to the simply-typed case, but with two additional complications. First, we must account for free type variables aswell as free value variables in the code of an abstraction.
Second, we must create closures for both value abstractions( -terms) and type abstractions (#-terms). In this section,
we give an overview of the typing diculties encounteredwhen closure converting value abstractions the treatmentof type abstractions is similar (see Section 5 for details).
To eliminate free occurrences of type variables and ordinary variables from the code, we abstract with respect
to a type environment and a value environment, replacing
free variables by references to the appropriate environment.
This process results in closed code that can be hoisted tothe top level and shared among multiple closures. The codeis partially applied to suitable representations of the typeand value environments to form a polymorphic closure. As
in the simply-typed case, we need a data structure to represent the delayed partial application of the code to its typeand value environments. In addition, we must abstract boththe kind of the type environment and the type of the value
environment so that their representations remain private to
the closure. Without the abstraction, we run into the same
typing problems that we encountered in the simply-typed
case.
As a running example, consider the expression

t

t

t

x: 1 . (x: 1, y: 2, z:int),

where t1 and t2 are free type variables and y and z are freevalue variables of type t2 and int respectively. It is easy tocheck that this expression has type t1 ! (t1  t2  int). To
closure convert the expression, we translate it to the partial
application
let val code =#tenv :: 1 ::$, 2 ::$ .
venv : y:# 2 tenv, z:int .
x : (# 1 tenv).(x, #y venv, #z venv)
incode
y=y, z=z
1= 1, 2= 2
end.

ft
f

g

t

t

t
ft t t t g f

gg

The code of the closure abstracts a type environment tenv
and a value environment venv. The actual type environment
ft1=t1,t2=t2g is a record of kind ft1::$,t2::$g, where $ is thekind of monotypes. The actual value environment fy=y,z=zg is a record with type fy:t2 , z:intg. Note, however,that this type contains a free reference to t2 , which must
be replaced by a reference to the type environment in orderto ensure that the translated code is closed. We therefore
ascribe the type fy:#t2 tenv, z:intg to the value environment, noting that the projection #t2 tenv is equivalent tot2 when the actual type environment is as given earlier. By
similar reasoning we assign the type #t1 tenv to the argument x of the -abstraction. It is easy to check that thecode of the closure has the type code given by the equation

code =

8tenv::ft ::$, t ::$g.
fy:#t tenv, z:intg!
(#t tenv)!((#t tenv)(#t tenv)int).
It follows that the entire let expression has the type of theoriginal term, namely t ! (t  t  int).
1

2

2
1

1

1

1

2

2

Now let us consider the representation of the partial application of code to its type and value environments as adata structure. This data structure must be \mixed phase"in the sense that it consists of both type and value components. This suggests using a package of existential type ofthe forme = pack ft1 =t1, t2 =t2 g with (code, fy=y, z=zg)
as 9tte :: te .code  ve ,where code is as given earlier andte = ft1 ::$, t2 ::$g

ve = fy:#t2 tte , z:intg.

This package is well-typed according to the usual rules forexistentials.
In contrast, consider what happens when we attempt togive the translation of the application of e to an argument
e of type t1 . Proceeding as in the simply-typed case, we introduce an open expression that extracts the code, the typeenvironment, and the value environment from the closure,and applies the code to the environments and argument.
Doing so results in the following translation:
0

e

t



open
as te:: te with w: codein(#1 w) te (#2 w) 0
end.

t



ve

e

Unfortunately, this expression is not well-typed. The diculty is that e has type t1 , whereas the expression (#1 w)
tte (#2 w) has type0

t tte)!((#t1 tte)(#t2 tte)int).
Since tte is abstract, the type variable t1 is not equivalent
to #t1 tte. Consequently, the proposed translation of appli(# 1

cation fails to type-check.
One way to get around this problem is to apply the code
to the type environment before forming the closure. This
yieldsft t t t g
ft t t t g
fy=y,z=zg)
9t
 

let val c = code
1= 1, 2= 2
inpack
1 = 1 , 2 = 2 with (c,aste :: te . cveend,where the type c is given by the equationc = fy:#t1 tte,z:intg!(#t1 tte)!
((#t1 tte)(#t2 tte)int).

The translation of application given above will work in thiscase because the code and the value environment both use
tte as the type environment. But this approach depends
upon the very mechanism we are attempting to eliminate,
namely partial application. The partial application of thecode to the type environment produces code that is no longer
closed. Thus, the code cannot be shared among the dierent
instantiations of the type environment.
Our solution to this issue is to constrain the code sothat it can be applied to a closure's value environment only
when it is also applied to the same closure's type environment. This ensures that the type environment passed to thecode and the type environment used in the construction of
the closure's value environment are the same. Fortunately,
typing constraints of this form have already been addressedby research on module systems 20, 19, 11].
Following Harper and Lillibridge 11], we use the notionof translucent types to express the desired constraint on thecode. In particular, when forming the closure, we coerce thecode to have the translucent type8tenv = ft =t ,t =t g:: .
fy:#t tenv,z:intg!(#t tenv)!
((#t tenv)(#t tenv)int).
1

1

2

2

te

1

1
2

1

This type is a super-type of the original code type code
because we have constrained the bound type variable tenv to
be bound to a particular type, namely the type environmentof the closure. (See Harper and Lillibridge 11] and Leroy
19] for further discussion of subtyping in this setting.) This
constraint ensures that this reference to the code will only
be applied to the type environment of the closure.
The constraint on tenv allows us to conclude that #t1
tenv is equivalent to t1 and similarly, that #t2 tenv is equivalent to t2 . We propagate these equivalences into the typeyielding

8tenv = ft =t ,t =t g:: .
fy:t ,z:intg ! t ! (t t int).
1

1

2

1

2

te

1

1

2

We can now form the package containing the type environment, code, and value

ft t t t g


pack
1 = 1 , 2 = 2 with (code, env)aste :: te .
ve ,

9t

where  is given via the equation

 = 8tenv=tte:: te.fy:#t1 tte ,z:intg!
(#t1 tte)!((#t1 tte )(#t2 tte )int),
and show that this package has type 9tte :: te :  ve . Notethat  is the same as c, (the type of the partial applicationof code to the type environment), except for the additional
constrained type abstraction of tenv. Through the use oftranslucency, we have accomplished the eect of partial application at the type-level without actually performing theapplication at the term-level.
Opening a package e of type 9tte :: te :  ve to apply toan argument e of type t1 yields:0et  vee

open
as te :: te, w:
in(#1 w) te (#2 w)
end.

t

0

The expression (#1 w) tte (#2 w) e has type t1 ! (t1 
t2  int), thus the entire expression is well-formed.
In summary, we use transluceny to constrain the typeof code before placing it in a closure. We use pack to represent the mixed-phase data structure containing the code,
type environent, and the value environment. The resulting
package has a type of the form
(9tte :: te :8t=tte:: te :ve ! 1 ! 2 )  ve :To avoid the typing problems encountered in the simplytyped case, we need to hide the representations of the value
environment and the type environment. Thus, we use packagain to abstract the kind of the type environment and thetype of the value environment, resulting in the following typefor closures:
9kte:9tve::$:9tte::kte:(8t=tte::kte:tve ! 1 ! 2)  tve:0

Careful consideration of the foregoing discussion reveals
that we only made limited use of translucency. The universally quantied variable tenv does not occur in the scopeof the abstraction once the equational constraint on tenv ispropagated. We use this property to provide a substantiallysimpler mechanism than the full translucent type calculus.
In particular, we only need to capture the restriction thata polymorphic function must be applied to a specic typeargument. This may be expressed by introducing a type )  consisting of functions that must be applied to theconstructor  to yield a value of type . The following two
rules govern this new type constructor: `  ::  ; ` e : 8t:: :  ; ` e :  )  ; ` e :  ) =t] ; ` e  : The rst rule restricts the domain of type application to thespecic constructor  . This corresponds to restricting thetype to 8t = : and propagating the equivalence t =  into
. The actual type application for  )  is permitted only
for constructors equivalent to  . These two rules naturally
come from the necessity of delaying type applications forclosure conversion. Using this notation, the type translationof 1 ! 2 becomes
9kte:9tve::$:9tte::kte:(tte ) tve ! 1 ! 2)  tve:
The type of closures abstracts the kind of the type environment and the type of the value environment, ensuringthat these may be chosen separately for each closure in thesystem. As in the simply-typed case, we have obtained an\object oriented" representation of polymorphic closures by
exploiting a combination of the type systems proposed by
Pierce and Turner 26] for objects and by Harper and Lillibridge 11] for modules.

5 A Formal Account of Polymorphic Closure Conversion
In this section, we present closure conversion for the predicative fragment of the second order -calculus. This fragment
is sucient to model Standard ML 13], and admits relatively simple correctness proofs based on logical relations.
Our results extend to the full impredicative polymorphic calculus, but at the expense of a substantially more complex
correctness argument (based on Girard's method of candidates 7]).
We dene the syntax of the source language as follows:
Kinds
::= $
Constructors  ::= b j t j 1 ! 2Types
 ::=  j 1 ! 2 j 8t:: :
Expressions e ::= c j x j x:1 :e j #t:: :e j e1 e2 j e Valuesv ::= c j x:1 :e j #t:: :e
We use kinds ( ) to describe constructors ( ) and types() to describe expressions (e). There is only one kind ($)
for cl , but since subsequent languages have a richer kindstructure, we introduce kinds here for uniformity. Closed
constructors of kind $ correspond to a subset of types, inparticular the types that do not include quantiers (themonotypes). Thus, constructors of kind $ can be injected
into types. We leave this injection implicit and treat  asboth a constructor and a type.
A kind assignment  is a sequence that maps type variables to kinds and is of the form ft1 :: 1  : : :  tn :: n g, (n 0).
Typing judgements are of the form  ; ` e :  where thefree type variables of ;, e, and  are contained in the domain of , and the free value variables of e are contained in88

the domain of ;. Typing judgements are derived according
to the standard typing rules of the second-order -calculus(see for example 13, 14]). The most interesting rules are
the introduction and elimination rules for quantied types:
 ] ft:: g ; ` e : (t 62 Dom()) ; ` #t:: : e : 8t:: :  ; ` e : 8t:: : (FTV( )  Dom()) ; ` e  : =t]

5.1 Abstract Closure Conversion

Abstract closure conversion for converts both -abstractions
and #-abstractions into abstract closures consisting of code,a type environment and a value environment. We consider
here only at environment representations, but note that thetreatment of nested environments given in Section 3 carries
over to the polymorphic case.
We dene the syntax of the target language cl as follows:
Kinds ::= $ j h 1  : : :  2 i
Con's  ::= b j t j 1 ! 2 j h1  : : :  n i j88h  : : :  ni j i  j

Types  ::=  j 1 ! 2 j 8t:: : j h1  : : :  n i jvcode(tte:: te ve  1  2 ) j
tcode(tte:: te  ve  t::   )Exp's e ::= c j x j e1 e2 j e  j he1  : : :  en i j i e j#tte:: te : xve :ve : x:1 :e j#tte:: te : xve :ve :#t:: :e j hhe1   e2 ii
We use product kinds of the form h 1  : : :  n i to specify the shapes of type environments in much the same waythat we use product types to specify the shapes of value
environments.
There are two sorts of code: code corresponding to an ordinary -abstraction has the form #tte :: te : xve :ve : x:1 :e
while code corresponding to a type abstraction has the form
#tte:: te: xve :ve :#t:: :e. The code in each case abstractsa type environment and a value environment. For the case the code also abstracts a value argument, and for the#-case the code abstracts a type argument. We introduce
the types vcode and tcode to distinguish the two types ofcode from the types of closures, to ensure closure conditions
on code, and to preclude partial applications of code to environments. These types may be described by the following
informal correspondences:vcode(tte :: te  ve  1  2 )8tte:: te:ve ! 1 ! 2
tcode(tte :: te  ve  t::  )
8tte:: te:ve ! 8t:: ::We consider code types to be polymorphic, so thesetypes
do not lie in the range of a polymorphic quantier.3
Abstract closures have the form hhe1  e2 ii, consisting ofpiece of code e1 , a type environment  , and a value environment e2 .
For the typing of cl , kind assignments () map typevariables to kinds while type assignments (;) map value
variables to types. The judgements of the static semantics
are as follows: `  ::
 is a well-formed constructor of kind .
` is a well-formed type.
 ` 1  2 :: 1 and 2 are equivalent constructors.
 ` 1  2
1 and 2 are equivalent types.
 ; ` e : 
e is a well-formed expression of type .
1

8

3 This restriction is relaxed in the impredicative case.

The formation rules of types are standard. We have to introduce denitional equality of constructors and types toaccount for projections of constructors from product kinds.
These rules consist of the equivalence rules for projections
below, as well as the standard rules for equivalence and congruence: ` i h1  : : :  n i  i :: i ` h1  : : :  n  i   :: h 1  : : :  n i
The typing rules for expressions are standard except for
the rules for codes and closures. These rules are dened in
Figure 5. We require that code values be closed with respect
to both type variables as well as value variables. This allows
us to share the code among multiple instantiations of the free
type variables and free value variables.
We dene abstract closure conversion from to cl by
the deductive system given in Figures 6 and 7. The judgement env  arg .   means that  is the translation of where env is a kind assignment corresponding to a typeenvironment and arg is a kind assignment corresponding
to a type argument (if any). This judgement also implicitly denes a translation from constructors to constructors,
since source-level constructors ( ) are a subset of types ()and the translation maps constructors to constructors. In
translated programs the type variable tte is used for typeenvironments.
The judgement env  arg  ;env  ;arg . ee means
e is a translation of e where env and arg are as in thetype translation, and ;env and ;arg are type assignments
corresponding to the value environment and value argument
respectively. A type environment corresponding to env anda value environment corresponding to ;env are implemented
in the target language by types of the form jenv j and j;env j
respectively, as dened below:
jft1:: 1  : : :  tn:: n gj = h 1  : : :  n i
jfx1:1  : : :  xn:ngj = h1  : : :  ni:
The most interesting rules are the term translations ofvalue and type abstractions. In each case, an appropriate type environment and value environment must be constructed as part of the closure. Thus, assignments env and;env must be chosen as subsets of the current assignments
env ] arg and ;env ] ;arg respectively. These assignments
must be chosen so that all of the free value variables of theterm are contained in ;env and furthermore, all of the free
type variables of the term and the value environment must
be contained in env .
The chief technical diculty in formulating these rules
is that we need two type assignments, ;env and ;env , to describe the value environment of the closure, depending upon
the context. The type assignment ;env is constructed fromthe context env  arg  ;env  ;arg and is used to build theenvironment eve in the context in which the closure is constructed. The type assignment ;env is obtained from ;env
via the translation env  . ;env ;env and corresponds
to the type of the value environment in the context of theclosure itself. This ensures that the code of the closure isclosed since the type ascribed to the value environment argument does not refer to free type variables in the context
where the closure was created.
The type correctness of the translation is proved by induction on the derivation of the translation.
8

0

8

0

0

0

0

0

0

0

0

00

0

00

0

0

0

00

e and env ]arg  ;env ];arg ` e : , then ftte ::jenv jg]arg  fxve:j;env jg];arg ` e :  where env  arg .   , env  arg .
;env ;env , and env  arg . ;arg ;arg .
The correctness of the translation may be established using an argument similar to that given for the simply-typed
case. The restriction to predicative polymorphism signicantly simplies the proof.

Theorem 4 If env  arg  ;env  ;arg . e
0

0

0

0

0

0

0

0

5.2 Closure Representation

We now turn to the representation of closures for the polymorphic language.
The target language for polymorphic closure representation, called  , is dened as follows:
Kinds ::= k j $ j h 1  : : :  n i
Types  ::= b j t j h1  : : :  n i j h1  : : :  n i j i  j
8t:: : j 1 ) 2 j 1 ! 2 j 9t:: : j 9k:Exp's e ::= x j c j x::e j e1 e2 j #t:: :e j e  j
8 9h e  : : :  en i j i e j
1

pack
open
pack
open

 with e as  je as t:: with x: in ewith e as  je as k with x: in e000

Our translation of function types involves existential quantiers. Since function types can instantiate a polymorphic
type in the source language, we need to be able to instantiate
polymorphic types with existentials in the target language.
As a consequence, the target language must be impredicative. To simplify the language, we provide general abstractions ( and #), instead of code types that abstract morethan one argument at a time.
Since we shall have limited need of existential kinds, wemust introduce kind variables k into the language, with corresponding kind contexts and judgements. A kind context K
is simply a sequence of kind variables fk1  : : :  kn g, (n 0).
The typing judgements of the language are as follows:K  `  ::
 has kind .
K  ` 1  2 :: 1 and 2 are equal types of kind .
K  ; ` e : 
e has type .
The formation rules, denitional equality rules, and typing rules are standard except that values of polymorphic
type 8t:: : may be coerced to the special type  )  =t],where  is a type of kind , as described in the Section 4.
The details of the typing rules are found in the companion
technical report 21].
We dene the closure representation stage as a typedirected translation from cl to  . We begin by deninga translation from source constructors and types to target
type as follows:
jtj = tjbj = bjh1 : : :  nij = hj1j : : :  jnjij j =  jjjh1  : : :  ni ij = hji1j  : : :  jnji
jvcode(t::       )j = 8t:: :j j ! j j ! j j
jtcode(t::  veves:: 1 22)j = 8t:: :jvevej ! 8s1:: :j22j
j1 ! 2j = 9k:9t0 ::$:9t::k:h(t ) t0 ! j1j ! j2j)  t0i
j8s:: :2j = 9k:9t0::$:9t::k:h(t ) t0 ! 8s:: :j2j)  t0i
0

0

0

8

0

8 9

0

ftte:: teg fxve:ve x:1g ` e : 2 ; ` #tte:: te : xve :ve : x:1 :e : vcode(tte:: te  ve  1  2 )ftte:: te t::$g fxve:veg ` e :  ; ` #tte:: te : xve :ve :#t::$:e : tcode(tte:: te  ve  t ) ; ` e1 : vcode(tte:: te ve  1  2 )  `  : te  ; ` e2 : ve =tte]
 ; ` hhe1   e2 ii : (1 ! 2 )=tte]
 ; ` e1 : tcode(tte :: te  ve  t )  `  : te  ; ` e2 : ve =tte]
 ; ` hhe1  e2 ii : (8t::$:2)=tte ]Figure 5: Typing Rules for Code and Closures of cl
8ft ::$ : : :  tn::$g  . ti i t   . t t (t 2 Dom( ))  .     .     ] ft::$g .    .  !   !    . 8t:: :  8t:: :   . t    . tn n   . ft ::$: : :  tn ::$g h  : : :  n i  .     . n n   . fx :  : : :  xn :n g fx :  : : :  xn :n g
env  arg . b

b

env

env

arg
env

1
arg

0

arg

arg

env
2

1
1

1

arg

arg

2

1

2

0

env
arg
env
arg

0

0

1

0

1

0

1
1 1

0

env
arg
env
arg

2

0

0

env
arg
1
env
arg

te

1

env

arg
1

env

arg
0
1 1

0

0

0

0

Figure 6: Polymorphic Abstract Closure Conversion: Types and Type Assignments(const) env  arg  ;env  ;arg . c c(env) env  arg  fx1 :1  : : :  xn :n g ;arg . xi i xve(arg) env  arg  ;env  ;arg . x x (x 2 Dom(;arg ))env  arg  ;env  ;arg . env te env  arg  ;env  ;arg . ;env eve
env  . ;env ;env env  . 1 1(abs)
env   ;env  fx:1 g . e e
env  arg  ;env  ;arg . x:1 :e hh#tte::jenv j: xve:j;env j: x:1 :e  te eve ii
0

0

0

0

00

0

0

0

0

0

0

00

0

0

env  arg  ;env  ;arg . env te env  arg  ;env  ;arg . ;env eve
env  . ;env ;env env  ft::$g ;env  . e e
env  arg  ;env  ;arg . #t::$: e hh#tte::jenv j: xve:j;env j:#t::$: e  te  eveii
0(tabs)

0

0

0

00

0

0

0

0

00

0

 ;arg . e1 e1 env  arg  ;env  ;arg . e2(app) env  arg  ;env
env  arg  ;env  ;arg . e1 e2 e e

e2

0

0

1

2

 ;env  ;arg . e e env  arg . (tapp) env  argenv  arg  ;env  ;arg . e  e 



0

0

0

0

0

0

env  arg  ;env  ;arg . xi ei(context) env  arg  ;env
 ;arg . fx1 :1  : : :  xn :n g he1  : : :  en i00

Figure 7: Polymorphic Abstract Closure Conversion: Terms

0

The code types are translated to the appropriate combination of target 8 and ! types. The translation of a function
type abstracts the kind of the type environment, k, and thetype of the value environment, t0 . The type environment t
is paired with the code by using an existential type. Since
the type of a code is instantiated by t, only the type environment of the closure can be given to the code. The codeand the value environment are paired as in the simply-typed
case. The translation of 8 has the same structure as that ofan arrow type.
The translation of expressions is summarized in Figure 8.
The kind of the type environment, the type of the value environment, and the type environment are packed with thepair of the code and the value environment. In the translation of applications, the type environment is obtained froma closure by an open expression and the code and the value
environment are obtained by projections. Then the typeenvironment, the value environment, and the argument ofapplication are passed to the code.
Type preservation is proved by induction on the structure of the translation derivation. The typing rules for )  are essential to prove the cases for the translationsof closures.
Theorem 5 If  ; . e :  e , then   j;j ` e : jj.
The correctness of the translation can be proven using
logical relations as in the simply typed case. However, thedenition of the relations is more complicated because of thepresence of polymorphic types and types of the form i ( )in the language cl . The relations and the proof appear
in the companion technical report 21].
0

0

0

8

6 Summary and Conclusions
We have given a type-theoretic account of closure conversion
by dening type-directed transformations for the simplytyped and polymorphic -calculi. The types used in thetarget languages of the translations may be characterized
in a natural way based on the \closures as objects" principle. In both the simply-typed and polymorphic cases ofclosure representation, we used Pierce-Turner-style existentials to hide the representations of environments. In thepolymorphic case, we took advantage of Harper-Lillibridgestyle translucency to ensure that the same type environmentis used to type both the code and the value environment ofa closure.
Our translations preserve types, facilitating correctness
proofs and composition with other type-based translations.
Furthermore, our translations provide support for run-time
type analysis and type-based, tag-free garbage collection.
We have put the ideas in this paper to practical use in
two separate compilers for ML. One compiler is being used
to study novel approaches to tag-free garbage collection.
The other compiler, called TIL (Typed Intermediate Languages), provides a general framework for analyzing types
at run time to support ecient data representations, ecient calling conventions, and \nearly" tag-free garbage collection in the presence of polymorphism 36]. Propagating
types through closure conversion is necessary for both compilers so that types can be examined at run time.
We have found that propagating types through closure
conversion (and other compilation phases) has an additional
engineering benet. In particular, we can automatically verify the type-integrity of each type-preserving phase in thecompiler. Indeed, automatic type-checking has enabled us
to isolate and eliminate various subtle bugs in TIL.
For simplicity, the current implementations of our compilers use only abstract closure conversion. However, bothcompilers extend this translation to avoid creation of closures for \known" functions in the style of Wand and Steckler 39]. In the future, we hope to use the closure representation phase described here to further expose closure handling
operations to optimization.

7 Acknowledgements
We would like to thank Lars Birkedal, Andrzej Filinski,
Mark Leone, Sue Older, Benjamin Pierce, Paul Steckler,
David Tarditi, and the anonymous reviewers for their many
helpful comments and suggestions.

References

1] A. W. Appel. Compiling with Continuations. Cambridge
University Press, 1992.
2] A. W. Appel and T. Jim. Continuation-passing, closurepassing style. In ACM Symp. on Principles of Programming
Languages, 1989.
3] D. E. Britton. Heap storage management for the programming language Pascal. Master's thesis, University of Arizona,
1975.
4] L. Cardelli. The functionalabstract machine. Polymorphism,
1(1), 1983.
5] C. Cousineau, P.-L. Curien, and M. Mauny. The categoricalabstract machine. In Functional Programming Languages
and Computer Architecture, pages 50{64, 1985.
6] H. Friedman. Equality between functionals. In R. Parikh,
editor, Logic Colloquium '75. Norh-Holland, 1975.
7] J.-Y. Girard, Y. Lafont, and P. Taylor. Proofs and Types,
volume 7 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, Cambridge, England,
1989.
8] J. Gosling. Java intermediate bytecodes. In ACM SIGPLAN Workshop on Intermediate Representations (IR'95),
Jan. 1995.
9] J. Hannan. A type system for closure conversion. In The
Workshop on Types for Program Analysis, 1995.
10] R. Harper and M. Lillibridge. Explicit polymorphism and
CPS conversion. In ACM Symp. on Principles of Programming Languages, 1993.
11] R. Harper and M. Lillibridge. A type-theoretic approach
to higher-order modules. In ACM Symp. on Principles ofProgramming Languages, pages 123{137, 1994.
12] R. Harper, D. MacQueen, and R. Milner. Standard
ML. Technical Report ECS{LFCS{86{2, Laboratory for
the Foundations of Computer Science, EdinburghUniversity,
Mar. 1986.
13] R. Harper and J. C. Mitchell. On the type structure of Standard ML. ACM Transaction on Programming Languages
and Systems, 15(2), 1993.
14] R. Harper and G. Morrisett. Compiling polymorphism using
intensional type analysis. In ACM Symp. on Principles ofProgramming Languages, pages 130{141, 1995.
15] T. Johnsson. Lambda lifting: Transforming programs to recursive equations. In Functional Programming Language andComputer Architecture, LNCS 201, pages 190{203. SpringerVerlag, 1985.

; . e : vcode(tte:: te  ve  1  2 ) e  ; . eve : ve eve(vcl)  ; . hhe  eveii : 1 ! 2 packte  jve j j j with he  eve i as j1 ! 2 j
0

0

0

0

0

0

0

 ; . e1 : 1 ! 2 e1  ; . e2 : 1 e2
open e1 as kte tve  tte(app)  ; . e1 e2 : 2with y : htte ) tve ! j1 j ! j2 j  tve iin (1 y) tte (2 y) e2; . e : tcode(tte:: te  ve  t::   ) e  ; . eve : ve eve(tcl)  ; . hhe eve ii : 8t:: :2 pack te jvej j j with he  eve i as j8t:: :j ; . e : 8t:: : e

;
.
e

:


=t
]
open e as kte tve  tte(tapp)
with y : htte ) tve ! 8t:: :j j  tve iin (1 y) tte (2 y ) j j
0

0

0

0

0

0

0

0

0

0

0

0

Figure 8: Polymorphic Closure Representation
16] R. Kelsey and P. Hudak. Realistic compilation by programtranslation {detailed summary {. In ACM Symp. on Principles of Programming Languages, pages 281{292, 1989.
17] D. Kranz et al. Orbit: An optimizing compiler for Scheme.
In Proc. of the SIGPLAN '86 Symp. on Compiler Construction, 1986.
18] X. Leroy. Unboxed objects and polymorphictyping. In ACM
Symp. on Principles of Programming Languages, 1992.
19] X. Leroy. Manifest types, modules, and separate compilation. In ACM Symp. on Principles of Programming Languages, pages 109{122, 1994.
20] D. MacQueen. Modules for Standard ML. In Proc. ACM
Conf. Lisp and Functional Programming, pages 198{207,1984. Revised version appears in 12].
21] Y. Minamide, G. Morrisett, and R. Harper. Typed closure
conversion. Technical Report CMU{CS{95{171, School ofComputer Science, Carnegie Mellon University, July 1995.
22] J. C. Mitchell and G. D. Plotkin. Abstract types have existential type. ACM Transaction on Programming Languages
and Systems, 10(3), 1988.
23] G. Morrisett, M. Felleisen, and R. Harper. Abstract modelsof memory management. In Functional Programming Languages and Computer Architecture, pages 66{77, June 1995.
24] R. Morrison, A. Dearle, R. Connor, and A. L. Brown. An
ad hoc approach to the implementation of polymorphism.
ACM Transaction on Programming Languages and Systems,
13(3), 1991.
25] A. Ohori. A compilation method for ML-style polymorphic
record calculi. In ACM Symp. on Principles of Programming
Languages, 1992.
26] B. C. Pierce and D. N. Turner. Simple type-theoretic foundations for object-oriented programming. Journal of Functional Programming, 4(2):207{247, Apr. 1994. A preliminary
version appeared in Principles of Programming Languages,
1993, and as University of Edinburgh technical report ECSLFCS-92-225, under the title \Object-Oriented Programming Without Recursive Types".
27] G. D. Plotkin. Lambda-denability in the full type hierarchy.
In To H.B.Curry: Essays on Combinatory Logic, Lambda
Calculus and Formalism. Academic Press, 1980.
28] U. S. Reddy. Objects as closures. In Proc. ACM Conf. Lispand Functional Programming, 1988.
29] J. C. Reynolds. Denitional interpreters for higher-orderprogramming languages. In Proceedings of the Annual ACM
Conference, pages 717{740, 1972.

30] Z. Shao and A. W. Appel. Space-ecient closure representations. In Proc. ACM Conf. Lisp and Functional Programming, 1994.
31] Z. Shao and A. W. Appel. A type-based compiler for Standard ML. In Programming Language Design and Its implemenation, pages 116{129, 1995.
32] R. Statman. Completeness, invariance, and lambdadenability. Journal of Symbolic Logic, 47:17{26, 1982.
33] R. Statman. Logical relations and the typed -calculus. Information and Control, 65, 1985.
34] G. L. Steele Jr. Rabbit: A compiler for Scheme. Master's
thesis, MIT, 1978.
35] W. W. Tait. Intensional interpretation of functionals of nite
type. Journal of Symbolic Logic, 32(2), 1967.
36] D. Tarditi, G. Morrisett, P. Cheng, C. Stone, R. Harper,
and P. Lee. TIL: A type-directed optimizing compiler for
ML. Technical report, School of Computer Science, Carnegie
Mellon University, Oct. 1995. To appear.
37] A. Tolmach. Tag-free garbage collection using explicit typeparameters. In Proc. ACM Conf. Lisp and Functional Programming, pages 1{11, June 1994.
38] R. Wahbe, S. Lucco, T. Anderson, and S. Graham. Ecient
software-based fault isolation. In 14th ACM Symposium on
Operating Systems Principles, Dec. 1993.
39] M. Wand and P. Steckler. Selective and lightweight closure
conversion. In ACM Symp. on Principles of Programming
Languages, 1994.