On the Expressive Power of User-Defined Effects: Effect Handlers, Monadic Reflection, Delimited Control
We compare the expressive power of three programming abstractions for user-defined computational effects: Bauer and Pretnar's effect handlers, Filinski's monadic reflection, and delimited control without answer-type-modification. 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 three calculi, one per abstraction, extending Levy's call-by-push-value. For each calculus, we present syntax, operational semantics, a natural type-and-effect system, and, for effect handlers and monadic reflection, a set-theoretic denotational semantics. We establish their basic meta-theoretic properties: safety, termination, and, where applicable, soundness and adequacy. Using Felleisen's notion of a macro translation, we show that these abstractions can macro-express each other, and show which translations preserve typeability. We use the adequate finitary set-theoretic denotational semantics for the monadic calculus to show that effect handlers cannot be macro-expressed while preserving typeability either by monadic reflection or by delimited control. We supplement our development with a mechanised Abella formalisation.
Mon 4 SepDisplayed time zone: Belfast change
16:40 - 18:10
|Abstracting Definitional Interpreters|
David Darais University of Maryland, USA, Nicholas Labich University of Maryland, USA, Phúc C. Nguyễn University of Maryland, USA, David Van Horn University of Maryland, USADOI
|On the Expressive Power of User-Defined Effects: Effect Handlers, Monadic Reflection, Delimited Control|
Yannick Forster Saarland University, Germany / University of Cambridge, UK, Ohad Kammar University of Oxford, UK, Sam Lindley University of Edinburgh, UK, Matija Pretnar University of Ljubljana, SloveniaDOI
|Imperative Functional Programs That Explain Their Work|
Wilmer Ricciotti University of Edinburgh, UK, Jan Stolarek University of Edinburgh, UK, Roly Perera University of Edinburgh, UK / University of Glasgow, UK, James Cheney University of Edinburgh, UKDOI
|Effect-Driven QuickChecking of Compilers|
Jan Midtgaard DTU, Denmark, Mathias Nygaard Justesen DTU, Denmark, Patrick Kasting DTU, Denmark, Flemming Nielson DTU, Denmark, Hanne Riis Nielson DTU, DenmarkDOI