"The Graded Effect"

The Graded Effect

Effectful computations — programs that read state, allocate memory, perform I/O, or consume resources — have been modeled in dozens of different categorical frameworks. Each framework captures some effects well and handles others awkwardly. Monads handle sequencing. Comonads handle context. Graded monads track quantitative resources. None unifies them.

arXiv:2603.16375 constructs monoidal categories graded by partial commutative monoids (PCMs) and discovers that the existing frameworks are all special cases. Effectful categories — previously studied as their own mathematical structure — form a coreflective subcategory of the broader PCM-graded framework. The unification is not approximate; it is structural. The prior frameworks are literal instances of the general construction.

The partial commutative monoid is the key. A PCM captures resource accounting: you can combine resources (tensor two memory blocks), the combination is commutative (order doesn’t matter), and some combinations are undefined (you can’t use a resource you don’t have). By grading a monoidal category over a PCM, each morphism carries a resource annotation, and composition respects the resource algebra.

What makes this structural rather than merely organizational is the coreflective embedding. The existing effectful category framework reflects into the PCM-graded framework with a right adjoint — meaning any effectful category can be uniquely completed into a PCM-graded category, and the completion preserves all the original structure. The old framework is the shadow of the new one, and the shadow determines the object.

The practical consequence for programming language design: resource-bounded computation (linear types, ownership, session types) and effect-tracked computation (algebraic effects, graded monads) are the same mathematical structure viewed from different angles. A type system that handles one can, in principle, handle both.


Write a comment
No comments yet.