Pre-folding 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 ab = 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 raise ma to X T1 T2 ma ?

It seems that the problem is that lift acts on some monad Monad m => ma , which I cannot guarantee that it will be done at intermediate steps. But it baffles me. I provide a lift implementation, so I can assume that I have Monad m => ma , so I apply the rightmost lift and get T1 ma , which I don’t know anything about, but should I not assume that T1 m a Monad ? If not, why can't I just add this to the restriction 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 the above I say "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 for me this still doesn’t really matter, can a working monad transformer create a non-monad when applied to a monad? If not, I must leave with a copy of MonadTrans (X t1 t2) .

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

Will the implication match anything other than

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

which would overlap other instances / could not provide a specific binding? Could this work with some indirectness? Create returnT :: Monad m => a -> tma and bindT :: Monad m => tma -> (a -> tmb) -> tmb part, so that you can then write

 instance MonadTrans (StateT s) where lift = ... returnT = ... bindT = ... ... instance (MonadTrans t, Monad m) => Monad (tm) where return = returnT a >>= b = a `bindT` b 

This type of instances is currently invalid due to overlap, can it be feasible, useful?

Answer 1

Does a [C] virtual monad transformer create a nonmonode when applied to a monad?

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

Although I would like this to be more explicitly stated in the transformers documentation , it says: "The monad transformer creates a new monad from the existing monad," and this implies the laws of MonadTrans :

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

Obviously, these laws make sense if lift m really a monadic calculation. As you noted in the comments, all bets are disabled if we have unlawful instances that you can deal with. This is Haskell, not Idris, so we are used to politely asking for laws to satisfy, using documentation, and not to demand them by force, using types.

More modern MonadTrans may require explicit proof that tm is a monad whenever m is. Here I use the operator "entailment" :- from Kmett constraints to say that Monad m means Monad (tm) :

 class MonadTrans t where transform :: Monad m :- Monad (tm) lift :: Monad m => ma -> tma 

(This is more or less the same idea as @MigMit, developed in his answer, but using ready-made components.)

Why is there no transform element in MonadTrans in transform ? When it was written, the GHC did not support the operator :- (the ConstraintKinds extension was not invented). There is a lot and a lot of code in the world that depends on MonadTrans without transform , so we cannot go back and add it without a really good reason , and in practice, the transform method really doesn't buy you.

Answer 2

First of all: what you want is impossible. You correctly identified the problem: even if m is a monad and t is a transformer, no one guarantees that tm will be a monad.

On the other hand, this is usually the case. But, at least theoretically - not always, so you will have to somehow note cases where this is so. This means that it marks it with an instance of another type, which you will need to determine yourself. See how it works.

Let's start with the name for the new class:

 class MonadTrans t => MonadTransComposeable t where 

Now, where what? We want to create an instance of Monad (tm) . Unfortunately, this is not something we can do. Class instances, being just data, are not considered the same data as everything else; we cannot create a function that generates them. So we have to get 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 (tm) 

Now define MonadInstance . We want to make sure that if there is MonadInstance n , then n is a monad. GADT come to the rescue:

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

Note that the MonadInstance constructor has a context that ensures that we cannot make MonadInstance n without n Monad .

Now we can define instances of MonadTransComposeable :

 instance MonadTransComposeable (StateT s) where transformedInstance = MonadInstance 

It will work because it is already installed in the transformers package, when whenever m is a monad, StateT m also a monad. Therefore, the MonadInstance constructor makes sense.

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

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

we can define an instance. Now we can prove that t2 m is a monad; it is not automatic, and we must tell Haskell what transformedInstance use, but it is not difficult:

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

---

Now do something funny. Let Haskell say that when t1 and t2 are “good” (compound) monad transformers, X t1 t2 too.

As before, it's pretty simple:

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

Same as with StateT . The trick is that Haskell will now complain that he cannot know if X t1 t2 m is really a monad. Which is fair - we did not define an instance. Let me do it.

We will use the fact that t1 (t2 m) is a monad. So we make it 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 define an instance of Monad (X t1 t2 m) . Due to the stupid decision to make Monad subclass of Applicative , we cannot do it in one expression, but must go through Functor and Applicative , but this is not difficult:

 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 fa of X ttb -> ttb) 

Answer 3

There is a well-known theory in which monads are usually not compositional. That is, for any two arbitrary monads, t and u there is no guarantee that t ○ u is a monad, where ( t ○ u ) a = t (ua) , This, apparently, is the final reason that this preposition is not available .

Rational is simple. First, note that any monad can be written as a transformation of an identical monad. Then any two monads can be converted to form X This corresponds to their composition, which is usually not allowed, so we know that X usually not allowed.

Let Id be the identity monad,

 newtype Id a = Id a 

and let the composition be set as follows:

 newtype t ○ ua = Comp (t (ua)) 

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

 t ○ Id ~ t ~ Id ○ t 

Then we investigate the case of X tuma , where t u are compositions with Id . Type and design are given

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

And the RHS constructor is equivalent

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

Which has type

 X (t ○) (u ○) ma 

So, the partial application X (t ○) (u ○) corresponds to the composition of any two monads, which is not allowed.

All this does not mean that we cannot compose monads, but rather explain why we need methods such as transform or MonadTransComposable from Benjamin Hodgson and MigMit, respectively.

I created this community wiki because, as I believe, the above, quick and free proof can be greatly improved by people who really know what they are doing.