Monoidal categories graded by partial commutative monoids

TL;DR

This paper introduces monoidal categories graded by partial commutative monoids (PCMs), unifying effectful categories and providing new examples and structural insights into graded monoidal structures.

Contribution

It axiomatizes PCM grading of monoidal categories, characterizes effectful categories as a special case, and explores their structural properties and examples.

Findings

Effectful categories are a special case of PCM-graded monoidal categories.

PCM grading captures resource and parallelism models in programming.

Effectful categories form a coreflective subcategory within PCM-graded monoidal categories.

Abstract

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.