Introduction to
Programming with Shift and Reset
Kenichi Asai

Oleg Kiselyov

September 23, 2011
Abstract
The concept of continuations arises naturally in programming: a conditional branch selects a continuationfrom the two possible futures; raising an exception discards a part of the continuation; a tail-call or ‘goto’ continues with the continuation. Although continuations are implicitly manipulated in every language, manipulatingthem explicitly as ﬁrst-class objects is rarely used because of the perceived diﬃculty.
This tutorial aims to give a gentle introduction to continuations and a taste of programming with ﬁrstclass delimited continuations using the control operators shift and reset. Assuming no prior knowledge on
continuations, the tutorial helps participants write simple co-routines and non-deterministic searches. The
tutorial should make it easier to understand and appreciate the talks at CW 2011.
We assume basic familiarity with functional programming languages, such as OCaml, Standard ML, Scheme,
and Haskell. No prior knowledge of continuations is needed. Participants are encouraged to bring their laptops
and program along.

1

Introduction

Continuations represent the rest of the computation. Manipulation of continuations is a powerful tool to realize
complex control ﬂow of programs without spoiling the overall structure of programs. It is a generalization of
exception handling, but is far more expressive.
Traditional way to handle continuations explicitly in a program is to transform a program into continuationpassing style (CPS) [13]. However, it requires us to transform whole the program (or at least the part of programs
where we want to manipulate continuations) into CPS. If we want to manipulate continuations in a more intuitive
direct-style program, we need control operators.
The most famous control operator is call/cc found in Scheme and Standard ML. However, continuations
captured by call/cc is the whole continuation that includes all the future computation. In practice, most of thecontinuations that we want to manipulate are only a part of computation. Such continuations are called delimitedor partial continuations.
There are several control operators that capture delimited continuations, such as Felleisen’s control/prompt[6], Danvy and Filinski’s shift/reset [4], and Gunter, Rémy, and Riecke’s cupto/prompt [8]. Among them, we
use shift/reset in this tutorial, because their foundation is established the most, having sound and complete
axiomatization [9] as well as polymorphism [2]. Furthermore, because of its clear connection to CPS, many
applications of shift/reset have been proposed.
In this tutorial note, we introduce programming with shift and reset with various examples to experience
what it looks like to program with shift and reset.

1.1

Implementation of shift and reset

There are a number of ways to use shift and reset in various programming languages.
• Filinski [5] showed that shift/reset can be emulated using call/cc and a reference cell. One can use
shift/reset using this method in Scheme and Standard ML. In this emulation, one has to ﬁx the answer
type beforehand for each context.
• Gasbichler and Sperber implemented shift/reset directly on Scheme48 [7]. It is reported that the implementation is much more eﬃcient than emulation using call/cc.
• Racket supports various control operators including shift/reset.
• Kiselyov implements delimited control in Delimcc library [10] for OCaml, Scheme, and Haskell.
1• Masuko and Asai implemented shift/reset directly in MinCaml compiler [11]. It supports type system withanswer-type modiﬁcation and polymorphism. The same idea is used to implement OchaCaml, an extension
of Caml Light with shift/reset [12].
In this tutorial note, we use OchaCaml to explain and demonstrate programming with shift/reset.

1.2

Organization

The next section explains programming with shift and reset with examples and exercises. The section is almost
self-contained and does not require base theory on delimited continuations. For those who are interested in thefoundations of shift/reset, Section 3 shows the brief overview of the base theory of shift/reset. For moredetails, however, readers are referred to read technical papers.

1.3

Prerequisite

We assume general knowledge on functional programming languages, such as OCaml, Standard ML, Scheme,
and/or Haskell, but no prior knowledge on continuations is required. In Section 3, we assume general knowledge
on the λ-calculus with let polymorphism, its evaluation rules and type system.

2

Programming with Shift and Reset

2.1

What are continuations?

Continuations represent the rest of the computation. When a complex program is executed, a next expression
to be evaluated (called redex, a reducible expression) is selected, the redex is evaluated, and the result is used
to execute “the rest of the computation”. This last “rest of the computation” is the continuation of the redex.
Thus, the concept of continuations arises in any programming languages regardless of whether control operators
are supported or not.
Continuations are relative to where the current expression being evaluated is. To clarify the currently executed
expression, we enclose the current expression with a bracket written as [ . . . ]. For example, consider a simple
arithmetic expression 3 + 5 ∗ 2 − 1. If we are about to execute 5 ∗ 2 of this expression, the current expression is
5 ∗ 2. To indicate it, we write 3 + [5 ∗ 2] − 1. At this moment, the continuation (or the current continuation)is 3 + [ · ] − 1, in other words, “given a value for [ · ] (called a hole), add three to it and subtract one from thesum.” A continuation is similar to a function in that it receives a value for a hole and evaluates the rest of thecomputation using the received value.
We can also understand the current continuation as the discarded computation when the current expression
is replaced with an aborting expression, such as raise Abort. In the above example, the current continuation of
3 + [5 ∗ 2] − 1 is 3 + [ · ] − 1, because it is the discarded computation when executing 3 + [raise Abort] − 1.
The current continuation changes as the computation proceeds. After the evaluation of 5 ∗ 2 ﬁnishes, theexpression becomes 3 + 10 − 1. Since the next expression to be evaluated is 3 + 10, the current expression becomes
3 + 10 written as [3 + 10] − 1. At this moment, the current continuation is [ · ] − 1, namely, “subtract one.” Afterthe evaluation of 3 + 10 ﬁnishes, the expression becomes 13 − 1. The only remaining expression to be evaluated is
13 − 1 written as [13 − 1]. The current continuation at this point is the empty context [ · ], namely, “do nothing.”
Exercise 1 In the following expressions, identify the next expression to be evaluated and its continuation bymarking the former with [ · ]. What is the type of the former? Given a value of this type, what is the type of thevalue returned by the continuation?
(1) 5 * (2 * 3 + 3 * 4)(2) (if 2 = 3 then "hello" else "hi") ^ " world"(3) fst (let x = 1 + 2 in (x, x))(4) string_length ("x" ^ string_of_int (3 + 1))

2.2

What are delimited continuations?

Delimited continuations are continuations whose extent is delimited. In the expression 3 + [5 ∗ 2] − 1, we implicitly
assumed that the rest of the current expression spans whole the expression, that is, 3 +[ ·]−1. Rather than taking2whole the rest of the computation, however, we sometimes want to capture only a part of it. Such continuations
are called delimited continuations.
The extent to which the current delimited continuation spans is designated by an explicit delimiter h· · ·i. For
example, in the expression h3 + [5 ∗ 2]i − 1, the current delimited continuation at [5 ∗ 2] is only h3 + [ · ]i anddoes not contain − 1.

2.3

Delimiting continuations: reset

In OchaCaml, continuations are delimited by the reset construct:
reset (fun () -> M )It receives a thunk (fun () -> M ) and executes its body M in a delimited context. If a continuation is captured
during the execution of M , it is delimited up to this reset. When M evaluates to a value, it becomes the valueof this whole reset expression.
For example, in the following expression:
reset (fun () -> 3 + [5 * 2]) - 1
the current delimited continuation at [5 * 2] becomes “add three” and does not contain “subtract one.” In
this example, however, because continuations are not captured, the execution goes without any surprise: 5 ∗ 2 isreduced to 10, 3 is added, 13 becomes the result of reset, and the ﬁnal result is 12.
The delimited continuation is the discarded computation when reset is replaced with try ... with Abort-> ... and the current expression with raise Abort. For example, the current delimited continuation ofreset (fun () -> 3 + [5 * 2]) - 1
is 3 + [ · ], because it is the discarded computation when executing(try 3 + [raise Abort] with Abort -> 0) - 1
Exercise 2 In the following expressions, identify the delimited continuation and its type.
(1) 5 * reset (fun () -> [2 * 3] + 3 * 4)(2) reset (fun () -> if [2 = 3] then "hello" else "hi") ^ " world"(3) fst (reset (fun () -> let x = [1 + 2] in (x, x)))(4) string_length (reset (fun () -> "x" ^ string_of_int [3 + 1]))

2.4

Capturing continuations: shift

To capture the current delimited continuation in OchaCaml, we use shift construct:
shift (fun k -> M )The execution of this expression proceeds in three steps:(1) The current delimited continuation is cleared.
(2) The cleared continuation is bound to k.
(3) The body M is executed.
We will see how to use shift in the subsequent sections in detail.

2.5

How to discard delimited continuations

The ﬁrst use of shift is to discard delimited continuations by:shift (fun _ -> M )Here, _ is a variable that does not occur anywhere else in the program. (The above program is the same as shift(fun k -> M ) where where k is not mentioned in M at all.) The execution of shift (fun _ -> M ) proceeds
as follows:(1) The current delimited continuation is cleared.
(2) The cleared continuation is passed to fun _ -> M as an argument, but it will never be used because it is
not mentioned in M .
(3) The body M is executed.
3

Since the body of shift does not mention the captured continuation, it is discarded and the current context up
to the enclosing reset is replaced with M . In other words, we can discard (or abort) the computation up to theenclosing reset.
For example, to discard the continuation of 3 + [5 ∗ 2] − 1, we enclose whole the expression with reset andreplace [ · ] with shift (fun _ -> M ).
# reset (fun () -> 3 + shift (fun _ -> 5 * 2) - 1) ;;- : int = 10#
In this case, M is 5 ∗ 2, so the result becomes 10. We can even return a value of diﬀerent type.
# reset (fun () -> 3 + shift (fun _ -> "hello") - 1) ;;- : string = "hello"#
Note that the discarded continuation 3 + [ · ] − 1 had type int -> int. Even though the current context delimited
by reset was going to return a value of type int, what is actually returned is a string. Still, the expression iswell-typed. We will come back to this type modiﬁcation later.
The discarded continuation is only up to the enclosing reset. In the following example, only “add three” isdiscarded:# reset (fun () -> 3 + shift (fun _ -> 5 * 2)) - 1 ;;- : int = 9#
In this case, we cannot return a string, because the value of reset is subtracted by one afterwards:# reset (fun () -> 3 + shift (fun _ -> "hello")) - 1 ;;Toplevel input:> reset (fun () -> 3 + shift (fun _ -> "hello")) - 1 ;;> ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
This expression has type string,but is used with type int.
#
Exercise 3 Discard the current continuations and return some values in the following expressions by replacing[ · ] with shift (fun _ -> M ) for some M .
(1) 5 * reset (fun () -> [·] + 3 * 4)(2) reset (fun () -> if [·] then "hello" else "hi") ^ " world"(3) fst (reset (fun () -> let x = [·] in (x, x)))(4) string_length (reset (fun () -> "x" ^ string_of_int [·]))
Exercise 4 Given a list of integers, the following function returns the product of all the elements.
(* times : int list -> int *)let rec times lst = match lst with[] -> 1| first :: rest -> first * times rest ;;For example, times [2; 3; 5] evaluates to 30. Suppose we apply times to [2; 3; 0; 5]. Because 0 exists inthe list, we know that the result becomes 0 without performing any multiplication. Such a behavior can be realized
by discarding the current continuation and returning 0 when 0 is found in the list. Modify the above deﬁnition oftimes to include the following clause| 0 :: rest -> ...
to implement this behavior. How can we invoke the modiﬁed times?

2.6

How to extract delimited continuations

The second use of shift is to extract delimited continuations by:shift (fun k -> k)
The execution of shift (fun k -> k) proceeds as follows:(1) The current delimited continuation is cleared.
4

(2) The cleared continuation is bound to k.
(3) The body k is executed.
Since the body of shift is just a variable representing the captured continuation, the last step ﬁnishes immediately
and returns the captured continuation. Since the current delimited continuation is cleared, the value returned by
the enclosing reset becomes the captured continuation. Thus, by executing shift (fun k -> k), we can extract
the current delimited continuation.
For example, if we want to capture the continuation of 3 + [5 ∗ 2] − 1, we enclose whole the expression withreset, replace [ · ] with shift (fun k -> k), and bind the result to a variable for later use.
# let f x = reset (fun () -> 3 + shift (fun k -> k) - 1) x ;;f : int -> int = <fun>#Because the returned continuation is a function, we η-expand it and bind it to a function f with an explicit
argument x above. We could have written:# let f = reset (fun () -> 3 + shift (fun k -> k) - 1) ;;f : int => int = <fun>#but then, because what is bound to f is not textually a value, we obtain a weakly polymorphic continuation thatcan be used only in a context with a speciﬁc answer type. In OchaCaml, such a special status of a function isindicated by a new arrow type =>. See Section 3.4 for details on =>. Here, we avoid it by η-expanding the deﬁnitionof f.
Now, f is bound to a function that, when applied, invokes the captured continuation “add three and subtractone” with the applied value.
# f 10 ;;- : int = 12#
In this case, f behaves the same as fun x -> reset (fun () -> 3 + x - 1).
Exercise 5 Extract delimited continuations of the following expressions by replacing [ · ] with shift (fun k ->k) and give names to them. Figure out what the extracted continuations do by actually applying them to values.
What are their types?
(1) reset (fun () -> 5 * ([·] + 3 * 4))(2) reset (fun () -> (if [·] then "hello" else "hi") ^ " world")(3) reset (fun () -> fst (let x = [·] in (x, x)))(4) reset (fun () -> string_length ("x" ^ string_of_int [·]))
Exercise 6 The following program traverses over a given list, and returns the list as is without any modiﬁcation.
In other words, it is an identity function over a list.
(* id : ’a list -> ’a list *)let rec id lst = match lst with[] -> []| first :: rest -> first :: id rest ;;Suppose we call this function with an argument list [1; 2; 3] as follows:
reset (fun () -> id [1; 2; 3]) ;;The function traverses over this list, and at last it reaches an empty list. What is the continuation at this moment?
Extract it by replacing [] with shift (fun k -> k). What is the type of the extracted continuation? What
does it do?

2.7

How to preserve delimited continuations

We can not only extract/discard continuations but also save them temporarily in a data structure, and resume
them later. For example, let us consider traversing over a tree deﬁned as follows:
type tree_t = Empty| Node of tree_t * int * tree_t ;;5

The following function traverses over a tree from left to right in a depth-ﬁrst manner and prints all the values
found in the tree.
(* walk : tree_t -> unit *)let rec walk tree = match tree with
Empty -> ()| Node (t1, n, t2) ->walk t1;
print_int n;walk t2 ;;For example, we have:# let tree1 = Node (Node (Empty, 1, Empty), 2, Node (Empty, 3, Empty)) ;;tree1 : tree_t = Node (Node (Empty, 1, Empty), 2, Node (Empty, 3, Empty))# walk tree1 ;;123- : unit = ()#The function walk traverses all the nodes in one go. But sometimes, we want to see each value one at a time andprocess it before receiving the next value (if any). To realize such a behavior, we replace print_int n with ashift expression as follows:(* walk : tree_t => unit *)let rec walk tree = match tree with
Empty -> ()| Node (t1, n, t2) ->walk t1;yield n;walk t2 ;;where yield is deﬁned as follows:(* yield : int => unit *)let yield n = shift (fun k -> Next (n, k)) ;;When a node is found, the function walk calls yield to abort and return the value n together with the current
continuation in a suitable constructor Next (to be deﬁned soon). The caller of walk will thus receive the ﬁrst
value n immediately, suspending traversal over other nodes. When the caller wants another value, it resumes
the traversal by passing a unit () to the continuation. This unit becomes the value of yield and the traversal
continues to walk t2. This way, by returning a value with the current continuation, one can stop and resume
execution of a function.
Now that walk captures continuations, we need to enclose it with reset to invoke it. However, we cannot
simply enclose walk with reset as follows:
reset (fun () -> walk tree1) ;;because it results in a type error. Remember that whenever walk ﬁnds a node, it returns Next (n, k) to theenclosing reset. On the other hand, if the list passed to walk is an empty list, walk returns a unit. Thus, if thecall to walk is directly enclosed by reset, the reset can return both Next (n, k) and a unit, leading to a typeerror.
To avoid the type error, we need another constructor Done (to be deﬁned soon) indicating that there are no
more nodes in a tree. Rather than ﬁnishing traversal with a unit, we return Done as in the following deﬁnition:(* start : tree_t -> ’a result_t *)let start tree =reset (fun () -> walk tree; Done) ;;Observe how the returned value in the body of shift in yield called from walk aﬀects the type of values returnedby the enclosing reset. This implies that typing a shift expression requires information on the type of theenclosing reset.
The remaining task is to deﬁne the two constructors, Next and Done. They are deﬁned as follows:
type ’a result_t = Done
| Next of int * (unit / ’a -> ’a result_t / ’a) ;;The constructor Done has no arguments, while Next has two arguments, one for an integer and the other for acontinuation. The type of a captured continuation is basically a function from unit to ’a result_t: given a unit,
it returns either Done or Next. In addition, however, one has to specify their answer types. Since answer types of6

captured continuations are polymorphic, we added a type parameter ’a and use it for both the answer types. We
will come back to answer types in detail in the subsequent sections.
We can now traverse over a tree by calling start. For example, the following function prints out all the integers
in the nodes of a tree:(* print_nodes : tree_t -> unit *)let print_nodes tree =let rec loop r = match r with
Done -> ()(* no more nodes *)| Next (n, k) ->print_int n;(* print n *)loop (k ()) in (* and continue *)loop (start tree) ;;At the last line, traversal over tree is initiated by calling start. The inner function loop examines the result: if
it is Done, there are no more nodes in tree; if the result is Next, it processes the current value n and continues(resumes) traversal by passing () to k. By calling print_nodes with tree1, We have:# print_nodes tree1 ;;123- : unit = ()#Likewise, the following function adds up all the integers in a tree:(* add_tree : tree_t -> int *)let add_tree tree =let rec loop r = match r with
Done -> 0| Next (n, k) -> n + loop (k ()) inloop (start tree) ;;We have:# add_tree tree1 ;;- : int = 6#
Using this idea, we can implement a kind of co-routines where two processes execute alternately. The following
exercise demonstrates it in the simplest form.
Exercise 7 Write a function same_fringe. Given two trees of type tree_t, it traverses over the two trees fromleft to right in a depth-ﬁrst manner, and checks if the encountered sequences of numbers are the same for the twotrees. For example, fringes of the following two trees are the same:
let tree1 = Node (Node (Empty, 1, Empty), 2, Node (Empty, 3, Empty)) ;;let tree2 = Node (Empty, 1, Node (Empty, 2, Node (Empty, 3, Empty))) ;;We can implement same_fringe by ﬁrst converting the trees into lists and comparing the resulting lists. However,this implementation requires to traverse all the trees even if the ﬁrst elements of the two trees are already diﬀerent.
Instead, write a function that can return false at the ﬁrst point where two numbers diﬀer without further
traversing the rest of the trees.

2.8

How to wrap delimited continuations: printf

Suspended computation captured in k can be resumed by applying k to a value. Rather than applying k immediately, if we wrap the application with fun, we can defer the resumption of captured computation. Furthermore, it
enables us to access an argument of the enclosing reset.
For example, consider the following expression:
shift (fun k -> fun () -> k "hello")
It captures the current continuation, binds it to k, aborts the current computation, and returns a thunk fun ()-> k "hello" as a result of the enclosing reset. Namely, it temporarily suspends the current computation andwaits for a unit to be passed outside the enclosing reset. When it receives a unit, it resumes computation withthe value "hello".
Suppose the above expression is placed in the context [...] ^ " world" as follows:1

1 The definition of f is η-expanded to make f answer-type polymorphic.

7

# let f x = reset (fun () ->shift (fun k -> fun () -> k "hello") ^ " world") x ;;f : unit -> string = <fun>#We then obtain a thunk f, which will resume the computation with the value "hello" when () is passed:# f () ;;- : string = "hello world"#
Observe that the thunk is placed (deep) under reset, while its argument () is passed outside of reset. By
wrapping continuations, we can access the information outside of the enclosing reset while staying within reset
lexically. By applying this idea, we can implement a (typed) printf function [1].
Exercise 8 By plugging "world" into the hole [...] of the following expression, we can obtain "hello world!".
reset (fun () -> "hello " ^ [...] ^ "!")
Instead of plugging "world" directly, can you ﬁll in the hole with an expression so that the argument to theenclosing reset is plugged into the hole? In other words, we want the following interaction, by replacing [...]
with a suitable expression:# reset (fun () -> "hello " ^ [...] ^ "!") "world" ;;- : string = "hello world!"#
The expression in [...] behaves like %s directive. Instead of a string, can you achieve the behavior of %d suchthat an integer argument is embedded into the string? (Use string_of_int to convert an integer to a string.)
Can you pass multiple arguments? (Be aware of the evaluation order of OchaCaml.)

2.9

Answer type modification

Now is a good time to consider how expressions with shift/reset are typed. In the following context,
reset (fun () -> [...] ^ " world")
the value returned by reset appears to be a string, because ^ returns a string. How can we pass an argument tothis expression without a type error?
To understand how the printf example is typed, we need to know what an answer type is. An answer typeis a type of the enclosing reset. For example, in the expression reset (fun () -> 3 + [5 * 2]) (where thecurrent expression is 5 * 2), the answer type is int, while in the expression reset (fun () -> string_of_int[5 * 2]), the answer type is string.
If an expression does not contain shift, it can be placed in a context of any answer type. In the above
example, the expression 5 * 2 can be placed both in reset (fun () -> 3 + [...]) and reset (fun () ->string_of_int [...]), because the type of the hole is int in both cases. In other words, the answer type ofcontinuations of 5 * 2 is arbitrary. This property is called answer type polymorphism.
When an expression contains shift, the story becomes diﬀerent. Because shift captures the current continuation and installs a new one (i.e., the body of shift), it can change the answer type. Back to the printf
example:reset (fun () -> [...] ^ " world")
the original answer type is string. Thus, the type of this context (to be captured below) is string -> string.
Suppose that in [...], we execute:shift (fun k -> fun () -> k "hello")
Since the type of the captured continuation k is string -> string, what is returned by shift to the enclosing
reset is a thunk fun () -> k "hello" of type unit -> string. In other words, the answer type of the enclosing
reset changed from string to unit -> string due to the execution of the shift expression. This phenomenon
is called answer type modification. This is how the above reset expression can accept () as an argument.
Because execution of shift expressions can change the answer type of the enclosing context, it is necessary tokeep track of the answer type all the time to properly type check expressions with shift and reset. This is how
programs in OchaCaml are type checked. See Section 3.4 for technical details.

2.10

How to wrap delimited continuations: state monad

By wrapping continuations, we can access information that resides outside the enclosing reset. Using this idea,
we can implement a mutable state by passing the current value of the state outside the enclosing reset.
8For example, let us consider having one integer as a state. Like "world" in the printf example, we pass aroundan integer as an argument of the context as follows:
reset (fun () -> M ) 3
In this example, the initial value of the state is 3. In the body M , we can access this state using the following
function:# let get () =shift (fun k -> fun state -> k state state) ;;get : unit => ’a = <fun>#After capturing the current continuation in k, the function get aborts it and returns a function fun state -> kstate state to the enclosing context. Thus, the current value of the state is passed to state. After that, thecomputation in k is resumed with state. Namely, the value of get () becomes the value of the current state.
In the above deﬁnition, k is passed state twice. The ﬁrst one becomes the value of get () while the second
one becomes the value of the new state after get () is executed. Continuations captured by shift include theoutermost enclosing reset. Thus, application of k to state constitutes a new context. To supply the value of thestate during the execution of k, we pass the value of the state after the execution of get. Since get is supposed
not to alter the value of the state, we pass state as a new value for the state. If we want to deﬁne a function thatalters the state, we pass the new value there. For example, the following function adds one to the current state(and returns a unit):# let tick () =shift (fun k -> fun state -> k () (state + 1)) ;;tick : unit => unit = <fun>#To start computation, we use the following function:# let run_state thunk =reset (fun () -> let result = thunk () infun state -> result) 0 ;;run_state : (unit => ’a) => ’b = <fun>#It executes thunk with 0 as the initial value for the state. When the execution of thunk ﬁnishes, the value of thestate is ignored and the result is returned. Using these functions, we have:# run_state (fun () ->tick ();(* state = 1 *)tick ();(* state = 2 *)let a = get () intick ();(* state = 3 *)get () - a) ;;- : int = 1#
Exercise 9 What would be the value of the following program?
run_state (fun () ->(tick (); get ()) - (tick (); get ())) ;;Check your result by actually executing it. (Be aware of the evaluation order of OchaCaml.)
Exercise 10 Similarly, write a function put. It updates the state with the argument of put and returns a unit.
The method presented in this section eﬀectively implements a state monad on top of a continuation monad.

2.11

How to reorder delimited continuations (advanced)

If we apply a continuation at the tail position, the captured computation is simply resumed. If we apply acontinuation at the non-tail position, we can perform additional computation after resumed computation ﬁnishes.
Put diﬀerently, we can switch the execution order of the surrounding context (captured continuation) and the
local (additional) computation. For example, in the following expression:# reset (fun () -> 1 + (shift (fun k -> 2 * k 3))) ;;- : int = 8#9the execution of 2 * [...] and the execution of the surrounding context 1 + [...] are swapped, and the latteris executed before the former. This simple idea generalizes to implementing A-normalization.
Consider the following deﬁnition of λ-terms:
type term_t = Var of string| Lam of string * term_t| App of term_t * term_t ;;Given a λ-term, we want to obtain its A-normal form, an equivalent term but all the applications in the term isgiven a unique name. For example, the A-normal form of the S combinator λx.λy.λz.(xz)(yz) is
λx.λy.λz.let t1 = xz in let t2 = yz in let t3 = t1 t2 in t3
To write an A-normalizer, we ﬁrst deﬁne an identity function that traverses all the subterms and reconstructthem:(* id_term : term_t -> term_t *)let rec id_term term = match term with
Var (x) -> Var (x)| Lam (x, t) -> Lam (x, id_term t)| App (t1, t2) -> App (id_term t1, id_term t2) ;;Because we want to assign a unique name to each application, we slightly change the above function to introduce
a let expression for each application as follows:(* id_term’ : term_t -> term_t *)let rec id_term’ term = match term with
Var (x) -> Var (x)| Lam (x, t) -> Lam (x, id_term’ t)| App (t1, t2) ->let t = gensym () in(* generate fresh variable *)App (Lam (t, Var (t)), (* let expression *)App (id_term’ t1, id_term’ t2)) ;;Here, we emulated let t = M in N by (λt.N )M . Using this new identity function, the S combinator is translated
to the following term:
λx.λy.λz.let t1 = (let t2 = xz in t2 )(let t3 = yz in t3 ) in t1
This is not quite what we want, however. What we want is a term where nested let expressions are ﬂattened.
Now, suppose we are traversing the syntax tree for the S combinator using id_term’, and are currently
looking at the ﬁrst application xz. At this point, the current continuation is “to traverse yz, to reconstruct anouter application, and to reconstruct three lambdas”:
λx.λy.λz.let t1 = [ · ](let t3 = yz in t3 ) in t1
To ﬂatten the nested let expressions, we now reorder the construction of the let expression for xz (i.e., let t2 =xz in [ · ]) and the rest of the reconstruction up to lambda (i.e., let t1 = [ · ](let t3 = yz in t3 ) in t1 ) as follows:(* a_normal : term_t => term_t *)let rec a_normal term = match term with
Var (x) -> Var (x)| Lam (x, t) -> Lam (x, reset (fun () -> a_normal t))| App (t1, t2) ->shift (fun k ->let t = gensym () in(* generate fresh variable *)App (Lam (t,(* let expression *)k (Var (t))), (* continue with new variable *)App (a_normal t1, a_normal t2))) ;;In the App case, after capturing the current continuation in k, it is resumed with a newly generated variable t.
Thus, the application in the original term is translated to this new variable. After translation of the whole term
is ﬁnished, the deﬁnition of t is added in front of it.
Because we do not want the deﬁnition of variables to extrude the scope of lambdas, the context is delimitedin the Lam case. With this deﬁnition, we achieve A-normalization. The presented method of residualizing let
expressions is called let insertion in the partial evaluation community.
Exercise 11 Transform the S combinator into A-normal form using the above function a_normal. What can weobserve?
10

2.12

How to duplicate delimited continuations

So far, we have used captured continuations only once. If we use them more than once, we can execute the rest of
the computation in various ways. It can be used to achieve backtracking.
Consider the following function:(* either : ’a -> ’a -> ’a *)let either a b =shift (fun k -> k a; k b) ;;The function either receives two arguments, a and b, captures the current continuation in k, and applies it toboth a and b in this order. Because k is applied twice, the rest of the computation that calls either is executed
twice. One can also understand either as returning two values. In fact, if we execute either in the following
context, we can actually see that the computation after either is actually executed twice.
# reset (fun () ->let x = either 0 1 inprint_int x;
print_newline ()) ;;0
1- : unit = ()#Since either executes its continuation twice, the value of x is printed twice, once for the ﬁrst argument of either
and the other for the second argument.
Exercise 12 Deﬁne a recursive function choice that receives a list of values and returns all the elements of thelist to the continuation one after the other.
Using either, we can write a simple generate-and-test style of functions easily. For example, suppose we have
two boolean variables, P and Q, and want to know if the following boolean formula is satisﬁable:(P ∨ Q) ∧ (P ∨ ¬Q) ∧ (¬P ∨ ¬Q)
Since P and Q take either true or false, we can write the following program:# reset (fun () ->let p = either true false in
let q = either true false inif (p || q) && (p || not q) && (not p || not q)
then (print_string (string_of_bool p);
print_string ", ";print_string (string_of_bool q);
print_newline ())) ;;true, false- : unit = ()#Notice that the program looks like a straightline program. It binds two variables p and q, checks whether theboolean formula is satisﬁed, and prints values of variables if it is. No loop, no backtracking. In the actual execution,
the operator either executes its rest of the computation twice. Because there are two occurrences of either, thetest is executed four times in total, each corresponding to the possible assignment of values to p and q. We canregard either as returning one of its arguments non-deterministically.
Exercise 13 Using choice, deﬁne a function that searches for three natural numbers between 1 and 5 that satisfy
the Pythagorean theorem. In other words, ﬁnd 1 ≤ x, y, z ≤ 5 such that x2 + y 2 = z 2 .

3Foundations of shift and reset

In this section, we show a brief overview of foundations of shift and reset. The language we consider is aleft-to-right2 call-by-value (CBV) λ-calculus extended with polymorphic let expressions and two control operators,
shift and reset.

2 Unlike OchaCaml.

11

3.1

Syntax(value) V(term) M(pure evaluation context) F(evaluation context) E

::=
::=
::=
::=

x | λx. M
V | M M | let x = M in M | Sk. M | hM i[ ] | F M | V F | let x = F in M
[ ] | E M | V E | let x = E in M | hEi

In this calculus, shift (fun k -> M ) is written as Sk. M and reset (fun () -> M ) as hM i. The evaluation
context is divided into two. The pure evaluation context is an evaluation context where the hole is not enclosed
by any reset.

3.2

Reduction rules(λx. M ) V
let x = V in M
hV i
hF [S V ]i

;
;
;
;

M [x := V ]M [x := V ]VhV (λx. hF [x]i)i x is fresh

The ﬁrst two rules are from the ordinary λ-calculus. The third rule says that reset around a value can be dropped.
The last rule shows how to capture the current continuation represented as a pure evaluation context F [ ]. It isreiﬁed as a function λx. hF [x]i and passed to V . Notice that the enclosing reset remains in the right-hand sideof the rule and that the reiﬁed function has an enclosing reset in it. (If one or both of these reset is removed,
we obtain other kinds of control operators.)

3.3

Evaluation rule

The evaluation rule is deﬁned as follows:
E[M ] → E[M 0 ] if M;

M0

The deﬁnition of an evaluation context speciﬁes that the evaluation order of this calculus is from left to right (i.e.,
the function part is evaluated before the argument part).
The evaluation rule can be divided into three steps:(1) If an expression to be evaluated is already a value, it is the result of evaluation. If it is not, it can be
decomposed into the form E[M ], where M is a redex.
(2) The redex M is reduced to M 0 according to the reduction rules.
(3) The result M 0 is plugged into the original evaluation context E[ ] to give the result E[M 0 ]. This is the resultof one-step reduction.

3.4

Typing Rules

Types and type schemes are deﬁned as follows, where t represents a type variable.
type τ
type scheme σ::= t | τ /τ → τ /τ::= τ | ∀t.σ

Here, the type τ1 /α → τ2 /β represents a type of a function from τ1 to τ2 , but during the execution of this function,
the answer type changes from α to β [3]. If a function does not have any control eﬀects (roughly speaking, thefunction does not use shift), the two answer types α and β become both the same type variable that does notappear anywhere else. Such a function is called pure. It is also called answer-type polymorphic. See the next
section for answer types.
In OchaCaml, types of pure functions are written as τ1 -> τ2 , omitting answer types. On the other hand,types of impure functions (that contain shift expressions) are written as τ1 => τ2 , indicating that the answer
types (also omitted) are not polymorphic. When one wants to see all the answer types, OchaCaml supports a
directive #answer "all";;. OchaCaml will then show types of impure functions as τ1 / α -> τ2 / β.
Typing judgements have one of the following forms:Γ `p M : τΓ, α ` M : τ, β12The former reads: under a type environment Γ, an expression M is pure and has type τ . The latter reads: undera type environment Γ, an expression M has type τ and execution of M changes the answer type from α to β. The
typing rules are given as follows:(x : σ) ∈ Γ σ  τΓ, x : τ1 , α ` M : τ2 , β
(fun)
(var)
Γ `p x : τΓ `p λx. M : τ1 /α → τ2 /βΓ `p M : τΓ, γ ` M1 : τ1 /α → τ2 /β, δ Γ, β ` M2 : τ1 , γ
(app)
(exp)
Γ, α ` M1 M2 : τ2 , δΓ, α ` M : τ, αΓ `p M1 : τ1 Γ, x : Gen(τ1 , Γ), α ` M2 : τ2 , β(let)Γ, α ` let x = M1 in M2 : τ2 , βΓ, k : ∀t.(τ /t → α/t), γ ` M : γ, β
Γ, γ ` M : γ, τ(reset)(shift)Γ, α ` Sk. M : τ, βΓ `p hM i : τAs usual, σ  τ represents that a type τ is an instance of a type scheme σ, and Gen(τ, Γ) represents a type scheme
obtained by generalizing the type variables in τ that does not occur free in Γ.

3.5

Answer Types

An answer type is a type of the current context. For example, in the following expression:
reset (fun () -> 3 + [5 * 2] - 1)
the type of the current expression [5 * 2] is int and the type of a value returned by its surrounding context 3+ [5 * 2] - 1 is int (both before and after the execution of 5 * 2). Thus, the answer type of [5 * 2] is int.
We represent this typing as the following judgement:
Γ, int ` 5 * 2 : int, int
The ﬁrst int is the answer type before the execution of 5 * 2; the second int is the type of 5 * 2; and the third
int is the answer type after the execution of 5 * 2.
The type of an expression and its answer type are not always the same. For example, in the expression:
reset (fun -> if [2 = 3] then 1 + 2 else 3 - 1)
the current expression 2 = 3 has type bool, but the answer type is int. Thus, the typing judgement becomes asfollows:
Γ, int ` 2 = 3 : bool, int
The two answer types are always the same if the current expression is pure. Because answer types do not aﬀect
the type of pure expressions, we can forget about answer types when we are dealing with only pure expressions.
Next, let us consider examples where the answer type changes.
reset (fun () ->[shift (fun k -> fun () -> k "hello")] ^ " world")
It is not immediately clear what the type of the current expression [...] is, but it is string, because the resultof the current expression is passed to ^ which requires two string arguments. What is the answer type? Before theexecution of [...], the answer type of the current context is string because it is the result of ^ which returns astring value. After the execution of [...], however, the current continuation is captured in k and what is actually
returned by the enclosing reset is a function fun () -> k "hello". Since this function receives a unit () andreturns a string "hello world", it has roughly type unit -> string. To be more precise, because the type of
this function must also mention answer types and because the function turns out to be pure, it has type unit /’a -> string / ’a. Thus, the typing judgement becomes as follows:Γ, string ` shift (fun k -> ...) : string, unit / ’a -> string / ’aThus, the use of shift can change the answer types in various ways. This phenomenon is called answer typemodification.
We can understand a type of functions in a similar way. For example, consider get introduced in Section 2.8.
Since this function receives () and returns an integer (the current value of the state), it has type unit -> int,
if we ignore answer types. To see what the answer types are, we consider the context in which get is used. For
example, in the following expression:13

reset (fun () ->let result = [get ()] + 2 * get () infun state -> result)since the context returns a function fun state -> result as a result, the answer type is (roughly) int -> int.
Thus, the type of get becomes something like unit / (int -> int) -> int / (int -> int). To be more
precise, because the type of state is not constrained to int from the deﬁnition of get and the type of context canbe more general, the exact type of get is:unit / (’a / ’b -> ’c / ’d) -> ’a / (’a / ’b -> ’c / ’d)The introduction of shift/reset forces us to think about answer types. It amounts to consider what the typeof context is and how it changes during execution.

References[1] Asai, K. “On Typing Delimited Continuations: Three New Solutions to the Printf Problem,” Higher-Orderand Symbolic Computation, Vol. 22, No. 3, pp. 275–291, Kluwer Academic Publishers (September 2009).
[2] Asai, K., and Y. Kameyama “Polymorphic Delimited Continuations,” Proceedings of the Fifth Asian Symposium on Programming Languages and Systems (APLAS’07), LNCS 4807, pp. 239–254 (November 2007).
[3] Danvy, O., and A. Filinski “A Functional Abstraction of Typed Contexts,” Technical Report 89/12, DIKU,
University of Copenhagen (July 1989).
[4] Danvy, O., and A. Filinski “Abstracting Control,” Proceedings of the 1990 ACM Conference on Lisp andFunctional Programming, pp. 151–160 (June 1990).
[5] Filinski, A. “Representing Monads,” Conference Record of the 21st Annual ACM Symposium on Principles
of Programming Languages, pp. 446–457 (January 1994).
[6] Felleisen, M. “The Theory and Practice of First-Class Prompts,” Conference Record of the 15th Annual ACM
Symposium on Principles of Programming Languages, pp. 180–190 (January 1988).
[7] Gasbichler, M., and M. Sperber “Final Shift for Call/cc: Direct Implementation of Shift and Reset,” Proceedings of the ACM SIGPLAN International Conference on Functional Programming (ICFP’02), pp. 271–282(October 2002).
[8] Gunter, C. A., D. Rémy, and J. G. Riecke “A Generalization of Exceptions and Control in ML-Like Languages,” Proceedings of the Seventh International Conference on Functional Programming Languages andComputer Architecture (FPCA’95), pp. 12–23 (June 1995).
[9] Kameyama, Y., and M. Hasegawa “A Sound and Complete Axiomatization of Delimited Continuations,”
Proceedings of the eighth ACM SIGPLAN International Conference on Functional Programming (ICFP’03),
pp. 177–188 (August 2003).
[10] Kiselyov, O. “Delimited Control in OCaml, Abstractly and Concretely: System Description,” In M. Blume,
N. Kobayashi, and G. Vidal, editors, Functional and Logic Programming (LNCS 6009), pp. 304–320 (April2010).
[11] Masuko, M., and K. Asai “Direct Implementation of Shift and Reset in the MinCaml Compiler,” Proceedingsof the 2009 ACM SIGPLAN Workshop on ML, pp. 49–60 (September 2009).
[12] Masuko, M., and K. Asai “Caml Light + shift/reset = Caml Shift,” Theory and Practice of Delimited Continuations (TPDC 2011), pp. 33–46 (May 2011).
[13] Plotkin, G. D. “Call-by-name, call-by-value, and the λ-calculus,” Theoretical Computer Science, Vol. 1, No. 2,
pp. 125–159 (December 1975).

14