Logical Methods in Computer Science
Vol. 9(4:23)2013, pp. 1–36
www.lmcs-online.org

Submitted
Published

Oct. 20, 2011
Dec. 17, 2013

HANDLING ALGEBRAIC EFFECTS ∗
GORDON D. PLOTKIN a AND MATIJA PRETNAR b
a

Laboratory for Foundations of Computer Science, School of Informatics, University of Edinburgh,
Scotland
e-mail address: gdp@inf.ed.ac.uk

b

Faculty of Mathematics and Physics, University of Ljubljana, Slovenia
e-mail address: matija.pretnar@fmf.uni-lj.si
Abstract. Algebraic effects are computational effects that can be represented by an equational theory whose operations produce the effects at hand. The free model of this theory
induces the expected computational monad for the corresponding effect. Algebraic effects
include exceptions, state, nondeterminism, interactive input/output, and time, and their
combinations. Exception handling, however, has so far received no algebraic treatment.
We present such a treatment, in which each handler yields a model of the theory for exceptions, and each handling construct yields the homomorphism induced by the universal
property of the free model. We further generalise exception handlers to arbitrary algebraic
effects. The resulting programming construct includes many previously unrelated examples from both theory and practice, including relabelling and restriction in Milner’s CCS,
timeout, rollback, and stream redirection.

Introduction
In seminal work [13], Moggi proposed a uniform representation of computational effects
by monads [1]. For example, working in the category of sets, a computation that returns
values from a set A is modelled by an element of T A for a suitable monad T . Examples
of such effects include exceptions, state, nondeterminism, interactive input/output, time,
continuations, and combinations of them. Later, Plotkin and Power proposed to represent
effects by
(1) a set of operations that represent the sources of effects; and
(2) an equational theory for these operations that describes their properties [19].
The basic operational intuition is that each computation either returns a value or performs an operation with an outcome that determines a continuation of the computation.
The arguments of the operation represent the possible continuations. For example, using a
2012 ACM CCS: [Theory of computation]: Semantics and reasoning—Program constructs; Semantics
and reasoning—Program semantics—Algebraic semantics.
Key words and phrases: algebraic effects, exception handlers, generalised handlers.
∗
A preliminary version of this work was presented at ESOP 2009, see [21].
a
This research was supported by EPSRC grant GR/586371/01 and by a Royal Society-Wolfson Award.

l

LOGICAL METHODS
IN COMPUTER SCIENCE

c
DOI:10.2168/LMCS-9(4:23)2013

CC

G. D. Plotkin and M. Pretnar
Creative Commons

2

G. D. PLOTKIN AND M. PRETNAR

binary choice operation choose, a computation that nondeterministically chooses a boolean
is:
choose(return true, return false)
The outcome of making the choice is binary: either to continue with the computation given
by the first argument or else to continue with that given by the second.
A computation that returns values from a set A is modelled by an element of the
free model F A, generated by the equational theory. In the case of nondeterminism, these
equations state that choose is a semilattice operation. Modulo the forgetful functor, the
free model functor is exactly the monad proposed by Moggi to model the corresponding
effect [17]. Effects whose monad can be obtained by such an equational presentation are
called algebraic; the relevant monads are exactly the ranked ones. With the notable exception of continuations [4, 6], all of the above effects are algebraic, and, indeed, have natural
equational presentations.
The algebraic view has given ways of combining effects [7] and reasoning about them [20].
However, exception handlers provided a challenge to the algebraic approach.
The monad −+exc for a given set of exceptions exc is presented by a nullary exception
raising operation raisee () for each e ∈ exc and no equations. The operation raisee () takes
no arguments as there is no continuation immediately after an exception has been raised.
The question then arises how to deal with exception handling. One approach would be
to consider a binary exception handling construct
handlee (M, N )
which proceeds as M unless the exception e is raised, when it proceeds as N . This construct
has a standard interpretation as a binary operation using the exception monad; however,
as explained in [18], it lacks a certain naturality property characterising equationally specified operations. In programming terms this corresponds to the operation commuting with
evaluation contexts E[−]. For example we would expect each of the following two equations
to hold:
E[choose(M, N )] = choose(E[M ], E[N ])
E[raisee ()] = raisee ()
but not:
E[handlee (M, N )] = handlee (E[M ], E[N ])
Since the naturality property is common to all equationally specified operations, it follows
that no alternative (ranked) monad will suffice either.
In this paper we give an algebraic account of exception handling. The main idea is that
(1) handlers correspond to (not necessarily free) models of the equational theory; and
(2) the semantics of handling is given using unique homomorphisms that target such models
and are induced by the universal property of the free model.
The usual exception handling construct corresponds to the application of the unique homomorphism that preserves returned values. We, however, adopt a more general approach,
suggested by Benton and Kennedy [2], and which was an inspiration for the present work. In
Benton and Kennedy’s approach returned values are passed to a user-defined continuation;
this amounts to an application of an arbitrary induced homomorphism to a computation.
As we shall see, this idea generalises to all algebraic effects, yielding a new programming
concept enabling one to handle any algebraic effect. Examples include relabelling and
restriction in CCS [12], timeout, rollback, stream redirection of shell processes, and many
others. Conceptually, algebraic operations and effect handlers are dual: the former could

HANDLING ALGEBRAIC EFFECTS

3

be called effect constructors as they give rise to the effects; the latter could be called effect
deconstructors as the computations they provide proceed according to the effects already
created. Filinski’s reflection and reification operations provide general effect constructors
and deconstructors in the context of layered monads [3].
In Section 1, we illustrate the main semantic ideas via an informal discussion of exception handlers. Then, in Section 2, we give a calculus extending Levy’s call-by-push-value [9]
with operations, handler definitions, and an effect handling construct, which handles computations using a given handler. In Section 3, we give some examples that demonstrate the
versatility of our handlers. Next, in Section 4, we provide a denotational semantics, and
define a notion of handler correctness; an informal introduction to handler correctness is
given in Section 1.3. The denotational semantics is given in terms of sets and functions
although a more general categorical semantics should also be possible.
In Section 5, we sketch some reasoning principles for handlers, and then, in Section 6, we
give some results on the difficulty of deciding handler correctness. In Section 7, we describe
the inclusion of recursion; to do this we switch from the category of sets and functions to
that of ω-cpos (partial orders with suprema of increasing countable chains) and continuous
functions (monotone functions preserving such suprema). In the conclusion, we list open
questions and briefly discuss some possible answers. At various points in the paper we use
operational ideas to aid understanding; we do not however present a formal operational
semantics of effect handlers.
1. Exception Handlers
We start our study with exception handlers, both because they are an established concept [2,
10] and also since exceptions are the simplest example of an algebraic effect. To focus on
the exposition of ideas, we write this section in a rather informal style, mixing syntax and
semantics.
We consider a finite set of exceptions exc. Computations returning values from a
def
set A are modelled by elements of the exception monad T A = A + exc. This has unit
def
ηA = in1 : A → A + exc, and the computation return V is interpreted by ηA (V ) = in1 (V ),
while raisee () is interpreted by in2 (e).
1.1. Simple handling construct. Fixing A, the simple, standard, handling construct is
M handled with {raisee () 7→ Me }e∈exc
where {· · ·}e∈exc represents a set of computations, one for each exception e ∈ exc. The
construct proceeds by carrying out the computation M ∈ A + exc, intercepting raised
exceptions e ∈ exc by carrying out predefined computations Me ∈ A + exc instead. If we
choose not to handle a particular exception e, we take Me to be raisee (). The handling
construct satisfies two equations:
return V handled with {raisee () 7→ Me }e∈exc = in1 (V )
raisee′ () handled with {raisee () 7→ Me }e∈exc = Me′
From an algebraic point of view, the computations Me give a new model M for the
theory of exceptions. The carrier of this model is A + exc as before; however, for each e,

4

G. D. PLOTKIN AND M. PRETNAR

raisee () is instead interpreted by Me . We then see from the above two equations that
def

h(M ) = M handled with {raisee () 7→ Me }e∈exc
is the unique homomorphism (a map preserving operations) from A+exc to M that extends
the map in1 : A → A + exc, i.e., so that the following diagram commutes:
A
in1

ηA

✲

❄

✲ M
A + exc ............
h
The idea is therefore to obtain such a homomorphism h using the freeness of the model
A+ exc, used for computations, and then interpret the handling construct as an application
of h to the computation being handled. The existence of h, in turn, requires a model M
on A + exc for its target; that model is supplied via the handling construct.

1.2. Extended handling construct. Benton and Kennedy [2] generalised the handling
construct to one of the form
M handled with {raisee () 7→ Ne }e∈exc to x : A. N (x)
(written using our syntax). Here returned values are passed to a user-defined continuation,
a map N : A → B + exc, where B is a set that may differ from A; handling computations
Ne return values in B, if they do not themselves raise exceptions: thus Ne ∈ B +exc. These
two facts can be expressed equationally:
return V handled with {raisee () 7→ Ne }e∈exc to x : A. N (x) = N (V )
raisee′ () handled with {raisee () 7→ Ne }e∈exc to x : A. N (x) = Ne′
As discussed in [2], this construct captures a programming idiom that was cumbersome
to write with the simpler construct, allows additional program optimisations, and has a
stack-free small-step operational semantics.
Algebraically we again have a model M, this time on B + exc, interpreting raisee () by
Ne . The handling construct can be interpreted as h(M ), where h : A + exc → M is the
unique homomorphism that extends N , i.e., such that the following diagram commutes:
A
N

ηA

✲

❄

✲ M
A + exc ............
h
Note that all the homomorphisms from the free model to a model on a given carrier are
obtained in this way. So Benton and Kennedy’s handling construct is the most general one
possible from the algebraic point of view.

HANDLING ALGEBRAIC EFFECTS

5

1.3. Handling arbitrary algebraic effects. We can now see how to give handlers for
other algebraic effects. A model of an equational theory is an interpretation, i.e., a set and
a set of maps, one for each operation, that satisfies the equations; handlers give definitions
of such interpretations. As before, computations are interpreted in the free model and
handling constructs are interpreted by the induced homomorphisms. Where exceptions
were replaced by handling computations, operations are now replaced by the handling maps;
as computations are built from combinations of operations, handling a computation may
involve several such replacements.
Importantly however, not all interpretations yield a model of the theory, and so, in
that sense, not all handlers need be correct (see Section 4). If a handler is not correct then
handling constructs using it have no meaning. Even more, whether or not a handler is
correct may be undecidable (see Section 6).
We can see two general approaches to this difficulty when designing programming languages with facilities to handle effects. One is to make the language designer responsible:
the definable families should be restricted so that only models can be defined; this is the
approach taken in [21]. Another, the one adopted in this paper, is to allow complete freedom in the language: all possible definitions are permitted. In this case not all handlers are
correct, and it is not the responsibility of the language designer to ensure that all handlers
defined are correct.
One can envisage responsibility being assigned variously to the language designer, to
the compiler, to the programmer, to a protocol for establishing program correctness, or, in
varying degrees, to all of them. For example, some handlers may be “built-in”, and so the
responsibility of the language designer, while others may be defined by the programmer,
and so their responsibility.
2. Syntax
2.1. Signatures. Signature types α, β are given by:
α, β :: = b | 1 | α × β |

P

ℓ∈L αℓ

where b ranges over a given set of base types, where L ranges over finite subsets of labels
(taken from a fixed set Lab of all possible labels); we do not specify the set of labels in
detail, but assume such ones as needed are available. We specify a subset of the base types
as arity base types, and say that a signature type is an arity signature type if the only base
types it contains are arity ones.
To represent finite data such as booleans bool = {true, false}, finite subsets of integers n = {1, 2, . . . , n}, the empty setP0, characters chr, or memory locations loc, we may
confuse a finite set L with the type ℓ∈L 1. For infinite sets, such as natural numbers nat
or strings, we take base types as needed.
Next, we assume given a set of typed function symbols f : α → β. These represent pure
built-in functions, for example arithmetic function symbols, such as + : nat × nat → nat,
or function symbols for arithmetic relations, such as < : nat × nat → bool.
Finally, we assume given a finite set of typed operation symbols op : α _ β, where each
such β is an arity signature type, and an effect theory T . The operations represent sources
of effects and the effect theory determines their properties. In order to to focus on handlers,
we postpone the consideration of effect theories to Section 4.1.

6

G. D. PLOTKIN AND M. PRETNAR

The typing op : α _ β indicates that the operation represented by op accepts a parameter of type α and, after performing the relevant effect, its outcome, of type β, determines
its continuation; we say that op is parameterised on α and has arity β, or is β-ary. In case
α = 1, we may just write op : β.
The given sets of base types, arity base types, typed function symbols, and typed
operation symbols constitute a signature; the syntax is parameterised by the choice of such
a signature. The choice of signature (and theory) that we take evidently depends on the
effects we want to represent.
We now give some examples, taken from [7].
Examples 2.1.
Exceptions: We take a single nullary (i.e., 0-ary) operation symbol raise : exc _ 0, parameterised on exc, for raising exceptions. Here exc is a finite set of exceptions; we could
instead take it to be a base type if we wanted an infinite set of exceptions. The operation symbol is nullary as there is no continuation after raising an exception: instead the
exception has to be handled.
State: We take an arity base type nat for natural numbers and read and write operation
symbols get : loc _ nat and set : loc×nat _ 1, where loc is a finite set of locations. The
idea is that there is a state holding natural numbers in the locations, and get retrieves
the number from a given location, while set sets a given location to a given number and
returns nothing.
Read-only state: Here we only take an arity base type nat and a read operation symbol
get : loc _ nat.
(Binary) nondeterminism: We take a binary (i.e., 2-ary) operation symbol choose for
nondeterministic choice. The operation symbol is binary as the outcome of making a
choice is to decide between one of two choices.
Interactive input and output (I/O): We take a finite set chr of characters, and operation symbols read : chr, for reading characters, and write : chr _ 1, for writing them.
The operation symbol read is chr-ary, as the outcome of reading is to obtain a character;
the operation symbol write is unary as there will be just one continuation after writing
a character.
2.2. Types. Our language follows Levy’s call-by-push-value approach [9] and so has a strict
separation between value types A, B and computation types C. These types are given by:
P
A, B :: = b | 1 | A × B | ℓ∈L Aℓ | U C
Q
C :: = F A | ℓ∈L C ℓ | A → C

The value types extend the signature types, as there is an additional type constructor U −.
The type U C classifies computations of type C that have been thunked (or frozen) into
values; such computations can be passed around and later forced back into evaluation.
The computation type F A Q
classifies the computations that return values of type A.
The product computation type ℓ∈L C ℓ classifies finite indexed products of computations,
of types C ℓ , for ℓ ∈ L. These tuples are not evaluated sequentially as in a call-by-value
setting; instead, a component of a tuple is evaluated only once it is selected by a projection.
Finally, the function type A → C classifies computations of type C parametric on values of
type A.

HANDLING ALGEBRAIC EFFECTS

7

2.3. Terms. The terms of our language consist of value terms V , W , computation terms M ,
N , and handler terms H. They are given by:
V, W :: = x | f(V ) | hi | hV, W i | ℓ(V ) | thunk M
M, N :: = match V with hx, yi 7→ M | match V with {ℓ(xℓ ) 7→ Mℓ }ℓ∈L | force V |
return V | M to x : A. N | hMℓ iℓ∈L | prjℓ M | λx : A. M | M V |
opV (x : β. M ) | k(V ) | M handled with H to x : A. N
H :: = {opx : α (k : β → C) 7→ Mop }op : α_β
where x, y, . . . range over an assumed set of value variables, and k ranges over an assumed
set of continuation variables. Here {· · ·}ℓ∈L represents a set of computations, one for each
label ℓ ∈ L; similarly, {· · ·}op : α_β represents a set of computations, one for each operation
symbol op : α _ β.
We may omit type annotations in bindings if it does not cause ambiguity; we may also
speak of values, computations, or handlers instead of value terms, computation terms, or
handler terms, respectively.
All the syntax is standard from call-by-push-value, other than that for the handler
terms and the last line of the computation terms. Value terms are built from value variables, the usual constructs for finite products, constructs for indexed sums, and thunked
computations. Note that value terms only involve constructors, for example, pairing hV, W i,
while the corresponding destructor terms, for example matching match V with hx, yi 7→ M ,
are computations.
Next, there are constructor and destructor computation terms for computation types.
Perhaps the most interesting ones are the ones for the type F A. The constructor computation return V returns the value V , while the sequencing construct M to x : A. N evaluates
M , binds the result to x, and proceeds as N .
Next, there is an operation application computation term:
opV (x : β. M )
This first triggers the operation op with parameter V and then binds the outcome to x,
proceeding as the continuation M .
Examples 2.2.
• The computation
readhi (c : chr. writec (x : 1. writec (y : 1. return hi)))
reads a character c, entered by the user, prints it out twice, and returns the unit value.
• The computation
getl (n : nat. sethl,n+1i (x : 1. return n))
increments the number x, stored in location l, and returns the old value.
Next, a handler term
{opx : α (k : β → C) 7→ Mop }op : α_β
is given by a finite set of handling operation definitions
opx : α (k : β → C) 7→ Mop
one for each operation symbol op. The handling terms Mop are dependent on their parameters, captured in their parameter variables x, and on the continuations of the handled

8

G. D. PLOTKIN AND M. PRETNAR

operations, captured in their continuation variables k. Note that continuation variables
never appear independently, only in the form k(V ), where they are applied to a value V .
Examples 2.3.
• The exception handler
{raisee () 7→ Ne }e∈exc
given in Section 1, can be written as:
Hexc = {raisey : exc (k : 0 → C) 7→ match y with {e(z) 7→ Ne }e∈exc }
P
where y is the raised exception and k is the continuation. As exc = e∈exc 1, we match
y against all possible cases e(z), where z is a dummy variable of type 1. Note that we
do not use the continuation k in the handling term. Indeed, raise is a nullary operation
symbol and there are no values of type 0 we could feed to the continuation, hence we
cannot use it.
• Even though we cannot modify read-only state, we can still evaluate a computation with
the state temporarily set to a different value. To do so, we use the temporary-state handler
that is dependent on a variable n : nat; it is
Htemporary = {getl : loc (k : nat → C) 7→ k(n)}
Finally, we have the handling computation term
M handled with H to x : A. N
This evaluates the computation M , handling all operation application computations according to H, binds the result to x and proceeds as N . In more detail, handling works as follows.
Assume that M triggers an operation application opV (y. M ′ ) and that the corresponding
handling term is opz (k) 7→ Mop ∈ H. Then, the operation is handled by evaluating Mop
instead, with the parameter variable z bound to V and with each occurrence of a term of
the form k(W ) in Mop replaced by
M ′ [W/y] handled with H to x : A. N
Thus, the continuation k receives an outcome W , determined by Mop , and is handled in
the same way as M . The handling term Mop may use the continuation k any number of
times and the behaviour of the handling construct can be very involved. Note that while
continuations are handled by H, the handling term Mop itself is not. Any operations it
triggers or values it returns escape the handler. They could however be handled by an
enclosing handler.
We remark that sequencing M to x : A. N is equivalent to the special case of handling in
which H handles all operations by themselves: see the discussion of this point in Section 5.
Example 2.4. The simplest use for the handling construct is handling exceptions. Using
handlers, we would write the computation
M handled with {raisee () 7→ Ne }e∈exc to x : A. N
given in Section 1, as
M handled with Hexc to x : A. N
In this case, the behaviour matches the one given by Benton and Kennedy. If the computation M returns a value V then N [V /x] is evaluated. If, instead, the computation M
triggers an exception e then the replacement term Ne is evaluated instead; so, if a value is

HANDLING ALGEBRAIC EFFECTS

9

then returned, that value is the final result of the entire computation and is not bound in
N.
Remark 2.5. The syntax of our handling construct differs from that of Benton and
Kennedy:
try x : A ⇐ M in N unless {e ⇒ Me }e∈exc
They noted some programming concerns regarding their syntax [2]. In particular, is not
obvious that M is handled but N is not; this is especially the case when N is large and the
handler is obscured. An alternative they propose is:
try x : A ⇐ M unless {e ⇒ Me }e∈exc in N
but then it is not obvious that x is bound in N but not in the handler. The syntax of our
construct M handled with H to x : A. N addresses both those issues. It also clarifies the order
of evaluation: M is handled with H and its results are bound to x and then used in N .
In the next example we use a standard let binding abbreviation, defined as follows:
def

let x : A be V in M = (λx : A. M ) V
Example 2.6. Consider the temporary state handler Htemporary given in Example 2.3.
Then the computation
let n : nat be 20 in
getl (x : nat. getl (y : nat. return x + y))
handled with Htemporary to z : A. return z + 2
involving the stateful computation of Example 2.2 evaluates as follows: the first get operation is handled, with an outcome 20 bound to x; the second get operation in the continuation
is handled in the same way, again with an outcome 20 bound to y; next, return 20 + 20 is
handled with result 40; this is substituted for z in return z + 2, and the final result is 42.
As remarked in Section 1.3, the language considered in [21] has restricted facilities
for defining handlers. In more detail, two levels of language are considered there. In the
first there are no handlers, and so no handling constructs. The first level is used to define
handlers, which, if they give models, are then used in handling constructs in the second
level (which has no facilities for the further definition of handlers). This can be considered
a minimal approach in contrast to that considered here, which can rather be considered
maximal as handlers and handling can be nested arbitrarily deeply. The advantage of the
maximal approach is that it accommodates all possible ways of treating the problem of
ensuring that handlers give models.
2.4. Typing judgements. All typing judgements are made in value contexts
Γ = x1 : A1 , . . . , xm : Am
of value variables xi bound to value types Ai and continuation contexts
K = k1 : α1 → C 1 , . . . , kn : αn → C n
of continuation variables kj bound to continuation types αj → C j . Continuation types have
the form α → C and type continuations k that accept a value of an arity signature type α
and proceed as a computation of type C. Values are typed as Γ | K ⊢ V : A, computations

10

G. D. PLOTKIN AND M. PRETNAR

are typed as Γ | K ⊢ M : C, and handlers are typed as Γ | K ⊢ H : C handler. Values are
typed according to the following rules:
Γ | K ⊢ x:A

Γ | K ⊢ V :α
Γ | K ⊢ f(V ) : β

(x : A ∈ Γ)

Γ | K ⊢ V :A
Γ | K ⊢ W :B
Γ | K ⊢ hV, W i : A × B

Γ | K ⊢ hi : 1

(f : α → β)

Γ | K ⊢ V : Aℓ
P
Γ | K ⊢ ℓ(V ) : ℓ∈L Aℓ

(ℓ ∈ L)

Γ | K ⊢ M :C
Γ | K ⊢ thunk M : U C

Next, computations are typed according to the following rules:
Γ | K ⊢ V :A×B
Γ, x : A, y : B | K ⊢ M : C
Γ | K ⊢ match V with hx, yi 7→ M : C
P
Γ | K ⊢ V : ℓ∈L Aℓ
Γ, xℓ : Aℓ | K ⊢ Mℓ : C (ℓ ∈ L)
Γ | K ⊢ match V with {ℓ(xℓ ) 7→ Mℓ }ℓ∈L : C

Γ | K ⊢ V : UC
Γ | K ⊢ force V : C

Γ | K ⊢ M :FA
Γ, x : A | K ⊢ N : C
Γ | K ⊢ M to x : A. N : C

Γ | K ⊢ V :A
Γ | K ⊢ return V : F A
Γ | K ⊢ Mℓ : C ℓ (ℓ ∈ L)
Q
Γ | K ⊢ hMℓ iℓ∈L : ℓ∈L C ℓ

Γ, x : A | K ⊢ M : C
Γ | K ⊢ λx : A. M : A → C

Γ | K ⊢ V :α
Γ, x : β | K ⊢ M : C
Γ | K ⊢ opV (x : β. M ) : C

Q
Γ | K ⊢ M : ℓ∈L C ℓ
Γ | K ⊢ prjℓ M : C ℓ

(ℓ ∈ L)

Γ | K ⊢ M :A → C
Γ | K ⊢ V :A
Γ | K ⊢ M V :C
(op : α _ β)

Γ | K ⊢ V :α
Γ | K ⊢ k(V ) : C

(k : α → C ∈ K)

Γ | K ⊢ M :FA
Γ | K ⊢ H : C handler
Γ, x : A | K ⊢ N : C
Γ | K ⊢ M handled with H to x : A. N : C
Finally, handlers are typed according to the following rule:
Γ, x : α | K, k : β → C ⊢ Mop : C (op : α _ β)
Γ | K ⊢ {opx : α (k : β → C) 7→ Mop }op : α_β : C handler
Observe that K may contain more than one continuation variable when the handler being
defined is used in handling definitions of other handlers.
2.5. Abbreviations. Before we continue, let us introduce a few abbreviations to help make
examples more readable. First, we obtain arbitrary finite products from binary products:
def

A1 × · · · × An = (A1 × · · · × An−1 ) × An
def

(n ≥ 3)

hV1 , . . . , Vn i = hhV1 , . . . , Vn−1 i, Vn i (n ≥ 3)

HANDLING ALGEBRAIC EFFECTS

11

understanding binary product, where n = 2, as before, the unit product, where n = 1 as
simply A1 , and the empty product, where n = 0, as 1.
The main use of products is to pass around multiple values as one, so we set:
def

f(V1 , . . . , Vn ) = f(hV1 , . . . , Vn i)
def

ℓ(V1 , . . . , Vn ) = ℓ(hV1 , . . . , Vn i)
def

opV1 ,...,Vn (x : β. M ) = ophV1 ,...,Vn i (x : β. M )
def

k(V1 , . . . , Vn ) = k(hV1 , . . . , Vn i)
Further, where possible, we omit empty parentheses in values and write:
def

f = f()
def

ℓ = ℓ()
def

k = k()
We also adapt the tuple destructor to tuples of arbitrary finite size. Using this destructor, we allow multiple variables in binding constructs such as sequencing or handler
definitions. For example, we set
def

opx1 ,...,xn (k) 7→ M = opx (k) 7→ (match x with hx1 , . . . , xn i 7→ M )
Similarly, we omit empty parentheses in binding constructs that bind no variables. For the
set of booleans, we set:
def

if V then M else N = match V with {true 7→ M, false 7→ N }
We may use infix or other suitable notation when writing function applications. We may
assume additional function symbols if appropriate defining terms are available. Examples
include logical function symbols, such as or : bool × bool → bool, and relations such as
inequality on locations, 6=loc : loc × loc → bool.
For operation symbols op : α _ n, we define the usual finitary operation applications
by:
def
opV (M1 , . . . , Mn ) = opV (x : n. match x with {i 7→ Mi }i∈n )
and write handling definitions as:
opx (k1 , . . . , kn ) 7→ Mop
where in Mop , we write ki instead of k(i) for 1 ≤ i ≤ n. In particular, we have:
def

opV () = opV (x : 0. match x with {})
and the handling definitions for nullary operations do not contain the corresponding continuation variable. This agrees with the discussion given in Examples 2.3.
Operation applications can be somewhat cumbersome for writing programs, and instead
we may write computations using generic effects [18]. The generic effect corresponding to
an operation symbol op : α _ β is defined by:
def

op = λx : α. opx (y : β. return y) : α → F β

12

G. D. PLOTKIN AND M. PRETNAR

Computations
and
opV (y : β. M )
op V to y : β. M
behave equivalently, in that both first trigger the operation with parameter V , bind the
outcome to x, and proceed as M .
Example 2.7. The computations of Example 2.2 could be written using generic effects as
follows:
read hi to c : chr. write c; write c
and
get l to x : nat. sethl, x + 1i; return x
Here M ; N is the usual abbreviation for a sequencing M to x : 1. N , where the useless result
of M is bound to a dummy variable x.
When a handler term contains handling terms only for operation symbols from a subset Θ of the set of operation symbols, we assume that the remaining operations are handled
by themselves (so they are “passed through”). Such a handler is defined by:
(
(
)
Mop
(op ∈ Θ)
def
{opx (k) 7→ Mop }op∈Θ = opx (k) 7→
opx (y : β. k(y))
(op ∈
/ Θ)
op

Sometimes we do not wish to write a value continuation in handlers. Then, we use the
following abbreviation:
def

M handled with H = M handled with H to x : A. return x
which employs a standard value continuation — the identity one. This abbreviation can be
considered as a generalisation to arbitrary algebraic effects of the simple exception handling
construct discussed in Section 1.
There is a difference between
M handled with H to x : A. N
which is the full handling construct,
(M handled with H) to x : A. N
which takes the result of the handled computation and binds it to x in N , and
(M to x : A. N ) handled with H
which handles the computation that evaluates M and binds the result to x in N . Both
the first and the second computation handle only effects triggered by M , while the third
computation handles effects triggered by both M and N . Furthermore, in the first computation, x binds the value returned by M , while in the second computation, x binds the
value returned by M once handled with H.
Example 2.8. To see the difference between the first two computations and the third, set:
def

H = {raisee () 7→ return 10}
def

M = return 5
def

N = raisee ()

HANDLING ALGEBRAIC EFFECTS

13

Then the first two computations raise exception e, while the third one returns 10. To see
the difference between the second computation and the other two, set:
def

H = {raisee () 7→ return 10}
def

M = raisee ()
def

N = return 5
Then the second computation returns 5, while the other two return 10.
3. Examples
We now give some more examples to further demonstrate the scope of handlers of algebraic effects. As before such examples can be understood using the informal operational
understanding of handlers given above. The question of the correctness of our examples is
addressed in Remark 4.6, after the notions of effect theories and handler correctness have
been presented.
3.1. Explicit Nondeterminism. The evaluation of a nondeterministic computation usually takes only one of all the possible paths. An alternative is to take all the paths in some
order and allow the possibility of a path’s failing. This kind of nondeterminism is represented slightly differently from binary nondeterminism. In addition to the binary operation
symbol choose, we take a nullary operation symbol fail, representing a path that failed. This
interpretation of nondeterminism corresponds to Haskell’s nondeterminism monad [14].
We consider a handler which extracts the results of a computation into a list (which can
then be operated on by other computations). Since our calculus has no polymorphic lists
— although they could easily be added — we limit ourselves to lists of a single base type
b. We take a base type listb and function symbols: nil : 1 → listb , cons : b × listb → listb ,
append : listb × listb → listb .
Then, all the results of a computation Γ | K ⊢ M : F b can be extracted into a returned
value of type F listb by
Γ | K ⊢ M handled with Hlist to x : b. return cons(x, nil) : F listb
where Hlist is the handler given by:
Γ|K⊢{
fail() 7→ return nil,
choose(k1 , k2 ) 7→ k1 to l1 : listb . k2 to l2 : listb . return append(l1 , l2 )
} : F listb handler

14

G. D. PLOTKIN AND M. PRETNAR

3.2. CCS. To represent (the finitary part of) Milner’s CCS [12] we take a type name
of (channel) names and an equality function symbol =name : name × name → name;
we write lab for a type of labels, abbreviating name+ + name− , and act for a type of
actions, abbreviating 1τ + lablab . We further take three operation symbols representing
combinators which we consider as effect constructors: deadlock nil : 1 _ 0, action prefix
prefix : act _ 1, and sum choose : 1 _ 2. We use the usual notation and write P instead of
M for processes, a.P instead of prefixa (P ), and P1 + P2 instead of choose(P1 , P2 ). Processes
P do not terminate normally, only in deadlock, hence we represent them as computations
P : F 0.
We consider the other CCS combinators as effect deconstructors. Both relabelling and
restriction can be represented using handlers. In order to write these handlers we assume
available an equality function symbol =act : act × act → act on actions and a “dual”
function symbol · : lab → lab: both have evident definitions. We also feel free to omit
evident conversions, from name to label, and from label to act.
Relabelling P [m/l] replaces all actions with label l (respectively l) in P by actions with
label m (respectively m); it can be represented using the following handler:
Γ, l : lab, m : lab | K ⊢ {a.k 7→ if a = τ then k else
if a = l then m.k else
if a = l then m.k else a.k}
: F 0 handler
One can deal with more general versions of renaming involving finitely given functions from
labels to labels similarly.
Restriction P \n blocks all actions with name n in P ; it can be represented using the
following handler:
Γ, n : name | K ⊢ {a.k 7→ if a = n or a = n then nil() else a.k} : F 0 handler
One can deal with more general versions of restriction involving finite sets of names similarly. The two handlers give handling terms only for prefix because our convention for
handling omitted operations gives exactly the expected structural behaviour of relabelling
and restriction on nil and choose.
We do however, not know how to represent the final CCS combinator — parallel, written
P | Q. Parallel is also an effect deconstructor, but unlike relabelling and restriction, which
are both unary deconstructors, it is a binary deconstructor as it reacts to actions of both
its arguments. For a discussion of the difficulties in the treatment of such deconstructors,
see [24].
The next few examples concern the use of parameter-passing handlers. We sometimes
wish to handle different occurrences of the same operation differently, depending on the
value of some parameter passed between the different occurrences. Although each handler
prescribes a fixed handling term for each operation, we can use handlers on function types
P → C to obtain C handlers that pass around parameters of value type P . Each handling
term then has the type P → C, rather than C, and captured continuations k have the type
α → (P → C), rather than α → C.
3.3. Interactive input and output (I/O). Suppose we wish to suppress output after a
certain number of characters have been printed out. For any computation type C, we define

HANDLING ALGEBRAIC EFFECTS

15

a character-suppressing handler Hsuppress by:
Γ, nmax : nat | K ⊢ {
writec (k : 1 → (nat → C)) 7→ λn : nat.
if n < nmax then writec (k() (n + 1)) else k() nmax
} : nat → C handler
The handling term for write is dependent on n : nat, the number of characters printed out. If
this number is less than nmax , the maximum number of characters we want to print out, we
write out the character and then handle the continuation, but now passing an incremented
parameter to it. But if n ≥ nmax , we do not perform the write operation, but continue with
the handled continuation. It does not matter exactly which parameter we pass to it, as long
as it at least nmax . Still, we call the continuation as it may return a value or trigger other
operations. (Using a convention introduced above regarding operations of type α _ n, the
definition of Hsuppress could have been written a little more elegantly, taking k : nat → C,
and so on.)
Since the type of the handler is not of the form F A handler, we need to specify a term
for “handling” values in the handling construct, also dependent on the current value of the
parameter. For example, if we wish to handle M : F A with Hsuppress , we write
Γ | K ⊢ M handled with Hsuppress to x : A. λn : nat. return x : nat → F A
This means than no matter what the value of parameter n is, we return the value x. The
handled computation has type nat → F A and so, in order to obtain a computation of type
F A, we need to apply it to the initial parameter 0 : nat as:
Γ | K ⊢ (M handled with Hsuppress to x : A. λn : nat. return x) 0 : F A
Remark 3.1. In the presence of parameters, the convention of handling omitted operations
by themselves is still valid (this convention was used above for the input operation read).
What one wishes to do in the case of an operation that is not handled is to pass an unchanged
parameter to the continuation, that is:
opy (k) 7→ λp : P. opy (x : β. k(x) p)
Since operations are defined pointwise on the function type, this is equivalent to
opy (k) 7→ opy (x : β. λp : P. k(x) p)
which, by η-equality, is equivalent to
opy (k) 7→ opy (x : β. k(x))
and is exactly what our convention assumes. The two equalities we have used here are
discussed further in Section 5.

16

G. D. PLOTKIN AND M. PRETNAR

3.4. Timeout. The timeout handler furnishes another example of parameter-passing. This
runs a computation and waits for a given amount of time. If the computation does not
complete in given time, it terminates it, returning a default value x0 instead.
We represent time using a single operation delay : nat _ 1, where delayt (M ) is a computation that stalls for t units of time, and then proceeds as M . For any value type A, the
timeout handler Htimeout is given by:
Γ, x0 : A, twait : nat | K ⊢ {
delayt (k : nat → F A) 7→ λtspent : nat.
if t + tspent ≤ twait
then delayt (k(t + tspent ))
else delaytwait −tspent (return x0 )
} : nat → F A handler
(now making use of the above convention introduced regarding operations op : α _ n). The
handler is used on a computation M : F A as follows:
Γ, x0 : A, twait : nat | K ⊢ (M handled with Htimeout to x : A. λt : nat. return x) 0 : F A
Note that the handling term preserves the time spent during the evaluation of the handled
computation.
3.5. Rollback. When a computation raises an exception while modifying the memory, for
example, when a connection drops halfway through a database transaction, we may want to
revert all modifications made during the computation. This behaviour is termed rollback.
Assuming, for the sake of simplicity, that there is only a single location, which is given
by a term l0 , an appropriate rollback handler Hrollback is given by:
Γ, ninit : nat | K ⊢ {raisee (k) 7→ setl0 ,ninit (M ′ e)} : C handler
where M ′ : exc → C. To evaluate a computation M , rolling back to the initial state ninit in
the case of exceptions, we write:
Γ | K ⊢ getl0 (ninit : nat. M handled with Hrollback ) : C
An alternative is a parameter-passing handler, which does not modify the memory,
but keeps track of all the changes to the location l0 in the parameter n. Then, once the
handled computation has returned a value, meaning that no exceptions have been raised,
the parameter is committed to the memory. This handler Hparam-rollback is:
Γ|K⊢{
getl0 (k : nat → (nat → C)) 7→ λn : nat. k(n) n
setl0 ,n′ (k : 1 → (nat → C)) 7→ λn : nat. k() n′
raisee () 7→ λn : nat. M ′ e
} : nat → C handler
It is used on a computation M as follows:
getl0 (ninit : nat. (M handled with Hparam-rollback to x : A. λn : nat. setl0 ,n (return x)) ninit )

HANDLING ALGEBRAIC EFFECTS

17

Here the initial state is read, obtaining ninit , which is passed to the handler as the initial
parameter value. If no exception is raised and a value x is returned, the state is updated
to reflect the final value n of the parameter.
3.6. Stream redirection. Let us conclude with a practical example of processes in a Unixlike operating system. These processes read their input and write their output through
standard input and output channels. These channels are usually connected to a keyboard
and a terminal window. However, an output of one process can be piped to the input of
another one, allowing multiple simple processes to be combined into more powerful ones.
We present a simplified model of files and devices. We take a base type file to represent
files and two operation symbols: read : channel _ chr and write : chr×channel _ 1. Here,
channel is an abbreviation for the sum 1std + filefile , where std represents the standard
input and output channel, and file(f ) represents the file f . A more realistic model would
have to include an operation that allows one to open a file and thus obtain a needed channel,
and a similar operation for closing an opened file. In our model, one may instead assume
that all files have already been opened for reading and writing.
We begin with the redirection p > out which takes the output stream of a process p
and writes it to a file out. This is used to either automatically generate files or to log the
activity of processes. The redirection is written as:
Γ | K ⊢ let f : file be out in p handled with H> : C
where the handler H> is given by:
Γ, f : file | K ⊢ {
writec,ch(k) 7→ match ch with {
std 7→ writec,file(f ) (k),
file(f ′ ) 7→ writec,file(f ′ ) (k)
}
} : C handler
Unix allows some devices to present themselves as ordinary files. This, for example,
allows a program to print out a document by simply redirecting its output to a file that
corresponds to the printer. A general treatment of devices is beyond the scope of this paper,
but some simple devices can be modelled with handlers.
An example is the null device /dev/null, which discards everything that is written to
it. The command p > /dev/null hence effectively suppresses the output of the process p.
The same behaviour can be achieved using the handler H> /dev/null , given by:
Γ|K⊢{
writec,ch (k) 7→ match ch with {
std 7→ k,
file(f ′ ) 7→ writec,file(f ′ ) (k)
}
} : C handler

18

G. D. PLOTKIN AND M. PRETNAR

A similar redirection p < in reads the file in and passes its contents to the process p.
This redirection can be represented using a handler that now replaces the standard input
with a given file in all read operations. It is given by:
Γ, f : file | K ⊢ {
readch (k) 7→ match ch with {
std 7→ readfile(f ) (c : chr. k(c)),
file(f ′ ) 7→ readfile(f ′ ) (c : chr. k(c)))
}
} : C handler
Both redirections can be combined so (p < in) > out reads the input file and writes the
processed contents to the output file.
We next consider Unix pipes p1 | p2, where the output of p1 is fed to the input of p2.
Using handlers we can express simple cases of the pipe combinator |. For example, consider
the pipe yes | p, where the process yes outputs an infinite stream made of a predetermined
character (the default one being y). Such a pipe then gives a way of routinely confirming a
series of actions, for example deleting a large number of files. (This is not always the best
way, since processes usually provide a safer means of doing the same thing, but is often
useful when they do not.) This particular pipe may be written using the following handler:
Γ, c : chr | K ⊢ {readstd (k) 7→ k(c)} : C handler
The general pipe combinator p1 | p2 is harder to represent, because like the CCS parallel
combinator, and unlike the above redirections and the simple pipe, it is a binary rather
than a unary deconstructor.
It would be very interesting to investigate to what extent the effects supported by Unix
can be realistically modelled using the methods of the algebraic theory of effects: as well as
files and devices there are, for example, signals or process scheduling.
4. Semantics
We now introduce effect theories and their interpretations and then give the denotational
semantics of our language for handling algebraic effects. For the sake of simplicity, we largely
limit ourselves to sets, but show in Section 7 how everything adapts straightforwardly to
ω-cpos.
4.1. Effect theories. We describe properties of effects with equations between templates T .
These describe the general shape of all computations, regardless of their type. Assuming a
given signature, templates are given by:
T :: = z(V ) | match V with hx, yi 7→ T | match V with {ℓ(xℓ ) 7→ Tℓ }ℓ∈L | opV (x : β. T )
where z ranges over a given set of template variables.
In templates, we limit ourselves to signature values. These are values that can be typed
as Γ ⊢ V : α, where Γ is a context of value variables bound to signature types; the typing
rules for this judgement are, with the omission of continuation contexts and the rule for
typing thunks, the same as those for values.

HANDLING ALGEBRAIC EFFECTS

19

We build templates in a context of value variables, bound to signature types, and a
template context
Z = z1 : α1 , . . . , zn : αn
of template variables zj , bound to arity signature types αj . Note: zj : αj does not represent
a value of type αj , but a computation dependent on such a value. As templates describe
common properties of computations, we do not assign them a type, but only check whether
they are well-formed, relative to a value context and a template context. The typing
judgement for being a well-formed template is Γ | Z ⊢ T ; it is given by the following rules:
Γ ⊢ V :α
Γ | Z ⊢ z(V )

(z : α ∈ Z)

Γ ⊢ V :α×β
Γ, x : α, y : β | Z ⊢ T
Γ | Z ⊢ match V with hx, yi 7→ T

P
Γ ⊢ V : ℓ∈L αℓ
Γ, xℓ : αℓ | Z ⊢ Tℓ (ℓ ∈ L)
Γ | Z ⊢ match V with {ℓ(xℓ ) 7→ Tℓ }ℓ∈L
Γ ⊢ V :α
Γ, x : β | Z ⊢ T
Γ | Z ⊢ opV (x : β. T )

(op : α _ β)

An effect theory T over a given signature is a finite set of equations Γ | Z ⊢ T1 = T2 ,
where T1 and T2 are well-formed relative to Γ and Z.
Some examples follow, continuing on from the corresponding signatures given in Example 2.1 and Section 3. We make use of abbreviations for handling tuples, etc., in templates
that are analogous to those introduced above for the other kinds of terms.
Examples 4.1.
Exceptions: The effect theory is the empty set, as exceptions satisfy no nontrivial equations.
State: The effect theory consists of the following equations (for readability, we write this
and other theories without contexts):
getl (x. z) = z
getl (x. setl,x (z)) = z
setl,x (setl,x′ (z)) = setl,x′ (z)
setl,x (getl (x′ . z(x′ )) = setl,x (z(x))
getl (x. getl (x′ . z(x, x′ ))) = getl (x. z(x, x))
setl,x (setl′ ,x′ (z)) = setl′ ,x′ (setl,x (z))

(l 6= l′ )

setl,x (getl′ (x′ . z(x′ )) = getl′ (x′ . setl,x (z(x′ )))

(l 6= l′ )

getl (x. getl′ (x′ . z(x, x′ ))) = getl′ (x′ . getl (x. z(x, x′ ))

(l 6= l′ )

We found it convenient to write the last three equations with a side condition l 6= l′ . This
still remains within the scope of our definition of an effect theory, reading T1 = T2 (l 6= l′ )
as an abbreviation of the equation
T1 = (if l 6=loc l′ then T2 else T1 )
There is some redundancy in these equations, with (see [17, 11]) the first, fifth, and
eight being consequences of the others for a suitable notion of equational consequence (a

20

G. D. PLOTKIN AND M. PRETNAR

semantic such notion can be provided using the interpretations of effect theories defined
in Section 4.2 below).
Read-only state: The effect theory consists of the following equations:
getl (x. z) = z
′

getl (x. getl (x . z(x, x′ ))) = getl (x. z(x, x))
getl (x. getl′ (x′ . z(x, x′ ))) = getl′ (x′ . getl (x. z(x, x′ ))

(l 6= l′ )

Nondeterminism: The effect theory consists of the following equations:
choose(z, z) = z
choose(z1 , z2 ) = choose(z2 , z1 )
choose(choose(z1 , z2 ), z3 ) = choose(z1 , choose(z2 , z3 ))
Explicit nondeterminism: The effect theory consists of the following equations:
choose(choose(z1 , z2 ), z3 ) = choose(z1 , choose(z2 , z3 ))
choose(z, nil()) = z
choose(nil(), z) = z
I/O, Stream redirection: The effect theory is (again) the empty set.
Time: The effect theory consists of the following equations:
delay0 (z) = z
delayt1 (delayt2 (z)) = delayt1 +t2 (z)
CCS: We take the effect theory for CCS to be the union of the effect theories for nondeterminism and explicit nondeterminism, i.e., it consists of the following equations:
choose(z, z) = z
choose(z1 , z2 ) = choose(z2 , z1 )
choose(choose(z1 , z2 ), z3 ) = choose(z1 , choose(z2 , z3 ))
choose(z, nil()) = z
choose(nil(), z) = z
These equations are those axiomatising strong bisimulation; for weak bisimulation one
would add Milner’s τ laws [12].
Destructive exceptions: The signature of destructive exceptions is that of state together
with that of exceptions, and its theory consists of all the equations for state and the
following two equations:
getl (x. raisee ()) = raisee ()
setl,x (raisee ()) = raisee ()
As raise is nullary, we have written raisee () instead of raisee (x : 0. T ), emphasising that
the continuation never gets evaluated.

HANDLING ALGEBRAIC EFFECTS

21

The equations imply that a memory operation followed by raising an exception is the
same as just raising the exception. Effectively, this implies that all memory operations
are moot if an exception occurs, hence the terminology of destructive exceptions. Observe that the first equation is an instance of one occurring in the effect theory for state.
The theory of destructive exceptions is discussed as that of “rollback” in [7], where it is
given as an example of the tensor of two theories.
4.2. Interpreting effect theories. We assume given an effect theory T . We begin by
interpreting each signature type α by a set JαK.
Suppose we are given an assignment JbK of a set to each base type b, such that JbK is
countable in the case that b is an arity base type. Finite products and sums of signature
types are then interpreted using the corresponding set operations, and base types are interpreted by the assigned sets. Note that JαK is then a countable set for any arity signature
type α; this will allow us to interpret effects in terms of countable equational theories.
An interpretation of T then consists of such an assignment together with a map
JfK : JαK → JβK for each function symbol f : α → β. The intended interpretations for each
of our examples should be clear. For instance Jlistb K is the set of lists of elements of JbK,
JappendK : Jlistb K → Jlistb K is list concatenation, and JnameK is a given set with equality
function J=name K :JnameK × JnameK → JnameK.
We assume given such an interpretation. We can then interpret each well-typed signature value Γ ⊢ V : α in an evident way by a map JV K : JΓK → JαK, where value contexts Γ
are interpreted component-wise by setting Jx1 : α1 , . . . , xm : αm K = Jα1 K × · · · × Jαm K.
Take a set |M| and an operation
opM : JαK × |M|JβK → |M|
for each operation symbol op : α _ β. Then, we can interpret a well-formed template
Γ | Z ⊢ T by a map JΓ | Z ⊢ T K : JΓK × JZK → |M|, where template contexts Z are
interpreted component-wise by Jz1 : α1 , . . . , zn : αn K = |M|Jα1 K × · · · × |M|Jαn K .
We can then interpret templates:
JΓ | Z ⊢ zj (V )K(a, b) = prj (b)(JV K(a))

(1 ≤ j ≤ n)

JΓ | Z ⊢ match V with hx, yi 7→ T K(a, b) = JT K(ha, pr1 (JV K(a)), pr2 (JV K(a))i, b)
JΓ | Z ⊢ match V with {ℓ(xℓ ) 7→ Tℓ }ℓ∈L K(a, b) = JTℓ K(ha, xi, b)

(if JV K(a) = ℓ(x))

JΓ | Z ⊢ opV (x : β. T )K(a, b) = opM (JV K(a), JT K(ha, −i, b))
where on the right, pri : A1 × · · · × An → Ai is the i-th projection, and we have abbreviated evident typing judgements. We also used a standard notation for functions, writing
JT K(ha, −i, b) for the function x :JβK 7→ JT K(ha, xi, b).
Definition 4.2. A model M of the effect theory T is a set |M|, called the carrier of the
model, together with an operation
opM : JαK × |M|JβK → |M|
for each operation symbol op : α _ β, such that JT1 K = JT2 K holds for all the equations
Γ | Z ⊢ T1 = T2 in T .
A homomorphism h : M1 ⊸ M2 is a map h : |M1 | → |M2 | such that
h ◦ opM1 = opM2 ◦ (idJαK × hJβK )

22

G. D. PLOTKIN AND M. PRETNAR

holds for all operation symbols op : α _ β.
The models of T and the homomorphisms between them form a category ModT . This
def
category is equipped with a forgetful functor U : ModT → Set, where U M = |M| and
def

U h = h.
Proposition 4.3. The functor U : ModT → Set has a left adjoint F : Set → ModT .
Proof. The existence of the adjoint functor follows from the corresponding result in the
context of countable equational theories [5].
First we obtain a countable equational theory Tω from T . The signature of Tω consists
of operations opa of arity |JβK| for each operation symbol op : α _ β and each a ∈ JαK. As
β is an arity signature type, JβK is a countable set, hence each operation has a countable
arity.
Next, for each well-formed template
Γ | z1 : α1 , . . . , zn : αn ⊢ T
and each c ∈ JΓK, we get a Tω term Z ′ : T c , where the context Z ′ consists of variables zia
for each 1 ≤ i ≤ n and each a ∈ Jαi K. Since all the αi are again arity signature types, the
sets Jαi K are countable, and so Z has countably many variables. The term T c is defined
recursively by:
JV K(c)

(zi (V ))c = zi

(match V with hx, yi 7→ T )c = T hc,pr1 (JV K(c)),pr2 (JV K(c))i
hc,ai

(match V with {ℓ(xℓ ) 7→ Tℓ }ℓ∈L )c = Tℓ′

(JV K(c) = inℓ′ (a))

(opV (x : β. T ))c = opJV K(c) (T hc,bi )b∈JβK
We then take Tω to be the equational theory generated by all equations Z ′ ⊢ T1c = T2c ,
where Γ | Z ⊢ T1 = T2 is a T equation and c ∈ JΓK. It is not difficult to see that the
category of models of Tω is equivalent to ModT , with the equivalence being consistent with
the forgetful functors; the result follows.
The left adjoint F is called the free model functor ; for a set A, the model F A is called the
free model over A; and for a map f : A → U M, the adjoint homomorphism f †M : F A ⊸ M
is called the homomorphism induced by f . We write ηA : A → F A for the unit, as usual.
4.3. Interpreting values and computations. We assume given a signature (so that
value and computation terms are determined), an effect theory T over that signature, and
an interpretation of the effect theory (so that the category of models, etc., is determined).
We can then interpret value types A by sets JAK and computation types C by models
JCK of the given effect theory T . Value types are interpreted in the same way as signature
types, except for U C, which is interpreted as the carrier of JCK. The computation type F A
is interpreted by the free model on JAK. Products of computation types are interpreted by
product models and function types are interpreted by exponent models. These are defined
as follows:
Definition 4.4.
Q For any family of models Mℓ , where
Q ℓ ranges over the index set L, the
product model ℓ∈L Mℓ is the model with carrier ℓ∈L |Mℓ | and component-wise defined

HANDLING ALGEBRAIC EFFECTS

23

operations. For any model M and any set A, the exponent model MA is the model with
carrier |M|A and pointwise defined operations.
Contexts are again interpreted component-wise, with Γ = x1 : A1 , . . . , xm : Am being
interpreted by JΓK =def JA1 K × · · · × JAm K, and K = k1 : β1 → C 1 , . . . , kn : βn → C n being
interpreted by JKK =def U JC 1 KJβ1 K × · · · × U JC n KJβn K .
We would like to interpret well-typed value terms Γ | K ⊢ V : A by maps of the form
JΓ | K ⊢ V : AK : JΓK × JKK → JAK
well-typed computation terms Γ | K ⊢ M : C by maps of the form
JΓ | K ⊢ M : CK : JΓK × JKK → U JCK
and well-typed handler terms Γ | K ⊢ H : C handler by maps of the form
Y
JαK × U JCKJβK → U JCK
JΓ | K ⊢ H : C handlerK : JΓK × JKK →
op : α_β

such that, for every c ∈ JΓK × JKK, the set U JCK, together with the operations prop (JHK(c)),
forms a model of T .
However, as discussed informally above, not all handlers receive an interpretation. As
handler terms occur in computation terms and computation terms occur in value terms,
computation terms and value terms may also not receive an interpretation. So, instead, we
interpret well-typed value terms Γ | K ⊢ V : A by partial maps
JΓ | K ⊢ V : AK : JΓK × JKK ⇀ JAK
on JΓK × JKK, and similarly for computation and handler terms.
Fix contexts Γ = x1 : A1 , . . . , xm : Am and K = k1 : β1 → C 1 , . . . , kn : βn → C n . Value
terms are interpreted as follows:
JΓ | K ⊢ xi : Ai K(a, b) ≃ pri (a) (1 ≤ i ≤ m)
JΓ | K ⊢ f(V ) : βK(c) ≃ JfK(JV K(c))

(f : α → β)

JΓ | K ⊢ hi : 1K(c) ≃ ∗
JΓ | K ⊢ hV, W i : A × BK(c) ≃ hJV K(c), JW K(c)i
P
JΓ | K ⊢ ℓ(V ) : ℓ∈L Aℓ K(c) ≃ inℓ (JV K(c))
JΓ | K ⊢ thunk M : U CK(c) ≃ JM K(c)

In the above, we have used Kleene equality e ≃ e′ which holds if either both the expressions
e and e′ are defined and equal, or both are undefined. Further, typing judgements are
abbreviated
Pon the right-hand side, ∗ is the unique element of the one-element set 1 and
inℓ : Aℓ → ℓ∈L Aℓ is the ℓ-th injection into a disjoint sum.

24

G. D. PLOTKIN AND M. PRETNAR

Next, computation terms, other than the handling construct (for which see below) are
interpreted as follows:
JΓ | K ⊢ match V with hx, yi 7→ M : CK(a, b)
(
JM K(ha, pr1 (JV K(a, b)), pr2 (JV K(a, b))i, b)
≃
undefined

(if ∀x ∈ JAK, y ∈ JBK. JM K(ha, x, yi, b) ↓)
(otherwise)

(where Γ | K ⊢ V : A × B and Γ, x : A, y : B | K ⊢ M : C)
JΓ | K ⊢ match V with {ℓ(xℓ ) 7→ Mℓ }ℓ∈L : CK(c)
(
JMℓ (ha, xi, b)K (if JV K(a, b) ≃ ℓ(x) and ∀ℓ′ ∈ L, xℓ′ ∈ JAℓ′ K. JMℓ′ K(ha, xℓ′ i, b) ↓)
≃
undefined
(otherwise)
P
(where Γ | K ⊢ V : ℓ∈L Aℓ and Γ, xℓ : Aℓ | K ⊢ Mℓ : C, for ℓ ∈ L)

JΓ | K ⊢ force V : CK(c) ≃ JV K(c)

JΓ | K ⊢ return V : F AK(c) ≃ ηA (JV K(c))
JΓ | K ⊢ M to x : A. N : CK(a, b)
(
U (JN K(ha, −i, b)†JC K )(JM K(a, b)) (if ∀x ∈ JAK. JN K(ha, xi, b) ↓)
≃
undefined
(otherwise)
Q
JΓ | K ⊢ hMℓ iℓ∈L : ℓ∈L C ℓ K(c) ≃ hJMℓ K(c)iℓ∈L
JΓ | K ⊢ prjℓ M : C ℓ K(c) ≃ prℓ (JM K(c))

JΓ | K ⊢ λx : A. M : A → CK(a, b)
(
JM K(ha, −i, b) (if ∀x ∈ JAK. JM K(ha, xi, b) ↓)
≃
undefined
(otherwise)
JΓ | K ⊢ M V : CK(c) ≃ JM K(c)(JV K(c))
JΓ | K ⊢ opV (x : β. M ) : CK(a, b)
(
opJCK (JV K(a, b), JM K(ha, −i, b))
≃
undefined

(if ∀x ∈ JβK. JM K(ha, xi, b) ↓)
(otherwise)

JΓ | K ⊢ kj (V ) : C i K(a, b) ≃ prj (b)(JV K(a, b))

(1 ≤ j ≤ n)

In the above, we have used existence assertions e ↓ which hold if, and only if, the expression e
is defined. Typing judgements are again abbreviated on the right-hand side and we used
the evident tupling and projections associated to labelled products.
Consider a handler Γ | K ⊢ H : C handler where
H = {opx : α (k : β → C) 7→ Mop }op : α_β
The interpretations of the handling terms Mop in H yield partial maps
JΓ, x : α | K, k : β → C ⊢ Mop : CK : (JΓK × JαK) × (JKK × U JCKJβK ) ⇀ U JCK

HANDLING ALGEBRAIC EFFECTS

25

and by suitable rearrangement and transposition, one obtains (total) maps
opH : JΓK × JKK → (JαK × U JCKJβK ⇀ U JCK)
Hence, for any c ∈ JΓK × JKK, we obtain partial maps opH (c) on U JCK.
Definition 4.5. A handler Γ | K ⊢ H : C handler is correct at c if the opH (c) are all total
and the set U JCK together with the opH (c) forms a model of T . The handler is correct if
it is correct at all c.
We can then give the interpretation of handlers:
(
hopH (c)iop
(if Γ | K ⊢ H : C handler is correct at c)
JΓ | K ⊢ H : C handlerK(c) ≃
undefined
(otherwise)
and the interpretation of the handling construct follows the lines discussed informally above:
JΓ | K ⊢ M handled with H to x : A. N : CK(a, b)

 U (JN K(ha, −i, b)†hU JC K,JHK(a,b)i )(JM K(a, b)) (∀x ∈ JAK. JN K(ha, xi, b) ↓
≃
and H is correct at ha, bi)

undefined
(otherwise)

The existence conditions adopted above for the existence of term denotations are quite
strict. For example, in the case of the first matching construct one might instead have
written:
JΓ | K ⊢ match V with hx, yi 7→ M : CK(a, b) ≃ JM K(ha, pr1 (JV K(a, b)), pr2 (JV K(a, b))i, b)
and there are similar alternatives for terms of any of the forms matchV with{ℓ(xℓ ) 7→ Mℓ }ℓ∈L
or M to x : A. N or M handled with H to x : A. N . Our choices followed the principle that
the denotation of a term should exist if, and only, that of all its subterms exist (taking due
account of variable binding occurrences).
The correctness of handlers is clearly of central concern. If the effect theory is empty,
then any handler is correct, but, in general — and unsurprisingly — correctness is undecidable. Indeed, as will be discussed in Section 6, even the decidability of the correctness of
very simple handlers is a Π2 -complete problem.
Remark 4.6. All the handlers, given in Examples 2.3 and Section 3 are correct. In particular, the exception handler and the stream redirection handlers are trivially correct as the
corresponding effect theories are empty. Also, the CCS relabelling and restriction handlers
are correct for both the weak and the strong bisimulation theories.
Both the rollback handlers are also correct in the presence of destructive exceptions,
given in Examples 4.1. The standard exception handler, however, is not correct for destructive exceptions, as it intercepts an exception and provides a replacement computation
instead, but does not correct any modifications made to the state. In particular, the handler
does not respect the equation
setl,x (raisee ()) = raisee ()
Another possible approach that may well be worth investigating to giving our language
a denotational semantics would be to consider only terms that are guaranteed to receive an
interpretation under suitable assumptions. One could introduce conditional judgements of
the form Γ | K | Φ ⊢ V : A (and similarly for computations and handlers), where Φ is a list
of universally quantified equations guaranteeing that handlers in V respect the equations of

26

G. D. PLOTKIN AND M. PRETNAR

the effect theory. One would also have a logic for establishing the assertions (the logic for
algebraic effects of [20] should be helpful here). Thus the typing judgement and the logic
would be integrated in a way somewhat reminiscent of Martin-Löf type theory.
5. Reasoning about handlers
The semantics we have just given allows us to reason about handlers. We are interested in
two questions in particular: which computations are equal, and which handlers are correct?
We content ourselves in this section with some initial observations, and do not attempt to
provide a full-fledged logic for algebraic effects and handlers.
We fix a signature, and an effect theory T and its interpretation, and consider as
well-formed formulas Γ | K ⊢ ϕ those that can be built up from atomic formulas by the
usual boolean connectives and universal and existential quantification over value types, e.g.,
∀x : A. ϕ, and continuations, e.g., ∀k : α → C. ϕ. As atomic formulas we take existence
(or definedness) and Kleene equality assertions for value terms, V ↓ and V ≃ W (with
evident well-formedness conditions), and for computation and handler terms. In the case
of a handler H the existence assertion H ↓ can equivalently be understood as that of the
correctness of H. There is a convenient “Kleene inequation” V . W , which abbreviates
V ↓ ⇒ V ≃ W (and similarly for computation and handler terms).
There is an evident inductively defined satisfaction relation c |=Γ|K ϕ for c ∈ JΓK × JKK
and ϕ well-formed relative to Γ and K. In particular c |=Γ|K V ↓ holds if, and only if,
JV K(c) ↓ and c |=Γ|K V ≃ W holds if, and only if, JV K(c) ≃ JW K(c), and similarly for
computation and handler terms. We say that |=Γ|K ϕ holds if, and only if c |=Γ|K ϕ holds
for all c ∈ JΓK × JKK; below we generally just say that ϕ holds, and the intended contexts
Γ and K will be clear.
We first consider equations. Versions of Levy’s call-by-push-value equations [9] hold.
For example we have a Kleene β-inequality for the sequencing construct:
return x to x : A. M . M
and a Kleene η-equality for functions:
λx : A. M x ≃ M
Next, we have equations that describe the component-wise and pointwise behaviour of
operations on product and function types, respectively:
Q
opV (x : α. hMℓ iℓ∈L ) ≃ hopV (x : α. Mℓ )iℓ∈L : ℓ∈L C ℓ
opV (x : α. λy : A. M ) ≃ λy : A. opV (x : α. M ) : A → C

We also have an equation giving the commutativity between operations and sequencing:
opV (x : α. M ) to y : A. N ≃ opV (x : α. M to y : A. N ) : C
This equation holds as sequencing is defined using the homomorphism induced by the universality of the free model, thus it maps an operation on F A to an operation on C. The
equations given by Levy [9] for two specific operations: printing and divergence (divergence
is considered in Section 7), are instances of the above three equations.
Further equations are inherited from from the effect theory T . Given a a template
x1 : α1 , . . . , xm : αm | z1 : β1 , . . . , zn : βn ⊢ T

HANDLING ALGEBRAIC EFFECTS

27

and distinct continuation variables k1 , . . . , kn we write T [k1 /z1 , . . . , kn /zn ] for the computation term obtained by replacing each occurrence of a zi in T by one of the corresponding ki .
If Γ contains the type assignments x1 : α1 , . . . , xm : αm and K contains the type assignments
k1 : β1 → C, . . . , kn : βn → C then Γ | K ⊢ T [k1 /z1 , . . . , kn /zn ] : C holds. We then have that
T1 [k1 /z1 , . . . , kn /zn ] ≃ T2 [k1 /z1 , . . . , kn /zn ]
holds for every equation
x1 : α1 , . . . , xm : αm | z1 : β1 , . . . , zn : βn ⊢ T1 = T2
in T and for every type assignment k1 : β1 → C, . . . , kn : βn → C.
We next give two Kleene inequations for the handling construct that state the universal
properties of the induced homomorphism: it extends the inducing map on values, and it
acts homomorphically on operations. For any handler H = {opy (k) 7→ Mop }op : α_β , the
inequations are:
return x handled with H to x : A. N . N
opy (x′ : β. M ) handled with H to x : A. N . Mop [x′ : β. M handled with H to x : A. N/k]
where substitutions of the form x′ : β. M ′ /k replace each occurrence of a computation k(V )
by M ′ [V /x′ ] — recall that continuation variables always appear only in the form k(V ).
As mentioned in Section 2.3, we have:
M to x : A. N ≃ M handled with {} to x : A. N
stating that sequencing is equivalent to the special case of handling in which all operations
are handled by themselves. One can then observe that (given the existence assertions
below) the two handler inequations generalise the formulas given above for the sequencing
construct, viz. the β-inequality and the commutativity of operations and sequencing.
There are other equations for exception handlers, given by Benton and Kennedy [2],
and Levy [10], and one would wish to generalise these to our general handlers. It turns out
that these equations fail for general handlers, but do hold for particular classes of handlers,
see: [22]. We do not consider this issue further here.
We next consider existence assertions. They all spell out the conditions for term interpretations to exist. For example the following hold:
return V ↓ ⇔ V ↓
M to x : A. N ↓ ⇔ M ↓ ∧ ∀x : A. N ↓
λx : A. M ↓ ⇔ ∀x : A. M ↓
opV (x : α. M ) ↓ ⇔ V ↓ ∧ ∀x : α. M ↓
Turning to handler existence, or correctness, we first need to be able to replace operations in templates by their corresponding definitions in handlers. So, let us consider a
handler Γ | K ⊢ H : C handler, where H is {opx : α (k : β → C) 7→ Mop }op : α_β , and a template variable context Z. Let K ′ be the continuation context with a continuation variable
kz : α → C for each template variable z : α ∈ Z. Then, for every template term Γ′ | Z ⊢ T

28

G. D. PLOTKIN AND M. PRETNAR

we recursively define a computation term Γ, Γ′ | K, K ′ ⊢ T H : C by:
z(V )H = kz (V )
(match V with hx1 , x2 i 7→ T )H = match V with hx1 , x2 i 7→ T H
(match V with {ℓ(xℓ ) 7→ Tℓ }ℓ∈L )H = match V with {ℓ(xℓ ) 7→ TℓH }ℓ∈L
opV (y : β. T )H = Mop [V /x, y : β. T H /k]
The following then holds:
^
^
H↓ ⇔
{∀x : α. Mop ↓ | op : α _ β} ∧ {T1H ≃ T2H | Γ′ | Z ⊢ T1 = T2 ∈ T }

asserting that a handler is correct when its operations are defined and respect the equations
of the effect theory. In particular, {} ↓ holds, where {} is the empty handler, the one defining
all operations by themselves. Regarding the handling construct itself, the following holds:
M handled with H to x : A. N ↓ ⇔ M ↓ ∧ H ↓ ∧ ∀x : A. N ↓
6. Deciding handler correctness

The decidability of handler correctness is an interesting question and one potentially pertinent for compiler writers. We now give some results on the decidability of some natural
classes of handlers; their proofs are given in Appendix A.
Definition 6.1. A handler Γ | K ⊢ H : C handler over a given signature is simple if
• up to reordering, Γ has the form
x1 : α1 , . . . , xm : αm , f1 : U (β1 → C), . . . , fn : U (βn → C)
• up to reordering, K has the form
k1′ : β1′ → C, . . . , kp′ : βp′ → C
and
• for each op : α _ β, there is a template
x1 : α1 , . . . , xm : αm , x : α | z1 : β1 , . . . , zn : βn , z1′ : β1′ , . . . , zp′ : βp′ , z : β ⊢ Top
such that the handling term
Γ, x : α | K, k : β → C ⊢ Mop : C
is obtained by the substitution of Top that replaces each xi by itself, x by itself, each zj
by (yj : βj . (force fj )yj ), each zl′ by (yl′ : βl′ . kl′ (yl′ )), and z by (y : β. k(y)).
In essence, simple handlers define handling computations in terms of algebraic constructs
only. The temporary-state handler, the CCS relabelling and restriction handlers, and stream
redirection handlers are all simple; none of the parameter-passing handlers are simple as
they all contain lambda abstractions in their handling terms. The exception handler
{raisey : exc (k : 0 → C) 7→ match y with {e(z) 7→ Ne }e∈exc }
is also not simple, as computation terms Ne may be arbitrary. One can instead use the
simple handler
f : U (exc → C) ⊢ {raisee : exc (k : 0 → C) 7→ (force f ) e}

HANDLING ALGEBRAIC EFFECTS

29

Then, letting f be the thunk of
λy : exc. match y with {e(z) 7→ Ne }e∈exc
one obtains exactly the same behaviour.
A signature is simple if it has no base types or function symbols. In that case there is
a unique interpretation, the trivial one, and we will omit mention of it. Simple signatures
and theories are equivalent to ones in which all operation symbols are n-ary for some n.
The signatures given above for exceptions (over a finite set), read-only state, I/O, and
nondeterminism are all simple, but none of the others are.
Theorem 6.2. The problem of deciding, given a simple signature, effect theory, and closed
simple handler ⊢ H : F 0 handler over the given signature, whether the handler is correct,
is Π2 -complete.
The polymorphic nature of template variables means that a template can define a whole
family of handlers, one for each computation type. This leads one to the definition of a
uniformly simple family of handlers:
Definition 6.3. A family of handlers {ΓC | KC ⊢ HC : C handler}C over a given signature,
where C ranges over all computation types, is uniformly simple if
• up to reordering, ΓC is
x1 : α1 , . . . , xm : αm , f1 : U (β1 → C), . . . , fn : U (βn → C)
• up to reordering, KC is

k1′ : β1′ → C, . . . , kp′ : βp′ → C

and
• for each op : α _ β, there is a template
x1 : α1 , . . . , xm : αm , x : α | z1 : β1 , . . . , zn : βn , z1′ : β1′ , . . . , zp′ : βp′ , z : β ⊢ Top
such that for each computation type C, the handling term
ΓC , x : α | KC , k : β → C ⊢ Mop : C
is obtained by the substitution of Top that replaces each xi by itself, x by itself, each zj
by (yj : βj . (force fj )yj ), each zl′ by (yl′ : βl′ . kl′ (yl′ )), and z by (y : β. k(y)).
If a family of handlers is uniformly simple then, as is evident, any member of the family
is simple. Conversely, because of the polymorphic nature of templates, any simple handler
can be generalised to obtain a uniformly simple one. Of the simple handlers given above,
the temporary-state handler, the stream redirection handlers, and the alternative exception
handler are also uniformly simple; the CCS relabelling and restriction handlers are not as
we define them only for the computation type F 0.
Note that a uniformly simple family of handlers is determined by the various variables,
types and template terms discussed in the above definition. As there are finitely many of
these altogether, uniformly simple families of handlers can be finitely presented and so it is
proper to ask decidability questions about them.
Definition 6.4. A family of handlers {ΓC | KC ⊢ HC : C handler}C over a given signature,
where C ranges over all computation types, is correct if each handler in the family is correct.

30

G. D. PLOTKIN AND M. PRETNAR

Since a uniformly simple family of handlers cannot use properties of a specific computation type, it cannot be as contrived as an arbitrary family of handlers; we may therefore
expect it to be easier to decide its correctness. As we now see, correctness can become
semidecidable:
Theorem 6.5. The problem of deciding, given a simple signature, effect theory, and a
uniformly simple family of closed handlers {⊢ HC : C handler}C over the given signature,
whether the family of handlers is correct, is Σ1 -complete.
Effect theories with a simple signature correspond (see the proof of Proposition 4.3) to
ordinary finite equational theories, i.e., those with finitely many finitary function symbols
and finitely many axioms. Consequently notions such as decidability can be transferred to
them. (All the above examples of simple signatures and theories are decidable in this sense.)
With this understanding, we have:
Theorem 6.6. The problem of deciding, given a simple signature, decidable effect theory,
and a uniformly simple family of closed handlers {⊢ HC : C handler}C over the given
signature, whether the family of handlers is correct, is decidable.
7. Recursion
We now sketch some changes to the syntax and semantics that enable the incorporation of
recursion. We begin with syntax. Signatures are as before except that we always assume an
additional operation symbol div : 1 _ 0 representing nontermination. To provide a recursion
facility, we follow [9] and add a fixed-point constructor rec x : U C. M , typed as follows:
Γ, x : U C | K ⊢ M : C
Γ | K ⊢ rec x : U C. M : C
Turning to semantics, templates are defined as before, but effect theories now consist
of inequations Γ | Z ⊢ T1 ≤ T2 rather than equations. We always assume that the effect
theory contains the inequation · | z : 1 ⊢ div() ≤ z, stating that div is the least element. As
examples one can take those of Section 4 with this additional inequation, reading equations
as conjunctions of two inequations; see [7] for further examples.
In order to interpret recursion, we move, as remarked above, from the category of
sets to ωCpo, the category of ω-cpos and continuous functions. First we assume given an
assignment of ω-cpos JbK to base types b, such that JbK is flat and countable in the case
that b is an arity base type; this yields interpretations of signature types α as ω-cpos JαK,
which are flat and countable in the case of arity signature types. (A ω-cpo is flat if no two
distinct elements are comparable.) An interpretation of an effect theory then consists of
such an assignment and an assignment JfK : JαK → JβK of continuous functions to function
symbols f : α → β, and well-formed base values Γ ⊢ V : α are interpreted as continuous
functions JV K : JΓK → JαK much as before.
Similarly, given an ω-cpo |M| together with operations, that is, continuous functions
opM : JαK × |M|JβK → |M|, for each operation symbol op : α _ β, well-formed templates
Γ | Z ⊢ T can be interpreted as continuous functions JT K : JΓK × JZK → |M|.
With that, one can define models M of effect theories T as ω-cpos together with
operations for each operation symbol such that such that JT1 K ≤ JT2 K holds for all the
inequations Γ | Z ⊢ T1 ≤ T2 in T . Defining homomorphisms in the evident way, one obtains

HANDLING ALGEBRAIC EFFECTS

31

a category of models ModT , equipped with a forgetful functor U : ModT → ωCpo. As we
discuss below, the forgetful functor has a left adjoint F : ωCpo → ModT . Both functors
have continuous strengths and are locally continuous, by which is meant that they act
continuously on the hom ω-cpos. It is also important to note that the unique continuous
homomorphism f †M : F A ⊸ M induced by a continuous map f : A → U M is itself a
continuous function of f . As effect theories assume least elements, carriers of models are
pointed ω-cpos (i.e., ω-cpos with a least element) and homomorphisms are strict continuous
functions (i.e., continuous functions preserving least elements).
The monads U F obtained in this way are the standard ones that occur in semantics. For
example, the monad obtained from the theory for exceptions together with a least element
is P 7→ (P + exc)⊥ , where the lifting Q⊥ is the ω-cpo obtained from Q by adding a new
least element; the monad for nondeterminism, together with a least element, is P 7→ P(P⊥ ),
where P is the convex powerdomain monad; and the monad for state, together with a least
element and inequations sating that the state operations are strict, is P 7→ (S ×P )S⊥ . See [7]
for further discussion and references.
To show the existence of the free model functor and its properties, one can proceed
along related lines to before. One again has families opa of operations of countable arity,
but now parameterised by elements a of given ω-cpos P , and one considers inequations
instead of equations between the resulting infinitary terms. Operations are interpreted by
continuous functions varying continuously over the parameter ω-cpos; this corresponds to
the fact that one is working with continuous functions opM : JαK × |M|JβK → |M| with JαK
an ω-cpo.
One thereby obtains continuously parameterised countably infinitary inequational theories; these can be shown to be equivalent to the discrete countable Lawvere ωCpo-theories:
see [8], and see too [15] for further discussion of parameterised equational logic. The existence of the free model functor and its continuity properties follow from the fact that ωCpo
is locally countably presentable as a cartesian closed category (see [8]).
Value types are now interpreted by ω-cpos and computation types are interpreted by
models whose carriers are pointed ω-cpos, again making use of product and exponentiation
models. Values, computations (including the handling construct) and handlers are interpreted by partial maps analogously to before, except that as well as requiring functions be
total, one requires that they are also continuous.
The fixed-point constructor is interpreted using the usual least fixed-point interpretation:
JΓ | K ⊢ rec x : U C. M : CK(a, b)

µx :JU CK. JM K(ha, xi, b) (∀x ∈ JU CK. JM K(ha, xi, b) ↓)
≃
undefined
(otherwise)

where, as usual, µx : P. f (x) is the least fixed-point of a continuous function f on a pointed
ω-cpo P .
One can show by structural induction that the sets of elements of JΓK × JKK at which
the denotations JΓ | K ⊢ V : AK of value terms exist form a sub-cpo of JΓK × JKK and that
the denotations are continuous when restricted to that sub-cpo, and, further, that the same
holds for computation terms and handlers. (One may then observe that, as a consequence,
the above continuity requirement is redundant.)

32

G. D. PLOTKIN AND M. PRETNAR

Correct handlers cannot redefine div as the theory of div fixes it uniquely. The handlers
given in the various examples above, as detailed in Remark 4.6, remain correct in the
presence of recursion, understanding them as defining div by itself (and with the addition
of the inequation stating that div is the least element to the corresponding theories).
Conclusion
The current work opens some immediate questions. The most important is how to simultaneously handle two computations to describe parallel combinators, e.g., that of CCS or the
Unix pipe combinator. Understanding this would bring parallelism within the ambit of the
algebraic theory of effects.
Next, the logical ideas of Section 5 should be worked out more fully and merged with
the general logic for algebraic effects [20, 22]. There is a close correspondence between the
handling construct and the free model principle in the logic, which should be examined in
detail.
It would be worthwhile to extend the results of Section 6 further, whether to wider
classes of signatures, handlers, or theories. One would also like to have analogous results
for (the interpretation over) ω-cpos.
Only correct handlers can be interpreted, but, as we have seen, obtaining mechanisms
that ensure correctness is hard. One option would be to drop equations altogether, when
handlers are interpreted as models of absolutely free theories (i.e., those with no equations).
This would be correctly implementable if one removed the connection with the equalities
expected for the real effects between handled computations.
More routinely, perhaps, the work done on combinations of effects in [7] should be extended to combinations of handlers, and there should be a general operational semantics [16]
which includes that of Benton and Kennedy [2].
In so far as possible, one would like to work in a general categorical setting as regards
both the denotational semantics and the logic. Considering only the denotational semantics,
it may be possible to generalise the above semantics to work over any category V that is
locally countably presentable as a cartesian closed category. Presumably one would use a
more abstract notion of the effect theories of Section 4 above, based on Lawvere V-theories
(see [19]) or, perhaps, just discrete Lawvere V-theories [8]. As one needs to deal with
partiality when handlers are incorrect, one would require a suitable factorisation system.
Finally, one should develop the programming language aspects further. For example,
while call-by-push-value serves well as a fundamental calculus and as an intermediate language, it may be more realistic, or at least more in accordance with current practice, to
find a formulation of handlers in a call-by-value context (and call-by-name also has some
interest). It would also be important to increase ease of programming, for example by allowing abstraction on handlers, rather than, as above, making use of their global variables;
one would also like syntactic support for parametric handlers; some ideas along these lines
can be found in [21]. In general, perhaps handlers could become more first-class entities.
Acknowledgments
We thank Andrej Bauer, Andrzej Filinski, Ohad Kammar, Paul Levy, John Power, Mojca Pretnar, Alex Simpson, and an anonymous referee for their insightful comments and
support.

HANDLING ALGEBRAIC EFFECTS

33

References
[1] Nick Benton, John Hughes, and Eugenio Moggi. Monads and effects. In APPSEM 2000, volume 2395
of Lecture Notes in Computer Science, pages 42–122, 2000.
[2] Nick Benton and Andrew Kennedy. Exceptional syntax. Journal of Functional Programming, 11(4):395–
410, 2001.
[3] Andrzej Filinski. Representing layered monads. In 26th Symposium on Principles of Programming Languages, pages 175–188, 1999.
[4] Cormac Flanagan, Amr Sabry, Bruce F. Duba, and Matthias Felleisen. The essence of compiling with
continuations. In Conference on Programming Language Design and Implementation, pages 237–247,
1993.
[5] George A. Grätzer. Universal Algebra. Springer, 2nd edition, 1979.
[6] Martin Hyland, Paul Blain Levy, Gordon D. Plotkin, and John Power. Combining algebraic effects with
continuations. Theoretical Computer Science, 375(1-3):20–40, 2007.
[7] Martin Hyland, Gordon D. Plotkin, and John Power. Combining effects: Sum and tensor. Theoretical
Computer Science, 357(1-3):70–99, 2006.
[8] Martin Hyland and John Power. Discrete Lawvere theories and computational effects. Theor. Comput.
Sci., 366(1-2):144–162, 2006.
[9] Paul Blain Levy. Call-by-push-value: Decomposing call-by-value and call-by-name. Higher-Order and
Symbolic Computation, 19(4):377–414, 2006.
[10] Paul Blain Levy. Monads and adjunctions for global exceptions. Electronic Notes in Theoretical Computer Science, 158:261–287, 2006.
[11] Paul-André Melliès. Segal condition meets computational effects. In LICS, pages 150–159. IEEE Computer Society, 2010.
[12] Robin Milner. Communication and Concurrency. International Series in Computer Science. Prentice
Hall, 1989.
[13] Eugenio Moggi. Notions of computation and monads. Information And Computation, 93(1):55–92, 1991.
[14] Simon L. Peyton Jones. Haskell 98. Journal of Functional Programming, 13(1):0–255, 2003.
[15] Gordon D. Plotkin. Some varieties of equational logic. In Essays Dedicated to Joseph A. Goguen, volume
4060 of Lecture Notes in Computer Science, pages 150–156, 2006.
[16] Gordon D. Plotkin and John Power. Adequacy for algebraic effects. In 4th International Conference
on Foundations of Software Science and Computation Structures, volume 2030 of Lecture Notes in
Computer Science, pages 1–24, 2001.
[17] Gordon D. Plotkin and John Power. Notions of computation determine monads. In 5th International
Conference on Foundations of Software Science and Computation Structures, volume 2303 of Lecture
Notes in Computer Science, pages 342–356, 2002.
[18] Gordon D. Plotkin and John Power. Algebraic operations and generic effects. Applied Categorical Structures, 11(1):69–94, 2003.
[19] Gordon D. Plotkin and John Power. Computational effects and operations: An overview. Electronic
Notes in Theoretical Computer Science, 73:149–163, 2004.
[20] Gordon D. Plotkin and Matija Pretnar. A logic for algebraic effects. In 23rd Symposium on Logic in
Computer Science, pages 118–129, 2008.
[21] Gordon D. Plotkin and Matija Pretnar. Handlers of algebraic effects. In ESOP 2009, volume 5502 of
Lecture Notes in Computer Science, pages 80–94, 2009.
[22] Matija Pretnar. The Logic and Handling of Algebraic Effects. PhD thesis, School of Informatics, University of Edinburgh, 2010.
[23] Terese. Term Rewriting systems. Cambridge University Press, 2003.
[24] Rob J. van Glabbeek and Gordon D. Plotkin. On CSP and the algebraic theory of effects. In Reflections
on the work of C.A.R.Hoare, pages 333–369. Springer, 2010.

Appendix A. Decidability of handler correctness
We prove our results on handler correctness by reducing correctness to related questions in
equational logic. An interpretation of an equational theory T in another T ′ is given by an
assignment of a T ′ -term with free variables included in x1 , . . . , xn to every function symbol

34

G. D. PLOTKIN AND M. PRETNAR

of arity n of T . This results in an interpretation of every T -term by a T ′ -term, and so in
an interpretation of every T -equation by a T ′ -equation.
Lemma A.1. Given a finitary equational theory with finite signature and finitely many
axioms, and an interpretation of this theory in itself, it is a Π2 -complete problem to decide
whether the interpretation holds in the initial model of the theory.
Proof. The problem is clearly in Π2 as an axiom holds in the initial model of such an
equational theory if, and only if, there exists a proof of all its closed instances. Conversely,
take a Π2 sentence of Peano Arithmetic. Without loss of generality, we can assume this to
be of the form ∀x. ∃y. ϕ(x, y), where ϕ(x, y) defines a primitive recursive relation R(m, n).
Changing to ∀x. ∃y. ∃y ′ ≤ y. ϕ(x, y ′ ) if necessary, we can assume that if R(m, n) holds and
n ≤ n′ , then R(m, n′ ) holds too. We now define a finitary equational theory T with
finite signature and finitely many axioms, and an interpretation of it in itself, such that
∀x. ∃y. ϕ(x, y) is true if, and only if, the interpretation of the axioms holds in the initial
model of the theory.
Let f1 , . . . , fk be a sequence of primitive recursive functions, including a function (coding) disjunction, each definable in terms of the previous ones by composition or primitive
recursion, such that fk is the characteristic function of R. Take a constant symbol zero
and a unary function symbol succ. Next, for all the primitive recursive functions fi take: a
function symbol fi of the same arity, and axioms corresponding to the primitive recursive
definition of fi , written using zero, succ, and the fj with j < i.
Next, take a binary function symbol try and a unary function symbol exists, together
with the following two axioms:
try(x, y) = fk (x, y) ∨ try(x, succ(y))
exists(x) = try(x, 0)
where ∨ is the function symbol corresponding to disjunction and n is the n-th numeral,
defined using zero and succ. All this defines the theory T .
Finally, take the interpretation of the theory T in itself where each function symbol f
other than exists is interpreted by itself — more precisely, the term f(x1 , . . . , xn ) — and
exists is interpreted by the term 1. This interpretation of the axioms evidently holds in the
initial model of T if, and only if, try(t, 0) = 1 is provable for all closed terms t.
Next, assume that the sentence ∀x. ∃y. ϕ(x, y) is true and choose m. Then there exists
an n such that fk (m, n) = 1 is provable in T . The following sequence of equations is then
provable in T :
try(m, 0) = fk (m, 0) ∨ try(m, 1)
= fk (m, 0) ∨ fk (m, 1) ∨ try(m, 2)
..
.
= fk (m, 0) ∨ · · · ∨ fk (m, n) ∨ try(m, n + 1)
=1
(with the last holding as fk (m, n) = 1 is provable). More generally, as fk (m, n′ ) = 1 whenever
n′ ≥ n, a similar argument shows that try(m, n) = 1 is provable for any m and n. It follows
that all closed terms of T are provably equal to numerals. Therefore, as we have also shown
that try(m, 0) = 1 is provable for all m, the interpretation of the axioms holds in the initial
model.

HANDLING ALGEBRAIC EFFECTS

35

Conversely, assume that try(t, 0) = 1 is provable in T for all closed terms t. Then,
in particular, try(m, 0) = 1 is provable in T for all m. We analyse proofs in T via the
first-order term rewriting system obtained by orienting all the axioms of T from left to
right. As the reduction rules are left-linear and there are no overlaps between them, we
have a Church-Rosser system [23]. Hence, for any two terms t and u, the equation t = u is
provable if, and only if, t and u reduce to a common term.
In particular, by our assumption, for every m, there is some number of steps s such that
try(m, 0) →s 1. We first observe that t ∨ u →∗ 1 if, and only if, t →∗ 1 or u →∗ 1. Using
this observation, it follows by induction on s that there exists an n such that fk (m, n) →∗ 1.
Therefore the sentence ∀x. ∃y. ϕ(x, y) is true, concluding the proof.
Proof of Theorem 6.2. Given a simple signature and theory T , following the proof of Proposition 4.3 one recursively constructs a corresponding finitary equational theory Tf with finite
signature and finitely many axioms whose models are in 1-1 correspondence with those of
the given theory. Handlers ⊢ H : F 0 handler then correspond to interpretations of Tf in
itself, and are correct if, and only if, the interpretation of Tf in itself holds in the model of
Tf corresponding to the model F J0K = JF 0K of T . As F J0K is the initial model of T (being
its free model on the empty set), that corresponding model of T is its initial model.
Conversely, given a finitary equational theory T with finite signature and finitely many
axioms, one immediately constructs a simple signature and theory Ts such that the above
construction yields back the original finitary equational theory T (up to a bijection of its
function symbols). Further, given an interpretation of T in itself one immediately constructs
a handler ⊢ H : F 0 handler to which the interpretation of T in itself corresponds.
The result then follows by combining these facts with Lemma A.1.
Lemma A.2. Given a finitary equational theory with finite signature and finitely many
axioms, and an interpretation of this theory in itself, it is a Σ1 -complete problem to decide
whether the interpretation is provable in the theory.
Proof. The proof is very similar to that of Lemma A.1. The problem is clearly in Σ1 .
Conversely, consider a Σ1 sentence of Peano Arithmetic. This can be taken, without loss of
generality, to be of the form ∃y. ϕ(y), where ϕ(y) defines a primitive recursive predicate R.
One then defines a finitary equational theory T with finite signature and finitely many
axioms, and an interpretation of it in itself, such that that ∃y. ϕ(y) is true if, and only
if, the interpretation of the axioms holds in all free models of the theory over finite sets.
The theory T is much like before, except that try is unary and exists is a constant, the
corresponding axioms are
try(y) = fk (y) ∨ try(succ(y))
exists() = try(0)
and one considers the interpretation where each function symbol other than exists is interpreted by itself and exists is interpreted by 1. This interpretation of the axioms evidently
holds in all free models of T over finite sets if, and only if, try(0) = 1 is provable.
The rest of the proof then proceeds entirely analogously to, but a little more simply
than, that of Lemma A.1.
Proof of Theorem 6.5. The proof proceeds analogously to that of Theorem 6.2 except that
one considers uniformly simple handlers {⊢ HC : C handler}C .

36

G. D. PLOTKIN AND M. PRETNAR

In particular there is, as before, a finitary equational theory Tf corresponding to any
given theory T over a given simple signature. As before, a given uniformly simple handler
{⊢ HC : C handler}C then corresponds to an interpretation of Tf in itself. The handler is
correct if that interpretation holds in all models of Tf corresponding to those of T of the
form JCK. Since the JCK include all free models of T of the form F n, this last is equivalent
to the interpretation holding in all free models of Tf over finite sets, and so to its being
provable in Tf .
Proof of Theorem 6.6. Following the proof of Theorem 6.5, we see that, given a theory
T over a given simple signature, determining the correctness of a given uniformly simple
handler {⊢ HC : C handler}C amounts to determining whether the corresponding interpretation of Tf in itself is provable in Tf . However that is decidable since Tf is.

This work is licensed under the Creative Commons Attribution-NoDerivs License. To view
a copy of this license, visit http://creativecommons.org/licenses/by-nd/2.0/ or send a
letter to Creative Commons, 171 Second St, Suite 300, San Francisco, CA 94105, USA, or
Eisenacher Strasse 2, 10777 Berlin, Germany

