Effect Handlers, Evidently

See the ICFP’2020 talk on youtube (opens in new tab)

Algebraic effect handlers are a powerful way to incorporate effects in a
programming language. Sometimes perhaps even _too_ powerful. In this
article we define a restriction of general effect handlers with _scoped
resumptions_. We argue one can still express all important effects, while
improving reasoning about effect handlers. Using the newly gained
guarantees, we define a sound and coherent evidence translation for effect handlers,
which directly passes the handlers as evidence to each operation. We
prove full soundness and coherence of the translation into plain lambda calculus. The
evidence in turn enables efficient implementations of effect operations;
in particular, we show we can execute tail-resumptive operations _in
place_ (without needing to capture the evaluation context), and how we
can replace the runtime search for a handler by indexing with a constant
offset.