Sat 21 Feb 2015

## Free Monoids in Haskell

Posted by Dan Doel under Category Theory , Haskell , Mathematics[6] Comments

It is often stated that `Foldable`

is effectively the `toList`

class. However, this turns out to be wrong. The real fundamental member of `Foldable`

is `foldMap`

(which should look suspiciously like `traverse`

, incidentally). To understand exactly why this is, it helps to understand another surprising fact: lists are not free monoids in Haskell.

This latter fact can be seen relatively easily by considering another list-like type:

data SL a = Empty | SL a :> a instance Monoid (SL a) where mempty = Empty mappend ys Empty = ys mappend ys (xs :> x) = (mappend ys xs) :> x single :: a -> SL a single x = Empty :> x

So, we have a type `SL a`

of snoc lists, which are a monoid, and a function that embeds `a`

into `SL a`

. If (ordinary) lists were the free monoid, there would be a unique monoid homomorphism from lists to snoc lists. Such a homomorphism (call it `h`

) would have the following properties:

h [] = Empty h (xs <> ys) = h xs <> h ys h [x] = single x

And in fact, this (together with some general facts about Haskell functions) should be enough to define `h`

for our purposes (or any purposes, really). So, let's consider its behavior on two values:

h [1] = single 1 h [1,1..] = h ([1] <> [1,1..]) -- [1,1..] is an infinite list of 1s = h [1] <> h [1,1..]

This second equation can tell us what the value of `h`

is at this infinite value, since we can consider it the definition of a possibly infinite value:

x = h [1] <> x = fix (single 1 <>) h [1,1..] = x

`(single 1 <>)`

is a strict function, so the fixed point theorem tells us that `x = ⊥`

.

This is a problem, though. Considering some additional equations:

[1,1..] <> [n] = [1,1..] -- true for all n h [1,1..] = ⊥ h ([1,1..] <> [1]) = h [1,1..] <> h [1] = ⊥ <> single 1 = ⊥ :> 1 ≠ ⊥

So, our requirements for `h`

are contradictory, and no such homomorphism can exist.

The issue is that Haskell types are domains. They contain these extra partially defined values and infinite values. The monoid structure on (cons) lists has infinite lists absorbing all right-hand sides, while the snoc lists are just the opposite.

This also means that finite lists (or any method of implementing finite sequences) are not free monoids in Haskell. They, as domains, still contain the additional bottom element, and it absorbs all other elements, which is incorrect behavior for the free monoid:

pure x <> ⊥ = ⊥ h ⊥ = ⊥ h (pure x <> ⊥) = [x] <> h ⊥ = [x] ++ ⊥ = x:⊥ ≠ ⊥

So, what is the free monoid? In a sense, it can't be written down at all in Haskell, because we cannot enforce value-level equations, and because we don't have quotients. But, if conventions are good enough, there is a way. First, suppose we have a free monoid type `FM a`

. Then for any other monoid `m`

and embedding `a -> m`

, there must be a monoid homomorphism from `FM a`

to `m`

. We can model this as a Haskell type:

forall a m. Monoid m => (a -> m) -> FM a -> m

Where we consider the `Monoid m`

constraint to be enforcing that `m`

actually has valid monoid structure. Now, a trick is to recognize that this sort of universal property can be used to *define* types in Haskell (or, GHC at least), due to polymorphic types being first class; we just rearrange the arguments and quantifiers, and take `FM a`

to be the polymorphic type:

newtype FM a = FM { unFM :: forall m. Monoid m => (a -> m) -> m }

Types defined like this are automatically universal in the right sense. [1] The only thing we have to check is that `FM a`

is actually a monoid over `a`

. But that turns out to be easily witnessed:

embed :: a -> FM a embed x = FM $ \k -> k x instance Monoid (FM a) where mempty = FM $ \_ -> mempty mappend (FM e1) (FM e2) = FM $ \k -> e1 k <> e2 k

Demonstrating that the above is a proper monoid delegates to instances of `Monoid`

being proper monoids. So as long as we trust that convention, we have a free monoid.

However, one might wonder what a free monoid would look like as something closer to a traditional data type. To construct that, first ignore the required equations, and consider only the generators; we get:

```
data FMG a = None | Single a | FMG a :<> FMG a
```

Now, the proper `FM a`

is the quotient of this by the equations:

None :<> x = x = x :<> None x :<> (y :<> z) = (x :<> y) :<> z

One way of mimicking this in Haskell is to hide the implementation in a module, and only allow elimination into `Monoid`

s (again, using the convention that `Monoid`

ensures actual monoid structure) using the function:

unFMG :: forall a m. Monoid m => FMG a -> (a -> m) -> m unFMG None _ = mempty unFMG (Single x) k = k x unFMG (x :<> y) k = unFMG x k <> unFMG y k

This is actually how quotients can be thought of in richer languages; the quotient does not eliminate any of the generated structure internally, it just restricts the way in which the values can be consumed. Those richer languages just allow us to prove equations, and enforce properties by proof obligations, rather than conventions and structure hiding. Also, one should note that the above should look pretty similar to our encoding of `FM a`

using universal quantification earlier.

Now, one might look at the above and have some objections. For one, we'd normally think that the quotient of the above type is just `[a]`

. Second, it seems like the type is revealing something about the associativity of the operations, because defining recursive values via left nesting is different from right nesting, and this difference is observable by extracting into different monoids. But aren't monoids supposed to remove associativity as a concern? For instance:

ones1 = embed 1 <> ones1 ones2 = ones2 <> embed 1

Shouldn't we be able to prove these are the same, becuase of an argument like:

ones1 = embed 1 <> (embed 1 <> ...) ... reassociate ... = (... <> embed 1) <> embed 1 = ones2

The answer is that the equation we have only specifies the behavior of associating three values:

x <> (y <> z) = (x <> y) <> z

And while this is sufficient to nail down the behavior of *finite* values, and *finitary* reassociating, it does not tell us that *infinitary* reassociating yields the same value back. And the "... reassociate ..." step in the argument above was decidedly infinitary. And while the rules tell us that we can peel any finite number of copies of `embed 1`

to the front of `ones1`

or the end of `ones2`

, it does not tell us that `ones1 = ones2`

. And in fact it is vital for `FM a`

to have distinct values for these two things; it is what makes it the free monoid when we're dealing with domains of lazy values.

Finally, we can come back to `Foldable`

. If we look at `foldMap`

:

foldMap :: (Foldable f, Monoid m) => (a -> m) -> f a -> m

we can rearrange things a bit, and get the type:

Foldable f => f a -> (forall m. Monoid m => (a -> m) -> m)

And thus, the most fundamental operation of `Foldable`

is not `toList`

, but `toFreeMonoid`

, and lists are not free monoids in Haskell.

[1]: What we are doing here is noting that (co)limits are objects that internalize natural transformations, but the natural transformations expressible by quantification in GHC are already automatically internalized using quantifiers. However, one has to be careful that the quantifiers are actually enforcing the relevant naturality conditions. In many simple cases they are.

February 23rd, 2015 at 5:40 am

So these differences are specific to lazy values and bottoms, right? In a language without either (e.g. Idris), does any of this apply?

February 26th, 2015 at 4:23 am

I believe it is incorrect. Values of the Foldable class can *also* be infinite. Consider:

toFreeMonoid (repeat 1)

There doesn’t exist a free monoid set containing a string of infinite number of 1’s, therefore either the concept of free monoid must me generalized, or the most fundamental operation of Foldable is not toFreeMonoid

(Correct me if I’m wrong.)

February 26th, 2015 at 4:26 am

P.S. I think that “the concept of free monoid must me generalized”

February 26th, 2015 at 7:51 am

Incidentally, (a -> m) -> m is the free algebra for the continuation monad. The monoid instance for (FM a) corresponds to what I think should be the MonadPlus instance of the continuation monad. By the way: Which of the existing Monoid instances are actually `proper’ instances in the sense that the denotational semantics of mempty and make the semantic domain (including bottom and infinite values) a monoid?

February 26th, 2015 at 8:46 am

Is FM a monad? It seems yes: Just use return (=embed) and >>= of the continuation monad. Also, monoids should now be FM-algebras. What is the algebra structure map Monoid a => FM a -> a? The first thing that comes to mind is:

structure :: Monoid a => FM a -> a;

structure (FM f) = f id

At least struct.embed = id is true.

February 27th, 2015 at 6:23 pm

Imm: in a total language, this does not apply. Types are set-like, and the free monoid is a type of finite sequences. Types containing infinite sequences would not be free, because there is no means to map them correctly into other monoids, because you are not allowed to fold them.

dramforever: The point of this post was to show that the free monoid in Haskell is a type that contains infinite values. It is incorrect to use set-theoretic intuition and say that the free monoid only contains finite sequences (at least, if you care about things beyond a “fast and loose” level).

This is the same reason that data types contain infinite values in Haskell. They are still inductive definitions, but the induction is properly understood to be on domains, not sets. The domain structure induces the infinite values, despite induction ‘normally’ only giving you finite values in set theory. The same thing happens for free things.

Olaf: I think most Monoid instances are fine. The thing you usually have to be careful of is not being too lazy. For instance, if you write ‘mappend _ _ = ()’ for the unit monoid, it is wrong, because then ‘mappend mempty undefined = ()’, when it should be undefined. Most definitions can’t get away without looking at the arguments, though, so they don’t have this problem. (Monoid a, Monoid b) => Monoid (a,b) is another case where you’d have to be careful, though.

FM is a monad, and you have the relevant structure correct. It’s also a MonadPlus that does the ‘obvious’ thing.