Polymorphic Delimited Continuations
Kenichi Asai1 and Yukiyoshi Kameyama2
1

Department of Information Science, Ochanomizu University
asai@is.ocha.ac.jp
2
Department of Computer Science, University of Tsukuba
kameyama@acm.org

Abstract. This paper presents a polymorphic type system for a language with delimited control operators, shift and reset. Based on themonomorphic type system by Danvy and Filinski, the proposed type system allows pure expressions to be polymorphic. Thanks to the explicit
presence of answer types, our type system satisﬁes various important
properties, including strong type soundness, existence of principal types
and an inference algorithm, and strong normalization. Relationship to
CPS translation as well as extensions to impredicative polymorphism
are also discussed. These technical results establish the foundation ofpolymorphic delimited continuations.
Keywords: Type System, Delimited Continuation, Control Operator,
CPS Translation, Predicative/Impredicative Polymorphism.

1

Introduction

Delimited continuation operators enable us to manipulate control of programsin a concise manner without transforming them into continuation-passing style(CPS). In particular, shift and reset, introduced by Danvy and Filinski [6], havestrong connection to CPS, and thus most of the control eﬀects compatible with
CPS can be expressed using shift and reset [8]. They have been used, for example,
to program backtracking [6], A-normalization in direct style [1], let-insertion inpartial evaluation [1], and type-safe “printf” in direct style [2].
Despite the increasing interest in the use of delimited continuations in typed
programming languages, there has been little work that investigates their basic
properties without sacriﬁcing their expressive power. The original type system
for shift and reset by Danvy and Filinski [5] is the only type system that allows
modiﬁcation of answer types but is restricted to monomorphic types. Polymorphism in the presence of call/cc has been discussed in the context of ML [11]but strong type soundness [21] does not hold for their type system. Gunter,Rémy, and Riecke [10] proposed typed cupto operator with strong type soundness theorem as well as various properties, but their type system is restricted toa ﬁxed answer type for each prompt. As such, none of the above type systems
can type check, for instance, the “printf” program written with shift and reset.
To establish the basic properties of shift and reset without sacriﬁcing theirexpressive power, we present in this paper a polymorphic type system, an extension of the monomorphic type system by Danvy and Filinski, and show that

it satisﬁes a number of basic properties needed to use them in ordinary programming languages. In particular, we show strong type soundness, existence ofprincipal types and an eﬃcient type inference algorithm, and strong normalization among others. The polymorphism does not break the semantic foundationof the original monomorphic type system: CPS translation is naturally deﬁned
for our polymorphic calculus and preserves types and equivalence. Because of its
natural connection to CPS, our framework can be extended to a calculus withimpredicative polymorphism [9].
Unrestricted polymorphism in the presence of control operators leads to anunsound type system [11]. We introduce and employ a new criteria called “purity” restriction instead of more restrictive value restriction. An expression issaid to be pure if it has no control-eﬀects [18]. By allowing pure expressions to
be polymorphic, an interesting non-value term can be given a polymorphic type.
Based on these results, we have implemented a prototypical type inference
algorithm, and applied it to many interesting programs to obtain their principal
types.
The rest of this paper is organized as follows: Section 2 illustrates a few
programming examples to give intuition about the type structure for shift andreset. In Section 3, we formalize a predicatively polymorphic calculus for shift
and reset, and prove its properties such as type soundness. We then study a CPS
translation for our calculus in Section 4. In Section 5, we extend our study tocover impredicative polymorphism under two evaluation strategies. In Section 6,
we compare our work with related work and give conclusion. Proofs of theorems
in this paper can be found in the extended version of this paper [3].

2Programming Examples

Polymorphism is inevitable in programming [17]. A simple example of polymorphism is found in list manipulating functions: a reverse function works for alist of elements of any type. In this section, we introduce the control operators,
shift and reset, and show examples of polymorphism that involves control
operators.
2.1

List Append: Answer Type Modiﬁcation

Consider the following program [5] written in OCaml syntax:
let rec append lst = match lst with[] -> shift (fun k -> k)| a :: rest -> a :: append rest
This program is a curried version of list append, written with control operators.
Here, shift captures its current continuation and passes it to its argument(typically a one-argument function fun k -> . . .) in the empty context. Unlike
callcc, however, continuations are captured only up to its enclosing reset(hence called delimited continuations).
When append is invoked in a delimited context as follows:let append123 = reset (fun () -> append [1; 2; 3])append recursively stores each element of its argument into the control stack.
When all the elements are stacked, the control stack could be thought of as aterm with a hole: 1 :: 2 :: 3 :: •, waiting for the value for the [] case. Then, shift(fun k -> k) captures it, turns it into an ordinary function λx.1 :: 2 :: 3 :: x,
and returns it. The returned continuation append123 is the partially applied
append function: given a list, it appends 1, 2, and 3 to it in the reversed order.
When shift is used in a program, it typically has an impact on the answer
type of its enclosing context. Before shift (fun k -> k) is executed, the context 1 :: 2 :: 3 :: • was supposed to return a list (given a list for •). In other words,
the answer type of this context was a list. After shift (fun k -> k) is executed, however, what is returned is the captured continuation λx.1 :: 2 :: 3 :: xof type int list -> int list. In other words, execution of shift (fun k ->k) modiﬁes the answer type from ’a list to ’a list -> ’a list, where ’ais the type of the elements of the list.
To accommodate this behavior, Danvy and Filinski used a function typeof the form S / A -> T / B [5]. It is the type of a function from S to T, but
modiﬁes the answer type from A to B when applied. Using this notation, append
has the type ’a list / ’a list -> ’a list / (’a list -> ’a list) for
all ’a: given a list of type ’a list, append returns a list of type ’a list to its
immediate context; during this process, however, the answer type of the context
is modiﬁed from ’a list to ’a list -> ’a list.
Gunter, Rémy, and Riecke mention the type of context (prompt) in their typesystem [10]. However, they ﬁx the answer type and do not take the answer type
modiﬁcation into account, limiting the use of control operators. To characterize
the full expressive power of shift and reset, it is necessary to cope with two
answer types together with polymorphism.
2.2

List Preﬁx: Answer Type Polymorphism

Once answer types are included in a function type, polymorphism becomes more
important in programming. First of all, the conventional function type S -> T isregarded as polymorphic in the answer type [18]: S / ’a -> T / ’a for a new
type variable ’a. This indicates that even a simple, apparently monomorphic,
function like:let add1 x = x + 1
has to be treated as polymorphic in the answer type. Otherwise, it cannot be
used in diﬀerent contexts as in:reset (fun () -> add1 2; ()); reset (fun () -> add1 3; true)
The ﬁrst occurrence of add1 is used at type int / unit -> int / unit whereas
the second one at type int / bool -> int / bool. To unify them, add1 has
to be given a polymorphic type: int / ’a -> int / ’a.
Answer type polymorphism plays an important role in captured continuations, too. Consider the following program [4]:

let rec visit lst = match lst with[] -> shift (fun h -> [])| a :: rest -> a :: shift (fun k ->(k []) :: reset (k (visit rest)))let rec prefix lst = reset (visit lst)
When applied to a list, e.g., [1; 2 3], prefix returns a list of its preﬁxes: [[1];[1; 2]; [1; 2; 3]]. In this example, there are two occurrences of shift. Intuitively, the continuation captured by the second shift represents consing ofelements read so far. It is applied twice: once to an empty list to construct acurrent preﬁx and once to construct a list of longer preﬁxes. Finally, the ﬁrst
occurrence of shift initiates the construction of preﬁxes by returning an empty
list of type ’a list list, discarding the current continuation.
It is important that the captured continuation k is polymorphic in its answer
type. A closer look at the function reveals that k is used in two diﬀerent contexts:
the ﬁrst occurrence of k has type ’a list / ’a list list -> ’a list / ’alist list whereas the second one has type ’a list / ’a list -> ’a list
/ ’a list. This demonstrates that without answer type polymorphism in thecaptured continuations, the above program does not type check.
2.3

PrintfFinally, we present a type-safe printf program written in direct style with shift
and reset (detailed in [2]). Given a representation of types:
let int x = string_of_int x
let str (x : string) = x
the following program achieves the behavior of printf in a type-safe manner:
let % to_str = shift (fun k -> fun x -> k (to_str x))
let sprintf p = reset p
Namely, the following programs are all well-typed:
sprintf (fun () -> "Hello world!")
sprintf (fun () -> "Hello " ^ % str ^ "!") "world"
sprintf (fun () -> "The value of " ^ % str ^ " is " ^ % int) "x" 3
and give "Hello World!" for the ﬁrst two and "The value of x is 3" forthe last. Depending on % appearing in the formatting text, sprintf returns a
diﬀerent type of values.
The dependent behavior of sprintf is well understood by examining its type:(unit / string -> string / ’a) -> ’a. The formatting text is represented
as a thunk that modiﬁes the ﬁnal answer type into ’a according to the occurrenceof %. Then, the type of the return value of sprintf is polymorphic to this ’a.
The dependent behavior of sprintf is only achievable through the support ofboth the answer type modiﬁcation and polymorphism.

v ::= c | x | λx.e | fix f.x.e

value

e ::= v | e1 e2 | Sk.e | hei | let x = e1 in e2| if e1 then e2 else e3

expression

α, β, γ, δ ::= t | b | (α/γ → β/δ)monomorphic type

A ::= α | ∀t.A

polymorphic types/r

Fig. 1. Syntax of λlet .

3

Predicative Polymorphism with Shift/Reset

We now introduce polymorphic typed calculi for shift and reset, and study theirproperties such as type soundness. Following the literature, we distinguish two
versions of polymorphism: predicative polymorphism (let-polymorphism) foundin ML and impredicative polymorphism which is based on the second order
lambda calculus (Girard’s System F [9]). In this section, we give the predicatives/rversion λlet . The impredicative version will be given in later sections.
3.1

Syntax and Operational Semantics

We assume that the sets of constants (denoted by c), variables (denoted byx, y, k, f ), type variables (denoted by t), and basic types (denoted by b) aremutually disjoint, and that each constant is associated with a basic type. We
assume bool is a basic type which has constants true and false.
s/r
The syntax of λlet is given by BNF in Figure 1. A value is either a constant,a variable, a lambda abstraction, or a ﬁxpoint expression fix f.x.e which represents a recursive function deﬁned by the equation f (x) = e. The variables f andx are bound in fix f.x.e. An expression is either a value, an application, a shiftexpression, a reset expression, a let expression, or a conditional. The expressions
Sk.e and hei, resp., correspond to OCaml expressions shift (fun k -> e) andreset (fun () -> e), resp. Types are similar to those in ML except that thefunction type is now annotated with answer types as (α/γ → β/δ). Free andbound variables (type variables, resp.) in expressions (types, resp.) are deﬁned
as usual, and FTV(α) denotes the set of free type variables in α.
s/r
We give call-by-value operational semantics for λlet . First we deﬁne evaluation contexts (abbreviated as e-contexts), pure e-contexts, and redexes as follows:
E ::= [ ] | vE | Ee | hEi | let x = E in e | if E then e else ee-context
F ::= [ ] | vF | F e | let x = F in e | if F then e else epure e-context
R ::= (λx.e)v | hvi | hF [Sk.e]i | let x = v in e
| if true then e1 else e2 | if false then e1 else e2| (fix f.x.e)v

redex

(λx.e)v Ã e[v/x](fix f.x.e)v Ã e[fix f.x.e/f ][v/x]hvi Ã vhF [Sk.e]i Ã hlet k = λx.hF [x]i in ei
let x = v in e Ã e[v/x]if true then e1 else e2 Ã e1
if false then e1 else e2 Ã e2
s/r

Fig. 2. Reduction rules for λlet

A pure e-context F is an evaluation context such that no reset encloses the hole.
Therefore, in the redex hF [Sk.e]i, the outermost reset is guaranteed to be theone corresponding to this shift, i.e., no reset exists inbetween.
s/r
A one-step evaluation in λlet is E[R] Ã E[e] where R Ã e is an instanceof reductions in Figure 2 where e[v/x] denotes the ordinary capture-avoiding
substitution. For example, prefix [1; 2] is reduced as follows. (We use fix
implicitly through recursion, and assume that lists and other constructs areavailable in the language).
prefix [1; 2]
Ã h1 :: Sk.(k[] :: hk (visit [2])i)i
Ã hlet k = λx.h1 :: xi in k[] :: hk (visit [2])ii
Ã h(λx.h1 :: xi)[] :: h(λx.h1 :: xi)(visit [2])ii
Ã+ h[1] :: h(λx.h1 :: xi)(2 :: Sk.(k[] :: hk (visit [])i))ii
Ã h[1] :: hlet k = λx.h(λx.h1 :: xi)(2 :: x)i in k[] :: hk (visit [])iii
Ã h[1] :: h(λx.h(λx.h1 :: xi)(2 :: x)i)[] :: h(λx.h(λx.h1 :: xi)(2 :: x)i)(visit [])iii
Ã+ h[1] :: h[1; 2] :: h(λx.h(λx.h1 :: xi)(2 :: x)i)(Sh.[])iii
Ã h[1] :: h[1; 2] :: let h = λx.h(λx.h(λx.h1 :: xi)(2 :: x)i)xi in []ii
Ã h[1] :: h[1; 2] :: []ii Ã+ [[1]; [1; 2]]
The notion of reduction Ã is deﬁned as the compatible closure3 of those in
Figure 2, and Ã∗ (and Ã+ , resp.) denotes the reﬂexive-transitive (transitive,
resp.) closure of Ã.
3.2

Type System

We begin with Danvy and Filinski’s monomorphic type system for shift andreset [5]. Since the evaluation of an expression with shift and reset may modify
answer types, a type judgment in their type system involves not only a type of3

A binary relation is compatible if it is closed under term-formation, for instance,
whenever e1 and e2 are related by this relation, λx.e1 and λx.e2 are related.

an expression being typed, but also answer types before and after evaluation.
Symbolically, a judgment takes the form:
Γ; α ` e : τ; βwhich means that, under the type context Γ , the expression e has type τ andthe evaluation of e changes the answer type from α to β. A rationale behind thisformulation is that, the CPS counterpart of e has type (τ ∗ → α∗ ) → β ∗ under
the type context Γ ∗ in the simply typed lambda calculus, where ( )∗ is the CPS
translation for types and type contexts deﬁned in the next section.
Introducing polymorphism into their type system is, however, not straightforward since the subject reduction property fails for the system with unrestricted
uses of let-polymorphism and side eﬀects such as references and control eﬀects.
In the literature, there are many proposals to solve this problem by restricting
the let-expression let x = e1 in e2 or by changing its operational semantics,
some of which are:– Value restriction [20]: e1 must be a value.
– Weak type variables [19]: the type variable in the type of e1 can be generalized only when it is not related to side eﬀects.
– Polymorphism by name [15]: the evaluation of e1 is postponed until x is
actually used in e2 , thus enforcing the call-by-name evaluation to e1 .
We take an alternative approach: we restrict that e1 in let x = e1 in e2
must be free from control eﬀects, that is, pure. Intuitively, an expression is purewhen it is polymorphic in answer types.4 In Danvy and Filinski’s type system,
we can deﬁne that e is pure if the judgment Γ ; α ` e : τ ; α is derivable forany type α. Typical examples of pure expressions are values but the expression
hei is also pure, since all control eﬀects in e are delimited by reset. To represent
purity of expressions, we introduce a new judgment form Γ `p e : τ .
s/r
Now let us formally deﬁne the type system of λlet . A type context (denoted byΓ ) is a ﬁnite list of the form x1 : A1 , · · · , xn : An where the variables x1 , · · · , xn
are mutually distinct, and A1 , · · · , An are (polymorphic) types. Judgments areeither one of the following forms:Γ `p e : τΓ; α ` e : τ; βjudgment for pure expression
judgment for general expression
s/r

Figure 3 lists the type inference rules of λlet where τ ≤ A in the rule (var)means the instantiation of type variables by monomorphic types. Namely, if A ≡∀t1 . · · · ∀tn .ρ for some monomorphic type ρ, then τ ≡ ρ[σ1 , · · · , σn /t1 , · · · , tn ]for some monomorphic types σ1 , · · · , σn . The type Gen(σ; Γ ) in the rule (let) is
deﬁned by ∀t1 . · · · ∀tn .σ where {t1 , · · · , tn } = FTV(σ) − FTV(Γ ).
4Thielecke studied the relationship between answer type polymorphism and the absence of control in depth [18].

(x : A ∈ Γ and τ ≤ A)var
Γ `p x : τ(c is a constant of basic type b)constΓ `p c : b

Γ, f : (σ/α → τ /β), x : σ; α ` e : τ ; βﬁxΓ `p fix f.x.e : (σ/α → τ /β)Γ, x : σ; α ` e : τ ; βfunΓ `p λx.e : (σ/α → τ /β)Γ ; γ ` e1 : (σ/α → τ /β); δ Γ ; β ` e2 : σ; γapp
Γ ; α ` e1 e2 : τ ; δΓ, k : ∀t.(τ /t → α/t); σ ` e : σ; βshift
Γ ; α ` Sk.e : τ ; βΓ `p e : τexp
Γ; α ` e : τ; α

Γ ; σ ` e : σ; τresetΓ `p hei : τΓ `p e1 : σ Γ, x : Gen(σ; Γ ); α ` e2 : τ ; βlet
Γ ; α ` let x = e1 in e2 : τ ; β
Γ ; σ ` e1 : bool; β Γ ; α ` e2 : τ ; σ Γ ; α ` e3 : τ ; σif
Γ ; α ` if e1 then e2 else e3 : τ ; β
s/rFig. 3. Type Inference Rules of λlet .

The type inference rules are a natural extension of the monomorphic typesystem by Danvy and Filinski [5]. Pure expressions are deﬁned by one of therules (ﬁx), (fun), or (reset).5 They can be freely turned into general expressions
through the rule (exp). Pure expressions can be used polymorphically throughthe rule (let). It generalizes the standard let-polymorphism found in ML. We
can allow a let expression let x = e1 in e2 even when e1 is not pure, in whichcase it is macro-expanded to (λx.e2 )e1 where e1 is treated monomorphically.
Finally, the rule (shift) is extended to cope with the answer type polymorphismof captured continuations: k is given a polymorphic type ∀t.(τ /t → α/t).
Examples. We show the principal types for the examples shown in Section 2.
Using the type inference rules (augmented with rules for lists, etc.), we candeduce that append (rewritten with fix) has type ’a list / ’b -> ’a list /(’a list -> ’b),6 where ’a list -> ’b is a shorthand for ’a list / ’c ->’b / ’c for a new type variable ’c. Given this type, the type of append123, i.e.,
reset (fun () -> append [1; 2; 3]), becomes int list -> int list (orint list / ’c -> int list / ’c). Since it is pure, append123 can be givena polymorphic type in its answer type ’c. Notice that append123 is not boundto a value but an eﬀectful expression enclosed by reset. If we employed value
restriction, append123 could not be polymorphic, and thus could only be used
in a context with a ﬁxed answer type.
We could have introduced a more general rule such as: if Γ ; t ` e : τ ; t is derivablefor t 6∈ FTV(Γ, τ ), then Γ `p e : τ . It would then allow expressions that are notsyntactically values nor reset expressions but in fact pure, such as Sk.k3. We did
not take this approach, because we can always insert reset around pure expressions
to make them syntactically pure.
6This is the principal type for append. In the typical case where the call to append isimmediately enclosed by reset as is the case for append123, ’b is instantiated to ’a
list.

5

Next, the principal type for visit is ’a list / ’b -> ’a list / ’b list.7
To deduce this type, we need to use the rule (shift) to give k a polymorphic type
in its answer type. Then, the type of prefix becomes ’a list -> ’a list
list. In other words, it accepts a list of any type ’a. Since it is pure (that is,
answer type polymorphic), it can be used in any context.
Finally, the principal type for % is somewhat complicated:(’a / ’p -> ’s / ’q) / ’t -> ’s / (’a / ’p -> ’t / ’q)
In the typical case where to_str is pure (’p=’q) and has type ’a -> string,and the output ’t is string, the above type becomes:(’a -> string) / string -> string / (’a -> string)This type describes the behavior of %: given a representation of a type (of type ’a-> string), it changes the answer type from string to a function that receives
a value of the speciﬁed type ’a. Then, sprintf returns a function of this ﬁnal
answer type, thus accepting an argument depending on the occurrence of %.
3.3

Propertiess/r

We have introduced the polymorphic calculus λlet with shift and reset. We
claim that our calculus provides a good foundation for studying the interaction
between polymorphism and delimited continuations. To support this claim, we
prove the following properties:– Subject reduction (type preservation).
– Progress and unique decomposition.
– Principal types and existence of a type inference algorithm.
– Preservation of types and equality through CPS translation.
– Conﬂuence.
– Strong normalization for the subcalculus without fix.
We ﬁrst show type soundness, i.e., subject reduction and progress.
Theorem 1 (Subject Reduction). If Γ ; α ` e1 : τ ; β is derivable and e1 Ã∗
e2 , then Γ ; α ` e2 : τ ; β is derivable. Similarly, if Γ `p e1 : τ is derivable ande1 Ã∗ e2 , then Γ `p e2 : τ is derivable.
The above theorem not only assures that a well-typed program does not go wrong(so-called weak type soundness [21]) but also guarantees that the evaluated term
has the same type as the original term (strong type soundness [21]). This is theconsequence of having answer types explicitly in our type system. We need threelemmas to prove this theorem.
Lemma 1 (Weakening of Type Context). Suppose Γ1 ⊂ Γ2 and Γ2 is avalid type context. If Γ1 ; α ` e : σ; β is derivable, then Γ2 ; α ` e : σ; β isderivable. Similarly for Γ1 `p e : σ.
7

Again, ’b is typically instantiated to ’a list.

Lemma 2 (Substitution for Monomorphic Variables). Suppose Γ1 ⊂ Γ2 ,
Γ2 is a valid type context, and Γ1 `p v : σ is derivable.
If Γ2 , x : σ; α ` e : τ ; β is derivable, then Γ2 ; α ` e[v/x] : τ ; β is derivable.
Similarly, if Γ2 , x : σ `p e : τ is derivable, then Γ2 `p e[v/x] : τ is derivable.
Lemma 3 (Substitution for Polymorphic Variables). Suppose Γ1 ⊂ Γ2 ,
Γ2 is a valid type context, and Γ1 `p v : σ is derivable.
If Γ2 , x : Gen(σ; Γ1 ); α ` e : τ ; β is derivable, then Γ2 ; α ` e[v/x] : τ ; β isderivable. Similarly for Γ2 , x : Gen(σ; Γ1 ) `p e : τ .
We next prove the progress property, which states that evaluation of a program does not get stuck. Although a program is usually deﬁned as an expression
with no free variables, we need to reﬁne it, since, for instance, Sk.k3 cannot
be reduced further due to the absence of an enclosing reset. Here, we deﬁne a
program to be an expression with a toplevel reset of the form hei which has nofree variables.
Theorem 2 (Progress and Unique Decomposition). If `p hei : τ is derivable, then either e is a value, or hei can be uniquely decomposed into the form
E[R] where E is an evaluation context and R is a redex.
By Theorems 1 and 2, we can conclude that our type system is sound (TypeSoundness).
Although our type system may look rather complex, we can smoothly extend
s/r
Hindley-Milner type inference algorithm W to accommodate λlet . The extended
algorithm W 0 takes two arguments as its inputs: Γ (for a valid context) and e(for a raw expression) such that all free variables in e are contained in Γ . Then,W 0 either fails or returns a tuple (θ; α, τ, β) where θ is a substitution for typevariables, and α, τ , and β are types.
Theorem 3 (Principal Type and Type Inference). We can construct a
s/r
type inference algorithm W 0 for λlet such that:0
1. W always terminates.
2. if W 0 returns (θ; α, τ, β), then Γ θ; α ` e : τ ; β is derivable. Moreover, forany (θ0 ; α0 , τ 0 , β 0 ) such that Γ θ0 ; α0 ` e : τ 0 ; β 0 is derivable, (Γ θ0 , α0 , τ 0 , β 0 ) ≡(Γ θ, α, τ, β)φ for some substitution φ.
3. if W 0 fails, then Γ θ; α ` e : τ ; β is not derivable for any (θ; α, τ, β).
We have implemented a prototypical type inference algorithm system for our
language based on this theorem. The principal types shown in Section 3.2 are
all inferred by it.
s/rFinally, we can show conﬂuence for λlet , and strong normalization for thesubcalculus without fix. This is in contrast to cupto operator, where strong
normalization does not hold.8
Theorem 4 (Conﬂuence and Strong Normalization).
s/r
1. The reduction Ã in λlet is conﬂuent.
s/r
2. The reduction Ã in λlet without fix is strongly normalizing.
8

See http://okmij.org/ftp/Computation/Continuations.html#cupto-nontermination.

b∗ = b∗t =t

for a basic type b
for a type variable t((α/γ → β/δ))∗ = α∗ → (β ∗ → γ ∗ ) → δ ∗(∀t.A)∗ = ∀t.A∗(Γ, x : A)∗ = Γ ∗ , x : A∗
Fig. 4. CPS translation for types and type contexts.
c∗ = cv∗ = v(λx.e)∗ = λx.[[e]](fix f.x.e)∗ = fix f.x.[[e]][ v]] = λκ.κv ∗[ e1 e2 ] = λκ.[[e1 ] (λm.[[e2 ] (λn.mnκ))[ Sk.e]] = λκ.let k = λnκ0 .κ0 (κn) in [ e]](λm.m)[ hei]] = λκ.κ([[e]](λm.m))[ let x = e1 in e2 ] = λκ.let x = [ e1 ] (λm.m) in [ e2 ] κ[ if e1 then e2 else e3 ] = λκ.[[e1 ] (λm.if m then [ e2 ] κ else [ e3 ] κ)
Fig. 5. CPS translation for values and expressions.

4s/r

CPS translation of λlet

The semantics of control operators have often been given through a CPS translation. In their ﬁrst proposal, Danvy and Filinski gave the precise semantics ofshift and reset in terms of a CPS translation [6, 7]. In this section, we show thatit can be naturally extended to polymorphic setting.
Harper and Lillibridge [12] were the ﬁrst to systematically study CPS translations in polymorphic language with control operators. They introduced CPS
translations from F ω+call/cc to F ω, and proved that, under a condition similar to the value restriction, a call-by-value CPS translation preserves types
and semantics (equality). We follow Harper and Lillibridge to give a type-andequality preserving CPS translation for polymorphic calculi with shift and reset.
s/r
The CPS translation for λlet is a Plotkin-style, call-by-value translation,and is deﬁned in Figures 4 and 5, where the variables κ, m and n are fresh.
The target calculus (the image) of the translation is λlet , the minimum lambda
calculus with let-polymorphism and conditional expressions.99s/r

λlet may be obtained from λlet by eliminating shift, reset, and answer types α andβ in Γ ; α ` e : τ ; β and (σ/α → τ /β). Since all expressions are pure in λlet , we do
not distinguish two kinds of judgments.

The type (α/γ → β/δ) is translated to the type of a function which, given
a parameter of type α∗ and a continuation of type β ∗ → γ ∗ returns a value oftype δ ∗ . For instance, the type of the visit function (in the prefix example)’a list / ’b -> ’a list / ’b list is CPS translated to ’a list -> (’alist -> ’b) -> ’b list.
The translation of reset is the same as that in Danvy and Filinski’s. For
shift, we use a let-expression rather than substitution, so that the captured
continuation λnκ0 .κ0 (κn) may be used polymorphically in the body [ e]](λm.m).
This is essential to retain enough polymorphism for delimited continuations.
The translation of the let expression let x = e1 in e2 needs care to takepolymorphism into account. We use a let-expression to express the polymorphismin the source term, and supply the identity continuation λm.m to the CPS
transform [ e1 ] . This is typable in the target calculus, since a pure expression istranslated to an expression of type ∀t.((τ → t) → t).
We can prove that the CPS translation preserves types and equality:
s/r

Theorem 5 (Preservation of Types). If Γ ; α ` e : τ ; β is derivable in λlet ,then Γ ∗ ` [ e]] : (τ ∗ → α∗ ) → β ∗ is derivable in λlet .
s/r
If Γ `p e : τ is derivable in λlet , then, Γ ∗ ` [ e]] : (τ ∗ → γ) → γ is derivable
for an arbitrary type γ in λlet .
Theorem 6 (Preservation of Equality). If Γ ; α ` e1 : τ ; β is derivables/r
and e1 Ã∗ e2 in λlet , then [ e1 ] = [ e2 ] in λlet where = is the least congruence
relation which contains Ã in λlet .10

5Impredicative Polymorphism with Shift and Reset

The second order lambda calculus (Girard’s System F) is a solid foundation foradvanced concepts in programming languages, since its impredicative polymorphism is strictly more expressive than the predicative one. In this section, westudy an extension of (call-by-value version of) System F with shift and reset.
It is an explicitly typed calculus rather than an implicitly typed calculus likes/r
λlet . Hence, we add two constructs to the expressions: Λt.e for type-abstractionand e{α} for type-application. Following Harper and Lillibridge [12], we consider
two calculi with impredicative polymorphism that diﬀer in evaluation strategies.
s/r,Std
The ﬁrst calculus, λ2, adopts the “standard” strategy: Λt.e is treated as as/r,M Lvalue, and hence we do not evaluate under Λ. The second one, λ2, adopts
the “ML-like” strategy: Λt.e is a value only when e is a value, and hence weevaluate under Λ.
s/r,Stds/r,M Ls/r
The syntax of λ2
and λ2extends that of λlet with the new constructs listed in Figure 6. We annotate bound variables with types, for instance,
λx : α. e. We eliminate let expressions, since they can be macro-deﬁned: fors/rinstance, the expression let f = λx.x in (f f )0 in λlet is represented11 as
10
11

The reduction Ã in λlet is the reduction Ã restricted to the expressions in λlet .
We assume that 0 is a constant of type int.

α, β, γ, δ ::= · · · | ∀t.α::= · · · | ∀t.αv ::= · · · | Λt.e::= · · · | Λt.v

e ::= · · · | e{α}::= · · · | Λt.e | e{α}s/r,Std

λ2(standard)values/r,M L

(ML-like)

s/r,Stdand λ2

λ2

Fig. 6. Syntax of λ2Γ `p e : τtabs, t 6∈ FTV(Γ )Γ `p Λt.e : ∀t.τtypes/r,M Lexpression.

Γ ; α ` e : ∀t.τ ; βtapp
Γ ; α ` e{σ} : τ [σ/t]; βFig. 7. Type inference rules for new constructs.

(λf : ∀t.(t → t). f {int → int}(f {int})0)(Λt.λx : t. x). Monomorphic andpolymorphic types are merged, since the type quantiﬁer ∀ may occur at any
place in types. The deﬁnitions for values and expressions reﬂect the diﬀerence
between the two calculi.
s/r,Std
The type inference rules for new constructs are common to λ2
ands/r,M Lλ2
, and are given in Figure 7. As can be seen by the rule (tabs), thes/r,M L, this restriction isbody e in Λt.e is restricted to a pure expression. For λ2
12necessary to ensure the type soundness due to a similar reason as Harper and
Lillibridge [12] who proposed to put a kind of value restriction when abstracting types. Unfortunately, their calculus under the value restriction is not very
interesting, since the standard and ML-like strategies completely agree on the
restricted calculus. We relax the restriction so that e in Λt.e may be an arbitrary
pure expression, which makes the two strategies diﬀer on some expressions.
Operational semantics is deﬁned in Figure 8 with a new reduction rule:(Λt.e){α} Ã e[α/t]s/r,M L,
where e[α/t] denotes the capture-avoiding substitution for types. For λ2
the subexpression e in the reduction rule is restricted to a value.
s/r,Std
Polymorphism in λ2
is a generalization of Leroy’s “polymorphism byname” [15]: consider the expression let f = hei in (f f )0 for an expression eof type t → t and a constant 0 of type int. It is represented by (λf : ∀t.(t →s/r,Stdt).(f {int → int})(f {int})0)(Λt.hei) in λ2, and it is easy to see that theevaluation of e is postponed until a type is applied to Λt.hei.
s/r,M L
Polymorphism in λ2
is a generalization of that for ML. Taking thesame example, the outermost β-redex is computed only after hei is computed
and returns a value. Then, the variable f is substituted for the value of Λt.hei,
and the body (f {int → int})(f {int})0 is computed.
12s/r,StdFor λ2, the restriction is not necessary, and we could have deﬁned a more liberal
type system. In the present paper, however, we choose a uniform, simpler syntax.

E ::= · · · | E{α}::= · · · | E{α} | Λt.E

F ::= · · · | F {α}::= · · · | F {α}R ::= · · · | (Λt.e){α}::= · · · | (Λt.v){α}s/r,Std
λ2e-context
pure e-context
redexs/r,M L
λ2

Fig. 8. Evaluation Contexts and Redexes.

(∀t.τ )∗ = ∀t.∀s.((τ ∗ → s) → s) for a fresh type variable s[ Λt.e]]α,∀t.τ,α = λκ : ((∀t.τ )∗ → α).κ(Λt.Λs.[[e]]s,τ,s )[ e{σ}]]α,τ [σ/t],β = λκ : ((τ [σ/t])∗ → α∗ ).[[e]]α,∀t.τ,β (λu : (∀t.τ )∗ .u{σ ∗ }{α∗ }κ)s/r,Std

Fig. 9. CPS translation for λ2.

(∀t.τ )∗ = ∀t.τ ∗[ Λt.e]]α,∀t.τ,α = λκ : ((∀t.τ ∗ ) → α).κ(Λt.[[e]]τ,τ,τ (λm : τ ∗ .m))
[ e{σ}]]α,τ [σ/t],β = λκ : ((τ [σ/t])∗ → α∗ ). [ e]]α,∀t.τ,β (λu : ∀t.τ ∗ .κ(u{σ ∗ }))s/r,M L

Fig. 10. CPS translation for λ2

s/r,Std

We can show type soundness for λ2.

s/r,M Land λ2.

Theorem 7 (Type Soundness). Subject reduction property and progress props/r,M L
s/r,Std.
and λ2erty hold for λ2
s/r,Stds/r,M Lin Figures 9 andand λ2
We deﬁne a CPS transformation for λ2
10. The target calculus of the translation is System F augmented with basic
types, constants, fix and conditionals. Equality of the target calculus is theleast congruence relation which includes call-by-value βη-equality, β-equality
for types ((Λt.e){α} = e[α/t]), and equality for fix and conditionals. Since
the target calculus is explicitly typed, the CPS translation for expressions isannotated by types as [ e]]α,τ,β , which is well-deﬁned when Γ ; α ` e : τ ; β isderivable for some Γ . It is interesting to see how the diﬀerence of evaluation
strategies aﬀect the diﬀerence of CPS translations in Figures 9 and 10.
s/r,M L
Note that the CPS translation for λ2
is a natural extension of that fors/rs/r
λlet : for instance, [ let f = hei in (f f )0]] in λlet is equal (up to the call-by-values/r,Stdβη-equality) to [ (λf : ∀t.(t → t).(f {int → int})(f {int})0)(Λt.hei)]] in λ2.
We can show that the CPS transformations for the two calculi preserve typess/r,Stds/r,M Land equality. Let T be λ2
or λ2.

Theorem 8 (Preservation of Types and Equality).
1. If Γ ; α ` e : τ ; β is derivable in T , then Γ ∗ ` [ e]]α,τ,β : (τ ∗ → α∗ ) → β ∗ isderivable in the target calculus.
2. If Γ `p e : τ is derivable in T , then Γ ∗ ` [ e]]s,τ,s : (τ ∗ → s) → s is derivable
for any type variable s in the target calculus.
3. If Γ ; α ` e : τ ; β is derivable in T , and e Ã∗ e0 , then [ e]]α,τ,β = [ e0 ] α,τ,βunder the equality of the target calculus.

6

Conclusion

We have introduced predicative and impredicative polymorphic typed calculi
for shift and reset, and investigated their properties such as type soundness
and relationship to CPS translations. We have extended Danvy and Filinski’s
monomorphic type system for shift and reset to polymorphic one, and haveshown that a number of pleasant properties hold for the polymorphic calculi.
We have shown that our calculi have a natural representation for the “purity”
of expressions, and that the purity restriction suﬃces for the type systems to besound, thus generalizing value restriction used in Standard ML and OCaml.
In the literature, a number of authors have tackled the unsoundness problemof polymorphism and eﬀects [19, 15, 20, 12]. We have proposed a simple solution
based on the notion of “purity”, which is, in the presence of the reset operator, less restrictive than the notion of “syntactic values” in ML. We have also
investigated two evaluation strategies for impredicative calculi, each of which
generalizes ML’s and Leroy’s solutions for the unsoundness problem.
Several authors have studied polymorphic calculi with control operators fordelimited continuations. Introducing polymorphism into a calculus with shift andreset has been implicit by Danvy who gave many programming examples (see,for instance, [4]). In fact, his interesting examples encouraged us to formulate thecalculi in the present paper. Filinski [8] implemented shift and reset in SML/NJ,
thus enabling one to write polymorphic functions with shift and reset. However,
the expressivity of his system is limited since the answer type is ﬁxed once andfor all. The same goes for the calculus with cupto by Gunter et al. [10]. Kiselyov
et al. [14] have implemented shift and reset in OCaml, and their examples madeuse of let-polymorphism. However, their paper did not give formal accounts forpolymorphism. As far as we know, the present paper is the ﬁrst to provide asystematic study on the interaction of polymorphism and control operators fordelimited continuations.
Although we believe that our calculus serves as a good foundation for studying polymorphic delimited continuations calculi, this is only the ﬁrst step; weneed deeper understanding and better theories. The ﬁrst author of the present
paper has studied logical relations based on Danvy and Filinski’s monomorphic
type system [1], but it is not apparent if his result extends to the polymorphic
case. Hasegawa [13] studied parametricity principle for the second order, callby-name λµ-calculus (similar to System F + call/cc), and obtained the notionof “focal parametricity”. Although he works in call-by-name, we hope to ﬁndsome connection between our work and his results in the future. A recent workby Mogelberg and Simpson [16] treats a similar notion in call-by-value.
Acknowledgments. We would like to thank Olivier Danvy and Masahito
Hasegawa for helpful comments and suggestions. This work was partly supported
by JSPS Grant-in-Aid for Scientiﬁc Research (C) 18500005 and 16500004.

References
1. K. Asai. Logical Relations for Call-by-value Delimited Continuations. In Trends
in Functional Programming, volume 6, pages 63–78, 2007.
2. K. Asai. On Typing Delimited Continuations: Three New Solutions to the Printf
Problem. 2007. Submitted. See http://pllab.is.ocha.ac.jp/~asai/papers/.
3. K. Asai and Y. Kameyama. Polymorphic Delimited Continuations. Technical
Report CS-TR-07-10, Dept. of Computer Science, University of Tsukuba, Sep 2007.
4. O. Danvy. An Analytical Approach to Program as Data Objects. DSc thesis, Department of Computer Science, University of Aarhus, Aarhus, Denmark, 2006.
5. O. Danvy and A. Filinski. A Functional Abstraction of Typed Contexts. Technical
Report 89/12, DIKU, University of Copenhagen, July 1989.
6. O. Danvy and A. Filinski. Abstracting Control. In Proc. 1990 ACM Conferenceon Lisp and Functional Programming, pages 151–160, 1990.
7. O. Danvy and A. Filinski. Representing Control: a Study of the CPS Transformation. Mathematical Structures in Computer Science, 2(4):361–391, 1992.
8. A. Filinski. Representing Monads. In POPL, pages 446–457, 1994.
9. J.-Y. Girard, Y. Lafont, and P. Taylor. Proofs and Types, volume 7 of Cambridge
Tracts in Theoretical Computer Science. Cambridge University Press, 1989.
10. C. A. Gunter, D. Remy, and J. G. Riecke. A Generalization of Exceptions andControl in ML-Like Languages. In FPCA, pages 12–23, 1995.
11. R. Harper, B. F. Duba, and D. MacQueen. Typing First-Class Continuations in
ML. J. Funct. Program., 3(4):465–484, 1993.
12. R. Harper and M. Lillibridge. Explicit polymorphism and CPS conversion. In
POPL, pages 206–219, 1993.
13. M. Hasegawa. Relational parametricity and control. Logical Methods in Computer
Science, 2(3), 2006.
14. O. Kiselyov, C. c. Shan, and A. Sabry. Delimited dynamic binding. In ICFP, pages
26–37, 2006.
15. X. Leroy. Polymorphism by name for references and continuations. In POPL,
pages 220–231, 1993.
16. R.E. Mogelberg and A. Simpson. Relational parametricity for computational effects. In LICS, 2007.
17. C. Strachey. Fundamental concepts in programming languages. International Summer School in Computer Programming, Copenhagen, Denmark, August 1967.
18. H. Thielecke. From Control Eﬀects to Typed Continuation Passing. In POPL,
pages 139–149, New York, January 2003. ACM Press.
19. M. Tofte. Type inference for polymorphic references. Inf. Comput., 89(1):1–34,
1990.
20. A. K. Wright. Simple imperative polymorphism. Lisp and Symbolic Computation,
8(4):343–355, 1995.
21. A. K. Wright and M. Felleisen. A syntactic approach to type soundness. Inf.
Comput., 115(1):38–94, 1994.