Journal de Chaource

The free monad on a functor F is often defined like this in Haskell:

data FreeMonad f a = Pure a | Join (f (Freemonad f a)

This is a recursive definition written schematically as a type equation `r = a + f(r)`.

However, as Haskell is lazy by default, this defines r as the greatest fixpoint of that type equation.
The free monad actually needs to be the least fixpoint, not the greatest fixpoint. Otherwise the properties of the free monad will not hold. I believe this detail is not usually emphasized or clarified.

What happens if we define the free monad as the greatest fixpoint? It will not be possible to have a unique arrow in the category of monads (monad morphism) from the free monad to an arbitrary other monad, in the following way:

If `Free : Functor → Monad` is a free monad constructor and M is any monad then there must exist a unique monad morphism of type Free(M) → M.

Now, a feature of greatest fixpoints is that they can represent an infinite data structure.
But the monad M is not necessarily an infinite data structure; it could be a least fixpoint.
A monad morphism must preserve monad operations.
The monad operations on Free(M) can add more parts to the structure; so then the image in M must also add more parts to the structure. It is impossible to make a monad morphism between an infinite structure and a finite structure such that all parts are preserved.

A specific example: Suppose M a = (a, List w). This is a Writer monad, and the Writer just appends more stuff to List w. (List w is used here as a monoid, and w can be any type.)

Then Free(M) a = a + (Free(M) a, List w). We can solve this type equation by expanding it out:

Free(M) a = a + (a, List w) + ((a, List w), List w) + (((a, List w), List w), List w) + ...

If we define Free(M) as the least fixpoint, then this is equivalent to (a, List (List w)).

If we define Free(M) as the greatest fixpoint, then this is (a, Stream(List w)); here `Stream` is the possibly-infinite list (the greatest fixpoint corresponding to List).

We should be able to map Free(M) → M, which means to map (a, List (List w)) → (a, List w).
Or (a, Stream(List w)) → (a, List w).
We have to map a → a identically in any case, or else we won't preserve the monads' "pure" methods. Then it remains to map either:

List (List w) → List w

or

Stream (List w) → List w

The first map is the standard join method on lists, that concatenates all inner lists.
Concatenation is required because the monad operations must be preserved; a "bind" operation on the Writer monad corresponds to appending in the monoid List w, which is concatenating the lists.

But the second map's type says we should be able to concatenate a possibly infinite sequence of inner lists. This is not possible: we cannot traverse an infinite sequence and concatenate all its data into a finite list. But the requirement of preserving the monad's operations means that we may not drop any data.

So, this function must return bottom, it cannot be implemented.

The greatest fixpoint is not a correct free monad. Haskell's implementations are incorrect unless they are made strict rather than lazy.