String Diagrams for Premonoidal Categories

TL;DR

This paper addresses the lack of a unified diagrammatic language for premonoidal and effectful categories by proposing string diagrams augmented with a runtime object, following Alan Jeffrey's intuition. It develops a runtime-based construction that yields a free effectful category from a pair of generators and formalizes an adjunction that lifts monoidal string diagrams to effectful diagrams, with central pure morphisms preserved by functors. A second adjunction is established to provide string diagrams for premonoidal categories, connecting their coherence data to a diagrammatic syntax. The global-state example demonstrates how race conditions and non-interchange behavior can be represented diagrammatically, illustrating the practical utility of the approach for reasoning about imperative effects. Overall, the work lays foundational diagrammatic semantics for effectful and premomoidal structures, enabling translation between programs and diagrams and informing future language-design insights for effectful computation.

Abstract

Premonoidal categories are monoidal categories without the interchange law while effectful categories are premonoidal categories with a chosen monoidal subcategory of interchanging morphisms. In the same sense that string diagrams, pioneered by Joyal and Street, are an internal language for monoidal categories, we show that string diagrams with an added "runtime object", pioneered by Alan Jeffrey, are an internal language for effectful categories and can be used as string diagrams for effectful, premonoidal, and Freyd categories.

Figures (18)

• 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 additional wire prevents interchange.
• Figure 5: Substitution with non-interchanging string diagrams.

Theorems & Definitions (40)

• Definition 2.1: Binoidal category
• Definition 2.2: Centre, central morphism
• Definition 2.3: Premonoidal category
• Remark 2.4
• Definition 2.5
• Remark 2.6: Terminology
• Definition 2.7: Effectful functor
• Remark 2.8: Non-interchanging string diagrams
• Definition 3.1
• Definition 3.2