0
$\begingroup$

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?

$\endgroup$
2
  • 1
    $\begingroup$ I'm having trouble understanding the question. Is $M$ a monad on $Set$? What is the "usual 'or' bifunctor" -- is it disjoint sum? Is $N(A)$ supposed to be an initial algebra of the endofunctor $X \mapsto M[\text{Either}[A, X]]$? $\endgroup$ – Todd Trimble Mar 20 '15 at 18:58
  • $\begingroup$ M is any monad, but my usecase comes from functional programming, so I am thinking in terms of monads on types. Either[A,B] is the functional programming way of representing the coproduct (i.e. disjoint sum) of A and B. N is an endofunctor constructed by composition. $\endgroup$ – greenTara Jun 23 '15 at 13:02
2
$\begingroup$

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".

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.