# Monoid Morphisms, Products, and Coproducts

Today I want to talk about relationships between monoids. These can be useful to think about when we’re developing libraries involving monoids, and we want to express some algebraic laws among them. We can then check these with automated tests, or indeed prove them with algebraic reasoning.

This post kind of fell together when writing notes on chapter 10, “Monoids”, of Functional Programming in Scala. I am putting it here so I can reference it from the chapter notes at the end of the book.

## Monoid homomorphisms

Let’s take the `String` concatenation and `Int` addition as example monoids that have a relationship. Note that if we take the length of two strings and add them up, this is the same as concatenating those two strings and taking the length of the combined string:

So every `String` maps to a corresponding `Int` (its length), and every concatenation of strings maps to the addition of corresponding lengths.

The `length` function maps from `String` to `Int` while preserving the monoid structure. Such a function, that maps from one monoid to another in such a preserving way, is called a monoid homomorphism. In general, for monoids `M` and `N`, a homomorphism `f: M => N`, and all values `x:M`, `y:M`, the following law holds:

The `|+|` syntax is from Scalaz and is obtained by importing `scalaz.syntax.monoid._`. It just references the `append` method on the `Monoid[T]` instance, where `T` is the type of the arguments.

This law can have real practical benefits. Imagine for example a “result set” monoid that tracks the locations of a particular set of records in a database or file. This could be as simple as a `Set` of locations. Concatenating several thousand files and then proceeding to search through them is going to be much slower than searching through the files individually and then concatenating the result sets. Particularly since we can potentially search the files in parallel. A good automated test for our result set monoid would be that it admits a homomorphism from the data file monoid.

## Monoid isomorphisms

Sometimes there will be a homomorphism in both directions between two monoids. If these are inverses of one another, then this kind of relationship is called a monoid isomorphism and we say that the two monoids are isomorphic. More precisely, we will have two monoids `A` and `B`, and homomorphisms `f: A => B` and `g: B => A`. If `f(g(b)) == b` and `g(f(a)) == a`, for all `a:A` and `b:B` then `f` and `g` form an isomorphism.

For example, the `String` and `List[Char]` monoids with concatenation are isomorphic. We can convert a `String` to a `List[Char]`, preserving the monoid structure, and go back again to the exact same `String` we started with. This is also true in the inverse direction, so the isomorphism holds.

Other examples include (`Boolean`, `&&`) and (`Boolean`, `||`) which are isomorphic via `not`.

Note that there are monoids with homomorphisms in both directions between them that nevertheless are not isomorphic. For example, (`Int`, `*`) and (`Int`, `+`). These are homomorphic to one another, but not isomorphic (thanks, Robbie Gates).

## Monoid products and coproducts

If `A` and `B` are monoids, then `(A,B)` is certainly a monoid, called their product:

But is there such a thing as a monoid coproduct? Could we just use `Either[A,B]` for monoids `A` and `B`? What would be the `zero` of such a monoid? And what would be the value of `Left(a) |+| Right(b)`? We could certainly choose an arbitrary rule, and we may even be able to satisfy the monoid laws, but would that mean we have a monoid coproduct?

To answer this, we need to know the precise meaning of product and coproduct. These come straight from Wikipedia, with a little help from Cale Gibbard.

A product `M` of two monoids `A` and `B` is a monoid such that there exist homomorphisms `fst: M => A`, `snd: M => B`, and for any monoid `Z` and morphisms `f: Z => A` and `g: Z => B` there has to be a unique homomorphism `h: Z => M` such that `fst(h(z)) == f(z)` and `snd(h(z)) == g(z)` for all `z:Z`. In other words, the following diagram must commute:

A coproduct `W` of two monoids `A` and `B` is the same except the arrows are reversed. It’s a monoid such that there exist homomorphisms `left: A => W`, `right: B => W`, and for any monoid `Z` and morphisms `f: A => Z` and `g: B => Z` there has to be a unique homomorphism `h: W => Z` such that `h(left(a)) == f(a)` and `h(right(b)) == g(b)` for all `a:A` and all `b:B`. In other words, the following diagram must commute:

We can easily show that our `productMonoid` above really is a monoid product. The homomorphisms are the methods `_1` and `_2` on `Tuple2`. They simply map every element of `(A,B)` to a corresponding element in `A` and `B`. The monoid structure is preserved because:

And for any other monoid `Z`, and morphisms `f: Z => A` and `g: Z => B`, we can construct a unique morphism from `Z` to `(A,B)`:

And this really is a homomorphism because we just inherit the homomorphism law from `f` and `g`.

What does a coproduct then look like? Well, it’s going to be a type `C[A,B]` together with an instance `coproduct[A:Monoid,B:Monoid]:Monoid[C[A,B]]`. It will be equipped with two monoid homomorphisms, `left: A => C[A,B]` and `right: B => C[A,B]` that satisfy the following (according to the monoid homomorphism law):

And additionally, for any other monoid `Z` and homomorphisms `f: A => Z` and `g: B => Z` we must be able to construct a unique homomorphism from `C[A,B]` to `Z`:

### The simplest thing that could possibly work

We can simply come up with a data structure required for the coproduct to satisfy a monoid. We will start with two constructors, one for the left side, and another for the right side:

This certainly allows an embedding of both monoids `A` and `B`. But `These` is now basically `Either`, which we know doesn’t quite form a monoid. What’s needed is a `zero`, and a way of appending an `A` to a `B`. The simplest way to do that is to add a product constructor to `These`:

Now `These[A,B]` is a monoid as long as `A` and `B` are monoids:

`These[A,B]` is the smallest monoid that contains both `A` and `B` as submonoids (the `This` and `That` constructors, respectively) and admits a homomorphism from both `A` and `B`. And notice that we simply added the least amount of structure possible to make `These[A,B]` a monoid (the `Both` constructor). But is it really a coproduct?

First we must prove that `This` and `That` really are homomorphisms. We need to prove the following two properties:

That’s easy. The first two cases of the `append` method on the `coproduct` monoid prove these properties.

But can we define `fold`? Yes we can:

But is `fold` really a homomorphism? Let’s not assume that it is, but test it out.Here’s the homomorphism law:

What happens if both `t1` or `t2` are `This` or `That`?

That holds. But what if we introduce a `Both` on one side?

So far so good. That holds because of associativity. What about the other side?

No! Something has gone wrong. This will only hold if the `Z` monoid is commutative. So in general, `These[A,B]` is not the coproduct of `A` and `B`. My error was in the `Both` constructor, which commutes all `B` values to the right and all `A` values to the left.

So what kind of thing would work? It would have to solve this case:

We need to preserve that `a1`, `b1`, `a2`, and `b2` appear in that order. So clearly the coproduct will be some kind of list!

We could modify the `Both` constructor this way:

And let’s add an empty case for the combined zero:

In which case `These[A,B]` has become a kind of tree, or an unbalanced list of `This[A]` and `That[B]` values. A free product of the two monoids `A` and `B`. The implementation of `append` for the `coproduct` monoid could be:

This `append` normalizes the list so that consecutive values of the same type are added together.

And we would modify `fold` to recurse over the tree:

This is now a homomorphism! We already know that this is so for the `This` and `That` cases. And now that the `Both` case simply appeals to the inductive hypothesis, we know that it holds for `Both` as well.

### Free monoids on coproducts

To better understand what’s going on, let’s try going the other way. What if we start with the coproduct of the underlying sets and get a free monoid from there?

The underlying set of a monoid `A` is just the type `A` without the monoid structure. The coproduct of types `A` and `B` is the type `Either[A,B]`. Having “forgotten” the monoid structure of both `A` and `B`, we can recover it by generating a free monoid on `Either[A,B]`, which is just `List[Either[A,B]]`. The `append` operation of this monoid is list concatenation, and the identity for it is the empty list.

Clearly `List[Either[A,B]]` is a monoid, but does it permit a homomorphism from both monoids `A` and `B`? If so, then the following properties should hold:

They clearly do not hold! The lists on the left of `==` will have two elements and the lists on the right will have one element. Can we do something about this?

Well, the fact is that `List[Either[A,B]]` is not exactly the monoid coproduct of `A` and `B`. It’s “too big” in a sense. But if we were to reduce the list to a normal form that approximates a “free product”, we can get a coproduct that matches our definition above. What we need is a new monoid:

`Eithers[A,B]` is a kind of `List[Either[A,B]]` that has been normalized so that consecutive `A`s and consecutive `B`s have been collapsed using their respective monoids. So it will contain alternating `A` and `B` values.

This is now a monoid coproduct because it permits monoid homomorphisms from `A` and `B`:

And we can implement the `fold` homomorphism:

And this time `fold` really is a homomorphism, and we can prove it by case analysis. Here’s the law again:

If either of `e1` or `e2` is empty then the result is the fold of the other, so those cases are trivial. If they are both nonempty, then they will have one of these forms:

In the first two cases, on the right of the `==` sign in the law, we perform `a1 |+| a2` and `b1 |+| b2` respectively before concatenating. In the other two cases we simply concatenate the lists. The `++` method on `Eithers` takes care of doing this correctly for us. On the left of the `==` sign we fold the lists individually and they will be alternating applications of `f` and `g`. So then this law amounts to the fact that `f(a1 |+| a2) == f(a1) |+| f(a2)` in the first case, and the same for `g` in the second case. In the latter two cases this amounts to a homomorphism on `List`. So as long as `f` and `g` are homomorphisms, so is `fold(_)(f,g)`. Therefore, `Eithers[A,B]` really is a coproduct of `A` and `B`.

Since we have already convinced ourselves that `These` is a monoid coproduct, we could also simply show that there is a homomorphism from `Eithers` to `These`:

Which would amount to proving that `(toThese(xs) |+| toThese(ys))` = `toThese(xs ++ ys)`.

The lesson learned here is to check assumptions and test against laws. Things are not always as straightforward as they seem.