Monad: to programming from category theory

We have seen the summarized article "monad in programming" in the previous post.

Let's find out what is a monad in category theory and how the concept became relevant for functional programming.

First, we need to understand the basics of category theory.

Category

A category consists of objects and morphisms (relationships) between those objects. More of it, the morphisms should be composable too.

Below is an example of a category.

Each dot is an object and each arrow shows morphism from some object to another. As arrows are composable, if there is a morphism from object a to object b, and there is another morphism from b to c, then we can find a morphism from a to c. 

If you notice, there is identity morphism too, it exists for each object, but we have shown it just for x. It is a morphism from an object to itself. If we compose identity morphism with any other morphism w, we get the same w in return.

Functor

A functor is a relationship between categories. Suppose, there are two categories C and D, if we could find functor F from category C to category D, the functor maps each object from C to another object in D. It also maps each morphism from C to another morphism in D. 

Suppose, there are objects a and b in category C, and there is a morphism f from a to b. If we have a functor F from category C to category D, we can map a to Fa, b to Fb, and f to Ff using functor F.

In category C, we have

So, using functor F, we can find a morphism Ff from Fa to Fb in category D.

Here, we can derive Ff using f.

 

The syntax says that we need Fa to be passed in Ff, in return we will get a function that requires f as an argument, using the f and Fa we can get Fb. Ff is called map or fmap in programming languages.

Let's dig down functor a little bit more,

As each object has its identity morphism, so we have

If we apply functor F to the morphism, we get

The above one is the same as finding identity morphism from Fa to Fa. 

So, 

   Equation 1

Now, suppose, there are two morphisms in C

For these, we have two mapped  morphisms in D.

If we find out the composed morphism for f and g.

and if we map the composed one to D using functor F, we get

This is the same as, directly composing Ff and Fg.

So, we can say that

Equation 2

Equations 1 and 2 are requirements of some F to be a functor.

Endofunctor 

 

Endofunctor is a functor that maps a category to itself. This type of functor maps an object from a category to some other object in the same category, or simply maps to the same object in the same category. The second type of endofunctor is also known as identity functor. 

We have shown here two endofunctors.  I_C is an identity functor and E is an endofunctor that maps a to Ea, b to Eb, and f to Ef in the same category.

Natural transformation

Natural transformation is a relationship between functors.

Suppose, there are two functors F and G from category C to D.

 We get below morphisms in category D.

Natural transformation exists if we could find some morphism components of the transformation in the target category.

If we could find out morphisms from  Fa to Gb, we can say that we have a natural transformation from F to G. How is that true? Since we already have morphisms from Fa to Fb, and from Ga to Gb, we just need to have morphisms from Fa to Ga, and Fb to Gb. Let's call that morphisms α_a and α_b.

Here, α_a leads us from Fa to Ga, and α_b leads us from Fb to Gb, so we can say that α is a natural transformation from functor F to functor G.  α_a and α_b  are morphism components of natural transformation α on objects a and b respectively.

Now, to reach from Fa to Gb, we have two composed morphisms as below.

Natural transformations are composable too, as components of natural transformation are morphisms in some category, and morphisms are composable, so natural transformations are too.

There are two types of compositions for natural transformations, vertical and horizontal. Let's see vertical composition first.

Vertical composition of natural transformations

 

For f in C, we have below morphism in D.

We have natural transformations too.

If we could find out morphisms from Fa to Hb, composed using components of α and β. We can say that transformations α and β are composable. α and β are vertically aligned as shown in the figure, so the composition is called vertical composition. 

Now, to reach from Fa to Hb we can derive three morphisms using the above information. 

Horizontal composition of natural transformations

Suppose there are three categories C, D, and E. There are two functors F and F' from C to D, and two functors G and G' from D to E.

 

For f in C, we have below morphisms in D.

And in E, we have

We have below natural transformations too.

Now, if we could find out morphisms from G(Fa) to G'(F'b), composed using components of α and β. Then, we can say that transformations α and β are composable. It is called horizontal composition as α and β are horizontally aligned in the above figure.

As per the figure, there are six morphisms we can find from G(Fa) to G'(F'b).

These are all relationships between GF to G'F', so we can define the horizontal composition as

Usage of horizontal composition

Let's consider a different scenario where two functors are not in the same direction, they are in opposite directions. More of it, each category also has its identity functor.

Suppose we have a functor F going from C to D and another functor G from D to C. We have an object x in C, we can get Fx in D using F. And then, we can get GFx from Fx using G in C. Now, x and GFx are in the same category C. We can say that we applied composed functor GF to x and got GFx in the same category. Recall that composed functor GF is an endofunctor, as it maps category C to itself.

Same way, if we have y in category D, we have below configuration

We get Gy in C for y in D using G, and FGy in D for Gy in C using F. We have an endofunctor FG for D.

Now, we want to define some special morphisms in both categories. Those morphisms are from x to GFx in C, and FGy to y in D. Let's see how we can define those morphisms using horizontal composition.

For simplicity, we might think of something like this for category C to work on.

Suppose, we have natural transformation α and β from identity functor I_C to F and G respectively. If we have composed functor GF, we can have horizontally composed natural transformation β ◦  α.

 

Let's consider category C first.

Here, we define identity morphism from x to x, and GFx to GFx, which is obvious. We have identity functor I_C which maps x to x and id_x to id_x. We have another composed functor GF which maps x to GFx and id_x to id_GFx. If we have a morphism from x to GFx, we can have a transformation from I_C to GF.

So,

Same way, we can think of something like this for category D.

Suppose, we have natural transformation α and β from F and G respectively to identity functor I_D. If we have composed functor FG, we can have horizontally composed natural transformation β ◦  α.

Now, let's consider category D.

Here, we want to define morphism from FGy to y. The reason behind defining morphism from the target object to the source object will be revealed shortly. Suppose, we have morphism from FGy to y, we can have transformation from FG to I_D.

So,

Adjunction

We have two categories C and D, and have objects x and y respectively in that. Functor F is going from C to D and functor G does the opposite.

We got Gy in C for y in D using G, and we got Fx in D for x in C using F. 

If we have morphism f from Fx to y in D and if we can find out morphism f' from x to Gy in C, We can say that functor F is left adjoint to G, and G is right adjoint to F.

Let's see, in what condition we can find out f' and can conclude that the above relation is an adjunction.

We have below morphism in category D.

 

So, if we apply functor G to the morphism, we can get

in category C.

As it must have f' to be an adjunction, category C must have morphism η_x from x to GFx.

So we can compose the η_x with Gf.

And got morphism f' from x to Gy.

 

Let's not stop here and further explore something.

If we apply F to f', we get morphism Ff' from Fx to FGy.

If we have morphism from FGy to y. (Target to source)

Composing the ε_y with Ff' we can get back our original morphism f.

Just for fun exercise, we can put Fx to both sides of the equation, and we can prove that,

Which is true. 

If F is left adjoint to G and G is right adjoint to F, we must have f and f' in categories D and C respectively. If we have f, and to prove that that we also have f', we must have η_x and ε_y in categories C and D respectively. η_x is a component of transformation η, and ε_y is a component of ε. Here, transformations η is called unit and ε is called counit of the adjunction.

Monad and Comonad

Monad and Comonad emerge from Adjunction.

If we found below transformations in category C then endofunctor GF is a monad.

Here, η is called unit, and μ is called multiplication of the monad.

If we found below transformations in category D then endofunctor FG is a comonad.

 

Here, ε is called counit, and δ is called extraction of the comonad.

How can we find  μ and ε transformations in the above adjunction?

Let's extend that figure and explore more.

We have η_x as a component of η. We can find a component on Gy as η_Gy in category C.

If we apply functor F to the morphism, we get

Let's call it

We have found a component of transformation δ in category D using η_Gy. So, we can have a transformation

Same way, we can find a component of ε on Fx as ε_Fx in category D.

If we apply functor G to the morphism, we get

Let's call it

We have found a component of transformation μ in category C using ε_Fx. So, we can have a transformation

 

Now, we have all transformations for GF to be a monad and FG to be a comonad.

So, endofunctor GF is a monad, if we have below transformations.

And, endofunctor FG is a comonad, if we have below transformations.

Relevance of monad in programming

Let's denote functor as F, monad as M, and comonad as W. 

So, for monad

And, for comonad

If we think of objects in a category as datatypes in a programming language. We can define two kinds of datatypes, normal and lifted. If the normal datatype is a then the lifted datatype can be Fa or Ma according to whatever functor or monad we apply to it.

When we work with a functor, we always have lifted value Fa and after some operation, we would get Fb. Though we have normal function f from a to b as an underlying operation, we would not have access to a or b outside functor F. We always work with lifted values while we work with a functor. This is the limitation of a functor.

Monad solves the problem of lifting normal value to lifted value, as Monad has η.

Now, we can work with a function where argument is a normal value and return value is a lifted value.

Now, problem is, how to compose this kind of functions as composition does not seem straightforward.

We might need a function that can accept Ma and gives us back a. But, unfortunately, we do not have one.

Okay. Do we have a function which accepts MMa and returns Ma? 

Yes, we have. It is μ.

So, we can rearrange the composition as

If you notice, that MMc to Mc is μ.

Can we simplify it more? As monad is a functor too. We can rearrange it as

So, if we have η and μ, and monad is a functor too, using all this, we can compose functions that accept a normal value and return a lifted value.

Now, here we encounter the limitation cum beauty of monad is, we can't get value out of monad. We can convert a normal value to a lifted one, but not vice versa.

The beauty is, we actually do not need the value, as once we entered into a monad realm we need to stay there until we come out of the functional world (See, the previous post for detail).

Comonad is the opposite concept, as we can get normal value out of lifted value, but can't do otherwise. This is not that much explored concept in programming, yet we will derive composition for it.

Happy learning!!!

References

https://bartoszmilewski.com/2014/10/28/category-theory-for-programmers-the-preface/

https://www.andrew.cmu.edu/course/80-413-713/notes/chap10.pdf