Monads

Monads are very important for pure functional programming languages such as Haskell. We shall start with Monoid consideration, continue with the formal mathematical definition for the monad and will finish with programming languages examples later.

Monoid in \(\mathbf{Set}\) category

In the Category as a monoid we considered the definition and importance of the Monoid concept. The definition was given in terms of internal structure i.e. the ordinary and not Categorical approach was used. Now we are going to consider Monoid in terms of Set theory but will try to give the definition that is based rather on morphisms than on internal set structure i.e. we shall use Categorical approach. Let \(M\) be a set and by the monoid definition (Monoid) \(\forall m_1, m_2 \in M\) we can define a new element of the set \(\mu(m_1, m_2) \in M\). Later we shall use the following notation for the \(\mu\): \[\mu(m_1, m_2) \equiv m_1 \cdot m_2.\] If \((M, \cdot)\) is a monoid then the following 2 conditions have to be satisfied. The first one (associativity) declares that \(\forall m_1, m_2, m_3 \in M\) \[m_1 \cdot ( m_2 \cdot m_3) = ( m_1 \cdot m_2 ) \cdot m_3.\] The second one (identity presence) says that \(\exists e \in M\) such that \(\forall m \in M\): \[m \cdot e = e \cdot m = m.\]

Associativity

Let’s consider (Monoid in Set) in detail. We can define \(\mu\) as a Morphism in the following way \[\mu: M\times M \to M,\] where \(M \times M\) is the Product in the Set category. I.e. \(M \times M, M \in \mathrm{ob}(\mathbf{Set})\) and \(\mu \in \mathrm{hom}(\mathbf{Set})\). Consider other objects of \(\mathbf{Set}\): \(A = M \times \left( M \times M \right)\) and \(A' = \left( M \times M \right) \times M\). They are not the same but there is a trivial Isomorphism between them \(A \cong_\alpha A'\), where the isomorphism \(\alpha\) is defined as \[\alpha(x,(y,z)) = ((x,y),z).\] Consider the action of Product of morphisms \(\mathbf{1}_{M \to M} \times \mu\) on \(A\): \[\left[\mathbf{1}_{M \to M} \times \mu \right]\left(x,\left(y,z\right)\right) = \left(\mathbf{1}_{M \to M}(x),\mu\left(y,z\right)\right) = \left(x, y \cdot z\right) \in M \times M\] i.e. \(\mathbf{1}_{M \to M} \times \mu: M \times \left( M \times M \right) \to M \times M\). If we act \(\mu\) on the result then we can obtain: \[\begin{aligned} \mu \left(\left[\mathbf{1}_{M \to M} \times \mu \right]\left(x,\left(y,z\right)\right)\right) = \nonumber \\ = \mu \left(\mathbf{1}_{M \to M}(x),\mu\left(y,z\right)\right) = \nonumber \\ = \mu\left(x, y \cdot z\right) = x \cdot (y\cdot z) \in M, \nonumber \end{aligned}\] i.e. \(\mu \circ \left[\mathbf{1}_{M \to M} \times \mu\right]: M \times \left( M \times M \right) \to M\).

For \(A'\) we have the following one: \[\begin{aligned} \mu\circ\left[\mu \times \mathbf{1}_{M \to M}\right]\left(\left(x,y\right),z\right) = \mu\left(x \cdot y, z\right) = (x \cdot y) \cdot z. \nonumber \end{aligned}\] Monoid associativity requires \[x \cdot (y\cdot z) = (x \cdot y) \cdot z\] i.e. the morphisms shown in Associativity commute: \[\mu\circ\left[\mu \times \mathbf{1}_{M \to M}\right] = \mu \circ \left[\mathbf{1}_{M \to M} \times \mu\right] \circ \alpha.\]

Very often the isomorphism \(\alpha\) is omitted i.e. \[M\times\left(M \times M\right) = \left(M \times M\right)\times M = M^3\] and the morphism equality (Associativity) is written as follow \[\mu\circ\left[\mu \times \mathbf{1}_{M \to M}\right] = \mu \circ \left[\mathbf{1}_{M \to M} \times \mu\right].\] The corresponding commutative diagram is shown in Associativity.

Identity presence

For (Monoid in Set) consider a morphism \(\eta\) from Singleton ¹ \(I = \{0\}\) to the special element \(e \in M\) such that \(\forall m \in M: e \cdot m = m \cdot e = m\). I.e. \(\eta: I \to M\) and \(e = \eta(0)\). Consider 2 sets \(B = I \times M\) and \(B' = M \times I\). We have 2 Isomorphisms: \(B \cong_\lambda M\) and \(B' \cong_\rho M\) such that \[\lambda(m) = (0, m) \in B = I \times M\] and \[\rho(m) = (m, 0) \in B' = M \times I.\]

If we apply the products (see Product of morphisms) \(\eta \times \mathbf{1}_{M \to M}\) and \(\mathbf{1}_{M \to M} \times \eta\) on \(B\) and \(B'\) respectively then we get \[\begin{aligned} \left[\eta \times \mathbf{1}_{M \to M} \right]\left(0, m\right) = (e, m), \nonumber \\ \left[\mathbf{1}_{M \to M} \times \eta \right]\left(m, 0\right) = (m, e). \nonumber \end{aligned}\] After the application of \(\mu\) on the result we obtain \[\begin{aligned} \mu \left(\left[\eta \times \mathbf{1}_{M \to M}\right] \left(0, m\right) \right) = \mu \left( e, m \right) = e \cdot m, \nonumber \\ \mu \left(\left[ \mathbf{1}_{M \to M} \times \eta \right]\left(m, 0\right) \right) = \mu \left(m, e \right) = m \cdot e. \nonumber \end{aligned}\]

The (Monoid in Set) leads to the following equation for morphisms \[\mu \circ (\eta \times \mathbf{1}_{M \to M}) \circ \lambda = \mu \circ (\mathbf{1}_{M \to M} \times \eta) \circ \rho = \mathbf{1}_{M \to M}\] or the commutative diagram shown on Identity presence.

Categorical definition for monoid

Before given a formal definition lets look at the operations were used for the construction. The first one is the product of 2 objects: \[M \times M.\] We also have 2 pairs of morphisms: \[\begin{aligned} \mu: M \times M \to M, \nonumber \\ \mathbf{1}_{M \to M}: M \to M. \nonumber \end{aligned}\] and \[\begin{aligned} \eta: I \to M, \nonumber \\ \mathbf{1}_{M \to M}: M \to M. \nonumber \end{aligned}\] The pairs can be combined into one using Product of morphisms as follows: \[\begin{aligned} \mu \times \mathbf{1}_{M \to M}: \left(M \times M\right) \times M \to M \times M, \nonumber \\ \mathbf{1}_{M \to M} \times \mu: M \times \left(M \times M\right) \to M \times M \nonumber \end{aligned}\] and \[\begin{aligned} \eta \times \mathbf{1}_{M \to M}: I \times M \to M \times M, \nonumber \\ \mathbf{1}_{M \to M} \times \eta: M \times I \to M \times M. \nonumber \end{aligned}\] The same structure ² is used by Functor and especially by Bifunctor.

Now we are ready to provide the monoid definition in the terms of morphisms.

Monoid importance

Why is the concept of Monoid so important? In pure math it provides the build blocks for important concepts such as Group, Ring, Field (Murashko 2016-2019). In programming languages it gives more simple and robust concept for software design (Gonzalez 2014).

We can notice that monoid definition (see Monoid) has the same requirements as morphisms in category theory. Moreover the monoid can be viewed as a Category (see Category as a monoid).

Monoid provides a closed collection of objects such that if you combine them you will get an object of the same type. This allows to create constructions which are more easy in maintenance. For instance there are 2 possible options to combine objects of type \(A\) in software architecture (Gonzalez 2014; Lex Sheehan 2017):

1. Conventional architecture assumes that a combination of several objects of type \(A\) will produce a “network” of the objects \(A\) i.e. new type \(B\)

2. Haskell architecture assumes that a combination of several objects of type \(A\) will produce a new object of the same type \(A\)

You can see that in the first case any modification of the base type \(A\) will require changes in the upper-layer class \(B\). This produce very complex structure of types if objects of type \(B\) will be combined into new type \(C\) etc.

You will not get the problems in the second case because you will be always in a closed collection of objects with the same type \(A\).

Monoidal category

As we saw in the categorical definition for monoid (see Monoid) the category \(\mathbf{C}\) should satisfy several conditions to have an object as monoid. Lets formalise the conditions.

In the Set category we have \(\times\) as the monoidal product (see Bifunctor). There is also a morphism \(\eta\) from terminal object \(t\) to \(e\) ((https://math.stackexchange.com/users/232/qiaochu-yuan), n.d.) (see Monoid).

Tensor product in Quantum mechanics

Let \(m,n \in \mathbf{FdHilb}\). The tensor product \(m \otimes n\) is another finite dimensional Hilbert space equipped with a bilinear form \[\phi: m \times n \to m \otimes n\] such that \(\forall a \in \mathbf{FdHilb}\) and for any bilinear \[f: m \times n \to a\] exists only one morphism \(\tilde{f}: m \otimes n \to a\) such that \[f = \tilde{f} \circ \phi\] i.e. the diagram on the Tensor product commutes

The tensor product in quantum mechanics is used for representing a system that consists of multiple systems. For instance if we have an interaction between an 2 level atom (\(a\) is excited state \(b\) as a ground state) and one mode light then the atom has its own Hilber space \(\mathcal{H}_{at}\) with \(\ket{a}\) and \(\ket{b}\) as basis vectors. Light also has its own Hilber space \(\mathcal{H}_f\) with Fock state \(\{\ket{n}\}\) as the basis. ³ The result system that describes both atom and light is represented as the tensor product \(\mathcal{H}_{at} \otimes \mathcal{H}_f\).

Category of endofunctors

The Fun category is an example of a category. We can apply additional limitation and consider only Endofunctors i.e. we shall look at the category \([\mathbf{C}, \mathbf{C}]\) - the category of functors from category \(\mathbf{C}\) to the same category. One of the most popular math definition of a monad is the following: “All told, a monad in X is just a monoid in the category of endofunctors of X”(Lane 1998, 138). Later we shall give an explanation for that one.

We start with the formal definition of category of endofunctors and a tensor product in the category

Lets look at the requirements (Monad) more closely. Notice that the functor composition is associative: \[M \circ ( M \circ M ) = (M \circ M) \circ M = M^3.\] Secondly all rewrite it with (Whiskering) and (Whiskering) as follows \[\begin{aligned} \mu \circ \left( \mathbf{1}_{M \xrightarrow{.} M} \star \mu \right) = \mu \circ \left( \mu \star \mathbf{1}_{M \xrightarrow{.} M} \right), \nonumber \\ \mu \circ \left( \mathbf{1}_{M \xrightarrow{.} M} \star \eta \right) = \mu \circ \left( \eta \star \mathbf{1}_{M \xrightarrow{.} M} \right) = \mathbf{1}_{M \xrightarrow{.} M}. \end{aligned}\] Thus we can notice that the pair of operations (composition \(\circ\) and Horizontal composition \(\star\)) forms the bifunctor (see Bifunctor in the category of functors).

The morphism \(\mathbf{1}_{M \xrightarrow{.} M} \star \mu\) acts on \(M \circ ( M \circ M )\) as \[\mathbf{1}_{M \xrightarrow{.} M} \star \mu : M \circ ( M \circ M ) \xrightarrow{.} M \circ M\] thus \[\mu \circ (\mathbf{1}_{M \xrightarrow{.} M} \star \mu) : M \circ ( M \circ M ) \xrightarrow{.} M.\] Similarly \[\mu \circ (\mu \star \mathbf{1}_{M \xrightarrow{.} M}) : (M \circ M) \circ M \xrightarrow{.} M.\] I.e. the both morphisms start at the same object \(M^3\) and finish also at the same point. The equality \[\mu \circ (\mathbf{1}_{M \xrightarrow{.} M} \star \mu) = \mu \circ (\mu \star \mathbf{1}_{M \xrightarrow{.} M})\] is similar to the conditions on the Associativity and can be written as Category of endofunctors. Thus if we compare (Category of endofunctors) and (Monoid) then we can say that they are same if we replace \(\star\) sign with \(\times\) one. I.e. in the case we can say that the monad looks like a Monoid.

For the identity element consider the same trick: replace in (Monoid) tensor product \(\times\) with Horizontal composition \(\star\) and morphisms \(\mathbf{1}_{M \to M}, \rho, \lambda\) with identity natural transformation \(\mathbf{1}_{M \xrightarrow{.} M}\). Thus the equation \[\mu \circ (\eta \times \mathbf{1}_{M \to M}) \circ \lambda = \mu \circ (\mathbf{1}_{M \to M} \times \eta) \circ \rho = \mathbf{1}_{M \to M}\] will be replaced with \[\mu \circ (\eta \star \mathbf{1}_{M \xrightarrow{.} M}) = \mu \circ (\mathbf{1}_{M \xrightarrow{.} M} \star \eta) = \mathbf{1}_{M \xrightarrow{.} M}\] that is the exact we want to get (see second equation of (Category of endofunctors)).

Monads in programming languages

There are several examples of Monad implementation in different programming languages:

Haskell

    class Functor m => Monad m where
        return :: a -> m a
        (>>=)  :: m a -> (a -> m b) -> m b

    class Functor m => Monad m where
        return :: a -> m a
        join  :: m (m a) -> m a

(>>=)  :: m a -> (a -> m b) -> m b
ma >>= f = join ( fmap f ma )

As an application of the last example lets consider the next one

joinHeads :: [[a]] -> [a]
joinHeads ys = ys >>= \xs -> [head xs]

> joinHeads ["a123", "b123", "c123"]
"abc"

> fmap (\xs -> [head xs]) ["a123", "b123", "c123"]
["a","b","c"]

C++

The monad in C++ use the functor definition from Functor

// from functor.h
template < template< class ...> class M, class A, class B> 
M<B> fmap(std::function<B(A)>, M<A>);

// file: monad.h
template < template< class ...> class M, class A> 
M<A> pure(A);

template < template< class ...> class M, class A> 
M<A> join(M< M<A> >);

where pure can be treated as \(\eta\) (Monad) and join as \(\mu\) (Monad). In the case the bind operator can be implemented as follows

template < template< class ...> class M, class A, class B> 
M<B> bind(std::function< M<B> (A) > f, M<A> a) {
  return join( fmap<>(f, a) );
};

Scala

trait M[A] {
  def flatMap[B](f: A => M[B]): M[B]
}
  
def unit[A](x: A): M[A]