MonadBaseControl laws

Question

The MonadBaseControl class offers very few laws. To get something I want, I need one more:

forall f q. f <$> liftBaseWith q
  = liftBaseWith $ \runInBase -> fmap f (q runInBase)

My extremely vague intuition suggests this is natural (in some sense) and that it might even follow from some combination of the Functor laws, parametricity, and the documented MonadBaseControl laws. Is this so? If not, are there any "reasonable" instances that disobey the law?

Note: I've also asked an abbreviated version of this question as a GitHub issue.

Answer 1

That's an immediate consequence of the free theorem of the type of liftBaseWith.

A simplified version of the "free theorem theorem" which is sufficient to generate a version of such a free theorem is:

Any function f :: forall a. F a -> G a where F and G are functors, satisfies, for any types a,b, and any function phi :: a -> b,

fmap phi . f = f . fmap phi  -- simplified "free theorem" for f

(in other words, that equation holds whenever it typechecks.)

I don't have a proof offhand, but I'd be extremely surprised if there is a counterexample.

Application

In this case f is liftBaseWith, where the functors are

F a = RunInBase m b -> b a  -- F = ReaderT (RunInBase m b) b
G a = m a

Apply both sides of the "free theorem" above to q, unfold the definition of fmap for ReaderT:

(fmap phi . liftBaseWith) q = (liftBaseWith . fmap phi) q
fmap phi (liftBaseWith q) = liftBaseWith (fmap phi q)
fmap phi (liftBaseWith q) = liftBaseWith \run -> fmap phi (q run)

Relevant literature

As a starting point to read up on the topic, there's of course the paper Theorems for free! by Philip Wadler, and another closely related one Free theorems involving type constructor classes by Janis Voigtlander.