Hefty Algebras: Modular Elaboration of Higher-Order Algebraic Effects

被引:0
|
作者
Bach Poulsen C. [1 ]
Van Der Rest C. [1 ]
机构
[1] Delft University of Technology, Netherlands
关键词
Agda; Algebraic Effects; Dependent Types; Modularity; Reuse;
D O I
10.1145/3571255
中图分类号
学科分类号
摘要
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. © 2023 Owner/Author.
引用
收藏
页码:1801 / 1831
页数:30
相关论文
共 50 条