research-article

Open access

Hefty Algebras: Modular Elaboration of Higher-Order Algebraic Effects

Authors:

Casper Bach Poulsen,

Cas van der RestAuthors Info & Claims

Proceedings of the ACM on Programming Languages, Volume 7, Issue POPL

Article No.: 62, Pages 1801 - 1831

https://doi.org/10.1145/3571255

Published: 11 January 2023 Publication History

Abstract

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.

References

[1]

Michael Gordon Abbott, Thorsten Altenkirch, and Neil Ghani. 2003. Categories of Containers. In 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, Andrew D. Gordon (Ed.) (Lecture Notes in Computer Science, Vol. 2620). Springer, 23–38. isbn:3-540-00897-7 https://doi.org/10.1007/3-540-36576-1_2

[2]

Michael Gordon Abbott, Thorsten Altenkirch, and Neil Ghani. 2005. Containers: Constructing strictly positive types. Theor. Comput. Sci., 342, 1 (2005), 3–27. https://doi.org/10.1016/j.tcs.2005.06.002

Digital Library

[3]

Michael A. Arbib and Ernest G. Manes. 1975. Arrows, Structures, and Functors: The Categorical Imperative. Academic Press.

[4]

Steve Awodey. 2010. Category Theory (2nd ed.). Oxford University Press, Inc., USA. isbn:0199237182

[5]

Casper Bach Poulsen and Jaro Reinders. 2023. Hefty Algebras: Modular Elaboration of Higher-Order Algebraic Effects – Artifact. https://doi.org/10.5281/zenodo.7315899

Digital Library

[6]

Andrej Bauer and Matija Pretnar. 2015. Programming with algebraic effects and handlers. J. Log. Algebraic Methods Program., 84, 1 (2015), 108–123. https://doi.org/10.1016/j.jlamp.2014.02.001

[7]

Dariusz Biernacki, Maciej Piróg, Piotr Polesiuk, and Filip Sieczkowski. 2018. Handle with care: relational interpretation of algebraic effects and handlers. Proc. ACM Program. Lang., 2, POPL (2018), 8:1–8:30. https://doi.org/10.1145/3158096

Digital Library

[8]

Richard S. Bird and Ross Paterson. 1999. Generalised folds for nested datatypes. Formal Aspects Comput., 11, 2 (1999), 200–222. https://doi.org/10.1007/s001650050047

Digital Library

[9]

Jonathan Immanuel Brachthäuser, Philipp Schuster, and Klaus Ostermann. 2020. Effects as capabilities: effect handlers and lightweight effect polymorphism. Proc. ACM Program. Lang., 4, OOPSLA (2020), 126:1–126:30. https://doi.org/10.1145/3428194

Digital Library

[10]

Edwin C. Brady. 2013. Idris, a general-purpose dependently typed programming language: Design and implementation. J. Funct. Program., 23, 5 (2013), 552–593. https://doi.org/10.1017/S095679681300018X

[11]

Edwin C. Brady. 2013. Programming and reasoning with algebraic effects and dependent types. 133–144. isbn:978-1-4503-2326-0 https://doi.org/10.1145/2500365.2500581

Digital Library

[12]

2017. Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017, Giuseppe Castagna and Andrew D. Gordon (Eds.). ACM. isbn:978-1-4503-4660-3 https://doi.org/10.1145/3009837

Digital Library

[13]

Pietro Cenciarelli and Eugenio Moggi. 1993. A syntactic approach to modularity in denotational semantics.

[14]

Koen Claessen. 1999. A Poor Man’s Concurrency Monad. J. Funct. Program., 9, 3 (1999), 313–323. https://doi.org/10.1017/s0956796899003342

Digital Library

[15]

Benjamin Delaware, Bruno C. d. S. Oliveira, and Tom Schrijvers. 2013. Meta-theory à la carte. In The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’13, Rome, Italy - January 23 - 25, 2013, Roberto Giacobazzi and Radhia Cousot (Eds.). ACM, 207–218. https://doi.org/10.1145/2429069.2429094

Digital Library

[16]

Andrzej Filinski. 1999. Representing Layered Monads. In POPL ’99, Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Antonio, TX, USA, January 20-22, 1999, Andrew W. Appel and Alex Aiken (Eds.). ACM, 175–188. isbn:1-58113-095-3 https://doi.org/10.1145/292540.292557

Digital Library

[17]

Marcelo P. Fiore and Sam Staton. 2014. Substitution, jumps, and algebraic effects. In Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS ’14, Vienna, Austria, July 14 - 18, 2014, Thomas A. Henzinger and Dale Miller (Eds.). ACM, 41:1–41:10. isbn:978-1-4503-2886-9 https://doi.org/10.1145/2603088.2603163

Digital Library

[18]

Peter G. Hancock and Anton Setzer. 2000. Interactive Programs in Dependent Type Theory. In Computer Science Logic, 14th Annual Conference of the EACSL, Fischbachau, Germany, August 21-26, 2000, Proceedings, Peter Clote and Helmut Schwichtenberg (Eds.) (Lecture Notes in Computer Science, Vol. 1862). Springer, 317–331. https://doi.org/10.1007/3-540-44622-2_21

[19]

Mauro Jaskelioff. 2008. Monatron: An Extensible Monad Transformer Library. In Implementation and Application of Functional Languages - 20th International Symposium, IFL 2008, Hatfield, UK, September 10-12, 2008. Revised Selected Papers, Sven-Bodo Scholz and Olaf Chitil (Eds.) (Lecture Notes in Computer Science, Vol. 5836). Springer, 233–248. isbn:978-3-642-24451-3 https://doi.org/10.1007/978-3-642-24452-0_13

[20]

Mark P. Jones. 1995. Functional Programming with Overloading and Higher-Order Polymorphism. In Advanced Functional Programming, First International Spring School on Advanced Functional Programming Techniques, Båstad, Sweden, May 24-30, 1995, Tutorial Text, Johan Jeuring and Erik Meijer (Eds.) (Lecture Notes in Computer Science, Vol. 925). Springer, 97–136. isbn:3-540-59451-5 https://doi.org/10.1007/3-540-59451-5_4

[21]

Mark P. Jones and Luc Duponcheel. 1993. Composing Monads. Yale University, New Haven, Connecticut, USA. http://web.cecs.pdx.edu/~mpj/pubs/RR-1004.pdf

[22]

Ohad Kammar, Sam Lindley, and Nicolas Oury. 2013. Handlers in action. 145–158. isbn:978-1-4503-2326-0 https://doi.org/10.1145/2500365.2500590

Digital Library

[23]

Oleg Kiselyov and Hiromi Ishii. 2015. Freer monads, more extensible effects. In Proceedings of the 8th ACM SIGPLAN Symposium on Haskell, Haskell 2015, Vancouver, BC, Canada, September 3-4, 2015, Ben Lippmeier (Ed.). ACM, 94–105. isbn:978-1-4503-3808-0 https://doi.org/10.1145/2804302.2804319

Digital Library

[24]

Daan Leijen. 2017. Type directed compilation of row-typed algebraic effects. 486–499. isbn:978-1-4503-4660-3 https://doi.org/10.1145/3009837.3009872

Digital Library

[25]

Paul Blain Levy. 2006. Call-by-push-value: Decomposing call-by-value and call-by-name. High. Order Symb. Comput., 19, 4 (2006), 377–414. https://doi.org/10.1007/s10990-006-0480-6

Digital Library

[26]

Sheng Liang, Paul Hudak, and Mark P. Jones. 1995. Monad Transformers and Modular Interpreters. In Conference Record of POPL’95: 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Francisco, California, USA, January 23-25, 1995, Ron K. Cytron and Peter Lee (Eds.). ACM Press, 333–343. isbn:0-89791-692-1 https://doi.org/10.1145/199448.199528

Digital Library

[27]

Sam Lindley, Conor McBride, and Craig McLaughlin. 2017. Do be do be do. 500–514. isbn:978-1-4503-4660-3 https://doi.org/10.1145/3009837.3009897

Digital Library

[28]

Per Martin-Löf. 1984. Intuitionistic type theory (Studies in proof theory, Vol. 1). Bibliopolis. isbn:978-88-7088-228-5

[29]

Erik Meijer, Maarten M. Fokkinga, and Ross Paterson. 1991. Functional Programming with Bananas, Lenses, Envelopes and Barbed Wire. In Functional Programming Languages and Computer Architecture, 5th ACM Conference, Cambridge, MA, USA, August 26-30, 1991, Proceedings, John Hughes (Ed.) (Lecture Notes in Computer Science, Vol. 523). Springer, 124–144. https://doi.org/10.1007/3540543961_7

[30]

Eugenio Moggi. 1989. An Abstract View of Programming Languages. Edinburgh University, Department of Computer Science.

[31]

Eugenio Moggi. 1989. Computational Lambda-Calculus and Monads. In Proceedings of the Fourth Annual Symposium on Logic in Computer Science (LICS ’89), Pacific Grove, California, USA, June 5-8, 1989. IEEE Computer Society, 14–23. https://doi.org/10.1109/LICS.1989.39155

[32]

J. Garrett Morris and James McKinna. 2019. Abstracting extensible data types: or, rows by any other name. Proc. ACM Program. Lang., 3, POPL (2019), 12:1–12:28. https://doi.org/10.1145/3290325

Digital Library

[33]

2013. ACM SIGPLAN International Conference on Functional Programming, ICFP’13, Boston, MA, USA - September 25 - 27, 2013, Greg Morrisett and Tarmo Uustalu (Eds.). ACM. isbn:978-1-4503-2326-0 https://doi.org/10.1145/2500365

Digital Library

[34]

Peter D. Mosses. 2004. Modular structural operational semantics. J. Log. Algebraic Methods Program., 60-61 (2004), 195–228. https://doi.org/10.1016/j.jlap.2004.03.008

[35]

Frank Pfenning and Conal Elliott. 1988. Higher-Order Abstract Syntax. In Proceedings of the ACM SIGPLAN’88 Conference on Programming Language Design and Implementation (PLDI), Atlanta, Georgia, USA, June 22-24, 1988, Richard L. Wexelblat (Ed.). ACM, 199–208. isbn:0-89791-269-1 https://doi.org/10.1145/53990.54010

Digital Library

[36]

Benjamin C. Pierce. 1991. Basic category theory for computer scientists. MIT Press. isbn:978-0-262-66071-6

Digital Library

[37]

Maciej Piróg and Jeremy Gibbons. 2014. The Coinductive Resumption Monad. In Proceedings of the 30th Conference on the Mathematical Foundations of Programming Semantics, MFPS 2014, Ithaca, NY, USA, June 12-15, 2014, Bart Jacobs, Alexandra Silva, and Sam Staton (Eds.) (Electronic Notes in Theoretical Computer Science, Vol. 308). Elsevier, 273–288. https://doi.org/10.1016/j.entcs.2014.10.015

Digital Library

[38]

Maciej Piróg, Tom Schrijvers, Nicolas Wu, and Mauro Jaskelioff. 2018. Syntax and Semantics for Operations with Scopes. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018, Anuj Dawar and Erich Grädel (Eds.). ACM, 809–818. https://doi.org/10.1145/3209108.3209166

Digital Library

[39]

Gordon D. Plotkin. 2004. A structural approach to operational semantics. J. Log. Algebraic Methods Program., 60-61 (2004), 17–139.

[40]

Gordon D. Plotkin and John Power. 2002. Notions of Computation Determine Monads. In Foundations of Software Science and Computation Structures, 5th International Conference, FOSSACS 2002. Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2002 Grenoble, France, April 8-12, 2002, Proceedings, Mogens Nielsen and Uffe Engberg (Eds.) (Lecture Notes in Computer Science, Vol. 2303). Springer, 342–356. isbn:3-540-43366-X https://doi.org/10.1007/3-540-45931-6_24

[41]

Gordon D. Plotkin and John Power. 2003. Algebraic Operations and Generic Effects. Appl. Categorical Struct., 11, 1 (2003), 69–94. https://doi.org/10.1023/A:1023064908962

[42]

Gordon D. Plotkin and Matija Pretnar. 2009. Handlers of Algebraic Effects. In Programming Languages and Systems, 18th European Symposium on Programming, ESOP 2009, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, York, UK, March 22-29, 2009. Proceedings, Giuseppe Castagna (Ed.) (Lecture Notes in Computer Science, Vol. 5502). Springer, 80–94. isbn:978-3-642-00589-3 https://doi.org/10.1007/978-3-642-00590-9_7

Digital Library

[43]

Matija Pretnar. 2015. An Introduction to Algebraic Effects and Handlers. Invited tutorial paper. In The 31st Conference on the Mathematical Foundations of Programming Semantics, MFPS 2015, Nijmegen, The Netherlands, June 22-25, 2015, Dan R. Ghica (Ed.) (Electronic Notes in Theoretical Computer Science, Vol. 319). Elsevier, 19–35. https://doi.org/10.1016/j.entcs.2015.12.003

Digital Library

[44]

Grigore Rosu and Traian-Florin Serbanuta. 2010. An overview of the K semantic framework. J. Log. Algebraic Methods Program., 79, 6 (2010), 397–434. https://doi.org/10.1016/j.jlap.2010.03.012

[45]

David Schmidt. 1986. Denotational Semantics. Allyn and Bacon.

[46]

Tom Schrijvers, Maciej Piróg, Nicolas Wu, and Mauro Jaskelioff. 2019. Monad transformers and modular algebraic effects: what binds them together. In Proceedings of the 12th ACM SIGPLAN International Symposium on Haskell, Haskell@ICFP 2019, Berlin, Germany, August 18-23, 2019, Richard A. Eisenberg (Ed.). ACM, 98–113. isbn:978-1-4503-6813-1 https://doi.org/10.1145/3331545.3342595

Digital Library

[47]

Tom Schrijvers, Nicolas Wu, Benoit Desouter, and Bart Demoen. 2014. Heuristics Entwined with Handlers Combined: From Functional Specification to Logic Programming Implementation. In Proceedings of the 16th International Symposium on Principles and Practice of Declarative Programming, Kent, Canterbury, United Kingdom, September 8-10, 2014, Olaf Chitil, Andy King, and Olivier Danvy (Eds.). ACM, 259–270. isbn:978-1-4503-2947-7 https://doi.org/10.1145/2643135.2643145

Digital Library

[48]

Neil Sculthorpe, Paolo Torrini, and Peter D. Mosses. 2015. A Modular Structural Operational Semantics for Delimited Continuations. In Proceedings of the Workshop on Continuations, WoC 2016, London, UK, April 12th 2015, Olivier Danvy and Ugo de’Liguoro (Eds.) (EPTCS, Vol. 212). 63–80. https://doi.org/10.4204/EPTCS.212.5

[49]

Guy L. Steele Jr. 1994. Building Interpreters by Composing Monads. In Conference Record of POPL’94: 21st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Portland, Oregon, USA, January 17-21, 1994, Hans-Juergen Boehm, Bernard Lang, and Daniel M. Yellin (Eds.). ACM Press, 472–492. isbn:0-89791-636-0 https://doi.org/10.1145/174675.178068

Digital Library

[50]

Wouter Swierstra. 2008. Data types à la carte. J. Funct. Program., 18, 4 (2008), 423–436. https://doi.org/10.1017/S0956796808006758

Digital Library

[51]

Walid Taha and Tim Sheard. 2000. MetaML and multi-stage programming with explicit annotations. Theor. Comput. Sci., 248, 1-2 (2000), 211–242. https://doi.org/10.1016/S0304-3975(00)00053-0

Digital Library

[52]

Hayo Thielecke. 1997. Categorical Structure of Continuation Passing Style. Ph. D. Dissertation. University of Edinburgh.

[53]

Birthe van den Berg, Tom Schrijvers, Casper Bach Poulsen, and Nicolas Wu. 2021. Latent Effects for Reusable Language Components. In Programming Languages and Systems - 19th Asian Symposium, APLAS 2021, Chicago, IL, USA, October 17-18, 2021, Proceedings, Hakjoo Oh (Ed.) (Lecture Notes in Computer Science, Vol. 13008). Springer, 182–201. isbn:978-3-030-89050-6 https://doi.org/10.1007/978-3-030-89051-3_11

Digital Library

[54]

Philip Wadler. 1992. The Essence of Functional Programming. In Conference Record of the Nineteenth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Albuquerque, New Mexico, USA, January 19-22, 1992, Ravi Sethi (Ed.). ACM Press, 1–14. isbn:0-89791-453-8 https://doi.org/10.1145/143165.143169

Digital Library

[55]

Nicolas Wu, Tom Schrijvers, and Ralf Hinze. 2014. Effect handlers in scope. In Proceedings of the 2014 ACM SIGPLAN symposium on Haskell, Gothenburg, Sweden, September 4-5, 2014, Wouter Swierstra (Ed.). ACM, 1–12. isbn:978-1-4503-3041-1 https://doi.org/10.1145/2633357.2633358

Digital Library

[56]

Zhixuan Yang, Marco Paviotti, Nicolas Wu, Birthe van den Berg, and Tom Schrijvers. 2022. Structured Handling of Scoped Effects. In Programming Languages and Systems - 31st European Symposium on Programming, ESOP 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings, Ilya Sergey (Ed.) (Lecture Notes in Computer Science, Vol. 13240). Springer, 462–491. isbn:978-3-030-99335-1 https://doi.org/10.1007/978-3-030-99336-8_17

Digital Library

[57]

Yizhou Zhang and Andrew C. Myers. 2019. Abstraction-safe effect handlers via tunneling. Proc. ACM Program. Lang., 3, POPL (2019), 5:1–5:29. https://doi.org/10.1145/3290318

Digital Library

Cited By

Bunkenburg NWu NVazou NMorris J(2024)Making a Curry Interpreter using Effects and HandlersProceedings of the 17th ACM SIGPLAN International Haskell Symposium10.1145/3677999.3678279(68-82)Online publication date: 29-Aug-2024
https://dl.acm.org/doi/10.1145/3677999.3678279
Frumin DTimany ABirkedal L(2024)Modular Denotational Semantics for Effects with Guarded Interaction TreesProceedings of the ACM on Programming Languages10.1145/36328548:POPL(332-361)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632854
van den Berg BSchrijvers T(2024)A framework for higher-order effects & handlersScience of Computer Programming10.1016/j.scico.2024.103086234:COnline publication date: 25-Jun-2024
https://dl.acm.org/doi/10.1016/j.scico.2024.103086
Show More Cited By

Index Terms

Hefty Algebras: Modular Elaboration of Higher-Order Algebraic Effects
1. Software and its engineering
  1. Software notations and tools
    1. Formal language definitions
      1. Semantics
2. Theory of computation
  1. Semantics and reasoning

Recommendations

Handling fibred algebraic effects

We study algebraic computational effects and their handlers in the dependently typed setting. We describe computational effects using a generalisation of Plotkin and Pretnar's effect theories, whose dependently typed operations allow us to capture ...
Algebraic effects and effect handlers for idioms and arrows
WGP '14: Proceedings of the 10th ACM SIGPLAN workshop on Generic programming

Plotkin and Power's algebraic effects combined with Plotkin and Pretnar's effect handlers provide a foundation for modular programming with effects. We present a generalisation of algebraic effects and effect handlers to support other kinds of effectful ...
Contextual modal types for algebraic effects and handlers

Programming languages with algebraic effects often track the computations’ effects using type-and-effect systems. In this paper, we propose to view an algebraic effect theory of a computation as a variable context; consequently, we propose to track ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Proceedings of the ACM on Programming Languages

Proceedings of the ACM on Programming Languages Volume 7, Issue POPL

January 2023

2196 pages

EISSN:2475-1421

DOI:10.1145/3554308

Editor:

Issue’s Table of Contents

Copyright © 2023 Owner/Author.

This work is licensed under a Creative Commons Attribution 4.0 International License.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 11 January 2023

Published in PACMPL Volume 7, Issue POPL

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Badges

Author Tags

Qualifiers

Research-article

Funding Sources

NWO

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

5
Total Citations
View Citations
1,108
Total Downloads

Downloads (Last 12 months)607
Downloads (Last 6 weeks)130

Reflects downloads up to 16 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Bunkenburg NWu NVazou NMorris J(2024)Making a Curry Interpreter using Effects and HandlersProceedings of the 17th ACM SIGPLAN International Haskell Symposium10.1145/3677999.3678279(68-82)Online publication date: 29-Aug-2024
https://dl.acm.org/doi/10.1145/3677999.3678279
Frumin DTimany ABirkedal L(2024)Modular Denotational Semantics for Effects with Guarded Interaction TreesProceedings of the ACM on Programming Languages10.1145/36328548:POPL(332-361)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632854
van den Berg BSchrijvers T(2024)A framework for higher-order effects & handlersScience of Computer Programming10.1016/j.scico.2024.103086234:COnline publication date: 25-Jun-2024
https://dl.acm.org/doi/10.1016/j.scico.2024.103086
Yang ZWu N(2023)Modular Models of Monoids with OperationsProceedings of the ACM on Programming Languages10.1145/36078507:ICFP(566-603)Online publication date: 31-Aug-2023
https://dl.acm.org/doi/10.1145/3607850
van der Rest CPoulsen C(2023)Types and Semantics for Extensible Data TypesProgramming Languages and Systems10.1007/978-981-99-8311-7_3(46-66)Online publication date: 26-Nov-2023
https://dl.acm.org/doi/10.1007/978-981-99-8311-7_3

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

Media

Figures

Other

Tables

View Issue’s Table of Contents