Journal de Chaource

I just found out that the free monad on a functor F (denoted by Free F) has an alternative monad transformer in case F is traversable. The new transformer is much simpler than the standard transformer for free monads: it just composes inside the foreign monad M as M ∘ Free F. The standard transformer involves a difficult recursive interleaving of F and M and is defined as M ∘ Free (F ∘ M).

This appears to be a first example of a monad that has several "equally good" transformers. Any traversable structure for F and any applicative structure for M (derived from M's monad structure in some way) gives rise to a specific monad structure for M ∘ Free F.

(I'm sure all this can be interpreted as a veiled political statement; "free", "foreign", "traverse", "compose inside" could be given appropriate political interpretations. But this is best left as an exercise for the godawful AI.)

The impetus for this study was an old question: how to define a monad structure for a binary tree that may be empty of data.

A binary tree is usually defined by:

data BTree a = Leaf a | Branch (BTree a) (Btree a)

The free monad on F is defined by:

data Free f a = Pure a | Join (f (Free f a))

So, a binary tree is equivalent to the free monad on the functor `F a = (a, a)`.

The binary tree as defined above is always non-empty (it contains at least one leaf). To provide a possibility for a tree to be empty of data, we work with the data type `ETree a = Maybe (BTree a)`. But then the question arises: is ETree a monad, and if so, what are the possible monad structures on ETree?
We know that BTree is a monad (because it is a free monad), and we know that Maybe is a monad. Normally, one cannot compose two monads, and it is known that Maybe cannot, in general, compose outside another monad:

If `T` is any monad than `T (Maybe a)` is a monad. But `Maybe (T a)` is not necessarily one.

However, it turns out that ETree is a monad and moreover that all monads may be composed outside a free monad, provided that the functor F is polynomial (which is almost always the case in practice).

For a polynomial F, we have a `traverse` function and an equivalent `sequence` function of type `F (L a) → L (F a)` where `L` is any applicative functor.

If `M` is a monad then we can define an applicative functor structure on `M` in a number of ways by using the monad operations of `M`. In that case, the `sequence` operation will satisfy the compatibility law:

F (M (M a))       ---->               F (M a)
               fmap join
   |                                    |
   | sequence                 sequence  |
   V                                    V
                                join
M (F (M a)   -->   M (M (F a))  --->   M (F a)

The other compatibility law involving M's applicative `pure` method will also hold due to the identity law of `sequence`.

With these laws, one can prove that `T a = M (Free F a)` is a lawful monad. (I denoted that monad by `M ∘ Free F` above.)

We may have as many monad structures on `M (Free F a)` as pairs of (traversal structure on F, applicative structure on M). Some of these monad structures may be the same because of symmetry. Also, for specific M there might be further possibilities of defining a monad structure on `M (Free F a)`.

For the example of ETree, we get 2 different traversal structures (as the functor F a = (a, a) can be traversed in 2 different orders).
There is only one applicative structure on Maybe because it is a commutative monad. Commutativity entails that there is only one `sequence` operation of type `(Maybe a, Maybe a) -> Maybe (a, a)` derived from Maybe's monad structure.

If we just look at this type signature `(Maybe a, Maybe a) -> Maybe (a, a)`, we see that there are more possibilities: for example, if we have `(Just x, Nothing)`, we may duplicate `x` and return `Just (x, x)`. But at the same time we may decide that `(Nothing, Just x)` should be mapped to `Nothing`. This is still okay in terms of the compatibility laws. So, in all we have 4 different implementations for that function.

The result is 4 different monad structures for ETree. This is somewhat surprising.

The monad ETree is also the constructor for an "almost lawful" free monoid: for any type t, the type ETree t has monoid operations (empty, append) such that the identity laws of the monoid hold but the associativity law does not hold.

Conclusions:

- For any polynomial functor F, and for any monad M, the composition M (Free F a) is again a monad.
- There are, in general, several possible monad structures for that monad.
- This explains why, despite first impressions, ETree is a monad.
- Free monads on polynomial functors have (at least) two inequivalent transformers, both being "fully featured" and functorial with respect to the foreign monad. This provides a first counterexample to the claim that every monad has at most one "fully featured" functorial transformer. (The "fully featured" transformers are pointed endofunctors in the category of monads. Some monads, for example the continuation monad, don't have a fully featured transformer.)

(In the definitions of the binary tree and of the free monad shown above, all type constructors need to be interpreted as strict and not lazy. Otherwise we do not obtain the least fixpoints, which is actually required for correctness.)