Hefty Algebras: Modular Elaboration of Higher-Order Algebraic Effects

Research output: Contribution to journalArticleScientificpeer-review

6 Downloads (Pure)


Algebraic effects and handlers is an increasingly popular approach to programming with effects. An attraction of the approach is its modularity: effectful programs are written against an interface of declared operations, which allows the implementation of these operations to be defined and refined without changing or recompiling programs written against the interface. However, higher-order operations (i.e., operations that take computations as arguments) break this modularity. While it is possible to encode higher-order operations by elaborating them into more primitive algebraic effects and handlers, such elaborations are typically not modular. In particular, operations defined by elaboration are typically not a part of any effect interface, so we cannot define and refine their implementation without changing or recompiling programs. To resolve this problem, a recent line of research focuses on developing new and improved effect handlers. In this paper we present a (surprisingly) simple alternative solution to the modularity problem with higher-order operations: we modularize the previously non-modular elaborations commonly used to encode higher-order operations. Our solution is as expressive as the state of the art in effects and handlers.

Original languageEnglish
Pages (from-to)1801-1831
Number of pages31
JournalProceedings of the ACM on Programming Languages
Publication statusPublished - 2023


  • Agda
  • Algebraic Effects
  • Dependent Types
  • Modularity
  • Reuse


Dive into the research topics of 'Hefty Algebras: Modular Elaboration of Higher-Order Algebraic Effects'. Together they form a unique fingerprint.

Cite this