Answer-Type Modification without Tears:
Prompt-Passing Style Translation
for Typed Delimited-Control Operators
Ikuo Kobori

Yukiyoshi Kameyama

Oleg Kiselyov

University of Tsukuba, Japan

University of Tsukuba, Japan

Tohoku University, Japanikuo@logic.cs.tsukuba.ac.jp

kameyama@acm.org

oleg@okmij.org

The salient feature of delimited-control operators is their ability to modify answer types during computation. The feature, answer-type modification (ATM for short), allows one to express various
interesting programs such as typed printf compactly and nicely, while it makes it difficult to embed
these operators in standard functional languages.
In this paper, we present a typed translation of delimited-control operators shift and reset with
ATM into a familiar language with multi-prompt shift and reset without ATM, which lets us use
ATM in standard languages without modifying the type system. Our translation generalizes Kiselyov’s direct-style implementation of typed printf, which uses two prompts to emulate the modification of answer types, and passes them during computation. We prove that our translation preserves
typing. As the naive prompt-passing style translation generates and passes many prompts even forpure terms, we show an optimized translation that generate prompts only when needed, which is also
type-preserving. Finally, we give an implementation in the tagless-final style which respects typing
by construction.

1

Introduction

Delimited continuations are parts of a continuation, the rest of computation, and delimited-control operators provide programmers a means to access the current delimited continuations. Since the delimitedcontrol operators control/prompt and shift/reset have been proposed around 1990 [12, 9], many researchers have been studying them intensively, to find interesting theory and application in programtransformation, partial evaluation, code generation, and computational linguistics. Today, we see theirimplementations in many programming languages such as Scheme, Racket, SML, OCaml, Haskell, andScala.
Yet, there still exists a big gap between theory and practice if we work in typed languages. Theoretically, the salient feature of delimited-control operators is their ability to modify answer types. The term
reset (3 + shift k -> k) looks as if it has type int, but the result of this computation is a continuation fun x -> reset (3 + x) whose type is int -> int, which means that the initial answer typehas been modified during the computation of the shift term. Whereas this feature, called Answer-Type
Modification, allows one to express surprisingly interesting programs such as typed printf, it is the sourceof the problem that we cannot easily embed the delimited-control operators in standard languages. We
can hardly expect that the whole type system of a full-fledged language would be modified in such a way.
With a few exceptions of Scala [19] and OchaCaml [18], we cannot directly express beautiful examples
with ATM as programs in standard languages.
We address this problem, and present a solution for it. Namely, we give a translation from a calculus
with ATM shift and reset into a calculus with multi-prompt shift and reset without ATM. Our translation is a generalization of Kiselyov’s implementation [15] of typed printf using multi-prompt shift andSubmitted to:
WoC 2015

c I. Kobori, Y. Kameyama & O. Kiselyov
This work is licensed under theCreative Commons Attribution License.

2

ATM without Tears

reset where he associates each answer type with a prompt (a tag) for delimited-control operators. Ourtranslation also uses prompts to simulate answer types, and the term obtained by our translation dynamically generates and passes two prompts during computation, thus we call it Prompt-Passing Style (PPS),
named after the well known Continuation-Passing Style.
We introduce a PPS translation from a calculus with ATM to a calculus without, and prove that it istype preserving. We also give an implementation based on our translation in the tagless-final style [6, 17],
which allows us to embed a domain-specific language while preserving types by construction.
The PPS translation differs from the definitional CPS translation for shift and reset [9] in that thegenerated term by our PPS translation are in direct style, while the generated terms by the CPS translation
are in continuation-passing style, which makes the size of terms bigger than the one obtained by the latter,that may affect performance. Further, we refine the naive PPS translation to obtain an optimized PPStranslation where prompts are generated and passed only when needed. It is based on the idea of one-pass
CPS translation [11] as well as an ad hoc optimization for prompts. The optimized translation is also typepreserving and has been implemented in the tagless-final style. We show by examples that the optimized
PPS translation generates much smaller terms than the naive PPS translation and the CPS translation.
The rest of this paper is organized as follows: Section 2 explains delimited-control operators andanswer-type modification by a simple example. Section 3 informally states how we simulate answertype modification using multi-prompt shift and reset, and Section 4 gives a formal account to it including
formal properties. Section 5 describes the syntax-directed translation and its property, and Section 6
introduces an optimized translation with examples. Based on these theoretical developments, Section 7
gives a tagless-final implementation of shift and reset with answer-type modification as well as several
programming examples. Section 9 gives related work and concluding remarks.

2

Delimited-Control Operators and Answer-type Modification

We introduce a simple example which uses delimited-control operators shift and reset where the answer
types are modified through computation.
The following implementation of the append function is taken from Danvy’s paper [7]. This program
uses shift operator instead of call/ct operator.
let rec append lst = match lst with| [] → shift (fun k → k)
| x :: xs → x :: append xs
in let append123 =reset (append [1;2;3])
inappend123 [4;5;6]

The function append takes a value of type int list as its input, and traverses the list. When it
reaches the end of the list, it captures the continuation (fun ys -> reset 1 :: 2 :: 3 :: ys inthe functional form) up to the nearest reset, and returns the continuation as its result. We then apply it to
the list [4;5;6] to obtain [1;2;3;4;5;6], and it is easy to see that the function deserves its name.
Let us check the type of append. We initially guess that the return type of append (called its
answer type) is int list, since in the second branch of the case analysis, it returns x :: append xs.
However, the final result is a function from list to list, which is different from our initial guess. The
answer type has been modified during the execution of the program.

I. Kobori, Y. Kameyama & O. Kiselyov

3

Since its discovery, this feature has been used in many interesting examples with shift and reset, fromtyped printf to suspended computations, to coroutines, and even to computational linguistics. Nowadays,
it is considered as one of the most attractive features of shift and reset.
Although the feature, answer-type modification, is interesting and sometimes useful, it is very hardto directly embed such control operators in conventional functional programming languages such as
OCaml, as it requires a big change of the type system; a typing judgment in the form Γ ` e : τ must bechanged to a more complex form Γ ` e : τ; α, β where α and β , resp., designate the answer types before
and after the execution of e, resp. Although adjusting a type system in this way is straightforward intheory, it is rather difficult to modify existing implementations of type systems, and we therefore needa way to represent the above features in terms of standard features and/or mild extensions of existing
programming languages.
This paper addresses this problem, and proposes a way to translate away the feature of ATM using
multi-prompt control operators.

3

Simulating ATM with Multi-prompt shift/reset

In this section, we explain the basic ideas of our translation. Kiselyov implemented typed printf in termsof shift and reset without ATM, and we have generalized it to a translation from arbitrary terms in thesource language.
Consider a simple example with answer-type modification: Lh5+S k.kiM in which S is the delimitedcontrol operator shift, and h· · ·i is reset. Its answer type changes through computation, as its initial answer
type is int while its final answer type is int->int.
Let us translate the example where LeM and JeK denote the results of the translations of the term e.
(The precise definition of the translations are given later.)
We begin with the translation of a reset expression:
LheiM = P p.Pq.hlet y = JeKpq in Sq z. yi p
where the primitive P p creates a new prompt (which is also written as p for brevity) and binds thevariable p to it. For brevity, the variable p which stores a prompt may also be called a prompt.
The translated term, when it is executed, first creates new prompts p and q and its body e is applied
to the arguments p and q. Its result is stored in y and then we execute Sq z.y, but there is no reset withthe prompt q around it. Is it an error ? Actually, no. As we will see in the definition below, JeK is always
in the form λ p.λ q.e0 and during the computation of e0 , S p is always invoked. Hence e0 never returns
normally, and the “no reset” error does not happen. The invariants in the translation are that the firstargument (the prompt p) corresponds to the reset surrounding the expression being translated, and thesecond argument (the prompt q) corresponds to the above (seemingly dangerous) shift.
For each occurrence of answer-type modification from α to β , we use two prompts to simulate thebehavior. The prompts p and q generated here correspond to the answer types β and α, respectively.
We translate the term 5 to J5K = λ p.λ q. S p k. hk 5iq and the term h5i is translated (essentially) to:P p.Pq.hlet y = S p k.hk 5iq in Sq z. yi p
When we execute the result, S p captures its surrounding evaluation context hlet y = [ ] in Sq z. yi p , binds
k to its functional form λ x.hlet y = x in Sq z. yi p , and continues the evaluation of hk 5iq . Then we get:hhhlet y = 5 in Sq z. yi p iq i p

4

ATM without Tears

and when this Sq is invoked, it is surrounded by a reset with the prompt q, and thus it is safe. The final
result of this computation is 5. In this case, since the execution of the term 5 does not modify the answer
type, the prompts p and q passed to the term J5K correspond to the same answer type, but we will soonsee an example in which they correspond to different answer types.
A shift-expression is translated to:
JS k.eK = λ p.λ q.S p k0 .let k = (λ y.h(λ .Ω)(k0 y)iq ) in LeM

As we have explained, p is the prompt for the reset surrounding this expression, hence S p in the translated term will capture a delimited continuation up to the reset (which, in turn, corresponds to the nearest
reset in the source term). However the delimited continuation contains a dangerous shift at its top position, so we must somehow detoxify it. For this purpose, we replace the captured continuation k0 by
a function λ y.h(λ .Ω)(k0 y)iq in which the calls to k0 is enclosed by a reset with the prompt q, and thedangerous shift in k0 will be surrounded by it, sanitizing the dangerous behavior.
Let us consider the types of captured continuations in this translation. Suppose the term S k.e modifies the answer type from α to β . We use the prompts p and q, whose answer types1 are β and α,
respectively. In the source term, the continuation captured by shift (and then bound to k) has the type
τ → α. In the translated term, the continuation bound to k0 has the type τ → β , since the continuation was captured by a shift with the prompt p. After some calculation, it can be inferred that the term
λ y.h(λ .Ω)(k0 y)iq has the type τ → α, hence we can substitute it for k. 2
We show the mechanism for detoxifying a dangerous shift by executing Lh5 + S k.kiM, which isequivalent to:
P p.Pq.hlet y = Pr.((Sr k.hk 5iq ) + (S p k0 .let k = λ u.h(λ w.Ω)(k0 u)ir in k)) in Sq z.yi p
where the subterm starting with Sr is the translation result of 5, and the one with S p is that of S k.k. In
general, each subterm may modify answer types. Hence, a term e1 + e2 needs three prompts corresponding to the initial, final, and intermediate answer types. The prompt r generated here corresponds to theintermediate answer type.
Evaluating this term in call-by-value, and right-to-left order (after generating all the prompts) leads
to the term: hlet k = λ u.h(λ w.Ω)(k0 u)ir in ki p where k0 is the delimited continuation λ x.hlet y =(Sr k.hk 5iq ) + x in Sq z.yi p . The result of this computation is λ u.h(λ w.Ω)(k0 u)ir , which is essentiallyequivalent to λ y.h5 + yi. To see this, applying it to 9 yields:(λ u.h(λ w.Ω)((λ x.hlet y = (Sr k.hk 5iq ) + x in Sq z.yi p )u)ir ) 9∗h(λ w.Ω)hlet y = (Sr k.hk 5iq ) + 9 in Sq z.yi p ir

Sr k.hk 5iq captures the context with the dangerous shift∗hh(λ u.h(λ w.Ω)hlet y = u + 9 in Sq z.yi p ir )5iq ir∗hhh(λ w.Ω)hlet y = 5 + 9 in Sq z.yi p ir iq ir∗

hh14iq ir

which reduces to 14.

Thus, our translation uses two prompts to make connections to two answer types, where prompts are
generated dynamically.
1 We assume that, our target language after the translation has multi-prompt shift and reset, but no answer-type modification.

Hence, each prompt has a unique answer type.
2 Here Ω is a term which has an arbitrary type. Such a term can be expressed, as, for instance, P p.S k.λ x.x. Its operationalpbehavior does not matter, as it will be never executed.

I. Kobori, Y. Kameyama & O. Kiselyov(evaluation contexts)(pure evaluation contexts)

EF

5[ ] | e E | E v | hEi[ ] | eF | F v

::=
::=

E[(λ x.e) v]

E[e{v/x}]

E[let x = v in e]E[e{v/x}]E[hvi]
E[hF[S k.e]i]E[v]E[he{k := λ y.hF[y]i}i]

y is a fresh variable for F

Figure 1: Operational Semantics of Source Calculus

4

Source and Target Calculi

In this section, we formally define our source and target calculi.
The source calculus is based on Asai and Kameyama’s polymorphic extension of Danvy and Filinski’s calculus for shift and reset, both of which allow answer-type modification [8, 2]. We slightly
modified it here; (1) we removed fixpoint and conditionals (but they can be added easily), (2) we use
value restriction for let-polymorphism while they used more relaxed condition, and (3) we use Biernacka
and Biernacki’s simplification for the types of delimited continuations [5].
The syntax of values and terms of our source calculus λ ATM is defined as follows:(values)(terms)

v
e

::=
::=

x | c | λ x.e
v | e1 e2 | let x = v in e | S k.e | throw(k, e) | hei

where x is an ordinary variable, k is a continuation variable, and throw(k, e) is application for continuations, which is syntactically different from ordinary application e1 e2 . This distinction is technical andinessential for expressivity, as we can always convert a continuation k to a value λ x.throw(k, x). The
variables x and k, resp., are bound in the terms λ x.e and S k.e, resp.,
Figure 1 defines call-by-value operational semantics to the language above where [ ] denotes theempty context and E[e] denotes the usual hole-filling operation. Evaluation contexts are standard, andpure evaluation contexts are those evaluation contexts that have no resets enclosing the hole. We use theright-to-left evaluation order for the function application to reflect the semantics of the OCaml compiler.
The first two evaluation rules are the standard beta and let rules where e{v/x} denotes captureavoiding substitution. The next two rules are those for control operators: if the body of a reset expression
is a value, the occurrence of reset is discarded. If the next redex is a shift expression, we capture the continuation up to the nearest reset (λ y.hF[y]i), and substitute it for k in the body. {k := λ y.hF[y]i} denotes
capture-avoiding substitution for continuation variables where we define throw(k, e){k := λ y.hF[y]i} ash(λ y.hF[y]i) (e{k := λ y.hF[y]i})i, namely throw(k, e) is the same as hk ei in the original formulation [9].
The other cases of the substitution are the same as the standard definition.
Types, type schemes and type environments are defined as follows:τ, σ , α, β ::= t | b | σ → τ | (σ /α → τ/β )A ::= τ | ∀t.A
Γ ::= 0/ | Γ, x : A | Γ, k : σ → τTypes are either type variables (t), base types (b), pure function (continuation) type (σ → τ), or effectful
function types (σ /α → τ/β ), which represent function types σ → τ where the answer type changes from6

ATM without Tears
x : A ∈ Γ, τ < AvarΓ `p x : τΓ `p e : τexpΓ ` e : τ; α, α
Γ, x : σ ` e : τ; β , γΓ ` e1 : (σ /α → τ/β ); β , γΓ ` e2 : σ ; γ, δappfun
Γ ` p λ x.e : (σ /β → τ/γ)Γ ` e1 e2 : τ; α, δΓ, k : σ → τ ` p e : σΓ ` e : σ; σ, τΓ, k : τ → α ` p e : β
reset
throw
shift
hei
Γ `p
:τ
Γ, k : σ → τ ` p throw(k, e) : τΓ ` S k.e : τ; α, β(c is a constant of type b)constΓ `p c : bΓ `p v : σ
Γ, x : Gen (σ ; Γ) ` e : τ; α, βlet
Γ ` let x = v in e : τ; α, βFigure 2: Typing Rules of the Source Calculus

α to β . Type scheme A represents polymorphic types as usual. Type environment Γ is a finite sequenceof variable-type pairs, which possibly contains continuation variables k, that has a pure function typeσ → τ.
Figure 2 defines the type system of λ ATM . Type judgments are either Γ ` p e : τ (pure judgments) orΓ ` e : τ; α, β (effectful judgments), the latter of which means that evaluating e with the answer type αyields a value of type τ with the answer type being modified to β . The typing rules are based on Danvy
and Filinski’s [8] except that we have let-polymorphism and clear distinction of pure judgments from
impure judgments following Asai and Kameyama [2].
In the var rule, τ < A means that the type τ is an instance of type scheme A, and the type Gen (σ ; Γ)denotes ∀t1 , · · · ∀tn .σ where t1 , · · · ,tn are the type variables that appear in σ but not appear in Γ freely.
The delimited continuations captured by shift expressions are pure functions (they are polymorphic inanswer types), and we use the pure function space τ → α for this purpose. On the contrary, the functions
introduced by lambda are, in general, effectful. Accordingly, we have two rules for applications. Notethat the body of a shift expression is restricted to a pure expression in order to simplify the definitionof our translation. This restriction is inessential; in the standard formulation (where the body of shift isan effectful expression), the term S x.e is typable if and only if S x.hei is typable, and their operational
behaviors are the same. The exp rule turns pure terms into effectful terms where we have chosen an
implicit coercion from a pure term to an effectful one.
The type system of the source calculus λ ATM enjoys the subject reduction property. The proof isstandard and omitted.
We introduce the target calculus λ mpsr , which is a polymorphic calculus with multi-prompt shift andreset without ATM. The calculus is similar, in spirit, to Gunter et al.’s calculus with the cupto and set
operators [13]. Besides disallowing ATM, the target calculus differs from the source calculus in that thecontrol operators are named, to allow mixing multiple effects in a single program. The names for control
operators are called prompts for historical reasons, and denoted by p, q, · · · . In our formulation, prompts
are first-class values and can be bound to ordinary variables x. Prompts are given as prompt-constants, orcan be generated dynamically by the P primitive. For instance, evaluating Px.h1 + Sx k.eix first createsa fresh prompt p and substitutes it for x, then it evaluates h1 + S p k.ei p . This choice of the formulation
closely follows Kiselyov’s DelimCC library for multi-prompt shift and reset.

I. Kobori, Y. Kameyama & O. Kiselyov

7

x : A ∈ Γ, τ < A(c is a constant of b)
omega
var
const
Γ`Ω:τ
Γ` x:τ
Γ`c:b
Γ ` e1 : σ → τΓ ` e2 : σ app
Γ, x : σ ` e : τfunΓ ` e1 e2 : τΓ ` λ x.e : σ → τΓ ` v : τ pr
Γ`e:τΓ ` v : σ prΓ, x : τ → σ ` e : σ
reset
shift
Γ ` heiv : τΓ ` Sv x.e : τΓ, x : σ pr ` e : τΓ`v:σΓ, x : Gen (σ ; Γ) ` e : τpromptletΓ ` Px.e : τΓ ` let x = v in e : τ
Figure 3: Typing Rules of the Target Calculus
Types and typing environments are defined as follows:τ, σ ::= t | b | σ → τ | τ pr
A ::= τ | ∀t.A
Γ ::= 0/ | Γ, x : A
where τ pr is the type for the prompts with the answer type τ. The syntax of values and terms are defined
as follows:v ::= x | c | λ x.e | p
e ::= v | e1 e2 | Sv x.e | heiv | Px.e | let x = v in e | Ω
where p is a prompt-constant. The control operators now receive not only prompt-constants, but values
which will reduce to prompts. Other values are rejected by the type system. The term Px.e creates a
fresh prompt and binds x to it. The term Ω denotes a non-terminating computation of arbitrary types. It
may be defined in terms of shift, but for the sake of clarity, we added it as a primitive.
Evaluation contexts and evaluation rules are given as follows:
E ::= [ ] | Ee | vE | hEi p
E[(λ x.e)v]

E[e{v/x}]

E[let x = v in e]E[e{v/x}]E[Px.e]E[e{p/x}]E[hvi p ]E[v]

E[hE p [S p x.e]i p ]E[Ω]p is a fresh prompt-constantE[he{λ y.hE p [y]i p /x}i p ]E[Ω]Note that we use E p in the second last rule, which is an evaluation context that does not have a reset withthe prompt p around the hole, and thus implies that we capture the continuation up to the nearest resetwith the prompt p.
Finally we give typing rules for the target calculus in Figure 3. The type system of the target calculus
is mostly standard except for the use of prompts. In the shift rule, the prompt expression v must be oftype σ pr where σ is the type of the body of the shift expression. A similar restriction is applied to thereset rule. In the prompt rule, we can create an arbitrary prompt and bind a variable x to it.
The type system enjoys the subject reduction property modulo the set of dynamically created prompts
which have infinite extents.

8

ATM without Tears

Jτ; α, β K = Jβ K pr → JαK pr → JτK
JbK = bJtK = tJσ → τK = Jσ K → JτK

Jσ /α → τ/β K = Jσ K → Jτ; α, β K
J∀t.AK = ∀t.JAK
J0K/ = 0/

JΓ, x : AK = JΓK, x : JAKJΓ, k : σ → τK = JΓK, k : Jσ K → JτK
Figure 4: Translation for Triples, Types, Type Schemes and Type Environments

LxM = x
LcM = cLλ x.eM = λ x.JeK

Lthrow(k, e)M = k LeM

LheiM = P pq.h(λ y.Sq .y)(JeKpq)i p

Je1 e2 K = λ pq.Prs.(Je1 Krs)(Je2 Kpr)sq

Jlet x = v in e2 K = λ pq.let x = LvM in Je2 Kpq

JS k.eK = λ pq.S p k0 .((λ k.LeM)(λ y.h(λ .Ω)(k0 y)iq )JeK = λ pq.S p k.hkLeMiq

if e = x, c, λ x.e0 , he0 i or throw(k, e0 )Figure 5: Translation for Typed Terms

5

The PPS Translation

In this section, we give a Prompt-Passing Style (PPS) translation, the syntax-directed translation from
λ ATM to λ mpsr , which translates away the feature of answer-type modification.
The translation borrows the idea of Kiselyov’s implementation of typed printf in terms of multiprompt shift and reset, but this paper gives a translation for the whole calculus and also proves the typepreservation property. Later, we will show a tagless-final implementation based on our translation which
is another evidence that our translation actually preserves typing.
Figure 4 defines the translation rules for types, type schemes, type environments and triples.
As we have explained in earlier sections, we emulate ATM from the type α to the type β in terms oftwo prompts whose answer types are α pr and β pr. Hence the triple τ; α, β in the typing judgment istranslated to the type Jβ K pr → JαK pr → JτK.
Types are translated in a natural way except the type for effectful functions σ /α → τ/β ; it is translated to a function type whose codomain is the translation of the triple Jτ; α, β K. Type schemes and typeenvironments are translated naturally.

I. Kobori, Y. Kameyama & O. Kiselyov

9

Figure 5 defines the translation for typed terms in λ ATM , which consists of the translation LeM for apure term e, and the translation JeK for an effectful term e. These translations are defined for typed terms
only, since the translation for throw(k, e) (and S k.e) contains LeM, which is defined only for a pure terme.
The first translation LeM does little for most constructs but reset terms. A reset term hei is translated
to a term which creates two new prompts p and q, and inserts a combination of reset-p and shift-q as we
explained earlier. Then it supplies p and q to its immediate subterm JeK.
The second translation JeK does a lot; For application e1 e2 , it receives two prompts p and q, butalso generates two new prompts r and s and distributes these prompts to its subterms etc. For a let-term
let x = v in e, it passes two prompts.
The translation of a shift term S k.e is a way more complicated than others; it receives two prompts
p and q and invokes shift to capture the delimited continuation and binds k0 to it. The captured delimited
continuation is slightly different from the one which would have been obtained by the shift-operator in
the source term, since we have inserted a combination of reset-p and shift-q at the position of reset. As
we have explained in Section 3, this (bad) effect is resolved by detoxifying the continuation, which isrealized by the involved term found in the translation above.
The last clause for JeK applies only when the type of the term e is derived by applying the exp rule as
its last rule. In this case, the translation generates a term which receives two prompts p and q, detoxify
the effect of the delimited continuation (mentioned above) by the combination of shift-p and reset-q.
We can show that our translation preserves typing.
Theorem 1 (Type preservation). If Γ ` e : τ; α, β is derivable in the source calculus λ ATM , then JΓK `JeK : Jτ; α, β K is derivable in the target calculus λ mpsr .
Similarly, if Γ ` p e : τ is derivable in λ ATM , so is JΓK ` LeM : JτK in λ mpsr .
Proof. We will prove the two statements by simultaneous induction on the derivations. Here we only
show a few interesting cases.
(Case e = he1 i) We have a derivation for:Γ ` e1 : σ ; σ , τΓ ` p he1 i : τ
By induction hypothesis, we can derive JΓK ` Je1 K : Jσ ; σ , τK. Let Γ0 = JΓK, p : JτK pr, q : Jσ K pr, Γ00 =Γ0 , y : Jσ K, and Γ000 = Γ00 , x : JτK → Jσ K. We have the following derivation:
Γ000 ` q : Jσ K pr

Γ000 ` y : Jσ K

Γ00 ` Sq x.y : JτK

Γ0 ` p : JτK pr

Γ0 ` λ y.Sq x.y : Jσ K → JτKΓ0 ` q : Jσ K pr
Γ0 ` λ y.Sq x.y (Je1 Kpq) : JτK

Γ0 ` p : JτK pr

Γ0 ` Je1 K : Jσ ; σ , τK0
Γ ` Je1 Kp : Jσ K pr → Jσ K

Γ0 ` Je1 Kpq : Jσ KΓ0 ` h λ y.Sq x.y (Je1 Kpq)i p : JτKJΓK ` P p.Pq.h λ v.Sq x.v (Je1 Kpq)i p : JτK

which derives JΓK ` Lhe1 iM : JτK.
(Case e = S x.e1 ) We have a deviation forΓ, k : τ → α ` p e1 : βΓ ` S k.e1 : τ; α, β
By induction hypothesis JΓ, k : τ → αK ` Le1 M : Jβ K is derivable. Let Γ0 = JΓK, p : Jβ K pr, q : JαK pr,
Γ00 = Γ0 , k0 : JτK → Jβ K, and Γ000 = Γ00 , y : JτK, then we have:10

ATM without Tears
Γ000 ` h(λ .Ω) (k0 y)iq : JαK
Γ00 , k : JτK → JαK ` Le1 M : Jβ K
Γ00 ` λ k.Le1 M : (JτK → JαK) → Jβ K
Γ00 ` λ y.h(λ .Ω) (k0 y)iq : JτK → JαKΓ00 ` p : Jβ K pr
Γ00 ` (λ k.Le1 M) (λ y.h(λ .Ω) (k0 y)iq ) : Jβ K
Γ0 ` S p k0 . (λ k.Le1 M) (λ y.h(λ .Ω) (k0 y)iq ) : JτKJΓK ` λ p.λ q.S p k0 . (λ k.Le1 M) (λ y.h(λ .Ω) (k0 y)iq ) : Jβ K pr → JαK pr → JτK

which derives JΓK ` JS k.e1 K : Jτ; α, β K.
Hence our translation preserves typing. We conjecture that our translation also preserve operationalsemantics but its proof is left for future work.

6

Optimization

The naive PPS translation in Section 5 works in theory, but is suboptimal for practical use, as it introduces
too many prompts. To solve this problem, we will introduce an optimized PPS translation in this section.
For the purpose of comparison, we consider the term hen i for a natural number n, where en is 1 +(2 + · · · + (n + S k.λ x.throw(k, x)) · · · ).3 Then we can derive ` en : int; int, (int/α → int/α) and` p hen i : (int/α → int/α) for some type α, in the type system of λ ATM augmented by the following
type rule for addition:Γ ` e1 : int; α, γΓ ` e2 : int; γ, βΓ ` e1 + e2 : int; α, βThe type rule for addition in the target calculus is standard and omitted.
We define the (naive) PPS translation for addition by Je1 + e2 K ≡ λ p.λ q.Pr. (Je1 Krq) + (Je2 Kpr). It
is easy to see that the naive PPS translation in the previous section translates hen i to a rather big term
which dynamically generates n + 2 prompts (2 for reset, and 1 for each addition) and passes them around.
This is not ideal and needs improvement.
Eliminating Unnecessary Prompt Passing
We first eliminate unnecessary dynamic passing of prompts. Since the residual terms of the naivetranslation often contain JeKpq as subterms where JeK takes the form λ p.λ q. · · · , they contain many beta
redexes (administrative redexes) that can be eliminated at the translation time, by adjusting the one-pass
CPS translation by Danvy and Filinski [10] to our PPS translation.
Figure 6 gives our one-pass PPS translation where function applications are made explicit (by the
infix symbol @), and the overline (e.g. @) means static constructs which are reduced at the translation
time, while the underline (e.g. @) means dynamic constructs which remain in the residual terms.
The one-pass PPS translation eliminates unnecessary prompt passing; Applying one-pass PPS translation to a term in λ ATM , and reducing all static beta-redexes (λ p.e1 )@q to e1 {q/p}, one obtains a term
without static constructs (constructs with overlines). The residual terms of one-pass PPS translation pass
prompts only for function applications; in Figure 6, dynamic application for prompts e@p@q appears in
the term Je1 e2 K1pass only.
The one-pass PPS translation gives a much better result than the naive one, as it eliminates unnecessary prompt passing, but it still generates as many prompts as the naive one.
Eliminating Unnecessary Prompt Generation
We eliminate unnecessary prompt generation. Our idea is simple; if the term being translated is pure,
we do not have to generate prompts. In the translation of Je1 + e2 K = λ p.λ q.Pr. (Je1 Krq) + (Je2 Kpr),
3 The term S k.λ x.throw(k, x) is written as S k.k in the standard formulation.

I. Kobori, Y. Kameyama & O. Kiselyov

11

LxM1pass = x
LcM1pass = c

Lλ x.eM1pass = λ x.λ pq.JeK1pass @p@q

Lthrow(k, e)M1pass = k@Le2 M1pass

LheiM1pass = P p.Pq.h(λ y.Sq .y)@(JeK1pass @p@q)i p

Je1 + e2 K1pass = λ pq.Pr.(Je1 K1pass @r@q) + (Je2 K1pass @p@r)

Je1 e2 K1pass = λ pq.Pr.Ps.(Je1 K1pass @r@s)@(Je2 K1pass @p@r)@s@q

Jlet x = v in e2 K1pass = λ pq.let x = LvM1pass in Je2 K1pass @p@q
JS k.eK1pass = λ pq.S p k0 .(λ k.LeM1pass )@ λ y.h(λ .Ω)@(k0 @y)iq
JeK1pass = λ pq.S p k.hk@LeM1pass iq

if e = x, c, λ x.e0 , he0 i or throw(k, e0 )Figure 6: One-Pass PPS Translation
the new prompt r is used to bridge Je1 K and Je2 K, and if one of e1 and e2 is pure, we can reuse p and q
to simulate ATM. For instance, if e1 is pure and e2 is effectful, we can define Je1 + e2 K = λ p.λ q.Le1 M +(Je2 Kpq).
To maximize the benefit of this optimization, we extend the notion of a pure term e p to a quasi-pureterm (or a q-pure term) eq by:
e p ::= x | c | λ x.e | hei | throw(k, e)
eq ::= e p | let x = v in eq
Namely, we allow nested let constructs appearing around pure terms. For instance, let x = 3 in let y =5 in 7 is not pure, but is q-pure.
Figure 7 defines the optimized PPS translation; LeMopt for a q-pure term e, and JeKopt for a non qpure term e. We omit the cases whose translation is the same as those for one-pass PPS translation.
The optimized PPS translation dispatches if each subterm is q-pure or not, and in the former case, it
gives an optimized result where prompt generation is suppressed. Translation for addition can be definedsimilarly, for instance, Je1 + e2 Kopt = λ pq.Le1 Mopt + (Je2 Kopt @p@q) if e1 is q-pure and e2 is not.
We compute Jhen iK and reduce all static redexes in it, to obtain the following term:4
P p.Pq. h(λ y.Sq .y)(1 + (2 + · · · + (n + (S p k0 .(λ k.Lλ x.throw(k, x)Mopt )@(λ y.h. . .iq ))) · · · ))i p
where only two prompts are generated at the beginning of the computation. The result is quite close to
the source term, and in fact, the source and target terms differ only at the control operators. Although
it is possible to further optimize the results, by applying partial evaluation techniques for shift and reset(e.g. [1]), we believe that our translation is practical and efficient. In the next section, we show animplementation of our translation based on the optimized PPS translation.
We can prove that the optimized PPS translation preserves types where the type system of the target
calculus λ mpsr has two function types σ →τ (static) and σ →τ (dynamic). Namely, we can prove that, if
4 We omitted the underlines in the result.

12

ATM without Tears(

λ x.λ pq.S p k.hk@Le1 Mopt iq

Lλ x.e1 Mopt =Lhe1 iMopt =

λ x.λ pq.JeKopt @p@q

if e1 is q-pureotherwise

Le1 Mopt
P p.Pq.h(λ y.Sq .y)@(Je1 Kopt @p@q)i p

if e1 is q-pureotherwise


opt
opt

2 M @p@q λ pq.Le1 M @Le
λ pq.Pr.Le1 Mopt @(Je2 Kopt @p@r)@r@q
Je1 e2 Kopt =
λ pq.Pr.(Je1 Kopt @p@r)@Le2 Mopt @r@q
 λ pq.Pr.Ps.(Je Kopt @r@s)@(Je Kopt @p@r)@s@q
1
2
Llet x = v in e1 Mopt = let x = LvMopt in Le1 Mopt
opt

Jlet x = v in e1 K

= λ pq.let x = LvM

opt

if e1 and e2 are q-pureif e1 is q-pure and e2 is not
if e2 is q-pure and e1 is nototherwise

if e1 is q-purein Je1 Kopt @p@q if e1 is not q-pure

Figure 7: Optimized PPS Translation (new cases only)Γ ` e : τ; α, β is derivable in λ ATM and e is not q-pure, so is JΓKopt ` JeKopt : Jβ Kopt pr→JαKopt pr→JτKopt
in λ mpsr . Similarly, if Γ ` e : τ; α, α is derivable and e is q-pure, or Γ ` p e : τ is derivable, so is JΓKopt `LeMopt : JτKopt . The details of this development and proofs are omitted.

7

Tagless-final embedding

We have implemented the calculus λ ATM in Figure 2 and the naive and optimized PPS translations inFigures 4, 5 and 7 for a monomorphic version of λ ATM .
Our implementation is based on the tagless-final style [6, 17], which allows one to embed a typed
domain-specific language (DSL) in a metalanguage. In this style, the syntax as well as the typing rules of
DSL are represented by a signature (an interface of modules), and its semantics is given as an interpretation of this signature. One of the important merits with this style is that type checking (or type inference)of DSL is automatically done by the type checker (or the type inferencer) of the metalanguage. Although
we have already proved the subject reduction property of λ ATM and the type preservation property for
the PPS translations, implementing them in the tagless-final style gives us another indication for well
typedness. It is particularly useful when we extend the source calculus and the translation; type errors
are immediately raised by the type system of the metalanguage.
We have chosen OCaml plus the DelimCC library as the metalanguage, where DelimCC gives an efficient implementation for multi-prompt shift and reset [16]. We also give an implementation in MetaOCaml, a multi-stage extension of OCaml, to generate (and show) the translated terms, rather than immediately executing them.
Figure 8 shows the signature called Symantics for our source calculus λ ATM . It represents the syntax
and the typing rules of λ ATM ; the types τ pure and (τ, α, β ) eff, resp., represent the relations
Γ ` p e : τ and Γ ` e : τ; α, β , resp. The type (σ , τ, α, β ) efun represents the effectful function
type (σ /α → τ/β ) and (σ , τ) pfun the pure function type σ → τ for continuations. Since all thesetypes are kept abstract, we can arbitrarily instantiate them in different implementations. Each function
but run encodes a typing rule in λ ATM . For instance, the function exp encodes the exp rule in λ ATM ,and does not have a concrete primitive in DSL. The function run does not correspond to a constructor in

I. Kobori, Y. Kameyama & O. Kiselyov

13

module type Symantics = sig
type τ pure(∗ pure expression ∗)type (τ, α, β ) eff(∗ effectful expression ∗)type (σ , τ, α, β ) efun(∗ effectful function type ∗)type (σ , τ) pfun(∗ pure function type ∗)val const : τ → τ pureval lam : (σ pure → (τ, α, β ) eff) → (σ , τ, α, β ) efun pureval app : ((σ , τ, α, β ) efun, β , γ) eff→ (σ , γ, ’d) eff → (τ, α, ’d) eff
val throw : (σ , τ) pfun pure → σ pure → τ pureval shift : ((τ, α) pfun pure → β pure) → (τ, α, β ) eff
val reset : (σ , σ , τ) eff → τ pureval exp : τ pure → (τ, α, α) eff
val run : τ pure → τ
end

Figure 8: Signature of the Embedded Language
DSL; it converts a DSL value to a value in the metalanguage, and is thus useful to test interpreters.
As an example, a DSL term S k.λ x.throw(k, x) is represented by the term
shift (fun k → lam (fun x → exp (throw k x))), which encodes a type derivation of theabove DSL term using higher-order abstract syntax. Note that, we can represent all and only typable
terms in λ ATM using this signatures, and the typability of embedded terms are checked by OCaml; allrepresentable terms are typable as they are constructed.
In the tagless-final style, operational semantics of the embedded language is given as an interpretation of the Symantics signature, namely, a module of type Symantics. For this work, we have given two
interpretations for each of two PPS translations, and thus obtained four interpreters. The two interpretations differ in the target; the first one, called the R interpreter, translates the source term and evaluates
the result. The second one, called the S interpreter5 translates the source term and generates the result asa code in MetaOCaml, which can be executed by the run primitive.
Due to lack of space, we cannot list the source code of these interpreters, but it should be noted thatthe two PPS translations (the naive one and the optimized one) have been successfully implemented in
the tagless-final style. After extending the source calculus with conditional, recursion and so on, we canwrite programming examples such as list-append in Section 1, list-prefix and others, and running theseexamples gives correct answers.
Figure 9 shows a few results of the optimized translation with the S interpreter. We first define
append and a test program res1. Then we translate res1 and run it, to obtain the desired list. We thentranslate append itself (but not run it), to obtain the code .<let rec g_56 ...>. where the variable
g_56 corresponds to6 the append function in Section 1. The result is instructive; control operators7
are used only at the point where shift was there in the source term, in particular, no dynamic prompt
generation happens during the recursive calls for append. This result clearly shows the merit of our
optimized translation over the naive translation as well as the definitional CPS translation [9].
This implementation also provides a good evidence that our translation is type preserving. Thanks to
5 The S interpreter is actually a compiler.
6 MetaOCaml renames all bound variables.
7 Delimcc.shift is shift and Delimcc.push prompt is reset.

14

ATM without Tears

module Example (S: SymPL) = structopen S
let append = fixE (fun f x →ifE (null @@ exp x) (shift (fun k → k))(head (exp x) @∗ app (exp f) (tail @@ exp x)))let res1 = run @@throw (reset (app (exp append) (exp @@ list [1;2;3])))(list [4;5;6])
end# let _ = let module M = Example(SPL_opt) in M.res1;;− : int list = [1; 2; 3; 4; 5; 6]# let _ = let module M = Example(SPL_opt) in M.append;;− : (int list, int list, int list, (int list, int list) SPL_opt.pfun)
SPL_opt.efun SPL_opt.pure= .<let rec g_56 x_57 p_58 q_59 =if x_57 = []thenDelimcc.shift p_58
(fun k’_62 →(fun x_64 → x_64)(fun y_63 →Delimcc.push_prompt q_59
(fun () →(fun _ → Pervasives.failwith "Omega") @@ (k’_62y_63))))
else(let v2_60 = g_56 (List.tl x_57) p_58 q_59 in
let v1_61 = List.hd x_57 in v1_61 :: v2_60) in
g_56>.

Figure 9: Programming Examples
the tagless-final style, our implementation is extensible, and in fact, it was easy to add primitives such as
the fixpoint operator to our source language in a type-safe way.

8

The List-prefix Example

The append function in Section 2 is not the only interesting example which uses shift and reset. Danvy [7]represented various programming examples using these control operators. In this section we take the listprefix example from his work, and show that it is correctly translated and implemented in our system.
The list-prefix function prefix takes a list as its input, and returns the list of all prefixes of the input.
For example, prefix [1;2;3] yields the list [[1]; [1;2]; [1;2;3]]. Using the control operators
shift and reset, prefix can be implemented as follows:
let prefix l =let rec aux = function

I. Kobori, Y. Kameyama & O. Kiselyov

15| [] → shift (fun k → [])| x :: xs → x :: shift (fun k → k [] :: reset (k (aux xs)))
in reset (aux l)This implementation is interesting for two reasons; first, it traverses the input only once. Second, it
creates no intermediate lists (explicitly). One can easily imagine that a straightforward implementationof the function would not satisfy these two properties.
Let us infer the type of the inner function aux. The pattern match has two cases, and on the second
branch, the answer type before the execution of this shift is α list, since the function returns x ::shift (fun k → ...), which has a list type. Then, the continuation captured by this shift has thetype α list → α list, which implies that k [] has the type α list. Finally, the answer type after
the execution of this shift is α list list, since it returns (k []) :: .... We have just observedthat the answer type changed from α list to α list list during the execution of the second branchof aux.
The functions aux and prefix are typable in λ ATM with a few extensions such as lists and recursion.
In fact, our tagless-final implementation can cope with these extensions and we only have to rewrite
pattern matching by conditionals. Our implementation of the function prefix is shown below:
module Ex2 (S: SymPL) = structopen S
let prefix = fixE (fun f x →ifE (null @@ exp x)(shift (fun k → list []))
(head (exp x) @∗ shift (fun k →reset @@ (exp (throw k (list [])))@∗ (exp (reset @@ app (exp @@ lam (fun x → exp @@ throw k x))(app (exp f) (tail @@ exp x)))))))
let res = run @@ reset @@ app (exp prefix) (exp @@ list [1;2;3])
end

The module Ex2 contains the definition of prefix and its example use res. The type of the term is
automatically infered by the OCaml’s type system, which helps debugging.
Running the example res with our optimized translation, denoted by Ex2(SPL_opt) in the following
code, we get the correct answer for the input [1;2;3] as follows:# let _ = let module M = Ex2(SPL_opt) in M.res;;− : int list list = [[1]; [1; 2]; [1; 2; 3]]

9Related Work and Conclusion

In this paper, we have proposed type-preserving translation for embedding programs with ATM into those
without. Our translation uses multi-prompt systems and dynamic creation of prompts to emulate twoanswer types in effectful terms. We proved type preservation for the naive and optimized translations,and implemented them in OCaml (and MetaOCaml) using the tagless-final style, which we think add
further assurance for type safety.
One may wonder if the reverse translation is possible. The answer is no, as our source calculus λ ATM
is strongly normalizing, while the target λ mpsr is not. An open question is to identify the image of ourtranslation which corresponds to the source calculus.

16

ATM without Tears

Let us briefly summarize related work. Rompf et al. [19] implemented shift and reset in Scala, thatallow answer-type modification. Their source language needs relatively heavy type annotations to be
implemented by a selective CPS transformation, and does not allow higher-order functions. Masuko andAsai [18] designed OchaCaml, which is an extension of Caml light with shift and reset. OchaCaml fully
supports ATM at the cost of redesigning the whole type system and an extension of the run-time system.
Wadler [20] studied monad-like structures to express shift and reset with Danvy and Filinski’s type system [8]. Inspired by his work, Atkey [3, 4] proposed parameterised monads as a generalization of monads. They take two additional type parameters to express inputs and outputs, and therefore, can express
answer-type modification. He studied categorical foundation of parameterised monads. Kiselyov [14]independently studied a similar notion, and gave an implementation and programming examples.
For future work, we plan to formally prove the semantics-preservation property mentioned in thispaper. Investigating other delimited-control operators such as shift0/reset0 and control/prompt withanswer-type modification would be also interesting.
Acknowledgments: We are grateful to the anonymous reviewers and the audience at WoC’15 for theirconstructive comments, and the editors of the post-proceedings, Olivier Danvy and Ugo de’Liguoro forsuggestions and advice. The authors are supported in part by JSPS Grant-in-Aid for Scientific Research(25280020, 25540023).

References[1] Kenichi Asai (2004): Offline partial evaluation for shift and reset. In: Proceedings of the 2004 ACM SIGPLAN Workshop on Partial Evaluation and Semantics-based Program Manipulation, ACM Press, pp. 3–14,
doi:10.1145/1014007.1014009.
[2] Kenichi Asai & Yukiyoshi Kameyama (2007): Polymorphic delimited continuations. In: Proceedings ofFifth Asian Symposium on Programming Languages and Systems, Lecture Notes in Computer Science 4807,
Springer Berlin Heidelberg, pp. 239–254, doi:10.1007/978-3-540-76637-7 16.
[3] Robert Atkey (2006): Parameterised notions of computation. In: Proceedings of the Workshop on Mathematically Structured Functional Programming, eWiC.
[4] Robert Atkey (2009): Parameterised notions of computation. Journal of Functional Programming 19(3-4), p.
335, doi:10.1017/S095679680900728X.
[5] Malgorzata Biernacka & Dariusz Biernacki (2009): Context-based proofs of termination for typed delimitedcontrol operators. Proceedings of the 11th ACM SIGPLAN conference on Principles and practice of declarative programming, p. 289, doi:10.1145/1599410.1599446.
[6] Jacques Carette, Oleg Kiselyov & Chung-Chieh Shan (2009): Finally tagless, partially evaluated: Tagless staged interpreters for simpler typed languages. Journal of Functional Programming 19(05), p. 509,
doi:10.1017/S0956796809007205.
[7] Olivier Danvy (1988): On some functional aspects of control. In: Proceedings of the Workshop on Implementation of Lazy Functional Languages, Program Methodology Group, University of Göteborg and Chalmers
University of Technology, pp. 445–449. Report 53.
[8] Olivier Danvy & Andrzej Filinski (1989): A Functional Abstraction of Typed Contexts. Technical Report,
Computer Science Department, University of Copenhagen.
[9] Olivier Danvy & Andrzej Filinski (1990): Abstracting control. In: Proceedings of the 1990 ACM conferenceon LISP and functional programming, ACM Press, pp. 151–160, doi:10.1145/91556.91622.
[10] Olivier Danvy & Andrzej Filinski (2009): Representing Control: a Study of the CPS Transformation. Mathematical Structures in Computer Science 2(04), p. 361, doi:10.1017/S0960129500001535.

I. Kobori, Y. Kameyama & O. Kiselyov

17[11] Olivier Danvy & Lasse R. Nielsen (2002): A First-Order One-Pass CPS Transformation. In: Foundations ofSoftware Science and Computation Structures, 5th International Conference, FOSSACS 2002, pp. 98–113.
[12] Matthias Felleisen (1988): The theory and practice of first-class prompts. In: Proceedings of the 15th
ACM SIGPLAN-SIGACT symposium on Principles of programming languages, ACM Press, pp. 180–190,
doi:10.1145/73560.73576.
[13] Carl A. Gunter, Didier Rémy & Jon G. Riecke (1995): A generalization of exceptions and control in ML-likelanguages. In: Proceedings of the seventh international conference on Functional programming languages
and computer architecture, ACM Press, pp. 12–23, doi:10.1145/224164.224173.
[14] Oleg Kiselyov (2006): Parametrized ’monad’. http://okmij.org/ftp/Computation/monads.html#
param-monad.
[15] Oleg Kiselyov (2007):
sprintf-cupto.ml.

First-class typed,

direct-style sprintf.

http://okmij.org/ftp/ML/[16] Oleg Kiselyov (2012): Delimited control in OCaml, abstractly and concretely. Theoretical Computer Science
435, pp. 56–76, doi:10.1016/j.tcs.2012.02.025.
[17] Oleg Kiselyov (2012): Typed Tagless Final Interpreters. In: Spring School on Generic and Indexed Programming, Lecture Notes in Computer Science 7470, Springer Berlin Heidelberg, pp. 130–174, doi:10.1007/9783-642-32202-0 3.
[18] Moe Masuko & Kenichi Asai (2011): Caml Light + shift/reset = Caml Shift. In: First International Workshop
on the Theory and Practice of Delimited Continuations, pp. 33–46.
[19] Tiark Rompf, Ingo Maier & Martin Odersky (2009): Implementing first-class polymorphic delimited continuations by a type-directed selective CPS-transform. In: Proceedings of the 14th ACM SIGPLAN international
conference on Functional programming, ACM Press, p. 317, doi:10.1145/1596550.1596596.
[20] Philip Wadler (1994): Monads and composable continuations. LISP and Symbolic Computation 7(1), pp.
39–55, doi:10.1007/BF01019944.