# A short recap of monads

I used the first theory lunch meeting at the Institute of Cybernetics to recap some basics about monads. I discussed how monads are defined in category theory, and how they are implemented in Haskell.

## Categories

A category $\mathcal C$ consists of the following:

• a class $\mathrm{Ob}(\mathcal C)$ of objects
• for any objects $A$ and $B$, a class $\mathrm{hom}_{\mathcal C}(A, B)$ of morphisms $f : A \to B$
• for any object $A$, an identity morphism $\mathrm{id}_A$
• for any objects $A$, $B$, and $C$, a composition operation that maps morphisms $f : A \to B$ and $g : B \to C$ to morphisms $gf : A \to C$

Composition is associative and identities are neutral elements of composition.

An example of a category is $\mathbf{Set}$, the category of sets and functions, which is defined as follows:

• $\mathrm{Ob}(\mathbf{Set})$ is the class of all sets.
• $\mathrm{hom}_{\mathbf{Set}}(A, B)$ is $B^A$, the set of all functions from $A$ to $B$.
• $\mathrm{id}_A$ is the identity function on $A$.
• Morphism composition is function composition.

The category $\mathbf{Hask}$ is similar to $\mathbf{Set}$. It is defined as follows:

• $\mathrm{Ob}(\mathbf{Hask})$ is the set of all monomorphic Haskell types.
• $\mathrm{hom}_{\mathbf{Hask}}(\tau_1, \tau_2)$ is the set of all inhabitants of the type $\tau_1$ -> $\tau_2$.
• $\mathrm{id}_\tau$ is the identity function on $\tau$.
• Morphism composition is function composition.

Categories with additional structure can also serve as models of logic. Here, objects model propositions, and morphisms model proofs.

## Functors

A functor $F : \mathcal C \to \mathcal D$ is a structure-preserving map from the category $\mathcal C$ to the category $\mathcal D$. It maps every object $A$ of $\mathcal C$ to an object $FA$ of  $\mathcal D$ and every morphism $f : A \to B$ of $\mathcal C$ to a morphism $Ff : FA \to FB$ such that

$\forall A \in \mathrm{Ob}(\mathcal C) \mathrel. F\mathrm{id}_A = \mathrm{id}_{FA}$

and

$\forall A, B, C \in \mathrm{Ob}(\mathcal C) \mathrel. \forall f : A \to B \mathrel. \forall g : B \to C \mathrel. F(gf) = (Fg)(Ff)$ .

For every category $\mathcal C$, there exists the identity functor $\mathrm{Id}_{\mathcal C} : \mathcal C \to \mathcal C$ with

$\forall A \in \mathrm{Ob}(\mathcal C) \mathrel. \mathrm{Id}_{\mathcal C}A = A$

and

$\forall A, B \in \mathrm{Ob}(\mathcal C) \mathrel. \forall f : A \to B \mathrel. \mathrm{Id}_{\mathcal C}f = f$ .

For functors $F : \mathcal C \to \mathcal D$ and $G : \mathcal D \to \mathcal E$, we can form the composition $GF : \mathcal C \to \mathcal E$ with

$\forall A \in \mathrm{Ob}(\mathcal C) \mathrel. (GF)A = G(FA)$

and

$\forall A, B \in \mathrm{Ob}(\mathcal C) \mathrel. \forall f : A \to B \mathrel. (GF)f = G(Ff)$ .

In Haskell, there is the Functor class, which is defined as follows:

class Functor f where

fmap :: (a -> b) -> (f a -> f b)

Every instance of Functor corresponds to a functor from $\mathbf{Hask}$ to $\mathbf{Hask}$. Thereby, f maps objects (which are types), and fmap maps morphisms (which are functions).

## Natural transformations

Let $\mathcal C$ and $\mathcal D$ be categories, and let $F$ and $G$ be functors from $\mathcal C$ to $\mathcal D$. A natural transformation $\tau$ from $F$ to $G$ is a family $\left\{\tau_A : FA \to GA\right\}_{A \in \mathrm{Ob}(\mathcal C)}$ for which

$\forall A, B \in \mathrm{Ob}(\mathcal C) \mathrel. \forall f : A \to B \mathrel. \tau_B(Ff) = (Gf)\tau_A$

holds.

From $\tau$ and a functor $V : \mathcal D \to \mathcal Q$, we can derive the natural transformation $V\tau : VF \to VG$ with

$\forall A \in \mathrm{Ob}(\mathcal C) \mathrel. \left(V\tau\right)_A = V\left(\tau_A\right)$ .

This is similar to applying a functor to a morphism. However if we have a functor $W : \mathcal Q \to \mathcal C$, we can also derive the natural transformation $\tau W : FW \to GW$ with

$\forall X \in \mathrm{Ob}(\mathcal Q) \mathrel. \left(\tau W\right)_X = \tau_{WX}$ .

Let f and g be instances of Haskell’s Functor class, and let $F, G : \mathbf{Hask} \to \mathbf{Hask}$ be the functors they denote. A natural transformation from $F$ to $G$ is a function t of the polymorphic type forall a . f a -> g a. The above axiom for natural transformations holds automatically, since t has to treat values of type a as black boxes. This is closely related to the concept of free theorems.

## Functor categories

For any categories $\mathcal C$ and $\mathcal D$, the functor category $\mathcal D^{\mathcal C}$ is defined as follows:

• $\mathrm{Ob}\left(\mathcal D^{\mathcal C}\right)$ is the class of all functors from $\mathcal C$ to $\mathcal D$.
• $\mathrm{hom}_{\mathbf{\mathcal D^{\mathcal C}}}(F, G)$ is the class of all natural transformations from $F$ to $G$.
• $\mathrm{id}_F$ is $\left\{\mathrm{id}_{FA}\right\}_{A \in \mathrm{Ob}(\mathcal C)}$.
• Morphism composition is pointwise composition of natural transformations.

A monad on a category $\mathcal C$ is a triple $(T, \eta, \mu)$ where

$\begin{array}{rcl}T & : & \mathcal C \to \mathcal C \\ \eta & : & \mathrm{Id}_{\mathcal C} \to T \\ \mu & : & TT \to T\end{array}$

and the equations

$\mu(\eta T) = \mu(T\eta) = \mathrm{id}_T : T \to T$

and

$\mu(\mu T) = \mu(T\mu) : TTT \to T$

hold.

Given this definition, the straightforward way to implement monads on $\mathbf{Hask}$ in Haskell is as follows:

class Functor m => Monad m where

return :: a -> m a

join   :: m (m a) -> m a

Thereby, return corresponds to $\eta$, and join corresponds to $\mu$. The definition of the Monad class in the Prelude is different though:

class Monad m where

return :: a -> m a

(>>=)  :: m a -> (a -> m b) -> m b

That said, both definitions are equivalent, as (>>=) can be defined in terms of fmap and join, and fmap and join can be defined in terms of return and (>>=). The latter is done in Control.Monad, where the fmap derived from return and (>>=) is called liftM.

Monads are used in Haskell to implement effectful computations. Thereby, the choice of a monad determines the kind of effect. Following is an overview of some monads:

Type Effect
data Maybe a = Nothing | Just a failure
data Either e a = Left e | Right a exception
data [a] = [] | a : [a] nondeterminism