Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Promonads and String Diagrams for Effectful Categories

Mario Román

TL;DR

This paper develops a rigorous, diagrammatic foundation for effectful categories by modeling runtime as a resource that turns a premonoidal structure into a monoidal one. It provides two core advances: a runtime-as-resource theorem establishing a free construction via an extra wire, and a promonad-centered framework showing that effectful categories are pseudomonoids in the monoidal bicategory of promonads, with a universal pure-tensor operation for combining effects. The results unify string-diagram techniques with promonad theory, offering a principled, diagrammatic approach to the semantics of effectful programming and paving the way for arrow-based reasoning and do-notation in a categorical setting.

Abstract

Premonoidal and Freyd categories are both generalized by non-cartesian Freyd categories: effectful categories. We construct string diagrams for effectful categories in terms of the string diagrams for a monoidal category with a freely added object. We show that effectful categories are pseudomonoids in a monoidal bicategory of promonads with a suitable tensor product.

Promonads and String Diagrams for Effectful Categories

TL;DR

This paper develops a rigorous, diagrammatic foundation for effectful categories by modeling runtime as a resource that turns a premonoidal structure into a monoidal one. It provides two core advances: a runtime-as-resource theorem establishing a free construction via an extra wire, and a promonad-centered framework showing that effectful categories are pseudomonoids in the monoidal bicategory of promonads, with a universal pure-tensor operation for combining effects. The results unify string-diagram techniques with promonad theory, offering a principled, diagrammatic approach to the semantics of effectful programming and paving the way for arrow-based reasoning and do-notation in a categorical setting.

Abstract

Premonoidal and Freyd categories are both generalized by non-cartesian Freyd categories: effectful categories. We construct string diagrams for effectful categories in terms of the string diagrams for a monoidal category with a freely added object. We show that effectful categories are pseudomonoids in a monoidal bicategory of promonads with a suitable tensor product.
Paper Structure (29 sections, 22 theorems, 15 equations, 28 figures)

This paper contains 29 sections, 22 theorems, 15 equations, 28 figures.

Table of Contents

  1. Introduction
  2. Contributions.
  3. Synopsis
  4. Premonoidal and Effectful Categories
  5. Premonoidal categories
  6. Effectful and Freyd categories
  7. Premonoidals are monoidals with runtime
  8. Profunctors and Promonads
  9. Profunctors: an algebra of processes
  10. Promonads: new morphisms for an old category
  11. Homomorphisms and transformations of promonads
  12. Pure Tensor of Promonads
  13. Pure tensor, via runtime
  14. Universal property of the pure tensor
  15. Effectful Categories are Pseudomonoids
  16. ...and 14 more sections

Key Result

lemma 1

Let $(\hyV,\hyG)$ be a . There exists a , $\EFF(\hyV,\hyG)$, that has objects the braid cliques, $\Braid(A_{0},\dots,A_{n})$, in $\MONRUN(\hyV,\hyG)$, and as morphisms the braid clique morphisms between them. See Appendix.

Figures (28)

  • Figure 1: The interchange law does not hold in a premonoidal category.
  • Figure 2: Writing does not interchange.
  • Figure 3: "Hello world" is not "world hello".
  • Figure 4: An extra wire prevents interchange.
  • Figure 5: Generators for the runtime monoidal category.
  • ...and 23 more figures

Theorems & Definitions (67)

  • definition 1: Binoidal category
  • definition 2
  • remark 1
  • definition 3
  • definition 4: Effectful functor
  • definition 5
  • remark 2
  • definition 6: Runtime monoidal category
  • definition 7: Braid clique
  • definition 8
  • ...and 57 more