Abstract: Algebraic effects offer a versatile framework that covers a wide variety of effects. However, the family of operations that delimit scopes are not algebraic and are usually modelled as handlers, thus preventing them from being used freely in conjunction with algebraic operations. Although proposals for scoped operations exist, they are either ad-hoc and unprincipled, or too inconvenient for practical programming. This paper provides the best of both worlds: a theoretically-founded model of scoped effects that is convenient for implementation and reasoning. Our new model is based on an adjunction between a locally finitely presentable category and a category of functorial algebras. Using comparison functors between adjunctions, we show that our new model, an existing indexed model, and a third approach that simulates scoped operations in terms of algebraic ones have equal expressivity for handling scoped operations. We consider our new model to be the sweet spot between ease of implementation and structuredness. Additionally, our approach automatically induces fusion laws of handlers of scoped effects, which are useful for reasoning and optimisation.
Recommendations
Cites work
- A category-theoretic account of program modules
- A functional theory of exceptions
- A poor man's concurrency monad
- Adjunction models for call-by-push-value with stacks
- Adjunctions whose counits are coequalizers, and presentations of finitary enriched monads
- Algebraic foundations for effect-dependent optimisations
- Algebraic operations and generic effects
- Algebras for combinatorial search
- An effect system for algebraic effects and handlers
- Categorical fixed point calculus
- Coequalizers and free triples
- Combining effects: sum and tensor
- Comprehending monads
- Data types à la carte
- Deforestation: Transforming programs to eliminate trees
- Do be do be do
- Explicit substitutions and higher-order syntax
- Foundations for structured programming with GADTs
- Free-algebra models for the \(\pi \)-calculus
- Fusion for free. Efficient algebraic effect handlers
- Generalised folds for nested datatypes
- Handlers in action
- Handling algebraic effects
- scientific article; zbMATH DE number 3855352 (Why is no real title available?)
- scientific article; zbMATH DE number 3959364 (Why is no real title available?)
- scientific article; zbMATH DE number 46995 (Why is no real title available?)
- scientific article; zbMATH DE number 3458870 (Why is no real title available?)
- scientific article; zbMATH DE number 1216133 (Why is no real title available?)
- scientific article; zbMATH DE number 575948 (Why is no real title available?)
- scientific article; zbMATH DE number 1373521 (Why is no real title available?)
- scientific article; zbMATH DE number 1380900 (Why is no real title available?)
- scientific article; zbMATH DE number 2087441 (Why is no real title available?)
- scientific article; zbMATH DE number 2120508 (Why is no real title available?)
- Initial Algebra Semantics Is Enough!
- Instances of computational effects: an algebraic perspective
- Not by equations alone. Reasoning with extensible effects
- Notions of computation and monads
- On the construction of free algebras for equational systems
- Programming with algebraic effects and handlers
- Second-Order Algebraic Theories
- Shallow effect handlers
- Substitution in non-wellfounded syntax with variable binding
- Syntax and semantics for operations with scopes
- The category theoretic understanding of universal algebra: Lawvere theories and monads
- Tracing monadic computations and representing effects
- Type directed compilation of row-typed algebraic effects
- Variations on algebra: Monadicity and generalisations of equational theories
Cited in
(3)
This page was built for publication: Structured handling of scoped effects
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6166800)
