Algebraic Effects for Functional Programming
2016 · paper · Computer science
Gives an end-to-end overview of algebraic effect handlers in the Koka language. It covers type inference with extensible effect rows, an operational semantics, and a type-directed selective CPS compilation scheme for platforms such as JavaScript, the JVM and .NET.
Checked: PDF from microsoft.com, fetched 4 Oct 2026. Page numbers are those of that PDF.
5 findings
Substance The printed result "> eager{ parse(”1+2*3”, expr) } Just((7,””))" does not follow from the eager handler ("the False branch is taken first") and choice as printed; those definitions return Just((1,"+2*3")).
- p. 6 Section 2.6, eager example output
Just((7,””))
- p. 5 Section 2.6, eager handler
Here, the False branch is taken first
Only the authors can say what is right here.
Judge's note: eager (p.5) is flip() → match(resume(False)) {Nothing → resume(True); Just(x) → Just(x)}, so it returns the first success in False-first order. Through choice (False → p2), expr → term → factor gives number = 1 on the first success. The parse handler's return x → (x,input) does not require the input to be consumed, so the first success is (1,"+2*3"). The output Just((7,"")) is printed on p.6. This has the same root cause as C010 but is a different printed value.
Second check: another model agreed
Report a problem with this finding
Substance p.9, Theorem 1: "If · ⊢ e : τ | ϵ then either e ⇑ or e ↦↠ v" is stated for an arbitrary effect ϵ. Lemma 4.b ("If Γ ⊢ Xop[op(v)] : τ | ϵ ... then l ∈ ϵ") does not make unhandled operations untypeable when l ∈ ϵ.
- p. 9 Section 4.3, Theorem 1
If · ⊢ e : τ | ϵ then either e ⇑ or e
- p. 9 Section 4.4, Lemma 4.b
b. If Γ ⊢ Xop[op(v)] : τ| ϵ, with op ∈ Σ(l), then l ∈ ϵ.
Only the authors can say what is right here.
Judge's note: My own reworking. Operations have to be typed from the initial environment Γ0, because rule HANDLE itself needs Γ ⊢ opi. Otherwise no closed program containing a handler would be typeable. Section 2 gives raise : string → ⟨exc⟩ a. By App with ϵ = ⟨exc⟩, raise("hi") is typeable. It is not a value. Checking Figure 4: (δ) needs a constant c, and (handle) needs an enclosing handle{h}. So the term is stuck: it neither diverges nor reaches a value. The proof sketch rests on "faulty expressions are not typeable", but Lemma 4.b only gives l ∈ ϵ. The paper itself reads it as "effect types are meaningful", not as untypeability. The theorem as printed therefore holds only for a restricted ϵ, for example ⟨⟩. Only the authors can say what was intended.
Second check: another model agreed
Report a problem with this finding
Reference or label Reference [31] lists 'Florian Loitsch, Manuel Serrano, and Inria Sophia Antipolis' as authors; 'Inria Sophia Antipolis' is an institution, not an author.
- p. 13 Reference [31]
Florian Loitsch, Manuel Serrano, and Inria Sophia Antipolis.
Judge's note: Viewed crop of p.13, reference [31]. An institution name is printed as the third author, which looks like the affiliation leaked into the bibliography metadata. That it is an institution is clear from the name itself.
Second check: another model agreed
Report a problem with this finding
Wording The printed output of solutions{ parse("1+2*3", expr) }, "[(7,””),(3,”*3”),(1,”+2*3”)]", is in the reverse order of what the printed definitions produce.
- p. 5 Section 2.6, solutions example output
[(7,””),(3,”*3”),(1,”+2*3”)]
- p. 5 Section 2.6, choice and solutions definitions
flip() → resume(False) + resume(True)
- p. 5 Section 2.6, choice definition
fun choice(p1,p2) { if (flip()) then p1() else p2() }
Only the authors can say what is right here.
Judge's note: Traced by hand from the page-5 definitions. solutions handles flip() as resume(False) + resume(True), so results of the False branch come first. choice is 'if (flip()) then p1() else p2()', so False selects p2. expr's False branch is { term() }; term's False branch is { factor() }; in factor = choice(number){paren}, the paren branch fails and number gives 1 (many's False branch is Nil). That gives (1,"+2*3") first. expr's True branch gives 1+2 = 3 with rest "*3" (term False) and then 1+2*3 = 7 with rest "" (term True). The definitions therefore give [(1,"+2*3"),(3,"*3"),(7,"")]. Only the authors can say whether choice or the printed output is meant to change.
Second check: another model agreed
Report a problem with this finding
Wording p.9, subject-reduction proof, handle case: "using lemma 1 in combination with (2) and (4) we conclude". Lemma 1 is Subject reduction itself; the substitution step needs Lemma 2 (Substitution).
- p. 9 Proof (Subject reduction), handle case
and using lemma 1 in combination with (2) and (4) we conclude
- p. 9 Proof of subject reduction, handle case
using lemma 1 in combination with (2) and (4)
Only the authors can say what is right here.
Judge's note: Page 9: Lemma 1 is "Subject reduction", the statement being proved. Lemma 2 is "Substitution". The step needs Γ, resume:τ2→ϵτr, x:τ1 ⊢ e : τr|ϵ, with (2) Γ⊢v:τ1 and (4) Γ⊢λy....:τ2→ϵτr, to conclude that e[x↦v, resume↦...] is well-typed. No reduction step is involved, so Lemma 1 does not apply; the step is substitution, applied twice. The (let) and (return) cases cite lemma 2 for the same step. The step is faulty as printed, but the result stands with Lemma 2, so S3.
Second check: another model agreed
Report a problem with this finding
33 minor (typos and the like; most checked by the judge only)
Wording Introduction says "introduced by Plotkin and Power in 2002 [36]", but reference [36] is dated 2003 ("Applied Categorical Structures 11 (1): 69–94. 2003.").
- p. 1 Introduction, first sentence
introduced by Plotkin and Power in 2002 [36]
- p. 14 Reference [36]
Applied Categorical Structures 11 (1): 69–94. 2003.
- p. 14 Reference [36]
Applied Categorical Structures 11 (1): 69–94. 2003
- p. 1 Introduction
Plotkin and Power in 2002 [36]
Judge's note: Both the text on p.1 and reference [36] on p.14 read as quoted. The year in the text and the year of the only work cited for it differ. The paper does not say that 2002 is the date of an earlier version. Rests on outside knowledge: whether an earlier 2001/2002 conference version exists that would explain the date. Either form could be legitimate, so this is an observation.
Second check: another model agreed
Report a problem with this finding
Wording Introduction says "introduced by Plotkin and Pretnar in 2009 [35]", but reference [35] is the LMCS article dated 2013 ("Logical Methods in Computer Science, volume 9. 4. 2013.").
- p. 1 Introduction, first sentence
introduced by Plotkin and Pretnar in 2009 [35]
- p. 14 Reference [35]
In Logical Methods in Computer Science, volume 9. 4. 2013.
Judge's note: Text (p.1) and reference [35] (p.14) checked in the images. The 2009 year does not match the cited entry, and no 2009 version is listed. Rests on outside knowledge: whether a 2009 ESOP version exists, which would explain the date. This is an observation, not an error.
Second check: another model agreed
Report a problem with this finding
Wording "fun digit(c : char) : parse int {" declares a parameter c that the body never uses, yet number() calls many1(digit), and many1 applies it as p() with no arguments.
- p. 5 Section 2.6, digit and number definitions
fun digit(c : char) : parse int {
Judge's note: Page-5 image: digit's body matches on input.first and d.digit? and never refers to c. many1(p) is defined as Cons(p(), many(p)). The parameter looks copied from symbol. The example is inconsistent as printed, and the fix (drop the parameter) is evident.
Second check: another model agreed
Report a problem with this finding
Wording Sections 3.1 and 3.3 are both titled "Type Inference", but 3.1 presents the declarative type rules ("The type rules for our calculus is given in Figure 3").
- p. 6 Section 3.1 heading
3.1. Type Inference
- p. 7 Section 3.3 heading
3.3. Type Inference
Judge's note: Both headings are visible in the page images (p.6 and p.7). Section 3.1 explains the rules of Figure 3; only 3.3 discusses inference.
Second check: another model agreed
Report a problem with this finding
Wording p.7: the prose says "bind resume to the function τ′i → τr", but rule HANDLE in Figure 3 binds resume : τ′i →ϵ τr.
- p. 7 Section 3.1, description of HANDLE rule
bind resume to the function τ′i → τr
- p. 7 Figure 3, HANDLE rule
resume : τ′i →ϵ τr
- p. 7 Section 3.1, text explaining HANDLE rule
bind resume to the function τ ′
- p. 7 Figure 3, rule HANDLE premise
Γ, resume : τ ′
Judge's note: Page 7: the Figure 3 HANDLE premise reads "Γ, resume : τ′i →ϵ τr, xi : τi ⊢ ei : τr | ϵ". The prose writes the arrow without an effect. In Section 2 (text layer line 88) the paper defines τ→τ′ as shorthand for the total function. Read strictly, the prose therefore gives resume a different type from the rule. Most likely the effect was left out informally, so I rate this as wording.
Second check: another model agreed
Report a problem with this finding
Typo Abstract, first sentence: "Algebraic effect handlers, are recently gaining in popularity" has a stray comma between the subject and the verb.
- p. 1 Abstract, first sentence
Algebraic effect handlers, are recently gaining
- p. 1 Abstract, first sentence
Algebraic effect handlers, are recently gaining in popularity
Judge's note: The comma is visible in the page-1 image of the abstract. The introduction has the same construction ("…in 2009 [35]), are recently"), but the abstract has no parenthetical that could justify a comma.
Second check: none (judge only)
Report a problem with this finding
Typo Section 2.1: "Just like monadic programming, algebraic effects allows us to conveniently program" has subject–verb disagreement.
- p. 2 Section 2.1
algebraic effects allows us to
Judge's note: Visible in the page-2 crop. This is a cosmetic grammar slip.
Second check: none (judge only)
Report a problem with this finding
Typo In foreach the parameter is declared as "act : () → ⟨yield⟨a⟩ | e⟩ ()", but the body uses "handle(action) {", so action is unbound.
- p. 3 Section 2.3, foreach definition
act : () → ⟨yield⟨a⟩ | e⟩ ()) : e () {
- p. 3 Section 2.3, foreach definition
fun foreach(f : a →e bool, act : () →⟨yield⟨a⟩| e⟩()) : e () {
- p. 3 Section 2.3, foreach body
handle(action) {
- p. 3 Section 2.3, foreach definition
fun foreach(f : a →e bool, act : () →⟨yield⟨a⟩| e⟩()) : e () { handle(action) {
Judge's note: The page-3 image shows the signature with 'act' and the next line with 'handle(action)'. The fix is evident: make the two names the same.
Second check: none (judge only)
Report a problem with this finding
Typo Section 2.4: "the result is now a list of tuples. and in both resumptions" has a full stop followed by a lowercase 'and'.
- p. 4 Section 2.4, after amb(state) example
a list of tuples. and in both resumptions
Judge's note: Visible in the page-4 image. This is a punctuation slip.
Second check: none (judge only)
Report a problem with this finding
Typo In the digit parser, "Just((d - ’0’).int,rest))" has one more closing parenthesis than opening ones; the tuple needs Just(((d - ’0’).int,rest)).
- p. 5 Section 2.6, digit definition
Just((d - ’0’).int,rest))
Judge's note: Counted in the page-5 image: two opening parentheses ('Just(' and '(d') against three closing ones (after '0', after rest, and the final one). Compare symbol's balanced Just((c,rest)).
Second check: none (judge only)
Report a problem with this finding
Typo Section 2.6: "we can now use the the solutions and parse handlers" has a duplicated 'the'.
- p. 5 Section 2.6, before the solutions example
we can now use the the solutions
- p. 5
n parser expr, we can now use the the solutions and parse
Judge's note: Visible in running text in the page-5 image, so it is not a line-break artefact.
Second check: code check
Report a problem with this finding
Typo "Changing the parsing strategy it orthogonal to the implementation" should read 'is orthogonal'; the reviewers also flagged "implement a extensible effects in Haskell" (p.12) and "produces a well-type value" (p.9).
- p. 6 Section 2.6, after Figure 2
Changing the parsing strategy it orthogonal
- p. 5 Section 2.6
we can now use the the solutions
- p. 6 end of Section 2.6
Changing the parsing strategy it orthogonal to the implementation
- p. 5 Section 2.6
now use the the solutions
Judge's note: All three are visible in the page images (p.6, p.12, p.9). The 'the the' on p.5 is covered by C011.
Second check: none (judge only)
Report a problem with this finding
Typo The text says "we also have kinds for effect rows ϵ, and effect constants (or effect labels) k", but in Figure 1 the kinds are the sans-serif e and k; ϵ is the metavariable for effect row types.
- p. 6 Section 3, kinds paragraph
we also have kinds for effect rows ϵ
Judge's note: The page-6 crop shows Figure 1 with 'k ::= ∗ | e | k' and 'ϵ ≐ τ^e'. The text uses italic ϵ in the position of the kind name, parallel to '∗' for value types. This is a minor notational inconsistency; the text may only be naming the types.
Second check: none (judge only)
Report a problem with this finding
Typo p.6: "Expression include handler expressions handle{h}(e)" should read "Expressions include".
- p. 6 Section 3, description of Figure 1
Expression include han-
- p. 6 Section 3
Expression include handler expressions
Judge's note: The page 6 crop shows "Expression include han-dler expressions" in the Section 3 paragraph. This is a number-agreement typo.
Second check: none (judge only)
Report a problem with this finding
Typo p.6, Sec. 3.1: "The type rules for our calculus is given in Figure 3" should read "are given".
- p. 6 Section 3.1
The type rules for our calculus is given in Figure 3.
Judge's note: The page 6 crop shows the sentence exactly as quoted. The plural subject takes a singular verb.
Second check: none (judge only)
Report a problem with this finding
Typo p.7: "the restriction is not necessary persé" should read "per se" (and arguably "not necessary per se").
- p. 7 Section 3.1, GEN rule discussion
not necessary persé
- p. 7 Section 3.1
the restriction is not necessary persé
Judge's note: The page 7 image shows "persé" in the GEN rule discussion. It is a misspelling of the Latin phrase.
Second check: none (judge only)
Report a problem with this finding
Typo p.7, Sec. 3.2: "up to 14.000 loc" uses a period as the thousands separator, which an English reader may take for 14.0.
- p. 7 Section 3.2
up to 14.000 loc
Judge's note: The page 7 crop shows "(up to 14.000 loc)". This is European style in an English text. It is minor, and either form could be intended.
Second check: none (judge only)
Report a problem with this finding
Typo p.9, proof handle case: "derive G0 ⊢ op : τ1 → ⟨l⟩ τ2 | ⟨⟩" uses a Latin G0 for the initial environment, which p.7 calls Γ0.
- p. 9 Proof (Subject reduction), handle case
derive G0 ⊢ op : τ1 → ⟨l⟩ τ2 | ⟨⟩
- p. 7 Section 3.1, HANDLE rule description
populate an initial environment Γ0
- p. 9 Proof (Subject reduction), final line
Γ ⊢ e[x↦v, resume↦λy. handle{h}(Xop[y])]
Judge's note: The page 9 crop shows a Latin italic G0. Page 7 introduces "an initial environment Γ0". This verdict covers only the G0 typo. The missing type in the final judgment is judged under C027.
Second check: none (judge only)
Report a problem with this finding
Typo p.8: "Evaluation continues with the expression ϵ but besides binding the parameter x to v": the clause body is e, not the effect symbol ϵ.
- p. 8 Section 4, paragraph on rule (handle)
Evaluation continues with the expression ϵ but besides binding
- p. 8 Section 4, text after Figure 4
Evaluation continues with the expression
- p. 8 Section 4, paragraph after the rules
Evaluation continues with the expression ϵ but besides binding the parameter x to v
Judge's note: The page 8 crop shows a Greek ϵ. Rule (handle) in Figure 4 continues with e[x↦v, resume↦...], where op(x)→e ∈ h, and ϵ is the effect-row metavariable.
Second check: none (judge only)
Report a problem with this finding
Typo p.8, Sec. 4.1: "optimizations that can be used to compiler handlers efficiently" should read "compile handlers".
- p. 8 Section 4.1, first sentence
can be used to compiler handlers efficiently
- p. 8 Section 4.1
that can be used to compiler handlers efficiently
Judge's note: The page 8 image shows "to compiler handlers efficiently".
Second check: none (judge only)
Report a problem with this finding
Typo p.8: "as the evaluation rules captures a delimited 'stack'": the subject and verb disagree (rules capture, or the rule captures).
- p. 8 Section 4, rule (handle)
as the evaluation rules captures a delimited
Judge's note: The page 8 crop shows the text as quoted.
Second check: none (judge only)
Report a problem with this finding
Typo p.9, proof handle case: "with op(x) → ϵ ∈ h (0)" writes the clause body as the effect symbol ϵ instead of the expression e.
- p. 9 Proof (Subject reduction), handle case
with op(x) → ϵ ∈ h (0)
Judge's note: The page 9 image shows Greek ϵ after the arrow. The reduct is e[x↦v,...], and the later step types e, so the body must be e. This is the same symbol slip as C021, but at a different location.
Second check: none (judge only)
Report a problem with this finding
Typo p.9: the handle case ends with "Γ ⊢ e[x↦v, resume↦λy. handle{h}(Xop[y])]" with no ": τr | ϵ", so the concluding judgment is incomplete.
- p. 9 Proof (Subject reduction), end of handle case
Γ ⊢ e[x↦ v, resume ↦ λy. handle{h}(Xop[y])]
Judge's note: The page 9 crop shows nothing between the closing bracket and the QED box. The lemma requires the conclusion Γ ⊢ e2 : τ | ϵ.
Second check: none (judge only)
Report a problem with this finding
Typo p.9, Sec. 4.3: "either produces a well-type value or diverges" should read "well-typed value".
- p. 9 Section 4.3
produces a well-type value or diverges
Judge's note: The page 9 image shows "well-type value".
Second check: none (judge only)
Report a problem with this finding
Typo p.10: "the xor function from the Section 2.4" has a stray article ("from Section 2.4").
- p. 10 Section 5
the xor function from the Section 2.4
Judge's note: The page 10 crop shows "from the / Section 2.4" across a line break.
Second check: none (judge only)
Report a problem with this finding
Typo Section 5.1: 'since the rule as state might duplicate code' should read 'the rule as stated'.
- p. 11 Section 5.1.2
since the rule as state might duplicate code
Judge's note: Viewed crop of p.11, right column: the text reads 'binding for k though since the rule as state might duplicate code.' The missing 'd' is a typo.
Second check: none (judge only)
Report a problem with this finding
Typo Section 6: 'Kiselyov et al. [20, 21] implement a extensible effects in Haskell' has a stray article; it should read 'implement extensible effects'.
- p. 12 Section 6
implement a extensible effects in Haskell
Judge's note: Viewed crop and p.12, right column, Related Work. The text reads 'implement a extensible effects in Haskell using the ‘freer’ monad.' The singular article 'a' before the plural noun is ungrammatical.
Second check: none (judge only)
Report a problem with this finding
Typo Section 6: 'type inference for Eff [2, 37] based subtyping and a region system' is missing 'on' ('based on subtyping').
- p. 12 Section 6, Eff paragraph
inference for Eff [2, 37] based subtyping and a region system
- p. 12 Section 6
[2, 37] based subtyping and a region system
Judge's note: Viewed both crops of p.12, right column. The text reads 'inference for Eff [2, 37] based subtyping and a region system.' on one line, so the word 'on' is missing.
Second check: none (judge only)
Report a problem with this finding
Typo Section 6, Frank paragraph: 'there is no primitive notion of a function: its handlers all the way down' should use 'it's'.
- p. 12 Section 6, Frank paragraph
its han-dlers all the way down
Judge's note: Viewed p.12, last paragraph of the right column. The text reads 'its han-dlers all the way down.' The intended meaning is 'it is handlers all the way down', so the contraction 'it's' is needed.
Second check: none (judge only)
Report a problem with this finding
Typo References [9] and [24] print 'In' twice: '[9] ... In In Proceedings of the 1998 ACM SIGPLAN Workshop on ML' and '[24] ... In In: Proceedings of the 2005 Symposium on Trends in Functional Programming'.
- p. 13 Reference [9]
In In Pro-
- p. 13 Reference [24]
In In: Pro-
- p. 13 Reference [9]
In In Pro-ceedings of the 1998 ACM SIGPLAN Workshop on ML
Judge's note: Viewed both crops of p.13. In [9] a roman 'In' is followed by an italic 'In Pro-ceedings'. In [24] a roman 'In' is followed by an italic 'In: Pro-ceedings'. The doubled word in both entries is a bibliography-field error.
Second check: none (judge only)
Report a problem with this finding
Typo Conclusion: 'In the future we plan use algebraic effects' is missing 'to' ('plan to use').
- p. 13 Section 7
In the future we plan use algebraic
- p. 13 Section 7 Conclusion
In the future we plan use algebraic effects
Judge's note: Viewed crop of p.13, Section 7. The text reads 'In the future we plan use algebraic effects to implement...', so 'to' is missing.
Second check: none (judge only)
Report a problem with this finding
Typo Reference [30] prints the author as 'Connor McBride' in 'Sam Lindley, Connor McBride, and Craig McLaughlin. “Do Be Do Be Do.”'
- p. 13 Reference [30]
Sam Lindley, Connor McBride, and Craig McLaughlin
Only the authors can say what is right here.
Judge's note: Rests on outside knowledge: that the co-author of 'Do Be Do Be Do' (POPL 2017) spells his name 'Conor McBride'. Viewed crop of p.13; the printed text does read 'Connor McBride'. The correct spelling cannot be checked within the files.
Second check: none (judge only)
Report a problem with this finding
Typo Reference [40] has an empty venue field: '“Implementing First-Class Polymorphic Delimited Continuations by a Type-Directed Selective CPS-Transform.” In . ICFP. 2009.'
- p. 14 Reference [40]
In . ICFP. 2009.
Judge's note: Viewed crop of p.14, reference [40]. 'In' is followed directly by ' . ICFP.', so the booktitle field is empty. This is a malformed bibliography entry.
Second check: none (judge only)