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

• Sam Lindley, University of Edinburgh
• Friday 01 December 2017, 14:00-15:00
• FW26.

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.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Computing and Mathematics
• Department of Computer Science and Technology talks and seminars
• FW26
• Interested Talks
• Logic and Semantics Seminar (Computer Laboratory)
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31
• yk373's list

Note that ex-directory lists are not shown.