Reference. Reasoning about effect interaction by fusion

Zhixuan Yang, Nicolas Wu · · effects · PDF · DOI · pldb
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

Cite as @yang-2021-reasoning (helia, typst) · \cite{yang-2021-reasoning} (LaTeX)
BibTeX
bibtex · 1 line
@article{yang-2021-reasoning, title={Reasoning about effect interaction by fusion}, volume={5}, ISSN={2475-1421}, url={http://dx.doi.org/10.1145/3473578}, DOI={10.1145/3473578}, number={ICFP}, journal={Proceedings of the ACM on Programming Languages}, publisher={Association for Computing Machinery (ACM)}, author={Yang, Zhixuan and Wu, Nicolas}, year={2021}, month=Aug, pages={1–29} }
hayagriva YAML (typst)
yaml · 18 lines
yang-2021-reasoning:
  type: article
  title: Reasoning about effect interaction by fusion
  author:
  - Yang, Zhixuan
  - Wu, Nicolas
  date: 2021-08
  page-range: 1-29
  url: http://dx.doi.org/10.1145/3473578
  serial-number:
    doi: 10.1145/3473578
    issn: 2475-1421
  parent:
    type: periodical
    title: Proceedings of the ACM on Programming Languages
    publisher: Association for Computing Machinery (ACM)
    issue: ICFP
    volume: 5
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.
PDF · DOI · pldb

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.
PDF · DOI · arXiv · pldb

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.
PDF · DOI · arXiv · pldb

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.
PDF · DOI · pldb

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.
PDF · DOI · arXiv · pldb
Cites 46 works (3 here)
With notes (3)

Handlers in action kammar-2013-handlers

PDF · DOI · pldb

Kan Extensions for Program Optimisation Or: Art and Dan Explain an Old Trick hinze-2012-kan

DOI

Just do it: simple monadic equational reasoning gibbons-2011-just

PDF · DOI · pldb
External (43)
yang-2021-reasoning reference entries/refs/yang-2021-reasoning/yang-2021-reasoning.hel