Internal effect handler primitives.

Internal primitives to implement evidence based algebraic effect handlers. These are emitted by the compiler during evidence translation and this module is always implicitly imported.

This module is compiled without monadic translation and thus we need to do this by hand in this module which allows us to implement most primitives directly in Koka keeping the external C/JavaScript/etc primitives to a minimum.

The paper:

Ningning Xie, and Daan Leijen. Generalized Evidence Passing for Effect Handlers, or efficient compilation of effect handlers to C. Proceedings of the ACM International Conference on Functional Programming (ICFP'21), August 2021, Vol 5: pp. 71, doi: 10.1145/3473576. https://​www.​microsoft.​com/​en-​us/​research/​publication/​generalized-​evidence-​passing-​for-​effect-​handlers-​or-​efficient-​compilation-​of-​effect-​handlers-​to-​c/​

describes precisely how the monadic evidence translation works on which this module is based. Read this first to understand how this module works.

Another paper of interest is:

Ningning Xie, and Daan Leijen. Effect Handlers in Haskell, Evidently. The 13th ACM SIGPLAN International Haskell Symposium, (Haskell'20), August 2020. https://​www.​microsoft.​com/​en-​us/​research/​uploads/​prod/​2020/​07/​effev.​pdf

which which explains the internal typing of handlers, evidence vectors, etc. in a simpler setting.

0.1. Notes

An effect row has kind ::E, while an atomic effect kind is ::X. (We will see that ::X is equal to the kind ::(E,V) -> V ) (::V is for value kinds *)

We use the term “answer” context to talk about the result type r and effect type e of (the context of) the handler in the stack. The e does not include the effect ::X of the handler.

type clause0std/core/hnd/clause0: (V, (E, V) -> V, E, V) -> V<a,b,e,c>
type clause1std/core/hnd/clause1: (V, V, (E, V) -> V, E, V) -> V<a,b,c,e,d>
fun clause-control1( clause : (x : a, k : (b) -> e d) -> e d ) : clause1std/core/hnd/clause1: (V, V, (E, V) -> V, E, V) -> V<a,b,c,e,d>

Generic control clause.

fun clause-control3( op : (x1 : a, x2 : b, x3 : c, k : (d) -> e b1) -> e b1 ) : clause1std/core/hnd/clause1: (V, V, (E, V) -> V, E, V) -> V<(a, b, c),d,a1,e,b1>
fun clause-control4( op : (x1 : a, x2 : b, x3 : c, x4 : d, k : (a1) -> e c1) -> e c1 ) : clause1std/core/hnd/clause1: (V, V, (E, V) -> V, E, V) -> V<(a, b, c, d),a1,b1,e,c1>

Clause that never resumes (e.g. an exception handler) (these do not need to capture a resumption and execute finally clauses upfront).

fun clause-never3( op : (a, b, c) -> e b1 ) : clause1std/core/hnd/clause1: (V, V, (E, V) -> V, E, V) -> V<(a, b, c),d,a1,e,b1>
fun clause-never4( op : (a, b, c, d) -> e c1 ) : clause1std/core/hnd/clause1: (V, V, (E, V) -> V, E, V) -> V<(a, b, c, d),a1,b1,e,c1>

Tail-resumptive clause that does not itself invoke operations (these can be executed ‘in-place’ without setting the correct evidence vector).

fun clause-tail-noop3( op : (c, d, a1) -> e b1 ) : clause1std/core/hnd/clause1: (V, V, (E, V) -> V, E, V) -> V<(c, d, a1),b1,b,e,a>
fun clause-tail-noop4( op : (c, d, a1, b1) -> e c1 ) : clause1std/core/hnd/clause1: (V, V, (E, V) -> V, E, V) -> V<(c, d, a1, b1),c1,b,e,a>

Tail-resumptive clause: resumes exactly once at the end (these can be executed ‘in-place’ without capturing a resumption).

fun clause-tail3( op : (c, d, a1) -> e b1 ) : clause1std/core/hnd/clause1: (V, V, (E, V) -> V, E, V) -> V<(c, d, a1),b1,b,e,a>
fun clause-tail4( op : (c, d, a1, b1) -> e c1 ) : clause1std/core/hnd/clause1: (V, V, (E, V) -> V, E, V) -> V<(c, d, a1, b1),c1,b,e,a>
type clause2std/core/hnd/clause2: (V, V, V, (E, V) -> V, E, V) -> V<a,b,c,d,e,a1>
fun clause-control2( clause : (x1 : a, x2 : b, k : (c) -> e a1) -> e a1 ) : clause2std/core/hnd/clause2: (V, V, V, (E, V) -> V, E, V) -> V<a,b,c,d,e,a1>
type evstd/core/hnd/ev: ((E, V) -> V) -> V<a>

Effect handler evidence of a handler h in the context.

alias ev-indexstd/core/hnd/ev-index: V = ssize_tstd/core/types/ssize_t: V

Index into an evidence vector.

type htagstd/core/hnd/htag: ((E, V) -> V) -> V<a>

The tag of a handler identifies the type at runtime (e.g. "exn/core/std").

type resume-contextstd/core/hnd/resume-context: (V, E, E, V) -> V<a,e,e1,b>
type yield-infostd/core/hnd/yield-info: V
fun finally( fin : () -> e (), action : () -> e a ) : e a
fun initially( init : (intstd/core/types/int: V) -> e (), action : () -> e a ) : e a
fun local-var( init : a, action : (l : local-varstd/core/types/local-var: (H, V) -> V<h,a>) -> <localstd/core/types/local: H -> X<h>|e> b ) : <localstd/core/types/local: H -> X<h>|e> b
fun unsafe-try-finalize( action : () -> e a ) : e eitherstd/core/types/either: (V, V) -> V<yield-infostd/core/hnd/yield-info: V,a>
fun yield-bind( x : a, next : (a) -> e b ) : e b
fun yield-bind2( x : a, extend : (a) -> e b, next : (a) -> e b ) : e b
fun yield-extend( next : (a) -> e b ) : e b
fun yielding(): boolstd/core/types/bool: V
fun yielding-non-final(): boolstd/core/types/bool: V
private import std/core/typesstd/core/types, std/core/undivstd/core/undiv