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.

• marker<e,r> : a unique integer corresponding to an answer context :<e,r>. This functions as a dependent type: when the integer matches at runtime, that will be the type of the answer context.

• handlers h are partially applied types with signature h<e,r> :: (E,V)->V for some answer context :<e,r>. The handlers contain all operations (much like a virtual method table). (these handler types are generated by the compiler for each effect type)

• Evidence ev<h :: (E,V)->V > for a handler h is an existential tuple forall e r. Ev( marker: marker<e,r>, hnd: h<e,r> ) containing the marker and the actual handler (pointer) for some answer context :<e,r> – we don't know the answer context exact type as it depends on where the handler was dynamically bound; we just have evidence that this handler h exists in our context.

• Actually, we use a quadruple for the evidence (corresponding to the evidence as formalized in the generalized evidence paper). We also add the handler effect tag (htagstd/core/hnd/htag: ((E, V) -> V) -> V<h>) (for dynamic lookup), and the evidence vector of the answer context where the handler was defind (evv<e,r>) (so we can execute operations in-place using the evidence vector at the point where they were defined).

• Each operation definition in a handler is called a clause. For a one argument operation, we have:

  abstract value type clause1<a,b,h,e::E,r>
    Clause1( clause: (marker<e,r>, ev<h>, a) -> e b )
  abstract value type clause1std/core/hnd/clause1: (V, V, (E, V) -> V, E, V) -> V<a,b,h,e::E,r>
    Clause1( clause: (marker<e,r>, evstd/core/hnd/ev: ((E, V) -> V) -> V<h>, a) -> e b )
  

  defining an operation a -> b for some handler h in an answer context :<e,r>. (these are generated by the compiler from a handler definition)

• An operation is performed by a rank-2 function: fun perform1( ev : evstd/core/hnd/ev: ((E, V) -> V) -> V<h>, select-op : (forall<e1,r> h<e1,r> -> clause1std/core/hnd/clause1: (V, V, (E, V) -> V, E, V) -> V<a,b,h,e1,r>), x : a ) : e b where we can call an operation given evidence for a handler evstd/core/hnd/ev: ((E, V) -> V) -> V<h> together with a polymorphic field selection function that for any handler h in any answer context, returns its clause. It is defined as:

  match ev
      Ev(_tag,m,h,_answ) -> match select-op(h)  // for an abstract `:<e1,r>`
        Clause1(f) -> f(m,ev,x)
  match ev
      Ev(_tag,m,h,_answ) -> match select-op(h)  // for an abstract `:<e1,r>`
           Clause1(f) -> f(m,ev,x)
  

• Each clause definition can now determine to fully yield to the handler, or be tail-resumptive etc. (that is, this is determined at the handler definition site, not the call site, and generated by the compiler) For example, we could be most general (ctl) and yield back to the marker (where the handler was defined in the call-stack) (with a function that receives the continuation/resumption k):

  Clause1( fn(m,ev,x) yield-to(m, fn(k) op(k,x) ))
  Clause1( fn(m,ev,x) yield-to(m, fn(k) op(k,x) ))
  

  or be super efficient and directly call the (tail-resumptive) operation in-place (fun):

  Clause1( fn(m,ev,x) op(x) )
  Clause1( fn(m,ev,x) op(x) )
  

  and various variants in-between. The last definition is unsafe for example if the (user defined) op invokes operations itself as the evidence vector should be the one as defined at the handler site. So, we norally use instead:

  Clause1( fn(m,ev,x) under1(ev,op,x) )
  Clause1( fn(m,ev,x) under1(ev,op,x) )
  

  where under1 uses the evidence vector (hevv) stored in the evidence ev to execute op(x) under. (this is also explained in detail in the generalized evidence paper).