Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Effectful Semantics in Bicategories: Strong, Commutative, and Concurrent Pseudomonads

Hugo Paquet, Philip Saville

TL;DR

This work extends Moggi's monadic approach to effects into the 2-dimensional setting of bicategories by developing strong and commutative pseudomonads and introducing concurrent pseudomonads to capture weak interchange between parallel and sequential composition. It provides a coherent 2D framework linking strong, commutative, and monoidal structures, with Kleisli bicategories and premonoidal/freyd-like structures that model effectful programming in bicategorical semantics. The authors illustrate the theory with concrete examples (e.g., continuation/pseudo-continuation monads, spans, and concurrent game semantics) and establish fundamental coherence results, including a bicategorical Kock-type correspondence between monoidality and commutativity. The results enable rigorous modeling of concurrency and interaction in a broad class of semantic models that are naturally bicategorical, thereby offering new insights and tools for reasoning about effectful programs in 2D contexts.

Abstract

We develop the theory of strong and commutative monads in the 2-dimensional setting of bicategories. This provides a framework for the analysis of effects in many recent models which form bicategories and not categories, such as those based on profunctors, spans, or strategies over games. We then show how the 2-dimensional setting provides new insights into the semantics of concurrent functional programs. We introduce concurrent pseudomonads, which capture the fundamental weak interchange law connecting parallel composition and sequential composition. This notion brings to light an intermediate level, strictly between strength and commutativity, which is invisible in traditional categorical models. We illustrate the concept with the continuation pseudomonad in concurrent game semantics. In developing this theory, we take care to understand the coherence laws governing the structural 2-cells. We give many examples and prove a number of practical and foundational results.

Effectful Semantics in Bicategories: Strong, Commutative, and Concurrent Pseudomonads

TL;DR

This work extends Moggi's monadic approach to effects into the 2-dimensional setting of bicategories by developing strong and commutative pseudomonads and introducing concurrent pseudomonads to capture weak interchange between parallel and sequential composition. It provides a coherent 2D framework linking strong, commutative, and monoidal structures, with Kleisli bicategories and premonoidal/freyd-like structures that model effectful programming in bicategorical semantics. The authors illustrate the theory with concrete examples (e.g., continuation/pseudo-continuation monads, spans, and concurrent game semantics) and establish fundamental coherence results, including a bicategorical Kock-type correspondence between monoidality and commutativity. The results enable rigorous modeling of concurrency and interaction in a broad class of semantic models that are naturally bicategorical, thereby offering new insights and tools for reasoning about effectful programs in 2D contexts.

Abstract

We develop the theory of strong and commutative monads in the 2-dimensional setting of bicategories. This provides a framework for the analysis of effects in many recent models which form bicategories and not categories, such as those based on profunctors, spans, or strategies over games. We then show how the 2-dimensional setting provides new insights into the semantics of concurrent functional programs. We introduce concurrent pseudomonads, which capture the fundamental weak interchange law connecting parallel composition and sequential composition. This notion brings to light an intermediate level, strictly between strength and commutativity, which is invisible in traditional categorical models. We illustrate the concept with the continuation pseudomonad in concurrent game semantics. In developing this theory, we take care to understand the coherence laws governing the structural 2-cells. We give many examples and prove a number of practical and foundational results.
Paper Structure (50 sections, 25 theorems, 64 equations, 9 figures, 1 table)

This paper contains 50 sections, 25 theorems, 64 equations, 9 figures, 1 table.

Table of Contents

  1. Introduction
  2. Semantics in 2-dimensional categories
  3. The monadic theory of effects
  4. Pseudo monoidality and lax monoidality: commutativity and concurrency
  5. Commutativity
  6. Monoidality
  7. Concurrency
  8. Outline
  9. Two examples of bicategories
  10. Pseudofunctors, pseudomonads, and monoidal bicategories
  11. Basic notions
  12. Pseudomonads and Kleisli bicategories
  13. Monoidal bicategories
  14. Coherence theorems
  15. Strong pseudomonads
  16. ...and 35 more sections

Key Result

lemma 1

Figures (9)

  • Figure 1: The weak interchange law of sequential and parallel composition, as a map of event structures (see \ref{['sec:games']}).
  • Figure 2: The structural modifications of a monoidal bicategory
  • Figure 3: Coherence axioms for a strong pseudofunctor.
  • Figure 4: Coherence axioms for a strong pseudomonad: compatibility with the pseudomonad structure, and relating $\boldsymbol{x}$ with $\boldsymbol{z}$ and $\boldsymbol{w}$.
  • Figure 5: Coherence axioms for a strong pseudomonad: relating $\boldsymbol{y}$ with $\boldsymbol{z}$ and $\boldsymbol{w}$.
  • ...and 4 more figures

Theorems & Definitions (41)

  • definition 1: Benabou1967
  • definition 2
  • definition 3
  • definition 4
  • definition 5: Marmolejo1997
  • definition 6
  • definition 7: e.g. Stay2016
  • definition 8
  • definition 9
  • lemma 1
  • ...and 31 more