I want to show some simple heuristic calculations which show how monad rules stem from a functor adjunction.

Heuristic Calculations

Suppose we have some sort of duality product, and some "operators" $A$ and $A^*$.

Adjunctions means that \[ \langle y , A x \rangle \equiv \langle A^* y , x \rangle \]

We assume that we have the following vague inequality: \[ 0 ≤ \langle x , x \rangle \qquad \forall x \]

If we define the operator $T := A A^*$, we get: \[ 0 ≤ \langle A^* y , A^* y \rangle ≤ \langle y, T y \rangle \] This give us the identity of the monad.

Now, assume that "$A$ is a functor", which means: \[ \langle x , x' \rangle ≤ \langle A x , A x' \rangle \qquad \forall x, x' \]

(Notice that if $A^*$ is also a functor, which we readily assume, then so is $T$)

Using that $A$ is a functor, we obtain: \begin{equation} 0 ≤ \langle A A^* y, A A^* y \rangle \equiv \langle A^* A A^* y, A^* y \rangle ≤ \langle A A^* A A^* y, A A^* y \rangle = \langle T(T y), T y \rangle \end{equation}

This is the join of the monad.

If we summarise, we have

\begin{equation} 0 ≤ \langle y, T y\rangle \end{equation} \begin{equation} 0 ≤ \langle T(Ty), T y \rangle \end{equation}

Functor Adjunction

In the case of functor adjunctions, the bracket $\langle x, x' \rangle$ should be read as $Hom(X, X')$, where $X$ and $X'$ are object in some category.

The inequality $0 ≤ \langle x, x' \rangle$ means that there exists a particular element of $Hom(X, X')$.

The two conditions above now mean that

  • there is a map in $Hom(Y, T Y)$.
  • there ia a map in $Hom(T(TY), Y)$.

Some examples

Functor adjunctions give rise to some of the most used monads in Haskell.

The easiest example of adjunction is that of currying. This corresponds to the following identification \[ Hom(Y \times Z, X) = Hom(Y, Z \to X) \]

namely that if we choose $A X := Z \to X$ and $A^* Y := Y \times Z$, then we get indeed \[ Hom(A^* Y, X) = Hom(Y, A X) \]

Incidentally, $A$ is called the reader functor, whereas $A^*$ is called the writer functor.

The composition $T := A A^*$ is none other than the state monad, which is in particular useful to model side-effects.

The other very common functor adjunction is the free-forgetful pair.

In this case, we use functors to another category. For this example, we choose the category of monoids, but it could be another one. In this case, we choose $A$ to be the forgetful functor, and $A^*$ to be the free functor. It is true, but not immediately obvious, that this is a functor adjunction.

Their composition, $A A^*$ is none other than the list monad.

Finally, there is a strange adjuction related to the opposite category. Take a category $C$ and its opposite, which I denote $C^*$. The functors $A$ and $A^*$ just swap the arrows. We then get the adjunction \[ Hom(Y, A X) = Hom(A^* Y, X) \]

The corresponding monad is the infamous continuation monad, of which I will talk more in another post.

Say thanks!