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 条
  • [31] HIGHER-ORDER INSTANTON EFFECTS
    LEVINE, H
    YAFFE, LG
    PHYSICAL REVIEW D, 1979, 19 (04): : 1225 - 1242
  • [32] HIGHER-ORDER ASYNCHRONOUS EFFECTS
    Ahman, Danel
    Pretnar, Matija
    LOGICAL METHODS IN COMPUTER SCIENCE, 2024, 20 (03)
  • [33] A Modular Semantics for Higher-Order Declarative Programming with Constraints
    del Vado Virseda, Rafael
    Perez Morente, Fernando
    PPDP 11 - PROCEEDINGS OF THE 2011 SYMPOSIUM ON PRINCIPLES AND PRACTICES OF DECLARATIVE PROGRAMMING, 2011, : 41 - 51
  • [34] Modular, Higher-Order Cardinality Analysis in Theory and Practice
    Sergey, Ilya
    Vytiniotis, Dimitrios
    Jones, Simon Peyton
    ACM SIGPLAN NOTICES, 2014, 49 (01) : 335 - 347
  • [35] A Modular Theory of Object Orientation in Higher-Order UTP
    Zeyda, Frank
    Santos, Thiago
    Cavalcanti, Ana
    Sampaio, Augusto
    FM 2014: FORMAL METHODS, 2014, 8442 : 627 - 642
  • [36] IMAGES OF HIGHER-ORDER DIFFERENTIAL OPERATORS OF POLYNOMIAL ALGEBRAS
    Liu, Dayan
    Sun, Xiaosong
    BULLETIN OF THE AUSTRALIAN MATHEMATICAL SOCIETY, 2017, 96 (02) : 205 - 211
  • [37] Higher-order Algebras and Coalgebras from Parameterized Endofunctors
    Kim, Jiho
    ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2010, 264 (02) : 141 - 154
  • [38] A completeness theorem for the expressive power of higher-order algebraic specifications
    Meinke, K
    JOURNAL OF COMPUTER AND SYSTEM SCIENCES, 1997, 54 (03) : 502 - 519
  • [39] SYSTEM DESCRIPTION OF LAMBDALG - A HIGHER-ORDER ALGEBRAIC SPECIFICATION LANGUAGE
    GUI, YX
    OKADA, M
    LOGIC PROGRAMMING AND AUTOMATED REASONING, 1993, 698 : 354 - 356
  • [40] Algebraic higher-order nets: Graphs and Petri nets as tokens
    Hoffmann, K
    Mossakowski, T
    RECENT TRENDS IN ALGEBRAIC DEVELOPMENT TECHNIQUES, 2003, 2755 : 253 - 267