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.

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

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:

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.

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.

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".

Proofs

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

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

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