![]() |
![]() |
Algebraic effects are computational effects that can be represented by an equational theory whose operations produce the effects at hand. The free model of this theory induces the expected computational monad for the corresponding effect. Algebraic effects include exceptions, state, nondeterminism, interactive input/output, and time, and their combinations. Exception handling, however, has so far received no algebraic treatment. We present such a treatment, in which each handler yields a model of the theory for exceptions, and each handling construct yields the homomorphism induced by the universal property of the free model. We further generalise exception handlers to arbitrary algebraic effects. The resulting programming construct includes many previously unrelated examples from both theory and practice, including relabelling and restriction in Milner's CCS, timeout, rollback, and stream redirection.
Comment: 36 pages
, 2025, On Decidable and Undecidable Extensions of Simply Typed Lambda Calculus, Proceedings of the ACM on Programming Languages, 9, POPL, pp. 1136-1166, 10.1145/3704875, https://doi.org/10.1145/3704875.
;SAM LINDLEY
;JOHN LONGLEY, 2024, Asymptotic speedup via effect handlers, Journal of Functional Programming, 34, 10.1017/s0956796824000030, https://doi.org/10.1017/s0956796824000030.
;Amin Timany
;Lars Birkedal
, 2024, Modular Denotational Semantics for Effects with Guarded Interaction Trees, Proceedings of the ACM on Programming Languages, 8, POPL, pp. 332-361, 10.1145/3632854, https://doi.org/10.1145/3632854.
;Zhixuan Yang
;Nicolas Wu
, 2024, Algebraic Effects Meet Hoare Logic in Cubical Agda, Proceedings of the ACM on Programming Languages, 8, POPL, pp. 1663-1695, 10.1145/3632898, https://doi.org/10.1145/3632898.
;Hiroshi Unno
;Taro Sekiyama
;Tachio Terauchi
, 2024, Answer Refinement Modification: Refinement Type System for Algebraic Effects and Handlers, Proceedings of the ACM on Programming Languages, 8, POPL, pp. 115-147, 10.1145/3633280, https://doi.org/10.1145/3633280.
, 2024, Type-Safe Code Generation with Algebraic Effects and Handlers, Proceedings of the 23rd ACM SIGPLAN International Conference on Generative Programming: Concepts and Experiences, pp. 53-65, 10.1145/3689484.3690731.
;Teodoro Freund;Dan R. Ghica
;Sam Lindley
, 2024, Effect Handlers for C via Coroutines, Proceedings of the ACM on Programming Languages, 8, OOPSLA2, pp. 2462-2489, 10.1145/3689798, https://doi.org/10.1145/3689798.
;Lindley, Sam
;Moss, Sean
;Staton, Sam
;Wu, Nicolas
;et al., 2024, Scoped Effects as Parameterized Algebraic Theories, Lecture notes in computer science, pp. 3-21, 10.1007/978-3-031-57262-3_1, https://doi.org/10.1007/978-3-031-57262-3_1.
;Atsushi Igarashi
, 2024, Abstracting Effect Systems for Algebraic Effect Handlers, Proceedings of the ACM on Programming Languages, 8, ICFP, pp. 455-484, 10.1145/3674641, https://doi.org/10.1145/3674641.
;Hiroshi Unno
, 2024, Higher-Order Model Checking of Effect-Handling Programs with Answer-Type Modification, Proceedings of the ACM on Programming Languages, 8, OOPSLA2, pp. 2662-2691, 10.1145/3689805, https://doi.org/10.1145/3689805.
;Matthijs I. L. Vákár
, 2024, Efficient CHAD, Proceedings of the ACM on Programming Languages, 8, POPL, pp. 1060-1088, 10.1145/3632878, https://doi.org/10.1145/3632878.
;Darius Foo
;Wei-Ngan Chin
, 2024, Specification and Verification for Unrestricted Algebraic Effects and Handling, Proceedings of the ACM on Programming Languages, 8, ICFP, pp. 909-937, 10.1145/3674656, https://doi.org/10.1145/3674656.
;TOM SCHRIJVERS
, 2023, Disjunctive Delimited Control, Theory and Practice of Logic Programming, 24, 1, pp. 110-131, 10.1017/s1471068423000029, https://doi.org/10.1017/s1471068423000029.
, 2023, When Programs Have to Watch Paint Dry, Lecture notes in computer science, pp. 1-23, 10.1007/978-3-031-30829-1_1, https://doi.org/10.1007/978-3-031-30829-1_1.
;Mateusz Pyzik
;Dariusz Biernacki
, 2023, A General Fine-Grained Reduction Theory for Effect Handlers, Proceedings of the ACM on Programming Languages, 7, ICFP, pp. 511-540, 10.1145/3607848, https://doi.org/10.1145/3607848.
;Hiroshi Unno
, 2023, Temporal Verification with Answer-Effect Modification: Dependent Temporal Type-and-Effect System with Delimited Continuations, Proceedings of the ACM on Programming Languages, 7, POPL, pp. 2079-2110, 10.1145/3571264, https://doi.org/10.1145/3571264.
;Nicolas Wu
, 2023, Modular Models of Monoids with Operations, Proceedings of the ACM on Programming Languages, 7, ICFP, pp. 566-603, 10.1145/3607850, https://doi.org/10.1145/3607850.
;Sam Lindley
;Marcos Maroñas Bravo
;Maciej Piróg
, 2022, High-level effect handlers in C++, Proceedings of the ACM on Programming Languages, 6, OOPSLA2, pp. 1639-1667, 10.1145/3563445, https://doi.org/10.1145/3563445.
;Yannick Zakowski
;Steve Zdancewic
, 2022, Formal reasoning about layered monadic interpreters, Proceedings of the ACM on Programming Languages, 6, ICFP, pp. 254-282, 10.1145/3547630, https://doi.org/10.1145/3547630.
, 2022, What You See Is What You Get: Practical Effect Handlers in Capability-Passing Style, Ernst Denert Award for Software Engineering 2020, pp. 15-43, 10.1007/978-3-030-83128-8_3.
;Roly Perera
;Meng Wang
;Nicolas Wu
, 2022, Modular probabilistic models via algebraic effects, Proceedings of the ACM on Programming Languages, 6, ICFP, pp. 381-410, 10.1145/3547635, https://doi.org/10.1145/3547635.
;Hidehiko Masuhara
;Daan Leijen
, 2022, Towards Efficient Adjustment of Effect Rows, Lecture notes in computer science, pp. 169-191, 10.1007/978-3-031-21314-4_9.
;Niels Voorneveld
, 2022, Streams of Approximations, Equivalence of Recursive Effectful Programs, Lecture notes in computer science, pp. 198-221, 10.1007/978-3-031-16912-0_8.
, 2022, Runners for Interleaving Algebraic Effects, Lecture notes in computer science, pp. 407-424, 10.1007/978-3-031-17715-6_26.
;Youyou Cong
;Kazuki Ikemori
;Daan Leijen
, 2022, First-class names for effect handlers, Proceedings of the ACM on Programming Languages, 6, OOPSLA2, pp. 30-59, 10.1145/3563289, https://doi.org/10.1145/3563289.
;Marco Paviotti
;Nicolas Wu
;Birthe van den Berg
;Tom Schrijvers
, 2022, Structured Handling of Scoped Effects, Lecture notes in computer science, pp. 462-491, 10.1007/978-3-030-99336-8_17, https://doi.org/10.1007/978-3-030-99336-8_17.
;Ningning Xie
;Leonardo de Moura
;Daan Leijen
, 2021, Perceus: garbage free reference counting with reuse, Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, pp. 96-111, 10.1145/3453483.3454032.
;Matija Pretnar
, 2021, Asynchronous effects, Proceedings of the ACM on Programming Languages, 5, POPL, pp. 1-28, 10.1145/3434305, https://doi.org/10.1145/3434305.
;Matija Pretnar
;Tom Schrijvers
, 2021, Efficient compilation of algebraic effect handlers, Proceedings of the ACM on Programming Languages, 5, OOPSLA, pp. 1-28, 10.1145/3485479, https://doi.org/10.1145/3485479.
;Maxime Amblard
;Philippe de Groote, 2021, Introducing ⦇ λ ⦈, a λ-calculus for effectful computation, 869, pp. 108-155, 10.1016/j.tcs.2021.02.038, https://inria.hal.science/hal-03200474.
, 2021, Smart Choices and the Selection Monad, 2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pp. 1-14, 10.1109/lics52264.2021.9470641.
;Niels F.W. Voorneveld
, 2021, Inductive and Coinductive Predicate Liftings for Effectful Programs, Electronic Proceedings in Theoretical Computer Science, 351, pp. 260-277, 10.4204/eptcs.351.16, https://doi.org/10.4204/eptcs.351.16.
;Aleksandar Nanevski
, 2021, Contextual modal types for algebraic effects and handlers, Proceedings of the ACM on Programming Languages, 5, ICFP, pp. 1-29, 10.1145/3473580, https://doi.org/10.1145/3473580.
;Daan Leijen
, 2021, Generalized evidence passing for effect handlers: efficient compilation of effect handlers to C, Proceedings of the ACM on Programming Languages, 5, ICFP, pp. 1-30, 10.1145/3473576, https://doi.org/10.1145/3473576.
;François Pottier
, 2021, A separation logic for effect handlers, Proceedings of the ACM on Programming Languages, 5, POPL, pp. 1-28, 10.1145/3434314, https://doi.org/10.1145/3434314.
;Norihiko Yoshida, 2021, Implementing Algebraic Effects and Handlers in Non-functional Programming Languages, 2021 IEEE Asia-Pacific Conference on Computer Science and Data Engineering (CSDE), pp. 1-6, 10.1109/csde53843.2021.9718480.
;Nicolas Wu
, 2021, Reasoning about effect interaction by fusion, Proceedings of the ACM on Programming Languages, 5, ICFP, pp. 1-29, 10.1145/3473578, https://doi.org/10.1145/3473578.
;Cezary Kaliszyk
, 2020, Mac Lane’s Comparison Theorem for the Kleisli Construction Formalized in Coq, Mathematics in Computer Science, 14, 3, pp. 533-549, 10.1007/s11786-020-00450-8, https://doi.org/10.1007/s11786-020-00450-8.
;SAM LINDLEY
;ROBERT ATKEY
, 2020, Effect handlers via generalised continuations, Journal of Functional Programming, 30, 10.1017/s0956796820000040, https://doi.org/10.1017/s0956796820000040.
;Andrej Bauer
;Danel Ahman
;Andrej Bauer
, 2020, Runners in Action, Lecture notes in computer science, pp. 29-55, 10.1007/978-3-030-44914-8_2, https://doi.org/10.1007/978-3-030-44914-8_2.
;Sam Lindley
;John Longley, 2020, Effects for efficiency: asymptotic speedup with first-class control, Proceedings of the ACM on Programming Languages, 4, ICFP, pp. 1-29, 10.1145/3408982, https://doi.org/10.1145/3408982.
;Sergueï Lenglet;Piotr Polesiuk
, 2020, A Complete Normal-Form Bisimilarity for Algebraic Effects and Handlers, Leibniz-Zentrum für Informatik (Schloss Dagstuhl), 10.4230/lipics.fscd.2020.7, https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2020.7.
;AMR HANY SALEH
;STIEN VANDERHALLEN
;TOM SCHRIJVERS
, 2020, Explicit effect subtyping, arXiv (Cornell University), 30, 10.1017/s0956796820000131, http://arxiv.org/abs/2005.13814.
;Oliver Bračevac
;Shangyin Tan;Tiark Rompf
, 2020, Compiling symbolic execution with staging and algebraic effects, Proceedings of the ACM on Programming Languages, 4, OOPSLA, pp. 1-33, 10.1145/3428232, https://doi.org/10.1145/3428232.
;PHILIPP SCHUSTER
;KLAUS OSTERMANN
, 2020, Effekt: Capability-passing style for type- and effect-safe, extensible effect handlers in Scala, Journal of Functional Programming, 30, 10.1017/s0956796820000027, https://doi.org/10.1017/s0956796820000027.
;Philipp Schuster
;Klaus Ostermann
, 2020, Effects as capabilities: effect handlers and lightweight effect polymorphism, Proceedings of the ACM on Programming Languages, 4, OOPSLA, pp. 1-30, 10.1145/3428194, https://doi.org/10.1145/3428194.
;SAM LINDLEY
;CONOR MCBRIDE
;CRAIG MCLAUGHLIN
, 2020, Doo bee doo bee doo, Journal of Functional Programming, 30, 10.1017/s0956796820000039, https://doi.org/10.1017/s0956796820000039.
;R. Kent Dybvig, 2020, Compiler and runtime support for continuation marks, Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 45-58, 10.1145/3385412.3385981.
;Daan Leijen
, 2020, Effect handlers in Haskell, evidently, Proceedings of the 13th ACM SIGPLAN International Symposium on Haskell, pp. 95-108, 10.1145/3406088.3409022.
;Jonathan Immanuel Brachthäuser
;Daniel Hillerström
;Philipp Schuster
;Daan Leijen
, 2020, Effect handlers, evidently, Proceedings of the ACM on Programming Languages, 4, ICFP, pp. 1-29, 10.1145/3408981, https://doi.org/10.1145/3408981.
;Jonathan Immanuel Brachthäuser
;Klaus Ostermann
, 2020, Compiling effect handlers in capability-passing style, Proceedings of the ACM on Programming Languages, 4, ICFP, pp. 1-28, 10.1145/3408975, https://doi.org/10.1145/3408975.
, 2020, One-Shot Algebraic Effects as Coroutines, Lecture notes in computer science, pp. 159-179, 10.1007/978-3-030-57761-2_8.
, 2020, Graded Algebraic Theories, Lecture notes in computer science, pp. 401-421, 10.1007/978-3-030-45231-5_21, https://doi.org/10.1007/978-3-030-45231-5_21.
;Exequiel Rivas
;Tarmo Uustalu
, 2020, Interaction Laws of Monads and Comonads, pp. 604-618, 10.1145/3373718.3394808.
;Niels Voorneveld
, 2020, Algebraic and Coalgebraic Perspectives on Interaction Laws, Opin vísindi (Opin vísindi), pp. 186-205, 10.1007/978-3-030-64437-6_10, https://hdl.handle.net/20.500.11815/4001.
;Takeshi Tsukada
;Atsushi Igarashi
, 2020, Signature restriction for polymorphic algebraic effects, Proceedings of the ACM on Programming Languages, 4, ICFP, pp. 1-30, 10.1145/3408999, https://doi.org/10.1145/3408999.
;Guido Salvaneschi
;Andrew C. Myers
, 2020, Handling bidirectional control flow, Proceedings of the ACM on Programming Languages, 4, OOPSLA, pp. 1-30, 10.1145/3428207, https://doi.org/10.1145/3428207.
;MATIJA PRETNAR
, 2020, Local algebraic effect theories, arXiv (Cornell University), 30, 10.1017/s0956796819000212, http://arxiv.org/abs/2005.13654.
, 2019, Behavioural Equivalence via Modalities for Algebraic Effects, ACM Transactions on Programming Languages and Systems, 42, 1, pp. 1-45, 10.1145/3363518, https://doi.org/10.1145/3363518.
;Sam Staton
, 2019, A Sound and Complete Logic for Algebraic Effects, Lecture notes in computer science, pp. 382-399, 10.1007/978-3-030-17127-8_22, https://doi.org/10.1007/978-3-030-17127-8_22.
;Maciej Piróg
;Piotr Polesiuk
;Filip Sieczkowski
, 2019, Binders by day, labels by night: effect instances via lexically scoped handlers, Proceedings of the ACM on Programming Languages, 4, POPL, pp. 1-29, 10.1145/3371116, https://doi.org/10.1145/3371116.
;Yannick Zakowski
;Paul He
;Chung-Kil Hur
;Gregory Malecha
;et al., 2019, Interaction trees: representing recursive and impure programs in Coq, Proceedings of the ACM on Programming Languages, 4, POPL, pp. 1-32, 10.1145/3371119, https://doi.org/10.1145/3371119.
;Sam Lindley
;J. Garrett Morris
;Sára Decova, 2019, Exceptional asynchronous session types: session types without tiers, Proceedings of the ACM on Programming Languages, 3, POPL, pp. 1-29, 10.1145/3290341, https://doi.org/10.1145/3290341.
;Francesco Gavazzo
, 2019, Effectful Normal Form Bisimulation, pp. 263-292, 10.1007/978-3-030-17184-1_10, https://inria.hal.science/hal-02386004.
;Andrew C. Myers
, 2019, Abstraction-safe effect handlers via tunneling, Proceedings of the ACM on Programming Languages, 3, POPL, pp. 1-29, 10.1145/3290318, https://doi.org/10.1145/3290318.
;Georgios Karachalias;Matija Pretnar
;Tom Schrijvers
, 2018, Explicit Effect Subtyping, Lecture notes in computer science, pp. 327-354, 10.1007/978-3-319-89884-1_12, https://doi.org/10.1007/978-3-319-89884-1_12.
, 2018, First class dynamic effect handlers: or, polymorphic heaps with dynamic effect handlers, Proceedings of the 3rd ACM SIGPLAN International Workshop on Type-Driven Development, 10.1145/3240719.3241789.
;Sam Lindley
, 2018, Shallow Effect Handlers, Edinburgh Research Explorer (University of Edinburgh), pp. 415-435, 10.1007/978-3-030-02768-1_22, https://www.research.ed.ac.uk/en/publications/068e28ef-5a21-458a-860d-dc42664f7e3d.
;Eneia Nicolae Todoran, 2018, On the Abstractness of Continuation Semantics, 2018 20th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC), 60?61, pp. 167-174, 10.1109/synasc.2018.00036.
, 2018, Abstract nonsense, Proceedings of the 6th ACM SIGPLAN International Workshop on Functional Art, Music, Modeling, and Design, pp. 26-37, 10.1145/3242903.3242908.
;Tijs van der Storm, 2018, JEff: objects for effect, University of Groningen research database (University of Groningen / Centre for Information Technology), pp. 111-124, 10.1145/3276954.3276955, https://research.rug.nl/en/publications/cfc28014-995c-4789-9955-d4caf3abe902.
;Spiros Eliopoulos;Daniel Hillerström
;Anil Madhavapeddy
;K. C. Sivaramakrishnan
;et al., 2018, Concurrent System Programming with Effect Handlers, Apollo, pp. 98-117, 10.1007/978-3-319-89719-6_6, https://doi.org/10.17863/cam.30603.
, 2017, Structured asynchrony with algebraic effects, Proceedings of the 2nd ACM SIGPLAN International Workshop on Type-Driven Development, 10.1145/3122975.3122977.
, 2017, Implementing Algebraic Effects in C, Lecture notes in computer science, pp. 339-363, 10.1007/978-3-319-71237-6_17.
, 2017, Type directed compilation of row-typed algebraic effects, ACM SIGPLAN Notices, 52, 1, pp. 486-499, 10.1145/3093333.3009872.
, 2017, Handling fibred algebraic effects, Proceedings of the ACM on Programming Languages, 2, POPL, pp. 1-29, 10.1145/3158095, https://doi.org/10.1145/3158095.
;Maciej Piróg
;Piotr Polesiuk
;Filip Sieczkowski
, 2017, Handle with care: relational interpretation of algebraic effects and handlers, Proceedings of the ACM on Programming Languages, 2, POPL, pp. 1-30, 10.1145/3158096, https://doi.org/10.1145/3158096.
;SAM STATON
, 2017, Backtracking with cut via a distributive law and left-zero monoids, Journal of Functional Programming, 27, 10.1017/s0956796817000077.
;MATIJA PRETNAR
;OHAD KAMMAR
;MATIJA PRETNAR
, 2017, No value restriction is needed for algebraic effects and handlers, arXiv (Cornell University), 27, 10.1017/s0956796816000320, http://arxiv.org/abs/1605.06938.
;Conor McBride
;Craig McLaughlin
, 2017, Do be do be do, ACM SIGPLAN Notices, 52, 1, pp. 500-514, 10.1145/3093333.3009897.
;Tom Schrijvers
, 2016, Efficient algebraic effect handlers for Prolog, arXiv (Cornell University), 16, 5-6, pp. 884-898, 10.1017/s147106841600034x, http://arxiv.org/abs/1608.00816.
, 2016, Type directed compilation of row-typed algebraic effects, Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, pp. 486-499, 10.1145/3009837.3009872.
;Neil Ghani;Gordon D. Plotkin
, 2016, Dependent Types and Fibred Computational Effects, Lecture notes in computer science, pp. 36-54, 10.1007/978-3-662-49630-5_3, https://doi.org/10.1007/978-3-662-49630-5_3.
;Sam Lindley
, 2016, Liberating effects with rows and handlers, Edinburgh Research Explorer (University of Edinburgh), pp. 15-27, 10.1145/2976022.2976033.
, 2016, Gentrification gone too far? affordable 2nd-class values for fun and (co-)effect, ACM SIGPLAN Notices, 51, 10, pp. 234-251, 10.1145/3022671.2984009.
, 2016, Gentrification gone too far? affordable 2nd-class values for fun and (co-)effect, Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, pp. 234-251, 10.1145/2983990.2984009.
;Conor McBride
;Craig McLaughlin
, 2016, Do be do be do, Strathprints: The University of Strathclyde institutional repository (University of Strathclyde), pp. 500-514, 10.1145/3009837.3009897.
;BENOIT DESOUTER;MARKO VAN DOOREN;et al., 2015, Tabling as a library with delimited control, Theory and Practice of Logic Programming, 15, 4-5, pp. 419-433, 10.1017/s1471068415000137, https://doi.org/10.1017/s1471068415000137.
;Martti Karvonen
, 2015, Reversible Monadic Computing, Electronic Notes in Theoretical Computer Science, 319, pp. 217-237, 10.1016/j.entcs.2015.12.014, https://doi.org/10.1016/j.entcs.2015.12.014.
, 2015, Generic weakest precondition semantics from monads enriched with order, Theoretical Computer Science, 604, pp. 2-29, 10.1016/j.tcs.2015.03.047.
, 2015, An Introduction to Algebraic Effects and Handlers. Invited tutorial paper, Electronic Notes in Theoretical Computer Science, 319, pp. 19-35, 10.1016/j.entcs.2015.12.003, https://doi.org/10.1016/j.entcs.2015.12.003.
;Tom Schrijvers
, 2015, Fusion for Free, Lecture notes in computer science, pp. 302-322, 10.1007/978-3-319-19797-5_15.
;Christoph Rauch
;Lutz Schröder
, 2015, Unguarded Recursion on Coinductive Resumptions, Electronic Notes in Theoretical Computer Science, 319, pp. 183-198, 10.1016/j.entcs.2015.12.012, https://doi.org/10.1016/j.entcs.2015.12.012.
, 2015, Stateful Runners of Effectful Computations, Electronic Notes in Theoretical Computer Science, 319, pp. 403-421, 10.1016/j.entcs.2015.12.024, https://doi.org/10.1016/j.entcs.2015.12.024.
