Correctness of implicit lifting

Question

Imagine that I have a value that is generic over the monad:

m :: (Monad m) => m A  -- 'A' is some concrete type

Now let's say that I specialize this value to a concrete monad transformer stack in two separate ways:

m1 :: T M A
m1 = m

m2 :: T M A
m2 = lift m

... where M and T M are monads, and T is a monad transformer:

instance Monad M where ...
instance (Monad m) => Monad (T m) where ...
instance MonadTrans T where ...

... and those instances obey the monad laws and monad transformer laws.

Can we deduce that:

m1 = m2

... knowing nothing about m other than its type?

This is just a long-winded way of asking if lift m is a valid substitution for m, assuming that both type-check. It is a little bit difficult to phrase the question because it requires m type-checking as two separate monads before and after the substitution. As far as I can tell, the only way such a substitution would type-check is if m is generic over the monad.

My vague intuition is that the substitution should always be correct, but I'm not sure that my intuition is correct, or how to prove it if it is correct.

Answer 1

If m :: Monad m => m A, then m must be equivalent to return x for some x :: A, because the only ways you have to get anything :: m x are return and (>>=). But in order to use (>>=) you must be able to produce some m y, which you can either do with return or with another application of (>>=). Either way you have to use return eventually, and the monad laws guarantee that the whole expression will be equivalent to return x.

(If m is completely polymorphic over the monad, then you must able to use it at m ~ Identity, so it can't use any fancy monad tricks, unless you pass it an argument. This sort of trick is used e.g. here and here.)

Given that m = return x, we know by the monad transformer laws (lift . return = return) that lift m = m.

Of course, this is only true for this particular type. If you have, say, m :: MonadState S m => m A, then m could easily be different from lift m -- for example, with a type like StateT A (State A) A, get and lift get will be different.

(And of course all of this is ignoring ⊥. Then again, if you don't, most monads don't obey the laws anyway.)

Answer 2

I believe this is a sloppy inductive proof that your m is equivalent to lift m.

I think we have to try to prove something about m (or rather, about all possible values of type (Monad m) => m A). If we consider Monad as consisting of bind and return only, and ignore bottom and fail then your m must at the top level be one of:

mA = return (x)
mB = (mX >>= f)

For mA the two forms of m are equivalent by the monad transformer law:

lift (return (x)) = return (x)

That's the base case. Then we're left with the second transformer law to reason about mB:

lift (mX >>= f) = lift mX >>= (lift . f)

and where we'd like to prove that that our mB is equal to that expansion:

mX >>= f = lift mX >>= (lift . f)

we assume that the left side of bind is equivalent (mX = lift mX) since that's our inductive hypothesis (right?).

So then we're left to prove f = lift . f by figuring out what f has to look like:

f :: a -> m b
f = \a -> (one of our forms mA or mB)

and lift . f looks like:

f = \a -> lift (one of our forms mA or mB)

Which leaves us back with our hypothesis:

m = lift m