Search code examples
haskellmonadscompositionmonad-transformers

Precomposing monad transformers


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?


Solution

  • [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.