Logical Methods in Computer Science
Vol. 10(3:21)2014, pp. 1–43
www.lmcs-online.org

Submitted
Published

Dec. 5, 2013
Sep. 12, 2014

INFERRING ALGEBRAIC EFFECTS
MATIJA PRETNAR
Faculty of Mathematics and Physics, University of Ljubljana, Slovenia
e-mail address: matija@pretnar.info
Abstract. We present a complete polymorphic effect inference algorithm for an ML-style
language with handlers of not only exceptions, but of any other algebraic effect such as
input & output, mutable references and many others.
Our main aim is to offer the programmer a useful insight into the effectful behaviour of
programs. Handlers help here by cutting down possible effects and the resulting lengthy
output that often plagues precise effect systems. Additionally, we present a set of methods that further simplify the displayed types, some even by deliberately hiding inferred
information from the programmer.

Though Haskell [10] fans may not think it is better to write impure programs in ML [18],
they do agree it is easier. You can insert a harmless printout without rewriting the rest
of the program, and you can combine multiple effects without a monad transformer. This
flexibility comes at a cost, though — ML types offer no insight into what effects may happen.
The suggested solution is to use an effect system [16, 29, 4, 31, 33, 3, 27], which enriches
existing types with information about effects.
An effect system can play two roles: it can be descriptive and inform about potential
effects, and it can be prescriptive and limit the allowed ones. In this paper, we focus on
the former. It turns out that striking a balance between expressiveness and simplicity of a
descriptive effect system is hard. One of the bigger problems is that effects tend to pile up,
and if the effect system takes them all into account, we are often left with a lengthy output
listing every single effect there is.
In this paper, we present a complete inference algorithm for an expressive and simple
descriptive polymorphic effect system of Eff [2] (freely available at http://eff-lang.org),
an ML-style language with handlers of not only exceptions, but of any other algebraic
effect [22] such as input & output, non-determinism, mutable references and many others [23, 2]. Handlers prove to be extremely versatile and can express stream redirection,
transactional memory, backtracking, cooperative multi-threading, delimited continuations,
and, like monads, give programmers a way to define their own. And as handlers eliminate
effects, they make the effect system non-monotone, which helps with the above issue of a
snowballing output.
2012 ACM CCS: [Theory of computation]: Semantics and reasoning—Program reasoning—Program
analysis.
Key words and phrases: algebraic effects, effect handlers, effect inference, effect system.

l

LOGICAL METHODS
IN COMPUTER SCIENCE

c
DOI:10.2168/LMCS-10(3:21)2014

CC

Matija Pretnar
Creative Commons

2

MATIJA PRETNAR

We start in Section 1 with an tour of Eff in which we informally explain handlers
and show the main features of the proposed effect system. Afterwards, we switch to formal development and in Section 2, we recap the effect system for core Eff [1], a minimal
formalization of Eff . Our contributions are:
• A set of syntax-directed rules for inferring types and constraints they must satisfy (Section 3). We show that these rules are sound and complete with regard to the effect
system.
• A unification algorithm that decomposes a set of constraints to a more basic form and
decides if it admits a solution (Section 4). Unification fails only in the case of type
mismatch, which fits our goal of a descriptive effect system that just refines existing ML
types with details about effects.
• A number of techniques that reduce the number of constraints without changing the set
of solutions (Section 5). The heavy lifting is done by garbage collection of constraints [25,
28, 32], which we borrow and adapt slightly to our purpose. We also introduce a few
more techniques particular to the algebraic setting.
• A further collection of tactics for simplifying the display of inferred types (Section 6). To
fully achieve their purpose, some of the presented tactics deliberately hide information
from the programmer, though entire information is always used in the background.
We conclude by showing a couple of full runs of the algorithm (Section 7) and by discussing
related and future work. To preserve the flow of the paper, we gather the (mostly routine)
proofs in Appendix A.
1. Eff
Effects aside, Eff should be familiar to anyone that has worked with OCaml [9]. For example,
the map function, which applies a function f to each element of the list xs is defined as:
let rec map f xs =
match xs with
| [] -> []
| x :: xs -> f x :: map f xs

The first important feature that distinguishes Eff from OCaml is its effect system. For
example, the inferred type of map is
δ

δ

map : (α −
→ β) −
→ (α list −
→ β list)
Here, the annotation on the arrow, called the dirt, describes any effects that the function
may trigger. This additional information is very easy to understand: the function map f
causes exactly the same effects δ as f. The lack of dirt on the second arrow signifies that the
application of map to f is pure. Inferred types of some other typical higher-order functions

INFERRING ALGEBRAIC EFFECTS

3

are:
δ′

δ

δ∪δ′

compose : (α −
→ β) −
→ (β −
→ γ) −
→ (α −−→ γ)
δ

δ

curry : (α × β −
→ γ) −
→ (α −
→β−
→ γ)
δ

δ′

δ∪δ′

δ

δ′

δ∪δ′

δ

δ′

δ∪δ′

uncurry : (α −
→β−
→ γ) −
→ (α × β −−→ γ)
→β−
→ α) −
→α−
→ β list −−→ α
fold left : (α −
→β−
→ β) −
→ α list −
→ β −−→ β
fold right : (α −
δ

δ

filter : (α −
→ bool) −
→ (α list −
→ α list)
The dirt annotations are similar to ones usually given in existing polymorphic effect systems such as [14]. Also note that if we disable the display of annotations, Eff shows the
programmer exactly the same types as OCaml.
The second distinguishing feature is that Eff is based on algebraic effects [21, 22]. This
means that effects are accessed exclusively through a set of operations, which are all of
the form ins#op, where an operation symbol op describes the action, and an instance ins
describes where it should happen. This means that we print to the standard output channel
using an operation std#print instead of a primitive function print_string, we access a
reference r through operations r#lookup and r#update instead of through ! and :=, and
we raise an exception exc by calling exc#raise instead of using a special keyword raise.
The latter constructs are, of course, all definable in terms of the former.
This uniform representation allows effects to be seamlessly combined [8], forms a natural
basis for an effect system — possible effects of a given computation are captured accurately
by the set of operations it calls — and paves the way for the third distinguishing feature of
Eff : handlers of arbitrary algebraic effects [23].
Let us take a look at a few concrete examples. What follows is by no means an exhaustive list of what can be accomplished with handlers. For more examples, please see [23, 2, 11].
1.1. Exceptions. We start with exceptions as they are the simplest algebraic effect and as
exception handlers are already a well established concept.
1.1.1. Effect types. Instances are first-class values in Eff and are given an effect type. For
exception instances, called simply exceptions, the effect type is of the form α exception,
where α is the type of any additional information that the exception may carry.
We declare each effect type together with an effect signature that lists available operation symbols together with the types of parameters they accept and of results they yield to
the waiting continuation. The signature corresponding to α exception is
{raise : α −
→ empty}
where the result type of raise is empty (a sum type with zero constructors) because raising
an exception terminates the computation and yields nothing to the continuation.
Each term of an effect type is also annotated with a region, which describes (an overapproximation of) the set of instances it may occupy. For example, an exception exc1 is
given the type α exception{exc1} , while the conditional if cond then exc1 else exc2 is
given the type α exception{exc1,exc2} (any bigger sets would also be fine).

4

MATIJA PRETNAR

1.1.2. Raising exceptions. Since there is little we can do with a result of the empty type, we
rarely raise exceptions directly with exc#raise. Instead, we define a convenience function,
also named raise, which places the exception call inside the empty type eliminator:
let raise exc arg =
match ( exc # raise arg ) with

with the inferred type
raise:ρ

raise : α exceptionρ −
→ α −−−−→ β
So, raise takes an exception from a region captured by a region parameter ρ and a matching
argument of type α. The second application results in a computation that can raise any
exception from ρ, while its return type β can be any arbitrary. This allows us to use raise
at any point in the computation, for example in computing the tail of a list:
let tail xs =
match xs with
| [] -> raise e m p t y L i s t T a i l
| _ :: xs -> xs

where emptyListTail is the exception stating that the empty list has no tail. The inferred
type of tail is
raise:{emptyListTail}

tail : α list −−−−−−−−−−−−−−→ α list
where the dirt shows that emptyListTail may be raised during execution.
In addition to inferring types of values, we can also infer dirty types A ! ∆ of computations. These consist of a value type A describing the result and of a dirt ∆ describing
the operations that may be called while computing it. For example, the inferred dirty type
of the computation tail [1; 2; 3] is int list ! {raise : {emptyListTail}}. Note that
the effect system is conservative and signals a possible exception even though it will not
be raised during runtime. This also means that a computation is guaranteed to be pure
whenever its inferred dirt is empty.
For a final example of the effect system before we turn to handlers, let us combine map
and tail as
let m a p _ t a i l f xs = map f ( tail xs )

with the inferred type
raise:ρ|δ

raise:{emptyListTail}∪ρ | δ

→ (α list −−−−−−−−−−−−−−−−−→ β list)
map tail : (α −−−−−→ β) −
Unlike the argument to map, the argument of map_tail has its dirt split into two parts:
the region parameter ρ captures the region of all the exceptions that f may raise, while
the dirt parameter δ captures all other operations. The split allows us to express the fact
that map_tail f may raise either emptyListTail or an exception from ρ, and that it may
call any operation from δ that f can. This is similar to row typing [26], where we use a
parameter to capture all the fields of a record that are not explicitly mentioned.

INFERRING ALGEBRAIC EFFECTS

5

1.1.3. Handling exceptions. As exceptions are the simplest example of effects, exception
handlers are the simplest example of handlers. A try with handling construct known from
OCaml, like the one in
let p r i n t _ r a t i o x y =
try
p r i n t _ s t r i n g ( " Ratio is " ^ s t r i n g _ o f _ f l o a t ( x /. y ))
with
| D i v i s i o n _ b y _ z e r o -> p r i n t _ s t r i n g " Ratio does not exist ! "

would be used in Eff as
let p r i n t _ r a t i o x y =
handle
std # print ( " Ratio is " ^ s t r i n g _ o f _ f l o a t ( x /. y ))
with
| d i v i s i o n B y Z e r o # raise _ _ -> std # print " Ratio does not exist ! "

Each handler case takes two arguments which we ignore for now.
Like instances, handlers are first-class values in Eff , and the above is just special syntax
for
let p r i n t _ r a t i o x y =
with h handle
std # print ( " Ratio is " ^ s t r i n g _ o f _ f l o a t ( x /. y ))

where h is given by
handler
| d i v i s i o n B y Z e r o # raise _ _ -> std # print " Ratio does not exist ! "

Handlers are given handler types A ! ∆ ⇒
= B ! ∆′ , meaning that a handler takes a computation with incoming dirty type A ! ∆ and transforms it into a computation with outgoing
dirty type B ! ∆′ . The inferred type for h is
unit ! {raise : ρ1 , print : ρ2 | δ} =
⇒
unit ! {raise : ρ1 − divisionByZero, print : {std} ∪ ρ2 | δ}
We see that h leaves the type of results to be unit. Its incoming dirt is split into three
parts: exceptions ρ1 that we may raise, channels ρ2 that we may print to, and any other
operations δ different from raise or print that we may call. The outgoing dirt is similarly split: the handled computation may still raise exceptions from ρ1 , except that now
divisionByZero will be handled. Next, the handled computation may print to std in addition to any channel in ρ2 . Finally, any operation in δ will be neither caught nor called by
h, so this part remains as it is.
Handler types usually (but not always) all have the same shape: they remove certain
operations, possibly add some of their own, and pass through any unhandled dirt. This
results in a repetitive type, which can be written in a more compact form that emphasises
only the differences. For h, this is:
raise:−divisionByZero, print:+std

unit ======================⇒ unit
So, h removes divisionByZero#raise, adds std#print, and leaves the rest as it is.

6

MATIJA PRETNAR

In practice, exception handlers are rarely reused, because treatment of exceptions varies
greatly depending on the context in which they are handled. An example of a more general
exception handler is optionalize, which transforms a computation into one that yields
an optional result, depending on if a given exception exc was raised or not. We define
optionalize as:
let o p t i o n a l i z e exc =
handler
| exc # raise _ _ -> None
| val x -> Some x

The first thing to notice is the special val case, which determines what to do when the
handled computation returns a value. In our case, we wrap it with the Some constructor of
the option type. Then, if we define
let t a i l _ o p t xs =
with ( o p t i o n a l i z e e m p t y L i s t T a i l ) handle ( tail xs )

the call tail_opt [1; 2; 3] evaluates to Some [2; 3], while tail_opt [] evaluates to
None. The inferred type of tail_opt is the pure α list −
→ (α list) option, while the type
of optionalize is
raise:´ρ

optionalize : α exceptionρ −
→ (β =====⇒ β option)
So, we change the result type from β to β option, and remove any call of exc#raise for
the exception exc determined by the region ρ.
1.1.4. Handled regions. You may have observed that we wrote ´ρ instead of −ρ in the type
of optionalize. This is meant to point out that we may remove ρ from the dirt only if it
denotes a singleton. The reason for this is as follows.
Take exceptions exc1 and exc2 and define a handler h as:
let exc = if cond then exc1 else exc2 in
let h =
handler
| exc # raise _ _ -> ...

So, does the exc#raise case of h handle exc1#raise or exc2#raise at runtime? Unfortunately, just by looking at the type exc : α exception{exc1,exc2} , we cannot say anything,
so we must assume that both are unhandled. The only way we can be sure during typechecking that a handling case removes a given operation is when the region of its instance
is a singleton.
For this reason, we write ´ρ whenever the region of the handled instance is still some
parameter ρ. If this eventually turns out to denote some singleton {ins}, we may safely
replace it by −ins. But if it turns to be a bigger set, we need to drop it from the handler
type.

INFERRING ALGEBRAIC EFFECTS

7

1.2. Input & output. Interactive input & output is also a very simple algebraic effect, yet
its handlers expose almost all the important aspects of general ones. For input & output,
the effect instances are called channels and have the effect type channel with the signature
{read : unit −
→ string, print : string −
→ unit}
A simple output handler is one that reverses the order of printouts:
handler
| std # print msg k -> k (); std # print msg

The std#print case takes two parameters: the string msg given to std#print and the
continuation k waiting for its result. We first resume the continuation by passing it the
unit value (), and only after that finishes, we print out msg. The handler recursively
handles any other std#print that the continuation may call, so the order of printouts in
the continuation is reversed as well. Note, however, that std#print on the right-hand side
is outside the scope of the handler and remains unhandled (unless there are more handlers
nested outside).
A more interesting example that can be useful in unit testing is a handler that collects
all printouts to a list of strings and returns it together with the result:
handler
| val x -> (x , [])
| std # print msg k ->
let (x , msgs ) = k () in
(x , msg :: msgs )

So, a computation that just returns the value x prints nothing, and we return an empty
list [] together with x. If, however, the computation prints the string msg, we resume the
continuation k. This is also handled with the same handler, so it returns some value x and
a list of its messages msgs. Now, we only need to prepend msg to this list and return it
together with x. The fact that the handler changes the type of the handled computation is
print:−std
reflected in its inferred type α =======⇒ α × string list.
A matching handler that is also useful in unit testing is one that feeds a list of strings
to std#read:
handler
| val x -> ( fun strs -> x )
| std # read () k -> ( fun strs ->
match strs with
| str :: strs ’ -> ( k str ) strs ’
| [] -> ( k " " ) []
)

We accomplish this by transforming a computation into a function that accepts a list of
strings strs. If the computation returns some value x, the function ignores its argument
and returns x. But if the computation calls std#read, we take a look at the list strs. If it
is non-empty, we pass k its first element str. And since the continuation is further handled,
it is also a function that accepts a list of strings, so we pass it the remainder strs’. If it is
empty, we pass k the empty string and again the empty list.
The inferred type of the handler is
∆

α ! {read : ρ | δ} =
⇒ (string list −
→ α) ! ∆

8

MATIJA PRETNAR

where ∆ = {read : ρ − std | δ}. The reason ∆ appears in two places is because operations
other than std#read may occur before or after we handle the first std#read and so obtain
a function. Since ∆ appears twice, we unfortunately cannot use the compact form.
However, Eff extends handlers with an additional finally case, which first transforms
the computation with the handler, and then applies the finally case computation to the
resulting value. In particular, if h is some handler and h_fin is the same as h except that it
also contains a case finally x -> c_fin, the computation with h_fin handle c behaves
exactly as
let x = ( with h handle c ) in c_fin

Using this extension, we can define
let s u p p l y _ i n p u t strs0 =
handler
| val x -> (* ... as before ... *)
| std # read () k -> (* ... as before ... *)
| f i n a l l y f -> f strs0

So, once we get back a function f accepting a list of inputs, we apply it to the given list
strs0. We use the handler as
with
s u p p l y _ i n p u t [ " Alpha " ; " Bravo " ; " C h a r l i e" ]
handle
...

The inferred type then takes the simpler form
read:−std

→ (α ======⇒ α)
supply input : string list −
1.3. References. Similar to OCaml, mutable references in Eff are given the effect type
α ref with the signature
{lookup : unit −
→ α, update : α −
→ unit}
We can define the OCaml accessors by:
let (!) r = r # lookup ()
let (:=) r v = r # update v

with the types
lookup:ρ

(!) : α refρ −−−−−→ α

update:ρ

(:=) : α refρ −
→ α −−−−−→ unit

With reference handlers, we can temporarily alter the value stored in the reference, make it
read-only, log all changes, and more. However, handlers are not meant only for overriding
but also for defining effects. In particular, we can use handlers to implement references with
a state monad:
let state r s0 =
handler
| val x -> ( fun s -> x )
| r # lookup () k -> ( fun s -> k s s )
| r # update s ’ k -> ( fun s -> k () s ’)
| f i n a l l y f -> f s0

INFERRING ALGEBRAIC EFFECTS

9

The function state gives a handler that handles a stateful computation using reference r
into a pure function that accepts the current state s and passes it around. So, we handle
lookup by a function that takes the state s and passes it to the continuation k, which
expects the current state as the outcome of lookup. Since this continuation is further
handled, it is again a function accepting current state. Looking up a reference does not
change the state, so we pass s again, thus k is applied to s twice. In the case for update,
the expected outcome of the call is the unit value, while the current state is overwritten by
the parameter s’. And the finally case says that once we get back a function accepting
current state, we apply it to a given initial state s0.
The inferred type of state is
lookup:´ρ,update:´ρ

state : α refρ −
→α−
→ (β =============⇒ β)
If we want to access the final state, we define state’ to be exactly the same as state,
except that its value case is val x -> (fun s -> (x, s)). In this case the inferred type
is
lookup:´ρ,update:´ρ
state’ : α refρ −
→α−
→ (β =============⇒ β × α)
We can use multiple references without a hitch. For example, given two references r1
and r2, the computation
with ( state r1 6) handle
with ( state r2 0) handle
let x = ! r1 in
r2 := x + 1;
! r2 * x

returns 42 and its inferred type is the pure int ! ∅.
If we replace state by state’, the handled computation returns (6, (7, 42)) and
the inferred type is int × (int × int) ! ∅. This shows how easy it is to change the effectful
behaviour by just switching the handlers and keeping the imperative code as it is.
2. Core Eff
For formal development, we restrict our attention to core Eff, a minimal fragment of Eff .
Core Eff differs from Eff in the following aspects:
• Core Eff is a fine-grain call-by-value calculus [15], which means that its terms are split
into inert expressions and possibly effectful computations. The separation makes the
formalization much simpler, but makes programming that much harder. For this reason,
Eff allows the programmer to freely mix the terms, and performs the routine separation
automatically. For example, a program such as
let t r a n s f o r m f m n = ( f m 42 , n )

gets translated into
let t r a n s f o r m = fun f -> val ( fun m -> val ( fun n ->
let tmp1 =
let tmp2 = f m in
tmp2 42
in
val ( tmp1 , n )
))

10

MATIJA PRETNAR

where val constructs a computation that immediately returns a value represented by a
given expression.
• Eff allows programmers to define their own parametric inductive datatypes and effect
types, while in core Eff , we fix the signature of effect types and drop inductive datatypes
entirely.
• Eff provides a new construct that allows a programmer to create fresh instances at runtime [2], and can be used to model both exception declarations and reference allocations
in ML. Since the formalization of this feature is still under investigation, we omit it from
our development and only briefly discuss it in the Conclusion.
• Handlers in Eff allow the additional finally case in handlers, but as already discussed
on page 8, this is merely a convenience that can be expressed with existing constructs.
2.1. Terms. We start with a given set of effects E, which are just labels such as channel,
exception or ref for all possible effects we want to use in our programs. Next, for each
effect E, we have a fixed set OE of operation symbols op and a fixed set IE of instances ins.
We assume that in each operation ins#op, both ins and op belong to the same effect.
The expressions e and computations c of core Eff are given by:
expression e :: = x

true

false

0

succ e

()

fun x 7→ c

ins

h

handler h :: = (handler val x 7→ cv |(ei #opi x k 7→ ci )i )
computation c :: = if e then c1 else c2
val e

iszero e

pred e

e1 #op e2 (y. c)

let x = c1 in c2

let rec f x = c1 in c2

with e handle c

absurd e

e1 e2

let val x = e in c

Here and everywhere, we write (−)i∈I or just (−)i to denote a finite repetition of −. The
language constructs are standard except for: the empty type eliminator absurd, the computation val that immediately evaluates to a value, polymorphic let-binding let val, and the
already discussed instance constants, handlers, operation calls and the handling construct.
Note that both instance constants and handlers are first-class values in core Eff .
The operation calls in core Eff are slightly different from the ones in Eff . The
call ins#op e (y. c) represents an application of an operation ins#op to a parameter e with a
continuation (y. c) waiting for the result of the call to be bound to y. Explicit continuations
are convenient for operational semantics, but we do not expect the programmer to use them.
Instead, Eff uses generic effects [22], defined as
def

e#op = fun x 7→ e#op x (y. val y)
which take a parameter and perform the operation call with the trivial continuation. Then,
the programmer can write the more familiar let y = ins#op e in c instead of ins#op e (y. c),
and we shall see that the two exhibit equivalent behaviour.
The rough idea is that each non-divergent computation either evaluates to a value or
calls an operation. We use a handler h = handler val x 7→ cv |(insi #opi x k 7→ ci )i on a
computation c as follows:
• If c evaluates to a value val e, we use the value case and evaluate cv [e/x].
• If c performs an operation call insj #opj e (y. c′ ) and the handler contains a matching
case insj #opj x k 7→ cj , we evaluate cj [e/x, (fun y 7→ with h handle c′ )/k]. We wrap

INFERRING ALGEBRAIC EFFECTS

11

the handler h around the continuation so that it may continue handling future operation
calls, though any operations called by cj escape its scope.
• If the handler has no matching operation cases for the called operation, then just like in
exception handlers, we propagate the call outwards for other handlers to catch, though
we still wrap h around the continuation as it may handle some other operations.
Let-binding let x = c1 in c2 works as follows: if c1 evaluates to val e, we continue
with c2 [e/x], but if c1 calls an operation, we propagate the call outwards just like when
a handler has no matching cases. In fact, let-binding let x = c1 in c2 works exactly as
with (handler val x 7→ c2 ) handle c1 Though this makes let binding redundant, we keep it
in the language for convenient notation and to serve as a stepping stone to the less familiar
handling construct.
To make the above intuition more precise and to motivate the effect system, we now
give a small-step operational semantics, determined by a relation c
c′ defined in Figure 1,
stating that a computation c takes a single step to c′ . Note that the relation is given for
computations only and that expressions are inert.
if true then c1 else c2
iszero (succ e)

(fun x 7→ c) e

c[e/x]

c1

if false then c1 else c2
pred 0

val false
c1
let x = c1 in c2

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

val 0

c′1
let x = c′1 in c2

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

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

c2

iszero 0
pred (succ e)

val true
val e

let x = val e in c
let val x = e in c

c[e/x]
c[e/x]

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

c′
with e handle c′

with h handle (insj #opj e (y. c))

with h handle (val e)

cv [e/x]

cj [e/x, (fun y 7→ with h handle c)/k]

ins#op 6∈ {insi #opi }i
with h handle (ins#op e (y. c))
ins#op e (y. with h handle c)

Figure 1: The inductive definition of the relation c
c′ . In the last three rules, we set
h = handler val x 7→ cv |(insi #opi x k 7→ ci )i .
Example 2.1. Take a reference handler
def

h = handler
| val x 7→ r#update x
| r#lookup x k →
7 k (succ 0)
| r#update x k →
7 k ()

12

MATIJA PRETNAR

which temporarily treats a reference r ∈ Iref as if it always contains 1, and afterwards
updates it with the final result of the handled computation. This update is not handled
by h because it escapes its scope. If we apply h on the computation
def

c = let x1 =
let x2 = r#lookup () in
r#update x2
in val 0
the outcome of the first lookup is 1, which is then bound to x2 , while the handler continues
handling the continuation. Then, the update is ignored and finally, the handler applies
the value case on 0 and terminates with a call of r#update. Note that Eff provides resources [2], which at this point trigger real-world effects and resume the continuation. The
exact reduction sequence is given in Figure 2.
with h handle
let x1 = (let x2 = r#lookup () in r#update x2 ) in val 0
with h handle
let x1 = (let x2 = r#lookup () (y1 . val y1 ) in r#update x2 ) in val 0
with h handle
let x1 = r#lookup () (y1 . let x2 = val y1 in r#update x2 ) in val 0
with h handle
r#lookup () (y1 . let x1 = (let x2 = val y1 in r#update x2 ) in val 0)
(fun y1 7→ with h handle (let x1 = (let x2 = val y1 in r#update x2 ) in val 0)) 1
with h handle (let x1 = (let x2 = val 1 in r#update x2 ) in val 0)
with h handle (let x1 = r#update 1 in val 0)
with h handle (let x1 = r#update 1 (y2 . val y2 ) in val 0)
with h handle (r#update 1 (y2 . let x1 = val y2 in val 0))
(fun y2 7→ with h handle (let x1 = val y2 in val 0)) ()
with h handle (let x1 = val () in val 0)
with h handle (val 0)

r#update 0

r#update 0 (y3 . val y3 )

Figure 2: The evaluation of with h handle c, as described in Example 2.1. We underline
the active parts of each step and shorten succ 0 to 1. We can see how the
operation call to r#lookup in the first line propagates outwards to the matching
handler while its continuation builds up. Once the call reaches a handler, it is
replaced with the handling term in which k is replaced by the further handled
continuation.

INFERRING ALGEBRAIC EFFECTS

13

2.2. Types. The types, which are also split into pure and potentially effectful (here called
dirty) ones, are given by
type A, B :: = bool
dirty type C, D :: = A ! ∆

nat

unit

empty

A−
→C

ER

C=
⇒D

We have the usual ground types and the function type A −
→ C of functions that take
expressions of type A and perform computations of type C. Next, we have the effect
type E R of instances of effect E from a region R, which is just a non-empty finite set of
instances {ins1 , . . . , insn } ⊆ IE . Finally, we have the handler type C =
⇒ D of handlers
that take a computation of type C and transform it into a computation of type D. We call
C the incoming and D the outgoing type. Finally, dirty type A ! ∆ contains computations
that return values of type A and may cause effects described by a dirt ∆, which is a set of
operations
{ins1 #op1 , . . . , insn #opn }
∆

To lighten the syntax, we write A1 −
→ A2 ! ∆ as A1 −
→ A2 where we also omit the outer
braces around ∆.
Note that for simplicity, the types of core Eff are monomorphic. However, we are going
to shift to polymorphic types with type, region and dirt parameters when we start with
type inference in Section 3.
2.3. Subtyping. As in most effect systems, we need to take care of the poisoning problem [34]. For example, what type should we give to ignore in
let ignore = val (fun msg 7→ val ()) in
let f = if b then (val ignore) else (val std#write) in
val ignore
for some suitable boolean b? If we give it the type string −
→ unit (for this example, we
allow ourselves the type string of strings), we cannot type the conditional statement as the
std#write
two branches cannot have the same type, but if we give it the type string −−−−−−→ unit,
we lose information that the final result is a pure function.
The simplest antidote for the poisoning problem is to allow subtyping, so that we may
give ignore the type with an empty dirt, and use subsumption to suitably enlarge this dirt
in the conditional statement.
Subtyping also solves a similar problem with regions of handled instances. Consider
the computation
let u = val ins in
let v = if b then val u else val ins′ in
val (handler val x 7→ · · · | u#op x k 7→ · · · )
′

Without subtyping we are forced to give both u and v the type E {ins,ins } . Therefore,
as discussed in Section 1.1.4, the type of u does not tell us whether h handles ins#op or
ins′ #op, and so we must assume that both may remain unhandled. With subtyping we may
give u the type E {ins} , which makes it clear that h handles ins#op.
For our purposes, it is enough to use structural subtyping [7], where we relate only
types of the same shape. The subtyping relations between types and between dirty types

14

MATIJA PRETNAR

Sub-bool

Sub-nat

Sub-unit

Sub-empty

bool 6 bool

nat 6 nat

unit 6 unit

empty 6 empty

Sub-E
R ⊆ R′
ER 6 ER

′

Sub-=
⇒
D 6 D′
C′ 6 C
⇒ D′
C=
⇒ D 6 C′ =

Sub-−
→
A′ 6 A
C 6 C′
A−
→ C 6 A′ −
→ C′

Sub-!
A 6 A′
∆ ⊆ ∆′
A ! ∆ 6 A′ ! ∆′

Figure 3: The inductive definition of the subtyping relations A 6 A′ and C 6 C ′ .

are defined in Figure 3. Sometimes, we shall be interested in types that have the same
shape. So, we define ≈ as the equivalence relation on types, generated by 6. Equivalence
classes of ≈ are called skeletons [28].
2.4. Effect system. Our effect system is built on two typing judgements, defined in Figure 4. The judgement Γ ⊢Σ e : A states that in context Γ and signature Σ, an expression e
has a type A. The judgement Γ ⊢Σ c : C states a similar thing for a computation c and
a dirty type C. In both cases, the context Γ is a unique assignment of (pure) types to
variables, while the signature Σ consists of effect signatures Σ(E) for each effect E. These
are of the form
{op1 : Aop1 −
→ B op1 , . . . , opn : Aopn −
→ B opn }
and assign a parameter type Aop and a result type B op to each listed operation op. For
example, the effect signatures for references is:
Σ(ref) = {lookup : unit −
→ nat, update : nat −
→ unit}
For technical reasons, we assume that both the parameter and the result type for each
operation do not contain any regions or dirt, which limits them to the basic ground types
such as nat or unit. We further discuss this restriction in Remark 3.4.
The purpose of the presented effect system is to offer guarantees on the behaviour
of programs, not (yet) to lead to an efficient inference algorithm. One sign of that is
rules like Val, Inst or Pred, where we assign types that are safe, but much coarser than
needed. A more obvious sign is the rule LetVal, where we employ a very naive form
of let-polymorphism that performs an explicit substitution. This is, of course, extremely
inefficient, but lets us postpone the use of parameters to the inference rules, which use the
more efficient variant with universally quantified types.
All the typing rules are standard except for:
Inst: in which we check that ins is contained in the region R that belongs to an effect E.
Op: in which we first check that e1 and op belong to the same effect. Then, we need to
check that the dirt ∆ 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 and Let.
With: where the handling construct is typed like an application, except that it is applied
to a computation rather than an expression.

INFERRING ALGEBRAIC EFFECTS

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

15

True

False

Zero

Γ ⊢ true : bool

Γ ⊢ false : bool

Γ ⊢ 0 : nat

Fun

Unit

Inst
ins ∈ R ⊆ IE

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

Γ ⊢ () : unit
SubExpr
Γ⊢e:A
A 6 A′
Γ ⊢ e : A′

Γ ⊢ ins : E R

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

Pred
Γ ⊢ e : nat
Γ ⊢ pred e : nat ! ∆

Absurd
Γ ⊢ e : empty
Γ ⊢ absurd e : C

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

Hand — in the text
IsZero
Γ ⊢ e : nat
Γ ⊢ iszero e : bool ! ∆

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

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

op

Γ ⊢ e2 : A

Γ ⊢ e1 : E R
op : Aop −
→ B op ∈ Σ(E)
op
Γ, y : B ⊢ c : A ! ∆
∀ins ∈ R. ins#op ∈ ∆
Γ ⊢ e1 #op e2 (y. c) : A ! ∆

Let
Γ ⊢ c1 : A ! ∆
Γ, x : A ⊢ c2 : B ! ∆
Γ ⊢ let x = c1 in c2 : B ! ∆

LetVal
Γ⊢e:A
Γ ⊢ c[e/x] : C
Γ ⊢ let val x = e in c : C

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

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

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

Figure 4: The inductive definition of the typing judgements Γ ⊢Σ e : A and Γ ⊢Σ c : C.
As the signature Σ does not change, we omit its display from all the judgements.
The rule for handlers is given in the main text.

Hand: which is a bit more daunting, so we write it out separately:
Hand

Γ, x : A ⊢ cv : B ! ∆′
(Ψi )i
Ψ∆
Γ ⊢ (handler val x 7→ cv |(ei #opi x k 7→ ci )i ) : A ! ∆ ⇒
= B ! ∆′
For a handler to be of type A ! ∆ ⇒
= B ! ∆′ , we first check that it takes values of type A
′
to computations of type B ! ∆ . Then, for each operation case ei #opi x k 7→ ci , we check
the premises Ψi , comprising:
Γ ⊢ ei : EiRi

opi : Aopi −
→ B opi ∈ Σ(Ei )

Γ, x : Aopi , k : B opi −
→ B ! ∆′ ⊢ ci : B ! ∆′

16

MATIJA PRETNAR

Like in Op, we check that ei and opi belong to the same effect Ei . Then, the handling
computation ci needs to have the same type B ! ∆′ , assuming that parameter x is of type
Aopi , and the continuation k of type B opi −
→ B ! ∆′ . Observe that since the continuation
is further handled, it already has the outgoing type.
Finally, in Ψ∆ we check that any operation in the incoming dirt ∆ that is not guaranteed to be caught by the handler must appear in the outgoing dirt ∆′ as well. As
discussed in Section 1.1.4, an operation ins#op will be (if not sooner) surely caught by
the case for insi #opi whenever op = opi and the region Ri is the singleton {insi }. Thus,
we define Ψ∆ to be
[
Ri ) ∨ (ins#op ∈ ∆′ )
∀ins#op ∈ ∆. (ins ∈

·

op=opi

where the singleton union ∪· behaves like a union, except that it considers only singletons. For example, {ins1 , ins2 } ∪· {ins2 } ∪· {ins3 , ins4 } ∪· {ins5 } = {ins2 , ins5 }. More
precisely, we define:
[
Ri = {ins | {ins} ∈ {Ri }i }

·

i

The given effect system is then safe with respect to the operational semantics: a computation
⊢ c : A ! ∆ can only call operations from ∆. In particular, if ∆ is empty, then c is guaranteed
to be pure, though it may diverge.
Theorem 2.2 (Safety). If for a computation c, the typing judgement ⊢ c : A ! ∆ holds,
then either:
• c is of the form val e for some expression ⊢ e : A, or
• c is of the form ins#op e (y. c′ ) for some ins#op ∈ ∆, or
• there exists a computation c′ such that c
c′ and ⊢ c′ : A ! ∆.
We do not give a proof of Theorem 2.2 in this paper. Instead, a full formalization of
core Eff in Twelf is available at https://github.com/matijapretnar/twelf-eff/
Example 2.3. To illustrate the type system, let us revisit Example 2.1. First, assume that
the reference r ∈ Iref is given the type ref{r} . Then, the stateful computation c has the
dirty type nat ! {r#lookup, r#update}, while the handler h has the type
(nat ! {r#lookup, r#update}) =
⇒ (unit ! {r#update})
as it handles both lookup and update, but then triggers update in the value case. This
update also changes the type of computation from nat to unit.
′
If the reference r has a less precise type ref{r,r } , the dirt of c is
def

∆ = {r#lookup, r ′ #lookup, r#update, r ′ #update}
while the best type we can give to h is (nat ! ∆) ⇒
= (unit ! ∆). Since the region of r is not
a singleton, we unfortunately cannot give any guarantees on the handled operations.
3. Inferring constraints
Turning to our inference algorithm, we first describe a collection of syntax-directed inference
rules that are readily transcribed into a recursive function that infers a type and a set of
constraints from a given term.

INFERRING ALGEBRAIC EFFECTS

17

3.1. Parametric types. As indicated in Section 2.2, we switch to a language that is more
suited for inference:
type A, B :: = α bool
dirty type C, D :: = A ! ∆

nat

unit

empty

A−
→C

E ρ̇

C=
⇒D

dirt ∆ :: = {op1 : ρ1 , . . . , opn : ρn | δO }
From now on, we refer to types and dirt from Section 2.2, which contain no parameters, as
closed ones.
To enable polymorphism, types are extended with the type parameters α. Then, regions
are not just extended, but completely replaced with region parameters ρ, as this greatly
simplifies the inference. We are going to capture the information about instances using
constraints instead. Recall that regions R describing the possible instances in an effect type
E R are always inhabited. This information will prove useful in Section 5 as it allows further
simplification. For this reason, we designate a special subset of region parameters, called
inhabited and marked by ρ̇.
Finally, we adopt a row-like [26] representation of dirt as described in Section 1.1.2. The
first part is a set of operation symbols together with a region parameter that captures the
(possibly empty) region of all the instances on which these symbols are used. This is similar
to before, except that operations are grouped by their operation symbols. The reason for
this grouping is that we are always able to precisely determine the operation symbols, but
not the instances of called or handled operations.
The second part consists of a single dirt parameter δ, intended to capture the rest of
operations. If the first part is empty, we write the dirt simply as δ. To keep track of the
operation symbols captured by δ and ensure that it does not capture any symbols from the
first part, we sometimes write the parameter as δO to emphasise the set O of symbols not
captured by δ (though O can always be reconstructed by looking at the first part of any
dirt in which δ appears because our algorithm ensures that all such dirts consistently list
the same operation symbols).
Any additional information is captured with constraints. For example, a conditional can
call any operation that one of its branches does. If these two branches cause dirt captured
by δ1 and δ2 , we can represent the dirt of the whole conditional with a fresh parameter δ
together with constraints δ1 6 δ and δ2 6 δ. Constraints can be of one of the following five
kinds:
• A 6 A′ states that the type A needs to be smaller than A′ ,
the same for dirty types,
• C 6 C ′ states
S
• ρ 6 ρ′ ∪ i ρ̇i is a generalisation of the inequality ρ 6 ρ′ due to handlers. It states that
′
all instances
S from ρ are either in ρ or in some ρ̇i that is a singleton,
• ins ∈ ρ ∪ i ρ̇i similarly states that ins is either in ρ or in some ρ̇i that is a singleton,
• ∆ 6 ∆′ states that the dirt ∆ is smaller than ∆′ .
S
In the right-hand side ρ ∪ i ρ̇i of two region constraints, we refer to ρ as the covering, and
to ρ̇i as the handled region parameters.
Unlike the subtyping relation, constraints do not have any inherent reasoning principles,
but are just a way of writing down the relationship between parameters. Instead, we give
constraints a meaning by specifying their solutions.

·

·

·

Definition 3.1. A closed substitution σ is a partial mapping that maps: each type parameter α to a closed type σ(α), each region parameter ρ to a closed region σ(ρ), each inhabited

18

MATIJA PRETNAR

region parameter ρ̇ to a non-empty closed region σ(ρ̇), and each dirt parameter δO to a
closed dirt σ(δO ) that contains no operations with operation symbols in O.
We write substitutions by specifying a set of mappings of parameters, for example
{α1 7→ nat, α2 7→ unit, ρ 7→ ∅, δ 7→ {ins#op}}
We can extend a closed substitution to other constructs by:
σ(bool) = bool
σ(A −
→ C) = σ(A) −
→ σ(C)
σ(E ρ̇ ) = E σ(ρ̇)

σ(nat) = nat
σ(unit) = unit

⇒ D) = σ(C) =
⇒ σ(D)
σ(C =

σ(empty) = empty

σ(A ! ∆) = σ(A) ! σ(∆)

σ({op1 : ρ1 , . . . , opn : ρn | δ}) =

n
[


{ins#opi | ins ∈ σ(ρi )} ∪ σ(δ)

i=1

Definition 3.2. A closed substitution σ is a solution of a set of constraints C, which we
write as σ |= C, if it satisfies all the constraints in C. This is defined by:
σ |= A 6 A′ ⇐⇒ σ(A) 6 σ(A′ )
σ |= C 6 C ′ ⇐⇒ σ(C) 6 σ(C ′ )
[
[
σ |= ρ 6 ρ′ ∪
ρ̇i ⇐⇒ σ(ρ) ⊆ σ(ρ′ ) ∪
σ(ρ̇i )
[i
[ i
σ |= ins ∈ ρ ∪
ρ̇i ⇐⇒ ins ∈ σ(ρ) ∪
σ(ρ̇i )

·
·

·

i

′

·
i

′

σ |= ∆ 6 ∆ ⇐⇒ σ(∆) ⊆ σ(∆ )
A parametric type A together with a set of constraints C between its parameters then
describes a family of closed types, obtained by taking all instances σ(A) of A for all solutions
σ |= C, and all their supertypes. More precisely, we define
def

JA | CK = {A′ | σ(A) 6 A′ , σ |= C}

def

JC | CK = {C ′ | σ(C) 6 C ′ , σ |= C}

Our aim now is to take an expression e and compute a type A and a set of constraints C
such that the set of all possible types A′ we can assign to e is captured exactly by JA | CK.
3.2. Inference rules. We infer types and constraints using syntax-directed inference rules
of the form Γ; Ξ ⊢F e : A | C for expressions and Γ; Ξ ⊢F c : C | C for computations, defined
in Figure 5. Here, C is a set of constraints, F is a set of all fresh parameters introduced in
the derivation, and Ξ is the polymorphic context, which is collection of unique assignments
xi : ∀Fi . Ai | Ci of type schemes to variables (assumed to be different from the ones in Γ).
As in typing judgements, we assume (though never write) a fixed signature Σ.
The type schemes are similar to polymorphic types of ML, which are types, universally
quantified over a given set of type parameters. In our case, we may also quantify over
region and dirt parameters, but we need to keep information about the constraints these
parameters need to satisfy. Even though the ordinary context Γ can be seen as a particular
instance of Ξ, we keep the two separate in order to relate the inference judgements to typing
judgements, as the latter employ only Γ.
Though C and F are sets, we sometimes write them as sequences to save space. For
example, we write F1 , F2 , α, δ instead of F1 ∪F2 ∪{α, δ}. We also assume that all parameters

INFERRING ALGEBRAIC EFFECTS

19

listed in F are distinct and this implies the usual freshness conditions [20, p. 321]. For
example, the above sequence implies that sets F1 and F2 are disjoint and do not contain α
or δ. In particular, in the rule Cstr-PolyVar, we implicitly rename any bound parameters
F so that a fresh copy is obtained at each use.
As announced at the beginning of Section 3.1, regions and dirts have a fixed representation with parameters. Thus in Cstr-Inst, we assign each instance a fresh region parameter
and add a suitable constraint. Similarly, we cannot simply state that the dirt of val is
empty. Instead, in Cstr-Val, we assign it a fresh dirt parameter δ that needs to satisfy no
constraints. That means that we may replace δ by anything, including the empty set.
Though we get an equivalent set of constraints in the rule Cstr-Op if we use a single
region parameter, we introduce two for technical reasons, discussed in Section 5.2. The
rule Cstr-With is analogous to Cstr-App.
Otherwise, the rules for the standard constructs are similar to ones in the HindleyMilner algorithm [20, p. 322], except that we need to use (correctly oriented) inequalities
instead of equalities in the constraints. In Cst-LetVal we can safely generalize over all the
fresh parameters F1 generated while inferring the type of e because they are guaranteed to
be distinct from any parameters appearing in Γ.
This leaves us with
Cstr-Hand

(Ψi )i
Γ, x : αin ; Ξ ⊢Fv cv : D v | Cv
Γ; Ξ ⊢F (handler val x 7→ cv |(ei #opi x k →
7 ci )i ) : C =
⇒D|C
To start, we take type parameters αin and αout to represent the incoming and outgoing
type of the handler. Next, we take O to be the set of all distinct operation symbols listed
op
op
in operation cases. For each op ∈ O, we take fresh parameters ρin and ρout that represent
the region assigned to op in the incoming and outgoing dirt of the handler. Finally, we
O and δ O to represent the rest of incoming and outgoing dirt. The
take fresh parameters δin
out
incoming and outgoing types are then
def

op

C = αin ! {(op : ρin )op∈O | δin }

and

def

op

D = αout ! {(op : ρout )op∈O | δout }

After introducing the necessary parameters, we infer the type and constraints of the value
case. Next, for each operation case, in the premises Ψi , consisting of:
Γ ⊢Fi ei : Ai | Ci

opi : Aopi −
→ B opi ∈ Σ(Ei )

Γ, x : Aopi , k : B opi −
→ D ⊢Fi′ ci : D i | Ci′

we check the suitability of operation, and infer the types and constraints of the handled
instance ei and of the operation case ci .
We end up with the a set of constraints C consisting of the following five parts:
• constraints Cv inherited from the value case and constraints Ci and Ci′ inherited from each
operation case;
• constraint D v 6 D stating that the outgoing type D subsumes the type of the value case
and constraints D i 6 D stating the same for all the operation cases;
• constraints Ai 6 E ρ̇i stating that the type Ai of the instance expression ei is subsumed
by the effect type E ρ̇i for S
some fresh ρ̇i ;
op
op
• constraints ρin 6 ρout ∪ op=op ρ̇i for each op ∈ O — the outgoing dirt must be big
i
enough to cover all operations in the incoming dirt that are not surely handled by one of
the operation cases; and
• a constraint δin 6 δout — any operation that is not listed in a handler cannot be handled,
so must appear in the outgoing dirt as well.

·

20

MATIJA PRETNAR

Cstr-Var
(x : A) ∈ Γ
Γ; Ξ ⊢∅ x : A | ∅

Cstr-PolyVar

x : ∀F. A | C ∈ Ξ
Γ; Ξ ⊢F x : A | C

Cstr-Zero
Γ; Ξ ⊢∅ 0 : nat | ∅

Cstr-True

Cstr-False

Γ; Ξ ⊢∅ true : bool | ∅

Γ; Ξ ⊢∅ false : bool | ∅

Cstr-Succ
Γ; Ξ ⊢F e : A | C
Γ; Ξ ⊢F succ e : nat | C, A 6 nat

Cstr-Fun
Γ, x : α; Ξ ⊢F c : C | C
Γ; Ξ ⊢F,α fun x 7→ c : α −
→C|C

Cstr-Unit
Γ; Ξ ⊢∅ () : unit | ∅

Cstr-Inst
Γ; Ξ ⊢ρ̇ ins : E ρ̇ | ins ∈ ρ̇

Cstr-Hand — in the text

Cstr-IfThenElse
Γ; Ξ ⊢F2 c2 : C 2 | C2
Γ; Ξ ⊢F e : A | C
Γ; Ξ ⊢F1 c1 : C 1 | C1
Γ; Ξ ⊢F,F1 ,F2 ,α,δ if e then c1 else c2 : α ! δ | C, C1 , C2 , A 6 bool, C 1 6 (α ! δ), C 2 6 (α ! δ)
Cstr-IsZero
Γ; Ξ ⊢F e : A | C
Γ; Ξ ⊢F,δ iszero e : bool ! δ | C, A 6 nat
Cstr-Absurd
Γ; Ξ ⊢F e : A | C
Γ; Ξ ⊢F,α,δ absurd e : α ! δ | C, A 6 empty

Cstr-Pred
Γ; Ξ ⊢F e : A | C
Γ; Ξ ⊢F,δ pred e : nat ! δ | C, A 6 nat
Cstr-App
Γ; Ξ ⊢F1 e1 : A1 | C1

Γ; Ξ ⊢F2 e2 : A2 | C2
δ

→ α)
Γ; Ξ ⊢F1 ,F2 ,α,δ e1 e2 : α ! δ | C1 , C2 , A1 6 (A2 −

Cstr-Val
Γ; Ξ ⊢F e : A | C
Γ; Ξ ⊢F,δ val e : A ! δ | C
Cstr-Op
op : Aop −
→ B op ∈ Σ(E)

Γ; Ξ ⊢F1 e1 : A1 | C1
Γ; Ξ ⊢F2 e2 : A2 | C2

Γ, y : B op ; Ξ ⊢F c : A ! ∆ | C

Γ; Ξ ⊢F1 ,F2 ,F,ρ,ρ̇,δ e1 #op e2 (y. c) : A ! {op : ρ | δ} | C1 , C2 , C, A1 6 E ρ̇ , A2 6 Aop , ρ̇ 6 ρ, ∆ 6 {op : ρ | δ}
Cstr-Let
Γ, x : α; Ξ ⊢F2 c2 : B ! ∆2 | C2
Γ; Ξ ⊢F1 c1 : A ! ∆1 | C1
Γ; Ξ ⊢F1 ,F2 ,α,δ let x = c1 in c2 : B ! δ | C1 , C2 , A 6 α, ∆1 6 δ, ∆2 6 δ
Cstr-LetVal
Γ; Ξ, (x : ∀F1 . A | C1 ) ⊢F2 c : C | C2
Γ; Ξ ⊢F1 e : A | C1
Γ; Ξ ⊢F2 let val x = e in c : C | C2
Cstr-LetRec
δ
δ
→ α2 ; Ξ ⊢F2 c2 : D | C2
Γ, f : α1 −
→ α2 , x : α1 ; Ξ ⊢F1 c1 : C | C1
Γ, f : α1 −
Γ; Ξ ⊢F1 ,F2 ,α1 ,α2 ,δ let rec f x = c1 in c2 : D | C1 , C2 , C 6 α2 ! δ
Cstr-With
Γ; Ξ ⊢F2 c : C | C2
Γ; Ξ ⊢F1 e : A | C1
Γ; Ξ ⊢F1 ,F2 ,α,δ with e handle c : α ! δ | C1 , C2 , A 6 (C =
⇒ α ! δ)

Figure 5: The inductive definition of the inference judgements Γ; Ξ ⊢F e : A | C and Γ; Ξ ⊢F
c : C | C. The rule for handlers is given in the main text.

INFERRING ALGEBRAIC EFFECTS

21

The set F of all fresh parameters gathers all fresh parameters mentioned above and equals
def

F = Fv , (Fi )i , (Fi′ )i , αin , αout , δin , δout , (ρ̇i )i , (ρin )op∈O , (ρout )op∈O
op

op

Looking at the presented inference rules, we see that there is exactly one rule that
applies to each language construct, so we can assign a unique type and set of constraints
to each term (up to a renaming of fresh parameters). This allows us to turn the rules into
a recursive function, which computes exactly the information about all the types we can
assign to a given term:
Theorem 3.3 (Soundness & completeness). Let Γ be a closed context.
• If we have Γ ⊢ e : A′ for some A′ , then Γ ⊢F e : A | C holds and
JA | CK = {A′′ | (Γ ⊢ e : A′′ )}
• We have Γ ⊢F c : C | C if and only if Γ ⊢ c : C ′ holds for some C ′ . In this case
JC | CK = {C ′′ | (Γ ⊢ c : C ′′ )}
Remark 3.4. We limit the parameter and result types in the signature Σ to basic types
because Σ is shared between typing judgements, which feature concrete regions and dirt,
and inference judgements, which represent regions and dirt exclusively with parameters.
There are three ways of reconciling this conflict:
• Extend the language of constraints with concrete upper bounds of the form ρ 6 R and δ 6
∅. Then we may, say, replace any occurrence of Aop = E {ins1 ,ins2 } in inference judgements
with E ρ̇ for some fresh ρ̇, and add constraints ins1 ∈ ρ̇, ins2 ∈ ρ̇, ρ̇ 6 {ins1 , ins2 }, or
ins#op

op:ρ|δ

replace B op = unit −−−−→ unit with a suitably fresh unit −−−→ unit and constraints
ins ∈ ρ, ρ 6 {ins}, δ 6 ∅.
• Extend monomorphic types with wild card regions and dirt. For example, the type
exception⊤ would capture any exception, no matter which concrete region it comes
from. Similarly, the dirt ⊤#raise would mean that a computation raises some exception,
though we do not know which one, while the dirt ⊤ would mean that any operation may
get called.
This solution agrees with practice [2], where most of types that appear in the signature
are already basic, and the only two deviations so far are cooperative multithreading and
delimited continuations, which both take functions as parameters. However, in both cases,
we are not interested in imposing any limits on this dirt, so a wild card dirt would fit our
goal.
To add wild card regions and dirt to core Eff , we need to: (1) add subtyping rules
such as R ⊆ ⊤, (2) extend Op with a condition that if e1 : E ⊤ then ⊤#op ∈ ∆, and (3)
adapt the rule Hand to ensure that any wild card dirt cannot be handled.
• Each of the above approaches has its advantages, and in addition, the two are compatible,
so one may consider both in a practical implementation. However, the first approach leads
a more powerful prescriptive effect system which is well beyond the scope of this paper
(discussed more in the Conclusion), while the second one is routine but messy. Thus,
we opt for the simplest option: prohibit any types that include regions and dirt from
appearing in Σ.

22

MATIJA PRETNAR

4. Unifying constraints
Unfortunately, unlike in ML, subtyping prevents us from computing a principal type from
a given set of constraints [24]. For example (ignoring dirt for a moment), if we just drop
the constraint in the type
(α −
→ β) −
→ (α −
→ β) | β 6 α
we get a type that captures too many closed types. On the other hand, the more restricted
parametric type (γ −
→ γ) −
→ (γ −
→ γ) is too strict because it fails to capture the type
′

′

(E {ins,ins } −
→ E {ins} ) −
→ (E {ins,ins } −
→ E {ins} )
′

or any of its subtypes (otherwise, the subtyping rules would imply E {ins,ins } 6 γ 6 E {ins} ).
Instead, the best we can do is to simplify the constraints as much as possible. First, we
are going to reduce the constraints down to a more convenient and basic form. Constraints in
this form always admit a solution, so the reduction also detects any unsolvable constraints.
Definition 4.1. A set of constraints C is unified, if all constraints are decomposed down to
ones between parameters and the set is closed under logical implication. In particular, C
may contain only constraints of the form
[
[
α 6 α′ ,
ρ 6 ρ′ ∪
ρ̇i ,
ins ∈ ρ ∪
ρ̇i ,
δ 6 δ′ ,

·

·

i

i

and the following closure properties must hold:
• if (α1 6 α2 ) ∈SC and (α2 6 α3 ) ∈ C, thenS
(α1 6 α3 ) ∈ C;
S
• if (ρ1 6 ρ2 ∪ S
i∈J ρ̇i ) ∈ C, then (ρ1 6 ρ3 ∪ i∈I∪J
i∈I ρ̇i ) ∈ C and (ρ2 6 ρ3 ∪ S
S ρ̇i ) ∈ C;
• if (ins ∈ ρ1 ∪ i∈I ρ̇i ) ∈ C and (ρ1 6 ρ2 ∪ i∈J ρ̇i ) ∈ C, then (ins ∈ ρ2 ∪ i∈I∪J ρ̇i ) ∈ C;
• if (δ1 6 δ2 ) ∈ C and (δ2 6 δ3 ) ∈ C, then (δ1 6 δ3 ) ∈ C.
To avoid circular types, we need to track all type parameters of the same shape. So, we
assume that C is equipped with an equivalence relation ≈C on type parameters, such that
(α 6 α′ ) ∈ C implies α ≈C α′ . For solutions of a unified set of constraints C, we consider
only such σ |= C, for which we also have σ(α) ≈ σ(α′ ) for any α ≈C α′ .

·
·

·
·

·

·

Lemma 4.2. If a set of constraints C is unified, there exists a solution σ |= C.
In Figure 6, we define an algorithm unify, which is similar to Robinson’s unification
algorithm [20, p. 327], except that it returns a set of unified constraints in addition to the
unifying substitution. The algorithm is defined recursively, passing around a triple (σ; C; Q),
where σ is a unifying substitution of replaced parameters (initially taken to be the identity),
C is a set of already unified constraints (initially C is empty while ≈C is the identity relation
on all type parameters in Q), and the queue Q is a set of constraints yet to be processed.
The unifying substitution is not a closed substitution (Definition 3.1), which maps type
parameters to closed types, etc., but one that maps them to parametric ones.
Definition 4.3. A substitution σ is a mapping that maps: each type parameter α to a
type σ(α), each region parameter ρ to a region parameter σ(ρ), each inhabited region parameter ρ̇ to an inhabited region parameter σ(ρ̇), and each dirt parameter δO to a dirt σ(δO )
′
of the form {(op : ρop )op∈O′ | δ′O∪O }, where O′ is disjoint from O. This ensures that the
dirt σ(δO ) does not capture any operations from O.
We write substitutions by listing a set of all the non-idempotent rules. We can extend a
substitution from parameters to other constructs just like we extended closed substitutions.

INFERRING ALGEBRAIC EFFECTS

23

unify(σ; C; ·) = (σ, C)
unify(σ; C; A 6 A′ , Q) =
match A 6 A′ with
| A 6 A 7→ unify(σ; C; Q)
| α 6 α′ 7→ unify(σ; C ⊎ (α 6 α′ ); Q)
| α 6 A 7→ if ∃α′ ≈C α. α′ ∈ free(A) then failure else
let σ ′ = {α′ 7→ refresh(A) | α′ ≈C α} in
let C ′ = {(α′ 6 α′′ ) ∈ C | α ≈C α′ ≈C α′′ } in
unify(σ ′ ◦ σ; C − C ′ ; σ ′ (Q), σ ′ (α) 6 A, σ ′ (C ′ ))
| A 6 α 7→ if ∃α′ ≈C α. α′ ∈ free(A) then failure else
let σ ′ = {α′ 7→ refresh(A) | α′ ≈C α} in
let C ′ = {(α′ 6 α′′ ) ∈ C | α ≈C α′ ≈C α′′ } in
unify(σ ′ ◦ σ; C − C ′ ; σ ′ (Q), A 6 σ ′ (α), σ ′ (C ′ ))
′

| E ρ̇ 6 E ρ̇ 7→ unify(σ; C ⊎ ρ̇ 6 ρ̇′ ; Q)
→ C ′ ) 7→ unify(σ; C; Q, A′ 6 A, C 6 C ′ )
|(A −
→ C) 6 (A′ −
|(C =
⇒ D′ ) 7→ unify(σ; C; Q, C ′ 6 C, D 6 D′ )
⇒ D) 6 (C ′ =
| otherwise 7→ failure
unify(σ; C; A ! ∆ 6 A′ ! ∆′ , Q) = unify(σ; C; Q, A 6 A′ , ∆ 6 ∆′ )
[
[
unify(σ; C; ρ 6 ρ′ ∪
ρ̇i , Q) = unify(σ; C ⊎ (ρ 6 ρ′ ∪
ρ̇i ); Q)
i
i
[
[
unify(σ; C; ins ∈ ρ ∪
ρ̇i , Q) = unify(σ; C ⊎ (ins ∈ ρ ∪
ρ̇i ); Q)

·

·

·

·

i

unify(σ; C; {(op : ρop )op∈O |

δ1O }

6 {(op :

ρ′op )op∈O′

|

′
δ2O }, Q)

i

=

if O = O′ then
unify(σ; C ⊎ {ρop 6 ρ′op | op ∈ O} ⊎ (δ1 6 δ2 ), Q)
else
′

let σ1 = if O′ ⊂ O then {} else {δ1 7→ {(op : ρop )op∈O′ −O | δ1′O∪O }} in
′

let σ2 = if O ⊂ O′ then {} else {δ2 7→ {(op : ρ′op )op∈O−O′ | δ2′O∪O }} in
let C ′ = {(δ 6 δ ′ ) ∈ C | δ ∼C δ ′ ∼C δ1 } ∪ {(δ 6 δ ′ ) ∈ C | δ ∼C δ ′ ∼C δ2 } in
unify(σ1 ◦ σ2 ◦ σ; (C − C ′ ), σ ′ (Q) ∪ σ ′ (C ′ ))

Figure 6: Definition of the constraint unification algorithm unify.

This allows us to compose substitutions and additionally, to compose a closed substitution σ
with a substitution σ ′ and obtain a closed substitution σ ◦ σ ′ .
δ1
The unification works as follows. Take, say, a constraint α1 6 (α2 −→
bool). Since
the rules of structural subtyping admit only comparison between types of the same shape,
the only way to satisfy this constraint is to set α1 to be some function type into bool.
δ2
So, we decompose the constraint by replacing α1 with some fresh α3 −→
bool and adding
constraints α2 6 α3 and δ2 6 δ1

24

MATIJA PRETNAR

We add these constraints using the closure operator ⊎, defined in Figure 7, which
extends C with a given constraint and all constraints it implies. This is done with a simplified
version of an algorithm for computing the transitive closure of a graph [24], except that for
region parameters, we also have to take instances and handled regions into account.
C ⊎ (α1 6 α2 ) = C ∪ {α′1 6 α′2 | (α′1 6 α1 ) ∈ C, (α2 6 α′2 ) ∈ C}
[
[
[
[
ρ̇i ) ∈ C}
ρ̇i ) ∈ C, (ρ2 6 ρ′2 ∪
ρ̇i | (ρ′1 6 ρ1 ∪
ρ̇i ) = C ∪ {ρ′1 6 ρ′2 ∪
C ⊎ (ρ1 6 ρ2 ∪

·
·
[
[
∪ {ins ∈ ρ ∪ · ρ̇ | (ins 6 ρ ∪ · ρ̇ ) ∈ C, (ρ
[
[
[
C ⊎ (ins ∈ ρ ∪ · ρ̇ ) = C ∪ {ins ∈ ρ ∪ · ρ̇ | (ρ 6 ρ ∪ · ρ̇ ) ∈ C}
·

′
i
2
i∈I∪J∪K

i

′

i∈I

C ⊎ (δ1 6 δ2 ) = C ∪ {δ1′ 6 δ2′ |

·

i∈K

i∈J

i∈I∪J∪K

i∈I

i

1

2

6 ρ′2 ∪

′

i∈I∪J
(δ1′ 6 δ1 )

ρ̇i ) ∈ C}

i∈K

i∈J

i

·

[

i

i∈J

∈ C, (δ2 6 δ2′ ) ∈ C}

Figure 7: Definition of the closure operator ⊎. In all cases, we assume that C implicitly
contains all reflexive constraints, so that, for example in the first case, the added
set also includes α1 6 α2 and all constraints of the form α1 6 α′2 and α′1 6 α2 .
Before decomposition, we need to perform an occur check in order to prevent ill-formed
types and ensure termination. This check is slightly more involved than usually [20, p. 327].
Say that we want to unify the set of constraints (let us again ignore dirt):
{(α1 −
→ α2 ) 6 α3 , α4 6 α1 , α4 6 α3 }
We decompose α3 as some α5 −
→ α6 and end up with constraints
{α5 6 α1 , α2 6 α6 , α4 6 α1 , α4 6 (α5 −
→ α6 )}
Now, we need to decompose α4 , then α1 , then α5 and the whole thing repeats. So we need
to check not only that α is not in free(A), the set of all parameters that occur in A, but
also that no other parameters in its skeleton are.
When decomposing α 6 A, we also replace each α′ ≈C α with a (distinct) fresh copy of
A. We do this by repeatedly calling a function refresh(A) that on each call returns a type
of the same form as A, except with all its type, region, and dirt parameters replaced with
fresh ones. Because of this expansion, any constraints C ′ ⊆ C that mention parameters from
the skeleton of α are no longer decomposed. So we need to take them out of the otherwise
unified C and put them back into the queue Q.
On the remaining unified set of constraints C − C ′ , we define ≈C−C ′ to be as before,
except that we remove the whole skeleton of α, and add the freshly generated parameters
into the skeletons of matching parameters in A. For example, if the skeletons of ≈C were
{α1 , α2 }, {α3 , α4 , α5 }, {α6 }
δ

δ

1
2
and we decompose the constraint α1 6 α3 −→
α6 , we replace α1 by α7 −→
α8 and α2 by
δ3
α9 −→ α10 , and the skeletons of ≈C−C ′ are

{α3 , α4 , α5 , α7 , α9 }, {α6 , α8 , α10 }
When we unify a constraint α 6 α′ , we merge the skeletons of α and α′ .

INFERRING ALGEBRAIC EFFECTS

25

For dirt constraints, we similarly expand both sides so to list the same operations. For
op
op′
example, if we have a constraint {op : ρ1 | δ1 } 6 {op′ : ρ2 | δ2 }, we replace δ1 with some
′
′
op,op
op,op
fresh {op′ : ρ3 | δ3
} and δ2 with {op : ρ4 | δ4
} and add constraints ρ1 6 ρ4 , ρ3 6 ρ2 ,
and δ3 6 δ4 . We define ∼C to be the equivalence relation on dirt parameters generated by
(δ 6 δ′ ) ∈ C, so that we can capture all related dirt parameters and expand them at the
same time.
An example of a full run of the unification algorithm is given in Figure 8.
no
unify
;
n
unify α2
n
unify α2
n
unify α2
n
unify α2
n
unify α2
n
unify α2
n
unify α2
n
α3
n
unify α2
n
α3
n
unify α2
n
α3
n
α2
n
α3

o
n
δ1
nat) 6 α2 , {op : ρ̇1 | δ2 } 6 δ1 )
=
(α1 −→
o no n
o
δ3
δ1
δ3
nat), {op : ρ̇1 | δ2 } 6 δ1
nat) 6 (α3 −→
nat) ;
;
(α1 −→
7→ (α3 −→
=
o
o no n
δ3
=
nat) ;
;
α3 6 α1 , (nat ! δ1 ) 6 (nat ! δ3 ), {op : ρ̇1 | δ2 } 6 δ1
7→ (α3 −→
o
o n
o n
δ3
=
(nat ! δ1 ) 6 (nat ! δ3 ), {op : ρ̇1 | δ2 } 6 δ1
nat) ;
α3 6 α1 ;
7→ (α3 −→
o
o n
o n
δ3
=
nat 6 nat, δ1 6 δ3 , {op : ρ̇1 | δ2 } 6 δ1
nat) ;
α3 6 α1 ;
7→ (α3 −→
o
o n
o n
δ3
=
δ1 6 δ3 , {op : ρ̇1 | δ2 } 6 δ1
nat) ;
α3 6 α1 ;
7→ (α3 −→
o
o n
o n
δ3
=
{op : ρ̇1 | δ2 } 6 δ1
nat) ;
α3 6 α1 , δ1 6 δ3 ;
7→ (α3 −→
o
op:ρ̇3 |δ5
7→ (α3 −−−−−→ nat), δ1 7→ {op : ρ̇2 | δ4 }, δ3 7→ {op : ρ̇3 | δ5 } ;
o n
o
6 α1 ;
{op : ρ̇1 | δ2 } 6 {op : ρ̇2 | δ4 }, {op : ρ̇2 | δ4 } 6 {op : ρ̇3 | δ5 }
=
o
op:ρ̇3 |δ5
7→ (α3 −−−−−→ nat), δ1 7→ {op : ρ̇2 | δ4 }, δ3 7→ {op : ρ̇3 | δ5 } ;
o n
o
6 α1 , ρ̇1 6 ρ̇2 , δ2 6 δ4 ;
{op : ρ̇2 | δ4 } 6 {op : ρ̇3 | δ5 }
=
o
op:ρ̇3 |δ5
7→ (α3 −−−−−→ nat), δ1 7→ {op : ρ̇2 | δ4 }, δ3 7→ {op : ρ̇3 | δ5 } ;
o no
=
6 α1 , ρ̇1 6 ρ̇2 6 ρ̇3 , δ2 6 δ4 6 δ5 ;
o
op:ρ̇3 |δ5
7→ (α3 −−−−−→ nat), δ1 7→ {op : ρ̇2 | δ4 }, δ3 7→ {op : ρ̇3 | δ5 } ,
o
6 α1 , ρ̇1 6 ρ̇2 6 ρ̇3 , δ2 6 δ4 6 δ5
no
;

δ

1
Figure 8: The unification of the set of constraints {(α1 −→
nat) 6 α2 , {op : ρ̇2 | δ2 } 6 δ1 }.
We display constraints in a coalesced form. For example, we write ρ̇1 6 ρ̇2 6 ρ̇3
instead of ρ̇1 6 ρ̇2 , ρ̇2 6 ρ̇3 and ρ̇1 6 ρ̇3 .

Proposition 4.4. For any set of constraints C, the algorithm unify(∅; ∅; C) always halts.
• If it halts with a failure, then C has no solutions.
• If it halts returning (σ ′ , C ′ ), then C has a solution. Furthermore, solutions σ |= C are
exactly all the ones of the form σ = σ ′′ ◦ σ ′ , where σ ′′ |= C ′ .
Note that unify can fail for two reasons: either we detect a cyclic constraint during occur
check, or we try to unify two incompatible types — no failure can happen due to unification

26

MATIJA PRETNAR

of dirt and region constraints. These are exactly the cases in which the Hindley-Milner
algorithm fails [20, p. 327], so our algorithm indeed infers the usual ML types, except
annotated with information about effects.
Corollary 4.5. The two-way inference rules
Unify-Expr

Unify-Comp

Γ ⊢F e : A | C
===================′
σ(Γ) ⊢F e : σ(A) | C

Γ ⊢F c : C | C
===================′
σ(Γ) ⊢F c : σ(C) | C

where unify(C) = (σ, C ′ ), are sound.
Since Unify-Expr and Unify-Comp are two-way rules, we can be sure that no information is lost, so we can perform unification phase not only after, but also while gathering
the constraints. In fact, in Eff , constraints are always kept in unified form, so unification
is performed each time we add a new constraint. Though this strategy seems expensive, it
offers many advantages:
(1) Any ill-typed terms are caught as soon as possible. This does not influence the efficiency
too much, but gives much more informative error messages.
(2) In each rule, the inferred constraints consist mostly of constraints inherited from subterms. In Eff , the inference algorithm uses a technique called λ-lifting [24] to ensure
that subderivations share no common parameters. Then, if constraints C1 and C2 , say,
are unified, so is their union C1 ∪ C2 , and we need to perform closure only for the small
number of additional constraints, specific to the current rule.
(3) As we shall soon see, unified constraints may be garbage collected, drastically reducing
their size and speeding up the algorithm.
5. Simplifying constraints
5.1. Garbage collection. The main simplification technique we employ is garbage collection [25, 28, 32]. We first recap the existing idea for type parameters, and then extend it
to dirt and region parameters so to fit into our setting.
Recall that a parametric type A together with a unified set of constraints C captures
exactly the closed types in the set JA | CK. Can we obtain a smaller set of constraints C ′
but keep JA | C ′ K = JA | CK?
Mark type parameters in A as positive or negative, if they appear in a covariant or
contravariant position, respectively. For example, in (α1 −
→ α2 ) −
→ α3 , the parameters α1
′
and α3 are positive while α2 is negative. It turns out that in C , we only need to keep the
constraints of the form α− 6 α+ , where α− is a negative and α+ is a positive.
Since C ′ contains less constraints than C, any solution of C ′ is a solution of C as well,
so we get JA | CK ⊆ JA | C ′ K. For the other direction, we need to show that for any solution
σ ′ |= C ′ , there exists some σ |= C such that σ(α+ ) 6 σ ′ (α+ ) holds for all positive α+ , and
σ ′ (α− ) 6 σ(α− ) holds for all negative α− . It is then easy to see that σ(A) 6 σ ′ (A) holds as
well, and so any type A′ such that σ ′ (A) 6 A′ already appears in JA | CK. For exact details,
see the proof of Proposition 5.3.

INFERRING ALGEBRAIC EFFECTS

27

Definition 5.1. The sets pos(A) of positive and neg(A) negative parameters in a given
type A are defined as:
pos(α) = {α}

neg(α) = ∅

pos(A −
→ C) = neg(A) ∪ pos(C)

neg(A −
→ C) = pos(A) ∪ neg(C)

ρ

neg(E ρ ) = ∅

pos(E ) = {ρ}
pos(C =
⇒ D) = neg(C) ∪ pos(D)

neg(C =
⇒ D) = pos(C) ∪ neg(D)

The sets of both positive and negative parameters in ground types (bool, nat, . . . ) are
empty. For dirty types, the sets of positive and negative parameters are defined as:
pos(A ! {op1 : ρ1 , . . . , opn : ρn | δ}) = pos(A) ∪ {ρ1 , . . . , ρn , δ}
neg(A ! ∆) = neg(A)
Definition 5.2. For a unified set of constraints C and sets of parameters P and N , we
define the garbage collected constraints gcP,N (C) as:
gcP,N (C) = {(α− 6 α+ ) ∈ C | α− ∈ N, α+ ∈ P } ∪
[
{(ρ− 6 ρ+ ∪
ρ̇i ) ∈ C | ρ− ∈ N, ρ+ ∈ P } ∪
i
[
{(ins ∈ ρ+ ∪
ρ̇i ) ∈ C | ρ+ ∈ P } ∪

·
·

i

{(δ− 6 δ+ ) ∈ C | δ− ∈ N, δ+ ∈ P }
On gcP,N (C), we define ≈gcP,N (C) to be the restriction of ≈C to the set P ∪ N .
To perform garbage collection on constraints in a typing judgement Γ ⊢ e : A | C, we
define P to contain not just pos(A), but also neg(Ai ) for all (xi : Ai ) ∈ Γ. Conversely, N
must contain neg(A) and all pos(AS
i ). We similarly extend
S P with all region parameters ρ̇i
′
in constraints of the form ρ 6 ρ ∪ i ρ̇i and ins ∈ ρ ∪ i ρ̇i . Otherwise, garbage collection
may drop some of their lower bounds and thus relax the constraints.
S Recall that regions
σ(ρ̇i ) are always non-empty, so decreasing them can only increase i ρ̇i .

·

·

·

Proposition 5.3. If the set of constraints C is unified, the two-way inference rules
GC-Expr

GC-Comp

Γ ⊢F e : A | C
===========================
Γ ⊢F ∩(P ∪N ) e : A | gcP,N (C)

Γ ⊢F c : C | C
===========================
Γ ⊢F ∩(P ∪N ) c : C | gcP,N (C)

where
P0 = pos(A) ∪ neg(Γ)

·[ ρ̇ ) ∈ C, ρ
∪ · ρ̇ ) ∈ C, ρ

P = P0 ∪ {ρ̇i | (ρ− 6 ρ+ ∪
{ρ̇i | (ins ∈ ρ+

[

−

i

i

i

i

+

∈ N, ρ+ ∈ P0 } ∪
∈ P0 }

N = neg(A) ∪ pos(Γ)
are sound.
Furthermore, the set gcP,N (C) is unified.
We present garbage collection in the form of two-way rules so that, like unification, we
can perform it while still gathering constraints. This allows us to dispose any intermediate
constraints as soon as possible, making the whole algorithm very efficient.

28

MATIJA PRETNAR

Ignoring handled region parameters in region constraints, the number of parameters
is linear in the size of type, and each constraint relates two parameters, so the number of
constraints is roughly quadratic in the size of the inferred type after garbage collection. In
practice, though, the number of constraints is often much smaller and for typical functional
programs, the current implementation of the inference algorithm in Eff is on a par with
the one in OCaml (more details can be found in Table 1). Without garbage collection, the
inference algorithm experiences exponential blow-up and is unusable.
filename
garsia wachs.eff/.ml
list.eff/.ml
map.eff/.ml
set.eff/.ml

OCaml

Eff
16
46
93
53

ms
ms
ms
ms

16
42
60
33

ms
ms
ms
ms

Table 1: The table contains average (N = 50, σ < 15%) file loading times for Eff 3.1 and
OCaml 4.01.0 on Mac OS X 10.9.3 running on a 1.7 GHz Intel Core i5 with 4 GB of
RAM. Except for a few initial definitions needed to bridge the differences, the Eff
and OCaml files are identical (they can be found in the examples/benchmarks/
folder of the Eff distribution). The test files contain only definitions and no executable code, so most of the loading time is spent on type-checking. To compensate
for the time needed to start the interpreter and load the standard library, we subtracted the average time spent to load a blank file from all the entries (23 ms for
Eff and 12 ms for OCaml).

5.2. Simplifying region constraints. Garbage collection is extremely efficient, but there
is a small number of additional tactics we can offer that simplify region constraints. These
are not meant to make the algorithm fast, but to make its output simpler. For as we shall
see in Section 6.3, region constraints tend to be the most difficult to present succinctly, so it
is crucial that they are as simple as possible before we display them. The main idea behind
all optimizations is thatSin region constraints, handled region parameters ρ̇i contribute to
the right-hand side ρ ∪ i ρ̇i only when they denote a singleton.
When determining if an inhabited region parameter ρ̇ denotes a singleton, it is helpful to
see that ρ̇ may appear as a covering
S region only in constraints of the form ρ 6 ρ̇ and ins ∈ ρ̇,
so ones with no handled regions i ρ̇i . To see this, one needs to laboriously check that no
other constraints are added during inference, unification, or garbage collection. Adding an
extra region parameter to Cstr-Op was a part of that effort.
Unlike garbage collection, each tactic is very basic, so we only sketch how they work.
• Any parameter ρ̇ for which we have both ins ∈ ρ̇ and ins′ ∈ ρ̇ for some ins S
6= ins′
cannot denote a singleton. Thus, it may be removed from all singleton unions i ρ̇i in
which it appears. Similarly, if we have ins ∈ ρ̇, we may
S remove any occurrence of ρ̇ as a
handled region in constraints of the form ins′ ∈ ρ ∪ i ρ̇i as it cannot contain ins′ and
be a singleton at the same time.
• Next, take inhabited region parameters ρ̇1 6 ρ̇2 (recall that all inequalities
between
S
inhabited region parameters are of that form) that both appear in some i ρ̇i . If ρ̇1 does

·

·

·

·

·

INFERRING ALGEBRAIC EFFECTS

29

not denote a singleton, neither
S does ρ̇2 , and if ρ̇1 does denote a singleton, ρ̇2 can make
no further contribution to i ρ̇i . So, we may safely remove ρ̇2 in both cases.
• We may Sreduce the number of constraints
by observing that if I ⊆ J, the constraint
S
′
′
ρ 6 ρ ∪ i∈I ρ̇i implies ρ 6 ρ ∪ i∈J ρ̇i and we may safely throw the latter one away.
• After all the simplifications, we may further reduce the number of constraints by another
round of garbage collection, in which we remove all lower bounds on region parameters
that no longer occur in singleton unions.

·

·

·

5.3. Further simplifications. Our algorithm also applies to the much simpler case when
one triggers effects with only operation symbols and no instances [11]. As this amounts
S to
having a single instance ⋆ of each effect, we can drop all instance constraints ins ∈ ρ ∪ i ρ̇i
with at least one handled region parameter ρ̇i . This is because ins must be ⋆ and all
inhabited region parameters ρ̇ must denote the singleton region {⋆}, so any such constraint
is always satisfied.
S
Another tempting way to drop constraints is to drop all constraints ins ∈ ρ ∪ i ρ̇i
for which ins ∈ ρ̇i is the only lower bound for some ρ̇i . But, unlike other simplification
techniques, this may not be done until after we have gathered all the constraints, because
ρ̇i may still receive further lower bounds.
Similarly, we may want to improve the second tactic from Section 5.2, and remove any
handled parameters ρ̇2 not only if we have ρ̇1 6 ρ̇2 , but also in case all lower bounds of ρ̇1
are also lower bounds of ρ̇2 . If ρ̇1 6 ρ̇2 , this is implied by closure properties. For example, if
we have lower bounds ρ̇3 6 ρ̇1 , ρ̇3 6 ρ̇2 and ρ̇4 6 ρ̇2 , we can always assign a smaller region
to ρ̇1 than to ρ̇2 . Thus, if ρ̇1 and ρ̇2 appear in the same singleton union, we can safely drop
ρ̇2 , for if it denotes a singleton, so does ρ̇1 . This condition is also stable under garbage
collection — if ρ̇1 is not negative, the constraint ρ̇1 6 ρ̇2 will be dropped, but since ρ̇1 and
ρ̇2 are both positive, all their lower bounds will be kept. However, ρ̇1 may similarly receive
further lower bounds, so we can perform the simplification only at the very end.

·

·

6. Displaying inferred types
However, once the algorithm finishes, we may perform further simplifications that lose
information but make the output much easier to understand. These simplifications can
be regarded as configurable, so one may, if desired, omit some of them to reveal more
details. We emphasize that the presented techniques incur information loss and should be
used only for displaying output to a programmer. For example, in Eff ’s interactive loop,
when we define a value, Eff shows the simplified type, but stores the full type in its typing
environment.
6.1. Displaying dirt parameters. First, we can get rid of all inequalities between dirt
parameters. Recall that increasing positive parameters always yields a valid typing, so we
are interested only in their smallest possible value. Since this is exactly
the union of all
S
lower bounds, we display a positive dirt parameter δ+ as the union δ− 6δ+ δ− of all smaller
negative parameters. So, given the constraints
δ1− 6 δ2+ , δ1− 6 δ3+ , δ4− 6 δ2+

30

MATIJA PRETNAR

we can replace δ2+ with its lower bound δ1− ∪δ4− and δ3+ with its lower bound δ1− . In particular,
δ

if a positive dirt parameter δ has no lower bounds, we write A ! δ as A ! ∅, and A −
→ B as
A−
→ B. We keep the negative parameters as they are, because each usually captures a dirt
of some input argument.
Since we can recover the constraints back from the displayed unions, this technique
loses no information, though due to complex dirts, the displayed types are no longer in a
form we can use for inference.
6.2. Displaying type parameters. Next, we could use the same approach for representing type parameters. However, though inequalities between type parameters are crucial for
inference, they do not offer much additional information to the programmer besides telling
what type parameters are of the same shape. So, we can get rid of all inequalities between
type parameters, and label all type parameters in the same skeleton with the same symbol.
So, instead of
δ
δ
(α1 −
→ α2 ) −
→ α3 −
→ α4 | α3 6 α1 , α2 6 α4
which is the inferred type of application fun f 7→ val (fun x 7→ f x), we can write
δ

δ

(α −
→ β) −
→α−
→β
This simplification does incur some information loss — see example at the beginning of
Section 4.
6.3. Displaying region parameters. Finally, we can get rid of region inequalities in the
same way as dirt inequalities, if we replace positive region parameters with their lower
bounds. The problem is that these lower bounds are more complex due to handled regions.
For inhabited parameters ρ̇, which have simpler constraints, we can use the same technique,
except that we also need to collect instance lower bounds. For example, we may write a
parameter ρ̇ with lower bounds
ins1 ∈ ρ̇, ins2 ∈ ρ̇, ρ1 6 ρ̇, ρ2 6 ρ̇
as {ins1 , ins2 } ∪ ρ1 ∪ ρ2 .
For other region parameters, we first employ the techniques suggested in Section 5.3.
Then, we display each constraint ρ− 6 ρ+ ∪ (ρ̇1 ∪· · · · ∪· ρ̇n ) by adding ρ− ´ ρ̇1 ´ · · · ´ ρ̇n to the
lower bounds of ρ+ . We similarly add lower bounds of the form {ins} − · · · for constraints
involving instances. We write ´ to emphasise the fact that we remove a region only if it
is a singleton. If it turns out that any ρ̇ has a single lower bound ins ∈ ρ̇, we write −ins
instead of ´ρ̇.
If ρ´· · · appears in multiple lower bounds but with different handled regions, we display
only the regions that appear in all constraints. Thus, instead of
(ρ ´ ρ̇1 ´ ρ̇2 ´ ρ̇3 ) ∪ (ρ ´ ρ̇2 ´ ρ̇3 ´ ρ̇4 ) ∪ (ρ ´ ρ̇2 ´ ρ̇3 ´ ρ̇5 )
we write just ρ ´ ρ̇2 ´ ρ̇3 .
If there are multiple constraints with the same handled regions, which happens when
we use the same handler more than once, we may merge them. For example, we may write
{ins} ∪ ({ins′ } ∪ ρ) ´ ρ̇1 ´ ρ̇2 . instead of {ins} ∪ ({ins′ } ´ ρ̇1 ´ ρ̇2 ) ∪ (ρ ´ ρ̇1 ´ ρ̇2 )
Still, this may be too much information in some cases, so we can also display ρ′ as
{ins} ∪ ({ins′ } ∪ ρ)? where the question mark lets the programmer know that some of

INFERRING ALGEBRAIC EFFECTS

31

instances in {ins′ } ∪ ρ may be handled and that this lower bound may be decreased if
further information is available. Finally, we can safely omit the question mark and overapproximate the lower bound with {ins, ins′ } ∪ ρ.
Determining the exact level of detail to show is subjective, and further techniques may
arise when the effect system is used in practice.
6.4. Displaying handler types. As mentioned in Section 1.1.3, handler types often have
a repetitive form that we can write in a more compact way. For example, a handler type
α ! {lookup : ρ1 , raise : ρ2 | δ} =
⇒ β ! {lookup : ρ1 ´ ρ, raise : (ρ2 ´ ρ′ ) ∪ ρ′′ | δ}
which describes a handler that handles memory lookups on a region ρ, handles exceptions
from ρ′ and raises exceptions from ρ′′ , can be written simply as
lookup:´ρ, raise:´ρ′ ,+ρ′′

α ================⇒ β
7. Examples
7.1. Function composition. Before we turn to handlers, we display a typical run of the
algorithm on an example with no special algebraic features: function composition, defined
as
def
compose = fun f 7→ val (fun g 7→ val (fun x 7→ let y = f x in g y))
The constraints are computed by the following derivation
Γ ⊢ f : αf | ∅

Γ, y : αy ⊢ g : αg

Γ ⊢ x : αx | ∅

Γ, y : αy ⊢ y : αy

δ1

δ

2
Γ ⊢ f x : α1 ! δ1 | αf 6 (αx −→ α1 )
Γ, y : αy ⊢ g y : α2 ! δ2 | αg 6 (αy −→
α2 )
Γ ⊢ let y = f x in g y : α2 ! δ3 | C
..
.

δ

δ

δ

5
4
3
∅ ⊢ compose : αf −→
αg −→
αx −→
α2 | C

where Γ = f : αf , g : αg , x : αx and
δ

δ

1
2
C = {αf 6 (αx −→
α1 ), αg 6 (αy −→
α2 ), α1 6 αy , δ1 6 δ3 , δ2 6 δ3 }

Unifying the constraints, we see that αf and αg need to be replaced with fresh function
types, and the result of unify(C) is the substitution
δ

δ

6
7
σ = {αf 7→ (α3 −→
α4 ), αg 7→ (α5 −→
α6 )}

and the unified constraints, which are:
C ′ = {αx 6 α3 , α4 6 α1 6 αy 6 α5 , α6 6 α2 , δ6 6 δ1 6 δ3 , δ7 6 δ2 6 δ3 }
Under σ, the inferred type is
δ

δ

δ

δ

δ

6
5
7
4
3
compose : (α3 −→
α4 ) −→
(α5 −→
α6 ) −→
(αx −→
α2 )

so the sets of positive and negative parameters are
N = {αx , α4 , α6 , δ6 , δ7 }

and

P = {α2 , α3 , α5 , δ3 , δ4 , δ5 }

32

MATIJA PRETNAR

After the garbage collection, the only constraints that remain are
gcP,N (C ′ ) = {αx 6 α3 , α4 6 α5 , α6 6 α2 , δ6 6 δ3 , δ7 6 δ3 }
Finally, we replace all positive dirt parameters with the union of their lower bounds, merge
all type parameters in the same skeleton, introduce fresh and readable parameters, and
obtain the final type
δ′

δ

δ∪δ′

compose : (α −
→ β) −
→ (β −
→ γ) −
→ (α −−→ γ)
7.2. Counting printouts. Next, let us define a handler that computes the number of calls
to print on a given channel c:
def

count print = fun c 7→ val (handler
| val x 7→ val 0
| c#print y k 7→ let n = k () in val (succ n)
)
δ

0
The computed type of count print is αc −→
⇒ D), where the form of the dirty types
(C =

def

C = αin ! {print : ρin | δin }

and

def

D = αout ! {print : ρout | δout }

reflects that print is the only operation symbol, appearing in the handler, while the computed constraints (in the order described on page 19) are

→ α2 ! δ2 ), α3 6 nat, α2 6 α3 , δ2 6 δ3 , δ4 6 δ3 ,
(unit −
→ D) 6 (unit −
nat ! δ1 6 D, nat ! δ3 6 D, αc 6 channelρ̇ , ρin 6 ρout ∪· ρ̇, δin 6 δout

After unification and garbage collection, we get that the type of count print is
δ

0
channelρ −→
(αin ! {print : ρin | δin } =
⇒ nat ! {print : ρout | δout })

under the constraints {δin 6 δout , ρ 6 ρ̇, ρin 6 ρout ∪· ρ̇}. If we rename the parameters and
use notation introduced in Section 6, we may write the type as
channelρ1 −
→ (α ! {print : ρ2 | δ} =
⇒ nat ! {print : ρ2 ´ ρ1 | δ})
print:´ρ

or even as channelρ −
→ (α =====⇒ nat).
Define c to be a simple imperative computation std#print "Hello, world!" with the
inferred type unit ! {print : ρ | δ} under the constraint std ∈ ρ. If we use count print to
count the number of std#print calls as
let h = (count print std) in (with h handle c)
the inferred type of the handled computation is nat ! {print : ρ | δ} under the constraints
{std ∈ ρ̇, std ∈ ρ∪· ρ̇}. Since ρ̇ will receive no further lower bounds, we may drop the second
constraint as described in Section 5.3, thus both ρ and δ are completely unconstrained and
we may write the type as nat ! ∅.

INFERRING ALGEBRAIC EFFECTS

33

Conclusion
Related work. Our inference algorithm borrows heavily from existing inference algorithms:
type inference is based on one for structural subtyping of Simonet [28], region inference is
based on one for non-structural subtyping by Pottier [24], and dirt inference is based on
Remy’s row-typing [26]. Furthermore, our algorithm would be unusable in practice without
garbage collection [25, 28, 32] — other lossless techniques presented in Section 5.2 merely
complement it. Our decision to store inferred types in one form but display them in the
other is similar to one in [24] except that to simplify display, we discard not only invariants
that were necessary for inference, but inferred information as well. One point where we differ
from current approaches is the use of unification for solving constraints. Though unification
is simple and familiar, repeated substitution makes it very inefficient, so in practice, it would
be better to replace it with a constraint-based algorithm as described in [28].
The related effect systems can be roughly divided into three groups: effect systems
with no handlers, effect systems for exception handlers, and effect systems for handlers of
arbitrary algebraic effects. So far, there are no approaches that offer general handlers and
are not based on algebraic effects.
Most of the ongoing research considers effect systems for languages without any handlers.
One of the main aims in the early work was a detailed analysis of memory allocation [16, 29,
33]. Due to the lack of handlers, there is no interest in the exact locations being accessed,
only in the parts of the program that share locations from the same memory region. Hence,
ordinary unification together with a simple constraint resolution is enough to infer the
information, though our approach yields the same results.
Recent research acknowledges the importance of a user-friendly output (or input in
prescriptive systems): Scala [27], a popular functional and object-oriented language, has a
prescriptive effect system where a programmer annotates functions with simple labels such
as @pure or @throws[IOException]. Unfortunately, our effect system is descriptive, so we
cannot compare the two at this point.
Koka [13], a recently developed functional language, is based on a descriptive effect
system that represents inferred effects with a row of labels such as exn, io or div. It is
interesting to note that the effect system of Koka used to be based on constraints similar
to ours [30], but they were dropped in favour of rows as they were found to be too complex
in practice. We hope that our decision to keep constraints in the background alleviates this
problem.
We can simulate the row-based approach to effect inference by assigning a single instance
to each effect, though this still gives us results with too precise dirt descriptions. In order
to obtain an output similar to Koka, we need to merge all related dirt parameters into a
single one, just as we do for type parameters.
One effect that we do not treat, but Koka does, is divergence. We can add a dummy
operation ⋆#div and suitably modify the rule Cstr-LetRec to track divergence, but to
prevent div from appearing in almost every practical program, we need to augment the
effect system with some form of termination analysis, just like Koka does. For a practical
language like Koka, this is essential, though we leave it as future work in our development.
Effect systems for exceptions and their handlers [6, 14, 35] often ignore other effects, but
provide much richer information about exception flow. For example, Pessaux & Leroy [14]
provide a row-based effect inference algorithm for OCaml that uses control-flow analysis in
order to provide information about the values that exceptions carry as arguments. This is

34

MATIJA PRETNAR

because handlers in OCaml may be written so that they handle only exceptions with particular arguments, for example only Failure "tl", which is raised when the tail function tl is
applied to an empty list. We believe that in Eff , declaring a new exception emptyListTail
is a cleaner solution and one for which our approach already infers all important information.
Exception arguments aside, the inference algorithm of Pessaux & Leroy produces results
similar to ours (for programs using only exceptions, that is). We already saw at the beginning of Section 1 that both algorithms infer the same types of polymorphic higher-order
functions. To simulate the row-based approach to exception inference, we could utilize our
row-based dirt and take an operation symbol exc with a single instance ⋆ for each exception exc. However, this prevents us from passing around exceptions as first-class values,
so it is better to represent each exception with a separate instance and obtain the same
information in an unrestricted setting.
Handlers of algebraic effects are a recent discovery and so far, there are only three
effect systems beside ours that employ them. First, Frank [17] is a prototype dependentlytyped language with handlers and a prescriptive effect system. Next, there is a library
that provides a simpler form of handlers embedded as a domain specific language (DSL)
inside a dependently-typed language Idris [5]. Finally, the closest to our approach is an
effect system by Kammar, Lindley & Oury [11], with safety results similar to ours, and
an implementation as a DSL inside Haskell. This implementation also uses the type class
mechanism of Haskell to infer effects. The main contributions we bring to the group are
first-class handlers and instances (other approaches use only operations to trigger effects),
and a stand-alone inference algorithm proven to be complete.
Future work. Our inference algorithm is general, offers strong guarantees on the effectful
behaviour, and presents the programmer with information that is easy to understand. There
are, as always, many possible improvements.
In its current form, the presented inference algorithm infers the same types as the
Hindley-Milner algorithm, except that it provides an additional description of effects. However, we can make the effect system prescriptive by adding constraints of the form ρ 6 R,
which limit the allowed instances. Then, a programmer may ensure that a given function will
{raise:∅|δ}

not raise exceptions by simply ascribing it the type α −−−−−−−→ β. Having such constraints
allows us to lift the restrictions placed on the effect signature (discussed in Remark 3.4),
but determining their satisfiability is quite involved. For example, ρ 6 ∅ may be satisfiable
simply because there are no constraints that give a lower bound to ρ. However, a more
comprehensive treatment must also consider the case when a ρ is empty because all of its
instances have been removed by handlers, and this is much more difficult to determine.
Next, let-polymorphism is currently based on value restriction, so that only types of
expressions are generalized. Since we already have an effect system in place, we could relax
this restriction and generalize the types of all pure computations, but this again leads to
the problem of determining empty regions as described in the above paragraph.
Furthermore, Eff allows dynamic creation of fresh instances [2]. Since instances are
a crucial part of our type system, instance generation has to be represented at that level
as well. One option is having dirty types of the form νR.A ! ∆, where R captures the set
of created instances, bound by ν in A ! ∆. Then, the type inference is particularly tricky
as, for example, the type of fun f -> f (); f () should reflect that it creates twice as
much instances as f. A combination with recursion is a separate problem, since programs

INFERRING ALGEBRAIC EFFECTS

35

can then create a potentially infinite number of instances, though a wild card region ⊤ as
discussed in Remark 3.4 may be used in this case.
Finally, before algebraic effects and handlers can be considered practical, we need an
efficient way of evaluating programs that use them. This may be difficult to achieve in
general because of the freedom that handlers allow when manipulating the continuations.
At the very least, running any existing ML programs in the algebraic setting should induce
a minimal overhead.
In this line, we could also pass any information inferred by the effect system to an
optimizing compiler: pure computations may be postponed, and computations with disjoint
effects may be exchanged or even ran in parallel [31]. This looks like a promising and
valuable direction of research, especially because such optimizations have already been
studied in the context of algebraic effects, though without handlers [12].
We hope that the presented work will help the ML community to recognize algebraic
effects as a natural progression of their current type system, and that the Haskell community
will acknowledge the additional flexibility that handlers have to offer.
Acknowledgements
I would like to thank Andrej Bauer, Chris Stone, Ohad Kammar and the anonymous referees
for all their extremely helpful comments and support.
References
[1] 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 — 5th International Conference,
CALCO 2013, Warsaw, Poland, September 3–6, 2013. Proceedings, volume 8089 of Lecture Notes in
Computer Science, pages 1–16. Springer, 2013.
[2] Andrej Bauer and Matija Pretnar. Programming with algebraic effects and handlers. Journal of Logical
and Algebraic Methods in Programming, 2014.
[3] Nick Benton, John Hughes, and Eugenio Moggi. Monads and effects. In Gilles Barthe, Peter Dybjer,
Luis Pinto, and João Saraiva, editors, Applied Semantics, International Summer School, APPSEM
2000, Caminha, Portugal, September 9–15, 2000, Advanced Lectures, volume 2395 of Lecture Notes in
Computer Science, pages 42–122. Springer, 2000.
[4] Nick Benton, Andrew Kennedy, and George Russell. Compiling standard ML to java bytecodes. In
Matthias Felleisen, Paul Hudak, and Christian Queinnec, editors, Proceedings of the third ACM SIGPLAN International Conference on Functional Programming (ICFP ’98), Baltimore, Maryland, USA,
September 27–29, 1998, pages 129–140. ACM, 1998.
[5] Edwin Brady. Programming and reasoning with algebraic effects and dependent types. In Morrisett and
Uustalu [19], pages 133–144.
[6] Manuel Fähndrich and Alexander Aiken. Program analysis using mixed term and set constraints. In
Pascal Van Hentenryck, editor, Static Analysis, 4th International Symposium, SAS ’97, Paris, France,
September 8–10, 1997, Proceedings, volume 1302 of Lecture Notes in Computer Science, pages 114–126.
Springer, 1997.
[7] You-Chin Fuh and Prateek Mishra. Type inference with subtypes. Theoretical Computer Science,
73(2):155–175, 1990.
[8] Martin Hyland, Gordon D. Plotkin, and John Power. Combining effects: Sum and tensor. Theoretical
Computer Science, 357(1):70–99, 2006.
[9] INRIA. OCaml. http://www.ocaml.org/.
[10] Simon Peyton Jones, editor. Haskell 98 Language and Libraries – The Revised Report. Cambridge
University Press, Cambridge, England, 2003.

36

MATIJA PRETNAR

[11] Ohad Kammar, Sam Lindley, and Nicolas Oury. Handlers in action. In Morrisett and Uustalu [19],
pages 145–158.
[12] Ohad Kammar and Gordon D. Plotkin. Algebraic foundations for effect-dependent optimisations. In
John Field and Michael Hicks, editors, Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on
Principles of Programming Languages, POPL 2012, Philadelphia, Pennsylvania, USA, January 22–28,
2012, pages 349–360. ACM, 2012.
[13] Daan Leijen. Koka: Programming with row polymorphic effect types. In Paul Levy and Neel Krishnaswami, editors, Proceedings 5th Workshop on Mathematically Structured Functional Programming,
MSFP 2014, Grenoble, France, 12 April 2014, pages 100–126, 2014.
[14] Xavier Leroy and François Pessaux. Type-based analysis of uncaught exceptions. ACM Transactions
on Programming Languages and Systems, 22(2):340–377, 2000.
[15] Paul Blain Levy, John Power, and Hayo Thielecke. Modelling environments in call-by-value programming languages. Information and Computation, 185(2):182–210, 2003.
[16] John M. Lucassen and David K. Gifford. Polymorphic effect systems. In Jeanne Ferrante and P. Mager,
editors, Conference Record of the Fifteenth Annual ACM Symposium on Principles of Programming
Languages, San Diego, California, USA, January 10–13, 1988, pages 47–57. ACM Press, 1988.
[17] Conor McBride. Frank: An experimental programming language with typed algebraic effects.
https://hackage.haskell.org/package/Frank/.
[18] Robin Milner. The definition of standard ML: revised. The MIT press, Cambridge, MA, USA, 1997.
[19] Greg Morrisett and Tarmo Uustalu, editors. ACM SIGPLAN International Conference on Functional
Programming, ICFP’13, Boston, MA, USA - September 25 - 27, 2013. ACM, 2013.
[20] Benjamin C Pierce. Types and programming languages. The MIT press, Cambridge, MA, USA, 2002.
[21] Gordon D. Plotkin and John Power. Adequacy for algebraic effects. In Furio Honsell and Marino Miculan,
editors, Foundations of Software Science and Computation Structures, 4th International Conference,
FOSSACS 2001 Held as Part of the Joint European Conferences on Theory and Practice of Software,
ETAPS 2001 Genova, Italy, April 2-6, 2001, Proceedings, pages 1–24. Springer, 2001.
[22] Gordon D. Plotkin and John Power. Algebraic operations and generic effects. Applied Categorical Structures, 11(1):69–94, 2003.
[23] Gordon D. Plotkin and Matija Pretnar. Handlers of algebraic effects. In Giuseppe Castagna, editor,
Programming Languages and Systems, 18th European Symposium on Programming, ESOP 2009, Held
as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, York,
UK, March 22–29, 2009. Proceedings, pages 80–94. Springer, 2009.
[24] François Pottier. Type inference in the presence of subtyping: from theory to practice. Technical Report
RR-3483, INRIA, 1998.
[25] François Pottier. Simplifying subtyping constraints: A theory. Information and Computation,
170(2):153–183, 2001.
[26] Didier Rémy. Type inference for records in a natural extension of ML. Theoretical Aspects Of ObjectOriented Programming. Types, Semantics and Language Design. MIT Press, 1993.
[27] Lukas Rytz, Martin Odersky, and Philipp Haller. Lightweight polymorphic effects. In James Noble,
editor, ECOOP 2012 — Object-Oriented Programming — 26th European Conference, Beijing, China,
June 11–16, 2012. Proceedings, pages 258–282. Springer, 2012.
[28] Vincent Simonet. Type inference with structural subtyping: A faithful formalization of an efficient constraint solver. In Atsushi Ohori, editor, Programming Languages and Systems, First Asian Symposium,
APLAS 2003, Beijing, China, November 27–29, 2003, Proceedings, pages 283–302. Springer, 2003.
[29] Jean-Pierre Talpin and Pierre Jouvelot. The type and effect discipline. Information and Computation,
111(2):245–296, 1994.
[30] Ross Tate and Daan Leijen. Convenient explicit effects using type inference with subeffects. Technical
Report MSR-TR-2010-80, Microsoft Research, 2010.
[31] Andrew P. Tolmach. Optimizing ML using a hierarchy of monadic types. In Xavier Leroy and Atsushi
Ohori, editors, Types in Compilation, Second International Workshop, TIC ’98, Kyoto, Japan, March
25–27, 1998, Proceedings, pages 97–115. Springer, 1998.
[32] Valery Trifonov and Scott F. Smith. Subtyping constrained types. In Radhia Cousot and David A.
Schmidt, editors, Static Analysis, Third International Symposium, SAS’96, Aachen, Germany, September 24–26, 1996, Proceedings, pages 349–365. Springer, 1996.

INFERRING ALGEBRAIC EFFECTS

37

[33] Philip Wadler and Peter Thiemann. The marriage of effects and monads. ACM Transactions on Computational Logic, 4(1):1–32, 2003.
[34] Keith Wansbrough and Simon L. Peyton Jones. Once upon a polymorphic type. In Andrew W. Appel
and Alex Aiken, editors, POPL ’99, Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on
Principles of Programming Languages, San Antonio, TX, USA, January 20–22, 1999, pages 15–28.
ACM, 1999.
[35] Kwangkeun Yi and Sukyoung Ryu. A cost-effective estimation of uncaught exceptions in standard ML
programs. Theoretical Computer Science, 277(1):185–217, 2002.

Appendix A. Proofs
Lemma A.1. The following two rules are admissible:
Sub-Trans

Sub-Refl

A 6 A′
A′ 6 A′′
A 6 A′′

A6A

Proof. The proof proceeds by an induction on the structure of types.
The subsumption rules SubExpr and SubComp allow us to increase types of expressions
and computations. Conversely, we may decrease the types in contexts.
Lemma A.2. Take contexts Γ and Γ′ that bind the same variables and assume that for
all (xi : Ai ) ∈ Γ, we have (xi : A′i ) ∈ Γ′ for some Ai 6 A′i . Then, the following rules are
admissible:
SubCtxExpr

SubCtxComp

Γ′ ⊢ e : A
Γ⊢e:A

Γ′ ⊢ c : C
Γ⊢c:C

Proof. The proof proceeds by a routine induction on the derivation of the typing judgement.
To relate monomorphic typing judgements of core Eff to polymorphic inference judgements, we first need to substitute away any variables from the polymorphic context Ξ.
For a polymorphic context Ξ = (xj : ∀Fj . Aj | Cj )nj=1 and expressions (ej )nj=1 , we write
j−1
Γ ⊢ (ej )j |= Ξ if for all j = 1, . . . , n, we have Γ; (xi : ∀Fi . Ai | Ci )i=1
⊢Fj ej : Aj | Cj . In this
def

case, we define the expression e[ej /xj ]j = e[e1 /x1 ][e2 /x2 ] · · · [en /xn ], and the computation
def

c[ej /xj ]j = c[e1 /x1 ][e2 /x2 ] · · · [en /xn ]. Note that because polymorphic definitions may
build on one another, we need to use nested, and not simultaneous substitution.
Proposition A.3 (Soundness).
• Assume that Γ; Ξ ⊢F e : A | C holds and take any expressions (ej )j such that Γ ⊢ (ej )j |= Ξ
j−1
holds and we have σj (Γ) ⊢ ej [ei /xj ]i=1
: σj (Aj ) for any σj |= Cj . Then, for any solution
σ |= C, we also have σ(Γ) ⊢ e[ej /xj ]j : σ(A).
• Assume that Γ; Ξ ⊢F c : C | C holds and take any expressions (ej )j such that Γ ⊢ (ej )j |= Ξ
j−1
holds and we have σj (Γ) ⊢ ej [ei /xj ]i=1
: σj (Aj ) for any σj |= Cj . Then, for any solution
σ |= C, we also have σ(Γ) ⊢ c[ej /xj ]j : σ(C).
Proof. We proceed by a mutual induction on the derivation of inference judgements. In all
cases, we use the same labels as in the considered rule. Also, as we never need the set of
fresh parameters F , we do not write it. Take any suitable (ej )j and any σ that satisfies the

38

MATIJA PRETNAR

set of constraints in the conclusion, and consider the case when the last rule used in the
derivation is:
Cstr-PolyVar: The case for a variable xi ∈ Ξ is immediate because we can use the assumption made for ei = xi [ej /xj ]j .
Cstr-Inst: Since σ |= ins ∈ ρ̇, we have ins ∈ σ(ρ̇). Because ins[ej /xj ]j = ins, we can
use Inst to get σ(Γ) ⊢ ins[ej /xj ]j : σ(E ρ̇ ).
Cstr-Hand: Let A ! ∆ = σ(C) and B ! ∆′ = σ(D). By assumption, we have σ |= Cv , so we
get σ(Γ), x : σ(αin ) ⊢ cv [ej /xj ]j : σ(D v ) by the induction hypothesis. Since σ |= Dv 6 D,
we further get σ(Γ), x : A ⊢ cv [ej /xj ]j : B ! ∆′ . Similarly, we get appropriate results for
each Ψi .
op
op
op
op
Next, for each op ∈ O, let Rin = σ(ρin ) and Rout = σ(ρout ). Now,
S take any ins#op ∈
op
op
op
∆. Then, if op ∈ O, we have ins ∈ Rin . Since σ |= ρin 6 ρout ∪ op=op ρ̇i , we either
i
S
op
have ins ∈ Rout hence ins#op ∈ ∆′ , or ins ∈ op=opi Ri . If op 6∈ O, then ins#op must
be in σ(δin ), thus also in σ(δout ) ⊆ ∆′ . We can then conclude by applying Hand.
Cstr-Op: As we have σ |= C1 , σ |= C2 , and σ |= C, we get σ(Γ) ⊢ e1 [ej /xj ]j : σ(A1 ),
σ(Γ) ⊢ e2 [ej /xj ]j : σ(A2 ), and σ(Γ), y : B op ⊢ c[ej /xj ]j : σ(A ! ∆) by the induction
hypothesis.
Next, because σ |= A1 6 E ρ̇ and σ |= A2 6 Aop , we can use SubExpr to get
σ(Γ) ⊢ e1 [ej /xj ]j : E σ(ρ̇) and σ(Γ) ⊢ e2 [ej /xj ]j : Aop . Then, σ |= ∆ 6 {op : ρ | δ}, and
by SubComp, we get σ(Γ), y : B op ⊢ c[ej /xj ]j : σ(A ! {op : ρ | δ}).
Finally, since σ(ρ̇) ⊆ σ(ρ), we have ins#op ∈ σ({op : ρ | δ}) for any ins ∈ σ(ρ̇), so
we may use Op to conclude.
Cstr-LetVal: By the induction hypothesis for e, we have that the terms e1 , . . . , en , e satisfy
the conditions of the induction hypothesis for c, thus σ(Γ) ⊢ (c[e/x])[ej /xj ]j : σ(C) holds,
and so, we have σ(Γ) ⊢ (let val x = e in c)[ej /xj ]j : σ(C) by LetVal.
Cstr-With: As σ |= C1 and σ |= C2 , we can use induction to get σ(Γ) ⊢ e[ej /xj ]j : σ(A)
and σ(Γ) ⊢ c[ej /xj ]j : σ(C). Next, we have σ |= A 6 (C =
⇒ α ! δ), thus we may use
= σ(α ! δ). So by With, we get σ(Γ) ⊢
SubExpr and get σ(Γ) ⊢ e[ej /xj ]j : σ(C) ⇒
(with e handle c)[ej /xj ]j : σ(α ! δ).
In all other cases, the proof proceeds routinely.

·

·

Lemma A.4 (Weakening).
• If Γ; Ξ ⊢F e : A | C holds, so does Γ; Ξ, (x : ∀F ′ . A′ | C ′ ) ⊢F e : A | C for any x that does
not appear in Γ, Ξ or e.
• If Γ; Ξ ⊢F c : C | C holds, so does Γ; Ξ, (x : ∀F ′ . A′ | C ′ ) ⊢F c : C | C for any x that does
not appear in Γ, Ξ or c.
Proof. The proof proceeds by routine induction on the derivation of inference judgements.
Lemma A.5 (Exchange).
• If Γ; Ξ, (x1 : ∀F1 . A1 | C1 ), (x2 : ∀F2 . A2 | C2 ) ⊢F e : A | C holds, then so does Γ; Ξ, (x2 :
∀F2 . A2 | C2 ), (x1 : ∀F1 . A1 | C1 ) ⊢F e : A | C.
• If Γ; Ξ, (x1 : ∀F1 . A1 | C1 ), (x2 : ∀F2 . A2 | C2 ) ⊢F c : C | C holds, then so does Γ; Ξ, (x2 :
∀F2 . A2 | C2 ), (x1 : ∀F1 . A1 | C1 ) ⊢F c : C | C.
Proof. The proof proceeds by routine induction on the derivation of inference judgements.

INFERRING ALGEBRAIC EFFECTS

39

Lemma A.6.
• For any e, we have that if Γ; Ξ ⊢F e[e′ /x] : A | C holds for some Γ; Ξ ⊢F ′ e′ : A′ | C ′ , so
does Γ; Ξ, (x : ∀F ′ . A′ | C ′ ) ⊢F e : A | C.
• For any c, we have that if Γ; Ξ ⊢F c[e′ /x] : C | C holds for some Γ; Ξ ⊢F ′ e′ : A′ | C ′ , so
does Γ; Ξ, (x : ∀F ′ . A′ | C ′ ) ⊢F c : C | C.
Proof. We proceed by a mutual induction on the structure of the term:
• If e is some variable y 6= x, we have that e[e′ /x] = e, hence Γ; Ξ ⊢F e : A | C. We conclude
by using Lemma A.4.
• If e is the variable x, we also have that Γ; Ξ ⊢F e′ : A | C holds. By induction on the
derivation of inference judgements, we can show that the inferred types and constraints
are unique up to renaming. Thus (∀F ′ . A′ | C ′ ) = (∀F. A | C) up to α-equivalence, so
Γ; Ξ, (x : ∀F ′ . A′ | C ′ ) ⊢F x : A | C holds.
• If e is fun x′ 7→ c, the only way of obtaining the inference judgement is by using Cstr-Fun
to get some Γ; Ξ ⊢F,α fun x 7→ c[e′ /x] : α −
→ C | C. Hence, we have that Γ, x : α; Ξ ⊢F
c[e′ /x] : C | C, so we get Γ, x : α; Ξ, (x : ∀F ′ . A′ | C ′ ) ⊢F c : C | C by the induction
hypothesis. Using Cstr-Fun we obtain the desired conclusion Γ; Ξ, (x : ∀F ′ . A′ | C ′ ) ⊢F,α
fun x 7→ c : α −
→ C | C.
• If e is let val x′ = e′′ in c, the only rule that applies is Cstr-LetVal. We proceed
just as in the previous case by using the induction hypothesis and reapplying the rule
Cstr-LetVal, except that we also need to use Lemma A.5 to obtain the proper ordering
of variables in Ξ.
In all other cases that do not touch Ξ, the proof proceeds routinely just like for functions.
Proposition A.7 (Completeness).
• For any polymorphic context Ξ, closed substitution σ, expressions σ(Γ) ⊢ (ej )j |= Ξ and
any σ(Γ) ⊢ e[ej /xj ]j : A, we have Ξ; Γ ⊢F e : A′ | C and there exists a solution σ ′ |= C,
which extends σ to F , such that σ(A′ ) 6 A.
• For any polymorphic context Ξ, closed substitution σ, expressions σ(Γ) ⊢ (ej )j |= Ξ and
any σ(Γ) ⊢ c[ej /xj ]j : C, we have Ξ; Γ ⊢F c : C ′ | C and there exists a solution σ ′ |= C,
which extends σ to F , such that σ(C ′ ) 6 C.
Proof. We again proceed by a mutual induction, this time on the derivation of typing
judgements. In all cases, we again use the same labels as in the considered rule.
Note that no parameters from F can appear in Γ, and we may safely assume that σ
is undefined on F . Furthermore, we may safely compose substitutions that are defined on
disjoint sets of parameters. For example, by taking σ1 and σ2 that extend σ to disjoint
sets F1 and F2 , respectively, we may uniquely define σ ′ = σ ∪ σ1 ∪ σ2 , which extends σ to
F1 ∪ F2 .
Consider the case when the last rule used in the derivation is:
Inst: Assume that σ(Γ) ⊢ ins : E R for some ins ∈ R. By Cstr-Inst, we first get Γ ⊢ρ̇ ins :
E ρ̇ | ins ∈ ρ̇. Next, we extend σ to ρ̇ by defining σ ′ = σ ∪ {ρ̇ 7→ R}. By assumption, we
have ins ∈ R, so σ ′ |= ins ∈ ρ̇ by definition. Finally, we get σ ′ (E ρ̇ ) 6 E R by Sub-Refl.
Hand: From the value case and operation cases, we get the necessary premises Ψv and (Ψi )i
of Cstr-Hand, and solutions σv , (σi )i and (σi′ )i that satisfy the required properties. We

40

MATIJA PRETNAR

then define
σ = σv ∪

[
i

σi ∪

[
i

n
σi′ ∪ αin 7→ A, αout 7→ B, δin 7→ {ins#op ∈ ∆ | op 6∈ O},
δout 7→ {ins#op ∈ ∆′ | op 6∈ O}, (ρ̇i 7→ Ri )i ,
op

(ρin 7→ {ins | ins#op ∈ ∆})op∈O ,
(ρout 7→ {ins | ins#op ∈ ∆′ })op∈O
op

o

We routinely check that σ satisfies all the necessary conditions and that we can apply
Cstr-Hand to obtain the expected result.
SubExpr: By assumption, we have σ(Γ) ⊢ e[ej /xj ]j : A′ for some σ(Γ) ⊢ e[ej /xj ]j : A and
A 6 A′ . By induction hypothesis, we have Γ ⊢F e : A′′ | C and σ ′ |= C that extends σ to
F such that σ ′ (A′′ ) 6 A. We may then use Sub-Trans to get σ ′ (A′′ ) 6 A′ .
Op: Assume σ(Γ) ⊢ (e1 #op e2 (y. c))[ej /xj ]j : A ! ∆ for some σ(Γ) ⊢ e1 [ej /xj ]j : E R ,
σ(Γ) ⊢ e2 [ej /xj ]j : Aop , and σ(Γ), y : B op ⊢ c[ej /xj ]j : A ! ∆. By induction hypothesis,
we get Γ ⊢F1 e1 : A1 | C1 , Γ ⊢F2 e2 : A2 | C2 , and Γ, y : B op ⊢F c : C | C, together with
σ1 , σ2 , and σ ′ that satisfy the required properties. Using Cstr-Op, we get
Γ ⊢F1,F2 ,F,ρ,ρ̇,δ e1 #op e2 (y. c) : A ! {op : ρ | δ}
| C1 , C2 , C, A1 6 E ρ̇ , A2 6 Aop , ρ̇ 6 ρ, ∆ 6 {op : ρ | δ}
We extend σ to all the fresh parameters by
σ ′′ = σ1 ∪ σ2 ∪ σ ′ ∪ {ρ 7→ R, ρ̇ 7→ R, δ 7→ {ins#op′ ∈ ∆ | op′ 6= op}}
We conclude the proof by observing that σ ′′ satisfies all the necessary conditions.
LetVal: As σ(Γ) ⊢ (let val x = e in c)[ej /xj ]j : C, we get some σ(Γ) ⊢ (c[e/x])[ej /xj ]j :
C. By induction hypothesis, we get some Γ; Ξ ⊢F1 e : A | C1 and Γ; Ξ ⊢F2 c[e/x] : C ′ | C2
together with σ |= C2 such that σ(C ′ ) 6 C. Then, by Lemma A.6, we have that
Γ; Ξ, (x : ∀F1 . A | C1 ) ⊢F2 c : C ′ | C2 , so we may conclude by using Cstr-LetVal.
⇒A!∆
With: As σ(Γ) ⊢ (with e handle c)[ej /xj ]j : A ! ∆ we get σ(Γ) ⊢ e[ej /xj ]j : C =
′
and σ(Γ) ⊢ c[ej /xj ]j : C. Next, by induction hypothesis, we get Γ ⊢F1 e : A | C1 together
⇒ A ! ∆. Similarly, we get
with σ1 |= C1 that extends σ to F1 , such that σ1 (A′ ) 6 C =
Γ ⊢F2 c : C ′ | C2 together with σ2 |= C2 that extends σ to F2 , such that σ2 (C ′ ) 6 C.
By Cstr-With, we get
⇒ α ! δ)
Γ ⊢F1,F2 ,α,δ with e handle c : α ! δ | C1 , C2 , A′ 6 (C ′ =
We define

σ ′ = σ1 ∪ σ2 ∪ {α 7→ A, δ 7→ ∆}
which extends σ to all the fresh parameters. Since σ ′ extends σ1 and σ2 , we have σ ′ |= C1
and σ ′ |= C2 . Furthermore,
σ ′ (A′ ) = σ1 (A′ ) 6 C =
⇒ A ! ∆ 6 σ2 (C ′ ) =
⇒ A ! ∆ = σ ′ (C ′ =
⇒ α ! δ)

hence σ ′ satisfies all the necessary conditions. Finally, we have σ ′ (α ! δ) 6 A ! ∆ by
Sub-Refl.
SubComp: The proof proceeds in the same way as in the case of SubExpr.
In all other cases, the proof again proceeds routinely.

INFERRING ALGEBRAIC EFFECTS

41

Proof of Theorem 3.3. Take any Γ ⊢ e : A′ . We may then use Proposition A.7 for the empty
context Ξ and the identical substitution to obtain Γ ⊢ e : A | C such that A′ ∈ JA | CK. Since
A and C are uniquely determined up to a renaming, we may use the same reasoning for any
A′′ and get {A′′ | (Γ ⊢ e : A′′ )} ⊆ JA | CK. The converse follows from Proposition A.3 while
the case for computations is exactly the same.
Proof of Lemma 4.2. We can define a solution σ of a unified set of constraints C as follows.
For all type parameters α and all dirt parameters δ, we define σ(α) = unit and σ(δ) = ∅.
Then, σ trivially satisfies all type and dirt constraints in C. In a similar way, we also show
that σ(α) ≈ σ(α′ ) for any α ≈C α′ . In fact, we get a solution whenever we replace all type
parameters in the same skeleton with the same type.
S
σ satisfies
For region parameters, S
we define σ(ρ) = {ins | (ins ∈ ρ ∪ i ρ̇i ) ∈ C}. Then,
S
′ ∪
ρ̇
ρ̇
)
∈
C.
Next,
take
a
constraint
(ρ
6
ρ
all constraints
(ins
∈
ρ
∪
i
i∈I i ). Then
i
S
S
ρ̇
)
∈
C
because
C
is
unified.
Thus, if
(ins ∈ ρ ∪ i∈J ρ̇i ) ∈ C implies (ins 6 ρ′ ∪ i∈I∪J
S i
′
′
ins ∈ σ(ρ) then ins ∈ σ(ρ ), and so σ |= ρ 6 ρ ∪ i ρ̇i .
There are, of course, countless other ways of choosing σ.

·

·

·

·

·

·

Proof of Proposition 4.4. We see that unify always terminates because at each recursive
call, we strictly decrease the degree, defined lexicographically according to:
(1) the number of skeletons of ≈C ,
(2) the number of all type constructors in Q,
(3) the total potential of all dirt parameters, where the potential of a dirt parameter δO is
the number of all operation symbols mentioned in Q that do not appear in O,
(4) the number of constraints in Q.
Because of occur check, (1) decreases each time we unify any constraint of the form α 6 A
or A 6 α. When decomposing constraints between types of the same form, we keep (1) as
it is, but decrease (2). When we unify a constraint α 6 α′ , (1) decreases if α was not in the
same skeleton as α′ . If it was, (1–3) remain the same, but (4) decreases. A similar situation
occurs when unifying region constraints or dirt constraints with matching operations. If we
unify dirt with non-matching annotations, we keep type constraints and thus (1–2) as they
are, but ensure that (3) decreases.
To show that unification preserves solutions, we observe that at each recursive call
unify(σk ; Ck ; Qk ) = unify(σk+1 ; Ck+1 ; Qk+1 ), and for each σk′ |= Ck ∪ Qk , there exists
′
′
◦ σk+1 . Similarly, we observe that if
|= Ck+1 ∪ Qk+1 such that σk′ ◦ σk = σk+1
σk+1
unify(σ; C; Q) results in a failure, then C ∪ Q does not have any solutions.
Since we start with σ0 = id, C0 = ∅ and Q0 = C and end with some σn = σ ′ , Cn = C ′
and Qn = ∅, then for each σ |= C, we have some σ ′′ |= C ′ such that σ = σ ′′ ◦ σ ′ .
Proof of Corollary 4.5. Let us show the soundness of rule Unify-Expr, because the proof
for Unify-Comp is exactly the same. First, take any σ ′ |= C ′ . By Proposition 4.4, we know
that σ ′ ◦ σ |= C, so by the induction hypothesis, we get (σ ′ ◦ σ)(Γ) ⊢ e : (σ ′ ◦ σ)(A), which
is exactly what we wanted to prove.
For the other direction, take any σ ′′ |= C. Again by Proposition 4.4, there must exist
some σ ′ |= C ′ such that σ ′′ = σ ′ ◦ σ. We then get σ ′ (σ(Γ)) ⊢ e : σ ′ (σ(A)) or, equivalently,
σ ′′ (Γ) ⊢ e : σ ′′ (A) by the induction hypothesis.
Proof of Proposition 5.3. Again, we shall prove only the soundness of rule GC-Expr, because the proof for GC-Comp is identical. The soundness of the reverse rule is trivial:

42

MATIJA PRETNAR

any solution σ |= C is also a solution of gcP,N (C) so by induction hypothesis, we get
σ(Γ) ⊢ e : σ(A).
For the forward direction, the reasoning follows the one sketched in the beginning of
Section 5.1. Take any solution σ ′ |= gcP,N (C). Following [28], we are going to construct
a solution σ |= C such that σ(α+ ) 6 σ ′ (α+ ) holds for all α+ ∈ P and σ ′ (α− ) 6 σ(α− )
holds for all α− ∈ N (and similarly for region and dirt parameters). Then, by the induction
hypothesis, we get σ(Γ) ⊢ e : σ(A). Since P contains pos(A) and N contains neg(A),
we have σ(A) 6 σ ′ (A), thus by SubExpr we get σ(Γ) ⊢ e : σ ′ (A). Conversely, for all
(xi : Ai ) ∈ Γ, the set P contains neg(Ai ) and N contains pos(Ai ), so we get σ ′ (Ai ) 6 σ(Ai ).
We may thus use SubCtxExpr and get σ ′ (Γ) ⊢ e : σ ′ (A).
We construct σ |= C as follows. Let us start with the simplest case of dirt parameters.
We define
[
def
σ(δ) =
σ ′ (δ− )
(δ− 6δ)∈C
δ− ∈N
−
(δ 6 δ− )

First, for any δ− ∈ N , we implicitly have
∈ C, so σ ′ (δ− ) ⊆ σ(δ− ). Next, for any
+
−
+
−
δ ∈ P , if have (δ 6 δ ) ∈ C, we also have δ 6 δ+ ∈ gcP,N (C) since δ− ∈ N . Because
σ ′ |= gcP,N (C), we have σ ′ (δ− ) ⊆ σ ′ (δ+ ), so
[
[
σ(δ+ ) =
σ ′ (δ− ) ⊆
σ ′ (δ+ ) = σ ′ (δ+ )
δ− 6δ+

δ− 6δ+

Finally, we need to show that σ satisfies all dirt constraints in C. Take some (δ 6 δ′ ) ∈ C.
Now, if (δ− 6 δ) ∈ C holds for some δ− ∈ N , then (δ− 6 δ′ ) ∈ C holds as well because C is
unified and therefore closed under logical implication. Thus σ(δ′ ) is defined as a union over
a bigger index set than σ(δ), so σ(δ) ⊆ σ(δ′ ) and σ |= δ 6 δ′ .
For type parameters α, we proceed similarly and define
[
def
σ(α) =
σ ′ (α− )
(α− 6α)∈C
α− ∈N

where we define union over closed types as:
bool ∪ bool = bool
nat ∪ nat = nat
unit ∪ unit = unit
empty ∪ empty = empty

→ C 2 ) = (A1 ∩ A2 ) −
→ (C 1 ∪ C 2 )
(A1 −
→ C 1 ) ∪ (A2 −
E R1 ∪ E R2 = E R1 ∪R2
⇒ D1 ) ∪ (C 2 =
⇒ D 2 ) = (C 1 ∩ C 2 ) ⇒
= (D 1 ∪ D 2 )
(C 1 =
(A1 ! ∆1 ) ∪ (A2 ! ∆2 ) = (A1 ∪ A2 ) ! (∆1 ∪ ∆2 )

The intersection is defined dually. We can see that the union is well defined because for
all (α− 6 α) ∈ C, we have α− ≈C α, hence all such α− belong to the same skeleton of ≈C ,
and so also of ≈gcP,N (C) . Since σ ′ is a solution of gcP,N (C), all types σ ′ (α− ) are of the same
shape.
We also need to consider the case when the union is empty because there are no α− ∈ N
such that (α− 6 α) ∈ C. In this case, we set σ(α) to be the intersection of σ ′ (α′ ) for all
α ≈C α′ . Then, σ(α) 6 σ ′ (α) holds in case α ∈ P , and σ satisfies all constraints (α 6 α′ ) ∈ C.
If we have a constraint (α′ 6 α) ∈ C, then α′ also cannot have any negative lower bounds
because C is closed, hence σ(α′ ) = σ(α). Finally, the case α ∈ N cannot occur.

INFERRING ALGEBRAIC EFFECTS

43

For region parameters ρ, we need to take both instances and handled regions into an
account. So, we define

[
[
[
[
 

def
σ ′ (ρ− ) −
{ins} −
σ(ρ) =
σ ′ (ρ̇i ) ∪
σ ′ (ρ̇i )

·

S
(ρ− 6ρ∪ i ρ̇i )∈C
ρ− ∈N

·

S
(ins∈ρ∪ i ρ̇i )∈C

i

·

·

i

As before, we get σ ′ (ρ− ) 6 σ(ρ− ) for all ρ− ∈ N and σ(ρ+ ) 6 σ ′ (ρ+ ) for all ρ+ ∈ P . Next,
let us show
S that σ satisfies all region constraints in C. Let us consider only ones of the form
the proof for ones with instances is similar. S
(ρ 6 ρ′ ∪ i∈I ρ̇i ) ∈ C because
S
−
to σ(ρ), we have (ρ− 6 ρ′ ∪ i∈I∪J ρ̇i ) ∈ C
For any (ρ 6 ρ ∪ i∈J ρ̇i ) ∈ C contributing
S
′
′
−
because
unified. Thus, σ (ρ ) − i∈I∪J σ (ρ̇i ) ⊆ σ(ρ′ ) by the definition of σ(ρ′ ). If we
S C is
′
add i∈I σ (ρ̇i ) to both sides, we get
[
[

σ ′ (ρ− ) −
σ ′ (ρ̇i ) ⊆ σ(ρ′ ) ∪
σ ′ (ρ̇i )

·

·

·

·

We similarly get
{ins} −
for each (ins ∈ ρ ∪
σ(ρ), thus

·

S

i∈J

·

·

·

i∈J

·

i∈I

i∈J

[

σ ′ (ρ̇i ) ⊆ σ(ρ′ ) ∪

·

i∈I

[

σ ′ (ρ̇i )

ρ̇i ) ∈ C that contributes to σ(ρ). These are all contributions to
σ(ρ) ⊆ σ(ρ′ ) ∪

·

[

i∈I

σ ′ (ρ̇i )

Now comes the critical step: since ρ̇i ∈ P , we have σ(ρ̇i ) ⊆ σ ′ (ρ̇i ). However, σ(ρ̇i ) was
non-empty and if we increase it, it contributes less to the singleton union, therefore
[
σ(ρ) ⊆ σ(ρ′ ) ∪
σ(ρ̇i )
i∈I
S
and σ |= (ρ 6 ρ′ ∪ i∈I ρ̇i ).
A careful reader might have observed
S that not all parameters ρ̇i occur in P , only those
that appear in constraints ρ− 6 ρ+ ∪ i ρ̇i where ρ− ∈ N and ρ+ ∈ P0 (and similar ones
for instances). However, this is easy to fix.
First, take P ′ to be P0 and the set of all parameters ρ̇i that appear in any singleton
union in any constraint in C. In this case, the above reasoning is valid and the set of
constraints gcP ′ ,N (C) is equivalent to C. Now, repeat the whole process and take P ′′ to be
P0 and all parameters that appear in any singleton union in any constraint in gcP ′ ,N (C).
Again, gcP ′′ ,N (C) is equivalent to gcP ′ ,N (C) and so also to C. However, the only region
S
constraints left in gcP ′ ,N (C) are ones of the form ρ− 6 ρ+ ∪ i ρ̇i with ρ− ∈ N and ρ+ ∈ P0 ,
thus P ′′ = P .
In the end, let us show that gcP,N (C) is unified if C is. We can consider only the case for
type constraints as for other cases the proof is almost exactly the same. Take constraints
α1 6 α2 and α2 6 α3 in gcP,N (C). Since gcP,N (C) ⊆ C, these two constraints must also
be in C, which is unified, hence α1 6 α3 is in C as well. From our assumption we have
α1 , α2 ∈ N and α2 , α3 ∈ P , therefore (α1 6 α3 ) ∈ gcP,N (C). We can similarly show that if
we have α 6 α′ ∈ gcP,N (C), then α ≈gcP,N (C) α′ .

·

·

·

·

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

