One-shot Algebraic Effects as Coroutines
Satoru Kawahara1,2 and Yukiyoshi Kameyama1,3
1

Department of Computer Science, University of Tsukuba, Japan2
sat@logic.cs.tsukuba.ac.jp
3kameyama@acm.org

Abstract. This paper presents a translation from algebraic effects andhandlers to asymmetric coroutines, which provides simple, portable andwidely applicable implementation of algebraic effects. Algebraic effects
and handlers are an emerging new feature to model effectful computations and attract attention not only from researchers but also from programmers. They are implemented in various ways as part of compilers,interpreters, or as libraries. We present a direct embedding of one-shot
algebraic effects and handlers in a language which has asymmetric coroutines. The key observation is that, by restricting the use of continuations
to be one-shot, we obtain a simple and sufficiently general implementation via coroutines, which are available in many modern programming
languages. Our translation is a macro-expressible translation, and wehave implemented it embedding as a library in Lua and Ruby, whichallows one to write effectful programs in a modular way using algebraic
effects and handlers.
Keywords: Algebraic Effects and Handlers · Coroutines · Continuations· Control Operators · Macro Expressibility

1Introduction

Algebraic effects [21] and handlers [22] (AEH for short) are an emerging newfeature to model effectful computations in a modular way. They are gaining more
and more attention not only from researchers but also from practitioners. There
are a few dedicated programming languages such as Eff [1], Multicore OCaml [7]and Koka [17] which have AEH as language primitives, and several main-stream
programming languages such as Haskell, OCaml, Scala, JVM bytecode and C
have library implementations for AEH. However, AEH is not yet available inmany other main-stream programming languages, which is a big obstacle toutilize theoretical results on AEH in real-world software. We, therefore, thinkthat it is an important and timely issue to develop a systematic implementation
method for AEH which is available in many existing programming languages.
AEH have been so far implemented in several ways such as the one basedon stack manipulation, delimited-control operators [6], or free monad. Unfortunately, none of them are fully satisfactory; The implementation method basedon stack manipulation is used for JVM bytecode and C [4,18], however, animplementer needs deep insight on its internal structure. It then follows that

2

Satoru Kawahara and Yukiyoshi Kameyama

the implementation cost is rather high, which prevents the feature from being implemented in various language systems. The implementation method via
delimited-control operators is used for OCaml and Scala [3,16]. It is a systematic
way to implement AEH, since it needs no knowledge on low-level features, however, only few languages have delimited-control operators as built-in primitives.
The implementation method based on free monads is yet another systematic way,
and used in Haskell and Scala [14,15]. While elegant, its major demerits are thatit enforces a programmer to use monadic-style, and that it is often inefficient.
This paper presents a new systematic method of implementing algebraic effects and handlers which is general, available in many languages, and simple
and portable, compared to the existing implementations. The key of our method
is to use coroutines to embed them in programming languages. Today we see
a number of programming languages which have coroutines as a built-in feature, which makes it possible to apply our implementation method in various
languages with no or little cost. While coroutines are less expressive than general delimited-control operators, they are as expressive as one-shot delimited
control-operators, a restricted control operator that is allowed to invoke a delimited continuation at most once [20]. One-shot delimited-control operators are
known to be implemented more efficiently than general, multi-shot ones, thanks
to the fact that no copying of continuations is necessary [5]. Hence, we face thetrade-off between expressiveness and efficiency. This paper studies the one-shot
variant which gives less expressive, but more performant primitives for AEH. In
fact, various control effects are expressible with the one-shot variant.
We translate one-shot AEH to asymmetric coroutines. The salient featureof our translation is that it is a macro-expressible translation in the sense ofFelleisen. Thanks to this property, we can implement AEH as a simple library,
and we have created AEH libraries for Lua 4 and Ruby5 , which have been published via github. Our libraries have been used by several users, and interested
users have ported our libraries to other languages67 .
Our main contributions in this paper are the following.
– We show an embedding of one-shot algebraic effects and handlers. We use
standard asymmetric coroutines only, and no special control features areneeded. Hence our embedding is applicable to various languages as long as
they have asymmetric coroutines.
– Comparing to the embedding based on free monads, our method does notforce programmers to use monadic style, and our embedding is more performant in many cases than the one based on free monads.
– Our embedding is defined as local and compositional translation from algebraic effects and handlers. Thanks to this property, we can implement theembedding as a library, and in fact we have done it for Lua and Ruby, which
4

https://github.com/nymphium/eff.lua
https://github.com/nymphium/ruff
6
https://github.com/MakeNowJust/eff.js
7
https://github.com/pandaman64/effective-rust Since Rust does not have coroutines,
Future is used instead.
5

One-shot Algebraic Effects as Coroutines

3

is available on GitHub. Algebraic effects and handlers is a complex system,and the implementation can be therefore error-prone. So our formalized implementation is desirable.
This paper is organized as follows. Section 2 shows typical examples using
AEH and demonstrates our algebraic-effect library for Lua. Section 3 describes
the embedding method by defining the translation from λeff , a language withalgebraic effect handlers, to λac , a language with asymmetric coroutines. We also
show that our translation is macro expressible in the sense of Felleisen. Section 4
discusses the extension of our model definitions for implementing our libraries
in Lua and Ruby, and problems in actual use. Section 5 shows the performance
evaluation of our embedding by comparing ours with the embedding based onfree monads. Section 6 describes related work, and Section 7 concludes.

2

Examples of one-shot algebraic effects

This section illustrates programming with AEH by examples. To express them,
we use the programming language Lua extended with our library, which is implemented using our embedding explained in the subsequent sections.
2.1

Exception

In our view, AEH is a generalization of exceptions, which is justified by thefollowing examples.
The function inst provided by our library creates, when called with zeroargument, a new label for an algebraic effect, and returns it.
1

local DivideByZero = inst()
We can invoke the labeled effect by calling the function perform in our library.

1
2
3
4
5
6
7

local div = function(x, y)
if y == 0 thenreturn perform(DivideByZero, nil)else
return x / y
end
endThis code snippet is Lua’s definition for the function div, which takes two argument x and y. It returns the result of dividing x by y unless y is 0. If y is 0,
it performs the effect labeled by DivideByZero, which means that an effect israised and the control of the program is brought to the nearest effect handler(which is not shown in the above code) similarly to exception handling.
Our library provides the function handler to create a new effect handler.

4

1
2
3
4
5
6

Satoru Kawahara and Yukiyoshi Kameyama

local with_nil = handler {val = function(_) return nil end,
[DivideByZero] = function(_, _)return nil
end}
The function handler receives a table, Lua’s data structure for an associativearray8 , as its sole argument in which e1 = e2 represents the key-value pair ["e1"] = e2. The first key-value pair (Line 2) has the key val, and defines avalue handler which is used when no effect happens, and the second key-value
pair (Lines 3 and 4) defines how the effect DivideByZero is processed. The
value part of the key-value pair is a function in both cases. While the value
handler receives one argument (which corresponds to the result of the handledexpression), the effect handler receives two arguments, the first of which is theargument of the effect invocation and the second is a delimited continuation
when the effect has been invoked (up to the handler invocation).
In the above snippet, the arguments are ignored, and the whole computation
returns nil in both cases, representing simple exception capturing. By evaluating
with_nil(function() return div(3, 0) end), we get nil as the result.
We can turn the above simple exception to a resumable exception by changing
the effect handler as follows.

1
2
3
4
5
6

local with_default_zero = handler {val = function(v) return v end,
[DivideByZero] = function(_, k)return k(0)end}Here we changed the second case of the handler (Lines 3 and 4) so that a parameter k is bound to the second argument (delimited continuation), which is
invoked with the argument 0, and its value becomes the final result.
We can test the handler with_default_zero as follows.

1
2
3
4

with_default_zero(function()
local v = div(3, 0)
return v + 20
end)
When we execute Line 2 of this code, the effect DivideByZero is performed(raised) as before. Then the handler with_default_zero catches it, and captures
the delimited continuation local v = ; return v + 20, which is bound tothe variable k. (Strictly speaking, the delimited continuation should be surrounded by the handler with_default_zero, but we omit it here since there
8

https://www.lua.org/manual/5.3/manual.html#3.4.9

One-shot Algebraic Effects as Coroutines

5

is no effect in the continuation and its value handler is the identity function.)
Then we execute k(0), which is equivalent to local v = 0; return v + 20.
The net effect is the same as the case when div(3,0) returns 0, and the entire
computation results in 0 + 20 = 20.
2.2

State

AEH can express not only exceptions, but also many other effects. Here, we show
how state can be expressed in terms of these operations using the state-passing
technique.
We first create two effect labels.
1
2

local Get = inst()
local Put = inst()
We then define the function run to execute stateful computations.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17

local run = function(init, task)
local step = handler {val = function(_) return function() end end,[Get] = function(_, k)return function(s)return k(s)(s)end
end,[Put] = function(s, k)return function(_)
return k()(s)
end
end
}
return step(task)(init)
end
The function takes two arguments init for the initial state (such as a single value
or a tuple of several values) and a thunk task for the stateful computation. It
first defines the handler step, which manipulates the normal-return case andthe two effects labeled by Get and Put. Following the state-passing scheme, thevalue handler returns a function which ignores its argument (for state). In thestateful computation, when the effect Get is invoked, then the handler returns
the function that retrieves the current state s. and supplies it to the current
continuation (k(s) in line 6) with the same state s. When the effect Put withan parameter s is invoked, the handler returns a thunk in which a meaninglessvalue () is passed to the continuation, but a new state s is installed (line 11).
After defining the handler, the function run executes the computation task with
the initial state init (line 16).

6

Satoru Kawahara and Yukiyoshi Kameyama

Note that it is important that the captured continuation is surrounded by
the same handler step. In fact, the algebraic effects and handler are similar tothe control operators shift0 and reset0 [19]; when an effect is invoked by shift0
and captured by reset0, the captured delimited continuation is surrounded by
the delimiter reset0.
2.3

Expressing other Computational Effects

We can express other advanced control effects using one-shot algebraic effects
and handlers. Examples include generators and iterators, let-insertion in partial
evaluation, and Go language’s defer9 , Due to lack of space, we cannot showthese examples in this paper. See the github repository of our library. We havealready implemented async/await, shift/reset, fetching current time (a sort ofdependency injection) and measuring execution time, by our library.

3

Embedding Algebraic Effects with Coroutines

This section explains our translation from one-shot algebraic effects and handlers
to asymmetric coroutines. For this purpose, we define λeff , a language which has
one-shot AEH, and λac , a language which has asymmetric coroutines. We thentranslate λeff to λac , and show that it is a macro-expressible translation.
3.1

λeff

λeff is an untyped language with one-shot AEH based on Effy [23]. For simplicity,
we omit dynamic creation of effect lablels.
Figure 1 defines the syntax of λeff . The set Effects is a finite set of effect lables, and we use eff as meta variables for it. The syntactic categories
v, e, and h, resp. represent values, expressions and handler expressions, resp.
The expression perform eff v invokes the effect eff with the argument v, andwith v handle e evaluates e under the handler specified by the value v. A usual
let binding is written as let x = c1 in c2 .
The handler expression handler eff (val x → e1 ) ((y, k) → e2 ) creates a handler which catches the effect eff and returns the value of e2 where y is bound to
the argument of the effect-performing operation, and k is bound to the delimited
continuation when the effect is invoked. The expression val x → e1 gives a value
handler, namely, a handler which is used when the body of a handler returns
normally (does not invoke an effect). For simplicity, λeff can handle only one
effect per handler, whereas handlers in Effy can cope with multiple effects. But
the latter can be simulated by our single-effect handlers, and our library actuallyprovides the multi-effect variant; see Section 4.
The syntactic category w and the subsequent lines are used to define thesemantics of λeff . The class w represents runtime values for function closures
9

https://golang.org/ref/spec#Defer statements

One-shot Algebraic Effects as Coroutines

7x ∈ Variables
eff ∈ Effects
v ::= x | h | λx. ee ::= v | v v | let x = e in e
| perform eff v | with v handle eh ::= handler eff (val x → e) ((x, x) → e)w ::= clos (λx.e, E) | closh (h, E)
F ::= ( e, E) | w | (let x =  in e, E)| (with w handle )eff| (with  handle e, E)
C ::= e | w
E ::= [] | (x = w) :: E
K ::= [] | F :: K

Fig. 1: Syntax and runtime representation of λeff

(clos (λx.e, E)) and handlers (closh (h, E)) where E is a runtime enviroment,
and F represents a frame, or a singular context, which means a ’one-step’ fragment of a continuation. A (delimited) continuation K is a list of frames.
The call-by-value operational semantics of λeff is defined in the CEK-machinestyle [9]. We give it in Section A of the appendix of this paper, and here we informally explain the effect primitives only. The handler expression handler eff (val x → ev ) ((x, k) → eef )creates a handler which consists of a value handler and an effect handler, andassociates the effect label eff to it. The expression with h handle e (which iscalled a handling expression) evaluates the expression e under the handler h. The
expression perform eff v invokes the effect eff with an argument v. Note that
handling expressions may be nested, and an effect invocation is caught (handled) by the nearest (innermost) handler which can handle the effect. When thehandled expression is evaluated to a value, the value handler is used.

3.2

λac

De Moura and Ierusalimschy’s seminal work [20] classified various forms of coroutines found in programming languages, and formalized calculi for symmetriccoroutines and asymmetric coroutines. The former represents classic coroutines
which can call (resume) other coroutines, but coroutines cannot return to theircallers. The latter represents modern coroutines where the caller-caller relation
exists, hence, coroutines may return to their callers.

8

Satoru Kawahara and Yukiyoshi Kameyama

The language λac is based on asymmetric coroutines10 . For the purpose oftranslation and practical programming, we have added to this language several
constructs such as data constructors, let with recursion, pattern matching, andcomparison operators.
Figure 2 defines the syntax of λac . The syntactic categories K and l, resp.,
represent data constructors and labels for coroutines, resp. The set eff corresponds to the set of effect labels in λeff , and we assume that its elements areconstants in λac Values v are either constants, an expression formed by applying−
a data constructor to values K →v ? , labels, variables, or lambda expressions. Expressions e are those in lambda calculus extended with conditional expressions,pattern matching and mutual recursion, plus those for asymmetric coroutines:l : e for a labeled expression which represents the “return point” of resuming a
coroutine, create e for creating a coroutine and returning its label, resume e1 e2
for resuming (calling) a coroutine, and yield e for yielding a value and returning
to the caller of the current coroutine.
−−−−−−
−−−→
−
−
−
f→
x is an abbreviation of f x0 x1 · · · · · · xn and and g →y = e is of and g0 →
y =
→
−
→
−
e0 and g1 y = e1 and · · · · · · and gm y = em . A similar abbreviation is applied
to constructors and pattern matching.
The expression match e with cases is for pattern matching. We add restricted−
guards to pattern matching so that cases may contain a form K →x when x =x → e. This restricted form is sufficient for our purpose.
The call-by-value operational semantics of λac is defined in the same way
as de Moura and Ierusalimschy and given in Section B of Appendix. Here webriefly explain the semantics of the primitives for coroutine; create e creates aunique label and a coroutine with its body being the value of e, and returns thelabel. The expression resume l v resumes the coroutine labeled with l against
the argument v. It is an error if a coroutine whose label is l does not exist, or
has already been called. A resumed coroutine must return to the caller, so wecreate an expression l : e3 where ee is the body of the resumed coroutine. Whenan expression yield v is called in the evaluation of a coroutine, the coroutine issuspended and stored for future use, and v is returned to the caller of the current
coroutine. It is an error if there is no caller of the current coroutine when yield
is invoked.

3.3

Translation from λeff to λac

We present a program translation from λeff to λac , which is syntax-directed andcompositional. The whole translation is defined in Figure 3 where a λeff -term eis translated to a λac -term VeW.
The translation is homomorphic for a variable, a λ-abstraction, an application, and the let expression. An effect label eff is translated to a constant withthe same name.
10

More strictly speaking, our calculus is the one for stackful asymmetric coroutines
according to de Moura and Ierusalimschy’s classification.

One-shot Algebraic Effects as Coroutines

9x ∈ Variables
K ∈ {Eff , Resend , True, False}l ∈ Labels
eff ∈ Effects→
v ::= nil | eff | K −v ? | l | x | λx.e−→?
e ::= v | K e | l : e | e e | let x = e in e
| match e with cases| create e | resume he e | yield e i−−−−−−−−−→→→
letrec ::= let rec x −x = e and x −x = e? in e−−−−−−−−−−→
cases ::= pat [cond ] → e;cond ::= when x = x−→
pat ::= K pat ? | x
C ::=  | C e | v C | let x = C in e | let x = v in C→
| match C with cases | let rec f −x = e in C
| C = e | eff = C−−−−−−−−−→→→| let rec f −x = e and f −x = e? in C
| create C | resume C e | resume l C | yield C | l : C

Fig. 2: the syntax of λac

We translate perform to yield based on the following observation. In thecalculus for AEH, when an effect is invoked, the control is transferred to ahandler corresponding to the effect, while in the calculus for coroutines, whena yield is called, the control is transferred to its parent coroutine. Hence we
can emulate the behaviour of perform by yield. The translation wraps thearguments of perform with the tag Eff and translates them. This tag is used
to determine whether the effect has been yield ed from the handled expression
itself, or the effect has been resent (forwarded) by the handler. The handling
expression with h handle e is translated to a simple application as the handler
is mapped to a function.
The translation for a handler (the last case in Figure 3) is highly non trivial,
and we shall explain it using an example.
Consider the program M in λeff with the effects C1 , C2 , and C3 (Figure 4).
Here we assume that our calculus is extended to have natural numbers arithmetic operations. Then M is translated to the program in Figure 5 where somevariables and let-bindings are renamed or inlined for readability.

10

Satoru Kawahara and Yukiyoshi Kameyama

VxW = xVλx.eW = λx.VeW

Vv1 v2 W = (Vv1 W) (Vv2 W)

Vlet x = e in e0 W = let x = VeW in Ve0 W
Veff W = eff

Vperform eff vW = yield (Eff (Veff W) (VvW))

Vwith h handle eW = VhW (λ .VeW)

Vhandler eff (val x → ev ) ((x, k) → eeff )W =let eff = Veff W in

let vh = λx.Vev W in

let effh = λx k.Veeff W in
handler eff vh effh
where handler =let rec handler eff vh effh th =let co = create th inlet rec continue arg = handle (resume co arg)and rehandle k arg = handler eff continue effh (λ .k arg)and handle r =match r with
| Eff eff 0 v
when eff 0 = eff → effh v continue| Eff→ yield (Resend r continue)| Resend (Eff eff 0 v) k when eff 0 = eff → effh v (rehandle k)| Resend effv k→ yield (Resend effv (rehandle k))|→ vh rin continue nil
in handler

Fig. 3: Translation from λeff to λac

The term after translation contains the function handler defined in Figure 3, which works as follows: handler makes a thunk from (λ . · · · · · · ), defines
three functions continue, rehandle and handle, and then evaluates continue nil.
continue passes arg to co, resume-s it, and passes the return value to handle.
handle splits the process from the return value of resume according to the equivalence of tags and effect labels.
When continue is evaluated by passing nil , Eff C1 10 is yield-ed first in thehandled expression and caught by the innermost handler h1 . In this case, since it
has an Eff tag and h1 can handle C1 , the first pattern of handle matches it. effhOne-shot Algebraic Effects as Coroutines

M = let h1 = handler C1(val v → v) ((x, k) → kx) in
let h2 = handler C2(val v → v) ((x, k) → kx) in
let h3 = handler C3(val v → v) ((x, k) → kx) inwith h3 handle
with h2 handle
with h1 handle

11

VM W = let h1 = let vh 1 = λv. v inlet effh 1 = λx. λk. k v inhandler C1 vh 1 effh 1 inlet h2 = let vh 2 = λv. v inlet effh 2 = λx. λk. k v inhandler C2 vh 2 effh 2 inlet h3 = let vh 3 = λv. v inlet effh 3 = λx. λk. k v inhandler C3 vh 3 effh 3 inh3 (λ . h2 (λ . h1 (λ .

let a = perform (C1 10) in

let a = yield (Eff C1 10) in

let b = perform (C1 13) in

let a = yield (Eff C1 13) in

let c = perform (C3 17) in

let a = yield (Eff C3 17) in

a+b+c

a + b + c )))Fig. 4: Example program in λeff

Fig. 5: Example after translation

is applied to the effect’s argument 10 and a continuation. By passing continue
as the continuation, the computation of a handled expression can be resumed,which is suspended at the yielded position. And since continue passes the return
value of resume to handle, the effect can be handled by the same handler again.
So a is bound to 10. When Eff C1 13 is yielded in the continuation resumed by
the handler, it is processed by h1 again in the same way, and b is bound to 13.
When the effect C3 is invoked, h1 catches the effect first. h1 can’t handle C3 ,so the second pattern of handle matches. The effect is sent to a handler one stepoutside, and the effect is processed by that handler. As with invoking an effect,an effect is re-sent to an outside handler by using a yield. At this time, the tag
Resend wraps the effect and a continuation to indicate resending. Then, as in
the first pattern, pass continue as a continuation.
The resent C3 is captured at h2 . Since it has Resend tag and h2 can’t handle
C3 , the fourth pattern of handle matches. As in the second pattern, it uses yield
to re-send the effect to an outside handler. At this time, rehandle k is wrapped by
Resend tag as a continuation. rehandle is a function that creates a handler that
handles the thunk of the application of two given arguments. By setting continue
to the value handler, the computation of the current handling expression canbe resumed when the computation of the rehandle passed as a continuation isfinished. rehandle has another role which adjusts the layers of the coroutines.
In the second clause of handle, handle calls yield , so control is exited from one
coroutine. In the third and fourth clauses, we could write λarg.handle (karg)

12Satoru Kawahara and Yukiyoshi Kameyama

instead of rehandle k, if only to manipulate the return value of the continuation.
In this case, the layers of the coroutines would decrease, and eventually, we would
get an error calling yield outside of coroutine. Therefore rehandle encapsulates
the expression with coroutine internally and avoid to decreasing the layer ofcoroutines.
The effect resent again is captured by h3 . It has Resend tag and h3 canhandle C3 , so the third pattern of handle matches. Same to the fourth pattern,rehandle k is passed to effh as a continuation. Then it returns 17 to the handledexpression, and c is bound to 17.
The handled expression results in 40. Then h1 receives it, and the fifth wildcard pattern of handle matches the untagged value, and the value is passed to
the value handler. Same to the h1 , h2 and h3 receive the value and pass to thevalue handler. Finally the entire expression returns 40.
Although our translation looks complicated, we emphasize that our translation is compositional and local, syntax-directed, and does not rely on higherorder stores or other fancy features, but need only basic functionality of asymmetric coroutines. With this simplicity, several programmers have already ported
our translation to other languages than Ruby and Lua.
3.4

Macro-expressible Translation

We claim that the translation from λeff to λac in the previous section is simple
and efficient. To support the former claim, this subsection shows that it is amacro-expressible translation in the sense of Felleisen. The latter claim will be
discusses in the subsequent section.
Felleisen studied the notion of macro expressivity, which is a more finegrained notion than most others to measure the expressive power of language
primitives [8]. For instance, call /cc (call-with-current-continuation) can be translated away by a CPS translation to a pure lambda calculus, yet, it is not macroexpressible in pure lambda calculus since the translation is global. On the other
hand, a simple let expression let x = e1 in e2 can be locally translated by(λx.e2 ) e1 , therefore, it is macro-expressible in the pure lambda calculus.
While Felleisen defined the notion for the setting where a language L1 is aproper extension of another language L2 , we want to compare the expressive
power of two languages L1 and L2 where L1 and L2 are extensions of a common
language L0 . To deal with this setting, we use Forster et al.’s definition for themacro-expressible translation [10], and we give its slightly simplified version here.
Definition 1 (Macro-expressible translation). Let L0 be a language, andL1 and L2 , resp., be the language L0 augmented with a set of primitives X1 , · · · , Xn
and Y1 , · · · , Ym , resp. A translation φ from L1 to L2 is macro-expressible translation if and only if all of the following conditions hold.
– φ is homomorphic for the primitives in L0 . For instance, if a binary infix
operator ⊕ is in L0 , then φ (e1 ⊕ e2 ) is φ (e1 ) ⊕ φ (e2 ).

One-shot Algebraic Effects as Coroutines

13– φ maps each Xi of arity n to a syntactic expression Mi in L2 which has nfree variables x1 , · · · , xn such that the following holds:
φ (Xi (e1 , · · · , en )) = Mi [φ (e1 ) /x1 , · · · , φ (en ) /xn ]The expression in the right-hand side represents simultaneous substitution
for the variables x1 , · · · , xn in Mi .
To state the above definition we have made two simplifications. First, theequality in this definition should be, in general, semantic equality where weassume that each language is equipped with a certain semantics, but in thispaper, we can regard it as syntactic equality. Second, we do not consider thecase when Xi works as a binder such as the let expression11 , but we do notneed to consider such cases.
It is easy to show that our translation in the previous subsection conforms
the conditions for a macro-expressible translation.
Theorem 1. Our translation in Figure 3 is a macro-expressible translation.
Proof sketch. It is easy to check that our translation V·W is homomorphic for thevariable, lambda abstraction, application, let, the effect expression.
For the primitives of algebraic effects and handlers, we need to check eachcase. For the primitive perform, let M be yield (Eff x1 x2 ), then we have
Vperform e1 e2 W = M [Ve1 W/x1 , Ve2 W/x2 ], and we are done. Other cases are
similar. (end of proof sketch)
As we wrote above, a macro-expressible translation is rather discriminating,or sensitive to small differences between language primitives. Only local translations are macro-expressible translation. Since global translations such as a CPS
translation and a state-passing translation do not qualify as macro-expressible
one, state and first-class continuations are not macro-expressible in pure lambda
calculus.
Put differently, if we have a macro-expressible translation for a primitive X ina language L0 , then we can implement X using the translation without changing
any other primitives in L0 This is a simple, but rather important property for
our work, as it is a necessary condition to implement X as a simple library in
L0 , unless we have an access to language’s run-time, or reification is allowed.

4

Implementation

We have implemented AEH in Lua and Ruby based on the translation in Section 3. Since the translation is macro-expressible, we can realize our implementation as a simple library. Our implementations are compact. The Lua library isimplemented in 160 lines and the core of the Ruby library is in 340 lines, even
including comments for documentation generation. All our code is available via
Github.
Several issues have arisen in the process of implementation we will address
below.
11

Felleisen considers the case where each argument may be bound by the construct.

14

Satoru Kawahara and Yukiyoshi Kameyama

Multiple Effect Handlers Our calculus λeff has the restriction that a handler
can catch only one effect. However, this restriction is only for the presentation
purpose, and in our actual implementation, one handler may catch multiple
effects, All examples including the examples in this paper that use multiple
effects per handler run without problems using our library. We also note that
there is no critical performance downgrade of having multiple effects per handler.
Dynamic Effect Creation In the language λeff , we have no way to create new
effect labels dynamically. Again this is due to simplicity, and we have eliminatedthis restriction in our implementation. The merit of allowing dynamic creation ofeffect instances is that a certain kind of effectful programs needs the uniquenessof effect instances, for instance, higher-order effects[16].
Conflict with Other Effects An assumption on our translation is that all effects
are written via AEH. If our source program uses other effects besides AEH, it
will cause a serious problem, since other effects may interfere with the internallyused coroutines. For instance, if we use our library in Lua, and simultaneously
use Lua’s native coroutine directly, yielding a value in the source program may
be accidentally caught by an internal coroutine. As consequence we must not
use native coroutines with (our implementation of) AEH.
This problem can be solved as follows, thanks to the expressivity of AEH.
See the following code.
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23

local Yield = inst()
local yield = function(v)return perform(Yield, v)
end
local create = function(f)return { it = f, handled = false }end
local resume = function(co, v)
if co.handled thenreturn co.it(v)elseco.handled = true
return handler({val = function(x) return x end,
[Yield] = function(u, k)co.it = kreturn u
end})(function() return co.it(v) end)
end

One-shot Algebraic Effects as Coroutines
24

15

end
The code above is an implementation of asymmetric coroutines by algebraic
effects and handlers in Lua. The function yield should throw a value to resume, so yield should be an effect invocation and resume should be a handler. This
correspondence is the inverse of the translation in Figure 3. So we define Yield
effect (line 1) and yield function (line 3) as a wrapper for the invocation of
the effect. The function create (line 7) creates a reference cell by a table. We
represent a coroutine as a reference cell, which is initialized to the function f andthe flag handled explained later. The handler resume (line 11) catches Yield
effect with an argument and a continuation. This continuation is the rest ofcomputation of the coroutine, so the handler stores the continuation to the celland returns the value u (line 19 and 20). Since we provide a deep handler, it is
not necessary to set the handler multiple times. The tag handled is to assert
if the function is handled by the handler or not (line 12). The function resume
checks the flag; if the flag is off, resume turns on the flag and runs the function
with the handler. Otherwise, resume runs the function only.
Although we believe that the above technique may be used in other computation effects, it is left for future work to combine them with algebraic effect andhandlers without big downgrade of performance.

5

Evaluation

We have conducted experiments on microbenchmark using our library in Lua,and implementation in Lua based on free monads [23], and compare their performance. All the code for the benchmark is publicly available in the GitHub
repository12 . In the following figures, the symbol N represents the result of ourlibrary, and  does of the free-monad based implementation. One of the benchmarks compares to native coroutines of Lua and indicates the result as the
symbol ? in a graph. The experiments have been conducted on the environmentin Table 1.

Table 1: Environment for Benchmark
Arch LinuxOSCPUIntel Core i7-8565U
Main memory
16GB DDR4
Lua processor
LuaJIT 2.05

Figure 6 is the result of the benchmark for emulating a state monad. The
benchmark uses the function count, cited from [14], adjusted for our library andfree monad, and recursively runs a simple computation consisting of one-layer
12

https://github.com/nymphium/effs-benchmark

16Satoru Kawahara and Yukiyoshi Kameyama
2time(sec)

1.5
param (105 ×)
1
2
3
4
5
free 0.3560 0.7199 1.1741 1.5449 2.0303
ours 0.0273 0.0521 0.0939 0.1811 0.2090

1
0.5
2

3

4
5
param ·105

Fig. 6: Result of onestate benchmark

one-effect handlers for the number of times as the input parameter. The resultshows that our library is approx. 10 times faster than the free-monad based
implementation for this simple case. The reason why free monads are rather
slow is that the bind operator requires a continuation as the next action, but
the cost for creating function closures is rather high for imperative languages
such as Lua. Also, functional languages such as Haskell may offer optimization
for free monads, while the benchmark uses naive implementation. Nevertheless,the results are encouraging for our embedding.
In the next experiments in Figure 7, the benchmark program iterates countfunction 3,000 times in deeply nested handlers. The parameter in the tabletime(sec)
0.4
param (10×)
1
2
3
4
5
free 0.0174 0.0303 0.0508 0.1374 0.1594
ours 0.0572 0.1722 0.3181 0.4064 0.5041

0.2

20

30

40
param

50

Fig. 7: Result of multistate benchmark

corresponds to the number of nested handlers/coroutines, hence 50 (the rightmost column) is already a rather unrealistic situation, but we included thisexperiment as an extreme. As expected, our library runs three times slower than
the free monad does for this case. The reason is that rehandle creates a new
coroutine, which is called every time an effect is caught from the other handler
shown in Figure 3, so it degrades the performance.
In the next experiment, the function looper performs algebraic effects in theiteration of the for loop, where the number of iteration is given as a parameterOne-shot Algebraic Effects as Coroutines

17

shown in the table of Figure 8. The benchmark program invokes an effect in atime(sec)
0.8
0.6

param (105 ×)
1
2
3
4
5
free 0.1650 0.3455 0.5304 0.7204 0.9319
ours 0.0215 0.0416 0.0630 0.0844 0.1064

0.4
0.2
2

3

4
5
param ·105

Fig. 8: Result of looper benchmark

for-loop and sets a handler out of the loop to catch the effect. Our library runs
9 times as fast as the free-monad based implementation. Note that free monads
need the forM-operator which has large overhead. Again an advanced compiler
may be able to eliminate all or part of this overhead.
Figure 9 shows the result of the benchmark, which solves the same-fringe
problem [11] by using algebraic effects and coroutines. The problem is to deter-time(sec)
0.4

param (104 ×)
1
2
3
4
5
free 0.0507 0.1837 0.3522 0.4761 0.5886
ours 0.0067 0.0127 0.0186 0.0252 0.0296
coroutines 0.0042 0.0082 0.0119 0.0158 0.0190

0.2

2

3

4
5
param ·104

Fig. 9: Result of same_fringe benchmark

mine whether given two trees have the same “fringe”, an enumeration of leavesof the tree in a certain order. The benchmark is given the number of leaves asa parameter. We implement coroutines to solve it, by algebraic effects with freemonad, and our library, described in Section 4. We also implement the solver
with native coroutines of Lua. Our library yields 18 times performance gain
compared to the free-monad method. Remarkably, our library is only 1.6 times
slower than native coroutines.
In summary, our way of implementing AEH is advantageous in several programming languages from the performance viewpoint. We also emphasize that

18

Satoru Kawahara and Yukiyoshi Kameyama

writing effectful programs using coroutines is harder than writing the same programs using AEH, which provide high-level abstraction.

6

Related Work and Discussion

In this section, we discuss closely related work which has not been mentioned inthis paper and picks up a few important issues for discussion.
Shallow Handler We have shown the embedding with deep handlers, which cancatch the effect invocation even during the execution of the continuation.
In the literature, there has been a discussion on deep vs shallow handlers [12],and it has its own merits. We have also implemented the shallow handler withcoroutines shown in Figure 10. The idea is simple; after a handler catches an

Vhandler† eff (val x → ev ) ((x, k) → eeff )W =let eff = Veff W in

let vh = λx.Vev W in

let effh = λx k.Veeff W in
handler † eff vh effh
where handler † =let rec handler eff vh effh th =let co = create th inlet rec continue arg = handle (resume co arg)and rehandle k arg = handler eff continue effh (λ .k arg)and continue 0 = resume coand rehandle 0 k = resume (create k)
and handle r =match r with
| Eff eff 0 v
when eff 0 = eff → effh v continue 0| Eff→ yield (Resend r continue)| Resend (Eff eff 0 v) k when eff 0 = eff → effh v (rehandle k)| Resend effv k→ yield (Resend effv (rehandle 0 k))|→ vh rin continue nil
in handler

Fig. 10: translation from shallow handlers to coroutines

One-shot Algebraic Effects as Coroutines

19

effect, it always resends any effects to the outer handler. We have explained
the role of rehandle in Figure 3 that it encapsulates the continuation with acoroutine to adjust the layer of coroutines, and rehandles the effect invocationin the continuation. In the shallow setting, it is also necessary to reset the numberof the layer of coroutines, which might degrade the performance. On the other
hand, rehandling is not needed because it is shallow.
One-shot Continuations It should be noted that we are not the first to study
the one-shot variant of control operators. Bruggeman et al. give an one-shotcontrol operator call/1cc with the observation that almost continuations are run
at most once [5]. When a compiler knows a continuation can be run at most once,
it can generate more sophisticated code. They state that, by replacing call/cc
using continuations at most once for call/1cc, program can be run with lessmemory consumption and higher performance. Berdine et al demonstrate thatmany control abstractions can be translated into typed CPS including one-shotcontinuations, with linear-types [2].
James and Sabry stated that the yield operator for generator, which is a
restricted variant of coroutines and can be found in various languages, is oneshot delimited continuations [13]. They also defined a generalized yield operator
which has multi-shot continuations and show the connection between it and thedelimited-control operators.
Multicore OCaml is a dialect of OCaml which natively supports algebraic
effects by runtime stack manipulation. Its motivation is to write concurrent
programming in direct-style[7]. They provide one-shot continuations due to theperformance problem, and if multi-shot continuations are needed, they allow
explicit copy for continuations.
Free monad We have already compared our with with free-monad based implementations of algebraic effects. On the positive side, it gives a systematicand elegant implementation for various effects. Its downside is it has significant
overhead in performance. We also point out that our embedding-based implementation does not interfere with surface languages, while free-monad based
implementations force a programmer to use monadic style, which is good forsome programmers, but is not for others. With our implementation, the surface
language with algebraic effects and handlers can be presented in direct style ormonadic style.

7

Conclusion

We have presented a novel embedding technique for algebraic effects and handlers
into asymmetric coroutines, and shown translation from the former to the latter as simple, direct, syntax-directed compositional translation. Compared withother embeddings or other ways, our technique can apply to many languages
which have coroutines due to the simplistic nature of our embedding. We havedemonstrated the applicability of our embedding by implementing the libraries

20

Satoru Kawahara and Yukiyoshi Kameyama

in Lua and Ruby. Our technique seems to be attractive for other researchers,
and some of them have implemented our translation for other languages such
as JavaScript and Rust. We expect that the simplicity of our implementation isadvantageous to be used by more people, more languages, and more applications.
The key of our development is the one-shotness restriction of continuations.
Our embedding uses the rest of the coroutine thread as a continuation, and thestatus of the coroutine cannot be copied, so the limitation exists that a continuation can be executed at most once. One-shotness is a dynamic property,
and its static approximation, linearly used (delimited) continuations, or linear
continuation-passing style, are the target of active research in the past. We hopethat the formal foundation of this paper’s result is studied more deeply, andcoroutines and their connection with other control operators find a solid theoretical foundation.
We briefly state future work. There are many directions to extend our work.
Of particular interest is to prove the semantics preservation of our translation.
Introducing an appropriate type system is also an interesting next step. Anotherexciting issue is to relate and compare various control abstractions in the literature and in the practical programming languages. For instance, React, a popular
web framework for JavaScript, has a utility software Hooks13 , which allows programmers to build components with side-effects modularly. Abramov pointed
out the relevance between Hooks and algebraic effects in his blog post14 , and we
think that investigating this relationship based on our work is promising.

References
1. Bauer, A., Pretnar, M.: Programming with Algebraic Effects and Handlers. Journalof Logical and Algebraic Methods in Programming 84, (03 2012)
2. Berdine, J., O’Hearn, P., Reddy, U., Thielecke, H.: Linear Continuation-Passing.
Higher-Order and Symbolic Computation 15, 181–208 (09 2002)
3. Brachthäuser, J., Schuster, P.: Effekt: extensible algebraic effects in Scala (shortpaper). pp. 67–72 (10 2017)
4. Brachthäuser, J., Schuster, P., Ostermann, K.: Effect handlers for the masses.
Proceedings of the ACM on Programming Languages 2, 1–27 (10 2018)
5. Bruggeman, C., Waddell, O., Dybvig, R.: Representing Control in the Presence of
One-Shot Continuations. vol. 31, p. (02 1970)
6. Danvy, O., Filinski, A.: Abstracting control. In: Proceedings of the 1990 ACM
Conference on LISP and Functional Programming. p. 151–160 (1990)
7. Dolan, S., White, L., Madhavapeddy, A.: Multicore OCaml. In: OCaml Users andDevelopers Workshop (2014)
8. Felleisen, M.: On the Expressive Power of Programming Languages. In: Selected
Papers from the Symposium on 3rd European Symposium on Programming. p.
35–75. ESOP ’90, Elsevier North-Holland, Inc., USA (1991)
9. Felleisen, Matthias and Daniel P. Friedman: Control operators, the SECD-machine,
and the λ-calculus. In: Formal Description of Programming Concepts (1987)1314

https://reactjs.org/docs/hooks-reference.html
https://overreacted.io/algebraic-effects-for-the-rest-of-us/

One-shot Algebraic Effects as Coroutines

21

10. Forster, Y., Kammar, O., Lindley, S., Pretnar, M.: On the expressive power of userdefined effects: Effect handlers, monadic reflection, delimited control. J. Funct.
Program. 29, e15 (2019). https://doi.org/10.1017/S0956796819000121, https://doi.org/10.1017/S0956796819000121
11. Gabriel, R.P.: The Design of Parallel Programming Languages, p. 91–108. Academic Press Professional, Inc., USA (1991)
12. Hillerström, D., Lindley, S.: Shallow Effect Handlers. In: Asian Symposium on
Programming Languages and Systems. pp. 415–435. Springer (2018)13. James, R., Sabry, A.: Yield: Mainstream Delimited Continuations. p. (01 2011)
14. Kammar, O., Lindley, S., Oury, N.: Handlers in Action. vol. 48, pp. 145–158 (092013)
15. Kiselyov, O., Ishii, H.: Freer Monads, More Extensible Effects. ACM SIGPLAN
Notices 50, (03 2015)
16. Kiselyov, O., Sivaramakrishnan, K.: Eff Directly in OCaml. Electronic Proceedingsin Theoretical Computer Science 285, 23–58 (12 2018)
17. Leijen, D.: Algebraic Effects for Functional Programming. Tech. rep., Technical
Report. 15 pages. (2016)
18. Leijen, D.: Implementing Algebraic Effects in C. pp. 339–363 (11 2017)19. Materzok, M., Biernacki, D.: Subtyping delimited continuations. In:
Chakravarty, M.M.T., Hu, Z., Danvy, O. (eds.) Proceeding of the 16th
ACM SIGPLAN international conference on Functional Programming,
ICFP 2011, Tokyo, Japan, September 19-21, 2011. pp. 81–93. ACM (2011).
https://doi.org/10.1145/2034773.2034786,
https://doi.org/10.1145/2034773.
2034786
20. Moura, A.d., Ierusalimschy, R.: Revisiting Coroutines. ACM Transactions on Programming Languages and Systems 31, (07 2004)
21. Plotkin, G., Power, J.: Algebraic Operations and Generic Effects. Applied Categorical Structures 11, 69–94 (02 2003)
22. Plotkin, G., Pretnar, M.: Handling Algebraic Effects. Logical Methods in Computer
Science 9, (12 2013)
23. Pretnar, M., Saleh, A.H., Faes, A., Schrijvers, T.: Efficient compilation of algebraic
effects and handlers. CW Reports, volume CW708 32 (2017)

A

Semantics of λeff

A.1

Helper functions

We introduce three helper functions for semantics in Figure 11:22

Satoru Kawahara and Yukiyoshi Kameyama

split



 

(with w handle )eff :: K , eff = [] , (with w handle )eff , Ksplit ((F :: K) , eff ) = F :: K 0 , F 0 , K 00
where F 6= (with w handle )effand K 0 , F 0 , K 00 = split (K, eff )LF :: KM = λx. LKM F [x]
L [] M = λx. x

K ∗ E = clos (λx.LKM x, E)

Fig. 11: Helper Functions for Semantics

split (K, eff ) returns a triple (K1 , F, K2 ) where F is the frame that handles theeffect named by eff, and K = K1 :: [F ] :: K2 holds. If more than one frame canhandle the effect eff, the first one is selected, and if none have the named effect,
the result is undefined. LKM converts a stack K to a continuation in functional
form. (K ∗ E) creates a closure with a stack frame K and an environment E.

A.2

Small-step semantics

Figure 12 defines the small-step, call-by-value, left-to-right semantics (−→eff ) in
the CEK-machine style [9].
In the rule Lookup, E (x) is the value associated with the variable x in theenvironment E. The rules PushLet, Bind, and Close, PushApp, PushArg,
and App are standard. The rest of the rules are the one for algebraic effects andhandlers. The rules PushWithHandle and CloseHandler push or pop evaluation contexts to the stack. The rule Handle manipulates a with-expression
with h handle e: if h evaluates to a handler value, then e is going to be evaluatedunder this handler. The rule PushPerform pushes the frame of perform-ing
an effect eff to the stack. The rules HandlePerform and HandleValue are
the key rules for algebraic handlers. In the rule HandlePerform, the code
component is a value w. Hence, the first frame in the stack perform eff  isretrieved and evaluated. Then we look for a handler whose name is eff in thestack K, and if we find it, we use the handler to cope with this effect whereformal parameters y and k are bound to the value w and the delimited continuation K 0 under environment E. We adopt the deep handlers, hence the handlereff(with wh handle )
remains in the stack after this step. The rule HandleValue is used when the handled expression does not invoke an effect andreturns a value w. Then the value handler (val x → ev ) is used, and the handler
is eliminated from the stack after this step.

One-shot Algebraic Effects as Coroutines

B

23

Semantics of λac

Auxiliary functions Figure 13 defines two auxiliary functions for pattern matching of λac . FV p (pat) is the set of free variables in pat. matchable (v, pat) is apredicate to assert that,given a value v and a pattern pat, the value matches thepattern. The operator ⊕ concatenates two stores and ∅ is an empty store. The
function genstore creates a new store which consists of pairs of a variable anda value (which consists of constructors). For example, by calling genstore withthe arguments Resend (Eff w v) u (for some values w, v and u), and a nested
pattern Resend (Eff y x) k, we get a new store ∅ [y ← w , x ← v, k ← u].
Small-step Semantics Figure 14 shows the operational semantics of λac by thetransition (−→ac ) of the state he, θi, an expression e and a store θ. dom (θ) is
the domain of θ, and θ (x) is a value associated with the variable x. Note thateven if θ (l) = nil, we include l in dom (θ). In those cases such as introducing avariable or a label (App, Let, LetRec, Create, Match, and MatchWhen),
we identify α-equivalent terms and assume that we rename bound variables
appropriately for substitution to be defined at any time. The distinctive pattern
is similar to a variable but generates no binding after pattern matching, so weallow to be overwritten. The rules contain those for variable lookup (Lookup),
function application (App), let, and let rec (Let and LetRec). The function
Create is to make a new coroutine. It creates a fresh label l, binds the coroutine
to l, and returns its label to the context C. The function Resume produces alabelled expression, an application θ (l) v with a label l. θ (l) v is what finds
the body corresponding to the label l from θ and apply v. The created labelled
expression l : θ (l) v expresses the computation in the coroutine labelled byl. To prevent the rest of the coroutine from being referred, the rule Resume
invalidates the associatedvalue by setting it to nil. The function Yield suspends the current computation of a coroutine and returns to the parent coroutine with an argument.
Since the target calculus represents asymmetric coroutines, a coroutine can bea parent of another coroutine by resuming it. The rule have an assumption that
C2 does not have any labelled expresses. The assumption indicates that C2 isthe innermost active coroutine. The function LabelledReturn transfers theresult of the computation v in the coroutine l to its caller. The functions EqTand EqF compare two effect operations. The operator =eff judges whether two
given effects are the same. The functions Match and MatchWhen are for−pattern-matching. The second rule applies when K →v matches a pattern, andthe match case has a guard c. This rule transforms the guard to another match
expression, with assigning the values to the corresponding variables in the pattern. The assignment may affect pattern variables in the guard c. If a guard
returns True, pattern matching is successful, and the body of the True clause isevaluated; otherwise, we go to match against the rest of the patterns.

24

Satoru Kawahara and Yukiyoshi Kameyama

hC; E; Ki −→eff hC 0 ; E 0 ; K 0 ihx; E; Ki −→eff hE (x) ; E; Ki(Lookup)hlet x = e in e0 ; E; Ki −→eff he; E; (let x =  in e0 , E) :: Ki (PushLet)
hw; E; (let x =  in e, E 0 ) :: Ki −→eff he; (x = w) :: E 0 ; Ki

(Bind)

hλx. e; E; Ki −→eff hclos (λx.e, E) ; E; Ki(Close)he e0 ; E; Ki −→eff he; E; ( e0 , E) :: Ki(PushApp)hw; E; ( e, E 0 ) :: Ki −→eff he; E 0 ; (w ) :: Ki(PushArg)

w; E; clos (λx.e, E)0  :: K −→eff he; (x = w) :: E 0 ; Ki

(App)hwith h handle e; E; Ki −→eff hh; E; (with  handle e, E) :: Ki(PushWithHandle)
hh; E; Ki −→eff hclosh (h, E) ; E; Ki(CloseHandler)
where h = handler eff (val x → ev ) ((x, k) → eeff )
*

+
*
+
e;
wh ;
0
E;
E;
−→eff (with  handle e, E) :: K
(with wh handle )eff :: K
where wh = closh (handler eff (val x → ev ) ((x, k) → eeff ) , E)
(Handle)hperform eff v; E; Ki −→eff hv; E; (perform eff ) :: Ki (PushPerform)
split (K, eff ) = K 0 , (with wh handle )eff , K 00
where wh = closh (handler eff (val x → ev ) ((y, k) → eeff ) , E 0 )
*
+
e ;
eff

hw; E; (perform eff ) :: Ki −→eff(y = w) :: (k = K 0 ∗ E) :: E 0 ;(with wh handle )eff :: K 00
(HandlePerform)

F = (with wh handle )eff
where wh = closh (handler eff (val x → ev ) ((y, k) → eeff ) , E 0 )hw; E; F :: Ki −→eff hev ; (x = w) :: E 0 ; Ki
(HandleValue)

Fig. 12: Semantics of λeff

One-shot Algebraic Effects as Coroutines

 −→ [−→
FV p K pat =p ∈ pat.FV p (p)FV p (x) = {x}

−→
−→
→
→
v , p ∈ pat.matchable (v, p)
matchable K −v , K 0 pat = K =K K 0 ∧ ∀v ∈ −θ1 ⊕ θ2 = ∅−→→genstore K −v , K pat =∀x ∈ dom (θ1 ) .x ← θ1 (x) ,∀y ∈ dom (θ2 ) .y ← θ2 (y)Mgenstore (v, p)

−
→
−
v∈→
v ,p∈pat

genstore (v, x) = ∅ [x ← v]

Fig. 13: Auxiliary functions for the semantics of λac

25

26

Satoru Kawahara and Yukiyoshi Kameyama

hC[x], θi −→ac hC[θ(x)], θi(Lookup)x∈/ dom (θ)(App)

hC [(λx.e) v] , θi −→ac hC [e] , θ [x ← v]ix∈/ dom (θ)(Let)
hC[let x = v in e0 ], θi −→ac hC[e], θ[x ← v]i
n
o
−−→
→
→
∀z ∈ f, −x , g, −y .z ∈/ dom (θ)
 +→#+ (LetRec)*"*  let rec f −x = ef→f ← λ−
x .ef ,
−
−
−
−
−
−
−
−
−
→
→
 , θ −→ac C[e], θ −−−−−−−→C  and g −y = eg→g ← λ−
y .eg
in e
l∈
/ dom (θ)(Create)hC [create v] , θi −→ac hC [l] , θ [l ← v]i
hC [resume l v] , θi −→ac hC [l : θ (l) v] , θ [l ← nil]iC2 does not contains labelled expressions
hC1 [l : C2 [yield v]] , θi −→ac hC1 [v] , θ [l ← λx.C2 [x]]ihC [l : v] , θi −→ac hC [v] , θieff =eff eff(Resume)(Yield)(LabelledReturn)0hC [eff = eff 0 ] , θi −→ac hC [True] , θieff 6=eff eff 0
hC [eff = eff 0 ] , θi −→ac hC [False] , θi

(EqT)

(EqF)

→
¬matchable (K −v , pat) +*  match K −→v with→C  pat [cond ] → e;  , θ −→ac hC [match K −v with cases] , θi
cases
(MatchNext)−→∀x ∈ FV p (pat) .x ∈/ dom (θ)
matchable (K v , pat)→
θ0 = θ ⊕ genstore (K −v , pat)(Match)−→hC [match K v with pat → e; cases] , θi −→ac hC[e], θ0 i→
∀x ∈ FV p (pat) .x ∈/ dom (θ)
matchable (K −v , pat)−→0θ = θ ⊕ genstore (K v , pat)match c with +*  match K −*→ True → e; +v with 0,θC  pat when c → e;  , θ −→ac C  False →

−
→

cases
match K v with 
cases(MatchWhen)Fig. 14: Semantics of λac