Graded monads and distributive laws

Monads have by now become a standard framework for modelling computational effects in programming languages. While a monad specifies what extra features a computation may have, such as producing a log, raising an error, or making a random choice, the associated Kleisli category provides a mathematical setting in which these effectful computations can be viewed as programs and composed in a natural way. When a program construction or data structure, usually modelled by a functor, is to be applied to such effectful computations, it must interact correctly with the underlying effects. This compatibility is captured by a distributive law between the functor and the monad, which is equivalent to the existence of a lifting of the functor to the Kleisli category of the monad. While a monad treats all effects of the same kind as uniform (e.g. “this computation may produce some log”), a graded monad keeps track of how much or what kind of effect is used by attaching a “grade” or label, for example, the exact number of steps a computation takes, the amount of memory it consumes, or a security level. The corresponding graded Kleisli category then allows us to compose programs while tracking and combining these grades, making it especially useful for resource-sensitive programming, complexity analysis, and fine-grained effect tracking. Distributive laws and functor liftings extend naturally to this graded setting as well, enabling structured forms of recursion and program transformations even in the presence of quantified effects.

Adriana Balan

Last modified: Mon Jun 15 2026