1
$\begingroup$

Can every monad give rise to a monad transformer?

In the paper Calculating monad transformers with category theory by Oleksandr Manzyuk, one finds a construction of monad transformers as translating monads along adjunctions. In particular, considering the Eilenberg-Moore construction, we can translate the monads on the category $C^T$ of $T$-algebras to monads on the original category $C,$ where $T$ is the monad we start from. Hence, if somehow a monad on $C$ induces a monad on $C^T,$ then we can translate that induced monad along the adjunction between $C$ and $C^T$ that defines $T.$ Since we can regard $C^T$ as a subcategory of $C,$ we know that there is indeed an induction if every monad $M$ on $C$ maps $T$-algebras to $T$-algebras, e.g. if $T$ commutes with all monads; in particular, the Writer-monad-transformers can be derived this way. But I know almost nothing about the center of the category $\text{Mon}(C)$ of monads on $C,$ which is equivalent to the category of monoids in the functor category $C^C=\text{Hom}(C, C).$

Then I found this question on MSE, from which I see that the functor $T\rightarrow\text{Ran}_{F^T}(F^TT)$ is a lax monoidal functor, hence inducing a functor $\text{Mon}(C)\rightarrow\text{Mon}(C^T),$ where $F^T$ is the left adjoint functor to the forgetful functor $U^T:C^T\rightarrow C.$ So the question becomes

When will the right Kan extension $\text{Ran}_{F^T}(F^TT)$ exist?
Does the construction ($T\rightarrow \text{Ran}_{F^T}(F^TT)\rightarrow\text{translating along }F^T$) give the right notion of monad transformers?

This question sounds quite obscure and confusing, but all I want to know is that are there general constructions of monad transformers for any given monad?

Any answer or reference will be sincerely appreciated, and thanks in advance.

$\endgroup$
1
$\begingroup$

I am not a mathematician nor a category theorist but a functional programmer, so my answer is along the lines of specific code examples.

In functional programming, one works in the category of sets ($\mathbb{S}et$) rather than in a general, arbitrary category. The objects of that category are types available in the programming language, and the arrows are functions from one type to another. Most frequently one works with endofunctors of that category, so monads used in functional programming are specific such endofunctors. The category of sets also has the useful properties that it has products, co-products, the initial object, the final object, and exponentials.

  1. So, for endofunctors in the category of sets, I think I have an example of a monad that has no monad transformer. (But I do not know how to prove it rigorously.)

The example monad is defined as the functor that maps an object $A$ as $A \mapsto A + A^C$. Here $C$ is a fixed object. In my notation, $X + Y$ is the co-product of objects $X$ and $Y$, and $A^C$ is the exponential object for the functions $C \rightarrow A$.

I tried many possibilities such as $M(A+A^C)$ or $A+M(A)^C$ but could not construct a monad transformer for this monad such that the necessary laws hold. I have intuitive ideas about why this monad should not have a monad transformer, but these ideas are not rigorous.

Right now I'm checking the laws for $M(A+M(A)^C)$ as a monad transformer, and maybe that will work. Even if so, I conjecture (again, I have no proof, so this could be wrong) that the monad $A+C^{(C^A)}$ has no monad transformer. Here, $C^{(C^A)}$ is the continuation monad.

A related stackoverflow question is https://stackoverflow.com/questions/24515876/is-there-a-monad-that-doesnt-have-a-corresponding-monad-transformer-except-io

  1. A monad transformer $T_L^M$ for a base monad $L$ and a foreign monad $M$ is useful for practical programming if it has the following properties:

    • $T_L^M$ is a monad for any base monad $L$ and a foreign monad $M$, and is defined monadically naturally in $M$ (i.e. $T_L^M$ does not depend on the structure of $M$ but only on the fact that $M$ is a monad)
    • there are monadic morphisms as natural transformations injecting $L \leadsto T_L^M$ and $M \leadsto T_L^M$

The construction $\mathrm{Ran}_{L}(L M)$ is a monad for any monads $L$ and $M$, is defined monadically naturally in $M$, but there is no injecting morphism $M \leadsto \mathrm{Ran}_{L}(L M)$.

In terms of functional programming, I understand this construction as the quantified type $T_L^M a = \forall i. (a \rightarrow L i) \rightarrow L (M i)$.

So, on the surface, this construction is not a fully functional monad transformer.

Here is how I would argue for that. Suppose I wanted to cheat and pretend that the monad $L$ itself is already a monad transformer $T_L^M$ (i.e. I did not use $M$ at all in the construction of the transformer, but I am not going to tell you that). How would you be able to expose my cheating? You will say that there is no injecting morphism $M \leadsto T_L^M$. Other than that, everything about this "fake transformer" seems to be working just fine.

So, the construction $\mathrm{Ran}_{L}(L M)$ is similar to this "fake transformer", in that one of the injecting morphisms is lacking.

$\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.