#### Howdy, Stranger!

It looks like you're new here. If you want to get involved, click one of these buttons!

Options

# [section3] Monads: definition, example and interpretation

edited February 2020

From the Wikipedia article on monads:

A monad on a category $$C$$ consists of an endofunctor $$T: C \rightarrow C$$ together with two natural transformations: $$\eta: 1_C \rightarrow T$$ (where $$1_C$$ denotes the identity functor on $$C$$) and $$\mu: T^2 \rightarrow T$$ (where $$T^2$$ is the functor $$T \circ T$$ from $$C$$ to $$C$$). These are required to fulfull the following "coherence" conditions:

$$\mu \circ T\mu = \mu \circ \mu T$$ (as natural transformations $$T^3 \rightarrow T$$;

$$\mu \circ T\eta = \mu \circ \eta T = 1_T$$ (as natural transformations $$T \rightarrow T$$; here $$1_T$$ denotes the identity transformation from $$T$$ to $$T$$.

See this section of the wikipedia article on natural transformations for the explanation of the notations $$T \mu$$ and $$\mu T$$.

• Options
1.
edited January 2020

The power set monad is monad on the category Set: For a set $$A$$ let $$T(A)$$ be the power set of $$A$$ (which consists of all subsets of $$A$$) and for a function $$f: A \rightarrow B$$ let $$T(f)$$ be the function between the power sets induced by taking direct images under $$f$$. For every set $$A$$, we have a map $$\eta_T: A \rightarrow T(A)$$, which assigns to every $$a \in A$$ the singleton $$\lbrace a \rbrace$$. The function:

$\mu_A: T(T(A)) \rightarrow T(A)$

takes a set of sets to its union. These data describe a monad.

Comment Source:Example: The power set monad The _power set monad_ is monad on the category Set: For a set \$$A\$$ let \$$T(A)\$$ be the power set of \$$A\$$ (which consists of all subsets of \$$A\$$) and for a function \$$f: A \rightarrow B\$$ let \$$T(f)\$$ be the function between the power sets induced by taking direct images under \$$f\$$. For every set \$$A\$$, we have a map \$$\eta_T: A \rightarrow T(A)\$$, which assigns to every \$$a \in A\$$ the singleton \$$\lbrace a \rbrace\$$. The function: \$\mu_A: T(T(A)) \rightarrow T(A)\$ takes a set of sets to its union. These data describe a monad. 
• Options
2.

Exercise: Prove this claim.

Comment Source:Exercise: Prove this claim.
• Options
3.
edited January 2020

We can break the proof up into components.

Proposition 1. T is a functor.

Proposition 2. $$\mu: T^2 \rightarrow T$$ is a natural transformation.

Proposition 3. $$\eta: 1_T \rightarrow T$$ is a natural transformation.

Proposition 4. $$\mu \circ T\mu = \mu \circ \mu T$$ (as natural transformations $$T^3 \rightarrow T$$)

Proposition 5. $$\mu \circ T\eta = \mu \circ \eta T = 1_T$$ (as natural transformations $$T \rightarrow T$$; here $$1_T$$ denotes the identity transformation from $$T$$ to $$T$$)

Comment Source:We can break the proof up into components. Proposition 1. T is a functor. Proposition 2. \$$\mu: T^2 \rightarrow T\$$ is a natural transformation. Proposition 3. \$$\eta: 1_T \rightarrow T\$$ is a natural transformation. Proposition 4. \$$\mu \circ T\mu = \mu \circ \mu T\$$ (as natural transformations \$$T^3 \rightarrow T\$$) Proposition 5. \$$\mu \circ T\eta = \mu \circ \eta T = 1_T\$$ (as natural transformations \$$T \rightarrow T\$$; here \$$1_T\$$ denotes the identity transformation from \$$T\$$ to \$$T\$$) 
• Options
4.

But before digging into the proofs, I'll take some space to unpack the definitions a bit. First I'll give a more elaborated explanation of the power set monad.

A monad T is a special kind of endofunctor $$T: C \rightarrow C$$ on a category $$C)$$.

In the case of the power set monad, $$C$$ is the category $$Set$$. The functor $$T: Set \rightarrow Set$$ is that which sends every set $$A$$ to its powerset $$2^A$$, defined as the set of all subsets of $$A$$.

Now to complete the definition of this functor, we need to specify how it acts on morphisms $$f: A \rightarrow B$$. Well, in our category $$Set$$, such a morphism $$f$$ is a function from set $$A$$ to set $$B$$. We need to define the result of applying functor $$T$$ to morphism $$f$$. Now, by the definition of a functor, $$T(f)$$ is required to be another function, of type $$T(f): T(A) \rightarrow T(B)$$. Which is to say, $$T(f): 2^A \rightarrow 2^B$$.

Now, given that we have a function $$f$$ mapping set $$A$$ into set $$B$$, what could this function $$T(f)$$ be, which must map $$2^A$$ into $$2^B$$?

Well a mapping from $$2^A$$ into $$2^B$$ is just another way of saying a function that maps subsets of $$A$$ to subsets of $$B$$.

Given that $$f$$ maps elements of $$A$$ to elements of $$B$$, there is a clear candidate for $$T(f)$$ mapping subsets of $$A$$ to subsets of $$B$$. Given a subset of $$A$$, the action of $$T(f)$$ will be to apply $$f$$ to every element of $$A$$ and collect the results to form a subset of $$B$$.

We say that $$T(f)$$ is the lifting of $$f: A \rightarrow B$$ to a function from $$2^A$$ to $$2^B$$:

$T(f)(A) = \lbrace f(x) | x \in A \rbrace$

This is referred to as the direct image of $$A$$ under $$f$$.

Comment Source:But before digging into the proofs, I'll take some space to unpack the definitions a bit. First I'll give a more elaborated explanation of the power set monad. A monad T is a special kind of endofunctor \$$T: C \rightarrow C\$$ on a category \$$C)\$$. In the case of the power set monad, \$$C\$$ is the category \$$Set\$$. The functor \$$T: Set \rightarrow Set\$$ is that which sends every set \$$A\$$ to its powerset \$$2^A\$$, defined as the set of all subsets of \$$A\$$. Now to complete the definition of this functor, we need to specify how it acts on morphisms \$$f: A \rightarrow B\$$. Well, in our category \$$Set\$$, such a morphism \$$f\$$ is a function from set \$$A\$$ to set \$$B\$$. We need to define the result of applying functor \$$T\$$ to morphism \$$f\$$. Now, by the definition of a functor, \$$T(f)\$$ is required to be another function, of type \$$T(f): T(A) \rightarrow T(B)\$$. Which is to say, \$$T(f): 2^A \rightarrow 2^B\$$. Now, given that we have a function \$$f\$$ mapping set \$$A\$$ into set \$$B\$$, what could this function \$$T(f)\$$ be, which must map \$$2^A\$$ into \$$2^B\$$? Well a mapping from \$$2^A\$$ into \$$2^B\$$ is just another way of saying a function that maps subsets of \$$A\$$ to subsets of \$$B\$$. Given that \$$f\$$ maps elements of \$$A\$$ to elements of \$$B\$$, there is a clear candidate for \$$T(f)\$$ mapping subsets of \$$A\$$ to subsets of \$$B\$$. Given a subset of \$$A\$$, the action of \$$T(f)\$$ will be to apply \$$f\$$ to every element of \$$A\$$ and collect the results to form a subset of \$$B\$$. We say that \$$T(f)\$$ is the _lifting_ of \$$f: A \rightarrow B\$$ to a function from \$$2^A\$$ to \$$2^B\$$: \$T(f)(A) = \lbrace f(x) | x \in A \rbrace\$ This is referred to as the _direct image_ of \$$A\$$ under \$$f\$$. 
• Options
5.
edited January 2020

Now Proposition 1 asks us to show that this $$T$$ is actually a bona fide functor. It's not enough to define any old mapping from the objects and morphisms of one category to the objects and morphisms of another category. In order to qualify as a functor, such a mapping from one category to another must be structure preserving. Specifically, it needs to preserve two structures: composition, and identities.

Preserving composition means that given $$f: A \rightarrow B$$ and $$g: B \rightarrow C$$, with composition$$f \triangleright g: A \rightarrow C$$, it must be the case that:

$T(f \triangleright g) = T(f) \triangleright T(g)$

In words, this says that if we lift the composition of two functions, we get the same result as when we lift the functions separately and then compose.

Preserving identities means that given $$Id_A: A \rightarrow A$$, it must be the case that:

$T(Id_A) = Id_{T_A}$

This says that if we lift the identity function on a set $$A$$, then we get the identity function on the power set $$2^A$$.

Both of these statements are true. And so we have proven that $$T$$ is a functor.

Comment Source:Now Proposition 1 asks us to show that this \$$T\$$ is actually a _bona fide_ functor. It's not enough to define any old mapping from the objects and morphisms of one category to the objects and morphisms of another category. In order to qualify as a functor, such a mapping from one category to another must be _structure preserving_. Specifically, it needs to preserve two structures: composition, and identities. Preserving composition means that given \$$f: A \rightarrow B\$$ and \$$g: B \rightarrow C\$$, with composition\$$f \triangleright g: A \rightarrow C\$$, it must be the case that: \$T(f \triangleright g) = T(f) \triangleright T(g)\$ In words, this says that if we lift the composition of two functions, we get the same result as when we lift the functions separately and then compose. Preserving identities means that given \$$Id_A: A \rightarrow A\$$, it must be the case that: \$T(Id_A) = Id_{T_A}\$ This says that if we lift the identity function on a set \$$A\$$, then we get the identity function on the power set \$$2^A\$$. Both of these statements are true. And so we have proven that \$$T\$$ is a functor. 
• Options
6.
edited January 2020

Next, in Proposition 2, we are asked to prove that $$\mu: T^2 \rightarrow T$$ is a natural transformation. Let's unpack this now!

Now, before proving that it is a natural transformation, let's review what this $$\mu$$ is. From the definition above, we see that it is a family of functions, with one member of the family $$\mu_A$$ for every set $$A$$.

The type of $$\mu_A$$ is given by:

$\mu_A: T(T(A)) \rightarrow T(A)$

Now we can rewrite this as:

$\mu_A: 2^{2^A} \rightarrow 2^A$

What's $$2^{2^A}$$? That's the powerset of the powerset, which consists of sets of subsets of $$A$$.

$$\mu_A$$ must therefore map a set of subsets of $$A$$ to a single subset of $$A$$.

As stated above, $$\mu_A$$ maps a set of subsets to their union:

$\mu_A(S \subseteq 2^A) = \bigcup S$

Comment Source:Next, in Proposition 2, we are asked to prove that \$$\mu: T^2 \rightarrow T\$$ is a natural transformation. Let's unpack this now! Now, before proving that it is a natural transformation, let's review what this \$$\mu\$$ is. From the definition above, we see that it is a family of functions, with one member of the family \$$\mu_A\$$ for every set \$$A\$$. The type of \$$\mu_A\$$ is given by: \$\mu_A: T(T(A)) \rightarrow T(A)\$ Now we can rewrite this as: \$\mu_A: 2^{2^A} \rightarrow 2^A\$ What's \$$2^{2^A}\$$? That's the powerset of the powerset, which consists of sets of subsets of \$$A\$$. \$$\mu_A\$$ must therefore map a set of subsets of \$$A\$$ to a single subset of \$$A\$$. As stated above, \$$\mu_A\$$ maps a set of subsets to their union: \$\mu_A(S \subseteq 2^A) = \bigcup S\$ 
• Options
7.

Now let's look into the claim that this family of functions $$\mu_A$$ constitutes a 'natural transformation' from $$T^2$$ to $$T$$.

Comment Source:Now let's look into the claim that this family of functions \$$\mu_A\$$ constitutes a 'natural transformation' from \$$T^2\$$ to \$$T\$$. 
• Options
8.
edited January 2020

Natural transformations are mappings between functors. Here, the source functor is $$T^2$$ -- which is the functor obtained by applying $$T$$ twice in succession -- and the target functor is $$T$$.

Suppose $$F$$ and $$G$$ are functors from category $$C$$ to category $$D$$. Then a natural transformation $$\mu$$ from $$C$$ to $$D$$ assigns to each object $$c$$ in $$C$$ some arrow $$\mu_c$$ taking $$F(c)$$ to $$G(c)$$.

In the case of the working example, $$C$$ and $$D$$ are the category $$Set$$; $$F$$ is the functor $$T^2$$ and $$G$$ is the functor $$T$$. So any natural transformation between $$T^2$$ and $$T$$ must give, for each set $$A$$, an arrow $$\mu_A$$ taking $$T^2(A) = 2^{2^A}$$ to $$T(A) = 2^A$$.

That is exactly the form that we observed for $$\mu_A$$, above, in comment 6. So we're on the right track for showing that $$\mu_A$$ is a natural transformation from $$T^2$$ to $$T$$.

Comment Source:Natural transformations are mappings between functors. Here, the source functor is \$$T^2\$$ -- which is the functor obtained by applying \$$T\$$ twice in succession -- and the target functor is \$$T\$$. Suppose \$$F\$$ and \$$G\$$ are functors from category \$$C\$$ to category \$$D\$$. Then a natural transformation \$$\mu\$$ from \$$C\$$ to \$$D\$$ assigns to each object \$$c\$$ in \$$C\$$ some arrow \$$\mu_c\$$ taking \$$F(c)\$$ to \$$G(c)\$$. In the case of the working example, \$$C\$$ and \$$D\$$ are the category \$$Set\$$; \$$F\$$ is the functor \$$T^2\$$ and \$$G\$$ is the functor \$$T\$$. So any natural transformation between \$$T^2\$$ and \$$T\$$ must give, for each set \$$A\$$, an arrow \$$\mu_A\$$ taking \$$T^2(A) = 2^{2^A}\$$ to \$$T(A) = 2^A\$$. That is exactly the form that we observed for \$$\mu_A\$$, above, in comment 6. So we're on the right track for showing that \$$\mu_A\$$ is a natural transformation from \$$T^2\$$ to \$$T\$$.
• Options
9.
edited January 2020

$$\require{begingroup}\begingroup\require{AMScd}\newcommand{\tlap}{\raisebox{0pt}[0pt][0pt]{#1}}\newcommand{\blap}{\vbox to 0pt{\hbox{#1}\vss}}$$ But a natural transformation is not just any old family of arrows of the prescribed type $$\mu_A: F(A) \rightarrow G(A)$$. There is a 'naturality' constraint, which is motivated by the following considerations.

Suppose we have an arrow $$\alpha: c_1 \rightarrow c_2$$ in $$C$$. Now consider the application of the functors $$F$$ and $$G$$ to $$\alpha$$. From the arrow $$\alpha$$ in $$C$$, we can obtain the pair of arrows $$F(\alpha), G(\alpha)$$ in $$D$$. Each functor gives a different image in $$D$$ of the arrow $$\alpha$$ in $$C$$.

A natural transformation $$\mu_c$$ from $$F$$ to $$G$$ gives a systematic way to 'transition' from the arrow $$F(\alpha): F(c_1) \rightarrow F(c_2)$$ to the arrow $$G(\alpha): G(c_1) \rightarrow G(c_2)$$. The constraint on the family of morphisms $$\mu_c$$ is that for all $$\alpha: c_1 \rightarrow c_2$$, the following diagram must commute:

\begin{CD} F(c_1) @>F(\alpha)>> F(c_2) \\@V{\mu_{c_1}}VV {}@VV{\mu_{c_2}}V \\ G(c_1) @>>G(\alpha)> G(c_2) \end{CD}

There are two ways to get from $$F(c_1)$$ to $$G(c_2$$ We can either first go through $$F(\alpha)$$ and then through the natural transformation, or first go through the natural transformation and then through $$G(\alpha)$$. These are required to be the same, by the naturality constraint on the arrows $$\mu_c$$.

Written as a formula, the naturality constraint states that:

$F(\alpha) \triangleright \mu_{c_2} = \mu_{c_1} \triangleright G(\alpha)$

Comment Source:\$$\require{begingroup}\begingroup\require{AMScd}\newcommand{\tlap}{\raisebox{0pt}[0pt][0pt]{#1}}\newcommand{\blap}{\vbox to 0pt{\hbox{#1}\vss}}\$$ But a natural transformation is not just any old family of arrows of the prescribed type \$$\mu_A: F(A) \rightarrow G(A)\$$. There is a 'naturality' constraint, which is motivated by the following considerations. Suppose we have an arrow \$$\alpha: c_1 \rightarrow c_2\$$ in \$$C\$$. Now consider the application of the functors \$$F\$$ and \$$G\$$ to \$$\alpha\$$. From the arrow \$$\alpha\$$ in \$$C\$$, we can obtain the pair of arrows \$$F(\alpha), G(\alpha)\$$ in \$$D\$$. Each functor gives a different image in \$$D\$$ of the arrow \$$\alpha\$$ in \$$C\$$. A natural transformation \$$\mu_c\$$ from \$$F\$$ to \$$G\$$ gives a systematic way to 'transition' from the arrow \$$F(\alpha): F(c_1) \rightarrow F(c_2)\$$ to the arrow \$$G(\alpha): G(c_1) \rightarrow G(c_2)\$$. The constraint on the family of morphisms \$$\mu_c\$$ is that for all \$$\alpha: c_1 \rightarrow c_2\$$, the following diagram must commute: \begin{CD} F(c_1) @>F(\alpha)>> F(c_2) \\\@V{\mu_{c_1}}VV {}@VV{\mu_{c_2}}V \\\ G(c_1) @>>G(\alpha)> G(c_2) \end{CD} There are two ways to get from \$$F(c_1)\$$ to \$$G(c_2\$$ We can either first go through \$$F(\alpha)\$$ and then through the natural transformation, or first go through the natural transformation and then through \$$G(\alpha)\$$. These are required to be the same, by the naturality constraint on the arrows \$$\mu_c\$$. Written as a formula, the naturality constraint states that: \$F(\alpha) \triangleright \mu_{c_2} = \mu_{c_1} \triangleright G(\alpha)\$ 
• Options
10.
edited January 2020

$$\require{begingroup}\begingroup\require{AMScd}\newcommand{\tlap}{\raisebox{0pt}[0pt][0pt]{#1}}\newcommand{\blap}{\vbox to 0pt{\hbox{#1}\vss}}$$ Let's instantiate back to our example, where $$F$$ is $$T^2$$, and $$G$$ is $$T$$.

Suppose $$A$$ and $$B$$ are sets in $$Set$$, and that $$\alpha: A \rightarrow B$$. Then the naturality diagram instantiates down to the following:

\begin{CD} T^2(A) @>T^2(\alpha)>> T^2(B) \\@V{\mu_{A}}VV {}@VV{\mu_{B}}V \\ T(A) @>>T(\alpha)> T(B) \end{CD}

Written as a formula, the constraint is:

$T^2(\alpha) \triangleright \mu_B = \mu_A \triangleright T(\alpha)$

Both of these compositions give a function going from the top-left to the bottom-right of the diagram, i.e., from $$T^2(A)$$ to $$T(B)$$, i.e., from $$2^{2^A}$$ to $$2^B$$.

So let's choose an $$x$$ in $$2^{2^A}$$. That means $$x$$ is a set of subsets of $$A$$.

The first composition applies $$T^2(\alpha)$$ to $$x$$ and then sends that through $$\mu_B$$.

That means mapping $$\alpha$$ to all the elements of $$A$$ in $$x$$, which yields a set of subsets of $$B$$, and then taking the union of these subsets, to obtain a single subset of $$B$$.

The second composition takes the union of all the elements in $$x$$ to obtain a single subset of $$A$$, and then maps $$\alpha$$ over all the elements in this subset, to obtain a single subset of $$B$$.

These two processes both convert $$x$$ to the same subset of $$B$$.

So the diagram commutes.

That means that the naturality condition is satisfied.

So we have shown that the family of functions $$\mu_A$$ is a natural transformation from $$T^2$$ to $$T$$.

That completes the proof of Proposition 2.

Comment Source:\$$\require{begingroup}\begingroup\require{AMScd}\newcommand{\tlap}{\raisebox{0pt}[0pt][0pt]{#1}}\newcommand{\blap}{\vbox to 0pt{\hbox{#1}\vss}}\$$ Let's instantiate back to our example, where \$$F\$$ is \$$T^2\$$, and \$$G\$$ is \$$T\$$. Suppose \$$A\$$ and \$$B\$$ are sets in \$$Set\$$, and that \$$\alpha: A \rightarrow B\$$. Then the naturality diagram instantiates down to the following: \begin{CD} T^2(A) @>T^2(\alpha)>> T^2(B) \\\@V{\mu_{A}}VV {}@VV{\mu_{B}}V \\\ T(A) @>>T(\alpha)> T(B) \end{CD} Written as a formula, the constraint is: \$T^2(\alpha) \triangleright \mu_B = \mu_A \triangleright T(\alpha)\$ Both of these compositions give a function going from the top-left to the bottom-right of the diagram, i.e., from \$$T^2(A)\$$ to \$$T(B)\$$, i.e., from \$$2^{2^A}\$$ to \$$2^B\$$. So let's choose an \$$x\$$ in \$$2^{2^A}\$$. That means \$$x\$$ is a set of subsets of \$$A\$$. The first composition applies \$$T^2(\alpha)\$$ to \$$x\$$ and then sends that through \$$\mu_B\$$. That means mapping \$$\alpha\$$ to all the elements of \$$A\$$ in \$$x\$$, which yields a set of subsets of \$$B\$$, and then taking the union of these subsets, to obtain a single subset of \$$B\$$. The second composition takes the union of all the elements in \$$x\$$ to obtain a single subset of \$$A\$$, and then maps \$$\alpha\$$ over all the elements in this subset, to obtain a single subset of \$$B\$$. These two processes both convert \$$x\$$ to the same subset of \$$B\$$. So the diagram commutes. That means that the naturality condition is satisfied. So we have shown that the family of functions \$$\mu_A\$$ is a natural transformation from \$$T^2\$$ to \$$T\$$. That completes the proof of Proposition 2.