Hefty algebras: Modular elaboration of higher-order effects

Abstract

Algebraic effects and handlers is an increasingly popular paradigm for programming with effects. A key benefit is modularity: programs with effects are defined against an interface of operations, allowing the implementation of effects to be defined and refined without changing or recompiling programs. The behavior of effects is specified using equational theories, with equational proofs inheriting the same modularity. However, higher-order operations (that take computations as arguments) break this modularity: while they can often be encoded in terms of algebraic effects, this typically breaks modularity as operations defined this way are not encapsulated in an interface, inducing changes to programs and proofs upon refinement of the implementation. In this paper, we show that syntactic overloading is a viable solution to this modularity problem by defining hefty algebras: a formal framework that captures an overloading-based semantics of higher-order effects by defining modular elaborations from higher-order effect trees into primitive algebraic effects. We demonstrate how this approach scales to define a wide range of known higher-order effects from the literature and develop modular higher-order effect theories and modular reasoning principles that build on and extend the state of the art in modular algebraic effect theories. We formalize our contributions in Agda.