Abstract
We compare the expressive power of three programming abstractions for userdefined computational effects: Plotkin and Pretnar's effect handlers, Filinski's monadic reflection, and delimited control without answertypemodification. This comparison allows a precise discussion about the relative expressiveness of each programming abstraction. It also demonstrates the sensitivity of the relative expressiveness of userdefined effects to seemingly orthogonal language features.
We present three calculi, one per abstraction, extending Levy's callbypushvalue. For each calculus, we present syntax, operational semantics, a natural typeandeffect system, and, for effect handlers and monadic reflection, a settheoretic denotational semantics. We establish their basic metatheoretic properties: safety, termination, and, where applicable, soundness and adequacy. Using Felleisen's notion of a macro translation, we show that these abstractions can macroexpress each other, and show which translations preserve typeability. We use the adequate finitary settheoretic denotational semantics for the monadic calculus to show that effect handlers cannot be macroexpressed while preserving typeability either by monadic reflection or by delimited control. Our argument fails with simple changes to the type system such as polymorphism and inductive types. We supplement our development with a mechanised Abella formalisation.
We present three calculi, one per abstraction, extending Levy's callbypushvalue. For each calculus, we present syntax, operational semantics, a natural typeandeffect system, and, for effect handlers and monadic reflection, a settheoretic denotational semantics. We establish their basic metatheoretic properties: safety, termination, and, where applicable, soundness and adequacy. Using Felleisen's notion of a macro translation, we show that these abstractions can macroexpress each other, and show which translations preserve typeability. We use the adequate finitary settheoretic denotational semantics for the monadic calculus to show that effect handlers cannot be macroexpressed while preserving typeability either by monadic reflection or by delimited control. Our argument fails with simple changes to the type system such as polymorphism and inductive types. We supplement our development with a mechanised Abella formalisation.
Original language  English 

Article number  13 
Journal  Proceedings of the ACM on Programming Languages 
Volume  1 
Issue number  ICFP 
Early online date  29 Aug 2017 
DOIs  
Publication status  Published  Sep 2017 
Fingerprint Dive into the research topics of 'On the expressive power of userdefined effects: effect handlers, monadic reflection, delimited control'. Together they form a unique fingerprint.
Profiles

Samuel Lindley
 School of Mathematical & Computer Sciences  Associate Professor
 School of Mathematical & Computer Sciences, Computer Science  Associate Professor
Person: Academic (Research & Teaching)