Monad transformers are known for all standard monads (Reader, Writer, State, Cont, List, etc.), but each of these monad transformers works in a slightly different way. There is no general method or formula for constructing a monad transformer given a definition of a type constructor with a monad instance. So, it is not assured that a monad data type designed according to some arbitrary business requirements will have a monad transformer. Is there such an explicit example?
Related work
Another question explains that a functor composition of two monads is not necessarily a monad. See also this question. Those examples do not answer the present question - they merely illustrate the problem of having no general method for constructing a monad transformer. Those examples show that, given two monads M and N, we will sometimes find that M (N a) is a monad, sometimes that N (M a) is a monad, and sometimes neither will be a monad. But this shows neither how to construct a monad transformer for M or N, nor whether it exists at all.
An answer to another question argues that the IO monad cannot have a monad transformer because if it had one IOT, we could apply IOT to List, and then lifting an empty list (lift []) into the resulting monad would have to undo the side effects performed "earlier" by the IO monad. This argument is based on the idea that the IO monad "actually performs" side effects that, presumably, cannot be undone. However, the IO monad is not an explicit type constructor.
Discussion
In every example where a monad type is given explicitly, a monad transformer could be found somehow, - sometimes with certain ingenuity required. For example, the ListT transformer that existed in the Haskell library was relatively recently found to be incorrect in a subtle way, but the problem was eventually fixed by changing the definition of ListT.
Standard examples of monads without transformers are monads such as IO, which is actually not defined by an explicit type constructor - IO is an opaque "magic" type defined by the library somehow, at low level. It seems clear that one cannot define IO as an explicit type constructor, with a monad instance given by pure functions. The IO example shows that a monad transformer may fail to exist if we allow the monad instance to contain hidden low-level code with impure side effects. So, let us limit our attention to monads implemented using pure functions.
There does not seem to be an algorithm that would derive monad transformers automatically from the monad's source code. Do we even know that this is always possible?
To make it more clear what I mean by an "explicit example" of a monad: Suppose I claim that
type Q u v a = ((u -> (a, Maybe a)) -> v) -> u -> (a, Maybe a)
can have a lawful Monad instance with respect to the type parameter a, and I produce the source code for an implementation of the Monad instance for Q u v as pure functions return and join. Do we then know that Q u v has a monad transformer QT u v such that QT u v Id is equivalent to Q u v, and the laws of the monad transformers hold? Do we then know how to construct QT explicitly? I don't.
To decide this question, we need either
- to demonstrate an algorithm that would find a monad transformer from an arbitrary given type constructor and a given implementation of a monad instance; e.g. given the code
type F a = r -> Either (a, a) (a, a, Maybe a)and an implementation of a monad instance for this, to find the code for the monad transformer; let's limit ourselves to type constructors made out of any combination of->, tuple, andEitherfor simplicity; or - to demonstrate a counterexample: an explicit monad type constructor, given by an explicit code definition, e.g.
type F a = r -> Either (a, a, a) (a, a, Maybe a)or whatever, such that this is a lawfulMonad, with aMonadinstance given by pure functions, but we can prove thatFhas no monad transformer.
