Abstract

We compare the expressive power of three programming abstractions for user-defined computational effects: Plotkin and Pretnar’s effect handlers, Filinski’s monadic reflection, and delimited control. This comparison allows a precise discussion about the relative expressiveness of each programming abstraction. It also demonstrates the sensitivity of the relative expressiveness of user-defined effects to seemingly orthogonal language features.

We present each notion as an extension of a simply-typed core lambda-calculus with an effect type system. Using Felleisen’s notion of a macro translation, we show that these abstractions can macro-express each other, providing we disregard types. Alas, not all of the translations are typeability-preserving. We show that if we add suitable notions of polymorphism to the core calculus and the extensions then the translations can be adapted to preserve typeability.

(based on joint work with Yannick Forster, Ohad Kammar, and Matija Pretnar)

If I have time I will also talk about how the translation of effect handlers into delimited control can be used to synthesise a CPS translation for effect handlers. Such a CPS translation is used in practice in the implementation of the Links web programming language in order to compile effect handlers to JavaScript.

(based on joint work with Bob Atkey, Daniel Hillerström, and KC Sivaramakrishnan)