Closing the Stage
From Staged Code to Typed Closures
Yukiyoshi Kameyama

Oleg Kiselyov

Chung-chieh Shan

University of Tsukuba
kameyama@acm.org

FNMOC
oleg@pobox.com

Rutgers University
ccshan@cs.rutgers.edu

Abstract1.

Code generation lets us write well-abstracted programs without
performance penalty. Writing a correct code generator is easier thanbuilding a full-scale compiler but still hard. Typed multistage languages such as MetaOCaml help in two ways: they provide simple annotations to express code generation, and they assure thatthe generated code is well-typed and well-scoped. Unfortunately,
the assurance only holds without side effects such as state andcontrol. Without effects, generators often have to be written in
a continuation-passing or monadic style that has proved inconvenient. It is thus a pressing open problem to combine effects withstaging in a sound type system.
This paper takes a first step towards solving the problem, bytranslating the staging away. Our source language models MetaOCaml restricted to one future stage. It is a call-by-value language,
with a sound type system and a small-step operational semantics,
that supports building open code, running closed code, cross-stage
persistence, and non-termination effects. We translate each typing
derivation from this source language to the unstaged System F withconstants. Our translation represents future-stage code using closures, yet preserves the typing, α-equivalence (hygiene), and (weconjecture) termination and evaluation order of the staged program.
To decouple evaluation from scope (a defining characteristic ofstaging), our translation weakens the typing environment of open
code using a term coercion reminiscent of Gödel’s translation fromintuitionistic to modal logic. By converting open code to closureswith typed environments, our translation establishes a frameworkin which to study staging with effects and to prototype staged
languages. It already makes scope extrusion a type error.

Keywords Multistage programming, type abstraction, parametricpolymorphism, mutable state and control effects, closures

Code generation is the most promising approach in high-performance computing (Püschel et al. 2005) and high-assurance embedded programming (Hammond and Michaelson 2003). Because ageneric program in an earlier stage can generate a specialized program in a later stage and assure it safe, the programmer need nottrade off abstraction and assurance for efficiency in time and space.
An attractive way to express such code generation is to use a
multistage programming language such as MetaOCaml (Lengauer
and Taha 2006), in which the programmer need only annotate theprogram to separate the stages (Taha 2004). Staging provides aprincipled interface through which a code generator can take advantage of the implementation of the language it is written in, whether
or not that implementation is a self-interpreter that can be specialized (Jones 1988). The applications of staging thus include theusual uses of code generation, such as partial evaluation (Davies
and Pfenning 2001; Ghani et al. 1998), embedding domain-specificlanguages (Czarnecki et al. 2004; Pašalić et al. 2002), and controlling special processors (Elliott 2004; Taha 2005).
Staging lets us symbolically manipulate pieces of open code,
which may contain free variables that will be bound to actual values
only at a future stage. Yet a staged language should ensure that αconversion preserves the meaning of a program, and that the code
finally generated is closed, that is, does not contain free variables(Taha and Nielsen 2003). Staged type systems exist in the literaturethat achieve these goals (Calcagno et al. 2004; Taha and Nielsen2003), but they do not consider side effects with open code.
Side effects let us apply code-generation techniques such as
let insertion without cumbersome programming in continuationpassing or monadic style. In particular, delimited control is usefulfor partially evaluating programs using sum types (Balat et al. 2004;
Lawall and Danvy 1994) and delimited control (Asai 2002), andmutable state and delimited control make it easy to express let
insertion (Sumii and Kobayashi 2001; Swadi et al. 2006) and tocount generated operations. Unfortunately, these effects with open
code make it possible to generate ill-scoped code—that is, to cause
scope extrusion—in all multistage type systems today.
Our motivation is to write effectful code generators in a language like MetaOCaml without risking scope extrusion. In otherwords, we want a multistage type system that is sound with effects.

Permission to make digital or hard copies of all or part of this work for personal orclassroom use is granted without fee provided that copies are not made or distributedfor profit or commercial advantage and that copies bear this notice and the full citationon the first page. To copy otherwise, to republish, to post on servers or to redistributeto lists, requires prior specific permission and/or a fee.
PEPM’08, January 7–8, 2008, San Francisco, California, USA.
Copyright c 2008 ACM 978-1-59593-977-7/08/0001. . . $5.00

Contributions To design a multistage type system that is soundwith effects, we must understand how effects interact with staging.
α , which models
To this end, we translate in this paper a language λ1v
the mature and practical multistage language MetaOCaml (§3), into
System F, which lacks staging (§4). Our translation incurs the overhead of functional and type abstraction, but keeps the speedup of
specialization and expresses the static and (we conjecture) dynamic
α , including the order of effects among stages (§5).
semantics of λ1v
Our translation reduces both closed and open code to closures.

Categories and Subject Descriptors D.3.1 [Programming Languages]: Formal Definitions and Theory; D.3.3 [Programming
Languages]: Language Constructs and Features—Control structures; polymorphism; F.3.3 [Logics and Meanings of Programs]:
Studies of Program Constructs—Type structure
General Terms Design, Languages

Introduction

Because we aim to combine staging with effects (especially delimited control), we formalize our source language using a smallstep operational semantics with evaluation contexts (Wright andFelleisen 1994). With staging, our redexes may be open and evaluation contexts may be binding (§3.2). Such a small-step semantics has only been used to study call-by-need (Ariola and Felleisen
1997; Maraist et al. 1998) to our knowledge. We prove subject reduction, determinism, and progress for this source language (§3.3).
After describing the translation, we present three payoffs: strong
normalization for the source language without fix (§5.3), detecting
scope extrusion (§6), and counting arithmetic operations in a soundstaged language (§6).
MetaOCaml supports an unlimited number of future stages(Glück and Jørgensen 1997), so generated code may in turn generate code. In this paper, we restrict ourselves to one future stage,
which suffices in many real-life applications (Carette and Kiselyov
2005; Lengauer and Taha 2006) and where issues such as scope
extrusion and cross-stage persistence already arise (see §2). Theseissues force us to type environments more precisely yet polymorphically, which complicates and distinguishes our translation ascompared to typed closure conversion (Minamide et al. 1996).

2.

The basics of staging and our translation

We begin by informally sketching our translation on some examples, starting with the classic power function. We use the language
formalized in §3, which is like OCaml with staging annotations(explained below) and fix (in place of let rec). Our examples in
MetaOCaml and translations in OCaml are all available online at
http://okmij.org/ftp/Computation/staging/.
let square = λ x :int. x × x
let power = (* (α) (int → hintiα → hintiα ) *)(α) fix f (n : int) : hintiα → hintiα . λ x :hintiα .
if n = 0 then h1iα
else if n mod 2 = 0 then h%square ∼( f (n/2) x)iαelse h∼x × ∼( f (n − 1) x)iα
let power7 = (* (α) (int → int) *)run(α)hλ xα :int. ∼(printf “power”; power[α] 7 hxα iα )iαlet res = (α) (power7 [α] 2, power7 [α] 3)This code uses staging annotations: bracket heiα , escape ∼e, crossstage persistence %e, and run e. The superscript α is a classifier,explained in §3. To ease the notation, we will often drop the classifier where it can be easily inferred according to the syntax of §3;
for now, classifier annotations along with the classifier introduction(α)e and the classifier application e[α] may be disregarded. If we
ignore these annotations—that is, regard heiα , ∼e, %e, run e, (α)e,and e[α] as just e, and xα as just x—then the code expresses a standard way to compute xn . The expression
λ x:int. (printf “power”; power 7 x)
builds a closure that includes the printf operation and the power
computation. The body of the closure is of course not evaluateduntil the argument x is supplied, so nothing is printed when power7
is computed. Computing res invokes power7 twice and so prints“power” twice with the unstaged code.
With staging annotations, the picture is different. The code still
expresses the same algorithm, but the computations are performedat different stages. The bracket heiα , like quasiquote in Lisp,
says to execute e at a future stage. If e has the type int, then heiα
has the type hintiα . The escape ∼e, like unquote in Lisp, says
to evaluate e while building a future-stage computation. The resultof e at the present stage must be a future-stage computation and is
spliced into the future-stage computation being built. The construct
run e, like eval in Lisp, evaluates the computation e.

With staging annotations in the code above, “power” is printed
only once—when power7 is evaluated. Consequently, when wecompute res, nothing is printed, and the function power is not
executed because the loop over n has been already performed. The
body of power7 is λ x. x × square (x × square (x × 1)).
2.1

Naı̈ve non-solution

Our goal is to represent staged computations in a regular language,
namely System F (§4). The essence of staging is to quote computations, delaying their execution to some future time. In call-by-value
languages, the standard way to delay a computation is to put it intoa function or simply a thunk. We may be tempted then to represent the type hti as () → t, the bracket expression hei as λ (). e, theescape ∼e and run e as e (), and cross-stage persistence %e as e.
If we interpret our staged power code that way, it works justlike the unstaged code: “power” is printed twice, when we compute res. Thus, we got rid of staging along with its benefit. This
failure to represent staging can be understood by considering an
expression h∼ei. The staged language evaluates e while building
the bracketed expression, so any side effect in e will occur then.
Our naı̈ve interpretation turns the expression into λ (). e(). Here e
becomes encapsulated into a thunk, so it will be evaluated when thebracketed computation is run, not while it is built.
For the thunk to encapsulate only the result of an escape and not
the escape itself, we need to ‘lift’ the escape out of the thunk, thatis, interpret h∼ei as let v = e in λ (). v(). But then, the expression
hλ xα :int. ∼(printf “power”; power[α] 7 hxi)i
in power7 above would become
let v = printf “power”; power[α] 7 λ (). x in λ (). λ x :int. v()
Now printf occurs outside the thunk, but so does the unboundvariable x. After all, we are supposed to compute v before a value
is supplied for x. Staging lets us use a variable symbolically before
it is bound to a value. Our translation must thus deal with symbolicreferences to variables without values (Taha 1999; §7.2.1).
2.2

Environment passing

To translate symbolic variable references, we can model the environment as a record whose keys are such first-class references. To
explore this idea, let us introduce an abstract data type of extensible records: R0 is some initial environment; R(0 x = v) extends theenvironment R by associating the key 0 x to the value v; and R(0 x)
looks up the value associated with the key 0 x in the environment R.
We can represent a code expression hei as λ R. . . . , where theargument R associates the free variables in e to their values. For
example, we represent hxi as λ R. R(0 x), a projection from theenvironment. This function is first-class and can be passed aroundbefore we have a concrete environment to apply it to. We represent
run e by applying the representation of e to R0 . Likewise, weinterpret the escape h∼h1ii as let v = λ R. 1 in λ R. vR. A binding
operation under bracket should extend the effective environment,
so we can translate let f y = h∼y + 1i in hλ x. ∼( f hxi)i as
let f y = λ R. yR + 1 inlet v = f (λ R. R(0 x)) in λ R. λ x. v (R(0 x = x)).
For this translation to work, we must ensure that look-up always succeeds. We prove it does below by assigning types to environments that reflect their contents. We should also specify how
to α-rename a translated expression: it is easy to rename x to y inhλ x. ∼( f hxi)i without affecting the meaning of the expression, but
it is more involved to perform the same renaming on our translation,
because we need to replace x with y as well as 0 x with 0 y. Before
addressing these issues, we use this approach to translate power.

let square = λ x. x × x
let power = fix f (n). λ x.
if n = 0 then λ R. 1
else if n mod 2 = 0
then let v = f (n/2) x in λ R. square(vR)
else let v1 = x in let v2 = f (n − 1) x in
λ R. v1 R × v2 R
let power7 = let v = printf “power”; power 7 λ R. R(0 x) in(λ R. λ x. v (R(0 x = x))) R0
let res = (power7 2, power7 3)
As in the staged code, the string “power” is printed only once, when
we compute power7.
2.3

Environment polymorphism

A common practice in staged programming is to splice a pieceof open code into a scope with additional bindings. Translating
this practice requires polymorphism, as we explain with a simple
example. The example is a function ef from the code type hintiα tothe code type hint → intiα . It splices the argument into code withan extra binding. Below we define ef and use it in two examples.
let ef = (α)λ z:hintiα . hλ xα :int. ∼z + xα iα
let ef 1 = (α)ef [α]h1iαlet ef 2 = (α)hλ xα . λ yα . ∼(ef [α]hxα × yα iα )iαThe term ef 1 evaluates to (α)hλ x. 1 + xi whereas ef 2 evaluates to(α)hλ x. λ y. λ x0 . x × y + x0 i. In the latter result, we need to distinguish two later-stage variables named x. To maintain hygiene andα-equivalence, we must lexically link each use of a variable to its
binding occurrence and rename variables if their names clash.
Applying the informal translation of the previous section to thisexample shows several problems.
let ef = λ z. λ R. λ x. z(R(0 x = x)) + x
let ef 1 = ef (λ R. 1)
let ef 2 = let v = ef (λ R. R(0 x) × R(0 y)) inλ R. λ x. λ y. v(R(0 x = x)(0 y = y))
The first problem is that ef needs a polymorphic type. To typecheck the multiplication R(0 x) × R(0 y), the type of R should associate the keys 0 x and 0 y with the type int, but R in ef 1 may notcontain a mapping for 0 y. In general, we may invoke ef in the scopeof any number of later-stage variables, so we seem to need so-calledρ-polymorphism for our environment records. The use of ef should
be typed in ef 1 as∀ρ. ({ρ} → int) → ({ρ} → int → int)
but in ef 2 as

2.4

Maintaining hygiene

We maintain α-equivalence and avoid name clashes by representing R not as a record keyed by names but as a tuple keyed byindices. The typing environment of the staged code is an orderedsequence of bindings, so we can use that ordering to index into R
at run time. This idea is reminiscent of de Bruijn indices, but we
index only later-stage variables and pass the indices around during
the earlier stage as first-class code values.
The translation of a code expression thus depends on the laterstage variables in scope. For example, the code expression h1itranslates to λ (). 1 in the empty typing environment. The expression hxi translates to λ x. x if x is the only later-stage variable in
the typing environment, but to λ (x,y). x if the typing environment
contains the later-stage variables x and y, in that order. To splicein a code value is to apply it to the current later-stage environment
reified as a tuple, so the translation of hλ x. λ y. ∼hx × xi + y × yi isessentially λ (). λ x. λ y. (λ (x,y). x × x)(x, y) + y × y.
A code value may be created in one typing environment thenused in many others, as inlet z = h1i in hλ xα :int. ∼z + xα i.

(1)

The code value z is created in an environment with no later-stage
variable, then used in an environment with one later-stage variable x. In general, the environment of use must extend the environment of creation; it is no accident that this crucial invariant holds inthe absence of effects. Having translated h1i to λ (). 1 in the empty
environment, we would commit a type error were we to translate∼z in (1) by applying λ (). 1 to (x). Instead, we need to coerce thecode value to accommodate the extended environment. Given theenvironment of use and of creation, it is easy to see that we should
apply the coercion λ f . λ (x). f () to λ (). 1. We thus translate (1) to
let z = λ (). 1 in λ (). λ x. (λ f . λ (x). f ()) z (x) + x.

(2)

(Actually, our formal translation produces some additional β -value
redexes. The gory details are shown in §5.2.)
A second sort of polymorphism arises when a function takes acode value as argument, as ef above does. The translation of thecode argument is a function from environments, but we do notknow those environments’ type when translating the function because the code argument may use any number of later-stage variables. Therefore the function must translate to a polymorphic function whose type is of the form ∀π. (π → · · · ) → · · · . For example,
we translate ef to a function of type ∀π. (π → int) → (π → int →int). As the examples using ef in §2.3 show, each application of ef
may instantiate the type variable π to a different environment type.
In particular, we translate ef 1 and ef 2 there as follows.

∀ρ. ({0 x:int ,0 y:int , ρ} → int) → ({0 x:int ,0 y:int , ρ} → int → int).

let ef 1 = ef [()](λ (). 1)
let ef 2 = let v = ef [(int , int)](λ (x,y). x × y) in λ (). λ x. λ y. v(x, y)The α-renaming problem noted above also rears its head. To
maintain hygiene, the translation needs to detect potential nameclashes among variables and avert them by renaming variables
along with fields in R. The translated example above does not work
because the extensions R(0 x = x) on the first and last lines clash.
To prevent such a clash, our type for R seems to require not only ρpolymorphism but also negative side conditions that state the namesthat must not occur in any instantiation of the polymorphic type.
Such conditions complicate type checking, especially with multiple
staging levels, yet still leave the problem of preserving the meaningof programs in the face of α-conversion (Taha and Nielsen 2003;§1.4). Taha and Nielsen avoid these difficulties by ingeniously
introducing classifiers, which track just enough information about
the structure of environments to ensure type safety in a staged
language without effects. Alas, we need more precision to maintainhygiene in a language with effects or without staging support.

It remains to translate ef itself, or equivalently, to translate its
body hλ xα :int. ∼z + xα iα in the environment z : hintiα . Again because the code value z may use any number of later-stage variables,
the translated type of z is π → int where π is a Λ-bound type variable. The code value returned by the translation of ef should havethe type π → int → int. Guided by these types and using the techniques described above, we obtain the translation
let ef = Λπ. λ z:π → int. λ r:π. λ x:int. (λ f . λ (r,x). f r)z(r, x) + x.
2.5

A higher-order example

A more complex example to translate is staged η-expansion, ahigher-order function on code values that is useful in staged programming and difficult for staged type systems (Taha and Nielsen
2003; §1.4). Below we define eta and give an example of its use.

Classifiers
Named levelsα, βA, B ::= 0 | αTypesFlat types

t ::= int | t → t | (α)t | huiαu ::= int | u → u

Variables

xA , yA , zA , f A

EnvironmentsΓ ::= [] | Γ, α | Γ, x : t | Γ, xα : uExpressions

e0 ::= i0 | x0 | λ x0 :t. e0 | fix f 0 (x0 : t) : t. e0 | e0 + e0 | e0 e0 | (α)e0 | e0 [α] | run e0 | heα iα
eα ::= iα | xα | λ xα :u. eα | fix f α (xα : u) : u. eα | eα + eα | eα eα | ∼e0 | %e0Valuesv0 ::= i0 | x0 | λ x0 :t. e0 | fix f 0 (x0 : t) : t. e0 | (α)v0 | hvα iα
vα ::= iα | xα | λ xα :u. vα | fix f α (xα : u) : u. vα | vα + vα | vα vα | %e0Contexts

C0 [ ] ::= [ ] | C0 [[ ] + e0 ] | C0 [v0 + [ ]] | C0 [[ ]e0 ] | C0 [v0 [ ]] | C0 [(α)[ ]] | C0 [[ ][α]] | C0 [run [ ]] | Cα [∼[ ]]Cα [ ] ::= Cα [[ ] + eα ] | Cα [vα + [ ]] | Cα [[ ]eα ] | Cα [vα [ ]] | Cα [λ xα :u. [ ]] | Cα [fix f α (xα : u) : u. [ ]] | C0 [h[ ]iα ]]αFigure 1. Syntax of λ1v

let eta = (α)λ f :hintiα → hbooliα . hλ xα :int. ∼( f hxα iα )iαlet eta1 = (α)hλ yα . λ uα . ∼(eta[α](λ z. h∼z < yα × uα iα ))iαThe term eta1 evaluates to (α)hλ yα . λ uα . λ xα . xα < yα × uα iα .
The function f passed to eta maps the open code hxα i to codethat may contain free variables other than xα . In eta1 , for example,
f splices hxα i into the open code hxα < yα × uα i, which uses the
additional free variables yα and uα . Because f and eta introduce
their free variables separately, they are each polymorphic in thepart of the later-stage environment extended by the other (O’Hearn
and Tennent 1995). That is, the translation of eta uses a type variable π to represent whatever free variables f introduces (namely
yα and uα in eta1 ), and the translation of f uses a type variable π 0
to represent whatever free variable eta introduces (namely xα ). The
translation of eta thus has the polymorphic function type
∀π. (∀π 0 . ((π, π 0 ) → int) → ((π, π 0 ) → bool))→ (π → int → bool),(3)

in which π is to be instantiated by the caller and π 0 by the callee.
In particular, the caller eta1 instantiates π to the tuple type(int , int) corresponding to yα and uα . Our formal translation performs this instantiation as part of coercing eta from its environmentof creation, which is empty, to its environment of use in eta1 , whichbinds yα and uα . As formalized in §5.1, this coercion
λ g. λ f . g[(int , int)](Λπ 0 . λ z. let z0 = f [π 0 ](λ (y,u,r). z((y, u), r)) inλ ((y,u),r). z0 (y, u, r))
is a function from the type (3) to the type(∀π 0 . ((int , int , π 0 ) → int) → ((int , int , π 0 ) → bool))→ ((int , int) → int → bool).

(4)

Our translation of eta1 is then essentially
let v = eta[(int , int)](Λπ 0 . λ z. λ ((y,u),r). z((y, u), r) < y × u) in
λ (). λ y. λ u. v(y, u).
Meanwhile, it is easier to translate eta to the type (3), as follows.
let eta = Λπ. λ f . let v = f [int](λ (r,x). x) in λ r. λ x. v(r, x)

3.

αThe source language λ1v

α , a simplyFigure 1 presents the syntax of our source language λ1v
typed call-by-value λ -calculus with fix and staging annotations.
This calculus is closely based on Taha and Nielsen’s λ α (2003) but
limited to only one future stage. Modulo this limitation, the two
calculi are equally expressive, as detailed in §3.4.
As our metavariable notation indicates, we superscript each expression eA , value vA , variable xA , and context CA [ ] with a namedlevel A, to be explained shortly. Literal constants, variables, abstractions, applications, and additions are standard. We define justone base type, int, but our examples use bool analogously. Because our language is call-by-value, we write an η-expanded fixpoint fix f A (xA : t1 ) : t2 . e for a recursive function with the argument
type t1 and return type t2 , whose body e may refer to the function f
as well as the argument x. The bound variables are annotated with
their types, although we will often omit the types when they can beinferred. The form let x = e1 in e2 abbreviates (λ x. e2 )e1 as usual.
The language also contains brackets heiα , escapes ∼e, andrun e. There is also an explicit form %x for cross-stage persistence(CSP), left implicit in MetaOCaml. Bracket expressions heiα andcode types htiα are labeled by an environment classifier α (Tahaand Nielsen 2003). Classifiers are distinct identifiers that associate
code expressions with the environments in which they are typed. A
classifier α is bound by a so-called α-closed type expression (α)t,which is akin to ∀α.t universally quantifying over a phantom type
(Launchbury and Peyton Jones 1995) or a nonce name (Miller andTiu 2003). An α-closed type is introduced by a classifier generalization expression (α)e and eliminated by a classifier instantiation
expression e[α]. A classifier generalization expression (α)e assertsthat the classifier α is used exclusively in e; that is, it introduces afresh new classifier α to label code in e, akin to Λα. e generalizing
over a type variable α. Dually, a classifier instantiation expression
e[α] is akin to type application; it instantiates an α-closed expression with a particular classifier. The type system uses classifiers toprevent running open code.
Named levels A (or levels for short) generalize numbered levels
in staged calculi (Glück and Jørgensen 1997; Nielson and Nielson
1996). A level is a sequence of classifiers that qualifies a term, avariable, or an evaluation context. The sequence corresponds tothe nesting of code expressions and the ordering of stages. Our
α restricts levels to at most one classifier:language λ1v• The empty level, written 0, corresponds to the present stage, inwhich the top-level program expression is run.
• A level consisting of one classifier α, written α by a slightabuse of notation, corresponds to a future stage, in which codevalues of the form h. . .iα are run (Taha and Nielsen 2003).
We have no nested future stages (see Definition 3.2 below), so we
can express code generators but no generators of code generators.
Even with this restriction, it may still be useful to keep track ofseveral classifiers at once, to write code such as(α)hλ x. ∼( f (run(β )h1iβ )[α])iα(5)but not(α)hλ x. ∼( f (run(β )hxiβ )[α])iα .
(6)Named levels can allow (5) yet prevent the attempt to run open codein (6), whereas merely numbered levels cannot.

Γ ` i0 : int

α ∈Γ

(x0 : t) ∈ Γ(xα : u) ∈ Γ α ∈ ΓΓ ` iα : intΓ ` x0 : t

Γ ` xα : uΓ, xA : t1 ` eA : t2

Γ, f A : t1 → t2 , xA : t1 ` eA : t2

Γ ` (λ xA :t1 . eA ) : t1 → t2

Γ ` (fix f A (xA : t1 ) : t2 . eA ) : t1 → t2

Γ ` eA1 : intΓ ` eA2 : intΓ ` eA1 : t1 → t2

Γ ` eA1 + eA2 : intΓ ` eA2 : t1

Γ ` eA1 eA2 : t2Γ, α ` e0 : tΓ ` e0 : (α)tβ ∈ΓΓ ` e0 : (α)huiαΓ ` (α)e0 : (α)tΓ ` e0 [β ] : t [α := β ]Γ ` run e0 : (α)uΓ ` eα : uΓ ` e0 : huiαΓ ` heα iα : huiαα ∈ΓΓ ` (∼e0 )α : uΓ ` e0 : u
Γ, α, Γ0 ` (%e0 )α : u

α . We assume that the names of all
Figure 2. Type system of λ1vvariables and classifiers are unique.

To unclutter the notation, we often drop classifiers where they
are easy to infer. For example, we will write (α)h∼h1iα iα as
α disallows escape and CSP
merely (α)h∼h1ii. The syntax of λ1v
expressions at level 0, and the only way for a level-0 expression tocontain a non-level-0 expression is to contain a bracket expression,so escape and CSP can only occur inside brackets in a program.
The classification of expressions into values depends on thelevel of the expression. At level 0, the only values are literals,functions, classifier generalization over values, and brackets that do
not escape back to level 0. For example, h∼h1iα iα is not a value
but h1iα and h(λ x. x)1iα both are. Notably, h%e0 iα is a value foran arbitrary expression e0 ; see §3.4.
3.1

Type system

α . A type environment Γ is an
Figure 2 shows the type system of λ1v
ordered sequence of variable and classifier bindings. We sometimes
omit the empty environment [], from which all environments arebuilt. We adopt the convention that all classifier names, like variablenames, are unique. Thus, any environment of the form Γ, α, Γ0requires α ∈/ Γ, but α can be used to label bindings in Γ0 .
Just to simplify our presentation, we assume that every type uses
at most one level, in the following sense.

Definition 3.1 (Used levels) The set Used(t) of classifiers used in
α -type t is defined as follows.
a λ1v
Used(int) = {}Used(huiα ) = {α}Used(t1 → t2 ) = Used(t1 ) ∪ Used(t2 ) (7)Used((α)t) = Used(t) \ {α}(8)For example, Used(hintiα → hintiα ) is {α}.
α -type t
Definition 3.2 (Restriction to one level) Wherever a λ1v
appears (in a term, type, binding, or judgment), we restrict Used(t)to be either empty or a singleton {α}.

To rule out nested future stages, it is not enough to syntactically
exclude terms with nested brackets, because of CSP. For example,
the term let f = λ x. h∼x + 1i in hλ x. % f xi has no nested brackets,
but it is equivalent to hλ x. h∼x + 1ii, which has nested brackets.
Therefore, our restriction to one level must be stated using types.
The most important typing rules for us are those for bracket hei,
escape ∼e, and CSP %e, because they are the main way to move
between levels and to interact with variable and classifier bindings.
The typing derivation in Fig. 3 illustrates these rules. The leftmost
branch of the proof derives the eta example in §2.5, except changing the type int to bool so as to apply eta to the identity function.

The typing rule for CSP %e rejects terms such as hλ x. %hxii,
which cannot be run even though it type-checks in MetaOCaml.
In exchange for not generating such un-runnable code, we gain amuch simpler operational semantics, which we now turn to.
3.2

Operational semantics

α , using
Figure 4 gives the small-step operational semantics of λ1v
A
the definition of contexts in Fig. 1. A context C [ ] can be plugged
with an expression eA to give a level-0 expression. All redexes
are level-0 expressions except in the second-to-last transition. Of
course, evaluation can get stuck, as on the programs 1[β ] and 1(2).
The last transition, of the redex run (α)hvα iα , demotes vα as
defined in the second half of the figure. Demotion homomorphically maps values vα to level-0 expressions e0 , by replacing thelevel α by 0 in expression annotations and converting %e0 into e0 .
(We could have simplified the run transition, inherited from λ α , tojust C0 [run (α)hvα iα ] C0 [vα ↓].)
Staging complicates our operational semantics by making ourredexes possibly open and our evaluation contexts possibly binding. For example, the program (α)hλ xα :int. ∼((λ y. y) hxα iα )iαdecomposes into the open redex (λ y. y) hxα iα and the context(α)hλ xα :int. ∼[ ]iα . The context binds the classifier α and thenthe later-stage variable xα , whose level depends on α.

3.3

Properties

Proposition 3.3 (Subject reduction) If Γ ` e : t and ee0 then0Γ ` e : t.
Proof In particular, demotion preserves types: if Γ, α ` vα : uthen Γ ` vα ↓ : u. The latter is obvious from the rules of Fig. 2. Ourtyping rule for CSP makes type-preservation of demotion trivial, instark contrast to Taha and Nielsen’s (2003).
Proposition 3.4 (Determinism) If e

e1 and ee2 then e1 = e2 .

Proposition 3.5 (Progress) If ` e:t then either e is a value or there
exists e0 such that e e0 .
3.4

Comparison with λ αα is essentially Taha and Nielsen’s λ α (2003) with the
Our λ1v
restriction to one level, except:• Our language is call-by-value, to better match languages in

actual use such as MetaOCaml.
• We add fix, to model an effect, namely nontermination. We

make this addition to show that our translation preserves thestage at which effects happen, by showing that it preserves
whether a program terminates. As the first example in §2
demonstrates, it is important to evaluate an escape expression
and incur its effects when the enclosing bracket is built, not run.
• We give our dynamic semantics by small-step transition rules

using evaluation contexts, rather than big-step reduction rulesthat apply anywhere in the program. This choice is because wewant to add state and control effects eventually, which is easier
when transitions represent evaluation contexts explicitly and do
not impose the nesting of subexpressions on their evaluation.
• Our typing rule for CSP greatly simplifies the operational se-

mantics, at the cost of excluding some un-runnable terms (§3.1).
• Since our language is call-by-value, we do not evaluate a per-sisted level-0 expression. That is, %e is always a value; for example, %(1 + 1) is a value and does not reduce to %2. Thus, if Ω
is an infinite loop such as (fix f (x : int). f x)0, then h%Ωiα halts,
as does run (α)hλ xα :int. %Ωiα , but not run (α)h%Ωiα .
The last difference makes the calculus more orthogonal (a redex inside brackets is always in an escape) but no less expressive: to eval-

. . . , xα : int ` xα : int
α, f : hintiα → hintiα , xα : int ` f : hintiα → hintiα. . . , xα : int ` hxα iα : hintiα

α, f : hintiα → hintiα , xα : int ` f hxα iα : hintiα
α, f : hintiα → hintiα , xα : int ` ∼( f hxα iα ) : int
α, f : hintiα → hintiα ` λ xα :int. ∼( f hxα iα ) : int → int
α, f : hintiα → hintiα ` hλ xα :int. ∼( f hxα iα )iα : hint → intiα

eta : . . . , β , y : hintiβ ` y : hintiβα ` λ f :hintiα → hintiα . hλ xα :int. ∼( f hxα iα )iα : (hintiα → hintiα ) → hint → intiα

eta : . . . , β ` λ y:hintiβ . y : (hintiβ → hintiβ ).
`(α)λ f :hintiα →hintiα .hλ xα :int.∼( f hxα iα )iα :(α)((hintiα →hintiα )→hint→intiα ) eta:...`(β )λ y:hintiβ .y:(β )(hintiβ →hintiβ ) ..
` let eta = (α)λ f :hintiα → hintiα . hλ xα :int. ∼( f hxα iα )iα in let id = (β )λ y:hintiβ . y in (α)(eta[α](id[α])) : (α)hint → intiααFigure 3. An example typing derivation in λ1v

C0 [i1 + i2 ]C0 [(λ x :t. e)v]
C0 [(fix f (x : t1 ) : t2 . e)v]
C0 [((α)e)[β ]]αα αC [∼hv i ]C0 [run (α)hvα iα ]iα ↓ = i0
A

x ↓=x

A

(%e0 )α ↓ = e0C0 [i1 +̇i2 ]C0 [e [x := v]]
C0 [e [ f := fix f (x : t1 ) : t2 . e] [x := v]]
C0 [e [α := β ]]Cα [vα ]C0 [(α)(vα ↓)](eα1 + eα2 )↓ = eα1 ↓ + eα2 ↓(eα1 eα2 )↓ = eα1 ↓eα2 ↓(λ xα :u. eα )↓ = λ x0 :u. (eα ↓ xα := x0 )(fix f α (xα : u1 ) : u2 . eα )↓= fix f 0 (x0 : u1 ) : u2 . (eα ↓ f α := f 0 xα := x0 )Figure 4. Operational semantics: small-step transitions e e0 anddemotions vα ↓. The latter is an inductively defined map from values vα to expressions e0 .
VariablesType variables
Types
Environments

setting of a Hindley-Milner language such as MetaOCaml, we keep
the classifiers explicit here to guide our translation. We do not concern ourselves with polymorphism and inference in this paper. We
α as a desugared programming language,
consider our calculus λ1v
with all classifiers made explicit and with all polymorphism eliminated by monomorphization (inlining and type instantiation).

x, y, z, r, f , qπτ ::= π | int | τ1 → τ2 | ∀π. τ | (~τ)γ ::= [] | γ, π | γ, x : τNamed environments ρ ::= [] | ρ, π | ρ, xA : τ
Expressions
ε ::= i | x | λ x:τ. ε | fix f [~π ](x : τ1 ) : τ2 . ε| ε + ε | εε | Λπ. ε | ε[τ] | (~ε) | ε.i
Figure 5. Syntax of F2
uate the persisted term, we can write %e as ∼(let x = e in h%xi).
Conversely, if we had made CSP evaluate the persisted term, thento avoid that evaluation, we could write %e as (%(λ x :int. e))0.
Calcagno et al. (2004) designed a few successors to λ α , withHindley-Milner polymorphism, inference, principal types and typings. Modulo the treatment of polymorphism, those calculi are designed to simplify λ α so that terms do not mention classifiers. Neither variable bindings nor brackets are labeled in those calculi; theirlevels are all inferred. A classifier is treated like a type variable,
and an α-closed type is introduced and eliminated like a type polymorphic in α. Although this approach is attractive in the practical

4.

The target language F2

Our target language is System F, also known as F2 , with products(tuples) and the fixpoint. Figure 5 reviews the syntax we use. We
write ~a for a1 , . . . an , the sequence of zero or more objects ai . As
particular cases of tuples, a tuple with one object is that object itself
and the tuple with 0 objects is unit. We also sometimes use patternmatching as syntactic sugar for selecting parts of a tuple; for example, λ (x,y):(int,bool). (y, x) is short for λ z:(int,bool). (z.2, z.1).
We omit our static and dynamic semantics for F2 , which arestandard and call-by-value. (It does not matter whether the dynamic
semantics evaluates under a type abstraction, because we only perform type abstraction immediately around a term abstraction andalways apply the result of a type application to a term argument.)
At the term level, this target language adds polymorphism (inα and removes stagcluding polymorphic recursion) and tuples to λ1v
ing and classifiers. A type environment γ is an ordered sequence oftype- and term-variable bindings.
The output of our translation uses tuples just to represent laterstage environments, for which we introduce some syntactic sugar.
Definition 4.1 (Environments as tuples) Let γ = ~x :~τ be an F2
environment that binds no type variable. We write the environment
abstraction term λ γ. ε to mean λ (~x):(~τ). ε, where γ binds into ε.
We also write γ for the tuple term ~x and the tuple type ~τ. Thus,
γ → τ 0 means the type (~τ) → τ 0 , and if ε has the type γ → τ 0 thenεγ means the application term ε(~x).
For example, if γ is r : π, f : π → int, then the abstraction λ γ. f r is
the term λ (r, f ):(π,π → int). f r, of type (π, π → int) → int. As a
special case, if γ is empty, then λ γ. ε is λ y:(). ε and εγ is ε().
Our translation uses classifiers in an auxiliary data structure,
named environments ρ. As defined in Fig. 5, a named environment
decorates every term-variable binding with a level. Of course, classifiers do not appear in the output of the translation.
Definition 4.2 (Restriction) Suppose ρ is a named environment
and A is a named level. The full restriction ρ k A of ρ to A is theF2 -environment consisting of the type variables in ρ and the term
variables in ρ that are decorated with A. The incremental restrictionρ|A of ρ to A is the F2 -environment consisting only of the term
variables in ρ that are decorated with A.
Definition 4.3 (Extension) An environment, named environment,or named level extends another if the latter is a prefix of the former.

5.

The formal translation

α to F by induction: first on types
We define our translation from λ1v
2and environments, then on typing derivations.

5.1

α -type t
Given a λ1v

Definition 5.1 (Extension by used classifiers)
and a named environment ρ, the result of extending ρ by theclassifiers used in t is the named environment(
ρ, π, rα : π if Used(t) = {α}ρ,~π (t) =(9)ρif Used(t) = {}where the type variable π and the term variable r are fresh in F2 .
We write ~π for a sequence of zero or one type variables; a longer
sequence is ruled out by the one-level restriction (Definition 3.2).
Definition 5.2 (Translating types) In a named environment ρ, a
α -type t translates to an F -type ρ ; t as follows.
λ1v2ρ ; int = int(10)0ρ ; (t1 → t2 ) = ∀~π . (ρ ; t1 ) → (ρ ; t2 )0

where ρ = ρ,~π (t1 ) (11)αρ ; (hui ) = (ρ|α) → u
ρ ; ((α)t) = ρ ; t(12)where α is fresh(13)

In particular, if t1 uses no classifier, then ρ ; (t1 → t2 ) = (ρ ; t1 ) →(ρ ; t2 ) homomorphically. For a flat type u, we have ρ ; u = u.
The ∀~π in (11) is reminiscent of Gödel’s translation from intuitionistic logic to S4 (1933). For example, in the empty named
α -typeenvironment, the λ1v(α)(hintiα → hbooliα ) → hint → booliα(14)translates to the F2 -type (cf. §2.5)∀π. (∀π 0 . ((π, π 0 ) → int) → ((π, π 0 ) → bool)) → (π → int → bool)(15)
because Used(hintiα → hbooliα ) = Used(hintiα ) = {α}.
Given the type translation in (11) and (13), the environmenttranslation below is not surprising, as in the deduction theorem.
α -environment Γ
Definition 5.3 (Translating environments) A λ1v
translates to a named environment bΓc as follows.

b[]c = []bΓ, αc = bΓc

α -type and α be a level.
Definition 5.5 (Conversion) Let t be a λ1v
Let ρ1 and ρ2 be two named environments with the same typevariable bindings, such that ρ1 |β = ρ2 |β for every level β usedby t except possibly α. Suppose ε and ε̄ are two F2 -terms such that

ρ1 k α ` ε : (ρ2 |α),Translating types and environments0

every classifier α used by t, then ρ1 ;t = ρ2 ;t. More generally, if we
can convert between ρ1 |α and ρ2 |α for every classifier α used by t,then we can convert between ρ1 ; t and ρ2 ; t. If t uses no classifier,then it is trivial to convert between ρ1 ; t and ρ2 ; t because they are
equal. If t uses a classifier, then the conversion is barely nontrivial.

bΓ, x : tc = bΓc, ~π (t), x : (bΓc,~π (t) ; t)bΓ, xα : uc = bΓc, xα : u

(16)
(17)

Thus bΓ2 c extends bΓ1 c whenever Γ2 extends Γ1 .
The rest of this section defines the coercions motivated withescapes in §2.4. The coercion function ρ1 ,→ ρ2 ; t is a certain injection in F2 from ρ1 ; t to ρ2 ; t. The precise definition of coercionsis less important than their availability, summarized below.
Proposition 5.4 (Coercions are total and compositional) Given
α -type t, as long as the named environment ρ extends ρ ,any λ1v
2
1
the coercion ρ1 ,→ ρ2 ; t is a total function from ρ1 ; t to ρ2 ; t. If ρ3
further extends ρ2 , then the coercion ρ1 ,→ ρ3 ;t is equivalent to thecomposition (ρ2 ,→ ρ3 ; t) ◦ (ρ1 ,→ ρ2 ; t).
Put differently, coercions constructively show that extension among
named environments induces injection among translated types.
First we show how isomorphism among named environments
induces isomorphism among translated types. If ρ1 |α = ρ2 |α forρ2 k α ` ε̄ : (ρ1 |α).

(18)

In words, ε has the tuple type (ρ2 |α) in the environment ρ1 k α,and ε̄ has the tuple type (ρ1 |α) in the environment ρ2 k α. Then we
define a pair of conversion functions in F2µt : (ρ1 ; t) → (ρ2 ; t),µ̄t : (ρ2 ; t) → (ρ1 ; t)(19)

simultaneously by the following induction on the structure of t. We
omit the definition of µ̄t by symmetry with µt.
µ int = λ x:int. x(20)µ(t1 → t2 ) = λ f . Λ~π . λ x. µt2 ( f [~π ](µ̄t1 (x)))
where the length of ~π is # Used(t1 )(21)µ(huiα ) = λ f . λ (ρ2 |α). f (ε̄)(22)µ((α)t) = µt(23)where α is fresh

We notate the conversion µ as Conv(ρ1 , ρ2 , α, ε, ε̄).
For example, if
ρ1 = π, xα : π, yα : int,

ρ2 = π, f : int → π, zα : (int , π) (24)and we let µ be Conv(ρ1 , ρ2 , α, (y, x), (z.2, z.1)), thenµ(hbooliα ) = λ f :(π,int) → bool. λ z:(int,π). f (z.2, z.1), (25)µ̄(hbooliα ) = λ f :(int,π) → bool. λ (x,y):(π,int). f (y, x). (26)Definition 5.6 (Coercion) Suppose ρ1 and ρ2 are named environα -type t, we define a coercion
ments and ρ2 extends ρ1 . For every λ1vfunction in F2 from ρ1 ;t to ρ2 ;t, that is, a term of type ρ1 ;t → ρ2 ;tin the environment ρ2 k A. We notate this coercion as ρ1 ,→ ρ2 ; t.
By induction on the difference between ρ1 and ρ2 , we consider
two cases then compose the coercions. First, if ρ2 is ρ1 or ρ1 , π or
ρ1 , y : τ, then the coercion is the identity. Second, if ρ2 = ρ1 , yβ : τ,then we define the coercion by the following induction on t.
ρ1 ,→ ρ2 ; int = λ x:int. x
ρ1 ,→ ρ2 ; (t1 → t2 ) = see below
ρ1 ,→ ρ2 ; (huiα ) = λ f . λ (ρ2 |α). f (ρ1 |α)ρ1 ,→ ρ2 ; ((α)t) = ρ1 ,→ ρ2 ; t where α is fresh

(27)
(28)
(29)
(30)

In (28), we define the coercion ρ1 ,→ ρ2 ; (t1 → t2 ) by considering
two cases. On one hand, if β is not used in t1 and so (ρ1 ,~π (t1 ));t1 =(ρ2 ,~π (t1 )) ; t1 , then the coercion is
λ f . Λ~π . λ x. (ρ1 ,~π (t1 ) ,→ ρ1 ,~π (t1 ), yβ : τ ; t2 )( f [~π ](x)).

(31)

On the other hand, if Used(t1 ) = {β }, then let
ρ10 = ρ1 ,~π (t1 ) = ρ1 , π, rβ : π,(32)

ρ20 = ρ2 ,~π (t1 ) = ρ1 , yβ : τ, π, rβ : π,(33)

following Definition 5.1. Then by Definition 5.2,
ρ1 ; (t1 → t2 ) = ∀π. (ρ10 ; t1 → ρ10 ; t2 ),(34)

ρ2 ; (t1 → t2 ) = ∀π. (ρ20 ; t1 → ρ20 ; t2 ).

(35)

Define the named environment ρ100 = ρ1 , π, r0 β : (τ, π) and let µ be
the conversion Conv(ρ100 , ρ20 , β , (ρ1 |β , r0 .1, r0 .2), (ρ1 |β , (y, r))). Wethen define the coercion from the type (34) to the type (35) to be
λ f . Λπ. λ x. µt2 ( f [(τ, π)](µ̄t1 (x))).

(36)

Examples A simple example of a coercion is bαc ,→ bα, xα :intc;
hbooliα , where bαc is [] and bα, xα : intc is xα : int by Definition 5.3. The coercion is an F2 -function from the type [] ; hbooliα =() → bool to the type xα : int ; hbooliα = int → bool, namely
λ f . λ x. f () by (29) and (the bool analogue of) (27).
A more involved example of a coercion is(bαc, π, rα : π) ,→ bα, f : hintiα → hbooliα , xα : intc;(hintiα → hbooliα ).

(37)This coercion occurs in the translation of the eta function in §2.5.
Here bαc is [] and bα, f : hintiα → hbooliα , xα : intc isΓ1 ` (fix f (x). e) : t to bΓ1 c k 0 ` fix f (x). ε : (bΓ1 c ; t). Second, ifUsed(t) = Used(t1 ) = {α} ⊇ Used(t2 ), then ρ = bΓ1 c, π, rα :π, π 0 ,r0 α : π 0 . Define the named environment ρ1 = bΓ1 c, π, rα : π and letµ be the conversion Conv(ρ1 , (ρ1 , r0 α : ()), α, (ρ1 |α, ()), (ρ1 |α)).
Then translate Γ1 ` (fix f (x). e) : t tobΓ1 c k 0 ` (fix f [π](x0 : ρ1 ; t1 ) : (ρ1 ; t2 ).
µ̄t2 @ (ε [π 0 := ()] [x := µt1 @ x0 ])) : (bΓ1 c ; t).

(40)

Third, if Used(t) = Used(t2 ) = {α} but Used(t1 ) = {}, then ρ =bΓ1 c, π, rα :π. Define the named environment ρ 0 = bΓ1 c, rα :() andlet µ be the conversion Conv(bΓ1 c, ρ 0 , α, (bΓ1 c|α, ()), (bΓ1 c|α)).
Then translate Γ1 ` (fix f (x). e) : t tobΓ1 c k 0 ` (fix f 0 (x0 : bΓ1 c ; t1 ) : (bΓ1 c ; t2 ).

π, rα :π, f :∀π 0 . ((π, π 0 ) → int) → ((π, π 0 ) → bool), xα :int (38)µ̄t2 @ (ε [π := ()] [ f := µt @ f 0 ] [x := µt1 @ x0 ])) : (bΓ1 c ; t). (41)by Definition 5.3. The coercion (37) is a function in F2 from
∀π 0 . ((π, π 0 ) → int) → ((π, π 0 ) → bool) to ∀π 0 . ((π, int , π 0 ) →int) → ((π, int , π 0 ) → bool). It is equivalent to the F2 -term

Addition: If eA1 : int translates to ε1 : int and eA2 : int translates
to ε2 : int (both with some auxiliary judgments if A is not empty),
then translate eA1 + eA2 : int to ε1 + ε2 : int (concatenating the twosequences of auxiliary judgments if A is not empty).
Application: Suppose that Γ ` eA1 : t1 → t2 translates to bΓc k A,
~q1 :~τ1 ` ε1 : τ1 and Γ ` eA2 : t1 translates to bΓc k A, ~q2 :~τ2 ` ε2 : τ2 ,both with some auxiliary judgments if A is not empty. If A is not
empty, then just translate e1 e2 to ε1 ε2 , concatenating the two sequences of auxiliary judgments. If A is empty, then Used(t1 ) iseither {} or {α} by the one-level restriction (Definition 3.2). If
Used(t1 ) is empty, then just translate e1 e2 to ε1 ε2 . If Used(t1 )is {α}, then define the named environment ρ = bΓc, rα : () and letµ be the conversion Conv(bΓc, ρ, α, (bΓc|α, ()), (bΓc|α)). Translate e1 e2 to let ( f , x) = (ε1 , ε2 ) in (µ̄(t1 → t2 ) @ ( f [()]))x.
Classifier introduction: If e translates to ε, then (α)e also translates to ε, where α is fresh.
Classifier instantiation: Suppose that Γ ` e : (α)t translates tobΓc k 0 ` ε : (bΓc ; t), where α is fresh, and β is a classifier in Γ.
Let x1 β : τ1 , . . . , xm β : τm be all the term-variable bindings in bΓcthat are decorated with β . Define the named environment ρ = bΓc,x1 α :τ1 , . . . , xm α :τm . Then ρ|α = bΓc|β , so ρ ;t = bΓc;(t [α := β ]).
Translate e[β ] to (bΓc ,→ ρ ; t) @ ε.
Run: If Γ ` e : (α)huiα (where α is fresh) translates to bΓc k 0 `ε : () → u, then translate Γ ` run e : (α)u to bΓc k 0 ` ε() : u.
Bracket: If Γ ` eα : u translates to bΓc k α, q1 : τ1 , . . . , qn : τn `ε : u with n auxiliary judgments bΓc k 0 ` εi : τi , then translate thequotation Γ ` heα iα : huiα to

λ f . Λπ 0 . λ f1 . let f2 = f [(int , π 0 )](λ (x,(y,z)). f1 (x, y, z)) in
λ (x,y,z). f2 (x, (y, z)).
5.2

Translating terms and derivations

Our translation of terms and derivations is guided by our translation of types and environments, so this section should be read
αin conjunction with the previous one. We want to translate a λ1v
0judgment Γ ` e : t to an F2 -judgment bΓc k 0 ` ε : (bΓc ; t). However, to handle code with escaping and cross-stage persistence inα -judgment Γ ` eα : u to a judgment
ductively, we also translate a λ1v
bΓc k α, q1 : τ1 , . . . , qn : τn ` ε : u along with an ordered sequence ofn auxiliary judgments bΓc k 0 ` εi : τi . As detailed in the following
definition and illustrated in the following example, the translationof brackets combines—that is, flattens—these judgments into let.
Definition 5.7 (Translating terms, judgments, and derivations)
The translation of the source derivation is defined inductively overthe source derivation, or, equivalently, on the source term eA . We
mark some applications ε1 ε2 as administrative by writing them as
ε1 @ ε2 . All elimination forms in conversions and coercions are also
administrative. See also the translation of bracket.
Literal constant: Translate the judgment Γ ` iA : int to the judgment bΓc k A ` i : int, with no auxiliary judgment if A is not empty.
Variable: Translate Γ ` xα : u to bΓc k α ` x : u, with no auxiliary
judgment. Translate the judgment Γ ` x0 :t, where Γ = Γ1 , x0 :t, Γ2 ,to the judgment bΓc k 0 ` (bΓ1 c, ~π (t) ,→ bΓc ; t) @ x : (bΓc ; t).
Abstraction: Let Γ be Γ1 , xA : t1 and t be t1 → t2 . Suppose thejudgment Γ ` eA : t2 translates to bΓc k A, ~q :~τ ` ε : τ, with some
auxiliary judgments if A is not empty. If A is not empty, then τ = t2
and bΓ1 c k 0 = bΓc k 0, so just translate Γ1 ` (λ xA :t1 . eA ) : t tobΓ1 c k A, ~q :~τ ` (λ x:t1 . ε) : t, with the same auxiliary judgments. If
A is empty, then τ = bΓ1 c,~π (t1 ) ; t2 , so translate Γ1 ` (λ x :t1 . e) : t
to bΓ1 c k 0 ` (Λ~π (t1 ). λ x :(bΓ1 c,~π (t1 );t1 ). ε) : (bΓ1 c ; t).
Fixpoint: Let Γ be Γ1 , f A : t, xA : t1 where t is t1 → t2 . SupposeΓ ` eA : t2 translates to bΓc k A, ~q :~τ ` ε : τ, with some auxiliary
judgments if A is not empty. If A is not empty, then τ = t2 andbΓ1 c k 0 = bΓc k 0, so just translate Γ1 ` (fix f A (xA : t1 ) : t2 . eA ) : t
to bΓ1 c k A, ~q :~τ ` (fix f (x : t1 ) : t2 . ε) : t, with the same auxiliary
judgments. If A is empty, then Γ1 , f : t, x : t1 ` e : t2 translates tobΓ1 c k 0, ~π , f : (bΓ1 c,~π (t) ; t), ~π 0 , x : (ρ ; t1 ) ` ε : (ρ ; t2 ),bΓck0 ` let q1 = ε1 in . . . let qn = εn in λ (bΓc|α). ε :(bΓc|α) → u.
(42)Mark as administrative: (a) let qi = εi for auxiliary judgments fromtranslating CSP; (b) environment tuple projections (bΓc|α).i.
Escape: If Γ ` e : huiα translates to bΓc k 0 ` ε : bΓc|α → u, thenmake the latter judgment the sole auxiliary judgment in translatingΓ ` ∼e : u to bΓc k α, q : (bΓc|α → u) ` q @ (bΓc|α) : u.
Cross-stage persistence: If Γ ` e : u translates to bΓc k 0 ` ε : u,then make bΓ, α, Γ0 ck0 ` λ (). ε :() → u the sole auxiliary judgment
in translating Γ, α, Γ0 ` %e : u to bΓ, α, Γ0 c k α, q : () → u ` q @ () : u.
Examples We return to the ef 2 example in §2.3 and §2.4. The
source term is the application of the function
λ ef 0 :(β )(hintiβ → hint → intiβ ).

(39)

where ρ = bΓ1 c,~π (t),~π 0 (t1 ). The one-level restriction (Definition 3.2) leaves three possibilities for Used(t1 ) and Used(t2 ).
First, if Used(t) = Used(t1 ) = Used(t2 ) = {}, then just translate(α)hλ xα . λ yα . ∼(ef [α]hxα × yα iα )iα(43)

to the argument(α)λ z:hintiα . hλ xα :int. ∼z + xα iα .

(44)

Because the type of the argument (44) uses no level, this application translates to the application of the translations of (43) and (44)in the empty environment. We can thus translate (43) and (44) separately (thanks to compositionality in the large, Proposition 5.14).
We translate the derivation

Translating ef

α, z0 : hintiα , xα : int ` z0 : hintiα
α, z0 : hintiα , xα : int ` ∼z : int

12α, z0 : hintiα , xα : int ` ∼z + xα : int
0

α

α

α

α, z : hinti ` λ x :int. ∼z + x : int → int

4

α

α

α α

((int , int) → int) → ((int , int) → int → int).
We then apply this function to (47).

α

α

5.3

7

`(α)λ z0 :hintiα .hλ xα :int.∼z+xα iα :(α)(hintiα →hint→intiα )8α -environment α, z0 : hintiα , xα : int
from top to bottom. The top λ1vtranslates to the named environment π, rα : π, z0 : π → int, xα : int.

1. π, z : π → int ` (λ f . λ (r,x) :(π,int). f r) @ z : (π, int) → int
2. π, r : π, x : int, q : (π, int) → int ` q @ (r, x) : int
with the auxiliary judgment
π, z : π → int ` (λ f . λ (r,x) :(π,int). f r) @ z : (π, int) → int
4. π, r : π, x : int, q : (π, int) → int ` q @ (r, x) + x : int
with the same auxiliary judgment as in 3
5. π, r : π, q : (π, int) → int ` λ x :int. q @ (r, x) + x : int → int
with the same auxiliary judgment as in 3
6. π, z : π → int ` let q = (λ f . λ (r,x) :(π,int). f r) @ z in
λ r. λ x :int. q @ (r, x) + x : π → int → int
7. ` Λπ. λ z :π → int. let q = (λ f . λ (r,x) :(π,int). f r) @ z in
λ r. λ x :int. q @ (r, x) + x : ∀π. (π → int) → (π → int → int)
8. Same as 7
The result is the same as at the end of §2.4, modulo a β -value redex.
Translating ef 2 proper In the typing derivation of (43), we focus
on the application
·
·
·2
·1
·
·
α
α
α
Γ ` ef [α] : hinti → hint → intiΓ ` hx × yα iα : hintiα3Γ ` ef [α]hxα × yα iα : hint → intiα .
α -environment Γ is defined byHere the λ1v

Γ = ef 0 : (β )(hintiβ → hint → intiβ ), α, xα : int, yα : int(45)

and translates to the named environmentbΓc = ef 0 : ∀π. (π → int) → (π → int → int), xα : int, yα : int.
(46)
The bracket 1 above translates easily to the judgment
ef : ∀π. (π → int) → (π → int → int)
` λ (x,y). x × y : (int , int) → int .

(47)

To translate the classifier instantiation 2, we apply the coercion
ββbΓc ,→ (bΓc, x : int, y : int) ; hinti → hint → inti

α , and it
Proposition 5.8 (Type preservation) If Γ ` e0 : t in λ1v
translates to bΓc k 0 ` ε : (bΓc ; t), then bΓc k 0 ` ε : (bΓc ; t) in F2 .

ProofDefinition 5.7 amounts to a constructive proof.

Because the type system of F2 is sound, type preservation ensuresthat our translation does not go wrong. In particular, the translated
term never looks up free variables, thus preventing scope extrusion.
We turn to the dynamic properties of our term translation.

This normal form ANF(ε) is observationally equivalent to ε since
all β -value reductions preserve observational equivalence in F2 .
Our translation preserves values in the following sense. We
conjecture that it also preserves reductions and hence observations.
Proposition 5.10 (Value preservation) If Γ ` v0 : t and v translates to ε, then ANF(ε) is a value.
Conjecture 5.11 (Reduction preservation) Suppose Γ ` e01 :t ande1e2 . If e1 and e2 translate to ε1 and ε2 , then there exists ε sothat ANF(ε) = ANF(ε2 ) and ANF(ε1 ) + ε in call-by-value F2 .
Corollary 5.12 (Observation preservation) If [] ` e0 :t translates
to [] ` ε : ([] ; t), then e terminates if and only if ε terminates.
The two conjectures above entail that our translation preserves
evaluation order. Because F2 without fix is strongly normalizing,
α without fix is strongly normalizing.
they also entail that λ1v
αAlthough our translation is defined to operate on an entire λ1v
program at once, it is in fact compositional enough for parts of an
expression or a modular program to be translated separately.
Proposition 5.13 (Compositionality in the small) Let e be a wellα -term with n subterms e , . . . , e , and e0 be the well-typed
typed λ1vn1result of replacing e1 , . . . , en by e01 , . . . , e0n . If the subterms e1 , . . . , enα , translate to the sameand e01 , . . . , e0n , in their environments in λ1v(or equivalent) F2 -judgments, then e and e0 , in their environments
α , also translate to the same (or equivalent) F -judgments.
in λ1v
2(48)

Proposition 5.14 (Compositionality in the large) Let Γ1 and Γ2
α -environments that differ only in their variable bindings
be two λ1v
at level 0 whose types use no classifier. If Γ1 ` e0 : t and Γ2 ` e0 : t,then the translation of e0 is the same in Γ1 as in Γ2 .

(49)

Proof

to ef , to turn it from the type
∀π. (π → int) → (π → int → int)

Properties

Definition 5.9 An administrative reduction is a β -value reduction
in F2 (anywhere in a term, even under λ ) of an elimination form
marked as administrative in Definition 5.7.
Administrative reduction is terminating (since each step reduces
the number of administrative redexes) and confluent (since there isno critical pair), so it brings every term ε to a normal form ANF(ε).

3. π, r : π, x : int ` x : int

β

(52)

6

α ` λ z :hinti . hλ x :int. ∼z + x i : hinti → hint → inti

β

(50)

The result of the coercion is essentially Λπ. λ r. ef [(int , int , π)]r.
Finally, to translate the application 3, we instantiate this type variable π to () and apply the conversion

5α, z0 : hintiα ` hλ xα :int. ∼z + xα iα : hint → intiα0∀π. ((int , int , π) → int) → ((int , int , π) → int → int).

Conv(bΓc, (bΓc, rα : ()), α, (x, y, ()), (x, y))(hintiα → hint → intiα )(51)
to get a function of type3

. . . , xα : int ` xα : int

to the type

Observe that bΓ1 c k α = bΓ2 c k α for all α.

Proposition 5.13 means that the translation of a term can proceedwith translating its parts in parallel. Proposition 5.14 means that
top-level definitions that do not share a classifier can be translated
separately. For example, the program in Fig. 3 defines the code
generators eta and id at the top level. These definitions and the
body that uses them can be translated separately from each other.

6.

Scope extrusion

We turn in this section from our formal translation to how it helps
us combine staging with effects soundly in our ongoing work.
To continue the power example from §2, suppose that we wantto count the multiplication operations as we generate them. For example, power7 should produce the count 5 along with the function
α and in MetaOCaml withλ x. x × square (x × square (x × 1)). In λ1v
out effects, this count is hard to pass out of the scope of the laterstage variable x, because the binder λ x must apply to later-stage
code, not an earlier-stage count.
α , then the counting
If we add ML-style mutable references to λ1v
becomes easy: we change the definition of power as follows.
let count = ref 0
let power = (α) fix f (n : int) : hintiα → hintiα . λ x :hintiα .
if n = 0 then h1iα else count ← !count + 1;
if n mod 2 = 0 . . .
After evaluating power7, the number of multiplications generated
can be retrieved by !count.
Unfortunately, adding state so naı̈vely to a staged language
results in scope extrusion. For example, the following program
generates a piece of open code then runs it.
run (α)(let x = ref h1iα in hλ y. ∼(x ← hyiα ; h()iα )iα ; !x)(53)

The let expression above evaluates to hyiα with no binder for yin sight, so the program gets stuck at (α)y. In MetaOCaml, thisexample causes a type-checking error at run time.
Adding state breaks soundness because the environment wherea code value is created may no longer be a prefix of the environment
where it is used. In terms of our translation, we would need tocoerce the type ρ1 ; t to the type ρ2 ; t when ρ2 does not extend ρ1 .
Such a coercion does not exist in general. If we translate (53)informally without such a reverse coercion, we get(let x = ref(λ (). 1) in let v = x ← (λ (y). y); λ (y). () in(λ (). λ y. v(y)); !x)(),which does not type-check in F2 , even without any value restriction.
These examples suggest that, to prevent scope extrusion instaged programs with effects, we can try to translate the staging
away and see if we can come up with the coercions needed to keep
the translation well-typed (that is, to maintain Proposition 5.8). For
example, the effectful use of count in the power example above
is sound, because mutation at the flat type int uses no classifiers
and so needs no coercion (as discussed above Definition 5.5). Of
course, other uses of effects in staging, such as for let insertion,
may require more coercions or different tests for scope extrusion.
In MetaOCaml without effects, we have implemented anothersolution to the counting problem in a sound staged language: Take
the changed definition of power above. Apply our translation, thena state-passing transformation to eliminate the use of references.
Finally, add staging annotations to the program so that it produces
not a function of type int → int but a cogen of type hinti → hinti.

7.

Related work

Our work is inspired by the expressive staged calculus λ α and its
sound type system (Taha and Nielsen 2003). We aim to make thecalculus model MetaOCaml more closely, by moving towards callα
by-value and accounting for effects. We compare our language λ1vαwith λ and its later development (Calcagno et al. 2004) in §3.4.
Taha (1999) poses the challenge of encoding staging using λ abstraction in §7.2.1, ‘Why lambda-abstraction is not enough formulti-stage programming’. Besides the pragmatic need to print
generated code, his main reason is that escapes are hard to encode because they permit ‘evaluation under lambda’. He suggests
one encoding scheme, using reference cells and exceptions, whichmake it hard to check that the target calculus is sound. This paperanswers this challenge by showing how System F with constants
suffices for two-stage programming. We discuss the challenges ofthe encoding and our solution in §2.2–§2.4.
The safety problem of staged languages with effects has a long
history. Calcagno et al. (2000) show that reference cells may safely
store values of closed types (in our terminology, types that use
no levels). Our discussion in §6 not only confirms this result, ina calculus with a small-step rather than big-step semantics, but
further suggests ways to safely store open code as well. Calcagno
et al. relate safe staging with effects to binding-time analyses forimperative languages. Indeed, our use of coercions is a sort ofbinding-time analysis that relies on the type environment in a term’s
derivation to describe the binding environment of the term.
Nanevski et al.’s contextual modality (2007) includes the namesof free variables in the types of open code. Discussing such inclusion, Taha and Nielsen (2003; §1.4) warn of the difficulty in maintaining α-equivalence and of the need for ρ-polymorphism andnegative side conditions. We avoid these nominal problems using
tuple indices based on the ordering of bindings in the type environment. In contrast, Kim et al.’s staging extension to ML (2006) includes variable-capturing substitution but sacrifices α-equivalence.
Taha (2000) recounts how hard it is to develop a reduction semantics and equational theory for even an untyped staged language.
He presents a confluent big-step call-by-name semantics that preserves observational equivalence for a staged language λ -U. Although that semantics has become popular (for instance used by
Taha and Nielsen (2003)), we give a small-step call-by-value semantics. This choice makes formalization challenging, as our redexes may be open and our evaluation contexts may be binding, but
it resolves the thorny problems described by Taha. For example, theterm (λ x. h%xi)(λ y. (λ z. z)5) threatens confluence under call-byname (Taha 2000; §3.4), but our reductions are deterministic andhence trivially confluent. This term satisfies our one-level restriction and translates to (λ x. let q = λ (). x in λ (). q())(λ y. (λ z. z)5),
with no substitution conflicts or level adjustments. We encode CSP
simply by enclosing an earlier-stage computation in a thunk.
Yuse and Igarashi (2006) design a staged calculus that canmanipulate open code, run closed code, and persist values acrossstages. Their paper is rare in that it gives a call-by-value smallstep semantics of a typed staged language. However, despite theclear correspondence between their calculus and linear-time temporal logic, the commuting conversions via which their ‘open’ and‘closed’ modalities interact seem to distance their calculus fromthe practice of languages like MetaOCaml and thus our work withclassifiers. Towards implementing their language, the authors suggest that ‘designing a suitable abstract machine with environments
would be a first step.’ Our translation may be viewed as such a step.

8.

Conclusions

Our derivation-directed translation from a staged language to an unstaged language represents future-stage code using λ -abstractions,
yet preserves the evaluation order, typing, and α-equivalence (hygiene) of the staged program. This translation exposes the problemof scope extrusion as a lack of type coercion. This work prepares usto develop safe staged languages that permit combining open codefragments using state and control effects, and executing the result.
Overcoming the challenge of decoupling evaluation from scope,
we have shown that call-by-value System F can encode staging,under a restriction to one future level that includes much publishedstaged code. Lifting this restriction is the subject of the current
work and may require a target language with kind polymorphism.
We have shown small-step call-by-value semantics to be a viable model of expressive staged languages such as MetaOCaml.
In exchange for dealing with open redexes and binding evaluation
contexts, we gain deterministic reductions and a better frameworkin which to account for effects, especially control.
Our translation produces much administrative overhead as itbuilds and uses coercion functions and environment tuples. We caneither postprocess the overhead away or avoid it in the first place using a genuine staging language (like a one-pass CPS transformer).
We rely on the order of bindings in type environments to index
free variables and construct coercions. For example, weakening is
explicit in our translation. This reliance is reminiscent of substructural logics. Following Yuse and Igarashi (2006), it would be interesting to explicate the Curry-Howard correspondence in this regard.

Acknowledgments
We thank Olivier Danvy for the counting example in §6, Walid
Taha for helpful conversations and explanations of his work, andthe anonymous reviewers for helpful suggestions.

References
Ariola, Zena M., and Matthias Felleisen. 1997. The call-by-needlambda calculus. Journal of Functional Programming 7(3):265–
301.
Asai, Kenichi. 2002. Online partial evaluation for shift and reset.
In PEPM, 19–30.
Balat, Vincent, Roberto Di Cosmo, and Marcelo P. Fiore. 2004.
Extensional normalisation and type-directed partial evaluation
for typed lambda calculus with sums. In POPL, 64–76.
Calcagno, Cristiano, Eugenio Moggi, and Walid Taha. 2000.
Closed types as a simple approach to safe imperative multi-stage
programming. In ICALP, 25–36. LNCS 1853.
———. 2004. ML-like inference for classifiers. In ESOP, 79–93.
LNCS 2986.
Carette, Jacques, and Oleg Kiselyov. 2005. Multi-stage programming with functors and monads: Eliminating abstraction overhead from generic code. In GPCE, 256–274. LNCS 3676.
Czarnecki, Krzysztof, John T. O’Donnell, Jörg Striegnitz, andWalid Taha. 2004. DSL implementation in MetaOCaml, Template Haskell, and C++. In DSPG 2003, 51–72. LNCS 3016.
Davies, Rowan, and Frank Pfenning. 2001. A modal analysis ofstaged computation. Journal of the ACM 48(3):555–604.
Elliott, Conal. 2004. Programming graphics processors functionally. In Haskell workshop, 45–56.
Ghani, Neil, Valeria de Paiva, and Eike Ritter. 1998. Explicit
substitutions for constructive necessity. In ICALP, 743–754.
LNCS 1443.
Glück, Robert, and Jesper Jørgensen. 1997. An automatic program
generator for multi-level specialization. Lisp and Symbolic Computation 10(2):113–158.
Gödel, Kurt. 1933. Eine Interpretation des intuitionistischen Aussagenkalküls. Ergebnisse eines Mathematischen Kolloquiums 4:
39–40.
Hammond, Kevin, and Greg Michaelson. 2003. Hume: A domainspecific language for real-time embedded systems. In GPCE,
37–56. LNCS 2830.

Jones, Neil D. 1988. Challenging problems in partial evaluationand mixed computation. New Generation Computing 6(2–3):
291–302.
Kim, Ik-Soon, Kwangkeun Yi, and Cristiano Calcagno. 2006. A
polymorphic modal type system for Lisp-like multi-staged languages. In POPL, 257–268.
Launchbury, John, and Simon L. Peyton Jones. 1995. State in
Haskell. Lisp and Symbolic Computation 8(4):293–341.
Lawall, Julia L., and Olivier Danvy. 1994. Continuation-based
partial evaluation. In Lisp & functional programming, 227–238.
Lengauer, Christian, and Walid Taha, eds. 2006. Special issue on
the 1st MetaOCaml workshop (2004), vol. 62(1) of Science ofComputer Programming. Elsevier.
Maraist, John, Martin Odersky, and Philip Wadler. 1998. The callby-need lambda calculus. Journal of Functional Programming
8(3):275–317.
Miller, Dale A., and Alwen Tiu. 2003. A proof theory for genericjudgments: An extended abstract. In LICS, 118–127.
Minamide, Yasuhiko, J. Gregory Morrisett, and Robert Harper.
1996. Typed closure conversion. In POPL, 271–283.
Nanevski, Aleksandar, Frank Pfenning, and Brigitte Pientka. 2007.
Contextual modal type theory. Transactions on Computational
Logic. In press.
Nielson, Flemming, and Hanne Riis Nielson. 1996. Multi-level
lambda-calculi. In Partial evaluation, 338–354. LNCS 1110.
O’Hearn, Peter W., and Robert D. Tennent. 1995. Parametricity
and local variables. Journal of the ACM 42(3):658–709.
Pašalić, Emir, Walid Taha, and Tim Sheard. 2002. Tagless staged
interpreters for typed languages. In ICFP, 157–166.
Püschel, Markus, José M. F. Moura, Jeremy Johnson, David
Padua, Manuela Veloso, Bryan W. Singer, Jianxin Xiong,Franz Franchetti, Aca Gačić, Yevgen Voronenko, Kang Chen,
Robert W. Johnson, and Nick Rizzolo. 2005. SPIRAL: Codegeneration for DSP transforms. Proceedings of the IEEE special issue on program generation, optimization, and adaptation
93(2):232–275.
Sumii, Eijiro, and Naoki Kobayashi. 2001. A hybrid approach toonline and offline partial evaluation. Higher-Order and Symbolic
Computation 14(2–3):101–142.
Swadi, Kedar, Walid Taha, Oleg Kiselyov, and Emir Pasalic. 2006.
A monadic approach for avoiding code duplication when staging
memoized functions. In PEPM, 160–169.
Taha, Walid. 1999. Multi-stage programming: Its theory and applications. Ph.D. thesis, Oregon Graduate Institute of Science andTechnology.
———. 2000. A sound reduction semantics for untyped CBN
multi-stage computation. In PEPM.
———. 2004. A gentle introduction to multi-stage programming.
In DSPG 2003, 30–50. LNCS 3016.
———. 2005. Resource-aware programming. In ICESS, 38–43.
LNCS 3605.
Taha, Walid, and Michael Florentin Nielsen. 2003. Environment
classifiers. In POPL, 26–37.
Wright, Andrew K., and Matthias Felleisen. 1994. A syntactic
approach to type soundness. Information and Computation
115(1):38–94.
Yuse, Yosihiro, and Atsushi Igarashi. 2006. A modal type system
for multi-level generating extensions with persistent code. In
PPDP, 201–212.