Monads are the de-facto mechanism for adding user-defined computational effects to programming languages. Support for monads has been developed in general-purpose statically-typed functional programming languages such as Haskell and OCaml, proof assistants such as Coq, and other verification tools such as F-star. Algebraic effects and handlers are a recently developed programming abstraction that allows programmers to define and program with custom effects using a specific delimited-control structure. This control structure has straightforward type-system, computational intuition, operational and denotational semantics, and reasoning principles.
Our goal is to compare the expressive power of programming constructs facilitating user-defined effects. We consider a calculus of effect handlers, Filinski’s calculus of monadic reflection, which encapsulate user-defined monads as a programmable abstraction, and a calculus of the standard delimited control operators shift-zero and reset. We compare the calculi using Felleisen’s notion of macro translations. When we ignore the natural type systems associated with each calculus, each pair of abstractions is macro inter-translateable, but this translation does not preserve typability. We present preliminary results regarding the non-existence of typability-preserving macro-translations, and extensions to the type system that preserve typability.
Joint work with Yannick Forster, Sam Lindley, and Matija Pretnar.