Precomposing monad transformers

Question

Suppose I have two monad transformers

T1 :: (* -> *) -> * -> *
T2 :: (* -> *) -> * -> *

with instances

instance MonadTrans T1
instance MonadTrans T2

and some

X :: (((* -> *) -> * -> *) -> ((* -> *) -> * -> *) -> * -> *)

such as

newtype X t1 t2 a b = X { x :: t1 (t2 a) b }

for which I would like to define something along the lines

instance (MonadTrans t1, MonadTrans t2) => MonadTrans (X t1 t2) where
    lift = X . lift . lift

so that I can use lift to lift m a into X T1 T2 m a?

The problem here seems to be that the lifts act on some monad Monad m => m a which I cannot guarantee to be produce in the intermediate steps. But this is confusing for me. I am providing an implementation of lift so I can assume I have Monad m => m a, so I apply the rightmost lift and get T1 m a that I know nothing about, but shouldn't it be implied that T1 m is a Monad? If not why cannot I simply add this to the constraint of my instance

instance ( MonadTrans t1
         , MonadTrans t2
         , Monad (t2 m) ) => MonadTrans (X t1 t2) where ...

This does not work either. I have an intuition that by the above I am saying "should there be t1, t2, m such that ..." which is too weak to prove that X t1 t2 is a transformer (works for any/all Monad m). But it still doesn't make much sense to me, can a valid monad transformer produce a non-monad when applied to a monad? If not, I should be able to get away with the instance of MonadTrans (X t1 t2).

Is there a trick to do it that just eludes me or is there a reason why it cannot be done (theoretical or a limitation of what current compilers support).

Would the implication correspond to anything other than

instance (MonadTrans t, Monad m) => Monad (t m) where
    return  = lift . return
    a >>= b = ... # no sensible generic implementation

which would overlap other instances / could not provide the specific bind? Couldn't this be worked around with some indirection? Making returnT :: Monad m => a -> t m a and bindT :: Monad m => t m a -> (a -> t m b) -> t m b part of MonadTrans so that one can then write

instance MonadTrans (StateT s) where
    lift = ...
    returnT = ...
    bindT = ...

...

instance (MonadTrans t, Monad m) => Monad (t m) where
    return  = returnT
    a >>= b = a `bindT` b

This kind of instances is not currently valid due to overlapping, would they however be feasible, useful?

Answer 1

[C]an a valid monad transformer produce a non-monad when applied to a monad?

No. A monad transformer is a type constructor t :: (* -> *) -> (* -> *) which takes a monad as an argument and produces a new monad.

While I'd like to see it more explicitly stated, the transformers documentation does say "A monad transformer makes a new monad out of an existing monad", and it's implied by the MonadTrans laws:

lift . return = return
lift (m >>= f) = lift m >>= (lift . f)

Obviously these laws only make sense if lift m is indeed a monadic computation. As you pointed out in the comments, all bets are off if we have non-lawful instances to contend with. This is Haskell, not Idris, so we're used to asking politely for laws to be satisfied using documentation, rather than requiring it by force using types.

A more "modern" MonadTrans might require explicit proof that t m is a monad whenever m is. Here I'm using the "entailment" operator :- from Kmett's constraints library to say that Monad m implies Monad (t m):

class MonadTrans t where
    transform :: Monad m :- Monad (t m)
    lift :: Monad m => m a -> t m a

(This is more or less the same idea that @MigMit developed in his answer, but using off-the-shelf components.)

Why doesn't the MonadTrans in transformers feature the transform member? When it was written GHC didn't support the :- operator (the ConstraintKinds extension hadn't been invented). There's lots and lots of code in the world which depends on the MonadTrans without transform, so we can't really go back and add it in without a really good reason, and in practice the transform method doesn't really buy you much.

Answer 2

First of all: what you want is impossible. You've correctly identified the problem: even if m is a monad, and t — a transformer, nobody guarantees that t m would be a monad.

On the other hand, it usually is. But — at least theoretically — not always, so, you'd have to somehow mark the occasions when it is. Which means marking it with an instance of another typeclass that you'd have to define yourself. Let's see how it works.

We'll start with a name for our new class:

class MonadTrans t => MonadTransComposeable t where

Now, where what? We want to generate a Monad (t m) instance. Unfortunately, it's not something we can do. Class instances, while being just data, are not considered the same kind of data as everything else; we can't make a function that generates them. So, we have to work around this somehow. But if we have such a thing, then the class is pretty simple

class MonadTrans t => MonadTransComposeable t where
    transformedInstance :: Monad m => MonadInstance (t m)

Let's define MonadInstance now. We want to make sure that if there is MonadInstance n, then n is a monad. GADTs come to the rescue:

data MonadInstance n where MonadInstance :: Monad n => MonadInstance n

Notice that the MonadInstance constructor has a context, which guarantees that we can't make MonadInstance n without n being a Monad.

We can define instances of MonadTransComposeable now:

instance MonadTransComposeable (StateT s) where
    transformedInstance = MonadInstance

It would work, since it's already established in the transformers package that whenever m is a monad, StateT m is a monad too. Therefore, MonadInstance constructor makes sense.

Now we can compose MonadTrans and MonadTransComposeable. Using your own definition

newtype X t1 (t2 :: (* -> *) -> (* -> *)) m a = X { x :: t1 (t2 m) a }

we can define an instance. We now can prove that t2 m is a monad; it's not automatic, and we have to tell Haskell which transformedInstance to use, but it's not hard:

instance (MonadTrans t1, MonadTransComposeable t2) => MonadTrans (X t1 t2) where
  lift :: forall m a. (Monad m) => m a -> X t1 t2 m a
  lift ma =
    case transformedInstance :: MonadInstance (t2 m) of
      MonadInstance -> X (lift (lift ma))

---

Now, let's do something fun. Let's tell Haskell, that whenever t1 and t2 are "good" (composeable) monad transformers, X t1 t2 is too.

As before, it's quite easy:

instance (MonadTransComposeable t1, MonadTransComposeable t2) => MonadTransComposeable (X t1 t2) where
  transformedInstance = MonadInstance

Same as with StateT. The catch is that now Haskell would complain that it can't know if X t1 t2 m is really a monad. Which is fair — we didn't define an instance. Let's do that.

We will use the fact that t1 (t2 m) is a monad. So, we make this explicit:

transformedInstance2 :: forall t1 t2 m. (MonadTransComposeable t1, MonadTransComposeable t2, Monad m) => MonadInstance (t1 (t2 m))
transformedInstance2 =
  case transformedInstance :: MonadInstance (t2 m) of
    MonadInstance -> transformedInstance

Now, we'll define a Monad (X t1 t2 m) instance. Because of a stupid decision to make Monad a subclass of Applicative, we can't do this in one statement, but have to go through Functor and Applicative, but it's not hard:

instance (MonadTransComposeable t1, MonadTransComposeable t2, Monad m) => Functor (X t1 t2 m) where
  fmap h (X ttm) =
    case transformedInstance2 :: MonadInstance (t1 (t2 m)) of
      MonadInstance -> X (fmap h ttm)

instance (MonadTransComposeable t1, MonadTransComposeable t2, Monad m) => Applicative (X t1 t2 m) where
  pure a =
    case transformedInstance2 :: MonadInstance (t1 (t2 m)) of
      MonadInstance -> X (pure a)
  (X ttf) <*> (X tta) =
    case transformedInstance2 :: MonadInstance (t1 (t2 m)) of
      MonadInstance -> X (ttf <*> tta)

and, finally

instance (MonadTransComposeable t1, MonadTransComposeable t2, Monad m) => Monad (X t1 t2 m) where
  X tta >>= f =
    case transformedInstance2 :: MonadInstance (t1 (t2 m)) of
      MonadInstance -> X (tta >>= \a -> case f a of X ttb -> ttb)

Answer 3

There is a well known theory which says that monads are not generally composable. That is, given any two arbitrary monads, t, and u there is no guarantee that t ○ u is a monad, where (t ○ u) a = t (u a). This seems to be the ultimate reason why this precomposition is not available.

The rational is simple. First, notice that any monad can be written as a transform of the identity monad. Then, any two monads can be translated to the form of X. This corresponds to their composition, which isn't generally allowed, so we know that X shouldn't generally be allowed.

Let Id be the identity monad,

newtype Id a = Id a

and let composition be given by:

newtype t ○ u a = Comp (t (u a))

Also let, for any monad t, the composition with Id is equal to t.

t ○ Id ~ t ~ Id ○ t

Then, we investigate the case of X t u m a wherein t u are compositions with Id. The type and construction are given by

X (t ○) (Id ○ (u ○)) (Id ○ m) a 
  = X ((t ○) (Id ○ (u ○ (Id ○ m)) a)

And the RHS constructor is equivalent to

  ~ X ((t ○) (u ○ m) a)

Which has the type

X (t ○) (u ○) m a

And so the partial application X (t ○) (u ○) corresponds to the composition of any two monads, which isn't allowed.

All this isn't to say that we can't compose monads, but rather an explanation of why we need methods such as transform or MonadTransComposable from Benjamin Hodgson and MigMit, respectively.

I've made this a community wiki, as I expect the above, fast-and-loose proof can be greatly improved by people who actually know what they're doing.