Reference. Reasoning about effect interaction by fusion
Effect handlers can be composed by applying them sequentially, each handling some operations and leaving other operations uninterpreted in the syntax tree. However, the semantics of composed handlers can be subtle—it is well known that different orders of composing handlers can lead to drastically different semantics. Determining the correct order of composition is a non-trivial task. To alleviate this problem, this paper presents a systematic way of deriving sufficient conditions on handlers for their composite to correctly handle combinations, such as the sum and the tensor, of the effect theories separately handled. These conditions are solely characterised by the clauses for relevant operations of the handlers, and are derived by fusing two handlers into one using a form of fold/build fusion and continuation-passing style transformation. As case studies, the technique is applied to commutative and distributive interaction of handlers to obtain a series of results about the interaction of common handlers: (a) equations respected by each handler are preserved after handler composition; (b) handling mutable state before any handler gives rise to a semantics in which state operations are commutative with any operations from the latter handler; (c) handling the writer effect and mutable state in either order gives rise to a correct handler of the commutative combination of these two theories.
Cite
Cited by (5)
Modular models of monoids with operations by lifting functors along fibrations yang-2026-modular
Inspired by Plotkin and Power’s algebraic treatment of computational effects and the principle of notions of computations as monoids, we propose a categorical framework for equational theories and models of monoids equipped with operations. This framework generalises Plotkin and Power’s algebraic treatment of effectful operations taking or returning values as input or output to operations that may take or return computations as input or output. Additionally, to give semantic models of computational effects in a modular way, we introduce a formal theory of modular constructions of algebraic structures based on the framework of lifting functors along fibrations.
Handling Higher-Order Effectful Operations with Judgemental Monadic Laws yang-2026-handling
This paper studies the design of programming languages with handlers of higher-order effectful operations - effectful operations that may take in computations as arguments or return computations as output. We present and analyse a core calculus with higher-kinded impredicative polymorphism, handlers of higher-order effectful operations, and optionally general recursion. The distinctive design choice of this calculus is that handlers are carried by lawless raw monads, while the computation judgements still satisfy the monadic laws judgementally. We present the calculus with a logical framework and give denotational models of the calculus using realizability semantics. We prove closed-term canonicity and parametricity for the recursion-free fragment of the language using synthetic Tait computability and a novel form of the ⊤⊤-lifting technique.
Modular Denotational Semantics for Effects with Guarded Interaction Trees frumin-2024-modular
We present guarded interaction trees — a structure and a fully formalized framework for representing higherorder computations with higher-order effects in Coq, inspired by domain theory and the recently proposed interaction trees. We also present an accompanying separation logic for reasoning about guarded interaction trees. To demonstrate that guarded interaction trees provide a convenient domain for interpreting higher-order languages with effects, we define an interpretation of a PCF-like language with effects and show that this interpretation is sound and computationally adequate; we prove the latter using a logical relation defined using the separation logic. Guarded interaction trees also allow us to combine different effects and reason about them modularly. To illustrate this point, we give a modular proof of type soundness of cross-language interactions for safe interoperability of different higher-order languages with different effects. All results in the paper are formalized in Coq using the Iris logic over guarded type theory.
Modular Models of Monoids with Operations yang-2023-modular
Inspired by algebraic effects and the principle of notions of computations as monoids, we study a categorical framework for equational theories and models of monoids equipped with operations. The framework covers not only algebraic operations but also scoped and variable-binding operations. Appealingly, in this framework both theories and models can be modularly composed. Technically, a general monoid-theory correspondence is shown, saying that the category of theories of algebraic operations is equivalent to the category of monoids. Moreover, more complex forms of operations can be coreflected into algebraic operations, in a way that preserves initial algebras. On models, we introduce modular models of a theory, which can interpret abstract syntax in the presence of other operations. We show constructions of modular models (i) from monoid transformers, (ii) from free algebras, (iii) by composition, and (iv) in symmetric monoidal categories.
Structured Handling of Scoped Effects yang-2022-structured
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.
Cites 46 works (3 here)
With notes (3)
Handlers in action kammar-2013-handlers
Kan Extensions for Program Optimisation Or: Art and Dan Explain an Old Trick hinze-2012-kan
Just do it: simple monadic equational reasoning gibbons-2011-just
External (43)
- Not by equations alone: Reasoning with extensible effects (2021)
- Effekt: Capability-passing style for type- and effect-safe, extensible effect handlers in Scala (2020)
- Local algebraic effect theories (2020)
- Compiling effect handlers in capability-passing style (2020)
- State Will do (2020)
- Effect handlers, evidently (2020)
- Handling Local State with Global State (2019)
- Monad transformers and modular algebraic effects: what binds them together (2019)
- Abstraction-safe effect handlers via tunneling (2019)
- Ready, set, verify! applying hs-to-coq to real-world Haskell code (experience report) (2018)
- Shallow Effect Handlers (2018)
- Syntax and Semantics for Operations with Scopes (2018)
- Total Haskell is reasonable Coq (2018)
- Theorem proving for all: equational reasoning in liquid Haskell (functional pearl) (2018)
- What is algebraic about algebraic effects and handlers? (2018)
- Handling fibred algebraic effects (2017)
- Handle with care: relational interpretation of algebraic effects and handlers (2017)
- On the Expressive Power of User-Defined Effects: Effect Handlers, Monadic Reflection, Delimited Control (2017)
- A Recipe for State-and-Effect Triangles (2017)
- Type directed compilation of row-typed algebraic effects (2017)
- Refinement reflection: complete verification with SMT (2017)
- Healthiness from Duality (2016)
- Fusion for Free: Efficient Algebraic Effect Handlers (2015)
- An Effect System for Algebraic Effects and Handlers (2014)
- Programming with algebraic effects and handlers (2014)
- Programming and reasoning with algebraic effects and dependent types (2013)
- Handling Algebraic Effects (2013)
- Theory and Practice of Fusion (2011)
- Program Calculation in Coq (2011)
- Handlers of Algebraic Effects (2009)
- A Logic for Algebraic Effects (2008)
- Asymptotic Improvement of Computations over Free Monads (2008)
- Combining effects: Sum and tensor (2006)
- Axioms for Probability and Nondeterminism (2004)
- Computational Effects and Operations: An Overview (2004)
- Algebraic Operations and Generic Effects (2003)
- Notions of Computation Determine Monads (2002)
- Representing layered monads (1999)
- A short cut to deforestation (1993)
- Notions of computation and monads (1991)
- A Couple of Novelties in the Propositional Calculus (1985)
- Communicating Sequential Processes (1978)
- Categories for the Working Mathematician (1978)