Handling Algebraic Effects
arXiv:1312.1399 · doi:10.2168/LMCS-9(4:23)2013
Abstract
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.
36 pages
Cited by in corpus (26)
- Notions of bidirectional computation and entangled state monads
- Interaction Trees: Representing Recursive and Impure Programs in Coq
- Unguarded Recursion on Coinductive Resumptions
- Reversible monadic computing
- Fibred Computational Effects
- Runners in action
- Soundly Handling Linearity
- Local Algebraic Effect Theories
- Modular Probabilistic Models via Algebraic Effects
- Tabling as a Library with Delimited Control
- Asynchronous Effects
- Explicit Effect Subtyping
- Efficient CHAD
- Efficient, Portable, Census-Polymorphic Choreographic Programming
- Signature Restriction for Polymorphic Algebraic Effects
- Interaction laws of monads and comonads
- On Decidable and Undecidable Extensions of Simply Typed Lambda Calculus
- Two-sorted algebraic decompositions of Brookes's shared-state denotational semantics
- Scoped Effects as Parameterized Algebraic Theories
- The Quantum Monadology
- When Programs Have to Watch Paint Dry
- Inductive and Coinductive Predicate Liftings for Effectful Programs
- Modular Termination for Second-Order Computation Rules and Application to Algebraic Effect Handlers
- Protocol Choice and Iteration for the Free Cornering
- Handling Bidirectional Control Flow: Technical Report
- From High to Low: Simulating Nondeterminism and State with State