Monoidal categories graded by partial commutative monoids
This work provides a foundational framework for modeling computational effects in category theory, which is incremental but extends existing concepts like effectful and Freyd categories.
The paper introduces monoidal categories graded by partial commutative monoids (PCMs) to generalize effectful categories, showing that effectful categories are a special case and providing examples like powerset PCMs for non-interfering parallelism and intervals for bounded resource usage.
Effectful categories have two classes of morphisms: pure morphisms, which form a monoidal category; and effectful morphisms, which can only be combined monoidally with central morphisms (such as the pure ones), forming a premonoidal category. This suggests seeing morphisms of an effectful category as carrying a grade that combines under the monoidal product in a partially defined manner. We axiomatize this idea with the notion of monoidal category graded by a partial commutative monoid (PCM). Monoidal categories arise as the special case of grading by the singleton PCM, and effectful categories arise from grading by a two-element PCM. Further examples include grading by powerset PCMs, modelling non-interfering parallelism for programs accessing shared resources, and grading by intervals, modelling bounded resource usage. We show that effectful categories form a coreflective subcategory of PCM-graded monoidal categories; introduce cartesian structure, recovering Freyd categories; and describe PCM-graded monoidal categories as monoids by viewing a PCM as a thin promonoidal category.