Graded monads are great. In functional programming, for example, they
can be used to track certain sorts of external state at the type
level. ^{1}

## Lax Functors and Monads

Graded monads generalize ordinary monads, let’s see how: An ordinary
monad can be viewed as a lax 2-functor 1 → *C**A**T* from the terminal
2-category 1 to the 2-category of large categories *C**A**T*.

The later contains the (idealized) category *H**a**s**k* as an object. And
it’s the only one I’m going to use as an example. But you may also
think of the category *S**e**t* of sets and functions, if that’s more
familiar.

Let’s note that the terminal 2-category 1 consists of a unique object, its identity arrow, and the later’s identity 2-arrow.

First, any lax 2-functor *T* : 1 → *C**A**T* needs to assign values for the
unique object * and for its identity (the image of the identity 2-arrow
is fixed by the choice of the 1-arrow).

Note in particular that *T* does not need to preserve the identity
arrow. That’s part of what makes it lax.

So we define *T* by choosing a category as the image of the unique
object. Let’s suppose we chose *H**a**s**k*.

Now we still get to freely choose an endomorphism of *H**a**s**k*, i.e., an
endofunctor. Let’s also call it *T*. So keep in mind there will be two
*T*s appearing, one a lax 2-functor, the other an endofunctor of
*H**a**s**k*.

We already see some structure emerge: because *T* : *H**a**s**k* → *H**a**s**k* is an
endofunctor, we can take its powers: *T*^{0}, *T*, *T*^{2}, *T*^{3} … by
composing *T* with itself repeatedly.

*T*^{0} is of course the identity functor *I**d* : *H**a**s**k* → *H**a**s**k* of *H**a**s**k*.
By contrast, if *T* were a strict 2-functor, our image *T* = *T*(*i**d*) would
have to be the identity functor of *H**a**s**k*, and equal to all its
powers. *Not so here*.

The relationship between the identity functor of *H**a**s**k* and *T* : *H**a**s**k* → *H**a**s**k* is not completely arbitrary however: the definition of a lax
2-functor requires us to provide a 2-arrow *I**d*_{Hask} ⇒ *T*, i.e., a
natural transformation.

In Haskell notation this is a function `eta :: a -> T a`

. As for the
identity, so for the composition: since *T* is lax, it is only
required to preserve composites up to 2-arrow. For our *H**a**s**k*
endofunctor *T* this means we require a natural transformation *T*^{2} ⇒ *T*, let’s call it *μ*.

In Haskell notation this is a `mu :: T(T a) -> T a`

. (The natural
transformations eta and mu are better known in Haskell as `return`

and
`join`

from the `Control.Monad`

module)

Continuing with our story: for (*T*,*η*,*μ*) to actually be a monad the
natural transformations *η* and *μ* have to satisfy two axioms usually
called UNIT and ASSOCIATIVITY^{2}.

Now the big shocking reveal is that the axioms for our lax 2-functor
*T* : 1 → *C**A**T* look exactly like the monad axioms for (*T*:*H**a**s**k*→*H**a**s**k*,*η*,*μ*).

Disregarding the fact that I have not actually given a precise
definition of lax 2-functors, we now take it as established that there
is a bijection between such *T* : 1 → *H**a**s**k* with object value *H**a**s**k*
and monads *T* on the category *H**a**s**k*.

## Graded Monads

Now, to obtain the concept of a graded monad we need to replace the terminal 2-category 1 in the story above with something else. That something else is going to be a monoid. Let me explain what I mean by that.

Monoids, i.e., sets with an associative and unital operation can be viewed as categories: introduce an object, let’s call it *, and let the morphisms * → * be the elements of the monoid. Then the monoid operation is a composition operation for this category and the monoid unit is the identity morphism of the single object *.

(The object * is not to be confused with the `Type`

kind in
Haskell.)

So a monoid in a way *is* a category. But we really needed to replace
the terminal 2-category 1 with another 2-category, since we want to
talk about lax 2-functors out of it. This is easily fixed: just add in
an identity 2-arrow for each 1-arrow.

Thus, in the same vein, a monoid in a way *is* a 2-category, and this
shifting of viewpoint does not require supplying any new data, but
merely the use of a more powerful language to talk about the same
thing.

## Example

As an example, let’s consider the monoid with elements 0 and 1 and
the usual multiplication as the operation. Then clearly 1 is the
unit. As a category it has arrows 0 : * → * and 1 : * → * and
composition is just multiplication, as we have said. Let’s call this
category *B*.

We view *B* as a 2-category, and consider what it means to have a lax
2-functor *T* : *B* → *C**A**T*. *T*(*) is some category, for concreteness, we
can continue to assume that’s *H**a**s**k*. Since *B* has 2 distinct arrows
we get two *H**a**s**k* endo functors *T*_{0} and *T*_{1} : *H**a**s**k* → *H**a**s**k*.

Note that *T*_{1} is the image of the identity 1 : * → * under the lax
2-functor, so laxness means there must be a natural transformation
*η* : *I**d*_{Hask} ⇒ *T*_{1}.

Also by laxness of *T*, as part of its data, there are natural
transformations *μ* : *T*_{i}*T*_{j} ⇒ *T*_{k} where *i* and *j* can be 0 or
1 and *k* is *i* × *j*. (Note that these are 4 different *μ*’s, but
I don’t want to clutter the notation with indices.)

In Haskell notation we might write these natural transformations as
`eta :: a -> T One a`

and `mu :: T i (T j a) -> T (Mult i j) a`

. (Note
that the first type parameter of `T`

is of a data kind with
constructors `Zero`

and `One`

, `Mult`

is a type family implementing
multiplication for them.)

The natural transformations need to satisfy unit and associativity
laws. These can be obtained from the diagrams I included earlier, by
inserting indices *i*, *j* and *i* × *j* in the right places.

## Generalization

Now, to see that graded monads generalize monads we only need to consider the fact that the trivial monoid having a single element gives exactly the terminal category when promoted to a 2-category in the way I described.

Furthermore, homomorphisms of monoids, i.e., maps preserving monoid
unit and composition, can be promoted to strict 2-functors in an
obvious way. In particular, for an arbitrary monoid *M* there is always a
unique homomorphism *e* : 1 → *M* picking out the unit.

If we write the homomorphism e promoted to a strict 2-functor as *E*,
and if we have a lax 2-functor *T* : *M* → *C**A**T* then by composing these
*T**E* : 1 → *C**A**T*, we obtain an ordinary monad contained in the graded
monad given by *T*.

## End

There is a type class interface for graded monads implemented in
effect-monad by
Dominic Orchard . Using the
`RebindableSyntax`

extension of GHC or the upcoming
`QualifiedDo`

extension we can even write `do`

-blocks that use graded monads.

To my knowledge, the primordial source for lax 2-functors is
Introduction to
bicategories by
Jean Bénabou. Although he calls them simply *morphisms* of
bicategories. The example section shows how versatile the notion is.
In particular, he describes «polyads», these are also known today as
indexed monads. I might write about them some other time.

I have used graded monads to implement tracking of kernel API capabilities in Haskell programs.

## Acknowledgements

Thanks to contributors on stackexchange for help with typesetting the diagrams.

We could also have presented these axioms as diagrams inside a category.↩︎