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

来源：

Proceedings of the ACM on Programming Languages | 2023年 / 7卷

关键词：

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

共 57 条

[1]

Abbott M.G., Altenkirch T., Ghani N., Categories of Containers, Foundations of Software Science and Computational Structures, 6th International Conference, FOSSACS 2003 Held as Part of the Joint European Conference on Theory and Practice of Software, ETAPS 2003, Warsaw, Poland, April 7-11, 2003, Proceedings (Lecture Notes in Computer Science, Vol. 2620), pp. 23-38, (2003)

[2]

Abbott M.G., Altenkirch T., Ghani N., Containers: Constructing strictly positive types, Theor. Comput. Sci., 342, 1, pp. 3-27, (2005)

[3]

Arbib M.A., Manes E.G., Arrows, Structures, and Functors: The Categorical Imperative, (1975)

[4]

Awodey S., Category Theory, (2010)

[5]

Poulsen C.B., Reinders J., Hefty Algebras: Modular Elaboration of Higher-Order Algebraic Effects - Artifact, (2023)

[6]

Bauer A., Pretnar M., Programming with algebraic effects and handlers, J. Log. Algebraic Methods Program., 84, 1, pp. 108-123, (2015)

[7]

Biernacki D., Pirog M., Polesiuk P., Sieczkowski F., Handle with care: relational interpretation of algebraic effects and handlers, Proc. ACM Program. Lang., 2, pp. 81-830, (2018)

[8]

Bird R.S., Paterson R., Generalised folds for nested datatypes, Formal Aspects Comput., 11, 2, pp. 200-222, (1999)

[9]

Brachthauser J.I., Schuster P., Ostermann K., Effects as capabilities: effect handlers and lightweight effect polymorphism, Proc. ACM Program. Lang., 4, pp. 1261-12630, (2020)

[10]

Brady E.C., Idris, a general-purpose dependently typed programming language: Design and implementation, J. Funct. Program., 23, 5, pp. 552-593, (2013)

← 1 2 3 4 5 6 →