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 lift
s 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?
[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.