## On the Expressive Power of Algebraic Effects and Handlers

*Talk by
Ohad Kammar
(University of Oxford) *

Time:
17:00-17:30

Slides

### Abstract

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.