Source-linked AI summary
Handling Algebraic Effects
Gordon D Plotkin, Matija Pretnar
TL;DR
Exception handling lacked an algebraic treatment despite the algebraic account available for many computational effects. The paper models handlers as theory models and handling as induced homomorphisms, then generalises this construction to arbitrary algebraic effects. It yields a programming construct covering examples such as CCS relabelling and restriction, timeout, rollback, and stream redirection, while handler correctness has substantial decision complexity.
Problem
Exception handlers challenge the algebraic approach because the standard handling construct lacks the naturality property characterising equationally specified operations.
Method
The paper represents handlers as models of the relevant equational theory and handling constructs as homomorphisms induced by the free model's universal property.
Results
The construction generalises exception handling to arbitrary algebraic effects and encompasses relabelling and restriction in CCS, timeout, rollback, and stream redirection.
Takeaways & Limitations
Algebraic operations and effect handlers form complementary effect constructors and deconstructors, supporting a unified programming concept for handling algebraic effects.
Takeaways & Limitations
The paper develops operational ideas for understanding effect handlers but does not present a formal operational semantics for them.
Abstract
from arXiv · showhide
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.
Introduction
The paper develops an algebraic account of exception handling because standard handling constructs lack the naturality property of equationally specified operations. It then generalises handlers to arbitrary algebraic effects and develops their calculus, semantics, examples, and correctness theory.
- Introduction: Algebraic effects are represented by equational theories whose free models induce computational monads; exceptions are an important unresolved case.The algebraic view supports combining and reasoning about effects, but exception handlers challenge this approach.
- Introduction: Standard exception handling lacks naturality with respect to evaluation contexts, and no alternative ranked monad suffices.Unlike choice and exception raising, handling does not generally commute with evaluation contexts.
- Introduction: The paper models handlers as models of the exception theory and interprets handling through unique homomorphisms into those models.The usual handler preserves returned values, while the general approach permits arbitrary induced homomorphisms.
- Introduction: The approach generalises to arbitrary algebraic effects, with examples including CCS relabelling and restriction, timeout, rollback, and stream redirection.The paper characterises operations as effect constructors and handlers as effect deconstructors.
- Introduction: The paper develops a call-by-push-value calculus, denotational semantics, handler-correctness criteria, reasoning principles, recursion, and decidability results.It does not present a formal operational semantics of effect handlers.
1. Exception Handlers
The paper develops exception handling algebraically by interpreting handlers as models and handling constructs as induced homomorphisms. It then generalises this framework to arbitrary algebraic effects while allowing handlers whose correctness may require separate verification.
- Simple handling construct: Exception computations use the monad A + exc, with returned values injected into the left component and raised exceptions represented in the right.The unit maps A into A + exc; return V becomes in1(V), while raise_e() becomes in2(e).
- Simple handling construct: A simple handler intercepts each raised exception e and replaces it with a predefined computation M_e, while unhandled exceptions are re-raised.The construct carries out M and substitutes M_e whenever e is raised.
- Simple handling construct: The handler computations define a new exception model, and handling is the unique homomorphism from the free computation model that preserves returned values.The homomorphism is induced by the free model’s universal property and extends in1.
- Extended handling construct: The extended construct passes returned values to a user-defined continuation N : A → B + exc, allowing handled computations to return values in a different set B.Handling computations N_e likewise produce values in B or raise exceptions.
- Extended handling construct: Benton and Kennedy’s construct captures a previously cumbersome programming idiom, supports additional optimisations, and has a stack-free small-step operational semantics.Algebraically, it again uses an induced homomorphism targeting a model on B + exc.
- Handling arbitrary algebraic effects: The same model-and-homomorphism account extends handlers from exceptions to arbitrary algebraic effects, including relabelling, restriction, timeout, rollback, and stream redirection.Operations are replaced by handling maps, potentially involving several replacements within a computation.
2. Syntax
The language separates values from computations and represents effects through typed operation symbols, while handlers define how computations are processed. Its call-by-push-value syntax includes operations, handlers, thunks, sequencing, and an explicit handling construct.
- Signatures: A signature comprises base types, typed pure function symbols, typed operation symbols, and an effect theory determining operation properties.Operations accept parameters and produce outcomes whose types determine their continuations.
- Types: The language follows call-by-push-value by strictly separating value types from computation types.Thunked computations are values that can later be forced, and FA classifies computations returning values of type A.
- Terms: Value terms use constructors such as variables, products, sums, functions, and thunks, while computation terms include returns, sequencing, operations, projections, and handling.Constructors and destructors are divided between values and computations, with computation terms performing evaluation.
- Operations: An operation application triggers an operation with a parameter, binds its outcome to a variable, and continues with the resulting computation.Operation symbols are parameterised by an input type and have an arity describing the continuation outcome.
- Handlers: A handler maps each operation symbol to a handling computation depending on its parameters and continuation variables.Continuation variables occur only when applied to values, and handlers may omit type annotations when unambiguous.
- Handling: The construct M handled with H to x. N handles M with H, binds its result to x, and then evaluates N.This syntax makes both the binding scope and the evaluation order explicit.
3. Examples
The examples show handlers implementing diverse algebraic-effect transformations, including nondeterministic result collection, CCS relabelling and restriction, output suppression, timeout, rollback, and stream redirection. Their scope is broad, but binary deconstructors such as general pipes remain difficult to represent.
- Nondeterminism: A list handler collects every result of a nondeterministic computation by recursively combining branch results with append.The handled computation returns a list containing the result of each path.
- CCS: CCS relabelling replaces actions with one label by actions with another, while restriction blocks actions associated with a specified name.Both are represented as handlers, with omitted operations retaining their expected structural behaviour.
- Parameter-passing: A parameter-passing handler suppresses output after nmax characters by writing while n < nmax and skipping writes thereafter.The handled computation carries the parameter and is initially applied at 0.
- Timeout: The timeout handler runs a computation for a given wait period, returns a default value if it does not finish, and preserves time spent during evaluation.The handler tracks elapsed time through its parameter.
- Rollback: Rollback handlers address exceptions during state modification by reverting modifications made during the computation.The motivating case is a connection dropping halfway through a database transaction.
- Files and devices: The file-and-device example uses a simplified model in which files are already opened for reading and writing.A more realistic model would add operations for opening and closing files.
- Stream redirection: The calculus represents simple pipes by feeding one process’s output to another process’s input, including the example yes | p.The general pipe combinator is harder because it is a binary rather than unary deconstructor.
4. Semantics
The semantics models algebraic effects with equational theories and interprets computations and handlers through models and homomorphisms. The free-model construction exists for the theories considered, while handler correctness is established for several examples but is generally difficult to decide.
- Recursion: The semantics adapts from sets to pointed ω-cpos and continuous functions when recursion is included.The corresponding functors, strengths, and induced homomorphisms are continuous.
- Interpretation: Templates are interpreted as maps from value environments and template-variable environments into a model carrier.Operation templates are interpreted using the corresponding model operation and the interpreted continuation template.
- Effect theories: An effect theory is a finite set of equations between well-formed computation templates over a signature.The paper gives theories for exceptions, state, nondeterminism, I/O, time, CCS, and destructive exceptions.
- Models: A model assigns a carrier set and interpretations to operation symbols such that every equation in the effect theory holds.Homomorphisms map model carriers while preserving the operations.
- Free models: The forgetful functor from models to sets has a left adjoint, yielding a free model over each set.The induced homomorphism is determined by the universal property of that free model.
- Handler correctness: All handlers in the examples are correct for their stated theories, including CCS relabelling and restriction for weak and strong bisimulation.Rollback handlers are correct for destructive exceptions, whereas the standard exception handler is not.
- Handler correctness: Handler correctness is generally undecidable, with even very simple cases being Π2-complete.The paper also considers restricting terms to those guaranteed to receive an interpretation under suitable assumptions.
5. Reasoning about handlers
The paper develops equations and existence assertions for reasoning about computations and handlers, including laws inherited from call-by-push-value and the effect theory. These principles characterize handling through induced homomorphisms, but a full logic and general equation theory remain incomplete.
- Assertions: The reasoning framework uses definedness, Kleene equality, and Kleene inequations for values, computations, and handlers.A Kleene inequation V ≲ W abbreviates that V being defined implies V and W are equal.
- Equations: The semantics validates call-by-push-value equations, including sequencing, function η-equality, and component-wise or pointwise operation behaviour.Operations also commute with sequencing because sequencing is induced by the free model’s universal property.
- Effect-theory reasoning: Equations from an effect theory are inherited by replacing template variables with continuation variables.The resulting computation terms remain equal under the corresponding substitutions.
- Handling equations: The handling construct satisfies inequations expressing that it extends the inducing map on values and acts homomorphically on operations.The operation-handling inequation substitutes the handled continuation into the operation’s handling term.
- Handling equations: Handling with the empty handler is equivalent to sequencing, because omitted operations are handled by themselves.The two handler inequations therefore generalize the sequencing laws.
- Scope: Equations proposed for exception handlers do not hold for general handlers, although they remain valid for particular handler classes.The paper does not develop this issue further into a full-fledged logic for algebraic effects and handlers.
- Existence: Existence assertions characterize when returns, sequencing, handlers, and handling computations are defined.A handling computation exists exactly when its computation and handler exist and every continuation result is defined.
6. Deciding handler correctness
The paper studies when handlers are correct and shows that correctness is generally difficult to decide, with improved decidability for uniformly simple handlers and decidable theories.
- Handler correctness is identified as a question potentially pertinent for compiler writers.
- A simple closed handler’s correctness is Π2-complete to decide.
- Uniformly simple handler families restrict dependence on specific computation types and can make correctness semidecidable.
- For uniformly simple families over decidable effect theories, correctness is decidable.
7. Recursion
The recursion extension adds nontermination and interprets programs over pointed ω-cpos with continuous functions and least fixed points. Correctness remains constrained by the effect theory, while several broader extensions remain open.
- Recursion syntax and semantics: Recursion is added through a fixed-point constructor and an operation div representing nontermination.
- Recursion syntax and semantics: The semantics moves from sets to ω-cpos and interprets functions, operations, terms, and handlers continuously.
- Recursion syntax and semantics: The fixed-point constructor is interpreted as the least fixed point of a continuous function on a pointed ω-cpo.
- Correctness under recursion: Correct handlers cannot redefine div because the theory fixes it uniquely.
- Open questions: Open questions include parallel handling, correctness results over ω-cpos, richer handler combinations, and more practical programming-language formulations.
Appendix A. Decidability of handler correctness
The appendix proves complexity results for handler correctness by translating handlers into interpretations of finite equational theories and reducing correctness to provability questions.
- Deciding whether such an interpretation holds in the initial model is Π2-complete.
- Simple signatures and theories are translated into finite equational theories whose models correspond to those of the original theories.
- Correctness of simple closed handlers corresponds to whether the associated interpretation holds in the initial model.
- Provability for the uniformly simple construction is Σ1-complete in general and decidable when the effect theory is decidable.
- For uniformly simple handler families, correctness corresponds to provability of the associated interpretation in the finite equational theory.