# Monadicity for the Curious Programmer

## 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
```

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:

1. Run the `Algebra` to reduce an `f a` to an `a`
2. 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:

1. We smoosh the two layers together via `join` to get an `f a`, then `eval` it.
2. 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
```