Polymorphic Multi-Stage Language with Control Effects
Yuichiro Kokaji and Yukiyoshi Kameyama
University of Tsukuba, Japan
kokaji@logic.cs.tsukuba.ac.jp,kameyama@acm.org

Abstract. Multi-stage programming (MSP) is a means for run-time code generation, and has been found promising in various fields including numerical computation and domain specific languages. An important problem in designing MSP
languages is the dilemma of safety and expressivity; many foundational calculi
have been proposed and proven to be type safe, yet, they are not expressive
enough. Taha’s MetaOCaml provides us a very expressive tool for MSP, yet, thecorresponding theory covers its purely functional subset only.
In this paper, we propose a polymorphic multi-stage calculus with delimitedcontrol operators. Kameyama, Kiselyov, and Shan proposed a multi-stage calculus with computation effects, but their calculus lacks polymorphism. In thepresence of control effects, polymorphism in types is indispensable as all purefunctions are polymorphic over answer types, and in MSP languages, polymorphism in stages is indispensable to write custom generators as library functions.
We show that the proposed calculus satisfies type soundness and type inference.
The former is the key to guarantee the absence of scope extrusion - open codes arenever generated or executed. The latter is important in the ML-like programming
languages. Following Calcagno, Moggi and Taha’s work, we propose a HindleyMilner style type inference algorithm to obtain principal types for given expressions (if they exist).

1

Introduction

Writing a code generator as a metaprogram is a vital means to achieve efficiency andmaintainability simultaneously. Typed multi-stage (multi-level) programming languages
help us write code generators easily and intuitively. The merit of typed multi-stage calculus over its untyped cousin, the quasiquote and unquote mechanism in Scheme, is thestatic assurance of type soundness: it subsumes not only type safety of code generators,
but also that of generated codes, which in turn subsumes the absence of scope extrusion:a closed code generator never generates open codes (codes with free variables).
Many researchers have addressed the problem of assuring type soundness for multistage calculi; foundational calculi based on modal logic include λ  by Davies andPfenning [5], λ by Davies [4], and λ  by Yuse and Igarashi[17]. More expressive
calculi have been proposed such as λ α by Taha and Nielsen [13], λ i by Calcagno,
sim by Kim, Yi and Calcagno [8], and the calculus by Tsukada
Moggi and Taha [2], λopen
and Igarashi [15].
Our goal is to extend the applicability of multi-stage programing so that one canwrite efficient code generators naturally, while keeping static type soundness. This is achallenging goal as efficient code generation (such as let-insertion) often needs impure(effectful) operations, while existing theories guarantee type soundness for purely functional subcalculi only. A recent hot topic is to add computational effects into multi-stage
languages [7, 10, 16]. All of them remain monomorphic setting, though.
In this paper, we introduce ML-like polymorphism into multi-stage languages withcomputational effects, and in particular, we propose a polymorphic multi-stage calculus with delimited-control operators which satisfies type soundness. We think polymorphism is necessary in this kind of calculi by the following reasons:– Many useful combinators for code generation are polymorphic functions1 , and,
therefore, we need polymorphism to build a useful library for code generation.
– In the presence of computational effects, a type system of MSP calculi necessarily
becomes so called a type-and-effect system. Then, all the pure functions (without effects) in existing libraries should be polymorphic over effects. In the caseof delimited-control operators, the effects are expressed as the answer types, and,
therefore, polymorphism in effects boils down to polymorphism in (answer) types.
– In MSP calculi based on Taha and Nielsen’s λ α or Calcagno et al.’s λ i , polymorphism in environment classifiers2 is necessary to write code generators as libraries.
The staged power function is the simplest example for MSP, which already needs
polymorphism in classifiers, if written as a library function (that is, not inlined).
Introducing ML-like let-polymorphism is not as trivial as one might expect. The
value restriction used in ML families is too restrictive, as we want to generate polymorphic functions as the result of code generation. Other syntactic conditions do not seemsuitable, either. Our solution for this problem is to revisit the semantic notion of purity, proposed by Asai and Kameyama [1] for the unstaged polymorphic calculus withdelimited-control operators. A term is called pure if it does not have computational effects observable from outside. Asai and Kameyama have shown that a pure term canbe made polymorphic. Following them, we allow polymorphism only for pure terms inthis paper. Surprisingly, this simple idea works: it rules out all dangerous terms, while
we retain the expressivity.
The proposed calculus extends Kameyama, Kiselyov, and Shan’s calculus in thesense that we add let-polymorphism and the run-construct (for code execution) to theircalculus. We prove type soundness of our calculus under the purity restriction, which
implies that open codes are never generated or executed. We also show Hindley-Milner’s
style type inference algorithm for our calculus, which gives principal types if they exist.
The rest of this paper is organized as follows: Section 2 shows several example
programs using multi-stage calculi and control operators, which need polymorphism.
Section 3 explains the key idea of introducing polymorphism safely. Section 4 introDC and operational semantics, and Section 5 introduces its type
duces our calculus λlet
system. Then we show several useful properties such as type soundness in Section 6
and the existence of principal types in Section 7. Section 8 states concluding remarks.
1 We will see an example of code generation combinators in Section 2.
2 Environment classifiers are identifiers for stages, first introduced by Taha and Nielsen [13].

II2Preliminaries

This section is an example-based introduction to MSP and delimited-control operators.
A comprehensive introduction to this subject may be found in the literature [11, 12,7]. We use MetaOCaml to write concrete programs3 in this section. It has three constructs for code generation: brackets, escape, and run. We do not treat CSP (cross-stage
persistence) in this paper.
Staged Power Function. The first, canonical example of MSP is the staged version of
the power function:
let rec s_power n x =if n = 1 then x
else < ~x * ~(s_power (n-1) x)>
The expression <e> (bracket expression) represents a code which is not executed at thepresent stage, but executed at the future (next) stage. We can splice a code fragment
into another code by an escape expression ∼e. In the expression <∼x ∗ · · ·>, the subexpression x is executed, and its value is spliced in this code. For instance, if we evaluate (fun x-> <~x * 2>) <3 + 4>, we get <(3 + 4) * 2>. For those familiar with
Scheme macros, brackets and escape, resp, correspond to quasiquote and backquote(unquote), resp.
By executing the expression <fun x -> ~(s_power 5 <x>)>, we get<fun x_1 -> (x_1*(x_1*(x_1*(x_1*x_1))))
as its value. Note that the bound variable x has been renamed to x_1 during the computation, which means that variables in codes are lexically bound unlike the templatemechanisms in C++ and Haskell. We can run the resulting code internally by the runconstruct (!). The computation of the expression:
let power5 = ! <fun x -> ~(s_power 5 <x>)>yields a function equivalent to
fun x_1 -> (x_1*(x_1*(x_1*(x_1*x_1))))
which can be used at the present stage, rather than the future stage.
Let us consider the type of s_power. Intuitively, it has type int → <int> → <int>
where <int> is the type of codes for integer expressions. Taha’s λilet , the underlying
calculus of MetaOCaml, assigns to each future stage an environment classifier (classifier for short), in order to distinguish different next stages from each other. Hences_power has type int → <int>` → <int>` where ` is a classifier. Since s_power
is polymorphic over stages (it is not specific to any environment classifiers), its typeshould be polymorphic over classifiers as: ∀`.(int → <int>` → <int>` ).
Code Generation Combinators. Combinators provide us useful patterns of generating
and manipulating code fragments. One of the simplest, but widely used combinators isthe following eta:
let eta f = <fun x -> ~(f <x>)>in eta (fun y -> <fun z -> z + ~y>)3 We use slightly simplified notation for multi-stage constructs: we write <e> for the MetaOCaml

notation .<e>. and we suppress type variables corresponding to environment classifiers.

IIIwhich, when executed, yields <fun x -> fun z -> z + x>. It is easy to see thateta should have the polymorphic type: ∀`.∀σ .∀τ .(<σ >` → <τ >` ) → <σ → τ >` .
The staged power function may be generalized to an arbitrary binary function:
let rec s_iterate n f x =if n = 1 then x
else < ~f ~x ~(s_iterate (n-1) f x)>
in let s_iterate5 =eta (fun f -> eta (s_iterate 5 f))which, when executed, returns <fun f -> fun x -> f x (f x (f x (f x x)))>.
MetaOCaml assigns a monomorphic type to this expression, but we hope to assign apolymorphic type: ∀`.∀σ .<(σ → σ → σ ) → σ → σ >` to this expression. Here, polymorphism is necessary both at the present stage and the future stage.
Delimited-Control Operators. Control operators in functional languages are constructs
for changing the order of execution, causing computational effects. Typical control operators are catch/throw (Lisp), exception (ML, Java), and call/cc (Scheme, SML/NJ).
While call/cc provides an access to unlimited continuations, delimited-control operators provide an access to part of the current continuations (delimited continuations).
The following examples use Danvy and Filinski’s delimited-control operators shift
and reset [3]:1 + reset (10 + 20)
1 + reset (10 + (shift k -> 20))
1 + reset (10 + (shift k -> (k (k 20))))yieldsyieldsyields31
21
41

We sometimes write shift and reset, resp., as Sk.e and {e}, resp.4 reset denotes adelimiter, and does nothing if there is no shift as shown in the first line. In the second
and third lines, shift captures the continuation (an evaluation context) up to the nearest
reset operator, and binds the variable k to it. In the example, the captured continuationis reset (10 + [ ]) where [ ] is a hole. It is bound to k and may be used later. In
the third line, k (k 20) evaluates to reset (10 + (reset (10 + 20))).
In the presence of delimited-control operators, the type system should take into
account control effects (thus becomes a type-and-effect system). If we execute the following program:let f = fun x -> shift k -> (k 10) + 20
in reset (f 30 >= 40)
the continuation captured by shift is reset ([ ] >= 40). Then we evaluate(reset (10 >= 40)) + 20, which raises a run-time type error.
The computational effect caused by shift and reset can be described by an answer type, the return type of a delimited continuation. In the above program, the shiftexpression expects the answer type to be int (since the captured continuation k is expected to return an integer), while the reset expression provides bool as its answer
4 In the literature, a reset expression is denoted by <e>. We write {e} to avoid conflict with abracket expression.

IVtype. In the type-and-effect system, a function type takes the form σ → σ 0 /β , whereβ represents the answer type. This change of type system makes all pure functions to
be polymorphic over effects: for instance, the function fun x -> x + 10 should havetype int → int/β for any type β .
Delimited-control operators such as shift and reset have been found rather expressive: Filinski [6] proved that they can express any monadic effect, and Kiselyov,
Shan and Sabry have shown a concise encoding of dynamic binding and local states interms of them [9]. Kameyama, Kiselyov and Shan [7] have introduced control operators to type-safe multi-stage calculi, and shown that memoization in code generators is
expressible as let-insertion in the calculus. In this paper, we proceed one step further, tointroduce polymorphism into their calculus.

3 Introducing Polymorphism Safely
In this section, we investigate the problem of introducing let-polymorphism into a multistage calculus with effects, and informally show our ideas to solve the problem.
Value Restriction. As is well known, unrestricted combination of computational effects(such as states and control) and polymorphism leads to type unsoundness, and the value
restriction is the standard solution for this problem: for an expression let x = e1 in e2 ,e1 must be a (syntactic) value for x to have a polymorphic type in e2 .
Unfortunately the value restriction is too restrictive in multi-stage calculi: in unstaged calculi we only define polymorphic functions, but in staged calculi we want togenerate (the codes of) polymorphic functions, while value restriction prohibits runtime code generation of such polymorphic functions. Let us consider the following
example:let iterate5 = ! s_iterate5
in
iterate5 (fun x y -> x * y) 3;
iterate5 (fun x y -> x ^ y) "abc"In this program snippet, the expression ! s_iterate5 is not a value, and, therefore,
iterate5 cannot have a polymorphic type under the value restriction.
The Problem. We need a better criterion as to which terms can be polymorphic. This
is not a trivial problem as one might expect. To see the problem, let us consider the program let y = e in <let x = ~y in e2>. Then we have different situations depending on the expression e:– if e evaluates to a code of a value, say, <fun z-> z>, then x can be polymorphic.
– if e evaluates to a code of an effectful computation (say, <shift k -> 10>), thenx cannot be polymorphic.
In summary, it is not possible to decide the condition by simply looking at the expression e1 in let x = e1 in e2 . In other words, the condition must be context sensitive.
Purity Restriction in Unstaged Calculus. Asai and Kameyama [1] have proposed amore liberal condition for let-polymorphism, called the purity restriction, for the (unstaged) calculus with the delimited-control operators shift and reset.
VAn expression is pure if there are no computational effects that are observable fromoutside. In the calculus with shift and reset, the only observable effect (other thantermination) is the control effect caused by shift, so an expression is pure if all thecalls to shift are captured within this expression, and is not pure otherwise. A pure
expression is polymorphic in the answer types [14], and we can determine if a given
expression is pure or not by tracking its answer type. However, type inference for sucha type system is hard, and they replaced it by its conservative approximation as:
Definition 1 (Syntactic Purity [1]). An (unstaged) expression is syntactically pure if it
is a value or a reset expression {e}.
The syntactic purity is a stronger (more restrictive) notion than purity, since a pure
expression is not necessarily syntactically pure, for instance, Sk.k 10. However, there is
no loss of expressivity by choosing syntactic purity, since, for any pure e, we can add asuperfluous reset as {e} while preserving typability and operational behavior. Asai andKameyama have proven type soundness as well as other desirable properties for theircalculus under the syntactic purity restriction.
Purity Restriction in Multi-Stage Calculus. We borrow their idea to formulate the notion of (syntactic) purity in multi-stage calculi, and apply it to let-polymorphism. Sincea level-0 expression (present stage expression) cannot have level-1 effects (computation
effects of future stage), we formulate (semantic) purity as follows:– A level-0 expression (an expression at the present stage) is pure if and only if it
does not have observable computational effects of level-0.
– A level-1 expression (an expression at the future stage) is pure if and only if it does
not have observable computational effects of level-0 and level-1.
As in the case of unstaged calculus, this semantic notion of purity is hard to decide,
and we replace it by syntactic purity as follows:– For a level-0 let-expression let x = e1 in e2 , the expression e1 must be a syntactic
value or in the form {e01 }.
– For a level-1 let-expression let x = e1 in e2 , the expression e1 must be a syntactic
value or in the form {∼{<e01 >}}.
The former is the same as syntactic purity in the unstaged calculus. As for the latter, fora level-1 expression e01 , the expression {∼{<e01 >}} introduces a level-0 reset, and thenthe outer most reset is of level-1. In summary, this expression has resets of both levels.
Syntactic Purity in Action. When we introduce the syntax of our calculus, we need
one more twist. Rather than directly treating the (syntactically) pure expressions in theabove forms, we instead use polymorphic let expression plet x = e1 in e2 , which
intuitively means let x = {e1 } in e2 for level-0, and let x = {∼{<e1 >}} in e2 forlevel-1. This change of syntax greatly simplifies our formulation and it is called theimplicit-delimiter method.
The implicit-delimiter method was also used in the literature for a different purpose;
Kameyama, Kiselyov and Shan [7] regarded a level-1 binder as a delimiter for level-0,
advocating that future-stage binders delimit present-stage control effects. For instance,VIthe level-1 expression λ x.e is intuitively equivalent to λ x.∼{<e>} which has a level-0
delimiter (reset).5
In fact, we need both techniques in our calculus – one for ensuring syntactic purity and the other for regarding binders as delimiters. We list all the uses of implicit
delimiters below.
(level 0)

run e ≡ run <{∼{e}}>plet x = e1 in e2 ≡ plet x = {e1 } in e2(level-1)

λ x.e ≡ λ x.∼{<e>}Sk.e ≡ Sk.∼{<e>}plet x = e1 in e2 ≡ plet x = {∼{<e1 >}} in ∼{<e2 >}Note that one should understand the above equivalences (denoted by ≡) as informal
ones. They will help us understand some reduction rules in Section 4 and the typesystem in Section 5, but they are not formal entities.
Summary and Discussion. We introduce the syntactic approximation of the notion of
purity in the multi-stage calculus. The notion of syntactic purity meets all our needs
for let-polymorphism: it is liberal so that we can generate the codes of polymorphic
functions in run-time. It is safe in the sense that type soundness holds for our calculus.
It is easy to decide if a given expression is pure or not.
We believe that disallowing uncaptured calls to shift in polymorphic functions isreasonable and our implicit-delimiter approach relies on this assumption. In our experience, polymorphism and computational effects in MSP languages are completely
separated, and, therefore, our purity restriction is not problematic. However, this is not
at all a final word, and a further study is left for future work.

4

The Calculus

DC , which is based on
This section introduces the polymorphic multi-stage calculus λleti
λ by Calcagno et al., and λ1 by Kameyama et al. The former has polymorphism,
more than two levels, CSP, but no control operators. The latter has control operators but
no polymorphism, no run constructs and no CSP, and is restricted to two levels. Our
DC has control operators, polymorphism, run constructs, but currently does
calculus λlet
not have CSP, and restricted to two levels. The principles of our design are simplicity
and essence: the combination of control operators, polymorphism, and run constructs
are the usual sources of type unsoundness, thus leading to scope extrusion, while adding
more than two stages and CSP seems orthogonal to these problems. It is desirable tohave all these features, but in this paper, to avoid clutter, we present a minimal calculus
which exposes the subtle problems in the design of multi-stage calculi. Extension tomore expressive calculi are left for future work.
We restrict the computational effects to those caused by shift and reset, andtheir answer types be invariant through the computation (no answer-type modification).
Danvy’s type-safe printf is a typical example which needs the effect of answer-type
5 We inserted brackets and escape to make the reset be of level 1.

VIIe0 ::= v0 | e0 e0 | e0 + e0 | plet x = e0 in e0 | {e0 } | Sk.e0 | <e1 > | run e0e1 ::= v1 | e1 e1 | e1 + e1 | plet x = e1 in e1 | {e1 } | Sk.e1 | ∼e0v0 ::= x | i | λ x.e0 | <v1 >v1 ::= x | i | λ x.v1 | v1 v1 | v1 + v1 | plet x = v1 in v1 | {v1 } | Sk.v1
Fig. 1. Syntax of Expressions

modification if written in direct style, so it is not typable in our calculus. However, thisrestriction is only for presentation; we can develop the calculus with answer-type modification, although it doubles the number of answer types in the judgment. We believethat our calculus provides a useful information on how to introduce polymorphism into
multi-stage calculus with computational effects.
DC . We assume to have an infinite number of enviSyntax. We define the syntax of λletronment classifiers (or classifiers) `, `1 , `2 , · · · . They are abstract entities; variables forclassifiers are quantified by ∀, but there are no constants for classifiers. The stage-level
L is either 0 (for the present stage), or a single classifier ` (for the next, or future stage).
In general a level is a finite sequence of classifiers, but we restrict the number of levels
to two, so the maximum length of levels is 1. When the names of classifiers do notmatter, all stage-levels `i are simply called “level 1”.
Fig. 1 defines the type-free expressions where en and vn , resp., are a level-n expression and a level-n value, resp., for n = 0, 1.
A level-0 expression e0 is either a variable x, an integer literal i, λ -abstraction λ x.e0 ,addition e0 + e0 , a polymorphic let expression plet x = e0 in e0 , a reset expression{e0 }, a shift expression Sk.e0 , a bracket expression <e1 >, or a run expression run e0 .
Note that, a level-1 expression e1 should come inside a bracket expression.
A level-1 expression e1 contains an escape expression ∼e0 , but since the maximum
level is one, there are no expressions like <e2 > or run e1 .
A level-0 value v0 is standard except that a bracket expression <v1 > constitutes acode value. Note that we will introduce call-by-value operational semantics. The definition of a level-1 value v1 contains all kinds of expressions except an escape expression.
The variable x in λ x.e and plet x = e0 in e, k in Sk.e are bound in each e. We
identify α -equivalent expressions as usual, and FV(e) denotes the set of free variables
in e. Given an expression e, a variable x and a value v of the same level as x, e[v/x]
denotes the result of substitution of v for x in e.
Operational Semantics. We define the call-by-value operational semantics. Fig. 2 defines evaluation contexts of various levels. E i j denotes an evaluation context such thatits hole (denoted by •) will be filled by a level- j expression, and then the whole context
will become a level-i expression. An interesting one is E 01 [λ x.•], which means that weevaluate under lambda abstraction.
We also define a pure evaluation context F 0 j for j = 0, 1. Intuitively, this context
does not have resets which enclose the hole. In our calculus, certain expressions have
implicit resets, and they cannot constitute pure evaluation contexts.
VIII

E 00 ::= • | E 00 [•e0 ] | E 00 [v0 •] | E 00 [• + e0 ] | E 00 [v0 + •]| E 00 [plet x = • in e0 ] | E 00 [{•}] | E 00 [run •] | E 01 [∼•]
E 01 ::= E 01 [•e1 ] | E 01 [v1 •] | E 01 [• + e1 ] | E 01 [v1 + •] | E 01 [λ x.•]
| E 01 [plet x = • in e1 ] | E 01 [plet x = v1 in •]| E 01 [Sk.•] | E 01 [{•}] | E 00 [< • >] | E 01 [run •]F 00 ::= • | F 00 [•e0 ] | F 00 [v0 •] | F 00 [• + e0 ] | F 00 [v0 + •] | F 01 [∼•]F 01 ::= F 01 [•e1 ] | F 01 [v1 •] | F 01 [• + e1 ] | F 01 [v1 + •] | F 00 [< • >]Fig. 2. Evaluation Contexts

E 00 [i + j]00

E 00 [(λ x.e0 )v0 ]E 00 [e0 [v0 /x]]0

00 0 00E [plet x = v in e ]E 00 [{F 00 [Sk.e0 ]}]E 00 [{v0 }]E 00 [v0 ]E 01 [∼<v1 >]E 01 [v1 ]00

E 00 [v1 ]E 00 [m] if i + j = m

E [e [v /x]]

1

E [run <v >]E 00 [{e0 [λ x.{F 00 [x]}/k]}]Fig. 3. Reduction Rules

Fig. 3 gives the reduction rules in the evaluation-context style.
The first three rules are integer addition, β reduction in call-by-value, and letreduction as usual. The next two rules are the ones for control operators. shift captures
the continuation delimited by the nearest delimiter. In the rule, F 00 is an evaluation context which does not have resets around the hole, which means that the reset displayedin the rule is the nearest one. After capturing the delimited context {F 00 }, we convert
it to a functional form λ x.{F 00 [x]}, and bind k to it, and continue the evaluation. For
the next rule, if the body of a reset expression is a level-0 value, the delimiter is simply
discarded.
The last two rules are the reduction rules for multi-stage constructs. In the second
last rule, the evaluation context E 01 signifies that the hole in E 01 is of level-1, whichmeans that there are brackets enclosing the hole. Hence the subexpression ∼<v1 > appears in a code, and thus we are splicing the code v1 into the code. Then it is easy tounderstand the reduction rule. The last rule defines the code execution. If the body of
the run expression is <v1 >, then we extract the content v1 of the code expression, andstart evaluating v1 . In the right-hand side of this rule, a level-1 value v1 is plugged in to
the level-0 hole in E 00 .
Reductions for Implicit Delimiter. One may notice that reduction rules Fig. 3 are too
weak. In fact, there are closed, non-value expressions that may not be reduced by any
reduction rules. For instance, {<λ x.∼(Sk.e)>} gets stuck, since the obvious candidate
for reduction is E 00 [{F 00 [Sk.e0 ]}] · · · , but the definition of F 00 does not allow level-1
abstraction λ x.e. Our calculus rules out some of such kinds of expressions, but not all of
IX

Auxiliary definition for pure evaluation contexts:
F 10 ::= F 10 [•e0 ] | F 10 [v0 •] | F 10 [• + e0 ] | F 10 [v0 + •] | F 11 [∼•]F 11 ::= • | F 11 [•e1 ] | F 11 [v1 •] | F 11 [• + e1 ] | F 11 [v1 + •] | F 10 [< • >]Additional reduction for level-0 implicit resets:
G[F 00 [Sk.e0 ]]
0

00

0

G [F [Sk.e ]]G[∼{e0 [λ x.{F 00 [x]}/k]}]0

where G ::= E 00 [plet x = • in e0 ]G [{e [λ x.{<{∼F [x]}>}/k]}]
000

where G0 ::= E 00 [run •]Additional reduction for level-1 implicit resets:
H[F 10 [Sk.e0 ]]H[∼{e0 [λ x.{<F 10 [x]>}/k]}]where H ::= E 01 [λ x.•] | E 01 [Sk0 .•] | E 01 [plet x = • in e1 ] | E 01 [plet x = e1 in •]Fig. 4. Reduction rules for implicit resets

them. Some expressions in the above form typecheck in our type system, and thus, weneed additional reduction rules for those safe patterns, to take into account the implicit
delimiters.
Fig. 4 gives the reduction rules corresponding to implicit resets.
Although the reduction rules look complicated, they are in fact simply derived fromthe informal reading for implicit resets, stated earlier.

5 Type System
DC . We first
In this section, we define a polymorphic type system for the calculus λletdefine types:

σ , τ , α , β ::= t | int | σ → τ /β | <σ /β >`T ::= σ | ∀t.T | ∀`.T

monomorphic type
polymorphic typewhere t is a type variable, and int is the type for integers. The type σ → τ /β is the function type with effects, which are determined by the answer type β . The type <σ /β >` isthe type for codes of level ` where σ is the type of the code, and β is a level-1 answer
type.
The polymorphic type T is a monomorphic type with universal quantification. Following Calcagno et al. [2], we have two kinds of quantification: ∀t.T represents universal quantification over types, and ∀`.T universal quantification over environment
classifiers. We sometimes write ∀t.∀`.σ for the type σ quantified over sequences oftype variables t1 , · · · ,tn and environment classifiers `1 , · · · , `m .
For a type T , FC(T ) and FTV(T ), resp., are the set of free classifiers in T , and theset of free type variables in T , resp. In the following, we sometimes write FV(Γ ) and soon, which has obvious meaning.
A general form of a judgment is Γ `L e : σ ; β0 ; β1 where the type context Γ isa (possibly empty) finite sequence of the form (x : T )L where T is a polymorphic typeXand L is a level. The level L in (x : T )L means that the variable x can be used in level
L. The above judgment means that, under the type context Γ , e is a level-L expressionof type σ with the level-0 answer type β0 and the level-1 answer type β1 . When L = 0,
the level-1 answer type β1 is not significant (a level-0 expression cannot contain level-1
effects), and therefore we often write − for β1 .
DC are defined as follows.
Typing rules of λlet(i is an integer constant)Γ `L i : int ; β

0

; β1

(τ ≤ T )intΓ , (x : T )L `L x : τ; β0 ; β1varΓ `L e1 : int ; β0 ; β1 Γ `L e2 : int ; β0 ; β1plus
Γ `L e1 + e2 : int ; β0 ; β1
Γ , (x : σ )0 `0 e : τ ; β0 ; −Γ `0 λ x.e : σ → τ /β0 ; α0 ; −Γ , (x : σ )` `` e : τ ; <τ /β1 > ; β1λ0Γ `` λ x.e : σ → τ /β1 ; α0 ; α1Γ `` e1 : σ → τ /α1 ; α0 ; α1Γ `` e2 : σ ; α0 ; α1app1
Γ `` e1 e2 : τ ; α0 ; α1Γ `0 e1 : σ → τ /α0 ; α0 ; −Γ `0 e2 : σ ; α0 ; −app0
Γ `0 e1 e2 : τ ; α0 ; −Γ `0 e1 : σ ; σ ; −t ⊆ FTV(σ ) − FTV(Γ ), ` ⊆ FC(σ ) − FC(Γ )Γ , (x : ∀t.∀`.σ )0 `0 e2 : τ ; β0 ; −let0Γ `0 plet x = e1 in e2 : τ ; β0 ; −Γ , (k : ∀t.(σ → β0 /t))0 `0 e : β0 ; β0 ; −Γ `0 Sk.e : σ; β0 ; −Γ `` e1 : σ ; <σ /σ >` ; σt ⊆ FTV(σ ) − FTV(Γ )Γ , (x : ∀t.σ )` `` e2 : τ ; <τ /β1 >` ; β1Γ `` plet x = e1 in e2 : τ ; <τ /β1 >` ; β1Γ `` Sk.e : σ ; α0 ; β1Γ `0 <e> : <σ /β1 >` ; β0 ; −Γ ` 0 e : β0 ; β0 ; −shift0Γ , (k : ∀t.(σ → β1 /t))` `` e : β1 ; <β1 /β1 >` ; β1Γ ` ` e : σ ; β0 ; β1

λ1brackets0

Γ `0 {e} : β0 ; α0 ; −shift1Γ ` ` e : β1 ; β0 ; β1Γ `` {e} : β1 ; β0 ; α1Γ `0 e : <σ /β1 >` ; β0 ; −Γ `` ∼e : σ ; β0 ; β1Γ `0 e : <σ /σ >` ; <σ /σ >` ; − (` 6∈ FC(Γ , σ ))Γ `0 run e : σ ; α0 ; −XI

reset0

run0

escape1reset1

let1

Let us explain the typing rules briefly.
The var rule is the standard one in polymorphic type systems where τ ≤ T meansthat τ is an instance of polymorphic type T . More precisely, if T = ∀t.∀`.σ for amonomorphic type σ , then τ = σ [α /t][`0 /`] for some α1 , · · · , αn , `01 , · · · , `0k .
The λ 0 rule is also standard except that it retrieves the level-0 answer type β0 into
the function type σ → τ /β0 . Since a function does not have computational effects,
its level-0 answer type can be an arbitrary type α0 . The λ 1 rule is the key to avoid
scope extrusion as studied by Kameyama, Kiselyov and Shan [7]. As we explained in
Section 3, the level-1 expression λ x.e has an implicit level-0 reset beneath this lambda,
namely, its intuitive meaning is λ x.∼{<e>}. In order to type this expression, we needto require the level-0 answer type for e be <τ /β1 >` . The app rules can be understoodeasily.
The level-0 polymorphic let expression plet x = e1 in e2 should be understoodas let x = {e1 } in e2 , hence the answer type of e1 must be the same as the typeof e1 itself. (See also the reset rule below.) The level-1 polymorphic let expressionplet x = e1 in e2 is slightly more complex. First, due to the purity restriction for e1 , it isunderstood as let x = {∼{<e1 >}} in e2 . But since this level-1 let expression is a binder
for e2 , it must not have level-0 effects, and therefore, let x = {∼{<e1 >}} in ∼{<e2 >}is the final meaning of polymorphic let expression. The type rule reflects this reading.
The shift rules are adaptation from the standard typing rules for them in the literature of delimited continuations. For instance, level-0 shift captures a delimited context
whose answer type is β0 . Thus the type of k must be a function type whose return type is
β0 . Since the delimited continuation is a pure function (no control effects are involved),
it is polymorphic in the answer type, and thus we quantify t in σ → β0 /t. The shift1 rule
is more complex, as it binds level-1 variables k, and again we have an implicit level-0
reset. (Note the level-0 answer type for e is <β1 /β1 >` .)The reset rules are also adaptation of the type rule in the literature. For a level-0
expression {e}, its type must be the same type as that of e and also the level-0 answer
type of e. Since {e} has no observable control effects, its level-0 answer type can bearbitrary type α0 . The level-1 reset rule can be understood similarly.
The rules for brackets and escapes are the same as those in λ α and λ i except that
we need to memoize the level-0 effect (β1 ) in the code type as <σ /β1 >` . Brackets turna level-1 expression to a level-0 expression, and escape does the converse.
Finally, the run rule is one of the most interesting ones. The run construct is to
execute the code (inside brackets) at the present stage, and thus it is important to ensure
it is a closed code. The calculi λ α and λ i ensure this closedness condition in terms of
the eigen-variable condition for the classifier `: it must not appear at any other placein the judgment for e. If the condition is met, e does not depend on the stage `, so we
can run (and compile) it at the present stage. In addition to this condition, we need torule out, for instance, an expression like run <shift k -> ..>. In general we needto ensure level-0 and level-1 purity of e in this rule. Thus we implicitly introduce resetsof both levels.
The following figure shows a type derivation for λ x.∼(Sk.<x + 10>) where Γ = (x :int)` , (k : ∀t.<int/int>` → <int/int>` /t)0 .

XIIΓ `` x + 10 : int ; <int/int>` ; intΓ `0 <x + 10> : <int/int>` ; <int/int>` ; −(x : int)` `0 Sk.<x + 10> : <int/int>` ; <int/int>` ; −(x : int)` `` ∼(Sk.<x + 10>) : int ; <int/int>` ; int`` λ x.∼(Sk.<x + 10>) : (int → int/int) ; β1 ; β26 Type Soundness
DC , which consists of the subject reduction
In this section we prove type soundness of λlet
property (type preservation) and the progress property. Due to lack of space, we do notgive complete proofs, and, instead state important lemmas in this paper.

Lemma 1 (Values do not have effects). If Γ `0 v0 : σ ; β0 ; − is derivable, thenΓ `0 v0 : σ ; α ; − is derivable for any α . If Γ `` v1 : σ ; β0 ; β1 is derivable, thenΓ `` v1 : σ ; α ; β1 is derivable for any α .
This lemma can be proven immediately. We then state two lemmas about substitution, which are used in the proof of subject reduction.
Lemma 2 (Substitution for monomorphic variable). If Γ1 `0 v : σ ; α0 ; − andΓ1 , Γ2 , (x : σ )0 `L e : τ ; β0 ; β1 are derivable, Γ1 , Γ2 `L e[v/x] : τ ; β0 ; β1 is derivable.
Lemma 3 (Substitution for polymorphic variable). If Γ1 `0 v : σ ; [ ] and Γ1 , Γ2 , (x :∀t.∀`.σ )0 `L e : τ ; ; β0 ; β1 are derivable, t1 , · · · ,tn ∈ FTV(σ )−FTV(Γ ) and `1 , · · · , `k ∈FC(σ ) − FC(Γ ), then Γ1 , Γ2 `L e[v/x] : τ ; ; β0 ; β1 is derivable.
These lemmas can be proven by structural induction on the second derivation, resp.
The next lemma is necessary to prove subject reduction for the case of the run construct.
First, we introduce an auxiliary definition ⇓` for elements of typing contexts, definedas:def(x : σ )0 ⇓` = (x : σ )0
def

(x : υ )` ⇓` = (x : υ )0
0

0

def

(x : υ )` ⇓` = (x : υ )`if `0 6= `The definition extends to Γ ⇓` straightforwardly.
Lemma 4. Suppose Γ1 , Γ2 `` v1 : σ ; β0 ; β1 is derivable such that ` 6∈ FC(Γ1 , σ , β0 , β1 ),and Γ2 consists of the form (xi : τi )` such that ` 6∈ FC(τi ). Then we can derive Γ1 , Γ2 ⇓` `0
v1 : σ ; ; β1 ; −.
This lemma is proven by induction on the derivation of Γ1 , Γ2 `` v1 : σ ; β0 ; β1 . As
its corollary, we obtain:
XIII

Corollary 1. Suppose Γ `` v1 : σ ; β0 ; β1 is derivable such that ` 6∈ FV(Γ , σ , β0 , β1 ),then we can derive Γ `0 v1 : σ ; β1 ; −.
Finally, we state the subject reduction property.
Theorem 1 (Subject Reduction). If Γ `0 e : τ ; β0 ; − is derivable and eΓ `0 e0 : τ ; β0 ; − is derivable.

∗ e0 , then

Proof. (very brief sketch) We prove the theorem by induction on the number of reduction steps, and case analysis of reductions.
For the reduction rules of shift (when shift captures a continuation up to the nearest
reset), we have the important observation: for any type derivation of a pure context F i j(i, j = 0, 1), there are no (explicit or implicit) level-0 resets and no level-0 binders which
enclose the hole. Moreover, there are no binders of the same level. Then by induction on
F i j , we can prove that the level-0 answer type does not change through this derivation.
By using this fact, we can prove the subject reduction property for this case.
The cases for β and let reductions are handled by Lemmas 2 and 3. Other cases areproven straightforwardly.
The progress property states that a closed well-typed express does not get stuck.
Theorem 2 (Progress). If `0 e : τ ; τ ; − is derivable, there exists an expression e1
such that {e} e1 .
Proof. (sketch) We first prove by induction that, for any typable expression e, it is avalue, a reducible expression, or a stuck expression E 00 [Sk.e0 ].
Then, we can prove that {e} is always a redex.

7 Principal Type and Type InferenceType inference is an important feature for ML-like languages, and it is even more important for our calculus, since we need to keep track of the effects of an expression
as type annotation. In this section we briefly mention the type inference algorithm for
DC .
λlet
Calcagno, Moggi and Taha [2] proposed the calculus λ i and its polymorphic versioniλlet , which is slightly less expressive than the earlier calculus λ α by Taha and Nielsen,
i ). λ i is suitable as the foundation of
but has principal typing (or principal type for λlet
multi-stage programming languages, as demonstrated by the success of the MetaOCaml
language.
DC also has the principal type property, and a sound and complete
Our calculus λlet
type inference algorithm similar to the algorithm W.
Given an expression e, a type context Γ and a level L, we say (θ , σ , α , β ) is asolution for these data if and only if θ is a substitution for type variables and classifiers,σ , α , β are types, and Γ `L e : σ ; α ; β is derivable.
Proposition 1 (Principal Type). Suppose there is a solution for an expression e, a typecontext Γ , and a level L. Then there exists a principal solution (θ0 , σ0 , α0 , β0 ) for them,
namely, for any solution (θ1 , σ1 , α1 , β1 ) for the same input, there exists a substitution φsuch that θ1 = θ0 φ , σ1 = σ0 φ , α1 = α0 φ and β1 = β0 φ .
XIVHere we slightly generalized the statement of the theorem than the standard form sothat the inductive proof goes through.
Proof. (sketch) We can construct a Hindley-Milner’s style type inference algorithm for
DC . This is due to the “implicit reset” approach, since we no longer have to infer the
λlet(semantic) purity in the process of type inference.
The only difficulty in constructing the algorithm is the case for the run rule, which
has the negative side condition ` 6∈ FV(Γ , σ ). To see how our algorithm handle this case,let us consider the expression run e under the context Γ and the level L. We first infer
the type of e under Γ and L. Suppose we get (θ0 , σ0 , α0 , β0 ) as the answer. Then we
unify σ0 with <σ 0 /σ 0 >` for a fresh σ 0 and so on. We check if the classifier ` appears in
the results or not. The algorithm fails to infer a type if ` appears in a wrong place of theresults, and continues otherwise. In the latter case, the future process of type inference
does not unify ` to other classifiers, so the side condition ` 6∈ FV(Γ , σ ) will remain valid.
Hence we can build a W-like type inference algorithm. The proof of soundness andcompleteness of the algorithm is as standard.

8

Conclusion

We have designed a polymorphic type system for multi-stage calculus with delimitedcontrol operators where polymorphism in types and that in classifiers are expressible.
The calculus in this paper extends Kameyama, Kiselyov and Shan’s calculus in that(besides polymorphism) we have the run construct. The key idea of integrating theseconflicting concepts into one calculus is to relax the value restriction to the syntactic
purity restriction, and then introduce the notion of implicit resets. We have proven typesoundness and the existence of principal types, both of which are essential to make ourlanguage usable.
The success of this combination strongly owes to the local nature of computational
effects by shift and reset: we can represent, in particular, mutable variables in terms ofshift and reset, but their scope is local to a certain block in a program. By placing asufficiently many resets (on the borders of polymorphism and run), we have obtained a
type-safe polymorphic calculus.
We mention other approaches to design type-safe multi-stage calculi with control
effects. Kim, Yi and Calcagno [8] proposed a polymorphic modal type system for Lisplike languages. Since their calculus has quite different flavors in nature (for instance,
α -equivalence is not admissible in their calculus, while it is built in our calculus), it isleft for future work to compare these two different lines of works.
Recently Westbrook et al. [16] designed a multi-stage programming language Mint
as an extension of Java. To ensure type safety, they introduced the notion of weak separability. Despite the difference of underlying languages, it will be interesting to compare
their conditions with ours so that we can build an even more powerful, and type-safe
calculus.
XVAcknowledgments
We would like to thank Kenichi Asai, Atsushi Igarashi, Oleg Kiselyov, Chung-chieh
Shan, and Kwangkeun Yi. We also thank anonymous reviewers for constructive comments. The second author is supported in part by JSPS Grant-in-Aid for Scientific Research (B) 21300005.

References
1. K. Asai and Y. Kameyama. Polymorphic Delimited Continuations. In Proc. Asian Programming Languages and Systems, LNCS 4807, pages 239–254, Nov-Dec 2007.
2. Cristiano Calcagno, Eugenio Moggi, and Walid Taha. Ml-like inference for classifiers. In
ESOP, pages 79–93, 2004.
3. Olivier Danvy and Andrzej Filinski. Abstracting control. In LISP and Functional Programming, pages 151–160, 1990.
4. Rowan Davies. A temporal logic approach to binding-time analysis. In LICS, pages 184–195,
1996.
5. Rowan Davies and Frank Pfenning. A modal analysis of staged computation. Journal of theACM, 48(3):555–604, May 2001.
6. Andrzej Filinski. Representing Monads. In Proc. 21st Symposium on Principles of Programming Languages, pages 446–457, 1994.
7. Yukiyoshi Kameyama, Oleg Kiselyov, and Chung-chieh Shan. Shifting the stage: staging
with delimited control. In PEPM, pages 111–120, 2009.
8. Ik-Soon Kim, Kwangkeun Yi, and Cristiano Calcagno. A polymorphic modal type system
for lisp-like multi-staged languages. In POPL, pages 257–268, 2006.
9. Oleg Kiselyov, Chung-chieh Shan, and Amr Sabry. Delimited dynamic binding. In John H.
Reppy and Julia L. Lawall, editors, ICFP, pages 26–37. ACM, 2006.
10. Keisuke Sugiura and Yukiyoshi Kameyama. Multi-stage language with control effect andcode execution (in Japanese). Computer Software (Journal of Japan Society of Software
Science and Technology), 28(1):217–229, 2011.
11. Walid Taha. A gentle introduction to multi-stage programming. In Domain-Specific Program
Generation, pages 30–50, 2003.
12. Walid Taha. A Gentle Introduction to Multi-stage Programming, Part II. In GTTSE, pages
260–290, 2007.
13. Walid Taha and Michael F. Nielsen. Environment classifiers. In POPL, pages 26–37, 2003.
14. Hayo Thielecke. From control effects to typed continuation passing. In POPL, pages 139–
149, New York, January 2003. ACM Press.
15. Takeshi Tsukada and Atsushi Igarashi. A logical foundation for environment classifiers.
Logical Methods in Computer Science, 6(4:9):1–43, 2010.
16. Edwin Westbrook, Mathias Ricken, Jun Inoue, Yilong Yao, Tamer Abdelatif, and Walid Taha.
Mint: Java multi-stage programming using weak separability. In PLDI, pages 400–411, 2010.
17. Yosihiro Yuse and Atsushi Igarashi. A modal type system for multi-level generating extensions with persistent code. In PPDP, pages 201–212, 2006.

XVI