On the Category of Graded Monads
Joint work with: Marco Paviotti, Dominic Orchard
Monads have become an invaluable tool in both pure mathematics and computer science. However, in many practical applications, we encounter situations where monads need to carry additional structure or parameters, necessitating a generalization known as graded monads. Graded monads allow us to refine the coarse-grained structure of classical monads by decorating them with grades from an indexing monoid, enabling finer control over composition and interaction of effects.
To develop a robust formal theory for graded monads, we follow the approach that proved successful for classical monads: we seek a 2-categorical perspective that reveals their underlying structure. Bénabou defined a monad as a morphism from the terminal bicategory [1]. Street capitalized on the structure of and considered the lax-functor category as the 2-category of monads [2]. This way of mapping any 2-category, , to the 2-category of monads over defines the functor . Street’s formal treatment of monads allowed for the wider adoption of monads for a multitude of uses in both mathematics and computing. Orchard et al. made the key conceptual leap by generalizing Bénabou’s definition of a monad to graded monads, replacing the terminal bicategory with the delooping of a monoid [3]. This generalization provides the natural jumping-off point for a formal treatment of graded monads: just as Street’s perspective provides a 2-categorical lingua franca for monads, we provide the same for graded monads.
We follow Street and Bénabou, defining a 2-functor that takes a monoidal category , and a 2-category , to the lax-functor category . We show Gmd is a graded monad on , which identifies distributive laws as graded monads in the category of graded monads themselves and gives us a notion of composition for graded monads, . We include a dual notion for graded comonads, and equivalences for distributive laws for graded monads and graded comonads in the style of Power and Watanabe [5], which contrast with the graded distributive laws of Gaboardi et al. [4].
With this machinery in place, we can close some additional open questions, namely, “what is the free graded monad?” We present a free-forgetful adjunction between the category of -graded monads over and -indexed endofunctors over , showing that the free graded monad is given by the the left Kan extension of the unit of the free monoid monad. We observe that the category of -graded monads, is still insufficient for understanding other relationships between graded monads: the fixed monoid means that this category does not capture reindexing and re-grading. To solve this we define the category of graded monads as the 2-Grothendieck construction of for a fixed 2-category . This construction gives us the appropriate 2-category with graded monads of any index.
- [1] J. Bénabou, Introduction to bicategories, in Reports of the Midwest Category Seminar, Lecture Notes in Math., vol. 47, Springer, Berlin-New York, 1967, pp. 1–77.
- [2] R. Street, The formal theory of monads, J. Pure Appl. Algebra 2, no. 2 (1972), 149–168.
- [3] D. Orchard, P. Wadler, and H. Eades III, Unifying graded and parameterised monads, in MSFP, EPTCS, vol. 317, 2020, pp. 18–38.
- [4] M. Gaboardi, S. Katsumata, D. A. Orchard, F. Breuvart, and T. Uustalu, Combining effects and coeffects via grading, in Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, ICFP 2016, Nara, Japan, September 18–22, 2016, ACM, 2016, pp. 476–489.
- [5] J. Power and H. Watanabe, Combining a monad and a comonad, Theor. Comput. Sci. 280, no. 1–2 (2002), 137–162.