1

Capturing the Future by Replaying the Past
Functional Pearl

arXiv:1710.10385v1 [] 28 Oct 2017

JAMES KOPPEL, MIT
ARMANDO SOLAR-LEZAMA, MIT
Delimited continuations are the mother of all monads! So goes the slogan inspired by Filinski’s 1994 paper, which showed
that delimited continuations can implement any monadic effect, letting the programmer use an effect as easily as if it was
built into the language. It’s a shame that not many languages have delimited continuations.
Luckily, exceptions and state are also the mother of all monads! In this Pearl, we show how to implement delimited
continuations in terms of exceptions and state, a construction we call thermometer continuations. While traditional implementations of delimited continuations require some way of "capturing" an intermediate state of the computation, the insight of
thermometer continuations is to reach this intermediate state by replaying the entire computation from the start, guiding it
using a "replay stack" it so that the same thing happens until the captured point.
Along the way, we explain delimited continuations and monadic reflection, show how the Filinski construction lets
thermometer continuations express any monadic effect, share an elegant special-case for nondeterminism, and discuss why
our construction is not prevented by theoretical results that exceptions and state cannot macro-express continuations.
CCS Concepts: •Theory of computation → Control primitives; Functional constructs; •Software and its engineering → Functional languages; Control structures; General programming languages;
Additional Key Words and Phrases: monads, delimited continuations
ACM Reference format:
James Koppel and Armando Solar-Lezama. 2016. Capturing the Future by Replaying the Past. 1, 1, Article 1 (January 2016),
27 pages.
DOI: 10.1145/nnnnnnn.nnnnnnn

1

INTRODUCTION

In the days when mainstream languages have been adopting higher-order functions, advanced monadic effects
like continuations and nondeterminism have held out as the province of the bourgeois programmer of obscure
languages. Until now, that is.
Of course, there’s a difference between effects which are built into a language and those that must be encoded.
Mutable state is built-in to C, and so one can write int x = 1; x += 1; int y = x + 1;. Curry 1 is nondeterministic,
and so one can write (3 ? 4) * (5 ? 6) , which evaluates to all of {15, 18, 20, 24}. This is called the direct style.
When an effect is not built into a language, the monadic, or indirect, style is needed. In the orthodox indirect
style, after every use of an effect, the remainder of the program is wrapped in a lambda. For instance, the nondeterminism example would be rendered in Scala as List(3,4).flatMap(x ⇒List(5,6).flatMap(y ⇒List(x * y))).
Effects implemented in this way are called monadic. "Do-notation," as seen in Haskell, makes this easier, but still
inconvenient.
1 Hanus

et al. (1995)

Permission to make digital or hard copies of part or all of this work for personal or classroom use is granted without fee provided that
copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page.
Copyrights for third-party components of this work must be honored. For all other uses, contact the owner/author(s).
© 2016 Copyright held by the owner/author(s). XXXX-XXXX/2016/1-ART1 $15.00
DOI: 10.1145/nnnnnnn.nnnnnnn

, Vol. 1, No. 1, Article 1. Publication date: January 2016.

We show that, in any language with exceptions and state, you can implement any monadic effect in direct
style. With our construction, you could implement a ? operator in Scala such that the example (3 ? 4) * (5 ? 6)
will run and return List(15,18,20,24). Filinski showed how to do this in any language that has an effect called
delimited continuations or delimited control 2 . We first show how to implement delimited continuations in
terms of exceptions and state, a construction we call thermometer continuations. Filinski’s result does the rest.
Continuations are rare, but exceptions are common. With thermometer continuations, you can get any effect in
direct style in 9 of the TIOBE top 10 languages 3 .
Here’s what delimited continuations look like in cooking: Imagine a recipe for making chocolate nut bars. Soak
the almonds in cold water. Rinse, and grind them with a mortar and pestle. Delimited continuations are like a step
that references a sub-recipe. Repeat the last two steps, but this time with pistachios. Delimited continuations can
perform arbitrary logic with these subprograms ("Do the next three steps once for each pan you’ll be using"), and
they can abort the present computation ("If using store-bought chocolate, ignore the previous four steps"). They
are "delimited" in that they capture only a part of the program, unlike traditional continuations, where you could
not capture the next three steps as a procedure without also capturing everything after them, including the part
where you serve the treats to friends and then watch Game of Thrones. Implementing delimited continuations
requires capturing the current state of the program, along with the rest of the computation up to a "delimited"
point. It’s like being able to rip out sections of the recipe and copy them, along with clones of whatever ingredients
have been prepared prior to that section. This is a form of "time travel" that typically requires runtime support —
if the nuts had not yet been crushed at step N, and you captured a continuation at step N, when it’s invoked, the
nuts will suddenly be uncrushed again.
The insight of thermometer continuations is that every subcomputation is contained within the entire computation, and so there is an alternative to time travel: just repeat the entire recipe from the start! But this time, use
the large pan for step 7. Because the computation contains delimited control (which can simulate any effect), it’s
not guaranteed to do the same thing when replayed. Thermometer continuations hence need state for a replay
stack, which makes each replayed effectful function call do the same thing as a previous invocation. Additionally,
like a recipe step that overrides previous steps, or that asks you to let it bake for an hour, delimited continuations
can abort or suspend the rest of the computation. Implementing this uses exceptions.
This approach poses an obvious limitation: the replayed computation can’t have any side effects, except for
thermometer continuations. And replays are inefficient. Luckily, thermometer continuations can implement all
other effects, and there are optimization techniques that make it less inefficient. Also, memoization — a "benign
effect" — is an exception to the no-side-effects rule, and makes replays cheaper.
Here’s what’s in the rest of this Pearl: Our construction has an elegant special case for nondeterminism,
presented in Section 2, which also serves as a warm-up to full delimited control. In the following section, we
give an intuition for how to generalize the nondeterminism construction with continuations. Section 4 explains
thermometer continuations. Section 5 explains Filinski’s construction and how it combines with thermometer
continuations to get arbitrary monadic effects. Section 6 discusses how to optimize the fusion of thermometer
continuations with Filinski’s construction, and provides a few benchmarks showing that thermometer continuations are not entirely impractical. Finally, Section 7 discusses why our construction does not contradict a
theoretical result that exceptions and state cannot simulate continuations.

2 Filinski
3 TIOBE

(1994)
Software BV (2017)

2

SML code

Closest Haskell equivalent

int option
type

α

f =

α

*

Maybe Int

α

type F a = (a, a)

!r
val x
let

:

readIORef r

int = 1

<decls> in <expr> end
1 :: 2 :: []

x

let

<decl1> in

let

:: Int; x = 1
<decl2> in <expr>
1 : 2 : []

f [1,2] @ g [3,4]

f [1,2] ++ g [3,4]

"abc" ^ "def"

"abc" ++ "def"

f o g

f . g

#1 (a,b)

fst (a,b)

Fig. 1. The SML/Haskell Cheat Sheet

2

WARM-UP: REPLAY-BASED NONDETERMINISM

Nondeterminism is perhaps the first effect students learn which is not readily available in a traditional imperative language. This section presents replay-based nondeterminism, a useful specialization of thermometer
continuations, and an introduction to its underlying ideas.
When writing the examples in this paper, we sought an impure language with built-in support for exceptions
and state, and which has a simple syntax with good support for closures. We hence chose to present in SML.
The cheat sheet in Figure 1 explains SML’s less obvious syntax by giving their closest Haskell equivalents. Also
note that ML functors are module-valued functions, and are substantially different from Haskell-style functors.
Throughout this paper, we will assume there is no concurrency.
Nondeterminism provides a choice operator choose such that choose [x1, x2, . . .] may return any of the x i . Its
counterpart is a withNondeterminism operator which executes a block that uses choose, and returns the list of values
resulting from all executions of the block.
withNondeterminism (fn ()

⇒

(choose [2,3,4]) * (choose [5,6]))
(* val it = [10,12,15,18,20,24]

:

int list *)

In this example, there are six resulting possible values, yet the body returns one value. It hence must run six
times. The replay-based implementation of nondeterminism does exactly this: in the first run, the two calls to
choose return 2 and 5, then 2 and 6 in the second, etc. In doing so, the program behaves as if the first call to choose
was run once but returned thrice. We’ll soon show exactly how this is done. But first, let us connect our approach
to the one most familiar to Haskell programmers: achieving nondeterminism through monads.
In SML, a monad is any module which implements the following signature (and satisfies the monad laws):
signature MONAD = sig
type

α

m;

val return
val bind

:

: α → α m;
α m → (α → β

m)

→β

m;

end;

Here is the implementation of the list monad in SML:
3

structure ListMonad
type

α

m =

α

:

MONAD = struct

list

fun return x = [x]
fun bind []

|

f = []

bind (x :: xs) f = f x @ bind xs f

end;

The ListMonad lets us rewrite the above example in monadic style. In the direct style, choose [2,3,4] would
return thrice, causing the rest of the code to run thrice. Comparatively, in the monadic style, the rest of the
computation is passed as a function argument to ListMonad.bind, which invokes it thrice.
open ListMonad;
bind [2,3,4] (fn x
bind [5,6]

(fn y

⇒
⇒

return (x * y)))
(* val it = [10,12,15,18,20,24]

:

int list *)

Let’s look at how the monadic version is constructed from the direct one. From the perspective of the invocation
the rest of the expression is a function awaiting its result, which it must invoke thrice:

choose [2, 3, 4],

C = (fn

 ⇒ 

* choose [5, 6])

This remaining computation is the continuation of choose [2,3,4]. Each time choose [2,3,4] returns, it invokes
this continuation. The monadic transformation captured this continuation, explicitly turning it into a function.
This transformation captures the continuation at compile time, but it can also be captured at runtime with the
callcc "call with current continuation" operator: if this first call to choose were replaced with callcc (fn k ⇒. . .),
then k would be equivalent to C. So, the functions being passed to bind are exactly what would be obtained if the
program were instead written in direct style and used callcc.
This insight makes it possible to implement a direct-style choose operator. The big idea is that, once callcc
has captured that continuation C in k, it must invoke k thrice, with values 2, 3, 4. This implementation is a little
verbose in terms of callcc, but we’ll later see how delimited continuations make this example simpler than with
callcc-style continuations.
Like the monadic and callcc-based implementations of nondeterminism, replay-based nondeterminism invokes
the continuation (fn x ⇒x * choose [5,6]) three times. Since the program is left in direct style (choose [2,3,4] * choose
and it cannot rely on a built-in language mechanism to capture the continuation, it does this by running the entire
block multiple times, with some bookkeeping to coordinate the runs. We begin our explanation of replay-based
nondeterminism with the simplest case: a variant of choose which takes only two arguments, and may only be
used once.

2.1

The Simple Case: Two-choice nondeterminism, used once

We begin by developing the simplified choose2 operator. Calling choose2
branches, returning x in the first branch and y in the second. For example:
(withNondeterminism2 (fn ()

=⇒
=⇒

⇒

3 * choose2 (5, 6)))

[3 * 5, 3 * 6]
[15, 18]

4

(x,y)

splits the execution into two

[5,6]) ,

br_idx
0

1

br_idx

1
1

pos=2

21 0

1 0

0

1

21 0

1 0

br_idx

1
0

1

0

0
pos=0

1 0

21 0

pos=0

(a)

(b)

(c)

Fig. 2. Several points in the execution of the replay-based nondeterminism algorithm.

This execution trace hints at an implementation in which withNondetermism2 calls the block twice, and where
returns the first value in the first run, and the second value in the second run. withNondeterminism2 uses a
single bit of state to communicate to choose2 whether it is being called in the first or second execution. As long as
the block passed to withNondeterminism2 is pure, with no effects other than the single use of choose (and hence no
nested calls to withNondeterminism2), each execution will have the same state at the time choose is called.
choose2

val firstTime = ref false
(* choose2

: α

*

α → α

*)

fun choose2 (x1,x2) = if !firstTime then x1 else x2
(* withNondeterminism2

→ α ) → α list *)
: = true ; f
(firstTime : = false; f

(unit

:

fun withNondeterminism2 f = [(firstTime

withNondeterminism2 (fn ()
(* val it = [15,18]

:

⇒

()),
())]

3 * choose2 (5,6))

int list *)

While simple and restrictive, this implementation contains the insights that allow arbitrary nondeterminism. View a nondeterministic computation as a tree, where each call to choose is a node, and the sequence of
values returned by calls to choose identify a branch. This section gives the special case where the tree has but
two branches. Here, withNondeterminism2 picks the branch, and choose2 follows it. Because there are only two
branches of execution, withNondeterminism2 and choose2 share only a single bit of state. What’s needed for arbitrary
nondeterminism? More state.

2.2

Towards Arbitrary Nondeterminism

Replay-based nondeterminism executes every branch in the computation tree, replaying the program once for
each. It’s like a depth-first tree traversal, except that reaching each leaf requires traversing the entire path from
the root. For instance, consider this program:
withNondeterminism (fn ()
if choose [3,4]

=

⇒

3 then

choose [5,6]
else
choose [7,8,9])

5

There are five branches in the execution tree of this program. In the first run, the two calls to choose return
(3, 5). In the second, they return (3, 6), followed by (4, 7), (4, 8) and (4, 9). Each branch is identified by a branch
index. Figure 2 depicts this execution tree with branch indices used at different points in the algorithm. The gist
of our algorithm is: withNondeterminism will run the block once for every branch index; within a run, each call to
choose uses the current branch index to pick which alternative to return.
Or, in code: br_idx stores the current branch index, while pos tells the next call to choose which element of the
branch index to look at.
val br_idx

int list ref = ref [];

:

val pos = ref 0;

A branch index is a list of numbers, each number indicating which alternative to return at a call to choose.
These choices are numbered right-to-left, so that, when this number reaches 0, the algorithm knows that all
choices at that call to choose have been exhausted. Like the stacks used to traverse trees, the first element of a
branch index corresponds to the last call to choose in that branch, which makes updating to the next branch index
simple. For instance, the first branch, in which the calls to choose return 3 and 5, has branch index [1, 1], and the
next branch, returning 3 and 6, has branch index [0, 1]. These are shown in Figures 2a and 2b. The decr inputs a
branch index, and returns the index of the next branch.
fun decr (0 :: ns) = decr ns

|
|

decr (n :: ns) = (n-1) :: ns
decr []

= []

After executing the branch with index [0, 1], withNondeterminism updates the current branch index to [0]. This
is merely a prefix of the actual branch index: it instructs the first call to choose to return 4, but withNondeterminism
does not yet know that doing so causes execution to encounter the call choose [7,8,9]. Instead, that call to choose
will extend the branch index to [2, 0]. Figure 2c depicts this.
Do note that nested calls to withNondeterminism will not work because they both use global state and will
interfere with each other. The thermometer continuations in Section 4.4 lack this problem.
We can now implement choose. If the branch index records a choice for the current invocation of choose, it
selects that alternative. Else, it extends the branch index to pick the first alternative of the current choice.
open List;
(* choose

: α

list

→ α

*)

fun choose xs = if not (0 = !pos) then
let val idxFromEnd = nth (!br_idx, !pos - 1) in
(pos

:=

(!pos) - 1;

nth (xs, (length xs - 1) - idxFromEnd))
end
else
(br_idx

:=

(length xs - 1)

::

!br_idx;

hd xs)

The withNondeterminism function repeatedly executes the given block. It picks a different branch each time until
the branches have been exhausted, and concatenates the results together. Note that no initialization code is
needed, because the state is always returned to its initial value upon completing a call of withNondeterminism.
6

(* withNondeterminism

(unit

:

→ α) → α

list *)

fun withNondeterminism f =
let val v = [f()] in
br_idx : = decr (!br_idx);
length (!br_idx);
_
case !br idx of

pos

|

:=

[]
_

⇒
⇒

v
v @ withNondeterminism f

end

With this implementation in place, we can now finally run the examples.

withNondeterminism (fn ()

⇒

choose [2,3,4] * choose [5, 6])

(* val it = [10,12,15,18,20,24]

withNondeterminism (fn ()
if choose [3,4]

=

:

int list *)

⇒

3 then

choose [5,6]
else
choose [7,8,9])
(* val it = [5,6,7,8,9]

2.3

:

int list *)

But What About the Empty Case?

The above implementation can handle nondeterminism with 1 or more alternatives. But having 0 alternatives is
fundamentally different: the previous implementation assumes one value per branch, but choose allows branches
with no values.
What to do when a program calls choose []? Returning a dummy value is not an option: choose has type
α list →α , and there is no value of type α to return. We look to the monadic version as a guide. A call to
choose [] is translated into:

bind [] (fn x

⇒ . . .)

Here, the function argument of bind represents the continuation of choose. bind never invokes it, which is
equivalent to aborting the continuation: it’s like choose never returns. The replay-based implementation of
choose [] achieves this by raising an exception.
Supporting empty choices requires minimal modification to our implementation. When a program calls
choose [], choose raises an exception to pass control to withNondeterminism, which moves on to the next branch.
7

exception Empty;
fun choose [] = raise Empty

|

choose xs =

...

fun withNondeterminism f =
let val v = [f()] handle Empty

⇒

[] in

...
end
fun fail () = choose []
withNondeterminism (fn ()

⇒

let val x = chooose [2,3,4] * choose [5,7] in
if x

≥

20 then x

else fail () end);
(* val it = [21,20,28]

3

:

int list *)

CONTINUATIONS IN DISGUISE

The previous section showed a trick for implementing direct-style nondeterminism in deterministic languages.
Now, we delve to the deeper idea behind it, and surface the ability to generalize from nondeterminism to
any monadic effect. We now examine how replay-based nondeterminism stealthily manipulates continuations.
Consider evaluating this expression:
val e = withNondeterminism (fn ()

⇒

choose [2,3,4] * choose [5, 6])

Every subexpression of e has a continuation, and when it returns a value, it invokes that continuation. After
the algorithm takes e down the first branch and reaches the point T = 2 * choose [5, 6], this second call to choose
has continuation C = fn ⇒2 * .
choose must invoke this continuation twice, with two different values. But C is not actually a function that can
be repeatedly invoked: it’s a description of what the program does with a value after it’s returned, and returning
a value causes the program to keep executing, consuming the continuation. choose invokes this continuation
the first time normally, returning 5. To copy this ephemeral continuation, it re-runs the computation until it’s
reached a point identical to T, evaluating that same call to choose with a second copy of C as its continuation —
and this time, it invokes the continuation with 6.
So, the first action of the choose operator is capturing the continuation. And what happens next? The
continuation is invoked once for each value, and the results are later appended together. We’ve already seen
another operation that invokes a function once on each value of a list and appends the results: the ListMonad.bind
operator. Figure 3 depicts how applying ListMonad.bind to the continuation produces direct-style nondeterminism.
So, replay-based nondeterminism is actually a fusion of two separate ideas:
(1) Capturing the continuation using replay
(2) Using the captured continuation with operators from the nondeterminism monad
In Section 4, we extract the first half to create thermometer continuations, our replay-based implementation of
delimited control. The second half — using continuations and monads to implement any effect in direct style
— is Filinski’s construction, which we explain in Section 5. These produce something more inefficient than the
8

Fig. 3. To implement
multiple times.

=

[

1
C

, , ]
2
C

3
C

[1,2,3]

>>=

choose:

first capture the continuation, and then use the list monad’s

C

bind

operator to evaluate it

replay-based nondeterminsm of Section 2, but we’ll show in Section 6 how to fuse them together into something
equivalent.

4

THERMOMETER CONTINUATIONS: REPLAY-BASED DELIMITED CONTROL

In the previous section, we explained how the replay-based nondeterminism algorithm actually hides a mechanism
for capturing continuations. Over the the remainder of this section, we extract out that mechanism, developing
the more general idea of thermometer continuations. But first, let us explain the variant of continuations that our
mechanism uses: delimited continuations.

4.1

What is delimited control?

When we speak of "the rest of the computation," a natural question is "until where?" For traditional continuations,
the answer is: until the program halts. This crosses all abstraction boundaries, making these "undelimited
continuations" difficult to work with. Delimited continuations on the other hand, introduced by Felleisen 4 ,
only represent a prefix of the remaining computation. Just as callcc makes continuations first class, allowing a
program to modify its continuation to implement many different global control-flow operators, the shift and
reset constructs make delimited continuations first-class, and can be used to implement many local control-flow
operators.
In the remainder of this section, we’ll denote a one-holed context C with the notation C[x], i.e.: C[x+1] is some
expression containing x+1. This notation makes it easy to give the semantics for shift and reset.
Consider an expression which is about to evaluate a shift. In the special case where there is only one shift in
the code, it evaluates as follows:
C 1 [reset (fn () ⇒C 2 [shift (fn k ⇒E)])]
=⇒C 1 [(fn k ⇒E)(fn x ⇒C 2 [x])]
C 1 [reset (fn () ⇒E)] =⇒E if E does not contain

a shift

Figure 4 depicts this evaluation. The name "shift" is illustrative. Suppose shift and reset were normal functions
rather than control operators. Then the delimited continuation of the shift up until the reset is C 2 , which in
turn has a delimited continuation of C 3 [x] = x. What shift does is, well, shift these. Continuation C 3 replaces
Continuation C 2 . This means that, after the shift returns, control jumps straight to the reset. In that regard, it
acts like a C-style return operator. C 2 , however, gets turned into a function and saved in the variable k.
E is free to use k in interesting ways. It can invoke k with several values. This essentially makes the shift
"return" multiple times, and can implement nondeterminism a la Figure 3. It can stuff k in a data-structure to be
"resumed" later, similar to a Python-style yield. It can even "chain" calls to k, like in this example:
1 + reset (fn ()
4 Felleisen

⇒

2 * (shift (fn k

⇒

k (k 5))))

(1988)

9

shift (λk.E)

k = λx

E

C
reset boundary

x
C

reset boundary

Fig. 4. Graphical depiction of the action of the shift operator.

Let’s rewrite this with C 1 [x]=
now evaluate it:

1+x

and C 2 [x]

= 2 * x

so that it matches the semantics we gave earlier. We can

⇒ 2 * (shift (fn k ⇒ k (k 5))))
C 1 [reset (fn () ⇒C 2 [shift (fn k ⇒k (k 5))])]
=⇒C 1 [(fn k ⇒k (k 5))(fn x ⇒C 2 [x])]
=⇒ 1 + (fn k ⇒ k (k 5))(fn x ⇒ 2 * x) end
=⇒ 21
1 + reset (fn ()

=

The definition above only works when there is only one shift. We now give the full semantics, which can
handle code with multiple shift’s. In the case where there is only one shift, this is equivalent to the previous
semantics.
C 1 [reset (fn () ⇒C 2 [shift (fn k ⇒E)])]
=⇒C 1 [reset (fn () ⇒(fn k ⇒E)(fn x ⇒ reset (fn
C 1 [reset (fn () ⇒E)] =⇒E if E does not contain a

()

⇒ C 2 [x])))]

shift

When the captured delimited continuation is invoked, it gets delimited by the inner reset. So, any shift in C_2
will return to the body of the first shift E, instead of discarding the computation in E. Meanwhile, if E contains a
shift, the inner shift will only capture the continuation up to the outer reset rather than the entire remainder of
the program, because the outer reset gets left in place.
Here’s an example of multiple shift’s in a row.
reset (fn ()

⇒

shift (fn k

⇒

=⇒ reset (fn
=⇒ 1 + reset
=⇒ 1 + reset
=⇒ 1 + 1 + 2
=⇒ 8

()

⇒

1 + k 2) (fn x

(fn k

(fn ()
(fn ()

⇒
⇒

⇒

1 + k 2) * shift (fn k’

2 * shift (fn k’
(fn k’

⇒

⇒

⇒

⇒

1 + k’ 3))

reset (fn ()

⇒

x * shift (fn k’

⇒

1 + k’ 3))))

1 + k’ 3))

1 + k’ 3)(fn x

⇒

reset (fn ()

⇒

2 * x)))

* 3

The outer reset gets left in place. This means that if there are nested shift’s (i.e.: a shift in E),
And here’s an example of nested shift’s. Note how the two delimited continuations fn x ⇒2 + x and fn
get applied in reverse-order.
1 + reset (fn ()

=⇒
=⇒
=⇒
=⇒

⇒

2 + (shift (fn k

1 + reset (fn ()
1 + reset (fn ()
1 + reset (fn ()

⇒
⇒
⇒

(fn k

⇒

⇒

3 * shift (fn l
(fn l

⇒

3 * shift (fn l

3 * shift (fn l

⇒

⇒

⇒

3 * x))

37

10

⇒3

l (k 10)))))

l (k 10)))(fn x

l (2 + 10)))

l 12)(fn x

⇒

x

⇒

reset (fn ()

⇒

2 + x)))

* x

As the previous examples show, shift and reset are quite versatile. Indeed, they can implement any other
control operator.
shift and reset are termed delimited control operators, and are encoded in the following SML signature. There
are also other equivalent formulations of delimited control using different operators5 .
signature CONTROL = sig
type ans
val reset
val shift

:
:

→ ans) → ans
→ ans) → ans) → α

(unit
(( α

end;

4.2

Baby Thermometer Continuations

Programming with continuations requires being able to capture and copy an intermediate state of the program. We
showed in Section 3 that replay-based nondeterminism implicitly does this by replaying the whole computation,
and hence needs no support from the runtime. We now see how to do this more explicitly.
This section presents a simplified pseudocode version of thermometer continuations. This version assumes the
reset block only contains one shift, and also ignores type-safety, but can still handle the example of delimited control from Section 4.1. Consider an expression containing a single shift, C 1 [reset (fn () ⇒C 2 [shift (fn k ⇒E)])]
The tough part of delimited continuations is to capture the continuation of the shift, namely C[t] = 2 * t, as
a function fn t ⇒C[t]. But suppose shift used mutable state so that change_state x; shift f evaluates to x. If C
doesn’t use any mutable state, then change_state x commutes with everything in C, so that change_state x;C [shift f]
is equivalent to C [change_state x; shift f]. Then, since block () is equal to C [shift (fn k ⇒E)], the function
fn x ⇒(change_state x; block () ) is equivalent to fn x ⇒C [x], the continuation to capture!
The other part of shift is to return a value directly to the enclosing reset (to "abort the current continuation").
It can do this by raising an exception. So, in totality, here are the semantics of shift and reset implemented in
this fashion:
C 1 [reset (fn () ⇒C 2 [shift (fn k ⇒E)])]
=⇒C 1 [C 2 [raise (Done (fn k ⇒E)(fn x ⇒(change_state x; C 2 [shift
handle (Done x ⇒ x)]
≡ C 1 [(fn k ⇒E)(fn x ⇒C 2 [change_state x; shift (fn k ⇒E)])]
≡ C 1 [(fn k ⇒E)(fn x ⇒C 2 [x])]

(fn k

⇒E)])))]

This is exactly the semantics of shift and reset given in Section 4.1 for the case when there is only one shift.
We will later add support for multiple shift’s.
For the remainder of this section, define block = (fn () ⇒2 * shift (fn k ⇒1 + k 5)). We consider the example
reset block. It evaluates as follows:
reset block

=⇒ let
=⇒ 11

val k = (fn t

⇒

2 * t) in 1 + k 5 end

⇒1 + k 5)] .
We now show a pseudocode implementation of shift and reset. shift checks a piece of mutable state to see
if it should ignore its argument and return some other value. For ease of extension, we use a stack, called the
replay_stack. If the replay_stack is nonempty, it does so; else, it does a "normal shift."
C[shift (fn k

5 Dyvbig

et al. (2007)

11

fun shift f = if

<replay_stack

is not empty>
pop replay_stack

else
normal_shift f
normal_shift calls its argument with "the captured continuation." In this example, (push replay_stack x; block ())
is equivalent to 2 * x. So, the captured continuation is equivalent to (fn x ⇒(push replay_stack x; block ())) .
Then normal_shift f must invoke f with this "proto thermometer continuation." shift then transfers control, along
with its result, to the enclosing reset — this is raising an exception.

fun normal_shift f = raise (Done (f (fn x

⇒

(push replay_stack x;
block ()))))

And reset must catch this exception so as to receive control.
reset f = (f ()) handle (Done x

⇒

x)

This is not a real definition of reset. With our definition of shift, reset f only works when f
ignoring how to handle multiple nested calls to reset until the real implementation.
The example is now translated as follows:

= block.

We’re

reset block

=⇒ (2

* (raise (Done (1 +
(push replay_stack 5; block ())))))
handle (Done x

=⇒

⇒

x)

11

This implementation also handles the example from Section 4.1 nicely. The example
1 + reset (fn ()

⇒

2 * (shift (fn k

⇒

k (k 5))))

becomes
⇒ 2 * (shift (fn k ⇒ k (k 5)))) in
1 + (2 * (raise (Done (push replay_stack
(push replay_stack 5; block ());

let val block = (fn ()

block ())))
handle (Done x

⇒

x))

end

==⇒ 21

4.3

Multiple (non-nested) shift’s

Replaying the block becomes more interesting when there are multiple shift’s. We’ll now show how to extend
our pseudocode implementation to handle multiple non-nested shift’s, introducing the record_stack. We’ll use
the following, which we explained in Section 4.1:
val block = (fn ()

⇒

shift (fn k

* shift (fn k’

⇒

⇒

1 + k

2)

1 + k’ 3))

reset block

12

With our previous implementation of shift, calling block () when the replay_stack contains [x, y] will return
x ∗ y. What happens when replay_stack only contains one value, [x]? It will run (pop replay_stack) * (shift . . .) .
x gets popped off the replay_stack before the second shift runs and pushes on y, so the block is never invoked
with more than one value on the replay_stack. This motivates the second record_stack. When shift pops a value
off the replay_stack, it saves it on the record_stack. This way, it can "remember" that value of x when it invokes
block the second time, moving values back from the record_stack to the replay_stack.
fun shift f = if

<replay_stack

is not empty>

let val x = pop replay_stack in
(push record_stack x;
x)
end
else
normal_shift f
fun normal_shift f = raise (Done (f (fn x

⇒

(replay_stack
record_stack

:=
:=

reverse (x

::

(!record_stack));

[];

reset block)))

This is enough to run our multi-shift example:
reset block

=⇒

(raise (Done (1 + (replay_stack : = reverse (2
record_stack : = [];

::

[]);

reset block)))

=⇒
=⇒

* shift (fn k’ ⇒ 1 + k’ 3)) handle (Done x ⇒ x)
1 + (push replay_stack 2; reset block)
1 + (push replay_stack 2; (((push record_stack 2; pop replay_stack)
* raise (Done (1 + (replay_stack : = reverse (3
record_stack : = [];

::

(!record_stack));

block ()))))
handle (Done x

=⇒

⇒

x)))

8

In Section 4.2, we could represent a continuation fn t ⇒C [t] as fn t ⇒(push replay_stack t; block ()). In this
section, if the continuation of a shift is fn t ⇒C [t], this continuation is represented by fn t ⇒(replay_stack : = reverse
where s is some stack. Hence, the continuation C can be represented by the pair (s, block). This motivates our
definition of a thermometer continuation.
Definition 4.1. A thermometer continuation for a continuation C is a pair of a stack and a computation,
(s, block), so that for appropriate functions change_state and run, change_state x s; run block evaluates to C [x].
So, the definitions of shift and reset in this section already implement thermometer continuations. Figure
5 depicts a thermometer continuation. For instance, the continuation of the second shift in this example,
(fn y ⇒2 * y) , is equivalent to invoking block with a replay stack of [2,y], and hence is represented by the
thermometer continuation ([2], block) .
Figure 5 shows a thermometer continuation. Figure 6 animates the execution of a thermometer continuation:
as block executes, each element of the replay stack pairs with a call to shift. When it’s finished, the remaining
13

(x

::st);

record

a
b
c
d
e

Function

Replay Record
Stack Stack

Fig. 5. A thermometer continuation before being invoked
e
d
c
b
stmt1 a
stmt2
stmt3

e
d
c
stmt1 b
stmt3

e
d
c
b
a

...
a

Thermometer
Continuation

Context

Fig. 6. Graphical depiction of running a thermometer continuation

execution of block is equivalent to that continuation C. The left side of Figure 6 resembles a thermometer sticking
out of the function, which inspired the name "thermometer continuations."
The version in this section, of course, still has limitations. We’ve been assuming the variable block was magically
set to the body of the reset, which ignores nested reset’s. It also ignores nested shift’s. It doesn’t work if the
captured continuation escapes the reset, which is needed for implementing the state monad (Section 5.4) and for
implementing iterators (e.g.: Python’s yield). And we’ve been assuming that replay_stack and record_stack only
contain integers; they need to store any value.
The general algorithm presented in the next section solves all these problems. The replay and record stacks
have a universal type. It’s careful about saving old values in closures. For nested shift’s, the replay stack can
store markers, indicating that the replay should re-enter a shift. And, to evaluate a nested reset, it must be able
to stow away the current block, record_stack, and replay_stack, evaluate the nested reset, and then restore them
afterwards. It does this with a third stack, called the reset_stack.

4.4

Real Thermometer Continuations

The previous two sections gave a quick sketch of thermometer continuations. Now we polish it, producing real
code that can handle anything that can be done with shift and reset. We start by defining the stack operations
we used in the previous sections. A stack is a mutable list:
(* push

: α

(* pop

: α

→ α → ()
: = x :: !st)

list ref

fun push st x = (st

list ref

→ α

*)

option *)

fun pop st = case !st of
(x :: xs)

⇒

(st

:=

xs;

14

SOME x)

|

⇒

[]

NONE

One problem with the record and replay stacks is that the values recorded may be of different types. So that
we may store many types of values on a single stack, following Filinski 6 , we define a universal type, which all
other types may be converted to and from:
signature UNIVERSAL = sig
type u;
val to_u

: α → u;
: u → α;

val from_u
end;

structure Universal

:

UNIVERSAL = struct

datatype u = U;
val to_u = Unsafe.cast;
val from_u = Unsafe.cast;
end;

Regrettably, this implementation uses Unsafe.cast, but shift and reset are carefully designed so that these casts
never fail. While Filinski was able to upgrade these definitions to a type-safe implementation of the universal
type in his follow-up paper 7 , the heavy use of replay in our construction unfortunately prevents that solution
from working. We chose not to search for another type-safe version of the universal type in order to keep this
paper focused.
A thermometer continuation is a (function, replay stack) pair. It can’t be called like a function directly. We will
provide a function called invoke_cont that invokes a thermometer continuation, running the function using the
replay stack as long as it lasts. We will present the definitions out-of-order, saving the invoke_cont function for
last, but the overall setup is:
functor Control (type ans)

:

CONTROL = struct

type ans = ans
(*
*

...

type, exception, and state definitions

*)
(* invoke_cont : (unit
fun invoke_cont f st =
fun reset f =

...

fun shift f =

...

→ ans) →
...

stack

→

ans *)

end;

6 Filinski
7 Filinski

(1994)
(1999)

15

The key state is the replay_stack and the record_stack. The entire executing computation is also stored in
mutable state.
To handle nested shift’s, the stacks store a frame type instead of raw values. Previously, when replaying an
expression that contains shift (fn k ⇒shift (fn l ⇒E)), there would be no way to enter the first shift, but make
the second shift return a value x. Now, this can be done with the replay stack [ENTER, RET x].
exception MissingFun
datatype frame = RET of Universal.u

|

ENTER

type stack = frame list
val record_stack
val replay_stack
val cur_fun

:

:
:

stack ref = ref []
stack ref = ref []

(unit

→

ans) ref = ref (fn ()

⇒

raise MissingFun)

The reset function is implemented as a small wrapper around invoke_cont: it invokes a computation with an
empty replay stack, causing the computation to execute from the start.
fun reset f = invoke_cont f []

The shift of Section 4.3 is almost complete. shift f just needs a couple casts to deal with the universally-typed
stacks, and it needs to dereference and it needs to dereference and capture the values of the record-stack and
cur_fun before invoking f. Then the captured continuation becomes observationally pure, so it can escape the
current reset.
exception Done of ans
fun shift f = case pop replay_stack of
(SOME (RET v)) ⇒ (push record_stack (RET v);
Universal.from_u v)

|

_

⇒

let val st = !record_stack
val g = !cur_fun in
(push record_stack ENTER;
raise (Done (f (fn v

⇒

invoke_cont g (RET (Universal.to_u v )

::

st)))))

end

One funny thing about this implementation is how it behaves the same when it encounters an ENTER frame
versus when the replay_stack is exhausted. Whether it was told to do so by the replay_stack or if it’s entering the shift for the first time, the correct thing to do is push an ENTER frame to the record stack. Note
how it captures the current state of the record_stack before pushing on the ENTER frame. So, in the expression
reset (fn () ⇒shift (fn k ⇒shift (fn l ⇒E))), invoking k x will replay the computation with a replay_stack
of [RET x], and will evaluate to reset (fn () ⇒x). Meanwhile, invoking l x will replay it with a replay_stack of
[ENTER, RET x], evaluating to reset (fn () ⇒shift (fn k ⇒x)).
We need one additional piece of state in order to implement invoke_cont. If a thermometer continuation is
invoked while executing another computation, the program must be able to save and restore the current values
in the replay and record stacks. Nested reset calls will also change the function currently being invoked, so this
must be saved as well. To accomplish this, invoke_cont uses a third stack, the reset stack.
type reset_stack = ((unit

→

ans) * stack * stack) list
16

val reset_stack

:

reset_stack ref = ref []

We are now ready to present invoke_cont f st. It is similar to the definition of reset given in 4.2, except that it
also saves and restores state to the reset_stack.
(* invoke_cont : (unit → ans) → stack → ans *)
fun invoke_cont f st =
(push reset_stack (!cur_fun, !record_stack, !replay_stack);
record_stack : = [];
replay_stack : = rev st;
cur_fun : = f;
let val res = (f () handle (Done x) ⇒ x)
val (SOME (f’, rec_stack’, rep_stack’)) = pop reset_stack in
cur_fun : = f’;
record_stack
replay_stack

:=
:=

rec_stack’;
rep_stack’;

res
end)

With this implementation finished, we can now run our earlier examples:
structure C = Control(type ans = int);
1 + C.reset (fn ()
(* val it = 21

:

C.reset (fn ()

⇒

⇒

2 * (C.shift (fn k

C.shift (fn k

* C.shift (fn k’
(* val it = 8

1 + C.reset (fn ()

5

k (k 5))))

⇒
⇒

1 + k

2)

1 + k’ 3))

int *)

:

(* val it = 37

⇒

int *)

:

⇒

2 + C.shift (fn k

⇒

3*(C.shift (fn l

⇒

l (k 10)))));

int *)

ARBITRARY MONADS

In 1994, Filinski showed how to use delimited continuations to express any monadic effect in direct style8 . The
explanation is quite obtuse, heavy on notation and light on examples. Dan Piponi has a blog post which is more
readable9 , but also missing big concepts like monadic reflection. In this section, we hope to convey a better intuition
for Filinski’s construction, and also discuss what it looks like when combined with thermometer continuations.
The code in this section comes almost verbatim from Filinski. This section is helpful for understanding the
optimizations of Section 6, in which we explain how to fuse thermometer continuations with the code in this
section.
8 Filinski
9 Dan

(1994)
Piponi (2008)

17

5.1

Monadic Reflection

In SML and Java, there are two ways to program with mutable state. The first is to use the language’s built-in
variables and assignment. The second is to use the monadic encoding, programming similar to how a pure
language like Haskell handles mutable state. A stateful computation is a monadic value, a pure value of type
s → (a, s).
These two approaches are interconvertible. The program can take a value of type s → (a, s) and run it,
yielding a stateful computation of return type a. This operation is called reflect. Conversely, it can take a stateful
computation of type a, and reify it into a pure value of type s → (a, s). Together, the reflect and reify operations
give a correspondence between monadic values and effectful computations. This correspondence is termed
monadic reflection.
reflect and reify generalize to arbitrary monads. Consider nondeterminism, where a nondeterministic computation is either an effectful computation of type a, or a monadic value of type [a]. Then the reflect operator
would take the input [1, 2, 3] and nondeterministically return 1, 2, or 3 — this is the choose operator from Section
2). reify would take a computation that nondeterministically returns 1, 2, or 3, and return the pure value [1, 2, 3]
— this is withNondeterminism.
So, for languages which natively support an effect, reflect and reify convert between effects implemented by
the semantics of the language, and effects implemented within the language. Curry is a language with built-in
nondeterminism, and it has these operators, calling them anyOf and getAllValues. SML does not have built-in
nondeterminism, but, for our previous example, one can think of the code within a withNondeterminism block as
running in a language extended with nondeterminism. So, one can think of the construction in the next section
as being able to extend a language with any monadic effect.
In SML, monadic reflection is given by the following signature:
signature RMONAD = sig
structure M

: MONAD
: α M.m → α
: (unit → α ) → α

val reflect
val reify

M.m

end;

5.2

Monadic Reflection through Delimited Control

Filinski’s insight was that the monadic style is similar to an older concept called continuation-passing style. We
can see this by revisiting an example from Section 2.
Consider this expression:
withNondeterminism (fun ()

⇒

(choose [2,3,4]) * (choose [5,6]))

It is transformed into the monadic style as follows:
bind [2,3,4] (fn x
bind [5,6]

(fn y

⇒
⇒

return (x * y)))

The first call to choose has continuation fn ⇒ * (choose [5,6]). If x is the value returned by the first call to
the second has continuation fn ⇒x * . These continuations correspond exactly to the functions bound
in the monadic style. The monadic bind is the "glue" between a value and its continuation. Nondeterministically
choosing from [2,3,4] wants to return thrice, which is the same as invoking the continuation thrice, which is the
same as binding to the continuation.
choose,

18

So, converting a program to monadic style is quite similar to converting a program to this "continuation-passing
style." Does this mean a language that has continuations can program with monads in direct style? Filinski
answers yes.
The definition of monadic reflection in terms of delimited control is short. The overall setup is as follows:
functor Represent (M

:

MONAD)

RMONAD = struct

:

structure C = Control(type ans = Universal.u M.m)
structure M = M

...
...

fun reflect m =
fun reify t =
end;

Figure 3 showed how nondeterminism can be implemented by binding a value to the (delimited) continuation.
The definition of reflect is a straightforward generalization of this.
fun reflect m = C.shift (fn k

⇒

M.bind m k)

If reflect uses shift, then reify uses reset to delimit the effects implemented through shift. This implementation
requires use of type casts, because reset is monomorphized to return a value of type Universal.u m. Without these
type casts, reify would read
fun reify t = C.reset (fn ()

⇒

M.return (t ()))

Because of the casts, the actual definition of reify is slightly more complicated:
⇒ M.return (Universal.to_u (t ()))))
(M.return o Universal.from_u)

fun reify t = M.bind (C.reset (fn ()

5.3

Example: Nondeterminism

Using this general construction, we immediately obtain an implementation of nondeterminism equivalent to the
one in Section 2.3 from Section 2’s definition of ListMonad.
structure N = Represent(ListMonad)
fun choose xs = N.reflect xs
fun fail () = choose []
N.reify (fn ()

⇒

let val x = choose [2,3,4] * choose [5,7] in
if x

≥

20 then x

else fail () end);
(* val it = [21,20,28]

:

int list *)

It’s worth thinking about how this generic implementation executes on the example, and contrasting it with
the direct implementation of Section 2.3. The direct implementation executes the function body 6 times, once
for each branch of the computation. The generic one executes the function body 10 times (once with a replay
stack of length 0, 3 times with length 1, and 6 times with length 2). In the direct implementation, choose will
return a value if it can. In the generic one, choose never returns. Instead, it invokes the thermometer continuation,
causes the desired value to be returned at the equivalent point in the computation, and then raises an exception
19

containing the final result. So, 4 of those times, it could just return a value rather than replaying the computation.
This is the idea of one of the optimizations we discuss in Section 6. This, plus one other optimization, let us
derive the direct implementation from the generic one.

5.4

Example: State monad

State implemented through delimited control works differently from SML’s native support for state.
functor StateMonad (type state)
type

α

m = state

fun return x = fn
fun bind m f = fn

: MONAD = struct
→ α * state
s ⇒ (x, s)
s ⇒ let val (x, s’) = m s
in f x s’ end

end;
structure S = Represent (StateMonad (type state = int) )
fun tick () = S.reflect (fn s

⇒

((), s+1))

= S.reflect (fn s ⇒ (s, s))
fun put n = S.reflect (fn _ ⇒ ((), n))
fun get ()

#1 (S.reify (fn ()

⇒

(put 5; tick ();
2 * get ()))

0)
(* val it = 12

:

int *)

Let’s take a look at how this works, starting with the example reify
(reify (fn ()

=⇒
=⇒
=⇒
=⇒
=⇒
=⇒

⇒

(reset (fn ()

⇒

⇒
⇒

3 * (reflect (fn s

⇒

⇒

* get ()).

(s, s))))) 2

return (3 * (shift (fn k

⇒ (s,s))
⇒ fn s ⇒

bind (fn s

(let val k = (fn x
(fn s

⇒3

3 * get ())) 2

(reify (fn ()
(fn k

(fn ()

k end)(fn x

⇒
⇒

bind (fn s

⇒

(s, s)) k))))) 2

return (3*x)) 2

(3*x, s)) in (fn s

⇒

k s s)) 2

(3*s, s)) 2

(6, 2)

The get in reify (fn () ⇒3 * get ()) suspends the current computation, causing the reify to return a function
which awaits the initial state. Once invoked with an initial state, it resumes the computation (multiplying by 3).
What does reify (fn () ⇒(tick (); get ())) do? The call to tick () expands into shift (fn k ⇒fn s ⇒k () (s+1)).
It again suspends the computation, awaiting the state s. Once it receives s, it resumes it, returning () from tick.
The call to get suspends the computation again, returning a function that awaits a new state; tick supplies s+1.
Think for a second about how this works when shift and reset are implemented as thermometer continuations.
The get, put, and tick operators do not communicate by mutating state. They communicate by suspending the
computation, i.e.: by raising exceptions containing functions. So, although the implementation of state in terms
of thermometer continuations uses SML’s native support for state under the hood, it only does so tangentially, to
capture the continuation.
20

6

OPTIMIZATIONS

Section 5.3 compared the two implementations of nondeterminism, and found that the generic one using
thermometer continuations replayed the computation gratuitously. Thermometer continuations also replay the
program in nested fashion, consuming stack space. In this section, we sketch a few optimizations that make
monadic reflection via thermometer continuations less impractical, and illustrate the connections between the
two implementations of nondeterminism.

6.1

CPS-bind: Invoking the Continuation at the Top of the Stack

The basic implementation of thermometer continuations wastes stack space. Look at the last example of Section
4.3, and notice how it calls block () three nested times. And yet, the outer two calls to block () will be discarded
by a raised exception as soon as the inner one completes. So, the implementation could save a lot of stack space
by raising an exception before replaying the computation. Indeed, we did this when symbolically evaluating that
example in 4.3 to make it easier to read.
So, when a program invokes a thermometer continuation, it will need to raise an exception to transfer control
to the enclosing reset, and thereby signal reset to replay the computation. While the existing Done exception
signals that a computation is complete, it can do this with a second kind of exception, which we call Invoke.
However, the shift and reset functions do not invoke a thermometer continuation: the body of the shift does.
In the case of monadic reflection, this is the monad’s bind operator. Raising an Invoke exception will discard the
remainder of bind, so it must somehow also capture the continuation of bind. We can do this by writing bind itself
in the continuation-passing style, i.e.: with the following signature:
val bind

: α

m

→ ( α → (β

m) cont)

→ (β

m) cont;

where (β m) cont = forall δ . (β m →δ ) →δ )
The above is not valid SML because SML lacks the rank-2 polymorphism (i.e.: the nested forall) required by
the continuation-passing style. Nonetheless, we have implemented this in both SML, using additional unsafe
casts, and in OCaml, which does support rank-2 polymorphism.
The supplementary material contains code with this optimization, and uses it to implement nondeterminism
in a way that executes more similarly to the direct implementation. We give here some key points. Here’s what
the CPS’d bind operator for the list monad would look like if SML hypothetically had rank-2 polymorphism:
fun bind []

|

f d = d []

bind (x :: xs) f d = f x (fn a

⇒

bind xs f
(fn b

⇒

d (a @ b)))

When used by reflect, f becomes a function that raises the Invoke exception, transferring control to the
enclosing reset, which then replays the entire computation, but at the top level. The continuations of the bind d
get nested in a manner which is harder to describe, but ultimately get evaluated at the very end, also at the
top level. So the list appends in d (a @ b) actually run at the top level of the reset, similar to how, in direct
nondeterminism, it is the outer call to withNondeterminism that aggregates the results of each branch.
While this CPS-monad optimization as described here can be used to implement many monadic effects, it
cannot be used to implement all of them, nor general delimited continuations. Consider the state monad from
Section 5.4: bind actually returns a function which escapes the outer reify. Then, when the program invokes that
function and it tries to invoke its captured thermometer continuation, it will try to raise an Invoke exception to
transfer control to its enclosing reify, but there is none. This CPS-monad optimization as described does not work
if the captured continuation can escape the enclosing reset. With more work, it could use mutable state to track
whether it is still inside a reset block, and then choose to raise an Invoke exception or invoke the thermometer
continuation directly.
21

6.2

Direct Returns

In our implementation, a reset body C[reflect (return 1)] expands into C[raise (Done (C[1] handle (Done x ⇒x)))].
So, the entire computation up until that reflect runs twice. Instead, of replaying the entire computation, that
reflect could just return a value. C[reflect (return 1)] could expand into C[1].
reflect (return 1) expands into shift (fn k ⇒bind (return 1) k). By the monad laws, this is equivalent to
shift (fn k ⇒k 1). Tail-calling a continuation is the same as returning a value, so this is equivalent to 1. So, it’s
the tail-call that allows this instance of reflect to return a value instead of replaying the computation.
Implementing the direct-return optimization is a small tweak to the CPS-bind optimization. The signature for
bind is further modified to:
val bind

: α

m

→ ( α → (β

m) cont)

→ ( α → (β

m) cont)

→ (β

m) cont;

where (β m) cont = forall δ . (β m →δ ) →δ ) . This variant of bind takes two arguments of type α →(β m) cont.
One raises an Invoke exception, as described in Section 6.1. The other returns a value directly, after updating the
internal state of the thermometer continuation implementation. So, the first time bind invokes the continuation,
it may do so by directly returning a value, and thereafter instead raises an Invoke exception.
The bind operator for the list monad never performs a tail-call (it must always wrap the result in a list), but,
after converting it to CPS, it always performs a tail-call. So this direct-return optimization combines well with
the previous CPS-monad optimization. Indeed, applying them both transforms the generic nondeterminsm of
Section 5.3 into the direct nondeterminism of Section 2. In Section 6.4, we show benchmarks showing that this
actually gives a faster implementation of nondeterminism than the code in Section 2.
In the supplementary material, we demonstrate this optimization, providing optimized implementations of
nondeterminism (list monad) and failure (maybe monad).

6.3

Memoization

While the frequent replays of thermometer continuations can interfere with any other effects in a computation,
it cannot interfere with observationally-pure memoization. Memoizing nested calls to reset can save a lot of
computation, and any expensive function can memoize itself without integrating into the implementation of
thermometer continuations.

6.4

Benchmarks

To get a better understanding of the performance cost of thermometer continuations and the effect of our
benchmarks, we implemented several benchmarks with different monadic effects.
There are four benchmarks: NQUEENS, INTPARSE-GLOB, INTPARSE-LOCAL, and MONADIC-ARITHPARSE. These four benchmarks use three different monads. Depending on the monad, we gave three to six
implementations of each benchmark. Each Direct implementation implements the program pure-functionally,
without monadic effects. The ThermoCont and Filinski implementations use monadic reflection, implemented
via thermometer continuations and Filinski’s construction, respectively. For the nondeterminism and failure
monads, our optimizations apply, given in Opt. ThermoCont. For the nondeterminism monad, we can also
use our Replay-based Nondet construction from Section 2. These were all implemented in SML. Finally,
for nondeterminism, we also compared to an implementation in Curry, which provides native support for
nondeterminism.
The SML solutions were all run using the SML/NJ interpreter v110.8010 . Although MLTON11 , the whole-program
optimizing compiler for SML, is far more efficient than SML/NJ, we could not easily port our implementation of
10 Appel
11 Weeks

and MacQueen (1991)
(2006)

22

thermometer continuations to MLTON because it lacks Unsafe.cast. We also tried using our OCaml implementation
of thermometer continuations; surprisingly, we got a stack overflow error even for relatively small inputs, even
though the implementation uses only shallow recursion, and the SML version ran fine. We ran the Curry
implementation in KiCS212 v0.5.1. Our informal experiments show that a different Curry compiler, PAKCS13 , was
much slower.All experiments were conducted on a 2015 MacBook Pro with a 2.8 GHz Intel Core i7 processor. All
times shown are the average of 5 trials, except for MONADIC-ARITH-PARSE, as discussed below.
The first benchmark NQUEENS is the problem of enumerating all solutions to the n-queens problem. Table 1
reports the times for each implementation for different n. While the direct implementation was unsurprisingly the
fastest, thermometer continuations beat Filinski’s construction for small n, and the optimized version remained
within a factor of 2 until n = 10. Optimized thermometer continuations beat replay-based nondeterminism, likely
because the optimized thermometer continuation solution replaces list allocations and operations with closures.
Surprisingly, Curry performed by far the worst; for n = 11, we killed the process after running it for 20 minutes.
The twin benchmarks INTPARSE-GLOB and INTPARSE-LOCAL both take a list of numbers as strings, parse
each one, and return their sum. They both use a monadic failure effect (like Haskell’s Maybe monad), and differ
only in their treatment of strings which are not valid numbers: INTPARSE-GLOB returns failure for the entire
computation, while INTPARSE-LOCAL will recover from failure and ignore any malformed entry. Table 2
gives the results for INTPARSE-GLOB. For each input size n, we constructed both a list of n valid integers, as
well as one which contains an invalid string halfway through. Table 3 gives the results for INTPARSE-LOCAL.
For each n, we constructed lists of n strings where every 1/100th, 1/10th, or 1/2nd string was not a valid int.
For INTPARSE-GLOB, unoptimized thermometer continuations wins, as it avoids Filinski’s cost of callcc, the
optimized version’s reliance on closures, as well as the direct approach’s cost of wrapping and unwrapping
results in an option type. For INTPARSE-LOCAL, unoptimized thermometer continuations lost out to the direct
implementation. Note that thermometer continuations here devolves into raising an exception for bad input, but
with a clean relation to the pure monadic monadic version.
Finally, benchmark MONADIC-ARITH-PARSE is a monadic parser in the style of Hutton and Meijer14 . These
programs input an arithmetic expression, and return the list of results of evaluating any prefix of the string which
is itself a valid expression. The Filinski and ThermoCont implementations closely follow Hutton and Meijer,
executing in a "parser" monad with both mutable state and nondeterminism (equivalent to Haskell’s StateT List
monad). The direct implementation inlines the monad definition, passing around a list of (remaining input, parse
result) pairs. We did not provide an implementation with optimized thermometer continations, as we have not
yet found how to make our optimizations work with the state monad. Note that all three implementations use
the same algorithm, while producing beautiful code (for the monadic versions), is exponentially slower than the
standard LL/LR parsing algorithms.
Table 4 reports the average running time of each implementation on 30 random arithmetic expressions with a
fixed number of leaves. There was very high variance in the running time of different inputs. For inputs with
40 leaves, the fastest input took under 25ms for all implementations, while the slowest took approximately 25
minutes on the direct implementation, 5 hours and 43 minutes for Filinski’s construction, and 9 hours 50 minutes
for thermometer continuations.
Overall, these benchmarks show that the optimizations of this section can provide a substantial speedup, and
there are many computations for which thermometer continuations do not pose a prohibitive cost. Thermometer
continuations are surprisingly competitive with Filinski’s construction, even though SML/NJ is known for its
efficient callcc, and yet thermometer continuations can be used in far more programming languages.
12 Braßel

et al. (2011)
et al. (2003)
14 Hutton and Meijer (1998)
13 Hanus

23

Direct
Replay-based Nondet
Filinski
ThermoCont
Opt. ThermoCont
Curry

4
0.006s
0.006s
0.010s
0.006s
0.006s
0.002s

5
0.005s
0.006s
0.009s
0.006s
0.006s
0.004s

6
0.005s
0.007s
0.010s
0.007s
0.006s
0.014s

7
0.006s
0.007s
0.011s
0.009s
0.008s
0.119s

8
9
10
0.006s 0.008s
0.015s
0.017s 0.089s
0.506s
0.014s 0.022s
0.046s
0.017s 0.052s
0.248s
0.013s 0.041s
0.198s
1.270s 13.593s 154.987s

11
12
0.064s
0.310s
2.606s 8m54.364s
0.199s
1.063s
1.497s
9.462s
1.210s
7.809s
>20m
>20m

Table 1. Benchmark NQUEENS

Bad input?
Y
Direct
N
Y
Filinski
N
Y
ThermoCont
N
Y
Opt. ThermoCont
N

1000
0.000s
0.000s
0.000s
0.000s
0.000s
0.000s
0.000s
0.000s

10,000
0.001s
0.002s
0.004s
0.004s
0.003s
0.003s
0.000s
0.002s

50,000
0.004s
0.014s
0.018s
0.020s
0.008s
0.011s
0.013s
0.015s

100,000
0.026s
0.051s
0.012s
0.014s
0.024s
0.029s
0.015s
0.024s

500,000
0.159s
0.213s
0.172s
0.221s
0.167s
0.223s
0.197s
0.247s

1,000,000
0.260s
0.371s
0.258s
0.360s
0.260s
0.367s
0.293s
0.364s

5,000,000
36.260s
1m54.072s
28.719s
1m26.603s
27.461s
1m20.841s
27.298s
1m23.433s

1000 10,000 50,000 100,000 500,000 1,000,000
0.000s 0.002s 0.011s
0.060s
0.232s
0.404s
0.000s 0.002s 0.002s
0.053s
0.221s
0.375s
0.000s 0.000s 0.001s
0.014s
0.176s
0.257s
0.000s 0.001s 0.048s
0.053s
0.264s
0.456s
0.000s 0.004s 0.043s
0.048s
0.234s
0.420s
0.000s 0.004s 0.008s
0.050s
0.182s
0.301s
0.000s 0.002s 0.045s
0.064s
0.344s
0.470s
0.000s 0.003s 0.028s
0.064s
0.266s
0.445s
0.000s 0.001s 0.023s
0.067s
0.214s
0.353s
0.000s 0.002s 0.030s
0.059s
0.227s
0.403s
0.000s 0.002s 0.030s
0.058s
0.218s
0.386s
0.000s 0.002s 0.023s
0.055s
0.183s
0.289s

5,000,000
2m04.316s
1m40.251s
15.515s
3m19.265s
3m22.245s
23.632s
4m28.700s
3m26.809s
22.750s
3m01.981s
2m37.321s
27.546s

Table 2. Benchmark INTPARSE-GLOB

% bad input
0.01
Direct
0.10
0.50
0.01
Filinski
0.10
0.50
0.01
ThermoCont
0.10
0.50
0.01
Opt. ThermoCont
0.10
0.50

Table 3. Benchmark INTPARSE-LOCAL

Direct
Filinski
ThermoCont

10
0.011s
0.116s
0.184s

20
0.163s
1.638s
2.540s

30
1.908s
19.035s
30.229s

40
2m39.860s
25m18.794s
39m58.183s

Table 4. Benchmark MONADIC-ARITH-PARSE

24

7

BUT ISN’T THIS IMPOSSIBLE?

In a 1990 paper, Matthias Felleisen presented formal notions of expressibility and macro-expressibility of one
language feature in terms of others, along with proof techniques to show a feature cannot be expressed 15 . Hayo
Thielecke used these to show that exceptions and state together cannot macro-express continuations 16 . This is
concerning, because, at first glance, this is exactly what we did.
First, a quick review of Felleisen’s concepts: Expressibility and macro-expressibility help define what should be
considered core to a language, and what is mere "syntactic sugar." An expression is a translation from a language
L containing a feature F to a language L 0 without it which preserves program semantics. A key restriction is
that an expression may only rewrite AST nodes that implement F and the descendants of these nodes. So, an
expression of state may only rewrite assignments, dereferences, and expressions that allocate reference cells. The
whole-program transformation that transforms a stateful program into a pure one that constantly passes around
an ever-updating "state" variables is not an expression. A macro-expression is an expression which may rewrite
nodes from F , but may only move or copy the children of such nodes (technically speaking, it must be a term
homomorphism). A classic example of a macro-expression is implementing the += operator in terms of normal
assignment and addition. A classic example of an expression which is not a macro-expression is desugaring
for-loops into while-loops (it must dig into the loop body and modify every continue statement). Another one is
implementing Java finally blocks (which need to execute an action after every return statement).
There are a couple reasons why Thielecke’s proof does not immediately apply. First, it only concerns macroexpressibility. Second, it concerns callcc-style continuations rather than delimited continuations. So, there are
two ways it could be extended to forbid our construction. First, one could extend Thielecke’s results to general
expressibility and delimited continuations. Second, we could limit the discussion to programs wrapped in an
all-encompassing reset, so that callcc will itself be macro-expressible using shift. We need not worry about their
combination: If we limit ourselves to programs that are entirely enclosed by a reset, then an "expression" of
shift/reset may rewrite the entire program.
It turns out that neither extension applies either. First, implementing effects with monadic reflection is not
an expression. An expression for mutable state may rewrite assignments and dereferences in terms of other
operations, but our construction must also enclose that entire program fragment in a reify. Filinski’s construction
is not an expression either for the same reason.
Second, even without the issue of wrapping with reify aside, our construction is still not a macro-expression.
Let’s take a look at Thielecke’s proof and see where it fails. Thielecke’s proof is based on showing that, in a
language with exceptions and state but not continuations, all expressions of the following form with different j
are operationally equivalent:
R j = λ f .((λx .λy.(f 0; x := !y; y := j; !x))(ref 0)(ref 0))
The intuition behind this equivalence is that the two reference cells are allocated locally and then discarded,
and so the value stored in them can never be observed. However, with continuations, on the other hand, f could
cause the two assignments to run twice on the same reference cells.
This example breaks down because it cannot be expressed in our monadic reflection framework as is. The
monadic reflection framework assumes there are no other effects within the program other than the ones
implemented via monadic reflection. To write the R j using thermometer continuations and monadic reflection,
the uses of ref must be changed from the native SML version to one implemented using the state monad. Then,
when the computation is replayed, repeated calls to ref may return the same reference cell, allowing the state to
escape, thereby allowing different R j to be distinguished.
15 Felleisen

(1990)
(2001)

16 Thielecke

25

8

RELATED WORK

Our work is most heavily based on Filinski’s work expressing monads using delimited control 17 . We have also
discussed theoretical results regarding the inter-expressability of exceptions and continuations in Section 7. Other
work on implementing continuations using exceptions relate the two from a runtime-engineering perspective
and from a typing perspective.
Continuations from stack inspection. Oleg Kiselyov’s delimcc library 18 provides an implementation of delimited
control for OCaml, based on the insight that the stack-unwinding facilities used to implement exceptions are
also useful in implementing delimited control. Unlike our approach, delimcc works by tightly integrating with
the OCaml runtime, exposing low-level details of its virtual machine to user code. Its implementation relies on
copying portions of the stack into a data structure, repurposing functionality used for recovering from stack
overflows. It hence would not work for e.g.: many implementations of Java, which recover from stack overflows
by simply deleting activation records. On the other hand, its low-level implementation makes it efficient and lets it
persist delimited continuations to disk. A similar insight is used by Pettyjohn et al 19 to implement continuations
using a global program transformation.
Typing power of exceptions vs. continuations. Lillibridge 20 shows that exceptions introduce a typing loophole
that can be used to implement unbounded loops in otherwise strongly-normalizing languages, while continuations
cannot do this, giving the slogan "Exceptions are strictly more powerful than call/cc." As noted by other authors 21 ,
this argument only concerns the typing of exceptions rather than their execution semantics, and is inapplicable
in languages that already have recursion.

9

CONCLUSION

Filinski’s original construction of monadic reflection from delimited continuations, and delimited continuations
from normal continuations plus state, provided a new way to program for the small fraction of languages which
support first-class continuations. With our demonstration that exceptions and state are sufficient, this capability
is extended to a large number of popular languages, including 9 of the TIOBE 1022 . While languages like Haskell
with syntactic support for monads may not benefit from this construction, bringing advanced monadic effects
to more languages paves the way for ideas spawned in the functional programming community to influence a
broader population.
In fact, the roots of this paper came from an attempt to make one of the benefits of monads more accessible.
We built a framework for Java where a user could write something that looks like a normal interpreter for a
language, but, executed differently, it would become a flow-graph generator, a static analyzer, a compiler, etc.
Darais 23 showed that this could be done by writing an interpreter in the monadic style (concrete interpreters
run programs directly; abstract interpreters run them nondeterministically). We discovered this concurrently
with Darais, and then discovered replay-based nondeterminism so that Java programmers could write normal,
non-monadic programs.
Despite the apparent inefficiency of thermometer continuations, the optimizations discussed in Section 6,
combined with the oft-unused speed of modern machines, provide hope that the ideas of this paper can find their
17 Filinski

(1994)
(2010)
19 Pettyjohn et al. (2005)
20 Lillibridge (1999)
21 Thielecke (2001)
22 TIOBE Software BV (2017)
23 Darais et al. (2017)
18 Kiselyov

26

way into practical applications. Indeed, Filinski’s construction is actually known as a way to make programs
faster 24
Overall, we view finding a way to bring delimited control into mainstream languages as a significant achievement. We hope to see a flourishing of work with advanced effects now that they can be used by more programmers.
Working code for all examples and benchmarks, as well as the CPS-bind and direct-return optimizations, is
available from https://github.com/jkoppel/thermometer-continuations .

REFERENCES
Andrew W Appel and David B MacQueen. 1991. Standard ML of new jersey. In International Symposium on Programming Language
Implementation and Logic Programming. Springer, 1–13.
Bernd Braßel, Michael Hanus, Björn Peemöller, and Fabian Reck. 2011. KiCS2: A new compiler from Curry to Haskell. Functional and
Constraint Logic Programming (2011), 1–18.
Dan Piponi. 2008. The Mother of all Monads. http://blog.sigfpe.com/2008/12/mother-of-all-monads.html. (2008). Posted: 2008-12-24. Accessed:
2017-02-27.
David Darais, Nicholas Labich, Phúc C Nguyen, and David Van Horn. 2017. Abstracting definitional interpreters (functional pearl). Proceedings
of the ACM on Programming Languages 1, ICFP (2017), 12.
R Kent Dyvbig, Simon Peyton Jones, and Amr Sabry. 2007. A monadic framework for delimited continuations. Journal of Functional
Programming 17, 6 (2007), 687–730.
Mattias 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, 180–190.
Matthias Felleisen. 1990. On the Expressive Power of Programming Languages. (1990), 134–151.
Andrzej Filinski. 1994. Representing Monads. In Proceedings of the 21st ACM SIGPLAN-SIGACT Symposium on Principles of Programming
Languages (POPL ’94). ACM, New York, NY, USA, 446–457. DOI:http://dx.doi.org/10.1145/174675.178047
Andrzej Filinski. 1999. Representing Layered Monads. In Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of
Programming Languages. ACM, 175–188.
M Hanus, S Antoy, B Braßel, M Engelke, K Höppner, J Koj, P Niederau, R Sadre, and F Steiner. 2003. PAKCS: The Portland-Aachen-Kiel Curry
System. (2003).
Michael Hanus, Herbert Kuchen, and Juan Jose Moreno-Navarro. 1995. Curry: A Truly Functional Logic Language. In Proc. ILPS, Vol. 95.
95–107.
Ralf Hinze. 2012. Kan Extensions for Program Optimisation or: Art and Dan Explain an Old Trick. In International Conference on Mathematics
of Program Construction. Springer, 324–362.
Graham Hutton and Erik Meijer. 1998. Monadic Parsing in Haskell. Journal of functional programming 8, 4 (1998), 437–444.
Oleg Kiselyov. 2010. Delimited Control in OCaml, Abstractly and Concretely: System Description. In International Symposium on Functional
and Logic Programming. Springer, 304–320.
Mark Lillibridge. 1999. Unchecked Exceptions Can Be Strictly More Powerful Than Call/CC. Higher-Order and Symbolic Computation 12, 1
(1999), 75–104.
Greg Pettyjohn, John Clements, Joe Marshall, Shriram Krishnamurthi, and Matthias Felleisen. 2005. Continuations from Generalized Stack
Inspection. In ACM SIGPLAN Notices, Vol. 40. ACM, 216–227.
Hayo Thielecke. 2001. Contrasting Exceptions and Continuations. Version available from http://www. cs. bham. ac. uk/hxt/research/exncontjournal. pdf (2001).
TIOBE Software BV. 2017. TIOBE Index for February 2017. http://www.tiobe.com/tiobe-index/. (2017). Posted: 2017-02-08. Accessed:
2017-02-22.
Stephen Weeks. 2006. Whole-program compilation in MLton. ML 6 (2006), 1–1.

24 Hinze

(2012)

27

