Is there a monad that doesn't have a corresponding monad transformer (except IO)?

Question

So far, every monad (that can be represented as a data type) that I have encountered had a corresponding monad transformer, or could have one. Is there such a monad that can't have one? Or do all monads have a corresponding transformer?

By a transformer t corresponding to monad m I mean that t Identity is isomorphic to m. And of course that it satisfies the monad transformer laws and that t n is a monad for any monad n.

I'd like to see either a proof (ideally a constructive one) that every monad has one, or an example of a particular monad that doesn't have one (with a proof). I'm interested in both more Haskell-oriented answers, as well as (category) theoretical ones.

As a follow-up question, is there a monad m that has two distinct transformers t1 and t2? That is, t1 Identity is isomorphic to t2 Identity and to m, but there is a monad n such that t1 n is not isomorphic to t2 n.

(IO and ST have a special semantics so I don't take them into account here and let's disregard them completely. Let's focus only on "pure" monads that can be constructed using data types.)

Answer 1

I'm with @Rhymoid on this one, I believe all Monads have two (!!) transformers. My construction is a bit different, and far less complete. I'd like to be able to take this sketch into a proof, but I think I'm either missing the skills/intuition and/or it may be quite involved.

Due to Kleisli, every monad (m) can be decomposed into two functors F_k and G_k such that F_k is left adjoint to G_k and that m is isomorphic to G_k * F_k (here * is functor composition). Also, because of the adjunction, F_k * G_k forms a comonad.

I claim that t_mk defined such that t_mk n = G_k * n * F_k is a monad transformer. Clearly, t_mk Id = G_k * Id * F_k = G_k * F_k = m. Defining return for this functor is not difficult since F_k is a "pointed" functor, and defining join should be possible since extract from the comonad F_k * G_k can be used to reduce values of type (t_mk n * t_mk n) a = (G_k * n * F_k * G_k * n * F_k) a to values of type G_k * n * n * F_k, which is then further reduces via join from n.

We do have to be a bit careful since F_k and G_k are not endofunctors on Hask. So, they are not instances of the standard Functor typeclass, and also are not directly composable with n as shown above. Instead we have to "project" n into the Kleisli category before composition, but I believe return from m provides that "projection".

I believe you can also do this with the Eilenberg-Moore monad decomposition, giving m = G_em * F_em, tm_em n = G_em * n * F_em, and similar constructions for lift, return, and join with a similar dependency on extract from the comonad F_em * G_em.

Answer 2

Here's a hand-wavy I'm-not-quite-sure answer.

Monads can be thought of as the interface of imperative languages. return is how you inject a pure value into the language, and >>= is how you splice pieces of the language together. The Monad laws ensure that "refactoring" pieces of the language works the way you would expect. Any additional actions provided by a monad can be thought of as its "operations."

Monad Transformers are one way to approach the "extensible effects" problem. If we have a Monad Transformer t which transforms a Monad m, then we could say that the language m is being extended with additional operations available via t. The Identity monad is the language with no effects/operations, so applying t to Identity will just get you a language with only the operations provided by t.

So if we think of Monads in terms of the "inject, splice, and other operations" model, then we can just reformulate them using the Free Monad Transformer. Even the IO monad could be turned into a transformer this way. The only catch is that you probably want some way to peel that layer off the transformer stack at some point, and the only sensible way to do it is if you have IO at the bottom of the stack so that you can just perform the operations there.