Monoidal categories graded by partial commutative monoids
Matthew Earnshaw, Chad Nester, Mario Román
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.