# Monadicity for the Curious Programmer

## Table of Contents

## 1. Introduction

Today, I want to tell an interesting story about algebraic structures and their evaluators. After we are finished, we will have learned some non-trivial category theory, and gained a greater appreciation for some of the basic tools that we take for granted. However, before we tell the end of the story, we must tell the beginning.

## 2. Algebra

The story starts, like many good programming stories, with the idea
of an algebraic structure. Most Haskell folks are pretty familiar
with a few of these: `Semigroup`

, `Monoid`

, etc. However, there are
a huge number of increasingly fancy structures that we don't see as
often: Rings, Vector Spaces, Abelian Groups, etc. What unites all of these
things together under the banner of "Algebra"? Furthermore, what
even *is* algebra all about?

Here's one perspective: Algebra is about the reduction or evaluation of expressions. For instance, given some expression language, we could consider "evaluators" of the expression language:

data Expr a = Op (Expr a) (Expr a) | Lit a type Evaluator a = Expr a -> a sumExpr :: Evaluator Int sumExpr (Op a b) = (sumExpr a) + (sumExpr b) sumExpr (Lit a) = a andExpr :: Evaluator Bool andExpr (Op a b) = (andExpr a) && (andExpr b) andExpr (Lit a) = a

Now, for a teeny bit of sweeping generalization. All that `Expr`

does here is provide a bunch of `a`

with some sort of structure
binding them together. There's nothing special about it! Therefore,
we can think about "evaluators" for *any* sort of expression
structure by making it a type parameter to `Evaluator`

:

type Evaluator f a = f a -> a sumExpr :: Evaluator Expr Int sumExpr (Op a b) = (sumExpr a) + (sumExpr b) sumExpr (Lit a) = a sumList :: Evaluator [] Int sumList = sum

Now, it is totally reasonable to regard this with suspicion. What do
we achieve by doing this? From a purely programming standpoint, not a
whole lot. However, this is a huge perspective shift. What we've
done here is capture the essence of "reduction of a structure" in a
very simple construct! Furthermore, our `Evaluator`

type is actually
a core idea in Categorical Algebra, where it has another name: an **F-Algebra**.
To keep things in line with the theory, moving forward I will using
F-Algebra, and refer to the following Haskell type:

type Algebra f a = f a -> a

## 3. Monads

Now, for a bit of conflict. For some choices of `f`

in our
F-Algebras, we have two ways of reducing down a structure!
Particularly, if `f`

is a `Monad`

, we can either:

- Run the
`Algebra`

to reduce an`f a`

to an`a`

- Use
`join :: f (f a) -> f a`

to smoosh two layers of`f`

together

This is quite the pickle! The whole point of this generalization is to capture the essence of reduction, and now we are presented two different ways! What a mess.

However, like many problems, we can resolve it by adding some laws
that make sure that our `Algebra`

and our `Monad`

instance
"play nicely". Let's say we have some `eval :: Algebra f a`

, as
well as `Monad f`

. Our first law should be pretty unobjectionable:

eval/pure: id = eval . pure

What this law says is that making an `f a`

via `pure`

and
immediately evaluating it down ought to be the same as doing
nothing. If we test this out with our `sumList`

evaluator before,
this makes a lot of sense:

sumList $ pure n = sumList [n] = n

Now, for the second law. This one is a bit trickier, so build it up
piece by piece. The original problem at hand was that we could
reduce down an `f (f a)`

to an `a`

in two ways:

- We smoosh the two layers together via
`join`

to get an`f a`

, then`eval`

it. - We first
`eval`

the inner layer via`fmap eval`

to get an`f a`

, then`eval`

the outer layer.

Therefore, our law will say that these two things ought to be the same!

eval/join : eval . fmap eval = eval . join

Now, let's give these extra-fancy F-Algebras a name, or rather, use
the name that mathematicians have given them: **T-Algebras**. The "T"
here refers to the common practice of denoting a monad with `T`

in
the literature.

## 4. A Surprising Equivalence

Now that the stage is set and we have met our cast of characters, we
can finally start to tell the actual story! Let's start with an observation:
We can turn any `Monoid`

into a T-Algebra for lists:

toAlgebra :: Monoid m => Algebra [] m toAlgebra xs = foldr (<>) mempty xs

Those interested in the proofs of these laws can check the Proofs section.

Now, time for the crazy part: Given a T-Algebra, we can construct a lawful Monoid! As Haskell doesn't let us programatically construct instances, let's just pretend a Monoid is a record for now:

fromAlgebra ::: Algebra [] m -> Monoid m fromAlgebra alg = Monoid { mempty = alg [] , mappend = \x y -> alg [x, y] }

The Monoid laws fall out of the T-Algebra laws we imposed earlier. Again, interested readers can check the Proofs section for the full proofs of this.

So in some sense, T-Algebras for lists are the same as Monoids!
This is no coincidence. In particular, lists form the Free Monoid,
which is what causes this whole series of events to unfurl. In
categorical language, we would say that the Category of T-Algebras
for Lists is **equivalent** to the Category of Monoids. This does
require us to show that `toAlgebra . fromAlgebra = id`

and
`fromAlgebra . toAlgebra = id`

, but that is relegated to the Proofs section.

The even more incredible part is that this isn't just restricted to Monoids. This works for all "well behaved" algebraic structures you can dream up! For instance, T-Algebras for free groups are the same as groups, T-Algebras for free modules are the same as modules, etc.

## 5. Conclusion

So what does this actually *mean*? Personally, it gives me a new
perspective on how to think about algebraic structures. Rather than
being a collection of operations and laws, we can think of them as
providing a way of interpreting particular types of expression
trees, or reducing down particular types of data structures. This
also opens the gate to all sorts of amazing generalization, where we
can view things that don't traditionally look algebraic as algebras!
For instance, this works for the power-set functor `Setᵒᵖ → Set`

, as
well as for certain types of spaces. All in all, I think this is a
gem of Categorical Algebra, and one that ought to be
appreciated. If you would like to learn more, the magic words to
search are "Monadic Functor" and "Monadicity".

## 6. Proofs

### 6.1. `toAlgebra`

is a T-Algebra

The first one is relatively straightforward:

eval/pure: toAlgebra (pure m) = toAlgebra [m] -- By Defn. of pure = foldr (<>) mempty [m] -- By Defn. of toAlgebra = m <> mempty -- By Defn. of foldr = m -- By right identity law for monoids

However, the next requires a proof by induction:

-- Base Case: eval/join/nil: toAlgebra $ fmap toAlgebra [] = toAlgebra [] -- By Defn. of fmap = toAlgebra $ join [] -- By Defn. of join -- Inductive Case -- Inductive Hypothesis: 'toAlgebra $ fmap toAlgebra mss = toAlgebra $ join mss' eval/join/cons: toAlgebra $ fmap toAlgebra (ms : mss) = toAlgebra $ (toAlgebra ms) : fmap toAlgebra mss -- By Defn. of fmap = foldr (<>) mempty $ (toAlgebra ms) : fmap toAlgebra mss -- By Defn. of toAlgebra = toAlgebra ms <> (foldr (<>) mempty $ fmap toAlgebra mss) -- By Defn. of foldr = toAlgebra ms <> toAlgebra (join mss) -- Inductive Hypothesis = (foldr (<>) mempty ms) <> (foldr (<>) mempty $ join mss) -- By Defn. of toAlgebra = foldr (<>) mempty $ (ms ++ join mss) -- By Defn. of foldr, monoid assoc, and monoid identity = foldr (<>) mempty $ join (ms : mss) -- By Defn. of join = toAlgebra $ join (ms : mss) -- By Defn. of toAlgebra

### 6.2. `fromAlgebra`

is a Monoid

First, left and right identities. The proof of the left identity is basically the same, so we only provide the right.

monoid/identity/right: m <> mempty = alg [m, alg []] -- By Defn. of <> and mempty = alg [alg [m], alg []] -- By eval/pure = alg $ fmap alg [[m], []] -- By Defn. of fmap = alg $ join [[m], []] -- By eval/join = alg [m] -- By Defn. of join = m -- By eval/pure

Now, associativity:

monoid/assoc: (x <> y) <> z = alg [alg [x, y], z] -- By Defn. of <> = alg [alg [x, y], alg [z]] -- By eval/pure = alg $ fmap alg [[x,y], [z]] -- By Defn. of fmap = alg $ join [[x, y], [z]] -- By eval/join = alg $ join [[x], [y, z]] -- By Defn. of join = alg $ fmap alg [[x], [y,z]] -- By eval/join = alg [alg [x], alg [y, z]] -- By Defn. of fmap = alg [x, alg [y, z]] -- By eval/pure = x <> (y <> z) -- By Defn. of <>

### 6.3. `toAlgebra . fromAlgebra = id`

and `fromAlgebra . toAlgebra = id`

First, let's show that `toAlgebra . fromAlgebra = id`

. Note that we
will need to compare equality of functions here, so let's do that
extensionally. We will also perform induction on the pointwise arguments.

-- Base Case toAlgebra/fromAlgebra/nil: toAlgebra (fromAlgebra alg) [] = foldr (\x y -> alg [x, y]) (alg []) [] = alg [] -- Inductive Case -- Induction Hypothesis: toAlgebra (fromAlgebra alg) xs = alg xs toAlgebra/fromAlgebra/cons: toAlgebra (fromAlgebra alg) (x : xs) = foldr (\x y -> alg [x, y]) (alg []) (x : xs) -- By Defn of toAlgebra and fromAlgebra = alg [x, foldr (\x y -> alg [x, y]) (alg []) xs] -- By Defn of foldr = alg [x, alg xs] -- Inductive Hypothesis = alg [alg [x], alg xs] -- By eval/pure = alg $ fmap alg [[x], xs] -- By Defn of fmap = alg $ join [[x], xs] -- By eval/join = alg (x : xs) -- By Defn of join

Now, onto `fromAlgebra . toAlgebra = id`

. We need to compare
equality of monoids here, so let's check that the mempty and
mappends we get are the same ones we started with.

fromAlgebra/toAlgebra/mempty Monoid.mempty (fromAlgebra (toAlgebra m)) = foldr (<>) mempty [] -- By Defn of fromAlgebra and toAlgebra = mempty -- By Defn of foldr fromAlgebra/toAlgebra/mappend Monoid.mappend (fromAlgebra (toAlgebra m)) x y = foldr (<>) mempty [x, y] -- By Defn of fromAlgebra and toAlgebra = x <> (y <> mempty) -- By Defn of foldr = x <> y -- By right identity