1One-shot Algebraic Effects as Coroutines?

2

Satoru Kawahara1,2?? and Yukiyoshi Kameyama1,3
1

3
4
5

Abstract. [Kwhr: fix 32] This paper presents a translation from algebraic
effects and handlers to asymmetric coroutines, which provides simple,
portable and widely 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 partof compilers, interpreters, or as libraries. We present a direct embeddingof one-shot algebraic effects and handlers in a language which has asymmetric coroutines. The key observation is that, by restricting the use ofcontinuations 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 we have implemented it embedding as a library in Lua and Ruby,
which allows one to write effectful programs in a modular way using
algebraic effects and handlers.

6
7
8
9
10
11
12
13
14
15
16
17
18
19
20

Keywords: Algebraic Effects and Handlers · Coroutines · Continuations· Control Operators · Macro Expressibility

21
22

23

24
25
26
27
28
29
30
31
32
33
34
35

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

1

Introduction

Algebraic effects [21] and handlers [22] (AEH for short) are an emerging new feature to model effectful computations in a modular way. They are gaining more
and more attention not only from researchers but also from practitioners. [Kwhr:
fix 1] 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 in many other main-stream programming languages, which is a big obstacle to utilize theoretical results on AEH in real-world software. We, therefore,
think that it is an important and timely issue to develop a systematic implementation method for AEH which is available in many existing programming
languages.
?
??

Research Paper
Student

2
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37

38
39

Satoru Kawahara and Yukiyoshi Kameyama

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; [Kwhr: fix 5 and 34] The implementation
method based on stack manipulation is used for JVM bytecode and C [4,18],
however, [Kwhr: fix 6 and 7] an implementer needs deep insight on its internal
structure. It then follows that the implementation cost is rather high, which
prevents the feature from being implemented in various language systems. [Kwhr:
fix 5 and 34] 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 havedelimited-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 that it 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 andportable, compared to the existing implementations. The key of our method is
to use coroutines to embed them in programming languages. Today we see anumber 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 generaldelimited-control operators, [Kwhr: fix 2] 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, [Kwhr: fix 31] thanks to the fact that no copying of continuations is necessary [5]. [Kwhr: fix I rewrote the following paragraph completely.] Hence, we face the tradeoff 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.
– [Kwhr: fix 12] We show an embedding of one-shot algebraic effects and handlers.
We use standard asymmetric coroutines only, and no special control features
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 [Kwhr: fix 25] Since Rust does nothave coroutines, Future is used instead.
5

One-shot Algebraic Effects as Coroutines
1
2
3
4
5
6
7
8
9
10
11

3

are needed. Hence our embedding is applicable to various languages as longas they have asymmetric coroutines.
– [Kwhr: fix 13] Comparing to the embedding based on free monads, our method
does not force 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, whichis available on GitHub. [Kwhr: fix 33] Algebraic effects and handlers is a complex system, and the implementation can be therefore error-prone. So ourformalized implementation is desirable.

21

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 [Kwhr: fix 39] translation from λeff , a language with algebraic effect handlers, to λac , a language with asymmetric coroutines. We also show that our translation is macro expressible in the sense ofFelleisen. Section 4 discusses the extension of our model definitions for implementing our libraries in Lua and Ruby, and problems in actual use. Section 5shows the performance evaluation of our embedding by comparing ours with theembedding based on free monads. Section 6 describes related work, and Section 7
concludes.

22

2

12
13
14
15
16
17
18
19
20

Examples of one-shot algebraic effects

25This 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.

26

2.1

23
24

Exception

30

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()

31

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
end

27
28
29

4

Satoru Kawahara and Yukiyoshi Kameyama

6This 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 [Kwhr: fix 30] DivideByZero, which means that aneffect is raised and the control of the program is brought to the nearest effecthandler (which is not shown in the above code) similarly to exception handling.
Our library provides the function handler to create a new effect handler.

1
2
3
4
5
6

local with_nil = handler {val = function(_) return nil end,
[DivideByZero] = function(_, _)return nil
end
}

1
2
3
4
5

21

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
}

7
8
9
10
11
12
13
14
15
16
17
18
19
20

22
23
24

1
2
3

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.
with_default_zero(function()
local v = div(3, 0)
return v + 20
8https://www.lua.org/manual/5.3/manual.html#3.4.9

One-shot Algebraic Effects as Coroutines
4

5

end)

9

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 [Kwhr: fix 30] with_default_zero, but we omit it here
since there 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; returnv + 20. The net effect is the same as the case when div(3,0) returns 0, andthe entire computation results in 0 + 20 = 20.

10

2.2

1
2
3
4
5
6
7
8

State

14

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()

11
12
13

15

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

We then define the function run to execute stateful computations.
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,
the value handler returns a function which ignores its argument (for state). In6

Satoru Kawahara and Yukiyoshi Kameyama

12

the stateful computation, [Kwhr: fix 43] when the effect Get is invoked, then thehandler 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 effectPut with an parameter s is invoked, the handler returns a thunk in which ameaningless value () 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).
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.

13

2.3

1
2
3
4
5
6
7
8
9
10
11

Expressing other Computational Effects

19

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.

20

3

14
15
16
17
18

Embedding Algebraic Effects with Coroutines

24

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.

25

3.1

21
22
23

26
27
28
29
30
31
32
33
34
35
36
37

λ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
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

1
2
3
4
5

6
7
8
9
10
11

12
13
14
15
16
17
18
19
20
21
22

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(clos (λx.e, E)) and handlers (closh (h, E)) where E is a runtime enviroment,and [Kwhr: fix 47] F represents a frame, or a singular context, which means a’one-step’ fragment of a continuation. A (delimited) continuation K is a list offrames.
[Kwhr: fix 45] The call-by-value operational semantics of λeff is defined in the
CEK-machine style [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 avalue handler and an effect handler, and associates the effect label eff to it. The
expression with h handle e (which is called a handling expression) evaluates theexpression e under the handler h. The expression perform eff v invokes the effecteff 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 the handled expression is evaluated to a value, thevalue handler is used.

8
1

2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40

Satoru Kawahara and Yukiyoshi Kameyama

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.
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.
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

1

3.3

Translation from λeff to λac

2

We present a program translation from λeff to λac , which is syntax-directed and3[Kwhr: fix 30] compositional. The whole translation is defined in Figure 3 where a

4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21

λeff -term e is 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.
We translate perform to yield based on the following observation. In thecalculus for AEH, when an effect is invoked, the control is transferred to a handler
corresponding to the effect, while in the calculus for coroutines, when a yield iscalled, the control is transferred to its parent coroutine. Hence we can emulate
the behaviour of perform by yield. The translation wraps the arguments ofperform with the tag Eff and translates them. [Kwhr: fix 50] This tag is used todetermine 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 arith-

10
1
2

Satoru Kawahara and Yukiyoshi Kameyama

metic operations. Then M is translated to the program in Figure 5 where somevariables and let-bindings are renamed or inlined for readability.

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

3
4
5
6

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.

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

2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22

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

1

11Fig. 5: Example after translation

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
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

12Satoru Kawahara and Yukiyoshi Kameyama

23

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)
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.

24

3.4

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22

25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40

41
42

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

One-shot Algebraic Effects as Coroutines
1
2
3
4
5
6

13

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 ).
– φ 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 .

7
8

16

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.

17

Theorem 1. Our translation in Figure 3 is a macro-expressible translation.

9
10
11
12
13
14
15

34

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.

35

4

18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33

36
37
38

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. [Kwhr: fix 31] Our implementations are compact. The
11

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

14
1
2
3
4
5

6
7
8
9
10
11

12
13
14
15
16

17
18
19
20
21
22
23
24
25

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

Satoru Kawahara and Yukiyoshi Kameyama

Lua library is implemented in 160 lines and the core of the Ruby library is in
340 lines, even including comments for documentation generation. All our codeis available via Github.
Several issues have arisen in the process of implementation we will address
below.
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.
[Kwhr: fix 22 and 23] This problem can be solved as follows, thanks to the expressivity of AEH. See the following code.
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,One-shot Algebraic Effects as Coroutines
18
19
20
21
22
23
24

15

[Yield] = function(u, k)co.it = kreturn u
end})(function() return co.it(v) end)
end
end

18

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.

19

5

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

20
21
22
23
24
25
26
27
28
29
30
31
32
33
34

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.
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
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
12

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

16Satoru Kawahara and Yukiyoshi Kameyama

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

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

1
2
3
4
5

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
6
7
8
9
10

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One-shot Algebraic Effects as Coroutines
1
2
3
4

17

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 parametershown 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
5
6
7
8
9
10

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. [Kwhr: fix 54] The problem

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
11
12
13
14
15
16

is to determine whether given two trees have the same “fringe”, an enumerationof leaves of the tree in a certain order. The benchmark is given the number ofleaves as a parameter. We implement coroutines to solve it, by algebraic effects
with free monad, and our library, described in Section 4. We also implement thesolver with native coroutines of Lua. Our library yields 18 times performance

18

Satoru Kawahara and Yukiyoshi Kameyama

6gain 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 thatwriting effectful programs using coroutines is harder than writing the same programs using AEH, which provide high-level abstraction.

7

6

1
2
3
4
5

8
9

10
11
12
13
14
15
16
17
18
19
20

21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39

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 aneffect, 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].
[Kwhr: fix 55] 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 one-shot delimited continuations [13]. They also defined a generalized yield
operator which has multi-shot continuations and show the connection between
it and the delimited-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.

One-shot Algebraic Effects as Coroutines

19

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→ yield (Resend r continue)| Eff| 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

9

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.

10

7

1
2
3
4
5
6
7
8

11
12

Conclusion

We have presented a novel embedding technique for algebraic effects and handlers
into asymmetric coroutines, and shown translation from the former to the lat-

20

Satoru Kawahara and Yukiyoshi Kameyama

26

ter 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
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.

27

References

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25

28
29
30
31
32
33
34
35
36
37
38
39
40
41

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)1314https://reactjs.org/docs/hooks-reference.html
https://overreacted.io/algebraic-effects-for-the-rest-of-us/

One-shot Algebraic Effects as Coroutines

21

37

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)
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)

38

A

Semantics of λeff

39

A.1

Helper functions

40

We introduce three helper functions for semantics in Figure 11: [Kwhr: fix 16]

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36

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

6

split (K, eff ) returns a triple (K1 , F, K2 ) where F is the frame that handles
the effect named by eff, and K = K1 :: [F ] :: K2 holds. [Kwhr: fix 31] If morethan one frame can handle 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 acontinuation in functional form. (K ∗ E) creates a closure with a stack frame K
and an environment E.

7

A.2

1
2
3
4
5

8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27

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 [Kwhr: fix 17] standard. The rest of the rules are the one for algebraic effects and handlers. 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 isgoing to be evaluated under this handler. The rule PushPerform pushes theframe of perform-ing an effect eff to the stack. The rules HandlePerformand HandleValue are the key rules for algebraic handlers. In the rule HandlePerform, the code component is a value w. Hence, the first frame in thestack perform eff  is retrieved and evaluated. Then we look for a handler
whose name is eff in the stack K, and if we find it, we use the handler tocope with this effect where formal parameters y and k are bound to the value
w and the delimited continuation K 0 under environment E. We adopt the deep
eff
handlers, hence the handler (with wh handle )
remains in the stack after
this step. The rule HandleValue is used when the handled expression does notinvoke an effect and returns a value w. Then the value handler (val x → ev ) isused, and the handler is eliminated from the stack after this step.

One-shot Algebraic Effects as Coroutines
1

2
3
4
5
6
7
8
9

10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41

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 be aparent of another coroutine by resuming it. [Kwhr: fix 29] The rule have an assumption that C2 does not have any labelled expresses. The assumption indicates that
C2 is the innermost active coroutine. The function LabelledReturn transfers
the result of the computation v in the coroutine l to its caller. The functions
EqT and 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

1

C

Reply to reviewers

2

Dear reviewers of an earlier version of this paper,

3
4
5
6
7
8
9

Thank you very much for your careful reading and helpful comments.
We do appreciate all your comments very much. In this revision,
we did our best to address the issues you raised. We have solved
most issues but unfortunately we have not been able to manage all,and here we show how and what we did for your comments. (To avoid
clutter, we omitted responses for small literal errors.)

10
11
12

Best regards,
Satoru Kawahara and Yukiyoshi Kameyama

13
14
15
16
17
18
19
20
21
22

>>----------------------- REVIEW 1 -------------------->>Cons:>> - No comparison is made with de Moura and Ierusalimschy’s earlier work,>>
which already shows that one-shot continuations can be encoded into>>
asymmetric coroutines.
>>
In fact, perhaps the encoding presented here could be presented as the>>composition of a simpler encoding (from multiple effects to a single>>
effect) with de Moura and Ierusalimschy’s encoding. (See below.)

23
24
25
26
27
28
29
30
31
32
33

It is true that we can give a translation from a calculus with one-shotcontrol operators to a calculus with asymmetric coroutines, by such acomposition. The merit of our translation is that it is given asa simple, local translation (de Moura and Ierusalimschy’s translation
uses mutable state which may store higher order functions.) This property
is made explicit as a ’macro-expressible’ translation in the sense ofFelleisen (Sect. 3.4 in the revised paper). Although it is a very simple
property, we think that it is sufficient to claim that our translation is
simple. The property also lets us implement the translation as a simple
library (which does not need any external resource).

34
35

>>

- The encoding is not well-explained.

36
37
38
39
40

We are sorry for this. In fact, we did not give explanation in theearlier version. The revised version contains a concrete example oftranslation (encoding) and we gave a detailed explanation based on theconcrete example. (Sect. 3.3)

41
42
43
44
45

>>MAJOR GENERAL COMMENTS>>>>>>> It seems to me that coroutines, as presented in this paper (the calculusOne-shot Algebraic Effects as Coroutines
1
2
3
4
5
6
7
8
9
10
11

>>>
>>>
>>>
>>>
>>>
>>>
>>>
>>>
>>>
>>>
>>>

25

lambda_{ac}), are a mix of delimited control and dynamically-allocated mutablestate. Because of this, instead of implementing delimited control in terms of
coroutines, as proposed in the present paper, it would seem rather morenatural to me to explain (or implement) coroutines in terms of delimited
control and mutable state. I can see that the encoding proposed in this paper
is useful in situations where the host language has coroutines (e.g. Lua), butotherwise this encoding seems to be going in the wrong direction. In a
language where mutable state and (one-shot) effect handlers are primitive,
coroutines can be programmed as a library. (See e.g. Section 4 of "EffectHandlers for the Masses", by Brachthäuser et al.) Isn’t that a more pleasing
approach?

12
13
14
15
16
17
18
19
20
21

Thank you for your insight. We agree that the converse direction is worth studying,
but we still do believe the present direction (from algebraic effects and handlers tocorouines) is interesting, as it gives an implementation of the former in a huge numberof programming languages. (The cretin Henry in Wikipedia has a large list of
programming languages with native support for coroutines; although we have notexamined the list in detail, as to whether they support stackful asymmetric coroutines
which is needed for our work, we can surely say that the direction to coroutines
is worth studying.) In the revised version, we modified the introduction (Sect. 1)
to mention these facts briefly.

22
23
24
25
26
27
28
29
30
31
32
33

>>>
>>>
>>>
>>>
>>>
>>>
>>>
>>>
>>>
>>>
>>>

p.2, I am confused by the sentence "However, as we will see in this paper,
coroutines are as expressive as one-shot delimited control-operators, a
restricted control operator that is allowed to invoke a delimited continuation
at most once [13]." Without the citation at the end, this sentence seems tosuggest that the equivalence between coroutines and one-shot delimited control
is a contribution of this paper. The abstract of the paper suggests the samething. Yet, once one looks up the citation [13], one discovers that thisequivalence has already been pointed out by de Moura and Ierusalimschy. As aresult, at this point, I am confused, and do not know exactly how the present
paper improves on (or distinguishes itself from) de Moura and Ierusalimschy’s
paper. This should be clarified!

34
35
36
37

The sentence was our mistake; we do not claim that we are the first to
make this equivalence (or connection), and we have removed the phrase "as we will
see in this paper,".

38
39
40
41
42
43
44
45

>>> Although the encoding (Figure 5) is relatively compact, the key part (the>>> definition of "handler") is still 10 lines of complex code, and the>>> explanation on page 12 does not really help; it is a paraphrase of the code.
>>> I suspect that part of the complexity has to do with the fact that the source>>> calculus has multiple named effects (like "Get", "Set", "Defer", etc.) and it>>> is possible to perform an effect that is handled by a handler which is *not*>>> the nearest handler; whereas the target calculus does not have a comparable

26
1
2
3
4
5
6
7
8
9
10
11
12

Satoru Kawahara and Yukiyoshi Kameyama>>> mechanism ("yield" transfers control to the nearest mark on the stack). So,>>> I wonder if the encoding could be viewed as the composition of two separate>>> (simpler) encodings, namely:>>>>>> - an encoding of a calculus with multiple (named) effects>>>
into a calculus with a single effect; and>>> - an encoding of this calculus with a single effect>>>into a calculus with coroutines.
>>>>>> The first encoding would take care of comparing effect labels for equality,>>> wrapping effects in "Resend", etc., while the second encoding would take care>>> of encoding "perform" into "yield". Does that make sense? Is this possible?

13
14
15
16
17
18

This perfectly makes sense, but, the definitions in this way are (conceptuallymuch simpler, but) not that simple, and we need to explain two non-trivial
translations, which needs huge space. Also if our translation is a compositionof two translations, which is less efficient the one given in this paper.
We will try again when we revise this paper in future (e.g. writing a journal version).

19
20
21
22
23
24

>>> Furthermore, the second encoding above might be essentially identical to the>>> encoding proposed by de Moura and Ierusalimschy. (They encode a calculus with>>> a "spawn" operator, which looks analogous to shift/reset, into a calculus with>>> coroutines.) If that were the case, then the contribution of this paper would>>> have to be re-explained in a different way.

25
26
27
28

As we wrote above, one of the major merits of our translation is that it isa macro-expressible translation, which distinguishes itself from the earlier
work by de Moura and Ierusalimschy (though the translations share the same spirit.)

29
30>>MINOR GENERAL COMMENTS

31
32
33
34
35

>>> Is there a proof that this encoding is correct? (A machine-checked proof would>>> be ideal.) I would not be interested in reading the details of the proof, but>>> I would be interested in reading the main invariants that explain why the>>> encoding works, and it would be good to know that a proof exists.

36
37
38

Unfortunately the precise (e.g. formalized in Coq) proof does not yet exist, though
it is a relatively routine work to carry out the proof.

39
40
41
42
43

>>> If the source and target calculi were equipped with (standard) type systems,>>> would the encoding be type-preserving? It would be worth answering this>>> question (if the answer is obvious) or explicitly deferring it to future work>>> (if nonobvious).

44
45

Well, it *is* an interesting future work and we mention it in the conclusion.

One-shot Algebraic Effects as Coroutines
1
2
3
4

27

The type system of asymmetric coroutines is not so trivial -- there exist a few
such proposals, but as long as we have examined much earlier, none of themis sufficiently strong (even a very simple typed calculus for shift and resetcannot be translated to any of them in a type-preserving way. )

5
6
7
8
9
10
11
12
13

>>DETAILED COMMENTS>>> p.1, "Implementations based on stack manipulation are used in JVM bytecode and>>> C implementations". Please provide citations at this point. Same request about>>> "OCaml implementation and one of Scala implementations". (In fact, the>>> required citations are given at the end of the first paragraph, but it was not>>> evident to me at first that these citations were specifically concerned with>>> the implementation of effect handlers; I initially thought that were generic>>> citations about the programming languages Haskell, OCaml, etc.)

14
15

Thank you for the comment. We have added citations and also rewritten the sentences.

16
17
18
19
20

>>> p.1, "it highly depends": what does "it" refer to?
>>> p.1, "which needs deep insight on language processors": who needs deep insight?
>>> The runtime system? What does that mean? And what is a "language processor"?
>>> I don’t think this terminology is standard.

21
22

We rephrased this to "an implementer needs deep insight on its internal structure."

23
24
25

>>> p.1, the English in paragraph 2 is not great. It would be good if the paper>>> could be proof-read by someone who is proficient in English.

26
27

We are sorry. We tried to revise it based on the comments.

28
29
30
31
32
33
34

>>> p.2, "implementing delimited control-operators in a language is non-trivial":>>> isn’t just as difficult to implement delimited control operators and to>>> implement effect handlers? Each feature can encode the other. (Assuming an>>> appropriate control operator is chosen.) (See e.g., Forster et al, "On the>>> expressive power of user-defined effects: Effect handlers, monadic reflection,>>> delimited control".)

35
36

Yes, you are right and we have removed the sentence.

37
38
39
40
41
42
43
44
45

>>> p.2, "We will show that using coroutines to implement algebraic effects and>>> handlers have another merit: a programmer does not have to think about what>>> data structures are used to embed algebraic effects." This sentence is unclear>>> to me in several ways. The authors write that this implementation scheme has a>>> "merit": in comparison with what other implementation scheme? And why would>>> the programmer have to think about data structures? One might hope that,>>> regardless of how effects are implemented, the programmer does not have to>>> think about it.

28

Satoru Kawahara and Yukiyoshi Kameyama

12

We have removed the sentence.

3
4
5
6
7
8
9
10
11

>>> p.2, "Although implementations of algebraic effects using coroutines already>>> exist such as 10 11 12, each one has such problems as it does not provide a>>> first-class continuation to the user, or is rather complicated." Please>>> clarify which implementation has which deficiency. Also, please clarify your>>> criticisms. "Not providing a first-class continuation to the user" sounds like>>> a critical problem: if that is the case, then this library *cannot* be called>>> an implementation of algebraic effects, can it? "Being rather complicated" is>>> somewhat vague; could you be more specific?

12
13

We have removed the original sentences, and rewritten the whole paragraph.

14
15
16
17
18
19

>>> p.3, "We show a new embedding". The word "new" suggests that there already>>> exist known encodings of algebraic effects in terms of coroutines in the>>> literature? Is this the case? If so, please cite them explicitly. If not,>>> then remove the word "new". (I suggest writing "We give an encoding of>>> one-shot algebraic effects and handlers into asymmetric coroutines.")20
21

Yes, there is no such encoding, and we have removed ’new’.

22
23
24
25
26
27

>>> p.3, "We do not use continuation-passing style nor user-level control>>> operators. As a consequence, our embedding is more performant in many cases>>> than other embeddings, including the one with free monads." This sentence>>> could be clarified to indicate exactly which other encodings you are comparing>>> against.

28
29

We were comparing it with free-monad based embedding, and we rephrased the sentence.

30
31
32
33

>>> Section 2.2, this material is standard. A citation of the original paper where>>> this is described would be welcome. Also, I am not sure how this example adds>>> value to the paper.

34
35
36

Well, we think that many readers are not familiar with even syntax of Lua etc.
and an easy introductory example is necessary for a technical paper.

37
38
39
40

>>> Section 2.3, this example seems a little underwhelming (I mean, not very>>> convincing), because it seems clear that "defer" can be implemented using>>> just first-class functions and references.

41
42
43

Thank you. We tried to fix the problem, but unfortunately due to lack of space,
finally we had to eliminate the example completely.

44
45>>> The placement of Figure 2 is not great. There is one line of text below it.

One-shot Algebraic Effects as Coroutines

29

1
2

Thank you, fixed it.

34>>> p.9, what does "more or less standard" mean?

5
6

Removed the phrase "more or less".

789>>> p.9, "We adopt the deep handlers". A citation of a paper that explains the>>> distinction between shallow and deep handlers would be welcome.

10
11
12

We have added one reference, though we have not found any good reference about this
discussion.

13
14
15
16
17

>>> p.11, "Due to lack of space [...]". The reader who is not familiar with>>> coroutines needs at least an intuitive explanation of the meaning of>>> labeled expressions and the operations create, yield, resume. It would>>> be easy to make some room in the paper by removing Section 2.2 or 2.3.

18
19

We have revised the explanation of the informal semantics of coroutines.

20
21
22

>>> In Figure 5, the various renamings of x to x’ are just noise, as far as>>> I can see. Why not just keep the name x?

23
24

Yes, you are right, primes have been eliminated.

25
26
27
28

>>> p.13, "our translation [...] does not rely on higher-order stores": the>>> operational semantics of coroutines does rely on a store (a mapping of>>> labels l to lambda-abstractions), so this statement is questionable.

29
30
31

De Moura and Ierusalimschy’s translation (not semantics) does use higher-orderstores.

32
33
34
35
36
37
38

>>> p.14, "Representing coroutines and other effects using algebraic effects and>>> handlers is possible, but tedious if the language has coroutines from the>>> beginning." I am not sure if "tedious" is the right word. It does not sound>>> difficult to encode coroutines in terms of effects (the encoding is known),>>> but this adds a lot of overhead, since one has to go through two layers of>>> encoding instead of using native coroutines.

39
40

Yes, we have removed the word ’tedious’ and rewritten the whole sentence.

41
42
43
44
45

>>> p.14, "This problem can be solved as follows [...]." I do not understand what>>> is going on here. The previous sentence suggested that encoding coroutines in>>> terms of effects is of course possible, but very costly. The text that follows>>> repeats that it is possible to encode coroutines in terms of effects, and gives

30
1
2

Satoru Kawahara and Yukiyoshi Kameyama>>> the encoding. How does that "solve" the problem? The encoding remains very>>> costly.

3
4
5

Since we have removed the sentence just before this one, we think the resulting
text makes sense.

6
7
8
9

>>> p.15, "Although we know several solutions to this direction, clearly we need>>> to do more [...]". This sentence is very unclear. Which solutions do you know,>>> and why are they not satisfactory? Only one solution has been shown.

10
11
12
13
14

We have rewritten it to
Although we can combine our library and coroutines by reimplementing coroutines as above, whenever we want to use other native effects,
we must deal with them.

15
16
17
18
19

>>> p.19, "Some of them have implemented our translation for other languages such>>> as JavaScript and Rust". This seems puzzling: does Rust have coroutines? How>>> are they implemented? As far as I know, they are not a primitive construct in>>> Rust.

20
21
22

Thank you. We rewrote the footnote toSince Rust does not have coroutines, we use Future instead.

23
24
25
26
27

>>> p.20, "a new store which consists of pairs of a variable and a value".
>>> A store usually maps *locations* to values. An environment usually maps>>> *variables* to values. It is confusing to see these notions apparently>>> mixed up here. What is going on?

28
29
30

The paper ’Revisiting coroutines’ uses this terminology (which might be somewhat
non-standard) and we want to follow their way as long as coroutines are concerned.

31
32
33

>>> p.21, "θ is a partial map from variables or labels to values". This is also a>>> bit confusing. A map of variables to values is an environment. However, here,

34
35

Yes, but again we followed the paper ’Revisiting coroutines’.

36
37
38
39

>>> The authors adopt environment-based semantics, as opposed to>>> substitution-based semantics, for the source and target calculi.
>>> Why is that? Could this decision be discussed?

40
41
42

We think environment-based semantics is also natural (and slightly morepractical).

43
44
45

>>> p.22, the reduction rule (Yield) seems non-deterministic, as there could be>>> several marks "l:" on the stack. Should one add a side condition stating that

One-shot Algebraic Effects as Coroutines
1
2

31>>> the context C_2 contains no marks? (See the distinction between C and C’ in>>> de Moura and Ierusalimschy’s semantics.)

3
4
5

The rule have an assumption that C2 has no labeled expresses, then C2 must
be the innermost active coroutine.

6
7
8
9
10
11

>>>done p.4, line 2 begins with a stray comma.
>>>>>>done p.4, "with still handled" does not make sense.
>>>>>>done p.11, "propositional": do you mean "compositional"?

12
13

Thank you for careful reading and spotting typos.

1415>>----------------------- REVIEW 2 ---------------------

16
17
18
19
20
21
22
23
24
25
26
27
28
29

>>I think this should be accepted for presentation. It’s certainly in scope,>>describes a topic which is certainly part of a trend, and applies it in a>>less conventional (for this audience) setting. I’m not sure it’s ready yet>>to be accepted for publication though. I’d like to see more discussion of>>the motivation and limitations. I assume, since Lua is a dynamically>>typed imperative language, the main motivation is to allow effects to be>>handled in different ways in different contexts? In which case, it’d be nice>>to be explicit about this and show examples to illustrate it. Another>>motivation for algebraic effects is to be explicit about the capabilities of>>a function in its type, so could your approach be adopted by a statically>>typed language to achieve this? And is it a serious limitation to have>>one shot continuations - it would prevent implementing non-determinism as>>an effect, for example.

30
31
32
33

We hoped so, but introduction type systems and making the translation type-preserving
are tricky, as the existing type system for coroutines are not expressive enough.
But this is an interesting future work, and we mention it.

34
35
36
37
38
39

>>It’s nice to see the benchmarks, but they are fairly small and I would also>>like to know what the overhead of the library is compared to writing>>effectful programs directly, and some discussion of whether that overhead>>is worth it. One example suggests the overhead is not too bad, but there>>has to be a strong enough motivation to explain why it’s worthwhile.

40
41
42
43

We have added more figures and more benchmarks. Although they are still
microbenchmarks, we think that the extreme-case examples show the small overheadof our implementation.

44
45>>> p4 I’m not familiar with Lua, and I can guess what the notation

1
2

32

Satoru Kawahara and Yukiyoshi Kameyama

>>>
>>>

[DivideByZero] means, but for this audience it might be worth explaining a
bit more

3
4
5

We are sorry and we should not assume the familiarity with Lua. We have added more
explanations for Lua syntax and the code.

678>>> p6 Instead of giving this in Go, could you should how it’s used in your>>>library instead?

9
10
11

We have tried to do so, but unfortunately we had to eliminate the last example
due to lack of space.

1213>>> p7 "To implement the full functionality of defer..." - have you done this?

14
15

Yes, you can find it in our Github repository.

16
17
18
19

>>> p16 Can you say in more detail what these benchmarks do? Rather than just>>>saying which effect they use. Also for state in particular, it’d be nice>>>to know the overhead over implementing state directly.

20
21
22

We have thoroughly revised the section for benchmark and performance evaluation,
which hopefully addresses your concern.

23
24>>>done p2 "thanks to that fact that" => "thanks to the fact that"25
26

Thank you, fixed.

27
28>>> p3 What is ’inst()’? Something which creates a unique new effect label?

29
30

We explained it in the text.

31
32
33

>>> p4 typo "catches the effect DivideByZero">>> p8 "more than one frames have" => "more than one frame has"

34
35

Fixed.

36
37
38
39

>>> p14 "The implementations are simple and easy to understand" - this is a>>>strong claim, without showing any of the code here! Is there any part of it>>>
which you can present?

40
41

We have clarified the meaning (and rephrased the sentences).

4243>>> p15 "the result of ours library" => "...our library"

44
45

Fixed.

One-shot Algebraic Effects as Coroutines

33

1
2
3
4
5
6
7
8

>>----------------------- REVIEW 3 -------------------->>One issue with the paper is that it doesn’t, from the start, state a clear, main goal.
>>The abstract states context, and the fact of what was implemented, but to what end?
>>As an advantage "modularity" is given. I think this could be made much stronger>>pointing to the good performance results, and referring to the other aspects as>>additional>>advantages.

9
10
11
12
13
14
15
16

Thank you for the comment. Our goal is to make AEH available in MANY languages. (AEH
for algebraic effects and handlers).
We think that algebraic effect and handlers are good abstraction for writing
control effects, and implementer who write controlful programs in Lua would
benefit from our work very much, as composing two effects realized by coroutines
is not an easy task, while composing two algebraic effects is straightforward.
We have revised the abstract and introduction along with this line.

17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33

>>The formal presentation builds on the CEK machine, and adds rules for performing and>>handling effects. The target of the translation is an existing calculus of asymmetric>>coroutines. No formal correctness proof is given, so correctness of the translation>>can’t be seen as a contribution. But the operational semantics of the CEK machine>>with effects, and the translation look plausible. Also, the implementation has been>>tested on a range of micro-benchmarks that are used for the performance results.
>>>>Notably, the style of the translation should be applicable to a range of languages,>>and the paper makes the point that it has been implemented not only in Lua and Ruby,>>but also (by others) in more main-stream languages such as JavaScript and Lua.
>>>>The performance results compare this translation with an existing free-monad>>based implementation of effects and show sizable gains, and good scalability,>>over increasing>>numbers of iterations. However, there is an additional cost for the unlikely case of a>>high number of nested handlers.

34
35
36

Thank you for your analysis, which spots merits and demerits of our current approachcorrectly.

37
38
39
40

>>> From the start, state the main goal: is it performance? or finding a translation>>> that is modular, portable and high-performant at the same time.
>>> Too much space is spent on context here, IMHO, and could go into intro.

41
42
43
44
45

We have added a sentence. "This paper presents a translation from algebraic
effects and handlers to asymmetric coroutines, which provides simple,
portable and widely applicable implementation of algebraic effects."

34
1
2
3

Satoru Kawahara and Yukiyoshi Kameyama>>> Might mention that reasoning about effects is notoriously difficult,>>> and implementations>>> are therefore error-prone. Therefore a formalized implementation is very desirable.

4
5
6

We could have mentioned it, but since we do not really ’reason about’ programs,
we hesitate to do so. But thank you for the very encouraging comment!

7
8
9
10

>>> p2, top: refers to a range of implementations of effects, with pros and cons,>>> but doesn’t>>> give references (at least to the main ones).

11
12>>> Highlight the "new embedding of alg effects and handlers" as main novelty.

13
14

We have revised the paper accordingly.

15
16>>> I’d expect more of a rationale why Lua and Ruby are used as languages.

17
18
19

Well, we think they are popular languages, and in particular, we believe that
Lua is the best language to study coroutines (but we cannot prove this claim).

20
21
22
23
24

>>> Good to have several repos of implementations mentioned early in the paper.
>>> Good summary of contribs: mention the main ones in the abstract already.
>>> "conversion of \lambda_eff" is a bit vague: stick to the phrasing "translation">>> throughout.

25
26

Yes, thank you, we revised it.

27
28
29
30
31
32
33

>>> Before the first example I’d expect some words about Lua syntax. As it stands>>> it’s hard>>> to read for someone not already familiar with the lang (main audience of TFP).
>>> Suggest to number the lines in the examples to more easily refer to it.
>>> Could use comments in the code to e.g. clarify that the 2 params to handler are the>>> (value) argument and the continuation.

34
35

We have added more explanations about the code with line numbers etc.

36
37>>> Some background on delimited continuations earlier in the paper would be useful.

38
39
40

It is hard to mention it within the limited space, but we have shown a concrete
example of a delimited continuation as a context.

41
42>>> What’s the role of the value 0 passed to the continuation in case of a DivideByZero?

43
44
45

Not very much, but it is natural to pass some default value...

One-shot Algebraic Effects as Coroutines
1
2

35>>> p5, bottom: in the text you talk about "binds s to v" and creating a thunk. Refer to>>> the lines in the code to link things up.

3
4

We did it.

567>>> last para: if you are saying the simplicity of implementation with your notation is>>> an advantage in itself, you should expand on it and mention this more prominently.

8
9
10

Our notion of simplicity is based on macro-expressiveness, which is now detailedin Sect. 3.4.

11
12
13

>>> Since you are building on the CEK machine, more context and concrete pointers>>> would be useful!

14
15

We have added a reference.

16
17
18
19

>>> Giving intuitions for frames, possibly as "break-points" in the execution,>>> would be good>>> (together with general CEK machine background)

20
21
22

Here we use frames as just an element of a continuation (where a continuation
is a list, or a stack of frames.) We have added a simple explanation for frames.

23
24
25
26
27
28
29
30
31
32
33
34

>>> Fig 2: minor issue, but I don’t find the notation for these operations>>> very intuitive;>>> maybe something more verbose such as "lookup" for // would be better?
>>> Fig 3 and text: mention that CloseHandler and Handle rules are analogous to>>> Close and App rules in the plain CEK machine.
>>> I think some rules can be simplified: in CloseHandle you don’t refer to>>> the syntactic components of the handler h, so you don’t need to>>> expand its structure in the rule>>> Might mention that HandlePerform and HandleValue correspond to the effect>>> and no-efect>>> cases respectively.

35
36
37

Well, we wanted to explain the semantics more but due to space limitation
we had to move the semantics section to appendix.

38
39
40
41
42
43
44
45

>>>
>>>
>>>
>>>
>>>
>>>

One bigger issue I have with the notation is that ’::’ is used both forsequencing the list of frames in the continuations part, andfor adding a binding to the environment.
I think using more established notation for the latter, andthus separating the two
operations would help here.

36
1Satoru Kawahara and Yukiyoshi Kameyama

Here we use the symbol to mean the ’cons’ operation for lists.

2
3>>> Fig 4: give in the text at least an intuition for the meaning of Eff, Resend etc.

45

We have added detailed explanation.

6
7
8
9
10
11
12
13
14
15

>>> Fig 5 and text: the translation of the main case ’handler’ is intricate,>>> but looks plausible;>>> it would help to give some explanation on the structures Eff and>>> Resume as well as the>>> operations yield and resume that are used here. Maybe a simple>>> presentation in a>>> sequence-diagram style figure would help. I think at least this>>> level of detail is needed>>> as context for the last 2 paras on p12.

16
17
18

We have added a concrete example to show how the translation (and the translatedcode) work.

19
20
21
22
23
24
25
26
27
28

>>> A summary of the main characteristics for the bench-mark programs>>> at the beginning would>>> be useful. In particular, the meaning of the ’parameter’ in each>>> of the benchmarks is>>> different (Fig 6 and 8: number of iterations; Fig 7: number of nested>>> handlers), and>>> this should be highlighted. Possibly, restructure into sub-section,>>> to measurement>>> the impact of different kinds of params.

29
30

Yes, we have added more explanation.

31
32
33
34
35
36

>>> In general, good analysis of the reasons for performance gains.
>>> It would help to back up>>> the statements by supportive data (isolating the costs for the main>>> impact factor), but>>> given the focus of the paper I don’t think this is strictly necessary.

37
38

Yes, we have revised the section within the page limitation.

39
40
41

>>> What is the same-fringe problem? Give an intuition. And thanks for>>> giving a link to the repo!

42
43

We are sorry, now you see a short explanation for ’fringe’.

44
45>>> Reference to "James and Sabry" is missingOne-shot Algebraic Effects as Coroutines
1
2

Fixed.

3
4>>> Overall: several spelling mistakes in the paper

56

We have tried our best.

7
8

Thank you for all your comments!

37

38

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

39

40

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