Typed Dynamic Control Operatorsfor Delimited Continuations
Yukiyoshi Kameyama and Takuo Yonezawa
Department of Computer Science, University of Tsukuba
kameyama@acm.org, yone@logic.cs.tsukuba.ac.jp

Abstract. We study the dynamic control operators for delimited continuations, control and prompt. Based on recent developments on purely
functional CPS translations for them, we introduce a polymorphically
typed calculus for these control operators which allows answer-type modiﬁcation. We show that our calculus enjoys type soundness and is compatible with the CPS translation. We also show that the typed dynamic
control operators can macro-express the typed static ones (shift andreset), while the converse direction is not possible, which exhibits a
sharp contrast with the type-free case.
Keywords: Type System, Delimited Continuation, Dynamic Control
Operator, CPS Translation, Polymorphism, Expressivity.

1

Introduction

Delimited continuations represent not the rest of the computation as with traditional continuations [18], but only part of the rest of the computation. As such,delimited continuations have been used to model backtracking in contrast to
traditional continuations that are used to model jumps.
In direct style, traditional continuations are accessed with control operatorssuch as call/cc. There is, however, more variety for delimited continuations:– Felleisen [12] proposed a control delimiter to signify part of an evaluation
context, or a delimited continuation. This lead to the new control operators
control and prompt, which are called dynamic control operators.
– Danvy and Filinski discovered that delimited continuations are supported byan already existing formalism of 2CPS, the image of iterated CPS translations. They proposed new control operators shift and reset in the directstyle counterpart [9]. They are called static control operators.
Since these proposals, the static control operators have been intensively studied
while the dynamic ones are relatively less studied. For shift/reset, there are
a number of theoretical results [13, 14] as well as useful examples in partial
evaluation, one-pass CPS translation, and mobile codes, while we do not ﬁnd
many corresponding works for control/prompt in the literature, partly due tothe diﬃculty in reasoning about the dynamic features of control/prompt.
Recently, several authors have started to obtain better understanding for dynamic ones, and to connect dynamic and static ones. Shan [7] macro-expressedcontrol and prompt in terms of shift and reset using recursive types. (Seealso Kiselyov’s work [15].) Biernacki, Danvy, and Millikin [6] derived a CPS
translation for control and prompt from a deﬁnitional abstract machine, andgave another encoding of control/prompt by shift/reset. Dybvig, Peyton
Jones, and Sabry [11] gave a uniform monadic framework for delimited continuations including control/prompt. However, no work has studied the direct-style
type system for control/prompt in a way comparative to the type system forshift/reset. The proposed encodings were done in either type-free or recursively typed settings,1 and the proposed CPS translations assumed a restricteddirect-style type system in that the control eﬀect of “answer-type modiﬁcation”
was not allowed. We think this eﬀect is indispensable for delimited continuations,for instance, it is needed to type the printf function in direct style [8, 1].
In this paper, we propose a direct-style type system for control and prompt,
which allows answer-type modiﬁcation, does not need recursive types, and has
ML-like let-polymorphism. We derive the type inference rules from the typestructure for the CPS translations for control and prompt recently developed by
the above mentioned works. The type system in this paper is a proper extensionof that in our previous work [20], which does not allow answer-type modiﬁcation.
We show that our type system enjoys Subject Reduction and Progress properties,
and that types are preserved by the CPS translation. The ﬁrst two properties
constitute type soundness, and the third property is necessary for a semantical
study.
As an application of our type system, we compare the expressivity of typed
control/prompt and that of typed shift/reset. In the type-free setting, they
are known to be equally expressive [7, 15, 4, 6]. However, there exists a big asymmetry in the complexity of these encodings, and a question remained whether
control/prompt is strictly more expressive than shift/reset under an appropriate typed setting (without recursive types). In this paper we answer thisquestion. Namely, we show:– typed control/prompt can macro-express typed shift/reset, while– typed shift/reset cannot macro-express typed control/prompt,
where the type system for shift/reset is the most expressive type system by
Asai and Kameyama [2]. This result contrasts with the type-free case.
This paper is organized as follows: in Section 2 we brieﬂy explain the control
operators for delimited continuations, and in Section 3 we review the functional
CPS translation in the literature. The subsequent three sections are original tothis paper: in Section 4 we introduce the type systems for the dynamic control
operators, and in Section 5 we give several properties for the type systems. In
Section 6, we compare the expressive power of typed control/prompt with typed
shift/reset. Section 8 concludes.
1

We distinguish (general) recursive types from inductive types in that the former
may contain negative occurrences of the type variable being taken the ﬁxed point,
for instance, µX.(X → int) where µ is for the ﬁxed point operator.

2

fun foo xs =let fun visit nil = nil| visit (x::xs) = visit (shift (fn k => x::(k xs)))
in reset (fn () => visit xs) end
fun bar xs =let fun visit nil = nil| visit (x::xs) = visit (control (fn k => x::(k xs)))
in prompt (fn () => visit xs) end
Fig. 1. List-copying and list-reversing functions

2

Informal Explanation of control and prompt

We begin with the examples by Biernacki et al. [6] listed in Figure 1 written inStandard ML syntax.
The functions foo and bar have type int list -> int list, and diﬀer
in the names for control operators only: shift and reset for the former andcontrol and prompt for the latter. Both shift and control capture evaluation
contexts up to the closest delimiter (reset and prompt, resp.) Given the list
[1,2,3], the function foo evaluates as:
foo [1,2,3] Ã <visit (shift (fn k => 1::(k [2,3])))>
Ã <let k = <visit • > in 1::(k [2,3]) end>
Ã <1::<visit [2,3]>>
Ã <1::<let k = <visit • > in 2::(k [3]) end>>Ã ...
Ã <1::<2::<3::nil>>> Ã [1,2,3]
where < . . . > denotes the delimiter inserted by reset, and <visit •> denotes
the delimited evaluation context (delimited continuation) captured by shift
with • being the hole in it. The expression <v> evaluates to v itself when v is avalue, hence the result of this computation is identical to the argument.
The evaluation of bar proceeds as follows (the delimiter is denoted by #):bar [1,2,3] Ã #(visit (control (fn k => 1::(k [2,3]))))
Ã #(let k = (visit • ) in 1::(k [2,3]) end)
Ã #(1::(visit [2,3]))
Ã #(let k = (1::(visit • )) in 2::(k [3]) end)
Ã #(2::(1::(visit [3])))Ã ...
Ã #(3::(2::(1::nil)))3Ã [3,2,1]

The evaluation context captured by control is the whole context since there isno other delimiters. Hence, we obtain a a reversed list as the result of computation.
The operational behavior for each set of control operators can be formalized
by reduction rules. Let v and P denote a value and a call-by-value evaluation
context such that no delimiter encloses the hole, resp. Then we have the reduction
rules as follows:(For shift/reset)hP [Sc.e]i → hlet c = λx.hP [x]i in ei(For control/prompt)# (P [Fc.e]) → # (let c = λx.P [x] in e)

Here Sc.e corresponds to (shift (fn c => e)), and hei to (reset (fn () =>e)) in the ML implementation in the previous subsection. Similarly, # e is(prompt (fn () => e)), and Fc.e is (control (fn c => e)).
Besides the names for control operators, the only diﬀerence between them iswhether the captured delimited continuation has an extra reset or not: λx.hP [x]ifor the former, and λx.P [x] for the latter. This small diﬀerence in syntax raises
a big diﬀerence in semantics. Suppose P has other occurrences of shift orcontrol, and the captured delimited continuation is applied to a value v in athen-current continuation E which may have a delimiter that encloses the hole.
– In the former, we evaluate E[hP [v]i] in which other occurrences of shift
in P will be delimited by this reset (unless they are “escaped” in function
closures). Namely, the corresponding delimiter for these shift is determinedwhen the delimited continuation is captured.
– In the latter, we evaluate E[P [x]] in which other occurrences of control
ought to be delimited by prompt in E. (Note that P does not have any
prompt which encloses the hole). Consequently, the corresponding delimiter for these control is determined not when it is captured, but when thedelimited continuation is used.
Hence the former is called static, and the latter is called dynamic by analogy withstatic and dynamic binding in Scheme and Lisp [5]. The static/dynamic natureof control operators has an impact on their implementation. For shift/reset, adelimited continuation can be represented by an ordinary, composable function,
which leads to a simple CPS translation [9, 10]. For control/prompt, we needto keep the captured delimited continuations as they are, until they are actuallyused, which needs an extra machinery.

3

A CPS translation for control/prompt

We regard a CPS translation as the fundamental analysis tool for control operators. For control and prompt, three such translations are known: Shan’s [7],Dybvig, Peyton-Jones, and Sabry’s [11], and Biernacki, Danvy and Millikin’s [6].
In this paper we use (a variant of) the last one since it is the simplest. We could
use Shan’s one as well.
4v ::= d | x | λx.e

value

e ::= v | e1 e2 | F c.e | # e | let x = e1 in e2| if e1 then e2 else e3

expression

P ::= [ ] | P e | vP
| let x = P in e | if P then e1 else e2

pure evaluation context

E ::= [ ] | Ee | vE
| let x = E in e | if E then e1 else e2 | # E

evaluation context

Fig. 2. Syntax of the language with control/prompt(λx.e)v Ã e[v/x]if true then e1 else e2 Ã e1
if false then e1 else e2 Ã e2
let x = v in e Ã e[v/x]# (P [F c.e]) Ã # (let c = λx.P [x] in e)#vÃvFig. 3. Reduction rules

Figure 2 gives the syntax of our source language where d is constant and x
and c are variables. The expression Fc.e is a construct for control in which
c is a bound variable. The expression # e is the one for prompt. Variables arebound by λ or F, the set of free variables in e is denoted by FV(e), and we
identify α-equivalent expressions. Sequencing a; b is an abbreviation of (λx.b)awith x 6∈ FV(b). In a pure evaluation context P , no prompt may enclose its hole[ ], while a (general) evaluation context E allows such occurrences of prompt.
Figure 3 gives call-by-value operational semantics to this language where e[v/x]
represents the result of capture-avoiding substitution.
Figure 4 deﬁnes the CPS translation for this language as a variant of the one
given by Biernacki et al. The diﬀerences are: (1) they gave a 2CPS translationwhch is an iterated translation (its image takes two continuations as its arguments), while we use a more traditional 1CPS translation, and (2) we extend
the source language with constant, conditional, and let.
The target language of this translation is a call-by-value lambda calculus
with constants, conditional, and let as well as list-manipulating constructs suchas Nil, cons (denoted by ::), append (@) and a destructor (case). Note that thetranslation for let expression is only meaningful for the typed source language(given in the next section), and we have included it in Figure 4 only to save
space. For a type-free source language, we can deﬁne it as [ let x = e1 in e2 ] =[ (λx.e2 )e1 ] .
5

[ ] : SourceTerm → Cont → Trail → TargetValue[ V ] = λk t. k (V )∗ t
[ e1 e2 ] = λk t. [ e1 ] (λm1 t1 . [ e2 ] (λm2 t2 . m1 m2 k t2 ) t1 ) t[ if e1 then e2 else e3 ] = λk t. [ e1 ] (λm1 t1 . if m1 then [ e2 ] k t1 else [ e3 ] k t1 ) t[ let x = e1 in e2 ] = λk t. let x = ([[e1 ] θ1 Nil) in [ e2 ] k t[ # e]] = λk t. k([[e]] θ1 Nil) t[ Fc.e]] = λk t. let c = λx k0 t0 . k x (t @ (k0 :: t0 )) in [ e]] θ1 Nil( )∗ : SourceValue → TargetValue(d)∗ = dfor constant(x)∗ = x

for a variable∗(λx.e) = λx k t. [ e]] k t
θ1 = λx t. case t of
| Nil ⇒ x
| (k1 :: t1 ) ⇒ k1 x t1
Fig. 4. 1CPS translation for the language with control and prompt

Let us see the types in Figure 4, although these types should be consideredinformal, and only for explanation. The types SourceTerm, SourceValue, Cont,
TargetValue, are those for terms and values in the source language, and thosefor continuations and values in the target language, resp.
The type Trail is new to their CPS translation. Recall that, in order to represent the dynamic behavior of control/prompt, we need to keep the delimited
continuations until they are used. A trail is a list of delimited continuations tostore these continuations. Thus, we may informally deﬁne Cont and Trail asfollows:
Cont = TargetValue → Trail → TargetValue
Trail = List(Cont)
This “deﬁnition” needs recursive types, which will be examined in the next
section.
Next, we look at the term-level translation in Figure 4. For the constructs
other than control operators, the translation is the same as the standard (e.g.
Plotkin’s) translation except that it passes trails without changing them.
The prompt-term # e initializes its continuation and trail: in its translation[ # e]], [ e]] is applied to θ1 and the empty trail Nil. The continuation θ1 acts as
the identity continuation (the empty evaluation context).
The control-term Fc.e captures a delimited continuation (and initializes thecontinuation and the trail): it captures the current delimited continuation k for6

a future use of c. When c is applied to some value, the captured continuation k
is “composed” with the then-current continuation k 0 . Rather than simply composing two delimited continuations, we store (in the trail) the list of all the
captured delimited continuations except the current one, namely, we extend thethen-current trail t0 to a new trail t @ (k 0 :: t0 ) and use k as the current continuation. Continuations stored in the trail will be used when the current continuation
becomes empty (i.e. θ1 ).
Note that we can easily extend our source language and the CPS translation
with practical language constructs such as the ﬁxed point operator and primitive
functions.
Finally, a CPS translation for a complete program e is deﬁned as [ e]]θ1 Nil.

4

Type System

We introduce a polymorphic type system for control/prompt in this section.
Types are an important facility in most programming languages to classify terms
and also to ensure a certain kind of safety for computation. We think that, forcontrol/prompt to be used by ordinary programmers, a sound type system is
deﬁnitely needed.
4.1

Design of Type System

Our strategy to construct a type system for control/prompt is basically thesame as that for shift/reset [2]: given a term e, we infer the most general typeof its CPS translation [ e]], and use this type as the type for e. There is, however,two problems in this strategy: (1) the target terms of the CPS translation forcontrol/prompt need recursive types if we assign types, and there is no notionof the most general type in a type system with recursive types, and (2) we needarbitrary many type variables to precisely represent types of the CPS translation.
The ﬁrst problem already appears if we type the identity (delimited) continuation θ1 . Assuming the type of trails is List(τ ) for some τ , θ1 must have thetype α → List(X) → α for some α, where X = α → List(X) → α. Hence weneed some sort of recursive types.
The second problem is this: Recall that Cont and Trail are informally deﬁned
as Cont = TargetValue → Trail → TargetValue and Trail = List(Cont).
When the source language is typed in some way, the type TargetValue should
be instantiated by more speciﬁc types, and in general, a trail has the type:
List(α1 → List(α2 → List(. . . List(αn → · · · → βn ) . . . ) → β2 ) → β1 )for diﬀerent αi and βi . Apparently, we cannot represent these types in a ﬁnite
manner.
We give a simple solution to these problems based on the observation thatmost (if not all) examples with control/prompt in the literature can be typed
under the following simple restriction:7

– In a trail type, all αi and βi is the same type.
This means that any trail must have type µX.List(τ → X → τ ) for some type
τ where µ is for recursive types. In the sequel, we adopt this restriction, andwrite Trail(τ ) for this type. Note that the restriction does not constrain thetype of continuations, that is, a continuation may have type α → Trail(τ ) → β
for diﬀerent types α, β, and τ .
We think that this restriction is not too strong, since, most (if not all) examples with control/prompt in the literature follow this restriction (list-reversing
function and several variations of search programs [6]). Also we will see later thatthe typed control/prompt calculus under this restriction can simulate typed
shift/reset calculus, which has many interesting examples.
Under this restriction, the target terms of the CPS translation can be typed in
the ordinary type system (with let-polymorphism, but without recursive types),in which the most general type always exists (if typable), and, therefore, the ﬁrst
problem is also solved.
Discussion. An anonymous reviewer has suggested us that, we could exclude
the circularity in the trail types by introducing an inductive (not recursive)
structure. One way to achieve it is: if we change the deﬁnition of the trail typefrom Trail = List(Cont) to
Trail(n) = Trail(0) | (Cont × Trail(n − 1))
where n denotes the length of the list, then we can avoid the circularity (recursiveness) of the trail type. However, the use of dependent types drasticallycomplicates the type structure of the target calculus (and possibly the corresponding source type system). Moreover, it is not our goal to obtain a strongly
normalizing calculus for control/prompt by constraining the source type system
artiﬁcially. Rather, we took Biernacki et al.’s CPS translation as a good starting
point, and based on it, we tried to construct a natural type system which is
harmonious with their CPS translation.
4.2

Deﬁnition of Type System

Now we introduce a type system for control/prompt.
Types and type contexts are deﬁned by:α, β · · · ::= b | t | α → (β, γ, δ/τ )A ::= α | ∀t.A
Γ ::= [ ] | Γ, x : A

monomorphic types
polymorphic types
type contexts

where b is a basic type (including bool), t is a type variable, and α → (β, γ, δ/τ )is a function type whose meaning will be made clear later. FTV(A) denotes theset of free type variables in A.
The type system has two forms of judgements, and the ﬁrst form is:Γ ` e : α, β, γ/τ8(x : A ∈ Γ and α ≤ A)var
Γ `p x : α(d is constant of type b)constΓ `p d : b

Γ, x : α ` e : β, γ, δ/τfunΓ `p λx.e : α → (β, γ, δ/τ )Γ `p e : αexpΓ ` e : α, β, β/τΓ ` e1 : α → (β, γ, δ/τ ), ², ρ/τ Γ ` e2 : α, δ, ²/τappΓ ` e1 e2 : β, γ, ρ/τΓ ` e1 : bool, δ, γ/τ Γ ` e2 : α, β, δ/τ Γ ` e3 : α, β, δ/τifΓ ` if e1 then e2 else e3 : α, β, γ/τΓ `p e1 : ρ Γ, x : Gen(ρ; Γ ) ` e2 : α, β, γ/τletΓ ` let x = e1 in e2 : α, β, γ/τΓ ` e : τ, τ, β/τ
promptΓ `p # e : βΓ, c : α → (τ, τ, β/τ ) ` e : ρ, ρ, γ/ρcontrolΓ ` Fc.e : α, β, γ/τFig. 5. Type Inference Rules

where Γ is a type context, α, β, γ, and τ are types, and e is an expression. Itmeans that, under the type context Γ , e is an expression of type α, with theanswer type modiﬁcation2 from β to γ, and the trail type is τ . The roles of theadditional types in the judgement can be made clearer by CPS translating it:Γ ∗ `[[e]] : Cont(α∗ , β ∗ /τ ∗ ) → Trail(τ ∗ ) → γ ∗withTrail(τ ∗ ) = µX.List(τ ∗ → X → τ ∗ )Cont(α∗ , β ∗ /τ ∗ ) = α∗ → Trail(τ ∗ ) → β ∗The second form of judgements is:Γ `p e : αwhich means e is a pure (eﬀect-free) expression of type α. This form is used to
introduce let-polymorphism with control eﬀects in a sound manner[2].
Figure 5 gives the type inference rules where α ≤ A in the rule (var) means, if
A ≡ ∀t1 . · · · ∀tn .ρ for some monomorphic type ρ, then τ ≡ ρ[σ1 , · · · , σn /t1 , · · · , tn ]for some monomorphic types σ1 , · · · , σn . We assume that, a basic type b is associated with each constant d. The type Gen(ρ; Γ ) in the rule (let) is deﬁned by∀t1 . · · · ∀tn .ρ where {t1 , · · · , tn } = FTV(ρ) − FTV(Γ ).
The rule (exp) allows one to switch from the second form to the ﬁrst form.
Since pure expressions are insensitive to continuations and trails, we can introduce arbitrary types for their answer type (β) and the trail type (τ ).
2

For the standard CPS translation, we say, the answer type is modiﬁed in a computation of e from β to γ, if the CPS transform of e has type (α → β) → γ. Without
control operators for delimited continuations, the types β and γ are equal. With
them, they may be diﬀerent. See Asai and Kameyama [2] for details.

9Γ ` e : α, β, γ/tstar-intro, if t 6∈ FTV(Γ, α, β, γ)Γ ` e : α, β, γ/∗Γ ` e : α, β, γ/∗star-elimΓ ` e : α, β, γ/τΓ ` e : α → (β, γ, δ/∗), ², ρ/σstar-funΓ ` e : α → (β, γ, δ/τ ), ², ρ/σc/p+Fig. 6. Type Inference Rules for λlet

Other rules are naturally derived from the type for the CPS translation.
The rule (var) is standard. In the rule (fun), the function type α → (β, γ, δ/τ )extends the ordinary function type α → β to encapsulate the eﬀect of answer
type modiﬁcation from γ to δ with the trail type τ . The rule (app) reﬂects thisintuition. The rule (let) is for ML-like let-polymorphism. As is well known, wemust restrict e1 in the expression let x = e1 in e2 to have a sound type system,
and we follow Asai and Kameyama’s type system [2] which restricts e1 to be apure term, i.e., either a value or # e.
For the rule (prompt), look at its CPS translation in Figure 4. It is easy tocheck θ1 must have type Cont(τ, τ /τ ) for some τ , and the return type of [ e]] is thesame as that of [ # e]]. So by letting this return type β, we get the rule (prompt).
The rule (control) is more complicated. In the CPS translation of Fc.e, a term
λxk 0 t0 .kx(t@(k 0 :: t0 )) is substituted for c, which poses constraints that t and t0
are of the same list type and k 0 is of its member type. Since we restricted all
trails to be of type Trail(τ ) for some τ , k 0 has to have the type Cont(τ, τ /τ )and t and t0 have the type Trail(τ ). Then we can derive the rule (control).
An example type derivation for a concrete term will be given in a later section.
c/p
We call the calculus with this type system λlet .
4.3

Introducing Trail-Polymorphismc/p

The type system of λlet can type many useful examples with control/prompt.
However, it cannot express a certain kind of polymorphism in trails. We occasionally want to express that a function has type α → (β, γ, δ/τ ) for any τ ,i.e., it is insensitive (or polymorphic) to the trail type. To solve this problem
with a small cost, i.e., not without introducing impredicative polymorphism, we
c/p
introduce a limited form of polymorphism, called trail-polymorphism, into λletas follows.
We add a special type constant “∗” to the deﬁnition of types, which canappear in a function type as α → (β, γ, δ/∗), or in a judgement as Γ ` e :α, β, γ/∗. Intuitively, ∗ represents a universally quantiﬁed type variable.
c/p
We add to λlet three new type inference rules listed in Figure 6, which reﬂectc/p+
the intuitive meaning of ∗. We call the extended calculus λlet . Note that thec/p
reductions rules are the same as those for λlet .
10

We can also introduce impredicative polymorphism in the same manner asthat system for shift/reset[2]. Since it is orthogonal to the present type system,
we omit the details in this paper.

5

Properties
c/p

c/p+

In this section, we state basic properties of λlet and λlet . Due to lack of space,
we only state proof sketches in this paper.
The ﬁrst property, subject reduction, is by far the most important property
in a typed calculus.
Theorem 1 (Subject Reduction). If Γ ` e1 : α, β, γ/τ is derived and e1 Ã
e2 , then Γ ` e2 : α, β, γ/τ can be derived.
The theorem is proved by the standard induction on the derivation. For thecase of the reduction # (P [Fc.e]) Ã # (let c = λx.P [x] in e), we decompose
it into several smaller reductions as in [3], then the theorem is easy to prove.
The next theorem is the progress property which states the computation ofa well typed, closed expression does not get stuck. Here, the word “close” meansthat the term does not have any free variables and any occurrences of control
which are not enclosed by prompt. To ensure the last property, we restrict ourattention to an expression in the form # e. A redex is one of the expressions in
the lefthand sides of the reduction rules in Figure 3.
Theorem 2 (Progress). If ` # e : α, β, γ/τ is derivable, then # e is in theform E[r] where E is an evaluation context and r is a redex.
Note that, if e is a value v, # e itself is a redex which reduces to v. The
progress property is proved by the standard case analysis.
These two theorems together constitute the strong type soundness property.
The next theorem states that our type system is compatible with the CPS
translation. For this purpose, we deﬁne the type structure of the target calculus
depending on the source calculus by:
c/p– for λlet , the target calculus is (predicatively) polymorphic lambda calculus
with conditionals, the trail type Trail(τ ), and the list type.
c/p+– for λlet , the target calculus is impredicatively polymorphic lambda calculus(second order lambda calculus) with conditionals, the trail type Trail(τ ),and the list type.
We deﬁne the CPS translation for types and type contexts by:α∗ = α for basic type and type variable(α → (β, γ, δ/τ ))∗ = α∗ → (β ∗ → Trail(τ ∗ ) → γ ∗ ) → Trail(τ ∗ ) → δ ∗(α → (β, γ, δ/∗))∗ = α∗ → ∀X.((β ∗ → Trail(X) → γ ∗ ) → Trail(X) → δ ∗ )[ ]∗ = [ ](Γ, x : ∀t1 . . . tn .α)∗ = Γ ∗ , x : ∀t1 . . . tn .α∗
11

c/p+

The third line is for λlet
theorem.

only. We then state type preservation property as a

Theorem 3 (Type Preservation for CPS Transformation).
– (For λlet and λlet ) If Γ ` e : α, β, γ/τ is derivable for τ 6= ∗, then Γ ∗ `[ e]] : (α∗ → Trail(τ ∗ ) → β ∗ ) → Trail(τ ∗ ) → γ ∗ is derivable in the target
calculus.
c/p+– (For λlet ) If Γ ` e : α, β, γ/∗ is derivable, then Γ ∗ ` [ e]] : (α∗ →Trail(τ ) → β ∗ ) → Trail(τ ) → γ ∗ is derivable for any τ in the target
calculus.
c/p

c/p+

In this paper, we do not state the property that equality is preserved by CPS
translation, since it is independent to our type system, and in order to state theproperty as a theorem, we need to develop a sophisticated equality theory in thetarget language. For the latter, we need the following property for an arbitrary
pure evaluation context P :λx k1 t1 . [ P [x]]] θ1 (k1 :: t1 ) = λx k1 t1 . [ P [x]]] k1 t1
which is about the inductive nature of trails (lists). Since t1 in this equation isa bound variable, we need to elaborate an inductive theory.

6

Encoding Shift/Reset by Control/Prompt

In type-free setting, shift/reset can be macro-deﬁned by control/prompt [4],and we show in this section that it also holds for the typed setting here. We
s/radopt the calculus λlet in [2] for shift/reset, since it is the most liberal typesystem which allows answer-type modiﬁcation and let-polymorphism. Its type
inference rules are listed in the appendix.
s/r
c/p+
We deﬁne a translation from λlet to λlet as follows:
Types
Expressions(α/γ → β/δ) = α → (β, γ, δ/∗)Sc.e = Fc0 .let c = λx.# (c0 x) in ehei = # e

Type Contexts

Γ, x : ∀t1 . . . tn .α = Γ , x : ∀t1 . . . tn .α

For other constructs, the translation is homomorphic. This translation preserves
types and reduction.
Theorem 4.
s/r

c/p+

– If Γ ; β ` e : α; γ is derivable in λlet , Γ ` e : α, β, γ/∗ is derivable in λlet .
c/p+s/r– If Γ ; β ` e1 : α; γ is derivable and e1 Ã e2 in λlet , e1 Ã∗ e2 in λlet .
12

Proof. We prove this theorem by induction on the derivation of Γ ; β ` e : α; γ.
We list two key cases here.
s/r(Reset) Suppose we have a derivation in λlet :..
..
Γ ; α ` e : α; βreset
Γ ; γ ` hei : β; γ
By induction hypothesis, we can derive Γ ` e : α, α, β/∗. Then we can derive:Γ ` e : α, α, β/∗Γ ` e : α, α, β/αΓ `p # e : βΓ ` hei = # e : β, γ, γ/∗s/r(Shift) Suppose we have a derivation in λlet :..
..
Γ, c : ∀t.(β/t → α/t); δ ` e : δ; γ
shift
Γ ; α ` Sc.e : β; γLet ∆1 = Γ , c : ∀t.(β → (α, t, t/∗)). By induction hypothesis, we have a derivac/p+tion for ∆1 ` e : δ, δ, γ/∗ in λlet . Let ∆2 = Γ , c0 : β → (s, s, α/s) where s is a
fresh type variable, then we can derive:∆2 , x : β ` c0 x : s, s, α/s∆2 , x : β `p # (c0 x) : α∆2 , x : β ` # (c0 x) : α, t, t/∗∆2 `p λx.# (c0 x) : β → (α, t, t/∗) ∆1 ` e : δ, δ, γ/∗∆2 `p λx.# (c0 x) : β → (α, t, t/∗)∆1 ` e : δ, δ, γ/δ0∆2 ` let c = λx.# (c x) in e : δ, δ, γ/δΓ ` Fc0 .let c = λx.# (c0 x) in e : β, α, γ/s
Since s 6∈ FTV(Γ , α, β, γ), we can derive Γ ` Sc.e : β, α, γ/∗.
s/rc/p+
We can also show that, if e Ã e0 in λlet , then e Ã∗ e0 in λlet , whose keycase is proved as follows:
hP [Sc.e]i = # (P [Fc0 .let c = λx.# c0 x in e])
Ã # (let c0 = λy.P [y] in let c = λx.# c0 x in e)
Ã # (let c = λy.# (λy.P [x])x in e)
Ã # (let c = λx.# P [x] in e)= hlet c = λx.hP [x]i in ei
c/p

We remark that this proof does not work for λlet .
13

7

Typed Control/Prompt is Strictly More Expressive
Than Shift/Reset

In the type-free setting, we can encode control/prompt in terms of shift/reset[7, 15, 6]. In the typed setting, it is not the case, as we will prove in this section.
s/r
Since λlet is strongly normalizing [2], it is suﬃcient to construct a typable exc/p+c/p
pression in λlet (or λlet ) whose computation is not terminating.
Let α and •, resp. be a type and its inhabitant, resp., for instance, α = booland • = true. Let Γ be the type context c : α → (α, α, α/α), and recall e1 ; e2
is an abbreviation of (λx.e2 )e1 for x 6∈ FV(e2 ). We can type the expressionc/p# (Fc.(c•; c•); Fc.(c•; c•)) in λlet as follows:Γ ` c : α → (α, α, α/α), α, α/α Γ ` • : αΓ ` c • : α, α, α/αΓ ` c •; c • : α, α, α/α`p Fc.(c •; c •) : α` F c.(c •; c •); Fc.(c •; c •) : α, α, α/α` # (Fc.(c •; c •); Fc.(c •; c •)) : α, β, β/τThe computation of this term does not terminate:# (Fc.(c•; c•); Fc.(c•; c•))Ã # (let c = λu.(u; Fc.(c•; c•)) in (c•; c•))Ã∗ # (Fc.(c•; c•); (λu.(u; # Fc.(c•; c•)))•)
Ã∗ # (Fc.(c•; c•); (λu0 .(u0 ; (λu.(u; # Fc.(c•; c•)))•))•)
Ã∗ . . .
Since this example does not use answer-type modiﬁcation or polymorphism, it
can be typed in a more restricted type system such as our previous one [20].
We can go a step further. After submission of this paper, Kiselyov [16] andthe second author (Yonezawa) have independently constructed ﬁxed point combinators in call-by-value:(Kiselyov) Y1 = λf.# (Zf ; Zf )(Y onezawa) Y2 = λf.# (Xf ; Xf )where Zf = Fc. f (λx. # (c•; c•) x)
where Xf = Fc. λx. (f # (c•; c•)) x

c/p

Both Y1 and Y2 are typable in λlet , and satisfy Y1 f x = f (λx. Y1 f x) x, andY2 f x = f (λx. f (Y2 f ) x) x. Therefore, they can serve as ﬁxed point combinators. The former satisﬁes a simpler equation, while Y1 e may not terminate forsome term e, but Y2 e always terminates.

8

Conclusion

We have introduced a polymorphic type system for control/prompt, which allows answer type modiﬁcation and does not need recursive types. We have shown14

that our calculus enjoys type soundness and is compatible with the CPS translation, and that typed control/prompt is strictly more powerful than typed
shift/reset in the absence of recursive types. Although we cannot claim that
our type system is *the* only type system for control/prompt, we believe that
ours can be a good starting point to study the type structure of these control
operators.
Based on this work, Kiselyov and the second author have successfully shownc/pthat λlet is Turing-complete if we extend the calculus with integers and primitive functions. The situation is similar to the exception mechanism in ML, forwhich Lillibridge [17] has proved that typed (unchecked) exception can simulate
all type-free lambda terms, and therefore can represent all Turing-computablefunctions. Thielecke also compared the expressive powers of several control operators using a diﬀerent technique [19].
In this paper we have been concentrating on the foundational aspect ofcontrol/prompt in this paper, and the practical aspect of our type systems
is unstudied. In particular, more application programs other than those by Biernacki, Danvy, Millikin’s are called for, but it is left for future work.
Acknowledgements: We thank Kenichi Asai, Dariusz Biernacki, Olivier
Danvy, and Chung-chieh Shan for their insights. Special thanks go to Oleg Kiselyov and anonymous reviewers for valuable comments. This work was partly
supported by JSPS Grant-in-Aid for Scientiﬁc Research (C) 16500004.

References
1. K. Asai. On Typing Delimited Continuations: Three New Solutions to the Printf
Problem. Technical Report OCHA-IS 07-1, Department of Information Science,
Ochanomizu University, September 2007.
2. K. Asai and Y. Kameyama. Polymorphic Delimited Continuations. In Proc. Asian
Programming Languages and Systems, LNCS 4807, pages 239–254, Nov-Dec 2007.
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. D. Biernacki and O. Danvy. A Simple Proof of a Folklore Theorem about Delimited
Control. J. Funct. Program., 16(3):269–280, 2006.
5. D. Biernacki, O. Danvy, and C. c. Shan. On the Static and Dynamic Extents ofDelimited Continuations. Science of Computer Programming, 60(3):274–297, 2006.
6. D. Biernacki, O. Danvy, and K. Millikin. A Dynamic Continuation-Passing Stylefor Dynamic Delimited Continuations. TOPLAS, to appear.
7. C. c. Shan. Shift to control. In Proc. Workshop on Scheme and Functional Programming, pages 99–107, 2004.
8. O. Danvy. Functional Unparsing. J. Funct. Program., 8(6):621–625, 1998.
9. O. Danvy and A. Filinski. Abstracting Control. In Proc. 1990 ACM Conferenceon Lisp and Functional Programming, pages 151–160, 1990.
10. O. Danvy and A. Filinski. Representing Control: a Study of the CPS Transformation. Mathematical Structures in Computer Science, 2(4):361–391, 1992.
11. R. K. Dybvig, S. Peyton Jones, and A. Sabry. A Monadic Framework for Delimited
Continuations. J. Funct. Program., to appear.
12. M. Felleisen. The Theory and Practice of First-Class Prompts. In Proc. 15th
Symposium on Principles of Programming Languages, pages 180–190, 1988.

15

13. A. Filinski. Representing Monads. In POPL, pages 446–457, 1994.
14. Y. Kameyama and M. Hasegawa. A sound and complete axiomatization for delimited continuations. In ICFP, pages 177–188, 2003.
15. O. Kiselyov. How to remove dynamic prompt: Static and dynamic delimited continuation operators are equally expressive. Technical Report 611, Computer Science
Department, Indiana University, March 2005.
16. O. Kiselyov.
Fixpoint combinator from typed prompt/control.
2007.
http://okmij.org/ftp/Computation/Continuations.html.
17. M. Lillibridge. Unchecked Exceptions Can Be Strictly More Powerful Than
Call/CC. Higher-Order and Symbolic Computation, 12(1):75–104, 1999.
18. C. Strachey and C. P. Wadsworth. Continuations: A mathematical semantics forhandling full jumps. Technical Monograph PRG-11, Oxford Univ. Comput. Lab.,
Oxford, England, 1974. Reprinted in Higher-Order and Symbolic Computation
13(1/2):135–152, 2000.
19. H. Thielecke. On Exceptions Versus Continuations in the Presence of State. In
ESOP, pages 397–411, 2000.
20. T. Yonezawa and Y. Kameyama. A Type System for Dynamic Delimited Continuations. IPSJ Transactions on Programming, Information Processing Society ofJapan, to appear.

A

Polymorphic Type System for shift/resets/r

We deﬁne the type system for λlet in [2] except the ﬁxed point operator. Types
and type contexts are deﬁned by:α, β · · · ::= b | t | (α/β → γ/δ)A ::= α | ∀t.A

monomorphic types
polymorphic types

Γ ::= [ ] | Γ, x : A

type contexts
c/p+

where the function type (α/β → γ/δ) corresponds to α → (γ, β, δ/∗) in λlet .
s/rJudgements in λlet are either Γ ; α ` e : β; γ or Γ `p e : β. The former correc/p+
sponds to Γ ` e : β, α, γ/∗ in λlet . Finally, Figure 7 gives several important
s/r
type inference rules of λlet .

Γ, x : σ; α ` e : τ ; βfunΓ `p λx.e : (σ/α → τ /β)Γ, k : ∀t.(τ /t → α/t); σ ` e : σ; βshift
Γ ; α ` Sk.e : τ ; β

Γ ; σ ` e : σ; τresetΓ `p hei : τs/rFig. 7. Type Inference Rules of λlet .

16