Logical Methods in Computer Science
Vol. 10(4:9)2014, pp. 1–29
www.lmcs-online.org

Submitted
Published

Feb. 18, 2014
Dec. 10, 2014

AN EFFECT SYSTEM FOR ALGEBRAIC EFFECTS AND HANDLERS ∗
ANDREJ BAUER AND MATIJA PRETNAR
Faculty of Mathematics and Physics, University of Ljubljana, Slovenia
e-mail address: Andrej.Bauer@andrej.com, matija.pretnar@fmf.uni-lj.si

Abstract. We present an effect system for core Eff, a simplified variant of Eff , which is
an ML-style programming language with first-class algebraic effects and handlers. We define an expressive effect system and prove safety of operational semantics with respect to it.
Then we give a domain-theoretic denotational semantics of core Eff , using Pitts’s theory
of minimal invariant relations, and prove it adequate. We use this fact to develop tools for
finding useful contextual equivalences, including an induction principle. To demonstrate
their usefulness, we use these tools to derive the usual equations for mutable state, including a general commutativity law for computations using non-interfering references. We
have formalized the effect system, the operational semantics, and the safety theorem in
Twelf.

1. Introduction
An effect system supplements a traditional type system for a programming language with
information about which computational effects may, will, or will not happen when a piece of
code is executed. A well designed and solidly implemented effect system helps programmers
understand source code, find mistakes, as well as safely rearrange, optimize, and parallelize
code [11, 8]. As many before us [11, 24, 25, 7] we take on the task of striking just the right
balance between simplicity and expressiveness by devising an effect system for Eff [2], an
ML-style programming language with first-class algebraic effects [17, 15] and handlers [19].
Our effect system is descriptive in the sense that it provides information about possible
computational effects but it does not prescribe them. In contrast, Haskell’s monads prescribe
the possible effects by wrapping types into computational monads. In the implementation
we envision effect inference which never fails, although in some cases it may be uninformative.
Of course, typing errors are still errors.
An important feature of our effect system is non-monotonicity: it detects the fact that
a handler removes some effects. For instance, a piece of code which uses mutable state is
determined to actually be pure when wrapped by a handler that handles away lookups and
updates.
2012 ACM CCS: [Software and its engineering]: Software notations and tools—General programming
languages—Language features; [Theory of computation]: Semantics and reasoning.
Key words and phrases: algebraic effects, effect handlers, effect system.
∗
A preliminary version of this work was presented at CALCO 2013, see [3].

l

LOGICAL METHODS
IN COMPUTER SCIENCE

c
DOI:10.2168/LMCS-10(4:9)2014

CC

A. Bauer and M. Pretnar
Creative Commons

2

(1)

(2)
(3)
(4)

(5)
(6)

(7)

A. BAUER AND M. PRETNAR

Our contributions are as follows:
We define core Eff, a fragment of the language which retains the essential features of Eff ,
including first-class handlers and instances (Section 2), although we leave out dynamic
creation of new instances.
We give small-step and big-step operational semantics for core Eff and show them to
be equivalent (Section 3).
We devise an expressive effect system for core Eff and prove safety of the operational
semantics with respect to it (Section 4).
Using the standard domain-theoretic apparatus and Pitts’s theory of minimal invariant
relations [14], we provide denotational semantics for core Eff and prove an adequacy
theorem (Section 5).
We identify a set of observational equivalences and an induction principle that allow us
to reason about effectful computations (Section 6).
We demonstrate how the equivalences are used by deriving the standard equations for
state from general principles. The induction principle is used in a proof of a general commutativity law which allows us to interchange two computations that use non-interfering
references (Section 7).
We formalized core Eff , the operational semantics, the effect system, and the safety
theorem in Twelf [13] (Section 8).
2. Core Eff

The current implementation of Eff includes a number of features, such as syntactic sugar,
products, records, inductive types, type definitions, effect definitions, etc., which are inessential for a conceptual analysis. We therefore restrict attention to core Eff, a fragment of the
language described here. We refer the readers to [2] for a more thorough introduction of
how one actually programs in Eff .
In Eff all computational effects are accessed uniformly and exclusively through operations. These are a primitive concept, of which typical examples are reading and writing on
a communication channel, updating and looking up the contents of a reference, and raising
an exception. Thus, in Eff each terminating computation results either in an effect-free
value, or it calls an operation. Each operation has an associated delimited continuation,
which is a suspended computation awaiting the result of the operation.
Operations do not actually perform effects, but are just suspended computations whose
behavior is controlled by a second primitive notion, the effect handlers. These are like
exception handlers, except that an effect handler has access to the continuation of the
handled operation, and so may restart the computation after the operation is handled. With
handlers we may implement all the usual computational effects, as well as great variety
of others, such as transactional memory, non-deterministic execution strategies, stream
redirection, cooperative multi-threading, and delimited continuations. At the top level there
may be built-in handlers that provide interaction with the external environment, although
we do not consider these in core Eff .
Since Eff is geared towards practical programming, it and core Eff depart in several
respects from previous work on handlers and algebraic effects [19, 7]. First, rather than
imposing equations on handlers by a typing discipline, the programmer may write arbitrary
handlers, and then prove that a particular handler satisfies the desired equations. We
demonstrate the technique in Section 7.1, where we implement a state handler and show that

AN EFFECT SYSTEM FOR ALGEBRAIC EFFECTS AND HANDLERS

3

it satisfies the standard equations. Second, Eff uses fine-grained call-by-value evaluation
strategy [10] rather than the theoretically more desirable call-by-push-value [9] because
we found the former to be closer to programming practice as well as easier to implement.
Third, every effect has multiple instances. For example, a program may write and read
from multiple communication channels, raise different kinds of exceptions, and manipulate
multipartite state. Thus in core Eff an operation symbol op is always paired with an instance
ι to give an operation ι#op. From a theoretical point of view instances are straightforward (as
long as we do not generate them dynamically) and inessential, but are absolutely necessary
for practical programming.
2.1. Effects and types. To get things going we presume given a collection of effects
Effect E :: = exception

ref

···

which in full Eff are declared by the programmer. For each E there is a given set IE of
instances ι1 , ι2 , ι3 , . . . of E. The instances may be thought of as atomic names. In full
Eff they may be dynamically created, but to keep the semantics reasonably simple we
assume a fixed set. Additionally, with each E we associate a set of OE of operation symbols
op1 , op2 , . . . An operation symbol is associated with at most one effect.
The terms of core Eff are split into effect-free expressions and possibly effectful computations, as described in the next subsection. Consequently, the type system of core Eff
consists of pure types for expressions and dirty types for computations:
Pure type A, B :: = bool
Dirty type C, D :: = A ! ∆

nat

unit

empty

A−
→C

ER

C=
⇒D

Region R :: = {ι1 , . . . , ιn }
Dirt ∆ :: = {ι1 #op1 , . . . , ιn #opn }
A dirty type A ! ∆ is just a pure type A tagged with a finite set ∆ of operations that might be
called during evaluation. We require that any operation ι#op appearing in ∆ is well-formed
in the sense that ι ∈ IE and op ∈ OE for some effect E.
The pure types comprise the usual ground types, the function types A −
→ C, the effect
R
⇒ D. Note that the function type takes pure types
types E , and the handler types C =
to dirty ones because a function accepts a pure expression as an argument and may call
operations when evaluated. We let ! bind more strongly than −
→, so that A −
→ B ! ∆ means
A−
→ (B ! ∆). Each effect type E R is tagged with a finite set of instances R = {ι1 , . . . , ιn } ⊆
⇒ D is the
IE which tells us that the expression equals one of the instances in R. Finally, C =
type of handlers which take computations of ingoing type C to computations of outgoing
type D.
We assume that each effect E has an associated effect signature
ΣE = {op1 : Aop1 −
→ B op1 , . . . , opn : Aopn −
→ B opn }
which assigns to each operation opi ∈ OE its parameter type Aopi and result type B opi . In
full Eff the signature is part of the definition of an effect, so for instance we might have
Σref = {lookup : unit −
→ nat, update : nat −
→ unit},
Σexception = {raise : unit −
→ empty}.

4

A. BAUER AND M. PRETNAR

Note that the signature may create circularities such as
ΣE = {op : unit −
→ (unit −
→ unit ! {ι#op})}.
Consequently, the denotational semantics of types in Section 5 will involve recursive domain
equations.
2.2. Terms. The abstract syntax of terms of core Eff is as follows:
Expression e :: = x

true

0

false

succ e

()

fun x : A 7→ c

ι

h

Handler h :: = (handler val x : A 7→ cv | ocs)
(e#op x k 7→ c | ocs)

Operation cases ocs :: = nilC
Computation c :: = val e

e1 #op e2 (y. c)

if e then c1 else c2

with e handle c
absurdC e

e1 e2

(match e with 0 7→ c1 | succ x 7→ c2 )
let x = c1 in c2

let rec f x : A −
→ C = c1 in c2

In order to ensure that each term has at most one skeletal typing derivation, cf. Subsection 4.3, certain terms include typing annotations. We shall omit these when they do not
play a role. The Eff implementation does not have typing annotations because its effect
system automatically infers types and effects [22].
An expression is either a variable, a constant of ground type, a function abstraction
(note that we abstract over computations), an effect instance, or a handler. It is worth
noting that both instances and handlers are first-class values. We sometimes abbreviate
succn 0 as n. A handler consists of a single value case and multiple operation cases, which
describe how values and operations are handled, respectively. We defined operation cases
inductively as lists, which is how they are formalized in Twelf, but we also write them as
(ei #opi xi ki 7→ ci )i .
A computation is either a pure expression, an operation call, a handle construct, an
eliminator for a ground type, an application, a let binding, or a recursive function definition.
3. Operational semantics
We first describe the operational semantics informally. A computation val e is pure and
indicates a “final” result e, while an operation call e1 #op e2 (y. c) is the principal way of
triggering an effect. The instance e1 and the operation symbol op together form an operation e1 #op, its parameter is e2 , and (y. c) the delimited continuation. We do not expect
programmers to write explicit continuations, so the concrete syntax of Eff only gives access
to calls through functions of the form fun x 7→ e#op x (y. val y), known also as generic
effects [17]. In examples we shall use generic effects rather than explicit continuations, and
there we write them as e#op. A general operation call e1 #op e2 (y. c) may then be expressed
in terms of a generic effect and a let binding as let y = e1 #op e2 in c.
A binding let x = c1 in c2 is evaluated as follows:
(1) If c1 evaluates to val e then the binding evaluates as c2 with x bound to e.

AN EFFECT SYSTEM FOR ALGEBRAIC EFFECTS AND HANDLERS

5

(2) If c1 evaluates to an operation call ι#op e (y. c′1 ), then the binding evaluates to
ι#op e (y. let x = c′1 in c2 ),
where we assume that y does not occur free in c2 .
It may be helpful to think of val and let as being similar to Haskell return and do,
respectively. In ML val is invisible, while let is essentially the same as ours.
The handle construct applies a handler to a computation. If h is the handler
handler val x 7→ cv |(ιi #opi xi ki 7→ ci )i
and c is a computation, then with h handle c first evaluates c which is then handled
according to h:
(1) If c evaluates to val e, then the handle construct evaluates as cv with x bound to e.
(2) If c evaluates to ι#op e′ (y. c′ ), and ιi #opi xi ki 7→ ci is the first operation case in h for
which ι#op = ιi #opi then the handle construct evaluates to ci with xi and ki bound to
e′ and fun y 7→ with h handle c′ , respectively. We assume that y does not occur free
in h.
(3) If c evaluates to an operation call ι#op e′ (y. c′ ) which is not listed by h, then the handle
construct propagates the call and acts as if h contained the clause
ι#op x k 7→ ι#op x (y. k y).
ι#op e′ (y. with

Thus it evaluates to
h handle c′ ), where again we assume that y does
not occur free in h.
Note that the handler always wraps itself around the continuation so that subsequent operations are handled as well. A binding let x = c1 in c2 is equivalent to
with (handler val x 7→ c2 ) handle c1
so we could theoretically omit let.
3.1. Small-step semantics. The small-step operational semantics of core Eff is defined
in terms of a relation c
c′ , which intuitively means that the computation c takes a single
′
step to c . There is no operational semantics for expressions, which are just inert pieces of

6

A. BAUER AND M. PRETNAR

data. The relation

is defined inductively by the following rules:

if true then c1 else c2

c1

(match 0 with 0 7→ c1 | succ x 7→ c2 )

c1

(fun x 7→ c) e
let x = (val e) in c

c[e/x]

c[e/x]

let x = (ι#op e (y. c1 )) in c2

c′
with e handle c′

c2

(match (succ e) with 0 7→ c1 | succ x 7→ c2 )
c1
let x = c1 in c2

let rec f x = c1 in c2
c
with e handle c

if false then c1 else c2

c2 [e/x]

c′1
let x = c′1 in c2
ι#op e (y. let x = c1 in c2 )

c2 [(fun x 7→ let rec f x = c1 in c1 )/f ]

with (handler val x 7→ cv | ocs) handle (val e)

cv [e/x]

def

h = (handler val x 7→ cv | ocs)
(op : Aop −
→ B op ) ∈ ΣE
with h handle (ι#op e (y. c))
ocsι#op (e, (fun y : B op 7→ with h handle c))

In the last rule for let binding and the last rule for the handle construct variable y must
not occur free in c2 and h respectively, and it goes without saying that the substitutions
are capture avoiding. In the last rule we have an auxiliary definition of ocsι#op :
(nil)ι#op (e, κ) = ι#op e (y. κ y)
(
c[e/x, κ/k]
(ι′ #op′ x k →
7 c | ocs)ι#op (e, κ) =
ocsι#op (e, κ)

if ι#op = ι′ #op′
otherwise

In words, ocsι#op (e, κ) finds the first handler case in ocs that matches the operation ι#op
and executes it, or calls the operation again if no match is found.
Example 3.1. The non-standard state handler (recall that in examples we use generic
effects)
def

h = handler
| val x 7→ ι#update x
| ι#lookup x k 7→ k 1
| ι#update x k 7→ k ()
treats the reference ι as if its content were always 1, and updates ι with the final result of
the handled computation. This update is not handled by h because it escapes its scope. If
we use h to handle the computation
def

c = let x1 = ι#lookup () in
let x2 = ι#update x1 in
val (succ x1 )
the outcome of the first lookup is 1, which is bound to x1 , the update is ignored and finally
ι#update 2 is called. The exact reduction sequence is as follows, where we underline the

AN EFFECT SYSTEM FOR ALGEBRAIC EFFECTS AND HANDLERS

7

active parts at each step and indicate desugaring of generic effects with ≡:
with h handle
let x1 = ι#lookup () in let x2 = ι#update x1 in val (succ x1 ) ≡
with h handle
let x1 = ι#lookup()(y1 . val y1 ) in let x2 = ι#update x1 in val (succ x1 )
with h handle
ι#lookup()(y1 . let x1 = val y1 in let x2 = ι#update x1 in val (succ x1 ))
(fun y1 7→ with h handle (let x1 = val y1 in let x2 = ι#update x1 in val (succ x1 ))) 1
with h handle (let x1 = val 1 in let x2 = ι#update x1 in val (succ x1 ))
with h handle (let x2 = ι#update 1 in val 2) ≡
with h handle (let x2 = ι#update 1 (y2 . val y2 ) in val 2)
with h handle (ι#update 1 (y2 . let x2 = val y2 in val 2))
(fun y2 7→ with h handle (let x2 = val y2 in val 2)) ()
with h handle (let x2 = val () in val 2)
with h handle (val 2)

ι#update 2 ≡ ι#update 2 (y3 . val y3 )

3.2. Big-step semantics. In addition to small-step operational semantics, we also provide
a big-step variant, which is closer to the actual implementation of Eff . Define a result to
be a pure expression or an operation call:
Result r :: = val e

ι#op e (x. c)

Big-step semantics c ⇓ r evaluates a computation c to a result r, according to the following
inductive rules:
c1 ⇓ r
if true then c1 else c2 ⇓ r
c1 ⇓ r
(match 0 with 0 7→ c1 | succ x 7→ c2 ) ⇓ r
c[e/x] ⇓ r
(fun x 7→ c) e ⇓ r

val e ⇓ val e

c2 ⇓ r
if false then c1 else c2 ⇓ r
c2 [e/x] ⇓ r
(match succ e with 0 7→ c1 | succ x 7→ c2 ) ⇓ r

ι#op e (x. c) ⇓ ι#op e (x. c)

c1 ⇓ ι#op e (y. c)
let x = c1 in c2 ⇓ ι#op e (y. let x = c in c2 )

c1 ⇓ val e
c2 [e/x] ⇓ r
let x = c1 in c2 ⇓ r

c2 [(fun x 7→ let rec f x = c1 in c1 )/f ] ⇓ r
let rec f x = c1 in c2 ⇓ r

c ⇓ val e
cv [e/x] ⇓ r
with (handler val x 7→ cv | ocs) handle c ⇓ r
def

h = (handler val x 7→ cv | ocs)
c ⇓ ι#op e (y. c)
(op : Aop −
→ B op ) ∈ ΣE
op
ocsι#op (e, (fun y : B 7→ with h handle c)) ⇓ r
with h handle c ⇓ r

8

A. BAUER AND M. PRETNAR

To relate the two semantics we define an auxiliary relation

∗

by the rules
c

val e

∗

val e

ι#op e (x. c)

∗

ι#op e (x. c)

c′
c

c′
∗
r

∗

r

This is roughly the reflexive transitive closure of , except that it relates computations to
results rather than to computations. The small-step and big-step semantics agree in the
following sense.
Proposition 3.2. For all computations c and results r, c ⇓ r if and only if c

∗

r.

Proof. Both directions of the equivalence proceed by a routine induction. The formalized
proofs of the two implications can be found in the file small-big.elf.
4. An effect system
4.1. Subtyping. As in most effect systems, we need to take care of the poisoning problem [26]. For example, what should be the type of ignore in
let ignore = val (fun msg 7→ val ()) in
let f = if b then (val ignore) else (val std#write) in
val ignore
assuming we have the ground type string and a boolean expression b? If we give it the
desired type string −
→ unit ! ∅ then there is a type mismatch between the branches in
the conditional statement, whereas the dirty type string −
→ unit ! {std#write} loses the
valuable knowledge that ignore is a pure function. The simplest antidote to the poisoning
problem is subtyping so that ignore may be given the function type with empty dirt which
is coerced in the conditional statement to a supertype that matches the other branch.
For our purposes, a straightforward variant of structural subtyping [6] suffices. We have
subtyping of pure types A 6 A′ and of dirty types C 6 C, given by the rules
bool 6 bool

nat 6 nat
R ⊆ R′

ER 6 ER

′

unit 6 unit

A′ 6 A
C 6 C′
A−
→ C 6 A′ −
→ C′

empty 6 empty

C′ 6 C
D 6 D′
⇒ D′
C=
⇒ D 6 C′ =

A 6 A′
∆ ⊆ ∆′
A ! ∆ 6 A′ ! ∆′

It is easily checked that reflexivity and transitivity of subtyping are admissible. Apart
from resolving the poisoning problem, subtyping allows us to better deduce the behavior of
handlers. Consider the computation
let u = val ι in
let v = (if b then val u else val ι′ ) in
let h = val (handler val x 7→ · · · | u#op x k 7→ c) in
···
′

Without subtyping we are forced to give both u and v the type E {ι,ι } . Therefore, by looking
at the type of u we cannot tell whether h handles ι#op or ι′ #op, and so we must assume

AN EFFECT SYSTEM FOR ALGEBRAIC EFFECTS AND HANDLERS

9

that both may be unhandled by h. With subtyping we may give u the type E {ι} which
makes it clear that h handles ι#op.
4.2. Typing rules. There are two typing judgments,
Γ⊢e:A

and

Γ⊢c:C

stating that an expression e has a pure type A and a computation c has a dirty type C,
respectively. Here Γ is a typing context of the form x1 : A1 , . . . , xn : An . There is also a
third, auxiliary typing judgment
Γ ⊢ ocs : C/∆
which states that operation cases ocs all have the same outgoing type C and are guaranteed
to handle operations in ∆. Most of the typing rules in Figure 1 are standard, except for:
Inst: we check that ι is one of instances in R, which in turn must be contained in IE .
Hand: to check that a handler has type A ! ∆ ⇒
= B ! ∆′ , we verify that it converts a compu′
tation of type A ! ∆ to one of type B ! ∆ , which involves checking three premises. First,
the value case must take a value of type A to a computation of type B ! ∆′ . Second, all
operation cases must have outgoing type B ! ∆′ . Third, every operation in ∆ is either
guaranteed to be handled by ocs, or is contained in ∆′ .
OpCases-Nil, OpCases-Cons: the auxiliary typing judgment verifies that the operation
cases have the given outgoing type, and that they cover the given dirt. The empty list
nil does not cover anything and has any outgoing type. The rule OpCases-Cons checks
the first operation case, checks the others inductively, and verifies that ∆ ⊆ ∆′ ∪· R#op,
where
(
∆′ ∪ {ι#op} if R = {ι},
def
∆′ ∪· R#op =
∆′
otherwise.
The idea is that we can be sure that an operation case handles ι#op only when the type
of its instance is of the form E {ι#op} .
Op: we first check that e and op belong to the same effect. Then we check that ∆ covers
not just all possible operations that the operation call may cause (recall that R may
contain more than one instance), but also any operations in the continuation c. We may
assume that c has the same dirt, as we can use SubComp otherwise. We use the same
reasoning in rules IfThenElse, Match and Let.
With: handlers behave like functions from computations to computations.
SubExpr, SubComp: these subsumption rules allow us to always assign a bigger type.
The effect system is safe with respect to the operational semantics:
Theorem 4.1 (Progress & Preservation).
Progress: If ⊢ c : A ! ∆ then either
• there exists a computation c′ such that c
c′ , or
• c is of the form val e for some expression e, or
• c is of the form ι#op e (x. c′ ) for some ι#op ∈ ∆.
c′ then ⊢ c′ : C.
Preservation: If ⊢ c : C and c
Proof. Both statements are proved by induction. The formalized proofs can be found in the
files progress.elf and preservation.elf.

10

A. BAUER AND M. PRETNAR

Var
(x : A) ∈ Γ
Γ⊢x:A

True

False

Zero

Γ ⊢ true : bool

Γ ⊢ false : bool

Γ ⊢ 0 : nat

Fun

Unit
Γ ⊢ () : unit

OpCases-Nil
Γ ⊢ nilC : C/∅

Inst
ι ∈ R ⊆ IE

Γ, x : A ⊢ c : C
Γ ⊢ fun x : A 7→ c : A −
→C

Hand
Γ, x : A ⊢ cv : B ! ∆′
Γ ⊢ ocs : B ! ∆′ /∆′′
∆ ⊆ ∆′′ ∪ ∆′
Γ ⊢ (handler val x : A 7→ cv | ocs) : A ! ∆ =
⇒ B ! ∆′

Succ
Γ ⊢ e : nat
Γ ⊢ succ e : nat

Γ ⊢ ι : ER
SubExpr
Γ⊢e:A
A 6 A′
Γ ⊢ e : A′

OpCases-Cons
Γ ⊢ e : ER
(op : Aop −
→ B op ) ∈ ΣE
op
op
Γ, x : A , k : B −
→C⊢c:C
Γ ⊢ ocs : C/∆′
∆ ⊆ ∆′ ∪· R#op
Γ ⊢ (e#op x k 7→ c | ocs) : C/∆

IfThenElse
Γ ⊢ e : bool
Γ ⊢ c1 : C
Γ ⊢ c2 : C
Γ ⊢ if e then c1 else c2 : C
Absurd
Γ ⊢ e : empty
Γ ⊢ absurdC e : C

Match
Γ ⊢ e : nat
Γ ⊢ c1 : C
Γ, x : nat ⊢ c2 : C
Γ ⊢ match e with 0 7→ c1 | succ x 7→ c2 : C

App
Γ ⊢ e2 : A
Γ ⊢ e1 : A −
→C
Γ ⊢ e1 e2 : C

Val
Γ⊢e:A
Γ ⊢ val e : A ! ∆

Op
Γ ⊢ e1 : E R
(op : Aop −
→ B op ) ∈ ΣE
op
op
Γ ⊢ e2 : A
Γ, y : B ⊢ c : A ! ∆
∀ι ∈ R. ι#op ∈ ∆
Γ ⊢ e1 #op e2 (y. c) : A ! ∆
Let
Γ ⊢ c1 : A ! ∆
Γ, x : A ⊢ c2 : B ! ∆
Γ ⊢ let x = c1 in c2 : B ! ∆

LetRec
Γ, f : A −
→ C, x : A ⊢ c1 : C
Γ, f : A −
→ C ⊢ c2 : D
Γ ⊢ let rec f x : A −
→ C = c1 in c2 : D

With
Γ⊢e:C=
⇒D
Γ⊢c:C
Γ ⊢ with e handle c : D

SubComp
Γ⊢c:C
C 6 C′
Γ ⊢ c : C′

Figure 1: The typing rules of core Eff .

Corollary 4.2 (Safety). A terminating computation of type A ! ∆ returns a value of type A,
or calls an operation in ∆.
In particular, a terminating computation of type A ! ∅ does not call any operations and
returns a pure value of type A.
Example 4.3. Let us see what the effect system tells us about Example 3.1. We may
give the reference ι ∈ Iref type ref{ι} . Then the computation c has the dirty type

AN EFFECT SYSTEM FOR ALGEBRAIC EFFECTS AND HANDLERS

11

nat ! {ι#lookup, ι#update}, and the handler h the type
(nat ! {ι#lookup, ι#update}) =
⇒ (unit ! {ι#update})
because it handles both lookup and update, but then calls update in the value case. This
update also changes the type of computation from nat to unit.
′
If we give ι the less precise type ref{ι,ι } , the dirt of c is
def

∆ = {ι#lookup, ι′ #lookup, ι#update, ι′ #update}
while the best type we can give to h is (nat ! ∆) ⇒
= (unit ! ∆). Since {ι, ι′ } is not a singleton,
we cannot give any guarantees on what operations are handled.
4.3. Skeletal types. We relate the pure and dirty types to ML-style types by an operation
which erases all effect information to produce a skeletal type. We will use these later to
obtain a coherent semantics of types. The skeletal types are defined as follows:
Skeletal type S, T :: = bool

nat

unit

empty

S−
→T

E

S=
⇒T

There is no distinction between pure and dirty types anymore. The typing rules for skeletal
types are like those for pure and dirty types with the effect information omitted, for instance
Inst’
ι ∈ IE
Γ⊢ι:E

Hand’
Γ, x : As ⊢ cv : S
Γ ⊢ ocs : S
Γ ⊢ (handler val x : A 7→ cv | ocs) : As =
⇒S

OpCases-Nil’
Γ ⊢ nilC : C s

OpCases-Cons’
Γ⊢e:E
(op : Aop −
→ B op ) ∈ ΣE
Γ, x : (Aop )s , k : (B op )s −
→S⊢c:S
Γ ⊢ (e#op x k 7→ c | ocs) : S
Op’
Γ ⊢ e1 : E

(op : Aop −
→ B op ) ∈ ΣE
Γ ⊢ e2 : (Aop )s
Γ ⊢ e1 #op e2 (y. c) : S

Γ ⊢ ocs : S

Γ, y : (B op )s ⊢ c : S

The remaining rules remain unchanged as they do not mention effects, while subsumption
rules are removed. To every pure type A and a dirty type C we assign their skeletal versions
As and C s , which are like A and C with region and dirt removed. The skeletal version Γs
of a typing context Γ is obtained by taking the skeletons of the types in Γ. We summarize
the properties of skeletal types:
Theorem 4.4.
(1) If A 6 B and C 6 D then As = B s and C s = D s .
(2) If
Γ⊢e:A
and
Γ⊢c:C
then
Γs ⊢ e : As
and
Γs ⊢ c : C s .
(3) In a given context, an expression and a computation has at most one skeletal type, with
a unique typing derivation.

12

A. BAUER AND M. PRETNAR

Proof. The first statement holds by an induction on the derivation of A 6 B and C 6 D.
To prove the second statement, observe that a typing derivation may be mapped to the
corresponding skeletal version rule by rule, except for subsumption rules. But these can be
simply omitted from the typing derivations because A 6 B and C 6 D imply As = B s and
C s = D s by the first statement.
The last statement holds by inversion: in any situation at most one skeletal typing rule
applies in at most one way.
A consequence of the theorem is that if a computation c has dirty types C and D then
C s = D s , hence C and D differ only in the effect information. An analogous property holds
for expressions and pure types.
5. Denotational semantics
We use standard domain theory to provide an adequate denotational semantics of core
Eff . We shall use ω-cpos as domains, but presumably a different kind of domains could be
used, as long as they support the standard constructions, in particular solutions of domain
equations, and are amenable to Pitts’s theory of minimal invariant properties [14]. We refer
to [1] for background on domain theory and denotational semantics.
We define a predomain to be a poset in which chains (ascending sequences) have
suprema, while a domain is a predomain with a least element ⊥. A continuous map is
a monotone map which commutes with suprema of chains. If D is a predomain and E is a
domain the set D −
→ E of all continuous maps forms a domain. The ordering on continuous
maps is pointwise. A continuous map is strict if it maps ⊥ to ⊥. The set D ⊸ E of strict
maps between domains D and E forms a subdomain of D −
→ E.
5.1. Computation domains. We first build domains that will serve as the meanings of
computation types. Let A be a predomain, I an index set, and for each i ∈ I let Ai and Bi
be predomains. We seek a domain T satisfying the domain equation T ∼
= F (T ) where F is
the functor

`
F (D) = A + i∈I Ai × (Bi −
→ D) ⊥ .
Following [14] we work in the category of domains and strict maps, and take T to be a
minimal solution in the sense that it possesses the minimal invariant property. The usual
limit-colimit construction [1, Chapter 7] yields such a domain. As domain equations go, this
one is quite simple because T occurs only covariantly. The elements of T can be thought of
as trees whose leaves are tagged with elements of A or ⊥, and whose nodes have branching
types Bi and are tagged with elements of Ai . The trees need not be well founded.
The minimality of T yields a recursion and an induction principle. The recursion
principle says that for any domain D, a continuous map fval : A −
→ D, and continuous
maps fi : Ai × (Bi −
→ D) −
→ D for i ∈ I, there is a unique strict continuous map f : T ⊸ D
such that
f (inval (x)) = fval (x)
f (ini (y, κ)) = fi (y, f ◦ κ)

for x ∈ A,
for y ∈ Ai and κ : Bi −
→ T.

The induction principle for T applies to admissible predicates on T , i.e., those that hold for
⊥ and are closed under suprema of chains. Precisely, if φ is an admissible predicate on T
such that

AN EFFECT SYSTEM FOR ALGEBRAIC EFFECTS AND HANDLERS

13

(1) φ(inval (x)) for all x ∈ A, and
(2) for all i ∈ I, x ∈ Ai , and κ : Bi −
→ T , if ∀y ∈ Bi . φ(κ(y)) then φ(ini (x, κ)),
then φ(t) holds for all t ∈ T .
For any I, the construction of a minimal solution TI (A, (Ai )i , (Bi )i ) from the input data
A, (Ai )i∈I , (Bi )i∈I forms a locally continuous functor
TI : pCpo × pCpoI × (pCpoop )I −
→ Cppo.
Here Cppo is the category of domains and strict continuous maps, while pCpo is the
category of predomains and partial continuous maps which are defined on open subsets (an
upper set which is inaccessible by suprema of chains). The functor will appear later on in
a larger system of recursive domain equations.
5.2. Semantics of skeletal types. We interpret pure and dirty types as predomains and
domains, respectively. A typing context is interpreted as a cartesian product of predomains,
and a typing judgment as a continuous map. However, typing judgments do not have unique
derivations because of the subsumption rules, and so we have to worry about coherence.
That is, when we define the meaning of a typing judgment by induction on its derivation,
we need to make sure that the result does not depend on the choice of derivation. We
accomplish this by providing a semantics which factors through the skeletal types from
Section 4.3.
Let
Ω = {ι#op | ∃E. ι ∈ IE ∧ op ∈ ΣE }
be the set of all operations. If dirts could be infinite, A ! Ω would be a dirty type expressing
the fact that any effect could happen.
To each skeletal type S we assign a predomain JSKe and a domain JSKc as follows:
JboolKe = {ff, tt},

JnatKe = N,

JunitKe = {⋆},

JemptyKe = ∅,

JS −
→ T Ke = JSKe −
→ JT Kc ,

JEKe = IE ,

JS =
⇒ T Ke = JSKc ⊸ JT Kc ,
and
JSKc = TΩ (JSKe , (J(Aop )s Ke )ι#op , (J(B op )s Ke )ι#op ).
These should be read as a system of domain and predomain equations indexed by the
skeletal types. There are possible circularities in the system because the equation for JSKc
refers to possibly larger skeletal types (Aop )s and (B op )s . As in the case of computation
domains, we take the minimal solutions which enjoy the minimal invariant property.
To each pure type A and dirty type C we assign a skeletal predomain JAK and skeletal
domain JCK by setting
JAK = JAs Ke

and

JCK = JC s Kc .

The first part of Theorem 4.4 guarantees that A 6 B and C 6 D imply JAK = JBK and
JCK = JDK.

14

A. BAUER AND M. PRETNAR

5.3. Semantics of expressions and computations. The meaning of a typing context Γ
x1 : A1 , . . . , xn : An
is
JΓK = JA1 K × · · · × JAn K.
We interpret typing judgments
Γ⊢e:A

and

Γ⊢c:C

JΓ ⊢ e : AK : JΓK −
→ JAK

and

JΓ ⊢ c : CK : JΓK −
→ JCK.

as continuous maps
When no confusion can arise we abbreviate these as JeK and JcK. The definition proceeds
by induction on the derivation of the typing judgment. Given an environment η ∈ JΓK, the
base rules for expressions and the successor rule are taken care of by
JΓ ⊢ xi : Ai Kη = ηi

JΓ ⊢ false : boolKη = ff

JΓ ⊢ () : unitKη = ⋆

JΓ ⊢ true : boolKη = tt

JΓ ⊢ 0 : natKη = 0

JΓ ⊢ succ e : natKη = (JΓ ⊢ e : natKη) + 1

JΓ ⊢ ι : E R Kη = ι,
and the abstraction rule by
JΓ ⊢ (fun x : A 7→ c) : A −
→ CKη = λa ∈ JAK . JΓ, x : A ⊢ c : CK(η, a)
For the handler rule we set
JΓ ⊢ (handler val x : A 7→ cv | ocs) : A ! ∆ ⇒
= B ! ∆′ K = h
where h : JΓK −
→ JA ! ∆K ⊸ JB ! ∆′ K is defined by recursion on JA ! ∆K:
h(η)(⊥) = ⊥
h(η)(inval (a)) = JΓ, x : A ⊢ cv : B ! ∆′ K(η, a)
h(η)(inι#op (a, κ)) = JocsKι#op (η, a, h(η) ◦ κ)
The auxiliary map
JocsKι#op : JΓK × JAop K × JB op −
→ B ! ∆′ K −
→ JB ! ∆′ K
is defined by
JnilC Kι#op (η, a, κ) = inι#op (a, κ)
′

′

Je #op x k 7→ c | ocsKι#op (η, a, κ) =
(
JΓ, x : Aop , k : B op −
→ B ! ∆′ ⊢ c : B ! ∆′ K(η, a, κ)
JocsKι#op (η, a, κ)

if (Je′ Kη)#op′ = ι#op,
otherwise.

Finally, if Γ ⊢ e : A′ is derived from the premises Γ ⊢ e : A and A 6 A′ by the subsumption
rule, we set
JΓ ⊢ e : A′ Kη = JΓ ⊢ e : AKη.

AN EFFECT SYSTEM FOR ALGEBRAIC EFFECTS AND HANDLERS

15

The definition is meaningful because A 6 A′ implies JAK = JA′ K. The meaning of pure
computations and operations is
JΓ ⊢ val e : A ! ∆Kη = inval (JΓ ⊢ e : AK)
JΓ ⊢ e1 #op e2 (y. c) : A ! ∆Kη = inJe1 Kη#op (Je2 Kη, λb ∈ JB op K . JΓ, y : B op ⊢ c : A ! ∆K(η, b)).
The meaning of elimination forms is
⇒ DKη)(JΓ ⊢ c : CKη)
JΓ ⊢ with e handle c : DKη = (JΓ ⊢ e : C =
(
JΓ ⊢ c1 : CKη if JΓ ⊢ e : boolKη = tt,
JΓ ⊢ if e then c1 else c2 : CKη =
JΓ ⊢ c2 : CKη if JΓ ⊢ e : boolKη = ff
JΓ ⊢ absurd e : CKη = ⊥
JΓ ⊢ e1 e2 : CKη = (JΓ ⊢ e1 : A −
→ CKη)(JΓ ⊢ e2 : AK)
and
JΓ ⊢ (match e with 0 7→ c1 | succ x 7→ c2 ) : CKη =
(
JΓ ⊢ c1 : CKη
if JΓ ⊢ e : natKη = 0,
JΓ, x : nat ⊢ c2 : CK(η, n) if JΓ ⊢ e : natKη = n + 1.
To give semantics of let binding, we first define the lifting of a map f : JAK −
→ JB ! ∆K to
†
be the map f : JA ! ∆K −
→ JB ! ∆K defined recursively by
f † (⊥) = ⊥,
f † (inval (x)) = f (x),
f † (inι#op (x, κ)) = inι#op (x, f † ◦ κ).
Then we set
JΓ ⊢ let x = c1 in c2 : B ! ∆Kη =
(λa ∈ JAK . JΓ, x : A ⊢ c2 : B ! ∆K(η, a))† (JΓ ⊢ c1 : A ! ∆Kη).
The meaning of a recursive function definition is
JΓ ⊢ (let rec f x : A −
→ C = c1 in c2 ) : CKη = JΓ, f : A −
→ C ⊢ c2 : CK(η, g)
where g : JAK −
→ JCK is the least fixed-point of the map
g 7→ (λa ∈ JAK . Jc1 K(η, g, a)).
Finally, just like for expressions, if Γ ⊢ c : C ′ is derived from the premises Γ ⊢ c : C and
C 6 C ′ by the subsumption rule, we set
JΓ ⊢ c : C ′ Kη = JΓ ⊢ c : CKη.
This concludes the definition of denotational semantics of expressions and computations.
Theorem 5.1 (Coherence). All derivations of a typing judgment give it the same meaning.
Proof. The semantics of Γ ⊢ e : A and Γ ⊢ c : C factor through the associated skeletal
derivations Γs ⊢ e : As and Γs ⊢ c : C s , respectively. This is so because the semantic
rules given above clearly factor through the associated skeletal rules. In other words, they
ignore the effect information and the subsumption rules. Uniqueness of meaning is thus a
consequence of the uniqueness of skeletal derivations, cf. Theorem 4.4.

16

A. BAUER AND M. PRETNAR

5.4. Semantics of effects. In the terminology of John Reynolds [23] the semantics given so
far is intrinsic, while the semantics of effects given below is extrinsic. This is in accordance
with our understanding that effect information is descriptive rather than prescriptive: a
function f of type (A −
→ B ! ∆) −
→ B ′ ! ∆′ should accept any function g of type A −
→ B ! ∆′′ ,
′′
′′
even if ∆ 6⊆ ∆, although it has the property that if ∆ ⊆ ∆ then f (g) calls only operations
in ∆′ .
For each pure type A and dirty type C we define subpredomains J[AK] ⊆ JAK and
subdomains J[CK] ⊆ JCK of those elements that behave according to the effect information.
The ground types are easy:
J[boolK] = JboolK,
J[emptyK] = JemptyK,

J[natK] = JnatK,

J[unitK] = JunitK,

J[E R K] = R.

For function types, handler types, and dirty types we would like to solve the following
system of equations with unknowns J[AK] and J[CK] where A and C range over pure and dirty
types, respectively:
→ JCK | ∀x ∈ J[AK]. f (x) ∈ J[CK]},
J[A −
→ CK] = {f ∈ JAK −
J[C =
⇒ DK] = {h ∈ JCK ⊸ JDK | ∀t ∈ J[CK]. h(t) ∈ J[DK]},
J[A ! ∆K] = {t ∈ JA ! ∆K | t = ⊥ ∨ (∃x ∈ J[AK]. t = inval (x)) ∨

(5.1)

∃ι#op ∈ ∆, y ∈ J[Aop K], κ ∈ JB op −
→ A ! ∆K.
(∀z ∈ J[B op K]. κ(b) ∈ J[A ! ∆K]) ∧ t = inι#op (y, κ)}.
The last rule says that t ∈ J[A ! ∆K] when it is ⊥, or of the form inval (x) for some x ∈ J[AK],
or of the form inι#op (y, κ) for some y ∈ J[Aop K] and κ ∈ J[B op −
→ A ! ∆K].
The system is potentially problematic because the types Aop and B op introduce circularities in the last equation. We apply Pitts’s theorem [14, Theorem 4.16] about existence
of invariant relations to obtain a solution that satisfies an induction principle, see Theorem 5.2 below. For Pitts’s theorem to apply we must verify that our conditions form an
admissible action on admissible relations, as defined in [14, Definition 4.6]. The relational
structure in question is that of [14, Example 4.2(ii)] for which the accompanying notion
of admissibility is the one we are using, cf. [14, Example 4.5(ii)]. The locally continuous
functor is the evident one, while its admissible action on relations is read off (5.1). The
admissibility of the action follows from [14, Lemma 6.6]: the first two actions in (5.1) are
considered explicitly, while the third one is a composition of actions from the cited lemma.
The solution so obtained possesses the following induction principle.
Theorem 5.2. Suppose φ is an admissible predicate on JA ! ∆K such that
(1) φ(inval (a)) for every a ∈ J[AK], and
→ A ! ∆K], if ∀b ∈ J[B op K]. φ(κ(b)) then
(2) for all ι#op ∈ ∆, a ∈ J[Aop K], κ ∈ J[B op −
φ(inι#op (a, κ)).
Then φ(t) for all t ∈ J[A ! ∆K].
Proof. Because we defined J[−K] mutually for all types, we first extend φ to be constantly
true on types other than A ! ∆. Then our theorem becomes an instance of the induction
property [14, Theorem 6.5]. The admissible action required for the application of the
theorem is obtained using [14, Lemma 6.6].

AN EFFECT SYSTEM FOR ALGEBRAIC EFFECTS AND HANDLERS

17

The semantics of effects and the semantics of expressions and computations fit together:
Theorem 5.3. If Γ ⊢ e : A and Γ ⊢ c : C then for all η ∈ J[ΓK] = J[A1 K] × · · · × J[An K], we
have
JΓ ⊢ e : AKη ∈ J[AK]
and
JΓ ⊢ c : CKη ∈ J[CK].
Proof. The proof proceeds by induction on the derivation of the typing judgment. All cases
are easy, except for the typing rule for a handler
Γ ⊢ (handler val x 7→ cv | ocs) : A ! ∆ ⇒
= B ! ∆′
First, we claim that if the auxiliary judgment
Γ ⊢ ocs : B ! ∆′ /∆c
is derivable then JocsKι#op (η, a, κ) ∈ J[B ! ∆′ K] for all ι#op ∈ ∆′ ∪ ∆c , η ∈ J[ΓK], a ∈ J[Aop K],
and κ : J[B op −
→ B ! ∆′ K]. Assuming the claim has been established, the above handler rule
follows immediately.
The proof of the claim proceeds by induction on the derivation of the auxiliary judgment.
For nil, we have ∆c = ∅ and the claim obviously holds. The other possibility is
Γ ⊢ (e#op′ x k 7→ c | ocs) : B ! ∆′ /∆′c
for some Γ ⊢ ocs : B ! ∆′ /∆c and ∆′c ⊆ (∆c ∪· R#op). Define ι′ = JΓ ⊢ e : E R Kη and consider
two cases. First, if ι′ #op′ = ι#op then
Je#op′ x k 7→ c | ocsKι#op (η, a, κ) = JΓ, x : Aop , k : B op −
→ B ! ∆′ ⊢ c : B ! ∆′ K(η, a, κ),
and we may apply the induction hypothesis (for the whole theorem) to c. Second, suppose
ι′ #op′ 6= ι#op. Then the assumption ι#op ∈ ∆′ ∪ ∆′c implies ι#op ∈ ∆′ ∪ ∆c . Indeed, if
ι#op ∈ ∆′ there is nothing to prove, and if ι#op ∈ ∆′c ⊆ (∆c ∪· R#op), then either R is not a
singleton and ∆c ∪· R#op = ∆c , or R = {ι′ #op′ } and ι#op 6∈ R. In any case, it follows that
Je#op′ x k 7→ c | ocsKι#op (η, a, κ) = JocsKι#op (η, a, κ)
and Γ ⊢ ocs : B ! ∆′ /∆c . Thus we may apply the induction hypothesis.
5.5. Soundness and adequacy. The soundness and adequacy theorems state that operational semantics and denotational semantics fit together. One is an easy induction, while
the other is proved using standard technique of formal approximation relations, e.g., see [1,
Theorem 6.3.6].
Theorem 5.4 (Soundness). If ⊢ c : C and c

c′ then J⊢ c : CK = J⊢ c′ : CK.

Proof. We just have to walk through all the defining rules for
indeed preserve the meaning of c.

and verify that they do

18

A. BAUER AND M. PRETNAR

To tackle adequacy, see Corollary 5.8 below, we define formal approximation relations
⊳A and ⊳C whose intuitive meaning is that an element of JAK or JCK approximates a closed
term of type A or C. Given d ∈ JAK and a closed expression e : A, we define d ⊳A e by:
d ⊳bool e ⇐⇒ (d = tt ∧ e = true) ∨ (d = ff ∧ e = false)
d ⊳nat e ⇐⇒ d = n ∧ e = succn 0
d ⊳unit e ⇐⇒ d = ⋆ ∧ e = ()
′ ′
′
′
′
′
d ⊳A−
→C e ⇐⇒ ∀d , e . (d ⊳A e ⇒ d(d ) ⊳C e e )
d ⊳E R e ⇐⇒ d = e
′
′
′
d ⊳C =
⇒D e ⇐⇒ ∀d , c. (d ⊳C c ⇒ d(d ) ⊳D (with e handle c))

Simultaneously we define when d ∈ JA ! ∆K approximates a closed computation c : A ! ∆,
where d ⊳A ! ∆ c holds when
• d = ⊥, or
• d = inval (d′ ), c ⇓ val e and d′ ⊳A e, or
• d = inι#op (d′ , κ), c ⇓ ι#op e (y. c′ ), d′ ⊳Aop e, and if d′′ ⊳B op e′ then κ(d′′ ) ⊳A ! ∆ c′ [e′′ /y].
The definition of ⊳A ! ∆ refers to types Aop and B op which are possibly larger than A, thus
we again use [14, Theorem 4.16] to establish existence of minimal such ⊳A and ⊳C , much
like for the recursive types considered in [14, Section 5].
Lemma 5.5. If d ⊳A ! ∆ c′ and c

c′ then d ⊳A ! ∆ c.

Proof. There is nothing to prove if d = ⊥. The other two cases follow because c
c′ and
′
′
′
c ⇓ r imply c ⇓ r. For instance, if d ⊳A ! ∆ c holds because d = inval (d ), c ⇓ val e and
d′ ⊳A e for some d′ and e, then d ⊳A ! ∆ c holds because c
c′ implies c ⇓ val e and so we
may reuse d′ and e.
Lemma 5.6. The relations ⊳A and ⊳C are closed under suprema of chains in the first
argument. The relations ⊳C relate ⊥ to every computation.
Proof. The second statement holds by the definition of ⊳C . For the first statement we
proceed by induction on the type. The base cases hold because the predomains for ground
→ CK and dn ⊳A−
types are flat. For A −
→ C, suppose (dn )n is a chain in JA −
→C e for all n.
Consider any d′ , e′ such that d′ ⊳A e′ . Then dn (d′ ) ⊳C e e′ for all n. Suprema in JA −
→ CK are
defined pointwise, so we can use the induction hypothesis for C and get
W
W
( n dn )(d′ ) = n dn (d′ ) ⊳C e e′ ,
W
hence n dn ⊳C e as desired. Handler types are treated similarly. Consider a computation
type A ! ∆, a closed computation c : A ! ∆ and a chain (dn )n in JA ! ∆K such that dn ⊳C c for
all n. There are three kinds of chains in JA ! ∆K:
W
• (dn )n is constantly ⊥: then n dn = ⊥ ⊳C c.
• for large enough n there are d′n such that dn = inval (d′n ): then (d′n )n form a chain in JAK.
Because operational semantics is deterministic, thereWexists a single e such that
W c ⇓ val e,
′ ⊳ e, from which
induction hypothesis
for
A
we
have
d
and d′n ⊳A e. By W
n dn ⊳A ! ∆ c
n n A
W
follows because n dn = inval ( n d′n ).
• there are ι and op such that for large enough n there are d′n and κ′n such that dn =
inι#op (d′n , κn ): this case is treated analogously to the previous one.

AN EFFECT SYSTEM FOR ALGEBRAIC EFFECTS AND HANDLERS

19

Lemma 5.7. Let Γ be the context x1 : A1 , . . . , xn : An . Suppose that for each 1 6 i 6 n we
have di ∈ JAi K and a closed expression ⊢ ei : Ai such that di ⊳Ai ei .
(1) If Γ ⊢ e : A then JΓ ⊢ e : AK(d1 , . . . , dn ) ⊳A e[e1 /x1 , . . . , en /xn ].
(2) If Γ ⊢ c : C then JΓ ⊢ c : CK(d1 , . . . , dn ) ⊳C c[e1 /x1 , . . . , en /xn ].
Proof. We prove the statements by induction on the derivation of the typing judgments.
Let η = (d1 , . . . , dn ) and σ = [e1 /x1 , . . . , en /xn ]. We write [σ, e/x] for the substitution
[e1 /x1 , . . . , en /xn , e/x]. Throughout we assume that bound variables occurring in various
terms do not appear in σ:
Cases Var, True, False, Unit, Zero, Inst: these are all trivial.
Case Succ: Γ ⊢ (succ e) : nat. By the induction hypothesis, we have JeKη ⊳nat eσ. Next,
notice that the closed expression eσ : nat must be succk 0 for some k, hence JeKη = k,
and so
Jsucc eKη = (k + 1) ⊳nat succ (eσ) = (succ e)σ.
Case Fun: Γ ⊢ (fun x 7→ c) : A −
→ C. If d′ ⊳A e′ then by the induction hypothesis for c
JΓ, x : A ⊢ cK(η, d′ ) ⊳C c[σ, e′ /x].
Because JΓ, x : A ⊢ cK(η, d′ ) = (JΓ ⊢ fun x 7→ cKη) d′ and
((fun x 7→ c)σ) e′ = (fun x 7→ cσ) e′

c[σ, e′ /x],

we may use Lemma 5.5 to get the desired conclusion
(JΓ ⊢ fun x 7→ cKη) d′ ⊳C ((fun x 7→ c)σ) e′ .
Most other cases in the proof follow the same pattern, so we shall not explicitly mention
uses of Lemma 5.5 anymore.
Case Hand: Γ ⊢ (handler val x 7→ cv | ocs) : A ! ∆ ⇒
= B ! ∆′ . We abbreviate the handler
as h. Assuming d ⊳A ! ∆ c we need to show that
(JhKη)(d) ⊳B ! ∆′ (with hσ handle c).
We proceed by an induction on d:
• If d = ⊥ then the conclusion follows because JhKη is strict.
• If d = inval (d′ ) then d ⊳A ! ∆ c implies c ⇓ val e′ and d′ ⊳A e′ for some e′ and d′ . In this
case, by induction hypothesis for cv ,
(JhKη)(d) = JΓ, x : A ⊢ cv K(η, d′ ) ⊳b ! ∆ cv [σ, e′ /x],
and

(with hσ handle c)
···
(cv σ)[e′ /x] = cv [σ, e′ /x].
• If d = inι#op (d′ , κ) then d ⊳A ! ∆ c implies c ⇓ ι#op e′ (y. c′ ), d′ ⊳Aop e′ and κ ⊳B op −
→A ! ∆
(fun y 7→ c′ ). Now
(JhKη)(inι#op (d′ , κ)) = JocsKι#op (η, d′ , JhKη ◦ κ)
and
(with hσ handle c)

···

(ocs σ)ι#op (e′ , (fun y 7→ with hσ handle c′ )),

therefore it suffices to prove
JocsKι#op (η, d′ , JhKη ◦ κ) ⊳B ! ∆′ (ocs σ)ι#op (e′ , (fun y 7→ with hσ handle c′ )),
which we do by induction on the length of ocs. When ocs is nil the statement becomes
inι#op (d′ , JhKη ◦ κ) ⊳B ! ∆′ ι#op e′ (y. with hσ handle c′ ).

20

A. BAUER AND M. PRETNAR

We already know d′ ⊳Aop e′ , and still need
JhKη(κ(d′′ )) ⊳B ! ∆′ (with hσ handle c′ [e′′ //y])
assuming d′′ ⊳B op e′′ . This follows from the available induction hypotheses.
When ocs is (ι′ #op′ x k 7→ c′′ | ocs′ ) there are two further subcases:
– if ι#op = ι′ #op′ then we get
JΓ, x, k ⊢ c′′ K(η, d, JhKη ◦ κ) ⊳B ! ∆′
c′′ [σ, e′ /x, (fun y 7→ with hσ handle c′ )/k]
which holds by induction on c′′ ,
– if ι#op 6= ι′ #op′ then we are left with
Jocs′ Kι#op (η, d′ , JhKη ◦ κ)⊳B ! ∆′
(ocs′ σ)ι#op (e, (fun y 7→ with hσ handle c′ )),
which is just the induction hypothesis for ocs′ .
Cases IfThenElse, Match, Absurd: We consider only
Γ ⊢ (if e then c1 else c2 ) : C,
as Match is similar and Absurd is vacuous. Because eσ is a closed expression of type
bool it is either true or false. Let us take a look at the first possibility. By induction
hypothesis for c1 we have Jc1 Kη ⊳C c1 σ. Again, because Jif true then c1 else c2 Kη =
Jc1 Kη and
(if true then c1 else c2 )σ
c1 σ
it follows that
Jif true then c1 else c2 Kη ⊳C (if true then c1 else c2 )σ,
as required.
→ C and Γ ⊢ e′2 : A. By induction hypotheses
Case App: Γ ⊢ e′1 e′2 : C where Γ ⊢ e′1 : A −
′
′
′
′
′
for e1 and e2 we have Je1 Kη ⊳A−
→C e1 σ and Je2 Kη ⊳A e2 σ, therefore by the definition of
⊳A−
→C ,
Je′1 e′2 Kη = (Je′1 Kη)(Je′2 Kη) ⊳C (e′1 σ)(e′2 σ) = (e′1 e′2 )σ.
Case Val: Γ ⊢ val e : A ! ∆. By induction on e we have JeKη ⊳A eσ, therefore by the second
clause in the definition of ⊳A ! ∆
Jval eKη = inval (JeKη) ⊳A ! ∆ val (eσ) = (val e)σ.
Case Op: Γ ⊢ ι#op e (y. c) : A ! ∆. This case works much like a combination of Val and
App, so we omit the details.
Case Let: Γ ⊢ (let x = c1 in c2 ) : B ! ∆. This case is treated like a handler which only
has a val case.
⇒ D and Γ ⊢ c : C. By induction
Case With: Γ ⊢ with e handle c : D where Γ ⊢ e : C =
hypotheses we have JeKη ⊳C =
⇒D eσ and JcKη ⊳C cσ, therefore by the definition of ⊳C =
⇒D
(JeKη)(JcKη) ⊳D (with eσ handle cσ).
The left-hand side equals Jwith e handle c : DKη and the right (with e handle c)σ, so
we are done.

AN EFFECT SYSTEM FOR ALGEBRAIC EFFECTS AND HANDLERS

21

Case LetRec: Γ ⊢ let rec f x = c1 in c2 : D. After a short calculation the problem
reduces to showing that
g ⊳A−
→C (fun x 7→ let rec f x = c1 σ in c1 σ)
where g is the least fixed-point of the operator Φ : JA −
→ CK −
→ JA −
→ CK, defined by
Φ(h) = λa ∈ JAK . JΓ, f, x ⊢ c1 K(η, h, a).
By Lemma 5.6 it suffices to show that
h ⊳A−
→C (fun x 7→ let rec f x = c1 σ in c1 σ)
implies
Φ(h) ⊳A−
→C (fun x 7→ let rec f x = c1 σ in c1 σ).
This amounts to proving that if d ⊳A e then
Φ(h)(d) = JΓ, f, x ⊢ c1 K(η, h, d)
⊳C c1 [σ, (fun x 7→ let rec f x = c1 σ in c1 σ)/f, e/x],
which holds by the induction hypothesis for c1 .
Case SubExpr, SubComp: For SubExpr, take Γ ⊢ e : A′ where Γ ⊢ e : A and A 6 A′ .
From induction hypothesis, we get JΓ ⊢ e : AKη ⊳A eσ. Since JAK = JA′ K, we have
⊳A = ⊳A′ . Additionally, JΓ ⊢ e : A′ K = JΓ ⊢ e : AK, hence JeKη ⊳A′ eσ. For SubComp, the
proof is similar.
Corollary 5.8 (Adequacy). If ⊢ c : unit ! ∆ and JcK = inval (⋆) then c ⇓ val ().
Proof. By the previous lemma JcK ⊳unit ! ∆ c. Therefore, if JcK = inval (⋆) then c ⇓ val () by
the definition of ⊳unit ! ∆ .
The stated adequacy suffices for our purposes, but of course similar statements holds
for other ground types. Regarding operations, if JcK = inι#op (d, κ), then ι#op ∈ ∆ and so
c ⇓ ι#op e k for some e and k such that JeK = d and JkK = κ. Therefore, if JcK 6= ⊥ then
c ⇓ r for some result r.
6. Equational reasoning
6.1. Contextual and denotational equivalence. In this section we provide principles
that allow us to reason about programs. Let us first recall how contextual equivalence is
defined. An expression context E is a computation with several occurrences of a hole [ ] in
positions where an expression is expected. When the hole is plugged with an expression e
we get a computation E[e]. A computation context E is defined analogously, except that the
holes appear where computations are expected.
We say that expressions e and e′ are contextually equivalent, written e ≈ e′ , when
for all expression contexts E such that E[e] and E[e′ ] are both of type unit ! ∆, we have
E[e] ⇓ val () if and only if E[e′ ] ⇓ val (). Contextual equivalence of computations is
defined analogously.
Contextually equivalent expressions or computations may be interchanged anywhere
in the code. Therefore, it is quite useful to know that a certain contextual equivalence
holds, but unfortunately it is difficult to work directly with contextual equivalence. Luckily,
denotational equivalence is more easily handled and is related to contextual equivalence by
the adequacy theorem.

22

A. BAUER AND M. PRETNAR

We write e ≡ e′ and c ≡ c′ when the denotations of two expressions or computations
are the same. More precisely, if Γ ⊢ e : A and Γ ⊢ e′ : A then Γ ⊢ e ≡ e′ : A, or just e ≡ e′ ,
means JΓ ⊢ e : AK = JΓ ⊢ e′ : AK, and similarly for computations.
Proposition 6.1. Denotationally equal expressions are contextually equivalent, and likewise
for computations.
Proof. Suppose e ≡ e′ and consider an expression context E such that E[e] and E[e′ ] both
have type unit ! ∆. Assume E[e] ⇓ val (). By soundness of denotational semantics JE[e]K =
inval (⋆). By assumption JeK = Je′ K and because denotational semantics is compositional it
follows that JE[e]K = JE[e′ ]K. Now by adequacy E[e′ ] ⇓ val (). The proof for computations
is the same.
Denotational equivalence is a congruence and is preserved by well-typed substitutions.
It validates the following β-rules, where the various expressions and computations have
suitable types, and h stands for handler val x 7→ cv | ocs:
if true then c1 else c2 ≡ c1
if false then c1 else c2 ≡ c2
match 0 with 0 7→ c1 | succ x 7→ c2 ≡ c1
match (succ e) with 0 7→ c1 | succ x 7→ c2 ≡ c2 [e/x]
(fun x 7→ c) e ≡ c[e/x]
let x = val e in c ≡ c[e/x]
let x = e1 #op e2 (y. c1 ) in c2 ≡ e1 #op e2 (y. let x = c1 in c2 )
let rec f x = c1 in c2 ≡ c2 [(fun x 7→ let rec f x = c1 in c1 )/f ]
with h handle (val e) ≡ cv [e/x]
with h handle (ι#op e (y. c)) ≡ ocsι#op (e, (fun y 7→ with h handle c))
We also have the following η-rules, provided the expressions and computations have easily
guessed types:
e ≡ ()
fun x 7→ e x ≡ e
let x = c in val x ≡ c
if e then c[true/x] else c[false/x] ≡ c[e/x]
match e with 0 7→ c[0/x] | succ y 7→ c[succ y/x] ≡ c[e/x]
absurd e ≡ c[e/x]
We omit the proofs because they just involve unfolding of semantic definitions. An exception
is the η-rule for let binding, which is proved by induction in the next section.
A variety of other equivalences is readily validated, for example
let x = c1 in c2 ≡ with (handler val x 7→ c2 | nil) handle c1
and the “associativity” of let binding [12]
let x = (let y = c1 in c2 ) in c3 ≡ let y = c1 in (let x = c2 in c3 ),
where y must not occur freely in c3 , see [20, 21] for other examples.

AN EFFECT SYSTEM FOR ALGEBRAIC EFFECTS AND HANDLERS

23

6.2. An induction principle for effects. The induction principle for the computation
domains from Section 5.1 is useful for deriving general laws that do not depend on a particular choice of effects. It is less useful for specific examples which involve a carefully chosen
set of effects and handlers, because it forces us to consider operations that have nothing to
do with the situation at hand. The induction principle Theorem 5.2 remedies the drawback.
A typical application arises when we prove an equivalence of the form E[c] ≡ E ′ [c] : C
for all computations c of a suitable type A ! ∆. The computation contexts E and E ′ are
interpreted as continuous maps JEK, JE ′ K : JA ! ∆K −
→ JCK, and the equivalence may be
phrased as
∀t ∈ J[A ! ∆K]. JEK(t) = JE ′ K(t).
The equality inside the quantifier is an admissible predicate on J[A ! ∆K], so the induction
principle applies. It is a bit cumbersome to perform the proof using the semantic brackets
J−K all over the place. Instead, with a bit of flexibility in notation, we can write the proof
in a syntactic manner as follows:
(1) We write ⊥ for a non-terminating computation, e.g., let rec f x = f x in f (), and
check that E[⊥] ≡ E ′ [⊥].
(2) We verify that E[val e] ≡ E ′ [val e] where e is a meta-variable of type A.
(3) We verify, for each ι#op ∈ ∆,
E[ι#op e (y. κ y)] ≡ E ′ [ι#op e (y. κ y)],
where e is a meta-variable of type Aop and κ is a meta-variable of type B op −
→ A ! ∆.
The induction hypothesis is that E[κ e′ ] ≡ E ′ [κ e′ ] for all expressions e′ of type B op .
We apply the method to prove the η-rule
let x = c in val x ≡ c
by induction:
(1) (let x = ⊥ in val x) ≡ ⊥ because let is strict in both arguments,
(2) (let x = (val a) in val x) ≡ (val x)[a/x] ≡ val a by a β-rule for let,
(3) The induction step is proved by
let x = (ι#op e (y. κ y)) in val x
≡ ι#op e (y. let x = κ y in val x)
≡ ι#op e (y. κ y)
where we used a β-rule in the first step and the induction hypothesis for κ y in the
second.
A non-trivial application of the induction principle is presented in Section 7.2.
7. Example: mutable references
As a more elaborate example we consider mutable references. In core Eff they are implemented by the effect ref with operations
lookup : unit −
→A

and

update : A −
→ unit,

24

A. BAUER AND M. PRETNAR

where A is a fixed pure type (in full Eff we could use a parameter). The handler which
handles the reference given by an expression r : refR is defined by (the underscore _
indicates an ignored parameter):
def

stater = handler val x 7→ val (fun s 7→ val x)
| r#lookup _ k 7→ val (fun s 7→ let f = k s in f s)
| r#update s′ k 7→ val (fun s 7→ let f = k () in f s′ )
This is just the usual monadic-style treatment of state which wraps a computation into a
state-carrying function. For any instance ι ∈ Iref , pure type B, and dirt ∆, the computation
stateι has the type
B ! ({ι#lookup, ι#update} ∪ ∆) ⇒
= (A −
→ B ! ∆) ! ∆.
The type says that the handler erases lookups and updates of ι from a computation. The
return type (A −
→ B ! ∆) ! ∆ has an outer dirt ∆ because effects could happen before the
first lookup or update. Note that the double dirt would not arise if we took the call-bypush-value approach to handlers [19].
The handler wraps a handled computation c of type B ! ∆ into a function expecting the
current state, which explains the type A −
→ B ! ∆. In practice such a function is immediately
applied to an initial state e of type A (such a final transformation of handled computations
is so common that in full Eff handlers have a special finally case just for this purpose):
let f = (with h handle c) in f e
The type of this computation is simply B ! ∆. In particular, if the only effects in c are
lookups and updates of ι, we get a pure computation.
If the type of r is weaker, for example ref{ι1 ,ι2 } , we are not able to deduce anything
useful. The best we can do is
stater : B ! ∆ ⇒
= (A −
→ B ! ∆) ! ∆
for any dirt ∆.
We may handle several references at once by wrapping a computation into several
handlers. For example, let c be the computation which swaps the contents of two references:
let y1 = ι1 #lookup () in
let y2 = ι2 #lookup () in
let _ = ι1 #update y2 in
let _ = ι2 #update y1 in (val ())
By itself, c has the type
unit ! {ι1 #lookup, ι1 #update, ι2 #lookup, ι2 #update},
When c is wrapped by the handler h2 = stateι2 ,
let f2 = (with h2 handle c) in f2 e2 ,
the type becomes unit ! {ι1 #lookup, ι1 #update}. When the handler h1 = stateι1 is used
on top of that,

let f1 = with h1 handle let f2 = (with h2 handle c) in f2 e2 in f1 e1

AN EFFECT SYSTEM FOR ALGEBRAIC EFFECTS AND HANDLERS

25

we get the pure type unit ! ∅. Beware, it is important that the state is initialized at the
correct point in the computation. For instance,

let f1 = with h1 handle (with h2 handle c) in (let f2 = f1 e1 in f2 e2 )

does not do the right thing. We are warned about possible trouble by the effect system
which gives the computation the type unit ! {ι1 #lookup, ι1 #update} — the operations for
ι1 are escaping the handlers! A less modular way of handling two instances is to create a
new handler with four operation cases, two for each of the instances.
7.1. Reasoning about references. With handlers the workings of a computation may be
inspected in a highly intensional way. Consequently, there are few generally valid observational equivalences. However, when known handlers are used to handle operations, we may
derive equivalences that describe the behavior of operations. The situation is opposite to
that of [19], where we start with an equational theory for operations and require that the
handlers respect it.
We demonstrate the technique for mutable state. Let h = stateι and abbreviate
let f = (with h handle c) in f e
as H[c, e]. Straightforward calculations give us the equivalences
H[(ι#lookup () (y. c)), e] ≡ H[c[e/y], e]
H[(ι#update e′ (_ . c)), e] ≡ H[c, e′ ]
H[val e′ , e] ≡ val e′ ,
for instance,
H[(ι#update e′ (_ . c)), e]
≡ let f = val (fun s 7→ let f ′ = (fun _ 7→ with h handle c) () in f ′ e′ ) in f e
≡ let f = val (fun s 7→ H[c, e′ ]) in f e
≡ (fun s 7→ H[c, e′ ]) e
≡ H[c, e′ ].
These suffice for simple equational reasoning about state. If we read them as rewrite rules
they allow us to progressively transform a computation to a simpler form. In fact, the
transformations mimic the usual coalgebraic operational semantics for state [18].
Of course, a realistic computation will contain several handlers. As long as they do not
interfere with each other, we can still use equivalences to usefully manipulate them. For
example, if h′ is a handler with no operation case for ι#lookup then
H[(with h′ handle ι#lookup () (y. c)), e]
≡ H[(ι#lookup () (y. with h′ handle c)), e]
≡ H[(with h′ handle c[e/y]), e].
It may happen that a lookup or an update is nested deeply inside several handlers. The
above transformation allows us to hoist the operation out of the inner handlers so that it
is handled by the outer handler, as long as the inner handlers do not attempt to handle ι.
The transformation applies to let bindings too, as they are like handlers without operation
cases.

26

A. BAUER AND M. PRETNAR

We may validate the seven standard equations governing state [16]. There are four
combinations of lookup and update (in the first equation y does not occur free in c):
H[ι#lookup () (y. ι#update y (_ . c)), e] ≡ H[c, e]
H[ι#lookup () (y. ι#lookup () (z. c)), e] ≡ H[ι#lookup () (y. c[y/z]), e]
H[ι#update e (_ . ι#update e′ (_ . c)), e] ≡ H[ι#update e′ (_ . c), e]
H[ι#update e (_ . ι#lookup () (y. c)), e] ≡ H[ι#update e (_ . c[e/y]), e]
For instance, the first equation is validated as follows:
H[ι#lookup () (y. ι#update y (_ . c)), e]
≡ H[ι#update e (_ . c), e]
≡ H[c, e]
Three more equations describe commutativity of lookups and updates at different distances.
Let ι1 6= ι2 , and write H1 and H2 for the the abbreviation H with respect to ι1 and ι2 ,
respectively:
H1 [H2 [ι1 #lookup () (y1 . ι2 #lookup () (y2 . c)), e2 ], e1 ]
≡ H1 [H2 [ι2 #lookup () (y2 . ι1 #lookup () (y1 . c)), e2 ], e1 ]
H1 [H2 [ι1 #update e1 (_ . ι2 #update e2 (_ . c)), e2 ], e1 ]
≡ H1 [H2 [ι2 #update e2 (_ . ι1 #update e1 (_ . c)), e2 ], e1 ]
H1 [H2 [ι1 #update e (_ . ι2 #lookup () (y2 . c)), e2 ], e1 ]
≡ H1 [H2 [ι2 #lookup () (y2 . ι1 #update e (_ . c)), e2 ], e1 ]
Let us check the last equation. The left-hand side transforms as
H1 [H2 [ι1 #update e (_ . ι2 #lookup () (y2 . c)), e2 ], e1 ]
≡ H1 [ι1 #update e (_ . H2 [ι2 #lookup () (y2 . c), e2 ]), e1 ]
≡ H1 [H2 [ι2 #lookup () (y2 . c), e2 ], e]
≡ H1 [H2 [c[e2 /y2 ], e2 ], e]
and the right-hand side as
H1 [H2 [ι2 #lookup () (y2 . ι1 #update e (_ . c)), e2 ], e1 ]
≡ H1 [H2 [ι1 #update e (_ . c[e2 /y2 ]), e2 ], e1 ]
≡ H1 [ι1 #update e (_ . H2 [c[e2 /y2 ], e2 ]), e1 ]
≡ H1 [H2 [c[e2 /y2 ], e2 ], e].
The remaining two equations are proved much the same way. The symmetry in the equations
also shows that it does not matter in which order we nest the handlers for ι1 and ι2 .
7.2. Commutativity of non-interfering computations. Swapping lookups and updates that act on different instances is only a basic reasoning step. In practice we want
to swap whole computations, as long as they do not interfere. To make the idea precise, let
∆1 = {ι1 #lookup, ι1 #update}, ∆2 = {ι2 #lookup, ι2 #update}, let c1 and c2 be computations

AN EFFECT SYSTEM FOR ALGEBRAIC EFFECTS AND HANDLERS

27

of types A1 ! ∆1 and A2 ! ∆2 , respectively, and c a computation of type C in the context
x1 : A1 , x2 : A2 . We would like to show the equivalence
H1 [H2 [let x1 = c1 in (let x2 = c2 in c), e2 ], e1 ]
≡ H1 [H2 [let x2 = c2 in (let x1 = c1 in c), e2 ], e1 ].
This is a commutativity law which allows us to transpose, or run in parallel, any computations that use only non-interfering references.
First, let us establish a simpler equivalence, which we are going to use in the proof:
H1 [H2 [ι1 #lookup () (y1 . let x2 = c2 in (let x1 = c′1 in c)), e2 ], e1 ]
≡ H1 [H2 [let x2 = c2 in (let x1 = ι1 #lookup () (y1 . c′1 ) in c), e2 ], e1 ]
We proceed by induction on c2 . Since handlers and let are strict, both sides are ⊥ when
we set c2 to ⊥. Next, if c2 is val e2 , the two sides are equal already without handlers:
ι1 #lookup () (y1 . let x2 = val e2 in (let x1 = c′1 in c))
≡ ι1 #lookup () (y1 . let x1 = c′1 in c[e2 /x2 ])
≡ ι1 #lookup () (y1 . let x1 = c′1 in (let x2 = val e2 in c))
≡ let x1 = ι1 #lookup () (y1 . c′1 ) in (let x2 = val e2 in c)
For the induction step, suppose c2 is a call of ι2 #update (the case lookup is similar):
H1 [H2 [ι1 #lookup () (y1 . let x2 = ι2 #update e′2 (z. κ z) in (let x1 = c′1 in c)), e2 ], e1 ]
≡ H1 [ι1 #lookup () (y1 . H2 [let x2 = κ() in (let x1 = c′1 in c), e′2 ]), e1 ]
≡ H1 [H2 [ι1 #lookup () (y1 . let x2 = κ() in (let x1 = c′1 in c)), e′2 ], e1 ]
≡ H1 [H2 [let x2 = κ() in (let x1 = ι1 #lookup () (y1 . c′1 ) in c), e′2 ], e1 ]
≡ H1 [H2 [let x2 = ι2 #update e′2 (z. κ z) in (let x1 = ι1 #lookup () (y1 . c′1 ) in c), e2 ], e1 ].
In the third step we used the induction hypothesis for κ().
We now prove the main statement by induction on c1 . When c1 is ⊥ or a value, the
statement is easy. If c1 is a call of ι1 #lookup, we have:
H1 [H2 [let x1 = ι1 #lookup () (y1 . κ y1 ) in (let x2 = c2 in c), e2 ], e1 ]
≡ H1 [ι1 #lookup () (y1 . H2 [let x1 = κ y1 in (let x2 = c2 in c), e2 )], e1 ]
≡ H1 [H2 [let x1 = κ e1 in (let x2 = c2 in c), e2 ], e1 ]
≡ H1 [H2 [let x2 = c2 in (let x1 = κ e1 in c), e2 ], e1 ]
where in the last step, we used the induction hypothesis for κ e1 . The last line is equivalent
to the other side of the desired equivalence:
H1 [H2 [let x2 = c2 in (let x1 = κ e1 in c), e2 ], e1 ]
≡ H1 [ι1 #lookup () (y1 . H2 [let x2 = c2 in (let x1 = κ y1 in c), e2 ]), e1 ]
≡ H1 [H2 [let x2 = c2 in (let x1 = ι1 #lookup () (y1 . κ y1 ) in c), e2 ], e1 ].
The proof for update is similar.

28

A. BAUER AND M. PRETNAR

8. Formalization in Twelf
We formalized core Eff , the effect system and the safety theorems in Twelf. The files
are enclosed with this paper, or can be found at the GitHub repository [4]. The code is
compatible with Twelf version 1.7.1. Further instructions and description of the code can
be found in the file README.md.
9. Discussion
The only essential feature of Eff that is missing from core Eff is dynamic creation of
instances with the new E construct. We omitted it because it leads to significant complications, both in the effect system and in semantics. One possible treatment of new would be
to upgrade the current setup with nominal logic and nominal domain theory.
Non-termination is a computational effect which is not reflected in our effect system.
It would be interesting to add a “divergence” effect. Such an effect would originate from
applications of recursive functions. However, since divergence cannot be handled it would
never disappear from effect information, and would likely become an uninformative nuisance.
A potential remedy would be to separate general recursive definitions, which may diverge,
from structural recursive definitions, which always terminate.
A realistic implementation of our effect system would only be useful if it actually inferred
computational effects. Such a possibility was explored by the second author [22], and an
early prototype is available in the latest implementation of Eff [5].
Acknowledgment. We thank the anonymous referees for useful suggestions and a lesson
in domain theory.
References
[1] Roberto M. Amadio and Pierre-Louis Curien. Domains and Lambda-calculi. Cambridge University Press,
New York, NY, USA, 1998.
[2] Andrej Bauer and Matija Pretnar. Programming with algebraic effects and handlers. arXiv:1203.1539,
2012.
[3] Andrej Bauer and Matija Pretnar. An effect system for algebraic effects and handlers. In Reiko Heckel
and Stefan Milius, editors, Algebra and Coalgebra in Computer Science, volume 8089 of Lecture Notes
in Computer Science, pages 1–16. Springer Berlin Heidelberg, 2013.
[4] Andrej
Bauer
and
Matija
Pretnar.
Formalization
of
Eff
in
Twelf,
2013.
https://github.com/matijapretnar/twelf-eff .
[5] Andrej Bauer and Matija Pretnar. Eff, 2014. https://github.com/matijapretnar/twelf-eff .
[6] You-Chin Fuh and Prateek Mishra. Type inference with subtypes. Theoretical computer science,
73(2):155–175, 1990.
[7] Ohad Kammar, Sam Lindley, and Nicolas Oury. Handlers in action. In Proceedings of the 18th ACM
SIGPLAN International Conference on Functional Programming, ICFP ’13, pages 145–158, New York,
NY, USA, 2013. ACM.
[8] Ohad Kammar and Gordon D. Plotkin. Algebraic foundations for effect-dependent optimisations. In
John Field and Michael Hicks, editors, POPL, pages 349–360. ACM, 2012.
[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, John Power, and Hayo Thielecke. Modelling environments in call-by-value programming languages. Information and Computation, 185:182–210, September 2003.

AN EFFECT SYSTEM FOR ALGEBRAIC EFFECTS AND HANDLERS

29

[11] J. M. Lucassen and D. K. Gifford. Polymorphic effect systems. In Proceedings of the 15th ACM
SIGPLAN-SIGACT symposium on Principles of programming languages, POPL’88, pages 47–57, New
York, NY, USA, 1988. ACM.
[12] Eugenio Moggi. Notions of computation and monads. Information and Computation, 93(1):55–92, 1991.
[13] Frank Pfenning and Carsten Schürmann. System description: Twelf – a meta-logical framework for
deductive systems. In Harald Ganzinger, editor, CADE-16, 16th International Conference on Automated
Deduction, Trento, Italy, July 7–10, 1999, Proceedings, volume 1632 of Lecture Notes in Computer
Science, pages 202–206. Springer, 1999.
[14] Andrew M. Pitts. Relational properties of domains. Information and Computation, 127(2):66–90, 1996.
[15] Gordon Plotkin and John Power. Adequacy for algebraic effects. In Furio Honsell and Marino Miculan,
editors, Foundations of Software Science and Computation Structures, volume 2030 of Lecture Notes in
Computer Science, pages 1–24. Springer Berlin Heidelberg, 2001.
[16] Gordon 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.
[17] Gordon Plotkin and John Power. Algebraic operations and generic effects. Applied Categorical Structures, 11(1):69–94, 2003.
[18] Gordon Plotkin and John Power. Tensors of comodels and models for operational semantics. In Andrej
Bauer and Michael Mislove, editors, Proceedings of the 24th Conference on the Mathematical Foundations of Programming Semantics (MFPS XXIV), volume 218 of Electronic Notes in Theoretical Computer Science, pages 295–311, 2008.
[19] Gordon D. Plotkin and Matija Pretnar. Handling algebraic effects. Logical Methods in Computer Science,
9(4), 2013.
[20] Gordon David Plotkin and Matija Pretnar. A logic for algebraic effects. In Proceedings of the TwentyThird Annual IEEE Symposium on Logic in Computer Science, LICS 2008, 24-27 June 2008, Pittsburgh,
PA, USA, pages 118–129. IEEE Computer Society, 2008.
[21] Matija Pretnar. The Logic and Handling of Algebraic Effects. PhD thesis, School of Informatics, University of Edinburgh, 2010.
[22] Matija Pretnar. Inferring algebraic effects. Logical Methods in Computer Science, 10(3), 2014.
[23] John Reynolds. The meaning of types—from intrinsic to extrinsic semantics. Technical report, Department of Computer Science, University of Aarhus, 2000.
[24] Jean-Pierre Talpin and Pierre Jouvelot. Polymorphic type, region and effect inference. Journal of functional programming, 2(3):245–271, 1992.
[25] Philip Wadler. The marriage of effects and monads. ACM SIGPLAN Notices, 34(1):63–74, 1999.
[26] Keith Wansbrough and Simon Peyton Jones. Once upon a polymorphic type. In Proceedings of the
26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’99, pages
15–28, New York, NY, USA, 1999. ACM.

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

