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 the monomorphic type system byDanvy 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 of polymorphic delimited continuations.
Keywords: Type System, Delimited Continuation, Control Operator, CPS Translation, Predicative/Impredicative Polymorphism.

Note. This technical report is an extended version (with proofs) of the paper: “Polymorphic Delimited Continuations”, Kenichi Asai and Yukiyoshi Kameyama, Proc.
Fifth Asian Symposium on Programming Languages and Systems, Lecture Notes in
Computer Science, 2007.

1

Introduction

Delimited continuation operators enable us to manipulate control of programs in a concise
manner without transforming them into continuation-passing style (CPS). In particular,
shift and reset, introduced by Danvy and Filinski [5], have strong connection to CPS, andthus most of the control eﬀects compatible with CPS can be expressed using shift and reset[7]. They have been used, for example, to program backtracking [5], A-normalization in
direct style [1], let-insertion in partial 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 andFilinski [4] 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 [10] but strong type soundness [21] does not hold for their type system.
Gunter, Rémy, and Riecke [9] proposed typed cupto operator with strong type soundness
theorem as well as various properties, but their type system is restricted to a ﬁ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 their expressive
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 typesoundness, existence of principal types and an eﬃcient type inference algorithm, and strong
normalization among others. The polymorphism does not break the semantic foundation of
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 with impredicative polymorphism [8].
Unrestricted polymorphism in the presence of control operators leads to an unsound typesystem [10]. We introduce and employ a new criteria called “purity” restriction instead of
more restrictive value restriction. An expression is said to be pure if it has no control-eﬀects[18]. By allowing pure expressions to be polymorphic, an interesting non-value term can begiven 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 and reset. In Section 3, weformalize 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 to cover impredicative polymorphism under two evaluation
strategies. In Section 6, we compare our work with related work and give conclusion.
Proofs of the theorems in this paper can be found in the appendix.

2

Programming Examples

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

List Append: Answer Type Modiﬁcation

Consider the following program [4] 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 arecaptured 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 a term with a hole:
1 :: 2 :: 3 :: •, waiting for the value for the [] case. Then, shift (fun k -> k) captures it,2

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 :: x of type int list -> int list. In other words, executionof shift (fun k -> k) modiﬁes the answer type from ’a list to ’a list -> ’a list,
where ’a is the type of the elements of the list.
To accommodate this behavior, Danvy and Filinski used a function type of the form S /A -> T / B [4]. 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 -> ’alist / (’a list -> ’a list) for all ’a: given a list of type ’a list, append returns alist of type ’a list to its immediate context; during this process, however, the answer typeof 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 type system[9]. 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 ofshift 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 inprogramming. First of all, the conventional function type S -> T is regarded as polymorphic
in the answer type [18]: S / ’a -> T / ’a for a new type variable ’a. This indicates thateven 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 [3]: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 of elements read so far. It is applied3

twice: once to an empty list to construct a current 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 occurrenceof k has type ’a list / ’a list list -> ’a list / ’a list list whereas the second
one has type ’a list / ’a list -> ’a list / ’a list. This demonstrates that withoutanswer type polymorphism in the captured continuations, the above program does not typecheck.

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" for the 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 thatmodiﬁes the ﬁnal answer type into ’a according to the occurrence of %. 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 of both the answer type modiﬁcation and polymorphism.

3

Predicative Polymorphism with Shift/Reset

We now introduce polymorphic typed calculi for shift and reset, and study their properties
such as type soundness. Following the literature, we distinguish two versions of polymorphism: predicative polymorphism (let-polymorphism) found in ML and impredicative polymorphism which is based on the second order lambda calculus (Girard’s System F [8]). In
s/rthis section, we give the predicative version λlet . The impredicative version will be given inlater sections.
4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.1

Syntax and Operational Semantics

We assume that the sets of constants (denoted by c), variables (denoted by x, y, k, f ), typevariables (denoted by t), and basic types (denoted by b) are mutually disjoint, and that eachconstant is associated with a basic type. We assume bool is a basic type which has constantstrue and false.
s/r

The syntax of λlet is given by BNF in Figure 1. A value is either a constant, a variable, alambda 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 and x are bound in fix f.x.e. An
expression is either a value, an application, a shift expression, a reset expression, a let
expression, or a conditional. The expressions Sk.e and hei, resp., correspond to OCaml
expressions shift (fun k -> e) and reset (fun () -> e), resp. Types are similar to
those in ML except that the function type is now annotated with answer types as (α/γ →β/δ). Free and bound 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 e
F ::= [ ] | vF | F e | let x = F in e | if F then e else e
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

e-context

pure e-context

redex

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 the one corresponding tothis 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 instance of reductionsin 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 assume5

(λ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 λletthat lists and other constructs are available 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 and reset [4]. 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 of 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 τ and the evaluationof e changes the answer type from α to β. A rationale behind this formulation is that, theCPS 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
3

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.

6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 usedin 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 freefrom control eﬀects, that is, pure. Intuitively, an expression is pure when it is polymorphic
in answer types.4 In Danvy and Filinski’s type system, we can deﬁne that e is pure if thejudgment Γ ; α ` e : τ ; α is derivable for any type α. Typical examples of pure expressions
are values but the expression hei is also pure, since all control eﬀects in e are delimited byreset. 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 Γ ) isa ﬁnite list of the form x1 : A1 , · · · , xn : An where the variables x1 , · · · , xn are mutually
distinct, and A1 , · · · , An are (polymorphic) types. Judgments are either one of the following
forms:Γ `p e : τjudgment for pure expression

Γ; α ` e : τ; β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(Γ ).
The type inference rules are a natural extension of the monomorphic type system byDanvy and Filinski [4]. Pure expressions are deﬁned by one of the rules (ﬁx), (fun), or(reset).5 They can be freely turned into general expressions through the rule (exp). Pure
expressions can be used polymorphically through the rule (let). It generalizes the standard
let-polymorphism found in ML. We can allow a let expression let x = e1 in e2 even whene1 is not pure, in which case 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 polymorphism of
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 can deduce thatappend (rewritten with fix) has type ’a list / ’b -> ’a list / (’a list -> ’b),6
4

Thielecke studied the relationship between answer type polymorphism and the absence of control
in depth [18].
5
We could have introduced a more general rule such as: if Γ ; t ` e : τ ; t is derivable for t 6∈
FTV(Γ, τ ), then Γ `p e : τ . It would then allow expressions that are not syntactically values nor
reset expressions but in fact pure, such as Sk.k3. We did not take this approach, because we canalways 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 is immediately
enclosed by reset as is the case for append123, ’b is instantiated to ’a list.

7

(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 .

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 (or int list / ’c -> int list / ’c). Since it is pure,append123 can be given a polymorphic type in its answer type ’c. Notice that append123
is not bound to 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.
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 inany 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 theoutput ’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 thespeciﬁ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 anddelimited continuations. To support this claim, we prove the following properties:
7

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

8

– 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 and e1 Ã∗ 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 typeas the original term (strong type soundness [21]). This is the consequence of having answer
types explicitly in our type system. We need three lemmas to prove this theorem.
Lemma 1 (Weakening of Type Context). Suppose Γ1 ⊂ Γ2 and Γ2 is a valid typecontext. If Γ1 ; α ` e : σ; β is derivable, then Γ2 ; α ` e : σ; β is derivable. Similarly forΓ1 `p e : σ.
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] : τ ; β is derivable.
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, weneed to reﬁne it, since, for instance, Sk.k3 cannot be reduced further due to the absence ofan enclosing reset. Here, we deﬁne a program to be an expression with a toplevel reset ofthe form hei which has no free variables.
Theorem 2 (Progress and Unique Decomposition). If `p hei : τ is derivable, theneither e is a value, or hei can be uniquely decomposed into the form E[R] where E is anevaluation context and R is a redex.
By Theorems 1 and 2, we can conclude that our type system is sound (Type Soundness).
Although our type system may look rather complex, we can smoothly extend Hindleys/rMilner 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 type variables, and α, τ , and β are types.
9

Theorem 3 (Principal Type and Type Inference). We can construct a type inferences/ralgorithm W 0 for λlet such that:
1. W 0 always terminates.
2. if W 0 returns (θ; α, τ, β), then Γ θ; α ` e : τ ; β is derivable. Moreover, for any(θ0 ; α0 , τ 0 , β 0 ) such that Γ θ0 ; α0 ` e : τ 0 ; β 0 is derivable, (Γ θ0 , α0 , τ 0 , β 0 ) ≡ (Γ θ, α, τ, β)φ forsome 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 the subcalculus
without fix. This is in contrast to cupto operator, where strong normalization does nothold.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.

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 of shift and reset in termsof a CPS translation [5, 6]. In this section, we show that it can be naturally extended topolymorphic setting.
Harper and Lillibridge [11] were the ﬁrst to systematically study CPS translationsin polymorphic language with control operators. They introduced CPS translations fromF ω+call/cc to F ω, and proved that, under a condition similar to the value restriction, acall-by-value CPS translation preserves types and semantics (equality). We follow Harperand Lillibridge to give a type-and-equality 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 (theimage) of the translation is λlet , the minimum lambda calculus with let-polymorphism andconditional expressions.9
The type (α/γ → β/δ) is translated to the type of a function which, given a parameterof type α∗ and a continuation of type β ∗ → γ ∗ returns a value of type δ ∗ . For instance,
the type of the visit function (in the prefix example) ’a list / ’b -> ’a list / ’blist is CPS translated to ’a list -> (’a list -> ’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 enoughpolymorphism for delimited continuations.
89

See http://okmij.org/ftp/Computation/Continuations.html#cupto-nontermination.
s/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 kindsof judgments.

10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.

The translation of the let expression let x = e1 in e2 needs care to take polymorphism
into account. We use a let-expression to express the polymorphism in the source term, andsupply the identity continuation λm.m to the CPS transform [ e1 ] . This is typable in thetarget calculus, since a pure expression is translated 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 derivable and e1 Ã∗ e2
s/r
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 for advanced
concepts in programming languages, since its impredicative polymorphism is strictly more
10

The reduction Ã in λlet is the reduction Ã restricted to the expressions in λlet .

11

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

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

λ2(standard)

type
value

s/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.τs/r,M Lexpression.

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

expressive than the predicative one. In this section, we study an extension of (call-by-value
version of) System F with shift and reset. It is an explicitly typed calculus rather than an
s/r
implicitly typed calculus like λlet . Hence, we add two constructs to the expressions: Λt.e for
type-abstraction and e{α} for type-application. Following Harper and Lillibridge [11], we
consider two calculi with impredicative polymorphism that diﬀer in evaluation strategies.
s/r,Std, adopts the “standard” strategy: Λt.e is treated as a value, andThe ﬁrst calculus, λ2
s/r,M L, adopts the “ML-like” strategy:
hence we do not evaluate under Λ. The second one, λ2
Λt.e is a value only when e is a value, and hence we evaluate under Λ.
s/rs/r,M Ls/r,Std
extends that of λlet with the new constructs listedand λ2The syntax of λ2
in Figure 6. We annotate bound variables with types, for instance, λx : α. e. We eliminate let expressions, since they can be macro-deﬁned: for instance, the expression let f =s/r
λx.x in (f f )0 in λlet is represented11 as (λf : ∀t.(t → t). f {int → int}(f {int})0)(Λt.λx :t. x). Monomorphic and polymorphic 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,M Ls/r,Std, and areand λ2The type inference rules for new constructs are common to λ2
given in Figure 7. As can be seen by the rule (tabs), the body e in Λt.e is restricted to a pures/r,M L, this restriction is necessary12 to ensure the type soundness due to aexpression. For λ2
similar reason as Harper and Lillibridge [11] 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 restrictedcalculus. 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 λ2pression e in the reduction rule is restricted to a value.
1112, the subex-

We assume that 0 is a constant of type int.
s/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.

12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.

s/r,Std

Polymorphism in λ2
is a generalization of Leroy’s “polymorphism by name” [15]:consider the expression let f = hei in (f f )0 for an expression e of type t → t and a constant
0 of type int. It is represented by (λf : ∀t.(t → t).(f {int → int})(f {int})0)(Λt.hei) in
s/r,Stdλ2, and it is easy to see that the evaluation 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 the same 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.
s/r,Std

We can show type soundness for λ2

s/r,M Land λ2.

Theorem 7 (Type Soundness). Subject reduction property and progress property hold for
s/r,Stds/r,M Lλ2
and λ2.

s/r,Stds/r,M Lin Figures 9 and 10. The targetand λ2
We deﬁne a CPS transformation for λ2
calculus of the translation is System F augmented with basic types, constants, fix andconditionals. Equality of the target calculus is the least congruence relation which includes
call-by-value βη-equality, β-equality for types ((Λt.e){α} = e[α/t]), and equality for fix andconditionals. Since the target calculus is explicitly typed, the CPS translation for expressions
is annotated by types as [ e]]α,τ,β , which is well-deﬁned when Γ ; α ` e : τ ; β is derivable forsome Γ . It is interesting to see how the diﬀerence of evaluation strategies aﬀect the diﬀerenceof CPS translations in Figures 9 and 10.
s/r,M Ls/r

Note that the CPS translation for λ2
is a natural extension of that for λlet : fors/rinstance, [ let f = hei in (f f )0]] in λlet is equal (up to the call-by-value βη-equality) tos/r,Std[ (λ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 types and equality.
s/r,Stds/r,M LLet T be λ2
or λ2
.
13

(∀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.

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

6

Conclusion

We have introduced predicative and impredicative polymorphic typed calculi for shift andreset, 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 have shown that a number of pleasant properties holdfor 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 be sound, thus generalizing value restriction used in Standard ML and OCaml.
In the literature, a number of authors have tackled the unsoundness problem of polymorphism and eﬀects [19, 15, 20, 11]. We have proposed a simple solution based on the notionof “purity”, which is, in the presence of the reset operator, less restrictive than the notionof “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 for delimited
continuations. Introducing polymorphism into a calculus with shift and reset has been implicit by Danvy who gave many programming examples (see, for instance, [3]). In fact, hisinteresting examples encouraged us to formulate the calculi in the present paper. Filinski [7]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 and for all. The same goes for the calculus with cupto by Gunter et al. [9].
14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 for polymorphism. As far as we know, the present paper is the ﬁrst to provide a systematic study on
the interaction of polymorphism and control operators for delimited continuations.
Although we believe that our calculus serves as a good foundation for studying polymorphic delimited continuations calculi, this is only the ﬁrst step; we need deeper understanding
and better theories. The ﬁrst author of the present paper has studied logical relations basedon Danvy and Filinski’s monomorphic type system [1], but it is not apparent if his result
extends to the polymorphic case. Hasegawa [12] studied parametricity principle for the second order, call-by-name λµ-calculus (similar to System F + call/cc), and obtained thenotion of “focal parametricity”. Although he works in call-by-name, we hope to ﬁnd someconnection between our work and his results in the future. A recent work by Mogelberg andSimpson [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. O. Danvy. An Analytical Approach to Program as Data Objects. DSc thesis, Department ofComputer Science, University of Aarhus, Aarhus, Denmark, 2006.
4. O. Danvy and A. Filinski. A Functional Abstraction of Typed Contexts. Technical Report
89/12, DIKU, University of Copenhagen, July 1989.
5. O. Danvy and A. Filinski. Abstracting Control. In Proc. 1990 ACM Conference on Lisp andFunctional Programming, pages 151–160, 1990.
6. O. Danvy and A. Filinski. Representing Control: a Study of the CPS Transformation. Mathematical Structures in Computer Science, 2(4):361–391, 1992.
7. A. Filinski. Representing Monads. In POPL, pages 446–457, 1994.
8. J.-Y. Girard, Y. Lafont, and P. Taylor. Proofs and Types, volume 7 of Cambridge Tracts in
Theoretical Computer Science. Cambridge University Press, 1989.
9. C. A. Gunter, D. Remy, and J. G. Riecke. A Generalization of Exceptions and Control in
ML-Like Languages. In FPCA, pages 12–23, 1995.
10. R. Harper, B. F. Duba, and D. MacQueen. Typing First-Class Continuations in ML. J. Funct.
Program., 3(4):465–484, 1993.
11. R. Harper and M. Lillibridge. Explicit polymorphism and CPS conversion. In POPL, pages
206–219, 1993.
12. M. Hasegawa. Relational parametricity and control. Logical Methods in Computer Science,2(3), 2006.
13. Y. Kameyama and M. Hasegawa. A sound and complete axiomatization for delimited continuations. In ICFP, pages 177–188, 2003.
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 eﬀects. In LICS,
2007.

15

17. C. Strachey. Fundamental concepts in programming languages. International Summer Schoolin 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.

A

Proofs of Theorems and Lemmas

In this appendix, we give detailed proofs of theorems and lemmas for interested readers.
Proof (Lemma 1). This lemma can be proved by induction on the derivation of Γ1 ; α ` e :σ; β. The only tricky case is the rule (let) in which the type variables in FTV(Γ2 ) − FTV(Γ1 )may clash with the type variables being generalized by this rule, i.e., those type variables inFTV(σ)−FTV(Γ ) in this rule. However, since these type variables are so called eigen variables,
and can be systematically renamed to fresh type variables, we can manage this case.
The other cases can be proved easily.
Lemmas 2 and 3 are proved by straightforward induction on the derivation, and the proof
is omitted.
Proof (Theorem 1). It suﬃces to prove that, for each reduction rule R Ã e, if Γ ; α ` R : τ ; β
is derivable, then Γ ; α ` e : τ ; β can be derived.
The cases when R is (λx.e1 )v or let x = v in e1 can be proved using Lemmas 2 and 3.
The cases when R is hvi or conditionals are easy to prove.
The remaining case is when R ≡ hF [Sk.e1 ]i and e ≡ hlet k = λx.hF [x]i in e1 i. We
consider the following set of reductions:(Sk.e1 )e2 → Sk 0 .let k = λu.hk 0 (ue2 )i in e1v(Sk.e1 ) → Sk 0 .let k = λu.hk 0 (vu)i in e1
hSk.ei → hlet k = λu.u in eih(λu.hF [u]i)ei → hF [e]i(λx.x)e → e
It is not diﬃcult to see that the reduction R Ã e can be “decomposed” into these reductions.
In other words, we have:hF [Sk.e1 ]i →∗ hlet k = λx.hF [x]i in e1 iwhich can be proved by induction on the pure evaluation context F . Then, it remains toshow the subject reduction property for these reductions, but all of them can be carried out
easily.
Proof (Theorem 2). We can prove that, if ; α ` e1 : τ ; β is derived (i.e., e1 has no freevariables), e1 is in one of the following forms: (1) a value v, (2) E[R] for some evaluation
16

context E and redex R, or (3) F [Sk.e2 ] for a pure evaluation context F , a variable k andan expression e2 .
Suppose `p hei : τ is derived. Then we have ; α ` hei : τ ; α, and hence hei must be oneof the three forms above. Since hei has an outermost reset, the case (3) cannot happen, andwe obtain the conclusion of the theorem.
The type inference algorithm stated in Theorem 3 is given in Section B of the appendix.
Proof (Theorem 4). Conﬂuence can be proved by Takahashi’s parallel reduction which isomitted. (Note we do not have overlapping redexes.)s/r

To prove strong normalization for λlet without fix, we deﬁne a reﬁned CPS translation,
which produces fewer administrative redexes (administrative redexes are those redexes generated at the translation time) than the CPS translation we gave in the main text of thepaper. There are several such CPS translations since Plotkin’s colon translation, and we use
a slightly modiﬁed version of Danvy and Filinski’s two-level lambda calculus [6].
In the two-level lambda calculus, λ and application (explicitly written as @ here) areclassiﬁed13 into “static” and “dynamic”, depending on whether they constitute administrative redexes (i.e., they are generated at the translation time) or source redexes (i.e., they
exist in the source expression). The static lambda’s and @’s are annotated by overlines as λand @, while the dynamic ones as λ and @.
The target of the modiﬁed CPS translation consists of dynamic constructs and those
constructs which are not lambda’s and application symbols. (We will later deﬁne the precise
grammar of the target language after deﬁning the reﬁned CPS translation.)
The modiﬁed CPS translation [ e, K]] takes an expression e and an extra argument K(representing the continuation), and returns an expression, which is deﬁned by:[ v, K]] = K@v ∗[ e1 @e2 , K]] = [ e1 , λm1 .[[e2 , λm2 .(m1 @m2 )@(λn. K@n)]]][ hei, K]] = K@[[e, λm.m]][ Sk.e, K]] = let m1 = true inlet k = λn.λκ0 .κ0 @(K@n) in [ e, λm.m]][ let x = e1 in e2 , K]] = let x = [ e1 , λm.m]] in [ e2 , K]][ if e1 then e2 else e3 , K]] = [ e1 , λm.if m then [ e2 , K]] else [ e3 , K]]]x∗ = xc∗ = c(λx.e)∗ = λx.λκ.[[e, λm. κ@m]]where m,m1 ,m2 ,n,κ, and κ0 are fresh variables. In the deﬁnition for shift, we have added a
redundant redex let m1 = true in · · · for the purpose of SN proof.
The complete CPS transform of an expression e is deﬁned by C[[e]] ≡ λκ.[[e, λx.κ@x]].
13

In fact, Danvy and Filinski classiﬁed every construct into two classes, but here we need to classify
only lambda’s and applications, and other constructs are implicitly classiﬁed as “dynamic”.

17The grammar of the target language of the reﬁned CPS translation is deﬁned as follows:d ::= c | x | n | n@d | (d@d)@(λn.d) | λx.λκ.d| let x = d in d | let n = d in d | if d then d else d|ss ::= K@d
K ::= λn.dwhere n ∈ FV(d)In the deﬁnition, x is a source variable (which appears in the source expression of the CPS
translation), n is an auxiliary variable (which is introduced by the CPS translation), d is a
dynamic expression, s is a static expression, and K is a (static) continuation.
It is important to note the side condition for K, n ∈ FV(d), which means that thecontinuation K does not discard its argument n.
Let λ+
let be the typed calculus λlet with the function space being replaced by two function
spaces α→β (for static functions) and α→β (for dynamic ones), and, accordingly, lambda
abstractions and applications being replaced by two versions.
s/rThen, we can easily prove the following for any expression e typable in λlet :– C[[e]] follows the grammar above (including the side condition of the arguments of continuations).
– C[[e]] typechecks in λ+let .
– Subject reduction w. r. t. static β-reduction holds. Namely, if we reduce a static β-redex(λx.e1 )@e2 to e1 [e2 /x], then an expression typable in λ+let reduces to an expression
still typable in λ+
.
Also
if
an
expression
beforeastaticβ-reduction
satisﬁes the side
letcondition of the arguments of continuations, so does the expression after the reduction.
The reduction of static β-redex (λx.e1 )@e2 → e1 [e2 /x] is Church-Rosser and strongly
normalizing in the target language, and we can take the unique normal form of each expression in the target language, which does not have any static constructs λ and @. Let us write
the unique normal form (w.r.t. static β reduction) of a term e by NF(e).
s/r

We are going to prove the key property that, for any reduction e1 Ã e2 in λlet otherthan the reset-value reduction (hvi Ã v), and any continuation K generated by the grammar
above, we have NF([[e1 , K]]) Ã+ NF([[e2 , K]]) in the target calculus λlet 14 .
– If the reduction is the call-by-value β reduction (the ﬁrst reduction in Figure 2), or
reductions for let (the ﬁfth reduction) or conditional (the sixth and seventh reductions),
then the key property can be proved easily.
– For the fourth reduction hF [Sk.e]i Ã hlet k = λx.hF [x]i in ei, we ﬁrst prove that
NF([[F [e], K]]) ≡ NF([[e, λm.[[F [m], K]]] ) for any pure e-context F , any expression e, andany continuation K, which can be proved by induction on F .
14Since we consider only normal forms wrt static β-redexes, all reductions in the target calculus
are dynamic β-reduction, let-reductions, or reductions for conditionals.

18

Then we can prove:
NF([[hF [Sk.e]i, K]])
≡ NF(K@[[F [Sk.e], λm.m]])≡ NF(K@[[Sk.e, λm0 .[[F [m0 ], λm.m]]] )≡ NF(K@(let m1 = true in let k = λn.λκ0 .κ0 @((λm0 .[[F [m0 ], λm.m]])@n) in [ e, λm.m]]))≡ NF(K@(let m1 = true in let k = λn.λκ0 .κ0 @[[F [n], λm.m]] in [ e, λm.m]]))Ã+ NF(K@let k = λn.λκ0 .κ0 @[[F [n], λm.m]] in [ e, λm.m]])
Note that, since K does not discard its argument, the reduction let m1 = true in e1 Ã
e1 is preserved, and at least one step reduction occurs during this sequence. We also have:
NF([[hlet k = λx.hF [x]i in ei, K]])
≡ NF(K@let k = λx.λκ.κ@[[F [x], λm.m]] in [ e, λm.m]])and therefore the resulting expressions are the same up to α-equivalence, hence we have:
NF([[hF [Sk.e]i, K]]) Ã+ NF([[hlet k = λx.hF [x]i in ei, K]])We also note that the reset-value reduction hvi Ã v will be CPS translated to identity, that
is, NF([[hvi, K]]) ≡ NF([[v, K]]) for a value v and a continuation K.
In summary we have:– If e1 Ã e2 by the reduction other than reset-value, then NF(C[[e1 ] ) Ã+ NF(C[[e2 ] ).
– If e1 Ã e2 by the reset-value reduction, NF(C[[e1 ] ) ≡ NF(C[[e2 ] ).
s/r

We now prove the strong normalization for λlet . Suppose there is an inﬁnite reductions/r
sequence e1 Ã e2 Ã · · · in λlet . Since the reset-value reduction (hvi Ã v) cannot be applied to an expression inﬁnite many times, the reduction sequence must contain inﬁnitely
many reductions which are not reset-value. Then by the property above, we have an inﬁnite sequence NF(C[[e1 ] ) Ã+ NF(C[[e2 ] ) Ã+ · · · . But the target calculus λlet is a strongly
s/r
normalizing calculus, we get contradiction. Hence, λlet does not have an inﬁnite reduction
sequence.
Proof (Theorem 5). The two statements in the theorem are proved by simultaneous induction
on the derivation of Γ ; α ` e : τ ; β and that of Γ `p e : τ .
We only prove the case when the last rule of the derivation is the rule (let). Thene ≡ (let x = e1 in e2 ), and we have derivations for Γ `p e1 : σ and Γ, x : Gen(σ, Γ ); α `e2 : τ ; β. By induction hypothesis, we can derive Γ ∗ ` [ e1 ] : (σ ∗ → σ ∗ ) → σ ∗ , and thenΓ ∗ ` [ e1 ] (λm.m) : σ ∗ . Again by induction hypothesis, we can derive Γ ∗ , x : (Gen(σ, Γ ))∗ `[ e2 ] : (τ ∗ → α∗ ) → β ∗ . Since (Gen(σ, Γ ))∗ ≡ Gen(σ ∗ , Γ ∗ ), we can apply the rule (let) toobtain Γ ∗ ` [ let x = e1 in e2 ] : (τ ∗ → α∗ ) → β ∗ .
Proof (Theorem 6). This theorem can be proved in the same manner as in Kameyama andHasegawa [13], where the soundness and completeness of the CPS translation with respect
to the equality were proved.
19

Proof (Theorem 7). To prove the subject reduction property, we need to consider two newcases.
(Case-1: (Λt.e){α} Ã e[α/t])
s/r,Stds/r,M LWe ﬁrst note that λ2
and λ2
both enjoy the type substitution property whichmeans, if Γ ; α ` e : τ ; β is derivable then, for any substitution θ for type variables, we
can derive Γ θ; αθ ` eθ : τ θ; βθ. Then, the subject reduction property for Case-1 is easily
proved.
(Case-2: hF [Sk.e1 ]i Ã hlet k = λx.hF [x]i in e2 i)s/r

In λlet , this case has been proved by “decomposing” this big reduction into several
s/r,Stds/r,M L
smaller reductions. In λ2
and λ2, we have a new small reduction after this “decomposition” as:(Sk.e1 ){α} → Sk 0 .let k = λu.hk 0 (u{α})i in e1
To prove the subject reduction property for this case is again straightforward.
s/r

Progress property can be proved in the same way as that for λlet .
Proof (Theorem 8). Due to the modularity of the CPS translations, we only have to provethe cases for new constructs.
The proof of the type-preservation part of the theorem is quite standard for both calculi.
The only problem was how to deﬁne them correctly.
The proof of the equation-preservation part of the theorem needs to treat two new
reductions that appeared in the proof of Theorem 7 above. In fact, we need to prove four
new cases (two new reductions for two calculi).
We frequently omit the type annotations in the following.
s/r,Std(Case-1 for λ2: (Λt.e){α} Ã e[α/t])[ (Λt.e){α}]]β,τ [α/t],β ≡ λκ.(λκ0 .κ0 (Λt.Λs.[[e]]))(λu.u{α∗ }{β ∗ }κ)Ã λκ.(λu.u{α∗ }{β ∗ }κ)(Λt.Λs.[[e]])Ã+ λκ.[[e]][α∗ /t][β ∗ /s]κ≡ λκ.[[e]][α∗ /t]κ= [ e[α/t]]]β,τ [α/t],βFrom the third last to the second last line, we used the fact that e does not contain the typevariable s freely. From the second last to the last line, we used η-equality.
s/r,Std(Case-2 for λ2: hF [Sk.e1 ]i Ã hlet k = λx.hF [x]i in e2 i)Again we pick up the following smaller reduction by decomposing the big reduction.
(Sk.e1 ){α} → Sk 0 .let k = λu.hk 0 (u{α})i in e120

[ (Sk.e1 ){α}]]≡ λκ.(λκ1 .let k = λnκ2 .κ2 (κ1 n) in [ e1 ] (λm.m))(λu.u{σ ∗ }{α∗ }κ)Ã+ λκ.let k = λnκ2 .κ2 (n{σ ∗ }{α∗ }κ) in [ e1 ] (λm.m)[ Sk 0 .let k = λu.hk 0 (u{α})i in e1 ]Ã+ λκ.let k 0 = λnκ1 .κ1 (κn) in
let k = λu.λκ3 .κ3 (u{σ ∗ }{α∗ }(λw.k 0 w(λm.m))) in [ e1 ] (λm.m)
Ã+ λκ.let k = λu.λκ3 .κ3 (u{σ ∗ }{α∗ }(λw.κw)) in [ e1 ] (λm.m)
The CPS translations of the two terms are equal up to call-by-value η-equality: λw.κw = κ.
s/r,M L
(Case-1 for λ2: (Λt.v){α} Ã v[α/t])[ (Λt.v){σ}]]β,τ [σ/t],β ≡ λκ.(λκ1 .κ1 (Λt.(λκ2 .κ2 (v)∗ )(λm.m)))(λu.κ(u{σ ∗ }))Ã+ λκ.κ((Λt.v ∗ ){σ ∗ })
Ã λκ.κ(v ∗ [σ ∗ /t])
≡ [ v[σ/t]]]s/r,M L: hF [Sk.e1 ]i Ã hlet k = λx.hF [x]i in e2 i)(Case-2 for λ2
Again we shall prove the following case.
(Sk.e1 ){α} → Sk 0 .let k = λu.hk 0 (u{α})i in e1[ (Sk.e1 ){α}]]≡ λκ.(λκ1 .let k = λnκ2 .κ2 (κ1 n) in [ e1 ] (λm.m))(λu.κ(u{α∗ }))Ã+ λκ.let k = λnκ2 .κ2 (κ(n{α∗ })) in [ e1 ] (λm.m)[ Sk 0 .let k = λu.hk 0 (u{α})i in e1 ]Ã+ λκ.let k 0 = λnκ1 .κ1 (κn) in
let k = λu.λκ3 .κ3 ((λw.k 0 w(λm.m))(u{α∗ })) in [ e1 ] (λm.m)
Ã+ λκ.let k = λuκ3 .κ3 (λw.κw)(u{α∗ }) in [ e1 ] (λm.m)
Again using call-by-value η-equality, the CPS translations of the two terms are equal.

B

s/rType Inference Algorithm for λlets/r

We can extend Hindley-Milner’s type inference algorithm W to λlet . The extended algorithm
is called W 0 here.
W 0 receives two parameters as inputs: a valid context Γ and a raw expression e suchthat all free variables in e are contained in Γ .
21

W 0 (Γ, e) either succeeds or fails. If it succeeds, it returns a quadruple (θ; α, τ, β) whereθ is a substitution for type variables, α, τ and β are types such that Γ θ; α ` e : τ ; β isderivable.
We deﬁne a few important cases for W 0 . In the following, it should be silently understoodthat, if any subcomputation (a recursive call to W 0 or uniﬁcation) fails, then the whole
computation fails.
(Case 1: e is a variable x)
Since x appears in Γ , we can assume (x : ∀t1 . · · · ∀tn .σ) ∈ Γ with monomorphic σ. Choose
fresh type variables s0 , s1 , · · · , sn . Then the algorithm returns ([ ]; s0 , σ[s1 , · · · , sn /t1 , · · · , tn ], s0 )where [ ] denotes the empty substitution.
(Case 2: e is e1 e2 )Compute W 0 (Γ, e1 ) to obtain (θ1 ; α1 , τ1 , β1 ), and compute W 0 (Γ θ1 , e2 ) to obtain (θ2 ; α2 , τ2 , β2 ).
Choose fresh type variables t1 and t2 , and unify: τ1 θ2 = (τ2 /t1 → t2 /α2 )θ2 and α1 θ2 = β2 .
Let θ3 be the most general uniﬁer of these equations, and return (θ3 ◦θ2 ◦θ1 ; t1 θ3 , t2 θ3 , β1 θ2 θ3 ).
(Case 3: e is Sk.e1 )Choose fresh type variables t1 , t2 and t3 , and let Γ 0 be Γ, k : ∀t1 .(t2 /t1 → t3 /t1 ). Compute
W 0 (Γ 0 , e) to obtain (θ1 ; α, τ, β). Unify α = τ , and let θ2 be its most general uniﬁer. Then
return (θ2 ◦ θ1 ; t3 θ, t2 θ, βθ).
(Case 4: e is he1 i)
Compute W 0 (Γ, e1 ) to obtain (θ1 ; α, τ, β). Unify α = τ and let θ2 be its most general
uniﬁer. Choose a fresh type variable t. Returns (θ2 ◦ θ1 ; t, βθ2 , t).
(Case 5: e is let x = e1 in e2 )If e1 is not pure, i.e., not a syntactic value or a reset expression, then it should be understood as a monomorphic let, or an abbreviation of (λx.e2 )e1 , then compute W 0 (Γ, (λx.e2 )e1 ).
If e1 is pure, it is a polymorphic let expression. Compute W 0 (Γ, e1 ) to obtain (θ1 ; α1 , τ1 , β1 ).
(It is automatically guaranteed that, α1 ≡ β1 is a type variable which does not appear inany other types.) Let t1 , · · · , tn be the type variables in FTV(τ ) − FTV(Γ θ1 ). Let Γ 0 be
Γ θ1 , x : ∀t1 . · · · ∀tn .τ . Compute W 0 (Γ 0 , e2 ) to obtain (θ3 ; α3 , τ3 , β3 ). Then return (θ3 ◦ θ2 ◦
θ1 ; α3 , τ3 , β3 ).
Other cases are straightforward.
We can prove Theorem 3 in the same manner as that for W .

22