Effect Handlers, Evidently (ICFP 2020)

More info about this talk: icfp20.sigplan.org/details/ic...
Authors:
Ningning Xie, Microsoft Research, USA (presenting)
Jonathan Immanuel Brachthäuser, University of Tübingen, Germany
Daniel Hillerström, The University of Edinburgh
Philipp Schuster, University of Tübingen, Germany
Abstract:
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 local 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.
This is an official ICFP 2020 talk video edited from an author-submitted video. Video captions supported by Jane Street. On a desktop browser, you can view captions without overlapping the video by clicking the three dots to the right of “Save” and clicking “Open transcript”.