JFP 21 (6): 617–662, 2011.

c Cambridge University Press 2011
617

doi:10.1017/S0956796811000256

Shifting the stage
Staging with delimited control
YUKIYOSHI KAMEYAMA
Department of Computer Science, University of Tsukuba(e-mail:)kameyama@acm.org)

OLEG KISELYOV
Monterey, CA, USA(e-mail:)oleg@okmij.org)

C H U N G-C H I E H S H A N
Cornell University(e-mail:)ccshan@post.harvard.edu)

Abstract
It is often hard to write programs that are eﬃcient yet reusable. For example, an eﬃcient
implementation of Gaussian elimination should be specialized to the structure and known
static properties of the input matrix. The most proﬁtable optimizations, such as choosing thebest pivoting or memoization, cannot be expected of even an advanced compiler because they
are speciﬁc to the domain, but expressing these optimizations directly makes for ungainly
source code. Instead, a promising and popular way to reconcile eﬃciency with reusability isfor a domain expert to write code generators.
Two pillars of this approach are types and eﬀects. Typed multilevel languages such as
MetaOCaml ensure safety and early error reporting: a well-typed code generator neither
goes wrong nor generates code that goes wrong. Side eﬀects such as state and control easecorrectness and expressivity: An eﬀectful generator can resemble the textbook presentationof an algorithm, as is familiar to domain experts, yet insert let for memoization and if forbounds checking, as is necessary for eﬃciency. Together, types and eﬀects enable structuringcode generators as compositions of modules with well-deﬁned interfaces, and hence scaling
to large programs. However, blindly adding eﬀects renders multilevel types unsound.
We introduce the ﬁrst multilevel calculus with control eﬀects and a sound type system.
We give small-step operational semantics as well as a one-pass continuation-passing-styletranslation. For soundness, our calculus restricts the code generator’s eﬀects to the scope ofgenerated binders. Even with this restriction, we can ﬁnally write eﬃcient code generators for
dynamic programming and numerical methods in direct style, like in algorithm textbooks,
rather than in continuation-passing or monadic style.

1 Introduction
High-performance computing and high-assurance embedded computing often callfor programs that are specialized for particular inputs, usages, or processors.
Examples include specializing matrix multiplication to the target computer system(Whaley & Petitet, 2005; Cohen et al., 2006), specializing Fast Fourier Transform to618

Y. Kameyama et al.

the length of the transformed sequence (Frigo & Johnson, 2005; Püschel et al., 2005),
and specializing signal processing algorithms to the architecture of a particular Field
Programmable Gate Array (Püschel et al., 2005). As another example, Carette (2006)
found 35 variously specialized implementations of the same Gaussian elimination
algorithm in the industrial computer algebra system Maple.
Specializations like these go well beyond inlining and constant propagation, demanding domain-speciﬁc knowledge (such as symmetry groups of the roots of unity,in the case of Fast Fourier Transform). A good illustration is the powerful specialization of 0 * x as 0, which predicts the result of multiplication even for unknown xand leads to further simpliﬁcations. For ﬂoating-point numbers, this specialization
is invalid – unless one knows that in no program run can x be NaN or Infinity.
General-purpose compilers cannot be counted on for optimizations so complex
and particular; in fact, optimizing compilers are lagging further behind experts in
producing the highest performance code (Cohen et al., 2006). That is why writing
specialized programs by hand – however labor-intensive and error-prone – is commonplace: All the versions of Gaussian eliminations in Maple were written by hand.
The leading approach to automating these specializations is code generation, also
called generative programming (Cohen et al., 2006). In this approach, domain experts
versed in the desired optimizations express their knowledge by building a custom
code generator or specializer. The generated or specialized code is then compiled
by a general-purpose compiler. This division of labor avoids the dilemma thateither a compiler writer has to acquire application-speciﬁc knowledge or a domain
expert has to learn the intimate internals of a compiler (such as closure conversion,
frame structure, instruction scheduling, and register allocation). The division of labor
may go further: Ideally, one expert on computational geometry, another on linear
algebra, and a third on loop transformations can work on separate modules of thesame custom code generator, pooling their expertise to produce high-performance
programs with a variety of optimizations.
Custom code generators today are built on top of a variety of substrates, including
general-purpose programming languages (Kamin, 1996) as well as preprocessors(such as m4) and macro processors (Lisp macros, camlp4), template systems (C++templates), partial evaluators and supercompilers, and multilevel languages. To
support the division of labor just described and enable modular reasoning about
the specialization process, a language for custom code generators needs to be highlevel: It ought to let domain experts express algorithms clearly, specify abstract
interfaces between modules, and establish basic prerequisites to correctness, suchas type safety. Most languages fall short in this regard. For example, the popular
strategy of generating code using printf is described by one practitioner Whaley(Whaley & Petitet, 2005) as “spending time in hell.”1 After all, domain experts
who use the language are not professional metaprogrammers, so it is paramount todetect and report errors early. At the very least, we demand that if the source ofa code generator is well-formed and well-typed, so must be its result. On the other
hand, although many partial evaluators have been proven correct (e.g., Bondorf,

1

http://math-atlas.sourceforge.net/devel/atlas_contrib/

Shifting the stage

619

1992; Dussart & Thiemann, 1996), they make it diﬃcult to express domain-speciﬁc
optimizations.
This paper presents a language for code generation that is high level in the sensethat it features an unprecedented combination of expressivity, modularity, and typesafety. Our starting point is multilevel languages such as MetaOCaml (Nielson andNielson, 1988; Gomard and Jones, 1991; Calcagno et al., 2004; Lengauer and Taha,
2006; MetaOCaml, 2006), which extend a high-level language with code-generation
constructs. These languages already oﬀer attractive support for modular, type-safe
programming. To start with, they treat generated code fragments – and functions
that transform them – as ﬁrst-class values that can be built and composed. Moreover,they guarantee that the generated code is syntactically well-formed, even well-typed
and well-scoped, so that it shall always compile. Multilevel languages are thus
popular in applications of code generation such as partial evaluation (Gomard &Jones, 1991), continuation-passing style (CPS) translation (Danvy & Filinski, 1992),
embedding domain-speciﬁc languages (Pašalić et al., 2002; Czarnecki et al., 2004),
and controlling special processors (Elliott, 2004; Taha, 2005).
Unfortunately, the type safety that current multilevel languages oﬀer comes at
a stiﬀ price of inexpressivity: many optimizations cannot be implemented in amodule that encapsulates domain-speciﬁc knowledge reusably, or even states themclearly. For example, many textbook numerical algorithms are typically expressed
as computations over mutable arrays. When specializing such algorithms, we may
be able to perform some of the computations on arrays at specialization time andso produce faster code (see Section 5.3 for an example; Sumii & Kobayashi (2001)
extensively discuss mutation in specialization). Alas, current multilevel languages
either prohibit mutations when it comes to code fragments or rescind their guarantees
of always generating well-formed code (see Section 2.1). Another example is acommon optimization called let-insertion or scalar promotion, which means to bindthe result of a complex expression such as array lookup to a temporary variable so
as to avoid recomputing it. Expressing this optimization in a clear and modular way
requires control eﬀects (Bondorf, 1992; Lawall & Danvy, 1994; Carette & Kiselyov,
2011); again, current multilevel languages either prohibit control eﬀects when it
comes to code fragments or rescind their safety guarantees (see Section 2.4).
This tension between expressivity and safety is the main challenge that we addressin this paper. We draw our notion of expressivity from Felleisen (1991): Informally,
it is the ability to deﬁne an operation without requiring a global, unmodulartransformation of the code that uses the operation. Just as it is possible to implement
mutable state in a call-by-value lambda-calculus by a state-passing transformation,
it is possible to implement both mutable array references and let-insertion in current
multilevel languages without voiding their safety guarantees. However, these features
are not expressible in current multilevel languages: We would have to programin CPS (Danvy & Filinski, 1990; Bondorf, 1992; Danvy & Filinski, 1992) or,
equivalently, monadic style (Swadi et al. 2006; Carette and Kiselyov, 2011). Hence,
although let-insertion is implementable, it is not implementable as a library function.
An expert on let-insertion cannot oﬀer it as a function that other experts can use
whenever they need it. To use let-insertion, the experts must write all of their codein CPS or monadic style. The pervasive use of CPS or monadic style is prohibitively

620

Y. Kameyama et al.

unpalatable, especially by domain experts who are not programming-language
researchers and especially in languages where ﬁrst-class functions are awkward
to express. CPS and monadic style also distort the expression of the algorithm
beyond its textbook-familiar style, as evident from the (moderately large) body ofcode developed by Carette & Kiselyov (2011). In theoretical terms, the inexpressivityof let-insertion in existing type-safe multilevel languages is troubling.
Contributions. This paper2 introduces λ , the ﬁrst multilevel language that allows
expressing a form of let-insertion – in general, a form of eﬀectful operations
on potentially open code values – while ensuring in its type system that all
generated code is well-typed and well-scoped. The language λ is the ﬁrst typesound calculus that combines code generation and delimited control. (Delimited
control in turn expresses any representable computational eﬀect (Filinski, 1994).)
The main innovation of the language is to maintain type soundness by restricting
side eﬀects incurred during code generation to the scope of generated binders. On
one hand, the language λ extends the multilevel calculus λ (Davies, 1996) withdelimited control operators. On the other hand, the language simpliﬁes a variant of
λα1v (Kameyama et al., 2008), and the restriction on eﬀects is also simple.
We have embedded the language in MetaOCaml, where the restriction has to bechecked manually, and implemented it fully in Twelf. The latter implementation alsomechanizes the proofs of type soundness. Another way to implement our language
is to translate it into any existing multilevel language using the one-pass CPS
translation we present in Section 6.
Our restriction means that let-bindings and if- and other statements are inserted
under the closest generated binder. Likewise, mutable cells and arrays created undera generated binder are not accessible beyond the scope of the binder or within
nested generated binders. In other words, no control, mutation, or other eﬀect cancross any generated binder. Exactly the same restriction holds if we implement
let-insertion or mutable cells in existing multilevel languages by means of CPS ormonadic style. Thus, any code that cannot be written in our λ (such as inserting
let-bindings across future-stage binders) cannot be written at all in any existing
type-safe multilevel language, irrespective of the style.
We demonstrate that our restriction is not severe: It does permit writing code
generators and specialization libraries that encapsulate useful high-level abstractions
such as dynamic programming. We are also able to write a framework for specialized Gaussian elimination, this time preserving the textbook-familiar style of thealgorithm. We can thus use our new language to create frameworks and embedded
domain-speciﬁc languages for program generation that application programmersand domain experts can use.
Our implementations of λ and direct-style code generators, including the examples of the dynamic-programming specialization benchmark (Swadi et al., 2005), are2

The present paper is the expanded version of our PEPM 2009 paper (Kameyama et al., 2009). The
major changes are as follows: We expanded Section 5 to discuss three larger examples of our system inuse. We revised Section 6 to present a one-pass CPS translation and prove that it preserves reductions.
We added Section 7 to extend our language to an arbitrary number of levels.

Shifting the stage

621

all available as supplementary material online at http://dx.doi.org/10.1017/
S0956796811000256 and also at http://okmij.org/ftp/Computation/staging/
README.dr
Organization. Section 2 illustrates the challenges of specialization on a simple
example of staging the memoizing ﬁxpoint combinator in MetaOCaml. For clarity,
the bulk of the paper deals with a two-level version λ
1 of our language. Section 3
introduces our new language and shows how its combination of delimited control
and staging meets the challenges. Section 4 explains the type system of our language
and proves that it is sound and delivers principal types. Section 5 gives larger
programming examples, found in the MetaOCaml literature. Section 6 presents a
CPS translation for the language. Section 7 generalizes λ
1 to the full language λwith an arbitrary number of levels. Section 8 discusses related work, and Section 9
concludes.
2 Running example
Our running example is to generate specialized code using a memoizing ﬁxpoint
combinator. The combinator underpins a simple library for dynamic programmingthat lets domain experts program their tasks without worrying about avoiding
repeated computations. Our memoizing ﬁxpoint combinator for code generationlets these domain experts generate specialized versions of their programs. The
running example illustrates both how to use the combinator to generate specialized
code and how to build the combinator to provide a useful abstraction.
We borrow the running example, quirks and all, from the dynamic-programming
specialization benchmark (Swadi et al., 2005). The benchmark had to use monadic
style to implement specialization. We use the language enriched with delimited
continuations to demonstrate the beneﬁts of expressivity, the diﬀerence between
just implementing let-insertion and expressing it. The example also illustrates thedangers of the unrestricted use of control eﬀects, motivating our restriction. We
focus on adjusting an existing library for dynamic programming and its openrecursion coding style to permit generation of specialized programs. Whether open
recursion coupled with the memoizing ﬁxpoint combinator is the best way to express
dynamic-programming algorithms is beyond the scope of this paper, and so is a
general discussion of dynamic programming, its domain-speciﬁc languages, andimplementation strategies.
As a toy dynamic-programming problem we take computing the Gibonacci
function, which generalizes the Fibonacci function and can be written in OCaml as
follows:
let rec gib x y n =if n = 0 then x else
if n = 1 then y else
gib x y (n-1) + gib x y (n-2)
There are better ways of computing Gibonacci – after all, there exists a closed
formula. The code above, however, is only slightly simpler than the serious examples

622

Y. Kameyama et al.

of dynamic programming found in the benchmark (Swadi et al., 2005), such as
longest common subsequence, binary knapsack, and optimal matrix-multiplication
ordering. We discuss such larger examples in Section 5.
To generate specialized versions of gib when the argument n is statically known,
we can write the following MetaOCaml code.
(* val gibgen: int code -> int code -> int -> int code *)let rec gibgen x y n =if n = 0 then x else
if n = 1 then y else.<.~(gibgen x y (n-1)) + .~(gibgen x y (n-2))>.
let test_gibgen n =.<fun x y -> .~(gibgen .<x>. .<y>. n)>.
A pair of brackets .<e>. encloses a future-stage expression e, which is a fragment ofgenerated code. Whereas 1 + 2 is a present-stage expression of type int, .<1 + 2>.
is a present-stage value of type int code, containing the code to add two integers.3
To combine code values, we use escapes .~e within brackets. The escaped expression
e is evaluated at the present stage; its result, which must be a code value, is spliced
into the enclosing bracket. The inferred type of gibgen above describes it as a code
generator that takes two code values as arguments (even open code values such as.<x>. and .<y>.). Brackets and escapes in MetaOCaml are thus equivalent to next
and prev in λ (Davies, 1996). They are similar to quasiquote and unquote in
Lisp, except a future-stage binder such as fun x above generates a new name andbinds it in a single operation, so no generator (even if ill-typed) ever produces illscoped code. To specialize gib to the case of n being 5, we evaluate test_gibgen 5
to yield the value.<fun x_1 -> fun y_2 ->((((y_2 + x_1) + y_2) + (y_2 + x_1)) + ((y_2 + x_1) + y_2))>.
in which MetaOCaml generates the names x_1 and y_2 fresh. This code value has
the type (int -> int -> int) code. Besides printing it, MetaOCaml can compile
it into independently usable C or Fortran code (Eckhardt et al., 2005) or run it.
2.1 Memoization
The naively specialized gib code is patently ineﬃcient like gib itself: the computation
y_2 + x_1 is repeated thrice. Gibonacci, as with dynamic-programming algorithms,
can be greatly sped up by memoization (Michie, 1968), a form of information
propagation (Sørensen et al., 1994).
The most appealing memoization method (and the one used by Swadi et al. (2006),
whom we follow) is to use the abstraction that has been developed for that purpose.
3

This expression actually has the type (’a,int) code in MetaOCaml, where the type variable ’a is anenvironment classiﬁer (Taha & Nielsen, 2003). Classiﬁers are not needed in this paper (see Section 3.1),
so we elide them.

Shifting the stage

623

The method requires minimal changes in the code. The programmer only needs torewrite the code to “open up the recursion”:
let gib x y self n =if n = 0 then x else
if n = 1 then y else
self (n-1) + self (n-2)
The function gib is no longer recursive. It receives an extra argument self for therecursive instance of itself. We “tie the knot” with the explicit ﬁxpoint combinatory_simple:let rec y_simple f n = f (y_simple f) n
Evaluating y_simple (gib 1 1) 5 yields 8 in the same ineﬃcient way as before.
To add memoization, we switch to a diﬀerent ﬁxpoint combinator y_memo_m, but
keep the same gib code (McAdam, 2001):
let y_memo_m f n =let tableref = ref (empty ()) in
let rec memo n =match (lookup n !tableref) with
| None -> let v = f memo n in (tableref := ext !tableref n v; v)| Some v -> v
in f memo n
Just as the deﬁnition of gib closely follows how a textbook might describe the
Gibonacci function, the deﬁnition of y_memo_m closely follows how a textbook
might describe memoization. We assume a ﬁnite-map data-type with the operations
empty () to create the empty table, lookup n table to locate a value associatedwith the integer key n, and ext table n v to return a new map extending table byassociating the key n to the value v. Now we can evaluate y_memo_m (gib 1 1) 30,
which ﬁnishes much faster than y_simple (gib 1 1) 30.
This memoization method is appealing because it relegates memoization to alibrary of ﬁxpoint combinators and does not distort the code of the algorithm (gibin our case). In a support library for dynamic programming (which was the goal of
Swadi et al. (2006)) this method allows application programmers to write naturaland modular code, implementing memoization strategies separately from functions
to memoize. We refer the reader to Swadi et al. (2006) for further justiﬁcation anddiscussion of this memoization method. Once again, our goal is to add staging toan already developed framework rather than to introduce our own.
However, this simple method does not work when specializing gib, for two
reasons. First, the memoizing combinator y_memo_m must use mutation so that thetwo sibling calls to self in gib, with no explicit data ﬂow between them, could reuseeach other’s computation by sharing the same memoization table. When specializing
memoized gib, the table stores code values. Alas, blindly combining mutation andstaging leads to scope extrusion, a form of type unsoundness. For example, evaluating
the expression

624

Y. Kameyama et al.

let r = ref .<1>. in.<fun y -> .~(r := .<y>.; .<()>.)>.;!rin MetaOCaml yields .<y_1>., a code fragment that contains an unbound variable
and is thus ill-formed. (MetaOCaml implicitly α-converts the names of all futurestage bound-variables into fresh names like y_1, y_2 etc.) This example illustrates
that mutation and other eﬀects, such as exceptions and control, defeat MetaOCaml’sguarantee that the generated code is well-formed and well-typed. Therefore, MetaOCaml does not assure that y_memo_m is safe to use, even though in this case itis.
In diﬀerent domains, the most proﬁtable optimizations often involve a diﬀerent setof combinators – for memoizing results, pivoting matrices, simplifying arithmetic, andso on (Cohen et al., 2006). Therefore, a language for code generation should empower
not just a programming-language researcher but also an application programmer
to create combinator libraries, including those using mutation. For such wide useof side eﬀects, the language should assure type soundness, especially the absence of
scope extrusion.
2.2 Let-insertion
Besides the risk of scope extrusion, there is a second, deeper problem: code
duplication. Suppose we stage gib with open recursion:
let sgib x y self n =if n = 0 then x else
if n = 1 then y else.<.~(self (n-1)) + .~(self (n-2))>.
Now .<fun x y -> .~(y_memo_m (sgib .<x>. .<y>.) 5)>. produces the same
ineﬃcient specialized gib as before, with the computation y_2 + x_1 repeatedthrice. Thus, whereas code generation is memoized, the generated code does notmemoize (Bondorf & Danvy, 1991). For example, we want y_memo_m (sgib .<x>.
.<y>.) 4 to return .<let t = y + x in let u = t + y in u + t>., where nocomputation is duplicated. In this desired output, self 2 should contribute thebinding and use of u, and self 3 those of t, but these contributions are not codefragments – subexpressions – that can be spliced in by escapes.
One way to insert let as desired is to write the code generator in CPS or monadic
style (Danvy & Filinski, 1990; Bondorf, 1992; Danvy & Filinski, 1992; Swadi et al.,2006). The memoized calls to the code generator can then share the memoizationtable and insert let-bindings as necessary, without risking scope extrusion. In
monadic style, the function gib takes the following form (Swadi et al., 2005):
let sgib_c x y self n =if n = 0 then ret x else
if n = 1 then ret y elsebind (self (n-2)) (fun r1 ->bind (self (n-1)) (fun r2 ->ret .<.~r2 + .~r1>.))

Shifting the stage625

We omit the deﬁnitions of the monad operations ret and bind and of the memoizing
combinator that applies to sgib_c. All this code no longer resembles textbook
algorithms, so it has lost its appeal of simplicity. Syntactic sugar for monadic
code (Wadler, 1992; Peyton Jones, 2003; Minsky, 2008; Carette & Kiselyov, 2011)
reduces the clutter but not the need to name intermediate results such as r1 and r2
above. In practice (for example, to generate Gaussian-elimination code), monadic
style imposes a severe notational overhead (Carette & Kiselyov, 2011) that alienates
application programmers and obstructs our quest to help end users specialize theircode. Theoretically, the problem is of expressivity (Felleisen, 1991): The direct-stylespecialized sgib diﬀers from the unspecialized code gib only in staging annotations
for parts of the code; erasing annotations from sgib recovers the original sgib. The
relation of sgib_c to sgib is quite more involved, including not only the placementof local staging annotations but also the global rewriting of the whole code to themonadic style. Therefore, in order to use the staging memoizing ﬁxpoint combinatorof (Swadi et al., 2006), the end user has to ﬁrst rewrite the code in the monadic
style – indicating that the memoizing ﬁxpoint combinator is inexpressive in pure
MetaOCaml.
2.3 If-insertion
We have seen that let-insertion is necessary to avoid code duplication in practicalcode generators and requires the unappealing use of CPS or monadic style. A similar
pattern is if-insertion (or assertion insertion), illustrated below. The code generator
gen invokes an auxiliary generator retrieve to extract the result of a complex
computation on a working array:let gen retrieve =.<fun array n -> (complex computation on array);.~(retrieve .<array>. .<n>.)>.
The auxiliary generator retrieve receives two code values from gen, which represent
an array and an index into it. The code generated by retrieve could just read then-th element of array:
let retrieve array n = .< (.~array) . (.~n) >.
We would like, however, to check that n is in the bounds of array. We could insert
the bounds check right before the array access:let retrieve array n =.<assert (.~n >= 0 && .~n < Array.length .~array);(.~array) . (.~n)>.
Such a check is too late: We want the check right after the array and the index aredetermined, before any complex computations commence. We wish the generator
gen to yield.<fun array_1 -> fun n_2 ->assert (n_2 >= 0 && n_2 < Array.length array_1);

626

Y. Kameyama et al.
(complex computation on array_1);
array_1.(n_2)>.

Again, it seems impossible for retrieve to splice in the assert far from theescape in gen. Again, this diﬃculty can be overcome by writing generators in CPS
or monadic style, which looks foreign to the application programmer. Again, therewriting of the code in CPS or monadic style indicates that if-insertion is not
expressible in pure MetaOCaml (without resorting to eﬀects).

2.4 Delimited control and its risk of scope extrusion
Lawall & Danvy (1994) show how to use Danvy and Filinski’s delimited control
operators shift and reset (Danvy & Filinski, 1989, 1990, 1992) to perform letand if-insertion in the familiar direct style by eﬀectively hiding trivial uses ofcontinuations as in sgib_c above. Since delimited control operators are available in
MetaOCaml (Kiselyov, 2010), we can build a memoizing staged ﬁxpoint combinatory_ms with this technique so that evaluating.<fun x y -> .~(top_fn (fun _ -> y_ms (sgib .<x>. .<y>.) 5))>.
– using the same direct-style sgib in Section 2.2 – gives the ideal code.<fun x_1 -> fun y_2 ->let z_3 = y_2 in
let z_4 = x_1 in
let z_5 = (z_3 + z_4) in
let z_6 = (z_5 + z_3) in
let z_7 = (z_6 + z_5) in (z_7 + z_6)>.
without duplicating computations. (We describe the memoizing staged ﬁxpoint
combinator y_ms and the let-insertion locus speciﬁer top_fn in Section 3.4.) The
same delimited control operators let us accomplish if-insertion using the intuitive
way to write gen in Section 2.3.
Delimited control, however, is a side eﬀect whose unrestricted use poses the riskof scope extrusion. For example, the expression
top_fn (fun _ -> .<fun x y -> .~(y_ms (sgib .<x>. .<y>.) 5)>.)is well-typed in MetaOCaml with shift and reset added, but it evaluates to thefollowing code value, which disturbingly uses the variables y_2 and x_1 unbound.
.<let z_3 = y_2 in
let z_4 = x_1 in
let z_5 = (z_3 + z_4) in
let z_6 = (z_5 + z_3) in
let z_7 = (z_6 + z_5) in
fun x_1 -> fun y_2 -> (z_7 + z_6)>.

Shifting the stage

627

Fig. 1. Syntax of λ
1.

3 Combining staging and control safely
To eliminate the risk of scope extrusion just demonstrated, we propose a simple
restriction: Informally, we place an implicit present-stage reset under each futurestage binder. Any escape under a future-stage binder thus incurs no eﬀect observable
outside the binder’s scope. This restriction turns out to permit many practicalforms of memoization, let-insertion, and if-insertion – in particular, all of thecases described by Carette and Kiselyov (2011) and Swadi et al. (2005, 2006) –so application programmers can now implement such optimizations safely (without
risking scope extrusion) and naturally (in direct style). Theoretically, let- and ifinsertion become expressible.
In this section, we detail our proposal by introducing a language with staging
and control eﬀects that builds in this restriction and, as we prove, prevents scope
extrusion. For clarity, until Section 7 we restrict our attention to a two-level version of
the language, called λ
1 . The language models a subset of MetaOCaml extended withdelimited control operators. (Delimited control operators may appear in both stages.
Just as we defer dealing with staging forms in the future-stage code until Section 7, we
could have likewise deferred future-stage delimited control. Doing so however makes
the type system, Section 4, less uniform and harder to understand.) Figure 1 shows thesyntax: It features integer literals n and their arithmetic +, λ-abstractions and theirapplications, and pairs (e1 , e2 ) and their projections fst and snd. We write let x1 = e1
and . . . and xn = en in e as shorthand for (λx1 . . . . λxn . e)e1 . . . en . The conditional
ifz e then e1 else e2 reduces to e1 if e is zero, and to e2 if e is a nonzero integer literal.
The constant ﬁx is the applicative ﬁxpoint combinator. In λ
1 , λ-abstractions are theonly binding forms, which simpliﬁes the Twelf implementation and the mechanizationof type soundness. (The same motivation explains our implementation choice forpair projections, as higher-order constants rather than syntactic forms.) As usual,
we identify α-equivalent terms and assume Barendregt’s variable convention. The
operational semantics of these constructs is standard and call-by-value, as deﬁned
in Figures 2 and 3 in terms of small steps
and evaluation contexts C 0 . In thesubsections below, we explain the staging forms e and se, the level superscripts 0
and 1, the delimited control forms d and {e}, and their interaction.
We have implemented the language in Twelf, where the eﬃcient Gibonacci
generator can run. Unlike our Twelf implementation, MetaOCaml does not currently
build in our restriction, so we must manually examine each escape under a futurestage binder and check that it has no observable control eﬀect, inserting reset
otherwise. It is possible to automate this check, either by extending MetaOCaml’s
type checker or by building a separate tool like Leroy and Pessaux’s exception
checker (Leroy & Pessaux 2000). It may be simpler however to add staging to a

628

Y. Kameyama et al.

Fig. 2. Values and contexts.

dialect of ML that has delimited control with the (superset of the) type systemdescribed in the present paper (Masuko & Asai, 2009).
3.1 Staging
As described in Section 2, our staging facility consists of brackets e and escapes
se. These constructs are written .< >. and .~ in actual MetaOCaml code. The
staging level of an expression aﬀects whether it is a value and how a non-value isdecomposed into a context and a redex (Taha, 2000). So far, our calculus has only twolevels, present stage and future stage (more levels are introduced in Section 7). They
correspond to two evaluation “modes,” reduction and code-building (Igarashi &Iwaki, 2007). To notate these levels, we put the superscripts 0 and 1 on metavariables,such as values and contexts in Figure 2.4 Brackets enclose a future-stage expression
to form a present-stage expression, whereas escapes do the opposite. In particular,present-stage values v 0 include code fragments v 1 , which are bracketed expressions
containing no escapes.
A present-stage context C 0 can be plugged (that is, have its hole  replaced)with a present-stage expression e to form a complete program C 0 [e], whereas
a future-stage context C 1 can be plugged with a future-stage expression. As isusual in a multilevel language, these contexts may contain future-stage bindings
introduced by λ, so present-stage evaluation can occur in the body of a future-stage
abstraction. Contexts C i are deﬁned by composing delimited contexts Dij , which canbe plugged with a level-j expression to form a level-i expression. Delimited contexts
are in turn deﬁned by composing frames F i , which are the smallest, with respect
to decomposition, non-empty contexts. A frame F i can be plugged with a level-i
expression to form a slightly larger level-i expression. In a degenerate language
4

Our Twelf formalization marks each expression as well with its level, but we suppress those superscripts
in this paper.

629

Shifting the stage

Fig. 3. Operational semantics: small-step reduction ee .

with neither staging nor delimited control, the superscripts would all be 0, and acontext C 0 and a delimited context D00 would both be just a sequence of frames F 0 .
If for a moment we disregard delimited control operators (to be explainedin Section 3.2), then the language λ
1 is almost the same as our earlier two-levelstaged calculus λα1v (Kameyama et al., 2008), but without cross-stage persistence andwithout the operation run to execute generated code. It can thus be regarded as
Davies’s λ (1996) restricted to two levels. It is also similar to Nielson and Nielson’s(1988) and Gomard and Jones’s (1991) two-level λ-calculi (though the latter does
not type-check the generated code).
Excluding run from our language makes it simpler to implement: otherwise,
either the run-time system has to include a compiler and a dynamic linker, or ourcompiler should be capable of producing target code that produces target codeat run-time (see Leone & Lee, 1998 for the example of the latter). Excluding run
makes the language simpler to prove sound, because the type system need notinclude environment classiﬁers (Taha & Nielsen, 2003) to prevent attempts to run
open code. The inability to run generated code in the language may appear severe,but it is no diﬀerent from the inability of the typical compiler (especially crosscompiler) to load and run any generated code in the compiler process itself. A code
generator written in λ
1 cannot run any generated code on the ﬂy to test it, but thegenerated code is guaranteed to be well-typed and can be saved to a source ﬁle tobe compiled and run in a separate process. That already supports the intended use
for λ
1 , namely to build domain-speciﬁc language “compilers” that generate families
of optimized library routines – such as Gaussian elimination (Carette & Kiselyov,
2011), Fast Fourier Transform (Frigo & Johnson, 2005; Kiselyov & Taha, 2005),
linear signal processing (Püschel et al., 2005), and embedded code (Hammond &Michaelson, 2003) – to be used in applications other than the generator itself.
The lack of cross-stage persistence in λ
1 means that there is no “polymorphic
lift” operation to uniformly convert a present-stage value of any type to somefuture-stage code that evaluates to that value. However, λ
1 can express lifting at

630

Y. Kameyama et al.

0

1

Fig. 4. Bubble-up reductions for delimited control, replacing rules d and d in Figure 3.

speciﬁc data types – integers, pairs of integers, and so on, as discussed by Davies
and Pfenning (2001). Whereas cross-stage persistence is important when using run(Taha & Nielsen, 2003), it is unnecessary for mere code generation. It can evenbe harmful if unrestricted because a generated library routine ought to be usable
without the generator being present.

3.2 Delimited control
Delimited control is realized by the control delimiter { } (pronounced “reset”) andthe constant d (pronounced “shift”).
When d is not used, the expression {e} (pronounced “reset e”) is evaluated like e,
as if {e} were just shorthand for (λx. x)e. We specify this behavior by allowing
contexts C 0 to include resets { }.
The constant d is supposed to be applied to a function value, say v 0 . When dv 0 is
evaluated, it captures the part of the current evaluation context C 0 up to the nearest
dynamically enclosing delimiter. We call this part a delimited context D00 ; unlike
C 0 , it does not include reset. As the d0 rule in Figure 3 shows, the subexpression
D00 [dv 0 ] reduces to the application v 0 (λx. {D00 [x]}), reifying the captured delimited
context D00 as the abstraction λx. {D00 [x]}.
The single step d0 reduction (and its companion d1 , discussed in Section 3.3) canbe decomposed into a sequence of ﬁner grain reductions in which the d-application
bubbles up and builds up the delimited context by local rewriting (Felleisen et al.,
1986; Parigot, 1992). More speciﬁcally, we can replace the rules d0 and d1 in
Figure 3 by the rules in Figure 4. The bubble-up reductions are truly small-step inthat they do not require examining an arbitrarily long part of the context looking
for the delimiter (such as reset). The bubble-up reductions are therefore insightful,and easier to mechanize, especially in our case where future-stage binders also act ascontrol delimiters (see Kameyama et al., 2010 for more details on mechanization).
The attraction of delimited control is the ability to express any representablecomputational eﬀect (Filinski, 1994). We illustrate this ability by using delimited
control to simulate mutable state (Filinski, 1994; Kiselyov et al., 2006). We deﬁne
the terms
const = λy. λz. y,

get = d(λk. λz. kzz),

put = λz  . d(λk. λz. kz  z  ).

(1)

631

Shifting the stage
The reduction sequence below illustrates how const and get work:{const (get + 40)} 2

d0 {(λk. λz. kzz)(λx. {const(x + 40)})} 2
βv {λz. (λx. {const(x + 40)})zz} 2{}(λz. (λx. {const(x + 40)})zz) 2βv(λx. {const(x + 40)}) 2 2βv{const(2 + 40)} 2(2)

The ﬁrst step replaces get and its delimited context const( + 40) by an applicationof λk. λz. kzz to the function λx. {const(x + 40)}. The latter function is precisely thecaptured delimited context, enclosed in reset and reiﬁed as a function.
Comparing the initial and ﬁnal programs in this reduction sequence shows thatits net result is to replace the expression get with 2. It is as if number 2 were stored
in a cell and accessed by get in the program get + 40. The reductions continue to avalue:{const 42} 2βv {λz. 42} 2{} (λz. 42) 2

βv 42

(3)

The reader may be reminded of the standard state-passing emulation of mutablestate, in which every expression receives the current state as the argument. The
just shown reductions have also occurred in the context of the application to thecurrent state, 2. To be precise, the program like get + 40 is evaluated in the context{const } 2 that when plugged with a state-invariant expression e will ignore thecurrent state, delivering e’s value. (One can easily see that if a program e contains
no d, then {e} is observationally equivalent to e.) The expressions like get “reachout and grab” the current state from the context.
We can also mutate the state: the term put(get + 1) increments the number in thecell and returns the new number.
{const (put(get + 1) + get)} 2+{const (put(2 + 1) + get)} 2+{const (put 3 + get)} 2+(λx. {const (x + get)}) 3 3(4)βv {const (3 + get)} 3

This sequence of reductions replaces the term put(get + 1) with 3 and at the sametime puts the new value 3 outside the reset. The result reduces to {const(3 + 3)} 3
and eventually 6. In general, the term {const e}v 0 behaves as if the expression e were
executed in the “context” of a mutable cell initialized to v 0 . Inside e, occurrences ofget retrieve the current value of the cell, and calls to put mutate the cell.
Although our language has no mutable state, we have just emulated it using
delimited control. We can therefore treat a memoization table as a piece of mutablestate, express the memoizing ﬁxpoint combinator y_memo_m (for details, see theaccompanying code in circle-shift-1.elf), and use it to transparently memoize
gib or another dynamic-programming algorithm in λ
1.
For the purpose of code generation, emulating mutable state by delimited control
brings two beneﬁts. First, our core calculus is smaller and its soundness is simpler
to prove. Second, the delimited nature of our control operations lets us limit the632

Y. Kameyama et al.

lifetime (or dynamic extent, Moreau 1998) of mutable state. In other words, we canmake sure that a mutable cell is only accessed or updated during the evaluation of aparticular subexpression. To prevent scope extrusion, it is crucial that our language
provides this assurance both in the operational semantics (described in Section 3.3)
and in the type system (described in Section 4). Although optimizing compilers ofimperative languages can determine the extent of mutation by control-ﬂow analyses,
the results of the analyses are not expressed in the language or exposed to theprogrammer.
3.3 Staging and delimited control without scope extrusion
At ﬁrst glance, it appears straightforward to combine staging and delimited control.
For example, the emulation of mutable state by delimited control appears to work
as explained in Section 3.2 even if we store code values rather than integers in themutable state and access them within escapes. For example, the following example
reuses a code value using const, get, and put:{const s(put8 + 5) + sget} 0βv{const s(d(λk. λz. k8 + 58 + 5)) + sget} 0

d0 {(λk. λz. k8 + 58 + 5)(λx. {constsx + sget})} 0{const s8 + 5 + sget} 8 + 5

(5)

+
s

{const (8 + 5) + sget} 8 + 5+

(8 + 5) + (8 + 5)

Like in Section 3.2, put8 + 5 assigns 8 + 5 to the mutable cell, so get is later
replaced by 8 + 5. The ﬁnal result is a piece of generated code that, when evaluatedin the future stage, will add 5 to 8 twice. The only apparent diﬀerence between
this emulation of mutable state and the examples in Section 3.2 is that captured
delimited contexts, such as λx. {constsx + sget} in the second reduction above,
may span across brackets and escapes.
We now confront the two problems described in Section 2 that arise when
memoizing code generators. The ﬁrst problem is the risk of scope extrusion, which
can happen when we store a code value that uses a bound variable then splice thecode value outside the scope of the variable. Let us try to trigger scope extrusionin λ
1:{const (let x = λy. s(puty) in get)} 0

(6)

If puty above were to assign the code value y to the mutable cell and get were to
retrieve that code value, then this program would generate the ill-scoped code y.
Fortunately, put cannot reach the mutable cell because the future-stage binder λystands in the way. In Figure 2, this restriction is built into the deﬁnition of delimited
contexts, which excludes not only present-stage resets but also future-stage binders.
Our attempt at scope extrusion thus fails; in fact, the type system in Section 4 rejects
it statically. We prove that scope extrusion is impossible in Section 4.2.
The d1 rule in Figure 3 shows that a future-stage binder acts as a control delimiter
just as a present-stage reset does: a future-stage abstraction λx. e implicitly expands
to λx. s{e}. In this regard, staging and delimited control are not orthogonal:Shifting the stage633

whenever staging brings evaluation under λ, any side eﬀect (in particular the lifetimeof mutable state) must also stay under λ. Our language prevents diﬀerent future-stage
scopes from sharing a memoization table because doing so risks scope extrusion.
The second problem with memoizing code, described in Section 2.2, is that thegenerated code duplicates computations such as 8 + 5 above. Armed with delimited
control operators, we can now solve this problem by inserting let in the generated
code without writing our code generator in CPS or monadic style. To illustrate
this key idea (due to Lawall & Danvy 1994 in an untyped setting), we deﬁne thefollowing alternative to put:
put = λz  . d(λk. λz. let x = sz  in s(kxx))(7)

Using this put instead of put, it is easy to insert let in the generated code to avoid
duplicating computations:{const s(put 8 + 5) + sget} 0βv{const s(d(λk. λz. let x = s8 + 5 in s(kxx))) + sget} 0

d0 {(λk. λz. let x = s8 + 5 in s(kxx))(λy. {constsy + sget})} 0
let x = 8 + 5 in s({const x + sget} x)

++let x = 8 + 5 in x + x

(8)Instead of storing any code for reuse that may contain a complex computation, put
inserts a let to bind the result of the computation to a new variable (x = 8 + 5
above) that takes scope over the entire generated expression, then stores just thevariable. The generated code performs the computation only once and can reuse theresult.
3.4 Payoﬀ: safe and eﬃcient code generation in direct style
We have shown how to simulate mutable state and perform let-insertion using
delimited control. Using these techniques, we have built the desired memoizing
staged ﬁxpoint combinator y ms (see circle-shift-1.elf for the complete codeand tests). Roughly,5 y ms has the type ((int → int) → int → int) → int → int.
As this type suggests, this combinator should be applied to a code generator with
open recursion whose ﬁrst argument is the recursive instance of itself, and second
argument is a present-stage integer on which to specialize and recur. For example,
recall the sgib function in Section 2.2:
sgib = λx. λy. λself . λn. ifz n then x else
ifz n − 1 then y elses(self (n − 1)) + s(self (n − 2))(9)

To specialize the Gibonacci function to n = 5, we evaluate6
λx. λy. s({const (y ms (sgib xy) 5)} empty)
5
6

(10)

We suppress eﬀect annotations in types until Section 4, where we introduce the type system formally.
This example reveals that top fn in Section 2.4 is λz. {const (z 0)} empty.

634

Y. Kameyama et al.

Fig. 5. The memoizing staged ﬁxpoint combinator y ms.

(where empty is the empty memoization table) to obtainλx. λy. let z3 = y in let z4 = x in let z5 = z3 + z4 in
let z6 = z5 + z3 in let z7 = z6 + z5 in z7 + z6 .

(11)This result is the ideal promised in Section 2.4 – a linear sequence of operations
without any code duplication.
Figure 5 shows our deﬁnition of y ms. (The reset on the last line of the code
compensates for the lack of impredicative answer-type polymorphism in our system
as Section 4.1 explains in detail.) This ﬁxpoint combinator simulates mutable state
to maintain a memoization table that maps integer keys to previously generated
code values. Therefore, it uses the table operations empty, lookup, and ext speciﬁedin Section 2.1, which are pure functions and trivial to implement. Whereas lookup
in Section 2.1 returns a value of type int option, our language λ
1 does not include
option, so we emulate the sum type τ option by a product type (int , int → τ): thevariant None is represented as (0, ﬁx λf. f) and the variant Some x as (1, λz. x).
When y ms is applied to a user function f and that function invokes self on an
integer argument n, our combinator retrieves the current state of the memoizationtable to check if code has been already generated for n. The lookup result (a pair)is bound to the variable x in Figure 5. If fst x is zero, meaning n is new, thenthe combinator invokes f to generate an expression y for n, binds y to a new
future-stage variable z, and updates the memoization table to map n to z. If thelookup succeeds (the last line of the code), then the combinator returns the foundvalue without invoking f.
In this way, we have successfully specialized the Gibonacci function in direct style
as well as Gaussian elimination and Swadi et al.’s (2005) other examples. These
successes show that our language is expressive enough for practical applications
despite not allowing delimited control to reach beyond any binder. We discuss theselarger examples in Section 5.
If-insertion is also within reach. To use a simpler example than in Section 2.3,
suppose that gen is a code generator in λ
1 of the form λf. λn. e + s(fn), where eis some complex computation. The argument f is an auxiliary generator, a function
from code to code. Suppose the code produced by f only makes sense if the futurestage argument n is nonzero – perhaps fn computes the inverse of n. We would
like the generated code to check if n is nonzero before evaluating e. To achieve thisgoal, we can deﬁne f to be
λn. d(λk. ifz sn then fail else s(kinverse sn)).

(12)

Shifting the stage

635

Passing this auxiliary generator to gen produces the desired code
λn. ifz n then fail else e + inverse n.

(13)

The complex expression e will not be evaluated if n turns out to be zero.
Our language is too restrictive when a code generator needs to reach beyond thenearest generated binder to insert a let, if, or assert, or access a piece of mutablestate. For example, if the code generated by f above takes a second argument mafter n, then the test on n would be inserted under λm, even though it may savemore computation to insert the test above λm. This situation can arise in Section
2.3 if the order of the arguments array and n is reversed in gen: we want to insert
assertions as in.<fun n_2 -> assert (n_2 >= 0);
fun array_1 -> assert (n_2 < Array.length array_1);(complex computation on array_1);
array_1.(n_2)>.
but we can only achieve.<fun n_2 -> fun array_1 -> assert (n_2 >= 0);
assert (n_2 < Array.length array_1);(complex computation on array_1);
array_1.(n_2)>.
even though the assertion n_2 >= 0 does not mention array_1. Similarly, for
let-insertion: while generating the body of a loop that binds an index variable,
we cannot insert a let-binding outside the loop even if the right-hand side ofthe let-binding does not mention the index variable. In other words, we cannot
express loop-invariant code motion. Balat et al.’s (2004) use of control eﬀects fornormalization-by-evaluation of sums also needs to reach beyond generated binders
and is unsupported by our language.

4 Type system
We have seen in Section 3.3 that attempting to generate code with scope extrusion inλ
1 causes the generator to get stuck. We now describe the type system that statically
prevents such a dynamic error. A well-typed generator shall not get stuck; anattempt at scope extrusion will be reported early, when type checking the generator
rather than when running it. Figure 6 displays the type system of our language λ
1.
It combines a simpliﬁcation of Danvy and Filinski’s (1989) type system for delimited
control and a simpliﬁcation of Davies’s (1996) type system for staging in a soundbut not orthogonal way.

The types τ of λ
1 are the base type int, arrow types τ → τ /τ0 , product types
(τ, τ ), and code types υ/υ0 . The type system is monomorphic like the simply typed
λ-calculus; we include type variables α only to state that our language has principal
typings.

636

Y. Kameyama et al.

Fig. 6. The type system of λ
1.

As a two-level language, λ
1 operates on code values in the present stage only.
Hence, the type of a future-stage expression never contains any code type. Terms
such as 42 are thus disallowed, and types such as int / int/ int are uninhabitedby any closed value. We reserve the metavariable υ for a type that contains no code
type. A type environment Γ is a set of associations x : τ of present-stage variables x
with types τ and associations x : υ of future-stage variables x with types υ.
There are two judgment forms, one for present-stage expressions and anotherfor future-stage expressions. Both forms include answer types to track the control
eﬀects that may occur: in a present judgment Γ  e : τ ; τ0 , the answer type isτ0 at the present stage; in a future judgment Γ  e : υ ; τ0 ; υ0 , the answer types
are τ0 at the present stage and υ0 at the future stage.7 The future answer type υ0is needed to ensure that the generated code, which may incur control eﬀects inthe future stage, never goes wrong. Those type metavariables in Figure 6 with

7

For simplicity, we equate the two answer types distinguished by Danvy and Filinski (1989). It is easy
but not necessary to restore the distinction. The distinction is useful – for example, to express typed
printf (Danvy, 1998) in direct style with staging (Asai, 2009, personal communication).

Shifting the stage

637

numeric subscripts (such as τ0 ) are answer types that can be ignored on the ﬁrst
reading. Because constructs such as addition that have nothing to do with staging
or delimited control are type-checked in the same way at both stages, we writeΓ  e : τ ; τ0 [; υ0 ] to mean either a present judgment (without “; υ0 ”) or a future
judgment (with “; υ0 ”).
An answer type is the type of the result of plugging an expression into a delimited
context. In other words, an answer type is the type of an expression surrounded
by a control delimiter. To take an example from Section 3.2, in the program{const (get+40)} 2, the answer type of the expression get plugged into the delimited
context const( + 40) is the type of a function from int to int, even though thewhole program has the type int instead. In terms of CPS, an answer type is just thecodomain type of a continuation or computation. In fact, our type system is just a“pullback” of the staged type system of our CPS target language in Section 6.
Since answer types are eﬀect annotations, they appear not only in judgments but
also in function types and code types (“/τ0 ” and “/υ0 ”), where eﬀects are delayed.
The typing rules for λx. e show that the eﬀect of e (represented by the answer types
τ1 and υ1 ) is incurred only when the function is invoked. The typing rules for eand se show that the future eﬀect of a code value (represented by the answer
type υ0 ) will be incurred only where the code value is spliced in (and never in thepresent stage).
As an example, the following derivation shows that the program {const (get +40)} 2 in Section 3.2 is well-typed. (Let T = int → int /τ0 and S = ((int → T /τ0 ) →T /T ) → int /T .)..
..
k : (int → T /τ0 )  λz. kzz : T ; T[]  d : S ; T []  λk. λz. kzz : (int → T /τ0 ) → T /T ; T[]  get : int ; T[]  get + 40 : int ; T[]  const (get + 40) : T ; T[]  {const (get + 40)} : T ; τ0[]  {const (get + 40)} 2 : int ; τ0

(14)

The accompanying ﬁle circle-shift-1.elf type-checks many tests in Twelf. For
example, the ﬁxpoint combinator y ms in Section 3.3 has the type((int → υ/υ1 ) → int → υ/υ0 ) → int → υ/υ0 ,(15)

in which the present-stage answer types are all(int → T /T ) → υ  /υ0 /υ  /υ0 ,(16)

in which int → T /T is the type of the memoization table, and the type T =(int , int → υ/υ0 /υ/υ0 ) encodes the lookup result type υ/υ0  option as explainedin Section 3.4.

638

Y. Kameyama et al.
4.1 Purity and answer-type polymorphism

Our type system has no polymorphism and hence is unable to straightforwardly
represent answer-type polymorphism that is characteristic of pure expressions. The
answer-type polymorphism is required in practice, even for our examples. Fortunately(somewhat inconvenient) roundabout ways of representing answer-type polymorphism are possible, which we discuss in this section. The inconvenience of emulating
answer-type polymorphism is the drawback we share with the CPS/monadic styleof encoding eﬀectful generators in a system without impredicative polymorphism.
An expression is pure if it incurs no observable control eﬀect; a pure expression ispolymorphic in the answer type (Thielecke, 2003). For example, it is easy to derive
the judgment Γ  (2 + 40) : int ; τ0 for an arbitrary answer type τ0 . In words,
since the expression 2 + 40 incurs no observable control eﬀect, it is safe to plug
it into any delimited context that expects an int, no matter what type τ0 resultsfrom the plugging. In contrast, the expression get + 40 incurs a control eﬀect, as
observed in Section 3.2. Our type system detects this eﬀect: It derives the judgmentΓ  (get + 40) : int ; τ0 if and only if the answer type τ0 has the form int → τ /τ1 forsome τ and τ1 . In words, it is safe to plug the expression get + 40 into a delimited
context that expects an int if and only if a function from int results from the plugging.
Our use of answer types to track control eﬀects, like any eﬀect system, exacerbates
the need for polymorphism. To start with, all values are pure, and the soundness of
our type system relies on their polymorphism in the answer type.
Lemma 1 If e is a value and Γ  e : τ ; τ1 [; υ0 ], then Γ  e : τ ; τ2 [; υ0 ].
Proof By induction on e and inversion on the derivation of Γ  e : τ ; τ1 [; υ0 ].
(In our Twelf code circle-shift-1.elf, the constructive proof of the lemma isrepresented by total type families val-new-at and val-new-at+.)For example, each occurrence of a bound variable x : τ must have the same type τ
but may have a diﬀerent answer type τ0 , so subject reduction for our βv and {} rules
relies on Lemma 1.
Values are just one particularly easy-to-identify class of pure expressions. Control
delimiters also make an expression pure by masking its eﬀect: In the typing rules forpresent-stage {e} and future-stage λx. e in Figure 6, the answer type τ0 is arbitrary.
The latter rule reﬂects how future-stage binders delimit present-stage control in theoperational semantics: The present-stage answer type is the code type υ  /υ1  in thepremise but arbitrary in the conclusion.
It is also pure to apply a pure function, but our type system does not represent
the purity of functions except by hard-coding the answer-type polymorphism of“built-in functions” such as ﬁx, fst, snd, and ifz into their typing rules (witness thetype metavariables τ0 and τ1 in those rules). For example, each occurrence of ﬁx v 0
must have the same function type τ → τ /τ2 but may have a diﬀerent answer type τ1 ,so subject reduction for our ﬁx rule relies on the trivial variant of Lemma 1 where
e is replaced by ﬁx v 0 .
Without impredicative answer-type polymorphism (Asai & Kameyama, 2007), oursystem never infers the purity of a user-deﬁned function. Consequently, in order toShifting the stage

639

write the desired code as in Section 3.4, we are forced to build product types andint into the language rather than Church-encode them. (This task is not diﬃcult; we
could have introduced the desired option data type.) Furthermore, we sometimes
need to annotate programs with additional resets. For example, the last line in
Figure 5 contains a rather mysterious reset, without which the code would not
type-check. The reason is that the lookup result x must have a type of the form
(int , int → υ/υ0 /τ0 ), where τ0 is some answer type. Without the reset, τ0 would be
uniﬁed with the answer type of the overall memoizing computation, which contains
the type of the memoization table, which in turn contains the type of x, whichcauses an occurs-check failure. With the reset, the answer type τ0 is uniﬁed withthe return type υ/υ0 , which passes the occurs check. In general, we can always
emulate a pure function type τ → τ by an impure function type τ → τ /τ , at thecost of additional resets. (We could take advantage of let-polymorphism, were it
present in our calculus, to infer the answer-type polymorphic type for pure functions.
Let-polymorphism does not help in the above case since the pure function is stored
in a data structure.)
The need to insert resets is a drawback – which is not however speciﬁc to ourdirect-style approach; exactly the same issue arises if we program in CPS/monadic
style. We observe the problem even for the unstaged state-passing memoizing ﬁxpoint
combinator in OCaml, if we implement the memo table, with keys ’a and values ’b as
we did in our calculus, with the type (’a -> bool * (unit -> ’s -> (’s,’b))).
The function of type unit -> ’s -> (’s,’b), essentially from Some, is written instate-passing style, for state of type ’s. The memo table is the state of the overall
computation, thus ’s must be the type of the whole table – hence the occurs-check
failure. The solution is to note that the projection function must be pure, that is,does not aﬀect the state; to indicate the purity, we wrap the projection function
into “reset,” deﬁned in our case as fun m -> fun s -> (s,snd (m empty)). The
problem does not arise if we avail ourselves to the built-in option type; the projection
function from Some is manifestly pure. In our extensive practical experience ofprogramming in both CPS/monadic style and direct style, the problem of lack ofpolymorphism and the need to introduce reset is exceedingly rare.

4.2 Formal properties
We are ready to formalize the safety assurances provided by our type system. The
formal properties of λ
1 and their proofs have been mechanized in the accompanying
Twelf code; see the ﬁle circle-shift-1.elf. In the present section, we restate theseproperties in mathematical notation and draw their corollaries.
Lemma 2 (type substitution) Let θ be a substitution on type variables. If thejudgment Γ  e : τ ; τ0 [; υ0 ] is derivable and Γ ⊇ Γθ, then the judgmentΓ  e : τθ ; τ0 θ [; υ0 θ] is derivable.
Proof By induction on the derivation of Γ  e : τ ; τ0 [; υ0 ]. For example, supposeΓ  x : τ ; τ0 . By inversion, (x : τ) ∈ Γ. Thus, (x : τθ) ∈ Γθ ⊆ Γ , so Γ  x : τθ ; τ0 θ. 

640

Y. Kameyama et al.

Proposition 3 (principal typing) If some judgment Γ  e : τ ; τ0 [; υ0 ] is derivable,
then some judgment Γ̂  e : τ̂ ; τˆ0 [; υˆ0 ] is derivable such that, for any derivable
judgment Γ  e : τ ; τ0 [; υ0 ], there exists a substitution θ for type variables so thatΓ ⊇ Γ̂θ, τ = τ̂θ, and τ0 = τˆ0 θ [and υ0 = υˆ0 θ].
Proof By induction on e, essentially reading our syntax-directed type system as abottom-up logic program that infers the principal typing using uniﬁcation. We show
two cases.
Case e = x at the present stage: Set τ̂ and τˆ0 to fresh type variables, and Γ̂ to x : τ̂.
Case e = λx. e1 at the present stage: We want to prove that, given Γ  λx. e1 :(τ1 → τ2 /τ3 ) ; τ0 is derivable, some judgment Γ̂  λx. e1 : (τˆ1 → τˆ2 /τˆ3 ) ; τˆ0 isderivable such that, for any derivable Γ  λx. e1 : (τ1 → τ2 /τ3 ) ; τ0 , there is a
substitution θ such that Γ ⊇ Γ̂θ and τi = τ̂i θ (i = 0, 1, 2, 3). By inversion, we getΓ, x : τ1  e1 : τ2 ; τ3 is derivable. By induction hypothesis, we have a principal
derivation Γ̌  e1 : τˇ2 ; τˇ3 . We have the following two subcases:
Subcase (x : τˇ1 ) ∈ Γ̌ for some τˇ1 : Set Γ̂ = Γ̌ − (x : τˇ1 ) and τ̂i = τ̌i (i = 1, 2, 3). Let τˆ0
be a fresh type variable, then Γ̂  λx. e1 : τˆ1 → τˆ2 /τˆ3 ; τˆ0 is derivable. We also havethat for each derivable judgment Γ  λx. e1 : τ1 → τ2 /τ3 ; τ0 there exists a derivable
judgment Γ , x : τ1  e1 : τ2 ; τ3 . By induction hypothesis, there exists a substitution
θ such that (Γ , x : τ1 ) ⊇ Γ̌θ and τi = τ̌i θ (i = 2, 3). The former implies τ1 = τˇ1 θ .
By setting θ = θ [τˆ0 → τ0 ], we have Γ ⊇ Γ̂θ and τi = τ̂i θ (i = 0, 1, 2, 3).
Subcase (x : τˇ1 ) ∈ Γ̌ for any τˇ1 : Set Γ̂ = Γ̌, τ̂i = τ̌i (for i = 2, 3), and let τˆ0 andτˆ1 be fresh type variables. Then we can prove this subcase in the same way as theprevious one.

The proof of subject reduction relies on the following three lemmas.
Lemma 4 (value substitution) If Γ, x : τ  e : τ ; τ0 [; υ0 ] and Γ  v 0 : τ ; τ1 , thenΓ  e[x := v 0 ] : τ ; τ0 [; υ0 ].
The proof is routine, relying on Lemma 1.
Lemma 5 (weakening) If Γ  e : τ ; τ0 [; υ0 ], then Γ, Δ  e : τ ; τ0 [; υ0 ].
The proof is also routine.
Lemma 6 (abstraction) If Γ  e : τ1 ; τ0 and Γ  D00 [e] : τ2 ; τ0 are derivable, thenso is Γ, x : τ1  D00 [x] : τ2 ; τ0 for a fresh variable x.
Proof

A straightforward induction on the context D00 .

Proposition 7 (subject reduction) If Γ  e : τ ; τ0 is derivable and eΓ  e : τ ; τ0 is derivable.

e , then

Proof Because our typing rules are all compositional, we can assume without lossof generality that C 0 and C 1 in Figure 3 are just . We prove the proposition bycase analysis on the reduction. We show a couple of interesting cases.
Case βv : Suppose Γ  (λx. e)v 0 : τ ; τ0 . By inversion, we have Γ, x:τ  e : τ ; τ0 andΓ  v 0 : τ ; τ0 for some τ. Then the substitution lemma gives Γ  e[x := v 0 ] : τ ; τ0 .

641

Shifting the stage
Case d0 : We have the derivationΓ  d : T → τ/τ ; τ..
..
0
Γ  v : T ; τΓ  dv 0 : τ ; τ..
..
00
Γ  D [dv 0 ] : τ ; τΓ  {D00 [dv 0 ]} : τ ; τ0(17)where T = (τ → τ /τ1 ) → τ /τ and the derivation from dv 0 to D00 [dv 0 ] does notchange the answer type τ . Then we can use the weakening and abstraction lemmas
to derive..
..
0Γ  v : T ; τΓ, x : τ  x : τ ; τ..
..
Γ, x : τ  D00 [x] : τ ; τΓ, x : τ  {D00 [x]} : τ ; τ1
Γ  λx. {D00 [x]} : τ → τ /τ1 ; τ

Γ  v 0 (λx. {D00 [x]}) : τ ; τΓ  {v 0 (λx. {D00 [x]})} : τ ; τ0

(18)

The d case is similar.



1Corollary 8 (absence of scope extrusion) If []  e : τ ; τ0 is derivable and ethen e does not contain free variables.
Proof

By induction on the number of steps from e to e .

∗

e ,


To state the next two propositions, we deﬁne the future-stage type environmentΓ = x1 : υ1 , . . . , xn : υn  whenever Γ = x1 : υ1 , . . . , xn : υn .
Proposition 9 (progress) If Γ  e : τ ; τ is derivable, then there exists a term e
such that {e}
e .
Proof

Deﬁne a pre-redex pi to be an expression of the following form:
p0 ::= v 0 + v 0 | v 0 v 0 | ifz v 0 then e else e | {v 0 },p1 ::= sv 0 .

(19)

We slightly generalize the assumption to Γ  e : τ ; τ1 . By induction on its
derivation, either e is already a value (e = v 0 ), or e can be decomposed into acontext plugged with a pre-redex (e = C i [pi ]).
If e is already a value, then {e}e. Otherwise, the reduction required follows fromcase analysis on the typing derivation of the pre-redex. For example, if e = C 1 [sv 0 ],{C 1 [v 1 ]}. In the case where e = C 0 [dv 0 ],then v 0 must be of the form v 1 , so {e}
we choose between the d0 and d1 reduction rules by case analysis on C 0 .
The statement of this proposition diﬀers from the ordinary form in two respects.
First, we consider terms in the form {e} only, since a term like dv 0 by itself,
without an enclosing control delimiter, cannot be reduced. Second, we allow apotentially non-empty future-stage environment Γ, in order for the induction on

642

Y. Kameyama et al.

the typing derivation of e to go through. This strengthening corresponds to theworld declaration bl-ev in the accompanying Twelf code.
Propositions 7 and 9 together show that well-typed programs never go wrong in λ
1.
In particular, well-typed code generators never go wrong. Moreover, by the following
argument any code they generate never goes wrong either. If []  {e} : υ/υ0  ; τ0is derivable, then the program {e} either fails to terminate or evaluates to a codevalue v 1  such that []  v 1 : υ ; τ0 ; υ0 . The next proposition then assures us that v 1
is well-typed at the present stage.
Proposition 10 If Γ  v 1 : υ ; τ0 ; υ0 , then Γ  v 1 : υ ; υ0 .
Proof

By induction on the derivation of Γ  v 1 : υ ; τ0 ; υ0 .

As a corollary of the previous proposition, we obtain the following result, which
is similar to the binding-time correctness theorem of Davies (1996).
Corollary 11 If []  {e} : υ/υ0  ; τ0 and {e}form v 1  such that []  v 1 : υ ; υ0 .

∗v 0 for a value v 0 , then v 0 has theProof By subject reduction, []  v 0 : υ/υ0  ; τ0 . By inversion, we have v 0 = v 1 for some v 1 such that []  v 1 : υ ; τ0 ; υ0 . Then by the previous proposition,[]  v 1 : υ ; υ0 .
5 Larger examples of program specialization
In this section, we give larger examples to demonstrate the applicability of our
combination of side eﬀects and code generation. These examples show that ourapproach does not require the open-recursion style and its utility goes far beyond
dynamic programming and even let-insertion.
5.1 Longest common subsequence
The longest common subsequence is one of the textbook dynamic-programmingalgorithms in Swadi et al.’s (2005) benchmark. The problem is, given two sequences,
to ﬁnd (the length of) the longest subsequence of elements that occur in bothsequences in the same order, though not necessarily contiguously. The naive
implementation of the algorithm
let rec lcs x y (i,j) =if i = 0 || j = 0 then 0
else if x.(i) = y.(j) then 1 + lcs x y (i-1,j-1)
else max (lcs x y (i,j-1)) (lcs x y (i-1,j))takes two arrays x and y as input and computes the length of the longest common
subsequence of x[1..i] and y[1..j]. The input arrays can be emulated withfunctions in λ
1 . This program is very ineﬃcient. To make it eﬃcient, the programmer
only needs to rewrite it in the open-recursion style:let lcs x y self (i,j) =if i = 0 || j = 0 then 0
else if x.(i) = y.(j) then 1 + self (i-1,j-1)
else max (self (i,j-1)) (self (i-1,j))Shifting the stage

643

The rewriting keeps the algorithm clear. Applying the memoizing ﬁxpoint combinator y_memo_m (described in Sections 2.1 and 3.2) gives the eﬃcient implementation.
To specialize the algorithm when the lengths of the inputs are statically known(although their contents are not), we merely need to add brackets and escapes tothis lcs code:
let slcs x y self (i,j) =if i = 0 || j = 0 then .<0>.
else .<if (.~x).(i) = (.~y).(j) then 1 + .~(self (i-1,j-1))
else max .~(self (i,j-1)) .~(self (i-1,j))>.
Applying the memoizing staged ﬁxpoint combinator y_ms described in Sections 2.4
and 3.4.<fun x y -> .~(top_fn (fun _ -> y_ms (slcs .<x>. .<y>.) (3,4)))>.
produces the ideal code.<fun x_1 -> fun y_2 ->let t_3 = 0 in let t_4 = 0 in let t_5 = 0 in
let t_6 = 0 in let t_7 = 0 in let t_8 = 0 in
let t_9 = if x_1.(1) = y_2.(1) then 1 + t_8 else max t_7 t_6 in
let t_10 = if x_1.(1) = y_2.(2) then 1 + t_6 else max t_9 t_5 in
let t_11 = if x_1.(1) = y_2.(3) then 1 + t_5 else max t_10 t_4 in
let t_12 = if x_1.(1) = y_2.(4) then 1 + t_4 else max t_11 t_3 in...
let t_19 = if x_1.(3) = y_2.(1) then 1 + t_13 else max t_18 t_14 in
let t_20 = if x_1.(3) = y_2.(2) then 1 + t_14 else max t_19 t_15 in
let t_21 = if x_1.(3) = y_2.(3) then 1 + t_15 else max t_20 t_16 in
if x_1.(3) = y_2.(4) then 1 + t_16 else max t_21 t_17>.
The complexity is the optimal O(n × m), where n and m are the lengths of the inputs.
For comparison, to use Swadi et al.’s (2006) dynamic-programming specialization
framework, Swadi et al. (2005) have to write the staged lcs code in a less direct
monadic style:let lcs_mks x y self (i,j) =if i = 0 || j = 0 then ret .<0>.
else bind (self (i-1,j-1)) (fun r1 ->bind (self (i ,j-1)) (fun r2 ->bind (self (i-1,j )) (fun r3 ->ret .<if (.~x).(i) = (.~y).(j) then 1 + .~r1
else max .~r2 .~r3>.)))
Other dynamic-programming algorithms can be specialized in the same way. For
example, to compute the product of a sequence of matrices while minimizing thenumber of multiplications, we have specialized the minimization when the numberof matrices is known (although their dimensions and contents are not).

644

Y. Kameyama et al.
5.2 Gaussian elimination

Let-insertion is useful not just for dynamic programming. Carette and Kiselyov(2011) implemented Gaussian elimination as a code generator that produces aroutine specialized to a particular choice of numeric representation and matrix
pivoting. Among the many parameters of this code generator is whether to computethe determinant. If the determinant is desired, the generated code should include
determinant accumulation, and, more importantly, let-bindings for mutable cells inwhich to accumulate the determinant’s sign and magnitude. Carette and Kiselyov(2011) achieved this let-insertion by writing the entire generator in monadic style.
We brieﬂy describe writing the generator for a family of Gaussian eliminations in
our approach, highlighting the modularity and the close similarity of the generator
to the textbook, unstaged code (written, for example, by an expert in linear algebra).
We start with the unstaged OCaml code for Gaussian elimination, whose fragment
is shown below. (See ge_unstaged.ml in the accompanying code for the complete
implementation and tests.) The code implements the standard textbook pseudo-code
description of the algorithm in the most straightforward way. In the loop, we search
for the pivot, exchange the current row and column with the pivot’s row and column
to bring the pivot to the matrix diagonal, and then perform the row reduction.
Swapping rows or columns in a matrix changes the sign of its determinant; we keep
track of the sign in the mutable cell det_sign.
let ge = fun a_orig ->let r = ref 0 in(* current row index*)
let c = ref 0 in(* current column index *)let a = Array.copy (a_orig.arr) in (* save input matrix A *)let m = a_orig.m in(* the number of cols*)
let n = a_orig.n in(* the number of rows*)
let det_sign = ref 1 in(* Accumulate sign and *)let det_magn = ref 1.0 in(*
magnitude of det*)
while !c < m && !r < n do
let pivot = find_pivot_row a (n,m) !r !c in
let piv_val = (match pivot with| Some ((piv_r, piv_c),piv_val) ->if piv_c <> !c then begin
swap_cols a (n,m) !c piv_c;
det_sign := - !det_sign
end;
if piv_r <> !r then ...;
Some piv_val| None -> None) in(* do the row-reduction over the (r,c)-(n,m) block *)...
The following is our generator for Gaussian elimination, which generates theunstaged code above, among many other variants. (The complete generator code isShifting the stage

645

in the ﬁle ge_gen.ml.)
let gge outchoice = .<fun a_orig ->let r = ref 0 in(* current row index*)
let c = ref 0 in(* current column index *)let a = Array.copy (a_orig.arr) in (* save input matrix A *)let m = a_orig.m in(* the number of cols*)
let n = a_orig.n in(* the number of rows*).~(let p = new_prompt () in
push_prompt p (fun () ->let env = {env_p = p; env_a = .<a>.; env_n = .<n>.;env_m = .<m>.; env_r = .<r>.;env_pivot = gfind_pivot_row;
env_det= make_det_nodet p} inlet env = outchoice.oc_init env in.<beginwhile !c < m && !r < n do
let pivot = .~(env.env_pivot env .<!r>. .<!c>.) in
let piv_val = (match pivot with| Some ((piv_r, piv_c),piv_val) ->if piv_c <> !c then begin.~(gswap_cols env .<!c>. .<piv_c>.);.~(env.env_det.det_flip_sign)end;
if piv_r <> !r then ...;
Some piv_val| None -> None) in(* do the row-reduction over the (r,c)-(n,m) block *)... >.
The generator is strikingly similar to the unstaged code; in fact, it was writtenby wrapping the unstaged code into a pair of brackets and placing a few escapesat places where inlining (e.g., of the row swapping) or variant implementations weredesired. The main diﬀerence between the generator and the unstaged code is thefactoring-out of pivoting and determinant computations. The unstaged code usedrow pivoting, implemented by a function find_pivot_row. The generator inlines theresult of the pivoting generator env.env_pivot, which defaults to the row-pivoting
generator but can be changed to a full-pivoting generator, for example. Textbooks
on Gaussian elimination describe several pivoting strategies and conditions for using
them. The user speciﬁes the desired variant of Gaussian elimination by passing gge
a value of the data type
type (’c,’result,’out) outchoice ={oc_init : (’c,’result) env -> (’c,’result) env;
oc_fin : (’c,’result) env -> (’c,’out) code;}

646

Y. Kameyama et al.

that sets the generation environment env and speciﬁes the generation of the
ﬁnal result. The generator gge may produce code that returns the complete LU
decomposition, just the U factor, the U factor and the determinant, the U factor
and the rank, etc. (The result type of the generated code varies accordingly.) Caretteand Kiselyov (2011) thoroughly discuss various aspects and parametrizations ofGaussian elimination.
Of interest to us here is how the determinant is computed. That computationis spread throughout the Gaussian elimination code: deﬁning mutable cells to be
used; ﬂipping the sign upon an exchange of rows or columns; and accumulating
the magnitude during row reductions. When we converted the unstaged code
to the generator, we abstracted determinant computations away, replacing, forexample, det_sign := - !det_sign in the unstaged code with the invocationof the corresponding generator env.env_det.det_flip_sign. The generators forﬂipping the sign etc. are collected in a data structure ’c det:type ’c det = {det_computes : bool;
det_flip_sign : (’c,unit) code;...}
The ﬁeld env.env_det of the generation environment holds an instance of ’c det
to be used when generating a particular version of Gaussian elimination.
There are two instances of the ’c det data structure. One generates no determinant computation:
let make_det_nodet p ={det_computes = false;
det_flip_sign = .<()>.; ...}The generator det_flip_sign generates () then, eﬀectively no code. More interesting is the instance that does generate determinant computation:
let genlet p e =shift p (fun k -> .<let t = .~e in .~(k .<t>.)>.);;
let make_det_compute_det p =let det_sign = genlet p .<ref 1>. in
let det_magn = genlet p .<ref 1.0>. in{det_computes = true;
det_flip_sign = .<.~det_sign := - !(.~det_sign)>.;...}Here, det_flip_sign generates the code that we have abstracted away from theunstaged original. To use that code however, we have to ﬁrst generate deﬁnitionsof the variables det_sign and det_magn. The genlet combinator lets us generate
let-bindings for these mutable cells at the place indicated at push_prompt (or, reset).
In our case that place is after all the other let-bindings at the beginning of theGaussian elimination code.
The determinant aspect is an example of the modularity and expressivity that isrequired for real-world generators and is aﬀorded in our approach. We abstracted

Shifting the stage

647

not only expressions (such as ﬂipping the sign) but also deﬁnitions of (private)
variables used within the abstracted expressions. The abstractions carry no run-time
penalty for the generated code. Our approach, despite its restriction, does allow
writing useful modular generators.
5.3 Markov models
Delimited control is not just useful for let-insertion. Taha8 used MetaOCaml to
specialize the execution of, and thus speed up the search for, Markov models of agiven form – whose number of states is known and many transition probabilities are
known to be zero. The Markov model is expressed using mutable state to initialize
and multiply matrices.
Whereas naively adding mutable state to MetaOCaml risks scope extrusion, oursystem allows this use of mutable state and assures it safe because all of the matrix
operations take place in the same generated scope. Our MetaOCaml implementation
relying on delimited control operators can be found in the ﬁle band_markov_lc.mlof the accompanying code.
6 CPS translation
In this section, we deﬁne a CPS translation for λ
1 . The translation maps terms
toamultilevelcalculus
without
control eﬀects. We show thatand types from λ1
the translation simulates λ1 – in other words, it preserves operational semantics.
We can thus understand the reduction semantics in Section 3 and the type system
in Section 4 in terms of pure staging: For example, the d0 and d1 reductions inFigure 3 correspond to the translation d in Figure 8; and the types of λ
1 pullback those of the target language. The translation also lets us implement λ
1 byimplementing the target language.
The target language of our CPS translation is λ
1 without present-stage control
eﬀects. In other words, the terms of the target are as in λ
1 but without the control
operators d and { } at the present stage. The type system of the target is as in λ
1 butwith all present-stage answer types removed from types and judgments, for instance,Γ  e : υ ;; υ0 for a future-stage judgment. We equate any level-0 expression e ofcode type with se, and any level-1 expression e with se.9 These equations bringour treatment of level switching closer to that in the two-level λ-calculus (Nielson

89

http://metaocaml.org/examples/band-markov.ml
The ﬁrst equation e = se is crucial in Equation (43). It forces us to turn the s reduction in
Figure 3 into the second equation e = se in order to avoid the inﬁnite loop s33 = s3.
Besides, to prove Proposition 15, we need to reduce the target term sv 1  in zero or more steps to v 1¯ sv 1  in Equation (41) may put sv 1  under
everywhere – even under a present-stage λ, because k̄ @a present-stage λ. For example, we need to translate the second step in{s(let x = 0 in 3) + s(dλf. . . . )}{s3 + s(dλf. . . . )}{3 + s(dλf. . . . )}sd0 {let f = λy. {3 + sy} in . . . }βv

to zero or more steps from s3 to 3 under a present-stage λ (namely λy, essentially).

648

Y. Kameyama et al.

uses of the reduction (20) to

Fig. 7. An example of applying the one-pass CPS translation to perform let-insertion.

& Nielson, 1988). We also consider sv 0 (including sx) a value. The reductions of
the target are• the reductions of λ
1 (Figure 3) restricted to these terms,• minus the now-superﬂuous s reduction,• plus the reduction(λx. e) v 0 → e[x := v 0 ]where x occurs at most once in e(20)

everywhere – even under a present-stage λ. This additional reduction does not
aﬀect the set of terminating terms.
Since the sets of values, frames, delimited contexts, and contexts (Figure 2) areinvariant up to the equations e = se and e = se just introduced, these reductions
are well-deﬁned over equivalence classes of target terms.
Before presenting our CPS translation in detail, we ﬁrst show an example of it atwork. Take the source program (s(dλf. let x = 1 + 1 in s(fx)), s(dλf. let x = 1 + 1 in s(fx)))  (21)in λ
1 . This program performs two let-insertions in a row. When placed inside a
top-level reset, it evaluates tolet x = 1 + 1 in let y = 1 + 1 in (x, y)

(22)

as speciﬁed in Figure 3. As detailed in Figure 7, our CPS translation maps the649

Shifting the stage
program (21) to a target term that reduces to
let z = λx. s((λx . x )(let z = λy. s((λx . x )((x, y)
)) in sz(1 + 1)
)) in sz(1 + 1)

(23)

using the reduction (20). This term does not use any delimited control operators,
but rather uses ordinary abstractions over x and y to represent the continuationsof the two d-applications in the source program (21). This term eventually reduces
to the value (22) just as the source program does.
Figure 8 shows the formal rules of our CPS translation. It is a one-pass translation(that is, it produces no administrative redexes), which makes it simpler to state andprove that it simulates the source language. Like Danvy and Filinski (1992), we
express it in a higher-order metalanguage and regard it as the result of analyzing
the binding times in a CPS translation that does produce administrative redexes.
¯ to denote variables, abstraction, and application at the level
We write x̄, λ̄, and @of this metalanguage.
Figure 8 deﬁnes the translation e0 of a present-stage expression e and thetranslation e1 of a future-stage expression e. Given a present-stage value v 0 , theﬁgure also deﬁnes its value translation v 0 , which is itself a value in the target
language. For example, λx. e is a target term of the form λx. λk. . . . where x and k
are fresh variable names; in particular, k is a dynamic continuation. In contrast,e0 and e1 are meta-level functions that map a term-to-term function k̄ (a static
continuation) to a term. More precisely,• the meta-level function e0 returns a present-stage term when given a metalevel function mapping a present-stage value to a present-stage term;• the meta-level function e1 returns a present-stage term when given a metalevel function mapping a future-stage value to a present-stage term.
The deﬁnition of e0 uses the static continuation ↑k (pronounced “reﬂect k”) andthe dynamic continuation ↓k̄ (pronounced “reify k̄”). If we ignore the diﬀerence ofobject language and metalanguage, then reﬂection and reiﬁcation do not change
the continuation at all. We make the distinction and use the metalanguage level toavoid producing administrative redexes and simplify the proof of simulation.
The output of the translation is in tail form except in {e}0 , d, and λx. e1 .
¯ λ̄z̄. k̄ @¯ λx. z̄ in tail form, then occurrences
If we naively deﬁne λx. e1 = λ̄k̄. e1 @of x in e would translate to unbound future-stage variables. The CPS translation
thus relies on our treating future-stage binders as present-stage control delimiters.
To make this description precise and to show that the translation preserves types∗in λ
1 , we deﬁne a CPS translation τ of present-stage types τ.
int∗ = int

υ/υ0 ∗ = υ/υ0 (τ1 → τ2 /τ3 )∗ = τ∗1 → (τ∗2 → τ∗3 ) → τ∗3(τ1 , τ2 )∗ = (τ∗1 , τ∗2 )α∗ = α(24)

650

Y. Kameyama et al.

Fig. 8. One-pass CPS translation for λ
1.

(Future-stage types do not change.) We also translate environments:[]∗ = []

(Γ, x : τ)∗ = Γ∗ , x : τ∗(Γ, x : υ)∗ = Γ∗ , x : υ

(25)

Proposition 12 (translation preserves typing) We have the following three properties.
(1) If Γ  v 0 : τ ; τ0 , then Γ∗  v 0  : τ∗ .
(2) Suppose Γ  e : τ ; τ0 . Let Φ be a type environment in the target language
and k̄ be a meta-level function such that, for any type environment Δ and¯ t : τ∗ . Thenterm t of the target language, if Γ∗ , Δ  t : τ∗ , then Γ∗ , Δ, Φ  k̄ @0∗∗¯
Γ , Φ  e0 @ k̄ : τ0 .

651

Shifting the stage(3) Suppose Γ  e : υ ; τ0 ; υ0 . Let Φ be a type environment in the target language
and k̄ be a meta-level function such that, for any type environment Δ and¯ t : τ∗ .
term t of the target language, if Γ∗ , Δ  t : υ ;; υ0 then Γ∗ , Δ, Φ  k̄ @0∗∗¯
Then Γ , Φ  e1 @ k̄ : τ0 .
If we ignore the diﬀerence of object language and metalanguage, the proposition canbe stated in a much simpler way. For instance, part 2 is stated as: if Γ  e : τ ; τ0 ,then Γ∗  e0 : (τ∗ → τ∗0 ) → τ∗0 . In our one-pass CPS translation, k̄ represents ameta-level function that (roughly) has type τ∗ → τ∗0 , and the assumption on k̄ in the
proposition is a precise statement for this intuition.
Proof The deﬁnitions in Figure 8 are mutually inductive, and v 0 0 is deﬁned interms of v 0 . Accordingly, we proceed by mutual induction on typing derivations,allowing part 2 to appeal to part 1 in the case where e = v 0 .
For part 1, the interesting case is when v 0 = λx. e. By inversion, let Γ, x : τ 
e : τ ; τ1 . Recall from Figure 8 that the translation in this case binds the
dynamic continuation variable k. Note that ↑k is a meta-level function such that¯ t : τ∗ whenever Γ∗ , x : τ∗ , Δ  t : τ∗ . By the inductionΓ∗ , x : τ∗ , Δ, k : τ∗ → τ∗1  ↑k @1
¯ ↑k : τ∗ .
hypothesis (choosing Φ = k : τ∗ → τ∗1 ), we have Γ∗ , x : τ∗ , k : τ∗ → τ∗1  e0 @
1
∗


∗
¯
¯
Hence, Γ  λx. λk. e0 @ ↑k : (τ → τ /τ1 ) , in which λx. λk. e0 @ ↑k is λx. e bydeﬁnition, as desired.
For part 2, the interesting cases are as follows:
Case e = v 0 : By the induction hypothesis for part 1, we have Γ∗  v 0  : τ∗ . Thus,¯ v 0  : τ∗ , in which k̄ @¯ v 0  is v 0 0 @¯ k̄by the assumption on k̄, we have Γ∗ , Φ  k̄ @0
by deﬁnition, as desired.
Case e = e1 e2 : By inversion, let Γ  e1 : τ → τ/τ0 ; τ0 and Γ  e2 : τ ; τ0 and k̄¯ t : τ∗ whenever Γ∗ , Δ  t : τ∗ . By
be a meta-level function such that Γ∗ , Δ, Φ  k̄ @0
the deﬁnition of e1 e2 0 and the induction hypothesis for e1 (choosing the same Φ),
we need only show
¯ λ̄x̄. t1 x̄↓k̄ : τ∗(26)
Γ∗ , Δ1 , Φ  e2 0 @0given Γ∗ , Δ1  t1 : (τ → τ/τ0 )∗ . By the induction hypothesis for e2 (choosing Φ to
be Δ1 , Φ), we need only showΓ∗ , Δ2 , Δ1 , Φ  t1 t2 ↓k̄ : τ∗0(27)¯ x, we choose Δ
given Γ∗ , Δ2  t2 : τ∗ . Finally, given that ↓k̄ is deﬁned to be λx. k̄ @∗to be x : τ , Δ2 , Δ1 and t to be x.
Case e = e : By inversion, let Γ  e : υ ; τ0 ; υ0 and k̄ be a meta-level function¯ t : τ∗ whenever Γ∗ , Δ  t : υ/υ0 . Then Γ∗ , Δ, Φ  k̄ @¯ t : τ∗such that Γ∗ , Δ, Φ  k̄ @00∗whenever Γ , Δ  t : υ ;; υ0 . By the induction hypothesis for part 3 (choosing the¯ λ̄x̄. k̄ @¯ x̄ : τ∗ , in which e 1 @¯ λ̄x̄. k̄ @¯ x̄ issame Φ), we have Γ∗ , Φ  e 1 @0
¯ k̄ by deﬁnition, as desired.
e 0 @For part 3, the interesting cases are as follows:
Case e = x: By inversion, let Γ  x : υ ; τ0 ; υ0 and k̄ be a meta-level function¯ t : τ∗ whenever Γ∗ , Δ  t : υ ;; υ0 . Then (x : υ) ∈ Γ, sosuch that Γ∗ , Δ, Φ  k̄ @0∗∗
(x : υ) ∈ Γ and so Γ  x : υ ;; υ0 . We thus choose Δ to be [] and t to be x and¯ x : τ∗ , in which k̄ @¯ x is x1 @¯ k̄ by deﬁnition, as desired.
conclude Γ∗ , Φ  k̄ @0

652

Y. Kameyama et al.

Case e = λx. e where e is not a value: By inversion, let Γ, x : υ  e :¯ t : τ∗
υ ; υ  /υ1  ; υ1 and k̄ be a meta-level function such that Γ∗ , Δ, Φ  k̄ @0whenever Γ∗ , Δ  t : υ → υ  /υ1 ;; υ0 . By the induction hypothesis (choosing thesame Φ), because Γ∗ , x : υ, Δ, Φ  t : υ  /υ1  whenever Γ∗ , x : υ, Δ  t : υ  ;; υ1 ,¯ λ̄z̄. z̄ : υ  /υ1 . So, Γ∗ , Φ  λx. s(e 1 @¯ λ̄z̄. z̄) :we have Γ∗ , x : υ, Φ  e 1 @
(υ → υ /υ1 )/υ0 . Finally, choose Δ = z : (υ → υ /υ1 )/υ0  and t = sz to show that¯ sz : (υ → υ  /υ1 )/υ0  → τ∗ .
Γ∗ , Φ  λz. k̄ @0Case e = {e }: By inversion, let Γ  e : υ ; τ0 ; υ and k̄ be a meta-level function¯ t : τ∗ whenever Γ∗ , Δ  t : υ ;; υ0 . Then Γ∗ , Δ, Φ  k̄ @¯ {t} : τ∗such that Γ∗ , Δ, Φ  k̄ @00∗whenever Γ , Δ  t : υ ;; υ. By the induction hypothesis (choosing the same Φ), we¯ λ̄x̄. k̄ @¯ {x̄} : τ∗ , in which e 1 @¯ λ̄x̄. k̄ @¯ {x̄} is e1 @¯ k̄ byhave Γ∗ , Φ  e 1 @0
deﬁnition, as desired.


We move on to show that our translation also preserves the dynamic semanticsof λ
1 . To do so, we need a crucial lemma that relates the translations of a delimited
context Dij and of it plugged with a term e. Intuitively, this lemma says that thetranslation of Dij [e] puts e “in control” by applying the translation of e to thetranslation of Dij [x]. After all, Dij is a delimited evaluation context. The subsequent
corollary then extends the lemma from delimited contexts to all contexts C i .
Lemma 13 Let k̄ be a meta-function from level-i target values to level-0 target
terms, and let x be a fresh object variable at level j (so x = x in case j = 0). Then¯ k̄ = ej @¯ λ̄z̄. (Dij [x]i @¯ k̄)[x := z̄].
Dij [e]i @(28)(That is, the target terms on the two sides are related by canceling   against s as
described at the beginning of this section.)
Proof
By induction and case analysis on Dij .
Case : By deﬁnition of xi , then β and η reductions at the metalanguage level.
Case Di1 [s]: We have¯ k̄
LHS = Di1 [se]i @¯ λ̄z̄. (Di1 [x]i @¯ k̄)[x := z̄]= se1 @by induction hypothesis¯ λ̄z̄. (D [x]i @¯ k̄)[x := sz̄]= e0 @by deﬁnition of se1 ,

i1

(29)

so
¯ λ̄z̄. (Di1 [sx]i @¯ k̄)[x := z̄]RHS = e0 @¯ λ̄z̄. (Di1 [x]i @¯ k̄)[x := sz̄]= e0 @by Equation (29) with e = x,and deﬁnition of x0

= LHS

(30)

by Equation (29).

Cases Di0 [], Di1 [{}] and Di0 [ifz  then e1 else e2 ] are similar.
Case Di0 [v 0 ]: We have¯ k̄
LHS = Di0 [v 0 e]i @¯ λ̄z̄. (Di0 [x]i @¯ k̄)[x := z̄]= v 0 e0 @¯ λ̄z̄. v 0 z̄(λx. Di0 [x]i @¯ k̄)= e0 @by induction hypothesis
by def. of v e0 and v 0 ,
0

0

(31)

653

Shifting the stageso¯ λ̄z̄. (Di0 [v 0 x]i @¯ k̄)[x := z̄]RHS = e0 @¯ λ̄z̄. v 0 z̄(λx. Di0 [x]i @¯ k̄) by Equation (31) with e = x,= e0 @and deﬁnition of x0
= LHS

(32)

by Equation (31).

Cases Di0 [v 0 + ], Di0 [(v 0 , )], Di1 [v 1 + ], Di1 [v 1 ], Di1 [(v 1 , )], and Di1 [ifz v 1 thenv11 else ] are similar.
Case Di0 [e2 ]: We have¯ k̄
LHS = Di0 [ee2 ]i @¯ λ̄z̄. (Di0 [x]i @¯ k̄)[x := z̄]= ee2 0 @¯ λ̄ȳ. e2 0 @¯ λ̄z̄. ȳz̄(λx. Di0 [x]i @¯ k̄)= e0 @¯ λ̄ȳ. (Di0 [fe2 ]i @¯ k̄)[f := ȳ]= e0 @by induction hypothesis
by deﬁnition of ee2 0
by Equation (31) with v 0 = f= RHS.
(33)
Cases Di0 [ + e2 ], Di0 [(, e2 )], Di1 [ + e2 ], Di1 [e2 ], Di1 [(, e2 )], Di1 [ifz v 1 then
 else e2 ], and Di1 [ifz  then e1 else e2 ] are similar.
Corollary 14 Let x be an object variable at level 0 that does not occur in expressions
C 0 [{e}] and C 1 [λy. e] mentioned below.
If C 0 is a context and e is a present-stage expression, then¯ λ̄z̄. z̄ = (C 0 [{x}]0 @¯ λ̄z̄. z̄)[x := e0 @¯ λ̄z̄. z̄],
C 0 [{e}]0 @(34)¯ λ̄z̄. z̄ is equal to the result of plugging x into
in which the target term C [{x}]0 @some evaluation context.
If C 1 is a context and e is a future-stage expression that is not a value, then0¯ λ̄z̄. z̄ = (C 1 [λy. sx]0 @¯ λ̄z̄. z̄)[x := e1 @¯ λ̄z̄. z̄],C 1 [λy. e]0 @(35)¯ λ̄z̄. z̄ is equal to the result of plugging x
in which the target term C 1 [λy. sx]0 @into some evaluation context.
Proof

By mutual induction on C 0 and C 1 , using Lemma 13 at each step.

Proposition 15 (reduction preservation) Let e and e be present-stage expressions. If¯ λ̄z̄. z̄ ∗ e 0 @¯ λ̄z̄. z̄. (Moreover, e0 @¯ λ̄z̄. z̄ = e 0 @¯ λ̄z̄. z̄
{e}{e }, then e0 @
1
1

1 1
only if e = C [sv ] and e = C [v ].)Proof By case analysis on .
{C 0 [n]} where n = n1 +̇n2 , and we need to show
Case +: We have {C 0 [n1 + n2 ]}
0
+
0
¯
¯
C [n]0 @ λ̄z̄. z̄. We perform case analysis on C 0 :C [n1 + n2 ]0 @ λ̄z̄. z̄¯ λ̄z̄. z̄ + D00 [n1 +̇n2 ]0 @¯• If C 0 = D00 , then what we need is D00 [n1 + n2 ]0 @λ̄z̄. z̄.
• If C 0 = C 0 [{D00 }], then the ﬁrst half of Corollary 14 gives us an evaluation¯ λ̄z̄. z̄) suchcontext C in the target language (namely, C[x] = C 0 [{x}]0 @
00
+
00
¯
¯ λ̄z̄. z̄].
C[D [n1 +̇n2 ]0 @that what we need is C[D [n1 + n2 ]0 @ λ̄z̄. z̄]654

Y. Kameyama et al.
¯ λ̄z̄. z̄ + D00 [n1 +̇n2 ]0 @¯ λ̄z̄. z̄ as
So we just need to show D00 [n1 + n2 ]0 @in the previous case.
• If C 0 = C 1 [λx. D10 ], then the second half of Corollary 14 gives us an evaluation¯ λ̄z̄. z̄) suchcontext C in the target language (namely, C[x] = C 1 [λy. sx]0 @10+
10¯ λ̄z̄. z̄]¯ λ̄z̄. z̄].
C[D [n1 +̇n2 ]1 @that what we need is C[D [n1 +n2 ]1 @
10
+
10
¯
¯ λ̄z̄. z̄.
D [n1 +̇n2 ]1 @So we just need to show D [n1 + n2 ]1 @ λ̄z̄. z̄To sum up this case analysis, we just need to show
¯ k̄  + Di0 [n1 +̇n2 ]i @¯ k̄ 
Di0 [n1 + n2 ]i @(36)

where either i = 0 and k̄  = λ̄z̄. z̄ or i = 1 and k̄  = λ̄z̄. z̄. We apply Lemma 13 to¯ k̄  )[x := z̄]:both sides, letting k̄ = λ̄z̄. (Di0 [x]i @¯ k̄ = ↓k̄(n1 + n2 ) + ↓k̄(n1 +̇n2 ) β k̄ @¯ (n1 +̇n2 ) = n1 +̇n2 0 @¯ k̄. (37)
n1 + n2 0 @v

The ﬁx, fst, and snd cases are similar.
Case βv : Again by Corollary 14 and Lemma 13, we just need to show¯ k̄
(λx. e) v 0 0 @

∗

¯ k̄.
e[x := v 0 ]0 @(38)

We have¯ k̄ = (λx. λk. e0 @¯ ↑k)v 0 ↓k̄(λx. e) v 0 0 @20¯βv (e0 @ ↑↓k̄)[x := v ].

(39)¯ k̄)[x := v ] using the reduction (20) zero or more
The last term reduces to (e0 @times, because our translation always applies the static continuation to a value, andthe static continuation always uses its argument at most once. The two ifz cases use¯ ↑↓k̄ and e2 0 @¯ ↑↓k̄ to e1 0 @¯ k̄ and e2 0 @¯ k̄.
the same reasoning to reduce e1 0 @Case {}: Again we use Corollary 14 and Lemma 13:0¯ k̄ = ↓k̄v 0 
{v 0 }0 @0¯ 0¯βv k̄ @ v  = v 0 @ k̄.

(40)

Case s: Again we use Corollary 14 and Lemma 13 (letting j be 1 rather than 0
this time):¯ v 1 = v 1  @¯ k̄.
¯ k̄ = k̄ @¯ sv 1  = k̄ @(41)sv 1 1 @If the source reduction turns a future-stage λ-abstraction into a value, then one
βv -reduction per future-stage λ-abstraction is needed to match the CPS translationof the value.
¯ λ̄z̄. z̄)[x := z̄], we compute
Case d0 : Letting k̄ = λ̄z̄. (D00 [x]0 @¯ λ̄z̄. z̄ = dv 0 ↓k̄D00 [dv 0 ]0 @

2
0

  
βv v (λx. λk . (λx . k x )((↓k̄)x))(λx. x)
0

  
¯

v (λx. λk . (λx . k x )(k̄ @ x))(λx. x)¯ λ̄z̄. z̄.
= v 0 (λx. {D00 [x]})0 @(42)¯ λ̄z̄. z̄)[x := z̄], we compute
Case d1 : Letting k̄ = λ̄z̄. (D10 [x]0 @¯ λ̄z̄. z̄ = dv 0 ↓k̄
D10 [dv 0 ]1 @

2
0

  
βv v (λx. λk . (λx . k x )((↓k̄)x))(λx. x)
0

  
¯

v (λx. λk . (λx . k x )(k̄ @ x))(λx. x)¯ λ̄z̄. z̄= v 0 (λx. {D10 [x]})0 @(43)¯ λ̄z̄. z̄.
= s(v 0 (λx. {D10 [x]}))1 @The last equality is why we equate se with e in the target language.

Shifting the stage655

Fig. 9. Values and contexts of λ . We write += to add alternatives to a preceding BNF
rule.

Fig. 10. Operational semantics: small-step reduction ee particular to λ . Other reductionii
rules are the same as those in λ1 . Here   and s stand for i levels of brackets and escapes;i > 1.

7 Multilevel calculus with control eﬀects
with an arbitrary number ofThis section generalizes λ
1 to the full language λlevels, removing the restriction on nesting of brackets and escapes and making thelanguage, its type system in particular, more uniform. The generalization only aﬀects
the number of levels for expressions; the syntax of expressions remains the same, see
Section 3 and Figure 1. Level 0 still refers to the present stage, at which reductions
may occur. The language λ permits more than one future-stage level by allowing
brackets and escapes to nest. Brackets increase the level of the expression and escapedecreases it. The language λ thus can express not only code generators but also
generators of code generators, and so on. The level superscripts are now arbitrary
natural numbers. Figure 9 deﬁnes values and contexts of λ , generalizing those ofλ
1 to multiple future levels.
For example, according to the deﬁnition of delimited contexts in Figure 9,  isa D22 , so s is a D21 and so ss is a D20 . Similarly, because  is a D00 as well asa D11 , we have that  is a D01 as well as a D12 . Putting these derivations together,
the parse tree below shows that λx. λy. ss is an evaluation context C 0 :D00 ::= 
D01 ::=  D11 ::= D22 ::= 112
C ::=  D ::=  D21 ::= s
C 2 ::= λx. D20 ::= ss
0
C ::= λx. λy. ss

(44)

The operational semantics of λ is, with one exception, identical to that of λ
1.
After all, in both calculi, reductions are only performed at level 0. The sole exceptioniis to generalize the d1 reduction of λ
1 to the d reduction as shown in Figure 10.

656

Y. Kameyama et al.

Fig. 11. The type system of λ and selected typing rules. The notation τn is explained in the
text.

The type system of λ is essentially the same as that of λ
1 ; Figure 11 shows the
crucial parts. Terms like 42 with nested brackets are now allowed and inhabit
types with nested brackets like int / int/ int. In type environments, the notation
x : τi (or just x : τ if i = 0) associates the level-i variable x with the type τ. We
generalize answer types to sequences of types Ti = τ0 , . . . , τi ; each type τj in asequence tracks the control eﬀects that may occur at the level j. A typing judgmentΓ  e : τ ; Ti for a level-i expression e includes the answer-type sequence Ti . The
typing rules of λ simply generalize those of λ
1 ; Figure 11 shows a sample. The
type system of λ is more uniform however: There is only one form of judgment,
which works for the present and the future stages. We no longer have to employ
the judgment schema Γ  e : τ ; τ0 [; υ0 ]; strictly speaking, λ has roughly half thenumber of typing rules compared to λ
1.
The rule for future-stage abstraction is the only one with nontrivial generalization,
giving more insight into our restriction of eﬀects within the closest future-stage
binder. (This restriction is similar to that in the region-based type-and-eﬀect system(Talpin & Jouvelot, 1992).) Recall that, to prevent scope extrusion, we put an implicit
present-stage reset under each future-stage binder. In the case of many future stages,
we place many implicit resets, for levels 0 through i − 1 (inclusive), under each level-i
binder. For example, the body e of a level-1 abstraction is implicitly delimited ass{e}; the body e of a level-2 abstraction is implicitly delimited as s{s{e}}.
These implicit resets explain the answer-type sequence for the body of the level-i λ. In
the ﬁrst rule in Figure 11, the sequence is written τ /τi i , τ /τi i−1 , . . . , τ /τi 1 , τiusing the notation τi inductively deﬁned as follows:τ1 = τ,τi+1 = τi /τi .

(45)

For example, at level 2, we can conclude Γ  (λx. e) : τ → τ /τ2 ; τ0 , τ1 , τ2 provided
that Γ, x : τ  e : τ ; τ /τ2 /τ /τ2 , τ /τ2 , τ2 .
The formal properties of the multilevel calculus λ straightforwardly generalize
those of λ
1 stated in Sections 4.2 and 6 – and so do their proofs. To be certain,
we have mechanized the type soundness proofs for λ in Twelf. Therefore, weomit the proofs, referring the reader for details to the well-commented code
circle-shift-n.elf accompanying the paper.

Shifting the stage657

8 Related work
Our work draws from two strands of research on partial evaluation and code
generation, namely, side eﬀects and custom generators.
8.1 Side eﬀects in code generators
There is a long tradition of using CPS to write program generators such as patternmatch compilers. Danvy and Filinski (1990, 1992) ﬁrst applied delimited control toprogram generation: They showed how to fuse a CPS translation and administrative
reductions into one pass by writing the translation either in CPS or using shift
and reset. Similarly in partial-evaluation research, Bondorf (1992) showed how to
improve binding times by writing the specializer rather than source programs in CPS.
This move helps because the specializer is a ﬁxed program that a programminglanguage expert can write and prove correct once and for all, whereas many source
programs are written and fed to the specializer over time, by domain experts who
may be unfamiliar with CPS. (Dussart and Thiemann (1996) in their Section 1.1
also criticized the approach of expanding source programs monadically.)
Danvy and Filinski’s (1990, 1992) CPS translations and Bondorf’s (1992) specializer are sound, in the sense that their continuations are well-behaved and do not leadto scope extrusion. Given that these code generators were ﬁxed, it was sensible for
their authors to prove their soundness as part of speciﬁc proofs of their correctness
rather than as a corollary of some type system that assures that every well-typed
generator is sound. Lawall and Danvy (1994) did not rely on such a type systemeither when they used shift and reset to reduce Bondorf’s specializer to direct
style. Our type system accepts these generators not as they are but reformulated as
combinators (Thiemann, 1999). It thus assures them sound; in particular, it is theﬁrst to accept Danvy and Filinski’s (1990, 1992) and Lawall and Danvy’s (1994)
uses of delimited control.
In contrast, we are not aware of any sound type system for code generators that
accepts Sumii and Kobayashi’s (2001) specializer, which performs let-insertion using
mutable state rather than delimited control to speed up specialization, or Dussart andThiemann’s (1996) specializer, which uses ﬁrst-class mutable state (Morrisett, 1993)
as well as ﬁrst-class continuations. For both of those specializers, code generation ispreceded by a sophisticated type-based binding-time analysis.
8.2 Domain-speciﬁc optimizations
Programs in particular domains often need to be optimized or specialized using
speciﬁc techniques that experts of the domains can implement more readily thancompiler or specializer writers. Examples include memoization for Gibonacci anddynamic programming (Swadi et al., 2006), pivoting for Gaussian elimination(Carette & Kiselyov, 2011), and simplifying complex arithmetic for Fast Fourier
Transform (Frigo & Johnson, 2005; Kiselyov & Taha, 2005). To better support
these domain-speciﬁc optimizations, two approaches have been developed in theliterature.

658

Y. Kameyama et al.

Side eﬀects in specializer input. The ﬁrst approach is to specialize a source languagethat has features (such as state) that help express custom optimizations. Alongthis line, Thiemann and Dussart (1999) built an oﬄine specializer for a higher-orderlanguage with mutable references. The example source programs in their paper show
how application programmers can persuade the specializer to produce eﬃcient code:by expressing unspecialized optimizations (such as memoization) and by improving
binding times manually (for instance, writing a recursive coercion to transform static
data into dynamic data).
As usual, Thiemann and Dussart’s (1999) specializer uses continuations to perform
let-insertion. What is less usual is that it is written in a store-passing style so as
to manage mutable references at specialization time. These static references areorganized by a binding-time analysis into regions (Talpin & Jouvelot, 1992; Tofte
et al., 2004). Regions limit the references’ lifetimes statically, much as our answer
types do in the simulation of state by delimited control in Section 3.2. However, oursimulation is relatively simplistic in that it allows access to only one mutable cell at atime, namely the cell at the nearest delimiter. To prevent scope extrusion, Thiemann
and Dussart’s (1999) binding-time analysis ensures that a static reference is used in
the scope of a dynamic binder only if the reference’s lifetime is local to the binder.
This constraint is analogous to our restriction of static eﬀects (not just mutation) to
the scope of dynamic binders. In general, the use of regions to encapsulate monadic
eﬀects is a large and productive research area (Kagawa, 2001; Fluet & Morrisett,2006; Ganz, 2006).
Optimizing compilers of imperative languages can determine the extent of possible
mutations by control-ﬂow analyses, but typically do not express the results of analysis
in the language or make them available to the programmer for inspection or control,
as our type system does. In particular, whereas Thiemann and Dussart’s (1999)
specializer infers binding-time annotations and performs let-insertion automaticallyand safely, our type system (akin to their constraints on annotations) ensures thesafety of code generators written by application programmers.
Custom code generators. The last diﬀerence brings us to the second way to support
domain-speciﬁc optimizations: letting domain experts write code generators. Thisapproach has the advantage that the behavior of a code generator on a static
input tends to be more predictable than the behavior of a specializer (especially its
binding-time analysis) on a source program. Swadi et al.’s (2006) and Carette andKiselyov’s (2011) uses of CPS and monadic style in domain-speciﬁc code generators
raise the need for a multilevel language to provide the convenience of eﬀects without
the risk of scope extrusion. Such a language is needed to ease the development andassure the safety of a variety of domain-speciﬁc code generators, not just a ﬁxed
specializer.
This paper addresses this need, following two previous papers. To prevent scope
extrusion in a multilevel language with references, Calcagno et al. (2000) proposed
to store only values of closed types in mutable cells. This (unimplemented) proposal
is too restrictive for our purposes, because we want to store future-stage variables
in memoization tables (as in our Gibonacci example).

Shifting the stage659

We previously (Kameyama et al., 2008) introduced a typed two-level language λα1v
and translated it to System F. That translation fails in the presence of eﬀects (dueto scope extrusion, manifest as a lack of type coercions), yet it is more complex
than our CPS translation in Section 6 here. (Choi et al. 2011 present anotherunstaging translation.) So far, then, it seems simpler to combine staging and eﬀects
by translating eﬀects rather than staging away.
9 Conclusions
We have presented the ﬁrst multilevel language for writing code generators thatprovides delimited control operators while assuring statically that all generated code
is well-formed. This language thus strikes a balance between clarity and safetythat helps application programmers implement domain-speciﬁc optimizations inpractical and reusable generators of specialized programs. The key idea that enables
this balance is to restrict control eﬀects to the scope of generated binders, that is, totreat generated binders as control delimiters.
As the examples illustrate, our language is expressive enough in many practicalsettings that we have encountered. Nevertheless, it would be useful to ﬁnd a soundway to relax our restriction on control eﬀects so as to perform let- and if-insertion
outside the closest generated binder. As discussed in Section 3.4, we could thenexpress loop-invariant code motion and generate assertions to be checked as earlyas possible. It might also help us to simultaneously access multiple pieces of state
at diﬀerent generated scopes, not just one piece as in Section 3.2. At the very least,
we would be able to throw exceptions as we generate code, for example, whenattempting to specialize Gibonacci (Section 2) to a negative n. (We can add an
ad hoc extension to our system permitting eﬀects to propagate beyond the closest
binder provided the answer type is a base type.)
Another good way to enrich our language is to add delimited control to a richer
language (like the language of Taha and Nielsen 2003) with run and cross-stage
persistence. Finally, as discussed in Section 4.1, our language can be made much more
comfortable to use by adding polymorphism over answer types (Asai & Kameyama,2007).
Supplementary material
For supplementary material for this article, please visit http://dx.doi.org/10.
1017/S0956796811000256
Acknowledgments
We thank Kenichi Asai, Olivier Danvy, and Atsushi Igarashi for helpful discussions,and the reviewers for their many helpful comments.
References
Asai, K. (2009) On typing delimited continuations: Three new solutions to the printf problem.
Higher-Order Symb. Comput. 22(3), 275–291.

660

Y. Kameyama et al.

Asai, K. & Kameyama, Y. (2007) Polymorphic delimited continuations. In Proceedings of
APLAS’07, LNCS, vol. 4807, pp. 239–254.
Balat, V., Di Cosmo, R. & Fiore, M. P. (2004) Extensional normalisation and type-directedpartial evaluation for typed lambda calculus with sums. In Proceedings of Annual Symposiumon Principles of Programming Languages (POPL), pp. 64–76.
Bondorf, A. (1992). Improving binding times without explicit CPS-conversion. In Proceedingsof LISP & Functional Programming, pp. 1–10.
Bondorf, A. & Danvy, O. (1991) Automatic autoprojection of recursive equations with global
variables and abstract data types. Sci. Comput. Program. 16(2), 151–195.
Calcagno, C., Moggi, E. & Taha, W. (2000) Closed types as a simple approach to safe
imperative multi-stage programming. In Proceedings of ICALP, LNCS, vol. 1853, pp. 25–
36.
Calcagno, C., Moggi, E. & Taha, W. (2004) ML-like inference for classiﬁers. In Proceedingsof ESOP, LNCS, vol. 2986, pp. 79–93.
Carette, J. (2006) Gaussian Elimination: A case study in eﬃcient genericity with MetaOCaml.
Sci. Comput. Program. 62(1), 3–24 (special issue on the First MetaOCaml Workshop 2004).
Carette, J. & Kiselyov, O. (2011) Multi-stage programming with functors and monads:
Eliminating abstraction overhead from generic code. Sci. Comput. Program. 76(5), 349–
375.
Choi, W., Aktemur, B., Yi, K. & Tatsuta, M. (2011) Static analysis of multi-staged programs
via unstaging translation. In Proceedings of POPL ’11: Conference Record of the Annual
ACM Symposium on Principles of Programming Languages, Ball, T. & Sagiv, M. (eds). New
York: ACM Press, pp. 81–92.
Cohen, A., Donadio, S., Garzarán, M. J., Herrmann, C. A., Kiselyov, O. & Padua, D. A.
(2006) In search of a program generator to implement generic transformations for highperformance computing. Sci. Comput. Program. 62(1), 25–46.
Czarnecki, K., O’Donnell, J. T., Striegnitz, J. & Taha, W. (2004) DSL implementation in
MetaOCaml, Template Haskell, and C++. In Proceedings of DSPG 2003, LNCS, vol.
3016, pp. 51–72.
Danvy, O. (1998) Functional unparsing. J. Funct. Program. 8(6), 621–625.
Danvy, O. & Filinski, A. (1989) A Functional Abstraction of Typed Contexts. Tech. Rep.
89/12, DIKU, University of Copenhagen, Denmark. Available at: http://www.daimi.au.
dk/~danvy/Papers/fatc.ps.gz Accessed 8 November 2011.
Danvy, O. & Filinski, A. (1990) Abstracting control. In Proceedings of LISP & Functional
Programming, Nice, France, June 1990, pp. 151–160.
Danvy, O. & Filinski, A. (1992) Representing control: A study of the CPS transformation.
Math. Struct. Comput. Sci. 2(4), 361–391.
Davies, R. (1996) A temporal logic approach to binding-time analysis. In Proceedings of
LICS, New Brunswick, New Jersey, July 27–30, pp. 184–195.
Davies, R. & Pfenning, F. (2001) A modal analysis of staged computation. J. ACM 48(3),555–604.
Dussart, D. & Thiemann, P. (1996). Imperative Functional Specialization. Tech. Rep. WSI-9628. Universität Tübingen.
Eckhardt, J., Kaiabachev, R., Pašalić, E., Swadi, K. N. & Taha, W. (2005) Implicitly
heterogeneous multi-stage programming. In Proceedings of GPCE, LNCS, vol. 3676,
pp. 275–292.
Elliott, C. (2004) Programming graphics processors functionally. In Proceedings of Haskell
Workshop, Snowbird, UT, USA, September 22, pp. 45–56.
Felleisen, M. (1991) On the expressive power of programming languages. Sci. Comput. Program.
17(1–3), 35–75.
Felleisen, M., Friedman, D. P., Kohlbecker, E. E. & Duba, B. F.. (1986) Reasoning with
continuations. In Proceedings of the 1st Symposium on Logic in Computer Science,
Cambridge, MA, USA, June 16–18, pp. 131–141.

Shifting the stage

661

Filinski, A. (1994) Representing monads. In Proceedings of POPL, Portland, Oregon, USA,
January 17–21, pp. 446–457.
Fluet, M. & Morrisett, J. G. (2006) Monadic regions. J. Funct. Program. 16(4–5), 485–545.
Frigo, M. & Johnson, S. G. (2005) The design and implementation of FFTW3. Proc. IEEE
93(2), 216–231.
Ganz, S. E. (2006). Encapsulation of State with Monad Transformers. Ph.D. thesis, Computer
Science Department, Indiana University.
Gomard, C. K. & Jones, N. D. (1991) A partial evaluator for the untyped lambda calculus.
J. Funct. Program. 1(1), 21–69.
Hammond, K. & Michaelson, G. (2003) Hume: A domain-speciﬁc language for real-timeembedded systems. In Proceedings of GPCE, LNCS, vol. 2830, pp. 37–56.
Igarashi, A. & Iwaki, M. (2007) Deriving compilers and virtual machines for a multi-level
language. In Proceedings of APLAS, LNCS, vol. 4807, pp. 206–221.
Kagawa, K. (2001) Monadic encapsulation with stack of regions. In Proceedings of FLOPS,
LNCS, vol. 2024, pp. 264–279.
Kameyama, Y., Kiselyov, O. & Shan, C.-c. (2008) Closing the stage: From staged code to
typed closures. In Proceedings of PEPM, San Francisco, CA, USA, pp. 147–157.
Kameyama, Y., Kiselyov, O. & Shan, C.-c. (2009) Shifting the stage: Staging with delimited
control. In Proceedings of PEPM. New York: ACM Press, pp. 111–120.
Kameyama, Y., Kiselyov, O. & Shan, C.-c. (2010) Mechanizing multilevel metatheory
with control eﬀects. In Proceedings of 5th ACM SIGPLAN Workshop on Mechanizing
Metatheory. Available at: http://www.cis.upenn.edu/~bcpierce/wmm/wmm10-program.
html Accessed 8 November 2011.
Kamin, S. (1996) Standard ML as a meta-programming language. Available at: http://loome.cs.uiuc.edu/pubs.html Accessed 8 November 2011.
Kiselyov, O. (2010) Delimited control in OCaml, abstractly and concretely: System description.
In Proceedings of FLOPS, LNCS, vol. 6009, pp. 304–320. Extended version to appear in
Theor. Comput. Sci.
Kiselyov, O., Shan, C.-c. & Sabry, A. (2006) Delimited dynamic binding. In Proceedings of
ICFP, Portland, OR, USA, pp. 26–37.
Kiselyov, O. & Taha, W. (2005) Relating FFTW and split-radix. In Proceedings of ICESS,
LNCS, vol. 3605, pp. 488–493.
Lawall, J. L. & Danvy, O. (1994) Continuation-based partial evaluation. In Proceedings of
LISP & Functional Programming, Austin, TX, USA, August 5–8, pp. 227–238.
Lengauer, C. & Taha, W. (eds). (2006) Special issue on the 1st MetaOCaml workshop (2004),
Sci. Comput. Program. 62(1).
Leone, M. & Lee, P. (1998) Dynamic specialization in the Fabius system. ACM Comput. Surv,
30(3es), article 23:1–23:6.
Leroy, X. & Pessaux, F. (2000) Type-based analysis of uncaught exceptions. ACM Tran. Prog.
Lang. Syst. 22(2), 340–377.
Masuko, M. & Asai, K. (2009) Direct implementation of shift and reset in the MinCaml
compiler. In Proceedings of ACM SIGPLAN Workshop on ML. New York: ACM Press,
pp. 49–60.
McAdam, B. J. (2001) Y in practical programs. Proceedings of Workshop on Fixed Points in
Computer Science. Available at: http://www.dsi.uniroma1.it/~labella/absMcAdam.ps
Accessed 8 November 2011.
MetaOCaml. (2006) MetaOCaml. Available at: http://www.metaocaml.org Accessed 8
November 2011.
Michie, D. (1968) “Memo” functions and machine learning. Nature 218: 19–22.
Minsky, Y. (2008) Bind without tears. Available at: http://ocaml.janestreet.com/?q=
node/23 Accessed 8 November 2011.
Moreau, L. (1998) A syntactic theory of dynamic binding. Higher-Order Symb. Comput. 11(3),233–279.

662

Y. Kameyama et al.

Morrisett, J. G. (1993) Reﬁning ﬁrst-class stores. In Proceedings of the ACM SIGPLAN
Workshop on State in Programming Languages, pp. 73–87.
Nielson, F. & Nielson, H. R. (1988) Automatic binding time analysis for a typed λ-calculus.
In Proceedings of POPL, San Diego, CA, USA, pp. 98–106.
Parigot, M. (1992) λμ-calculus: An algorithmic interpretation of classical natural deduction.
In Proceedings of LPAR, LNAI, vol. 624, pp. 190–201.
Pašalić, E., Taha, W. & Sheard, T. (2002) Tagless staged interpreters for typed languages. In
Proceedings of ICFP, pp. 157–166.
Peyton Jones, S. L. (2003) The Haskell 98 language and libraries. J. Funct. Program. 13(1),1–255.
Püschel, M., Moura, J. M. F., Johnson, J., Padua, D., Veloso, M., Singer, B. W., Xiong, J.,Franchetti, F., Gačić, A., Voronenko, Y., Chen, K., Johnson, R. W. & Rizzolo, N. (2005)
SPIRAL: Code generation for DSP transforms. Proc. IEEE 93(2), 232–275.
Sørensen, M. H. B., Glück, R. & Jones, N. D. (1994) Towards unifying deforestation,
supercompilation, partial evaluation, and generalized partial computation. In Proceedingsof ESOP, LNCS, vol. 788, pp. 485–500.
Sumii, E. and Kobayashi, N. (2001) A hybrid approach to online and oﬄine partial evaluation.
Higher-Order Symb. Comput. 14(2–3), 101–142.
Swadi, K., Taha, W. & Kiselyov, O. (2005) Dynamic programming benchmark. Available at:
http://www.metaocaml.org/examples/dp/ Accessed 8 November 2011.
Swadi, K., Taha, W., Kiselyov, O. & Pašalić, E. (2006) A monadic approach for avoiding
code duplication when staging memoized functions. In Proceedings of PEPM, Charleston,SC, USA, January 9–10, pp. 160–169.
Taha, W. (2000). A sound reduction semantics for untyped CBN multi-stage computation. In
Proceedings of PEPM, Boston, MA, USA, pp. 34–43.
Taha, W. (2005) Resource-aware programming. In Proceedings of ICESS, LNCS, vol. 3605,
pp. 38–43.
Taha, W. & Nielsen, M. F. (2003) Environment classiﬁers. In Proceedings of POPL, New
Orleans, LA, USA, January 15–17, pp. 26–37.
Talpin, J.-P. & Jouvelot, P. (1992) Polymorphic type, region and eﬀect inference. J. Funct.
Program. 2(3), 245–271.
Thielecke, H. (2003) From control eﬀects to typed continuation passing. In Proceedings of
POPL, New Orleans, LA, USA, January 15–17, pp. 139–149.
Thiemann, P. (1999) Combinators for program generation. J. Funct. Program. 9(5), 483–525.
Thiemann, P. & Dussart, D. (1999) Partial evaluation for higher-order languages with state.
Available at: http://www.informatik.uni-freiburg.de/~thiemann/papers/mlpe.ps.
gz Accessed 8 November 2011.
Tofte, M., Birkedal, L., Elsman, M. & Hallenberg, N. (2004) A retrospective on region-based
memory management. Higher-Order Symb. Comput. 17(3), 245–265.
Wadler, P. L. (1992) Comprehending monads. Math. Struct. Comput. Sci. 2(4), 461–493.
Whaley, R. C. & Petitet, A. (2005) Minimizing development and maintenance costs insupporting persistently optimized BLAS. Softw. Pract. Exp. 35(2), 101–121.