Strengthen `hoist` constraints

[khwarizmii]

Hi! My company is using mmorph in our codebase. We would like to give an instance of MFunctor for the continuation passing style WriterT from writer-cps-transformers. Sadly, we cannot do this correctly unless we strengthen the constraints on hoist like so:

hoist :: (Monad m, Monad n) => (forall a. m a -> n a) -> t m b -> t n b

Here's why: if you look at the CPS WriterT, it is superficially the same as StateT:

newtype WriterT w m a = WriterT (w -> m (a, w))

However, it has different semantics. For one, runWriterT for this transformer is defined as follows:

runWriterT :: Monoid w => WriterT w m a -> m a
runWriterT (WriterT f) = f empty 

CPS WriterT also comes with a smart constructor so it can hide its internal state:

writerT :: (Functor f, Monoid w) => f (a, w) -> WriterT w f a
writerT f = WriterT $ \ w -> (\ (a, w') -> (a, w <> w')) <$> f

These two are inverses and obey the following laws. This distinguishes CPS WriterT from StateT:

runWriterT . writerT = id
writerT . runWriterT = id

We can't give the usual instance of MFunctor for CPS WriterT because of the Functor constraint unless we strengthen hoist:

-- Doesn't compile!
instance MFunctor (WriterT w) where
  hoist nat m = writerT (nat (runWriterT m))

I suspect that introducing a constraint on the second type constructor to be a monad might break some unlawful code. Otherwise I can't see how this change could introduce any backward incompatibility.

[Gabriella439]

@khwarizmii: Do you need to use writerT/runWriterT to implement the instance? Could you implement it instead as:

instance MFunctor (WriterT w) where
    hoist nat (WriterT f) = WriterT (\w -> nat (f w))

[khwarizmii]

This was my initial thought too. I think this breaks the semantics of WriterT, however. This is because nat can drop the continuation. Hopefully I can get to you quickly with a concrete example soon!

[khwarizmii]

Composing a counter example has not been particularly straightforward :-/

So here's a (failed!) attempt at a proof of correctness.

Let unWriterT (WriterT f) = f. Let's try to prove the StateT-like instance for CPS WriterT is the same as the smart constructor instance. This is the case if and only if the following equation is obeyed:

WriterT . nat . unWriterT $ (WriterT f) = writerT . nat . runWriterT $ WriterT f     (1)

Rewriting the LHS yields:

WriterT . nat . unWriterT $ (WriterT f) = WriterT . nat . f                          (2)

Rewriting the RHS yields:

writerT . nat . runWriterT $ WriterT f
  = writerT . nat $ f empty
  = WriterT $ \ w -> (\ (a, w') -> (a, w <> w')) <$> nat (f empty)
  = WriterT $ fmap (\ w -> (\ (a, w') -> (a, w <> w'))) . nat $ f empty              (3)

From (1), (2) and (3) we have, for all natural transformations nat,

nat . f = fmap (\ w -> (\ (a, w') -> (a, w <> w'))) . nat $ f empty                  (4)

by naturality we have fmap g . nat = nat . fmap g, hence

nat . f = nat . fmap (\ w -> (\ (a, w') -> (a, w <> w'))) $ f empty                  (5)

Since id is a natural transformation, we know that (5) is true if and only if

f = fmap (\ w -> (\ (a, w') -> (a, w <> w'))) $ f empty                              (6)

This doesn't appear to be obvious, although coming up with a counter example hasn't been fruitful for me.

[EDIT: I expanded this attempted proof a little further]

[Gabriella439]

@khwarizmii: I can complete your proof. The missing piece is that nat is a monad morphism and all monad morphisms are natural transformations, which must obey the following law:

nat . fmap k = fmap k . nat

That means that you can rearrange this:

nat . f = \ w -> (\ (a, w') -> (a, w <> w')) <$> nat (f empty)

... to this:

nat . f = \ w -> nat ((\ (a, w') -> (a, w <> w')) <$> f empty)

... which you can further rearrange to:

nat . f = nat . (\w -> (\ (a, w') -> (a, w <> w')) <$> f empty)

... which is true if:

f = \w -> (\ (a, w') -> (a, w <> w')) <$> f empty

If we wrap both sides of that in the WriterT constructor

WriterT f = WriterT (\w -> (\ (a, w') -> (a, w <> w')) <$> f empty)

... then we can recognize that the right-hand-side of that is the same as:

WriterT f = (writerT . runWriterT) (WriterT f)

... and since writerT . runWriterT = id then we complete the proof:

WriterT f = WriterT f

[khwarizmii]

Thanks! I regret having to resort to skipping the smart contructor to write this instance, but presumably introducing the proposed monad constraint could be breaking to anyone abusing this library.

Thanks again for helping me work through the proof!

[Gabriella439]

@khwarizmii: You're welcome! 🙂