University of Cambridge > Talks.cam > Logic and Semantics Seminar (Computer Laboratory) > On the expressive power of user-defined effects: effect handlers, monadic reflection, delimited control

On the expressive power of user-defined effects: effect handlers, monadic reflection, delimited control

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact Dominic Mulligan.

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)

This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

© 2006-2020 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity