brucou/my_introduction_to_monads

## my_introduction_to_monads
[TOC]


# Introduction
As many before me, I have struggled (and probably continue to struggle) with the concept of monads and comonads. I reviewed a large number of tutorials presenting the concept in many different ways. I think I found a way that works for me, at least for monads, and I wanted to detail that in what follows with the hope that it will be useful for others too[^1].

[^1]: Note that I am referring to monads in the context of computer science and programming. While this is obviously linked to monads in category theory, the presentation of the latter is much more abstract, and I do not deal with that here.

Now, I am trying to end the struggle with :

- comonads
- functor algebra
- coalgebras
- abstract state machine

Maybe one day I will win over :

- zippers
- fold and traversable, in particular the separation between content and structure

# Function composition
Let's review the function composition operator ($\circ$) :

- $\forall  h : U \rightarrow A, g : A \rightarrow B, f : B \rightarrow C $
  - (existence and definition) : $\exists f \circ g : A \rightarrow C $
  - right identity : $\forall A, \exists Id_A : A \rightarrow A $ such that $f \circ Id_A = f$
  - left identity : $\forall B, \exists Id_B : B \rightarrow B $ such that $Id_B  \circ g= g$
  - associativity : $f \circ (g \circ h) = (f \circ g) \circ h$

As we can see from this definition, to be able to compose two functions, the codomain of one must equal to the domain of the other.

# Generalizing function composition
## Equational reasoning
Would we able to compose two functions $f$ and $g$ such that the resulting operation have the same property as the standard function composition operator $\circ$?
$$ f : C \rightarrow D$$ $$g : A \rightarrow B $$ $$ \exists \bullet,  (f,  g) \rightarrow f\bullet g$$

A necessary condition would be to have what we call an extension function $\eta$, such that, for all such $f$ and $g$, $ \eta(f,g) = f \odot g : B \rightarrow C$, and:

$$ f \bullet g = f \circ (f \odot g) \circ g$$

Basically $\eta$ does the linking between the codomain and domain of the functions to compose, and allows to use the standard function composition.

Of course we also want the $\bullet$ operator to satisfy the equations for the standard composition operator $\circ$.

What we quickly realize is that, we cannot have $\eta$ defined for all $f$ and $g$. If for instance, we take a $g : A \rightarrow 1$, i.e. a function $g$ which assign any element to a constant ; and a $f : C \rightarrow D$ where $C$ is a set with more than one element, then such a $\eta$ cannot associate the single element of $1$ to two elements of $C$. In fact this will be true anytime we have a $g$ codomain which is smaller than a $f$ domain.

This leads us to consider to abandon the general case and consider more restricted cases. To increase our chances, we will examine the case when $B$ and $C$ are into a relation of some form. We know that $B = C$ trivially works. We will extend that by analyzing the conditions for existence of a $\bullet$ composition operator when $B$ and $C$ are functionally related. Let $T$ be such a function :

$$ \forall A, T : A \rightarrow T(A) $$

We will write in what follows $TA$ for the image of $A$ by $T$, instead of $T(A)$. So we seek :

$$ f : B \rightarrow C $$ $$ g : A \rightarrow TB $$ $$ f \bullet g : A \rightarrow C$$

The first realization to come to, is that, in order to compose more than two functions, it is nicer to have $f$ to be of the same shape as $g$, i.e.$ f : B \rightarrow TC $. For instance :

$$ f : B \rightarrow TC $$ $$ g : A \rightarrow TB $$ $$ h : U \rightarrow TA $$ $$ f \bullet g \bullet h : U \rightarrow TC$$

The requirement for right identity can be written as follows :

$\forall A, \exists Id_A : A \rightarrow TA $ such that $f \bullet Id_A = f$

The requirement for left identity can be written as follows :

$\forall B, \exists Id_B : B \rightarrow TB $ such that $Id_B  \bullet g= g$

We called $\eta$ again the extension function $\eta(f) : TB \rightarrow TC$ which allows us to express the extended composition operator $\bullet$ to the standard one $\circ$ :
$$f \bullet g = \eta(f) \circ g$$

The left identity can then be written as :

$$ Id_B  \bullet g= g $$  or $$ \eta(Id_B)  \circ g= g $$ This implies the following sufficient condition on $\eta$ : $$ \forall B, \eta(Id_B)  = Id_{TB} $$

In summary the left and right identity gives us the following :

$$ \forall A, \exists Id_A : A \rightarrow TA $$ $$ \forall f : B \rightarrow TC, \exists \eta(f) : TB \rightarrow TC $$ $$ \forall A, \eta(Id_A)  = Id_{TA} $$

Let's see the implications of the associativity :

$$ f \bullet(g \bullet h) = (f \bullet g) \bullet h$$

This means :

$$ \eta(f) \circ (\eta(g) \circ h) = \eta((\eta(f) \circ g)) \circ h$$
or, removing the parenthesis :
$$ \eta(f) \circ \eta(g) \circ h = \eta(\eta(f) \circ g) \circ h$$

We get another sufficient condition on $\eta$ :
$$ \eta(f) \circ \eta(g) = \eta(\eta(f) \circ g) $$

In summary, our sufficient conditions are :
$$ \forall A, \exists Id_A : A \rightarrow TA $$ $$ \forall f : B \rightarrow TC, \exists \eta(f) : TB \rightarrow TC $$ $$ \forall A, \eta(Id_A)  = Id_{TA} $$ $$ \eta(f) \circ \eta(g) = \eta(\eta(f) \circ g) $$

This is exactly the definition of a monad. If one can find a suitable $T$, $\eta$, and $Id$, which satisfy the previous equations, then we can define a composition operator operating on functions of the form $A \rightarrow TB$ :
$$ \bullet : (f,g) \rightarrow f \bullet g = \eta(f) \circ g $$

Hence, as one can see, a monad is a triple $(T, Id, \eta)$ which allows to compose functions $A \rightarrow TB$. Alternatively, a monad can also be seen as a triple $(T, Id, \bullet)$. Whatever equations which the triple must satisfy are dictated by the necessity to abide by the composition operator laws.

The same way, one can show that a comonad is also a triple which allows in fine to compose functions $TA \rightarrow B$.

### Links with other definitions
We can also express $fmap$, and the $bind$ operator $>>=$ succinctly:

$fmap f  = \eta(Id_\bullet \circ f)$
$(f \bullet g) (x) = bind(g(x), f) =  g(x) >>= f = f <<= g(x)$

The last equation shows how $bind$ can  be understood as the function application operator for $\bullet$, also called monadic application.

## Derived types
Given a function $T$ which takes a type and returns another type, i.e. $T : A \rightarrow T(A)$, we will note $T(A) = TA$, and say that $TA$ type is derived from $A$, or that the $TA$ is a $T$-derived type. We will call $A$ the underlying type of $TA$.

In the general case, $T$ can be anything. It is not very helpful to try to get an 'intuition' of $T$, the same way as it is not very fruitful to get an intuition about a function. Some functions will give you the next best move in a game of go, others will convert an integer to a string. A function is a set of relations between two things (input and output), and that is always going to be abstract, like anything in algebra.

So we have a function between sets, i.e. in the context of programming, a function between types. A type itself is a set of objects, which are abstract representations of actual things. So the type of `PositiveInt` is the set of objects $\{0, 1, 2, 3...\}$ where $1$ represent the value 1 for a given interpreting machine. If the machine has a 32 bits processor, then the last object of `PositiveInt` will be $2^{32} -1$.

Essentially objects of a type can represent anything, as long as the interpreting machine can understand its meaning. For instance :

- we can represent failure by the element $Nothing$. We can define a failure type $Nothing$ to be a singleton $\{Nothing\}$. For any computation $f : A \rightarrow B$ which can fail, we can define $f' : A \rightarrow B \cup Nothing$, which extend the $f$ computation by including its possible failure result. This means here we could have a function between types and extended types, such that the extension includes the failure type, i.e. $\forall A, T : A \rightarrow A \cup Nothing$.
- The command to print "Hello" can be represented by $\{Print\ Hello\}$, as long as it is understood as such by the interpreter. So we can imagine a `printStr` function between strings, so that $\forall str \in Str, printStr (str) = Print\ str$. If we call the image of that function `PrintStr`, we have $printStr : Str \rightarrow Print Str$. If there are other things of type $A$ which can be printed, i.e. which can be understood by the interpreter as printable, we can define a $printA$ for any such $A$ whose image will be named $PrintA$. We can then define a more generic function $\forall A, T: A \rightarrow Print A$, where $A$ is a set of printable objects, $PrintA$ is the image of the associated printing function for elements of that set. Now, a better name for $T$ would be $DoPrint$, as it is a function between types whose elements can be printed, and the set whose elements are the representation of the command to the interpreter to print those elements.
- $T$ could be an extension operation over types. The first example extends a type by one element. $T$ could be a wrapping operation ($Array$ for instance). $T$ could be anything really, and the meaning of $TA$ will depend on each $T$.

Note that if we have a function $T$ over types, and we can find a function which maps computation between underlying types to computation between derived types, then that function is unique[^2]. The mapping function is generally called $fmap$, and $(T, fmap)$ is then called a functor :

$$ fmap : (A \rightarrow B) \rightarrow (TA \rightarrow TB)$$

[^2]: Theorems for free! Philip Wadler. 4'th International Conference on Functional Programming and Computer Architecture, London, September 1989.


## Examples
We have shown a necessary condition for a $\bullet$ composition operator which generalizes the $\circ$ composition operator to exist. But can we indeed satisfy those conditions? Let's see a few examples.

### T(A) = A
This is a pretty trivial case, in which $\circ = \bullet$. The $(T, \eta, Id)$ is as follows :

$$ \forall A, \forall x, Id_A(x) = x $$ $$ \forall f, \eta(f) = f$$

### T(A) = A + 1
This is a less trivial case but still relative simple. A quick reminder about set notation, $1$ denotes the singleton set. Let write $1 = \{Nothing\}$, i.e. we call $Nothing$ the single element of the singleton set. The $+$ operator here is the set union operator.
In that case $f : A \rightarrow B + 1 \implies \eta(f) : A + 1 \rightarrow B + 1$. We then define $\eta$ and $Id_A$ as follows :

$$ \forall A, \forall x \in A, Id_A(x) = x $$ $$ \forall f : A \rightarrow B + 1, \forall x \in A, \eta(f)(x) = f(x)  $$ $$ \forall f : A \rightarrow B + 1, \eta(f)(Nothing) = Nothing$$

One can trivially check that the equations hold. Hence given $g : A \rightarrow B + 1$, and $f : B \rightarrow C + 1$, $\forall x \in A, f \bullet g (x) = \eta(f) \circ g(x)$, i.e. :

$$ g(x) = Nothing \implies f \bullet g(x) = Nothing$$ $$ g(x) \neq Nothing \implies f \bullet g(x) = f \circ g (x)$$

One will of course have recognized by now the **Maybe** monad, which allows to compose functions which can produce a value or not, i.e. computations which can succeed or not.

### TA = E $\rightarrow$ A
This is a bit more complicated. We have $g : A \rightarrow (E \rightarrow B)$, $f : B \rightarrow (E \rightarrow C)$. We want $f \bullet g : A \rightarrow (E \rightarrow C)$. We define :

$$ \forall A, \forall x \in A, Id_A(x) = \lambda\_ \to x$$ $$ \forall x \in E \rightarrow B, \eta(f)(x) = \lambda e \rightarrow f(x(e))(e)$$

Substituting the $Id_A$ for its value gives us $ \eta(Id_A)(x) = \lambda e \rightarrow x(e) $, which means $ \eta(Id_A)(x) = x$. The identity equation is then satisfied.

Checking the last equation : $ \eta(f) \circ \eta(g) = \eta(\eta(f) \circ g) $ is more arduous but is also achieved by substitution.

One will have recognize the **Reader** monad, which allows to compose computations that use values from an environment $E$. To see why this is the case, one can rewrite $f : B \rightarrow (E \rightarrow C)$ as $f : B \rightarrow E \rightarrow C$, and see $f$ as a computation taking two inputs, one of which is the environment.

### Others Ts
Among others, the following type functions $T$ are commonly used :

- TA = S $\rightarrow$ A $\times$ S (state monad)
- TA = A $+$ E (exceptions monad)
- TA = (A $\rightarrow$ R) $\rightarrow$ R (continuation monad)
- TA = W $\times$ A, with W equipped with monoid operation (writer monad)

I leave to the reader as an exercise to explicit the specific form of each of the mentioned monads.

# How is that useful?
In the previous sections, we have used an explicit $T$ and constructed an associated monad. In practice, however, it happens the other way around. One observes that some functions should compose, but cannot be composed directly because the domain and codomain do not match. After doing the composition by hand repeatedly, one can decide to use a monad abstraction and express computations more succinctly, clearly and without repetition (DRY). Monads can as a matter of fact be reused in many different contexts.

On the other hand, given that the most useful monads have already been explicited, one can (re)use them as a library for handling different concerns (error, exceptions, state, etc.).

In short, if there is only one thing to understand from monad, is that it is an abstraction which allows to compose functions of a specific shape. It is unnecessary to  try and get an intuition of  $TA$ *values* because there isn't any, in general. There is not as a matter of fact a monad for every $T$. What is important to understand are monadic functions (the $f : A \rightarrow TB$), which are $T$-enhanced computations (they compute values related to an underlying type), and the fact that those monadic functions compose thanks to the monadic $\bullet$ composition operator.

What is even more important in the day to day programming is to understand how to use the available monads, and how to recognize new ones when they occur.

# Further readings
I recommend also reading [this introductory article](http://blog.sigfpe.com/2006/08/you-could-have-invented-monads-and.html) , which builds monads from the concrete to the abstract, i.e. the reverse approach that I have adopted here. I believe doing it both ways should made things more clear.

> Written with [StackEdit](https://stackedit.io/).
	[TOC]


	# Introduction
	As many before me, I have struggled (and probably continue to struggle) with the concept of monads and comonads. I reviewed a large number of tutorials presenting the concept in many different ways. I think I found a way that works for me, at least for monads, and I wanted to detail that in what follows with the hope that it will be useful for others too[^1].

	[^1]: Note that I am referring to monads in the context of computer science and programming. While this is obviously linked to monads in category theory, the presentation of the latter is much more abstract, and I do not deal with that here.

	Now, I am trying to end the struggle with :

	- comonads
	- functor algebra
	- coalgebras
	- abstract state machine

	Maybe one day I will win over :

	- zippers
	- fold and traversable, in particular the separation between content and structure

	# Function composition
	Let's review the function composition operator ($\circ$) :

	- $\forall h : U \rightarrow A, g : A \rightarrow B, f : B \rightarrow C $
	- (existence and definition) : $\exists f \circ g : A \rightarrow C $
	- right identity : $\forall A, \exists Id_A : A \rightarrow A $ such that $f \circ Id_A = f$
	- left identity : $\forall B, \exists Id_B : B \rightarrow B $ such that $Id_B \circ g= g$
	- associativity : $f \circ (g \circ h) = (f \circ g) \circ h$

	As we can see from this definition, to be able to compose two functions, the codomain of one must equal to the domain of the other.

	# Generalizing function composition
	## Equational reasoning
	Would we able to compose two functions $f$ and $g$ such that the resulting operation have the same property as the standard function composition operator $\circ$?
	$$ f : C \rightarrow D$$ $$g : A \rightarrow B $$ $$ \exists \bullet, (f, g) \rightarrow f\bullet g$$

	A necessary condition would be to have what we call an extension function $\eta$, such that, for all such $f$ and $g$, $ \eta(f,g) = f \odot g : B \rightarrow C$, and:

	$$ f \bullet g = f \circ (f \odot g) \circ g$$

	Basically $\eta$ does the linking between the codomain and domain of the functions to compose, and allows to use the standard function composition.

	Of course we also want the $\bullet$ operator to satisfy the equations for the standard composition operator $\circ$.

	What we quickly realize is that, we cannot have $\eta$ defined for all $f$ and $g$. If for instance, we take a $g : A \rightarrow 1$, i.e. a function $g$ which assign any element to a constant ; and a $f : C \rightarrow D$ where $C$ is a set with more than one element, then such a $\eta$ cannot associate the single element of $1$ to two elements of $C$. In fact this will be true anytime we have a $g$ codomain which is smaller than a $f$ domain.

	This leads us to consider to abandon the general case and consider more restricted cases. To increase our chances, we will examine the case when $B$ and $C$ are into a relation of some form. We know that $B = C$ trivially works. We will extend that by analyzing the conditions for existence of a $\bullet$ composition operator when $B$ and $C$ are functionally related. Let $T$ be such a function :

	$$ \forall A, T : A \rightarrow T(A) $$

	We will write in what follows $TA$ for the image of $A$ by $T$, instead of $T(A)$. So we seek :

	$$ f : B \rightarrow C $$ $$ g : A \rightarrow TB $$ $$ f \bullet g : A \rightarrow C$$

	The first realization to come to, is that, in order to compose more than two functions, it is nicer to have $f$ to be of the same shape as $g$, i.e.$ f : B \rightarrow TC $. For instance :

	$$ f : B \rightarrow TC $$ $$ g : A \rightarrow TB $$ $$ h : U \rightarrow TA $$ $$ f \bullet g \bullet h : U \rightarrow TC$$

	The requirement for right identity can be written as follows :

	$\forall A, \exists Id_A : A \rightarrow TA $ such that $f \bullet Id_A = f$

	The requirement for left identity can be written as follows :

	$\forall B, \exists Id_B : B \rightarrow TB $ such that $Id_B \bullet g= g$

	We called $\eta$ again the extension function $\eta(f) : TB \rightarrow TC$ which allows us to express the extended composition operator $\bullet$ to the standard one $\circ$ :
	$$f \bullet g = \eta(f) \circ g$$

	The left identity can then be written as :

	$$ Id_B \bullet g= g $$ or $$ \eta(Id_B) \circ g= g $$ This implies the following sufficient condition on $\eta$ : $$ \forall B, \eta(Id_B) = Id_{TB} $$

	In summary the left and right identity gives us the following :

	$$ \forall A, \exists Id_A : A \rightarrow TA $$ $$ \forall f : B \rightarrow TC, \exists \eta(f) : TB \rightarrow TC $$ $$ \forall A, \eta(Id_A) = Id_{TA} $$

	Let's see the implications of the associativity :

	$$ f \bullet(g \bullet h) = (f \bullet g) \bullet h$$

	This means :

	$$ \eta(f) \circ (\eta(g) \circ h) = \eta((\eta(f) \circ g)) \circ h$$
	or, removing the parenthesis :
	$$ \eta(f) \circ \eta(g) \circ h = \eta(\eta(f) \circ g) \circ h$$

	We get another sufficient condition on $\eta$ :
	$$ \eta(f) \circ \eta(g) = \eta(\eta(f) \circ g) $$

	In summary, our sufficient conditions are :
	$$ \forall A, \exists Id_A : A \rightarrow TA $$ $$ \forall f : B \rightarrow TC, \exists \eta(f) : TB \rightarrow TC $$ $$ \forall A, \eta(Id_A) = Id_{TA} $$ $$ \eta(f) \circ \eta(g) = \eta(\eta(f) \circ g) $$

	This is exactly the definition of a monad. If one can find a suitable $T$, $\eta$, and $Id$, which satisfy the previous equations, then we can define a composition operator operating on functions of the form $A \rightarrow TB$ :
	$$ \bullet : (f,g) \rightarrow f \bullet g = \eta(f) \circ g $$

	Hence, as one can see, a monad is a triple $(T, Id, \eta)$ which allows to compose functions $A \rightarrow TB$. Alternatively, a monad can also be seen as a triple $(T, Id, \bullet)$. Whatever equations which the triple must satisfy are dictated by the necessity to abide by the composition operator laws.

	The same way, one can show that a comonad is also a triple which allows in fine to compose functions $TA \rightarrow B$.

	### Links with other definitions
	We can also express $fmap$, and the $bind$ operator $>>=$ succinctly:

	$fmap f = \eta(Id_\bullet \circ f)$
	$(f \bullet g) (x) = bind(g(x), f) = g(x) >>= f = f <<= g(x)$

	The last equation shows how $bind$ can be understood as the function application operator for $\bullet$, also called monadic application.

	## Derived types
	Given a function $T$ which takes a type and returns another type, i.e. $T : A \rightarrow T(A)$, we will note $T(A) = TA$, and say that $TA$ type is derived from $A$, or that the $TA$ is a $T$-derived type. We will call $A$ the underlying type of $TA$.

	In the general case, $T$ can be anything. It is not very helpful to try to get an 'intuition' of $T$, the same way as it is not very fruitful to get an intuition about a function. Some functions will give you the next best move in a game of go, others will convert an integer to a string. A function is a set of relations between two things (input and output), and that is always going to be abstract, like anything in algebra.

	So we have a function between sets, i.e. in the context of programming, a function between types. A type itself is a set of objects, which are abstract representations of actual things. So the type of `PositiveInt` is the set of objects $\{0, 1, 2, 3...\}$ where $1$ represent the value 1 for a given interpreting machine. If the machine has a 32 bits processor, then the last object of `PositiveInt` will be $2^{32} -1$.

	Essentially objects of a type can represent anything, as long as the interpreting machine can understand its meaning. For instance :

	- we can represent failure by the element $Nothing$. We can define a failure type $Nothing$ to be a singleton $\{Nothing\}$. For any computation $f : A \rightarrow B$ which can fail, we can define $f' : A \rightarrow B \cup Nothing$, which extend the $f$ computation by including its possible failure result. This means here we could have a function between types and extended types, such that the extension includes the failure type, i.e. $\forall A, T : A \rightarrow A \cup Nothing$.
	- The command to print "Hello" can be represented by $\{Print\ Hello\}$, as long as it is understood as such by the interpreter. So we can imagine a `printStr` function between strings, so that $\forall str \in Str, printStr (str) = Print\ str$. If we call the image of that function `PrintStr`, we have $printStr : Str \rightarrow Print Str$. If there are other things of type $A$ which can be printed, i.e. which can be understood by the interpreter as printable, we can define a $printA$ for any such $A$ whose image will be named $PrintA$. We can then define a more generic function $\forall A, T: A \rightarrow Print A$, where $A$ is a set of printable objects, $PrintA$ is the image of the associated printing function for elements of that set. Now, a better name for $T$ would be $DoPrint$, as it is a function between types whose elements can be printed, and the set whose elements are the representation of the command to the interpreter to print those elements.
	- $T$ could be an extension operation over types. The first example extends a type by one element. $T$ could be a wrapping operation ($Array$ for instance). $T$ could be anything really, and the meaning of $TA$ will depend on each $T$.

	Note that if we have a function $T$ over types, and we can find a function which maps computation between underlying types to computation between derived types, then that function is unique[^2]. The mapping function is generally called $fmap$, and $(T, fmap)$ is then called a functor :

	$$ fmap : (A \rightarrow B) \rightarrow (TA \rightarrow TB)$$

	[^2]: Theorems for free! Philip Wadler. 4'th International Conference on Functional Programming and Computer Architecture, London, September 1989.


	## Examples
	We have shown a necessary condition for a $\bullet$ composition operator which generalizes the $\circ$ composition operator to exist. But can we indeed satisfy those conditions? Let's see a few examples.

	### T(A) = A
	This is a pretty trivial case, in which $\circ = \bullet$. The $(T, \eta, Id)$ is as follows :

	$$ \forall A, \forall x, Id_A(x) = x $$ $$ \forall f, \eta(f) = f$$

	### T(A) = A + 1
	This is a less trivial case but still relative simple. A quick reminder about set notation, $1$ denotes the singleton set. Let write $1 = \{Nothing\}$, i.e. we call $Nothing$ the single element of the singleton set. The $+$ operator here is the set union operator.
	In that case $f : A \rightarrow B + 1 \implies \eta(f) : A + 1 \rightarrow B + 1$. We then define $\eta$ and $Id_A$ as follows :

	$$ \forall A, \forall x \in A, Id_A(x) = x $$ $$ \forall f : A \rightarrow B + 1, \forall x \in A, \eta(f)(x) = f(x) $$ $$ \forall f : A \rightarrow B + 1, \eta(f)(Nothing) = Nothing$$

	One can trivially check that the equations hold. Hence given $g : A \rightarrow B + 1$, and $f : B \rightarrow C + 1$, $\forall x \in A, f \bullet g (x) = \eta(f) \circ g(x)$, i.e. :

	$$ g(x) = Nothing \implies f \bullet g(x) = Nothing$$ $$ g(x) \neq Nothing \implies f \bullet g(x) = f \circ g (x)$$

	One will of course have recognized by now the Maybe monad, which allows to compose functions which can produce a value or not, i.e. computations which can succeed or not.

	### TA = E $\rightarrow$ A
	This is a bit more complicated. We have $g : A \rightarrow (E \rightarrow B)$, $f : B \rightarrow (E \rightarrow C)$. We want $f \bullet g : A \rightarrow (E \rightarrow C)$. We define :

	$$ \forall A, \forall x \in A, Id_A(x) = \lambda\_ \to x$$ $$ \forall x \in E \rightarrow B, \eta(f)(x) = \lambda e \rightarrow f(x(e))(e)$$

	Substituting the $Id_A$ for its value gives us $ \eta(Id_A)(x) = \lambda e \rightarrow x(e) $, which means $ \eta(Id_A)(x) = x$. The identity equation is then satisfied.

	Checking the last equation : $ \eta(f) \circ \eta(g) = \eta(\eta(f) \circ g) $ is more arduous but is also achieved by substitution.

	One will have recognize the Reader monad, which allows to compose computations that use values from an environment $E$. To see why this is the case, one can rewrite $f : B \rightarrow (E \rightarrow C)$ as $f : B \rightarrow E \rightarrow C$, and see $f$ as a computation taking two inputs, one of which is the environment.

	### Others Ts
	Among others, the following type functions $T$ are commonly used :

	- TA = S $\rightarrow$ A $\times$ S (state monad)
	- TA = A $+$ E (exceptions monad)
	- TA = (A $\rightarrow$ R) $\rightarrow$ R (continuation monad)
	- TA = W $\times$ A, with W equipped with monoid operation (writer monad)

	I leave to the reader as an exercise to explicit the specific form of each of the mentioned monads.

	# How is that useful?
	In the previous sections, we have used an explicit $T$ and constructed an associated monad. In practice, however, it happens the other way around. One observes that some functions should compose, but cannot be composed directly because the domain and codomain do not match. After doing the composition by hand repeatedly, one can decide to use a monad abstraction and express computations more succinctly, clearly and without repetition (DRY). Monads can as a matter of fact be reused in many different contexts.

	On the other hand, given that the most useful monads have already been explicited, one can (re)use them as a library for handling different concerns (error, exceptions, state, etc.).

	In short, if there is only one thing to understand from monad, is that it is an abstraction which allows to compose functions of a specific shape. It is unnecessary to try and get an intuition of $TA$ values because there isn't any, in general. There is not as a matter of fact a monad for every $T$. What is important to understand are monadic functions (the $f : A \rightarrow TB$), which are $T$-enhanced computations (they compute values related to an underlying type), and the fact that those monadic functions compose thanks to the monadic $\bullet$ composition operator.

	What is even more important in the day to day programming is to understand how to use the available monads, and how to recognize new ones when they occur.

	# Further readings
	I recommend also reading [this introductory article](http://blog.sigfpe.com/2006/08/you-could-have-invented-monads-and.html) , which builds monads from the concrete to the abstract, i.e. the reverse approach that I have adopted here. I believe doing it both ways should made things more clear.

	> Written with [StackEdit](https://stackedit.io/).