tree derived from monad is itself a monad

Question

I have constructed a functor from a monad that appears (based on computer experiments to test the monad laws) to also have monad properties but I am having trouble proving it.

Here is the idea: M[A] is a monad, and Either[A.B] is the usual "or" bifunctor.

Let N[A] = M[Either[A, N[A]]] It's a recursive definition so these M-trees could be finite or infinite. I specify that they are finite only.

Now we can define map, unit and join transformations of the correct type signature

N(f) = M( bimap(f, N(f))) and so on.

I have managed to prove, with brute force techniques, that N is a functor and unit is a natural transformation in the appropriate way. However, I am having difficulty with the laws dealing with the join, because the definitions of map and join are recursive, and so my proofs go around in circles.

Is there a particular mathematical technique for proving a functor is a monad when it is defined recursively?

Answer 1

I believe that what you construct here is known in the functional programming community as the resumption monad. In general, given an endofunctor $F$ and a monad $M$, the functor part of the resumption monad $R^{F,M}$ is given as

$$R^{F,M} A = \mu X. M(FX+A),$$

where $\mu X. G X$ is the carrier of the initial $G$-algebra for an endofunctor $G$. A bit nicer way to specify this monad is

$$R^{F,M} A = M (FM)^*A,$$

where $(FM)^*$ is the free monad generated by the composition of endofunctors $F$ and $M$. This gives you automatically that $R^{F,M}$ is an endofunctor.

Your construction is obtained for $F = \mathrm{Id}$, that is the identity endofunctor.

The monadic structure for $R^{F,M}$ can be obtained via a distributive law $(FM)^*M \rightarrow M(FM)^*$ and the construction was introduced by Hyland, Plotkin, and Power in "Combining effects: Sum and tensor", Theorem 4.

The construction in the "infinite case" was given by me and J.Gibbons in "The Coinductive Resumption Monad", Theorem 3.8.

If you are interested in general methods of constructing monadic structure for endofunctors given by similar fixed points, try Uustalu's "Generalizing substitution".