Could liftM be too strict for a Functor instance, if we are writing down mfix with it?

Question

fmap for Monads often defaults to liftM:

liftM   :: (Monad m) => (a1 -> r) -> m a1 -> m r
liftM f m1 = do { x1 <- m1; return (f x1) }

Yet, as one can see it uses binding (as the right hand desugars into m1 >>= \ x1 -> return (f x1)). I wonder whether such a fmap can be used for writing down mfix down for monads which have a strict >>= operator. To be more precise, I wonder about the following implementation with Control.Arrow.loop (again).

The monad I use is Identity, yet it forces whatever is inside it whenever binding takes place with seq.

newtype Id' a = Id' { runId' :: a } deriving ...

instance Functor Id' where
    fmap = liftM -- instead of `f <$> (Id' x) = Id' (f x)`. 

instance Applicative Id' where
    pure  = return
    (<*>) = ap

instance Monad Id' where
    return         = Id'
    (Id' x)  >>= k = x `seq` k x

instance MonadFix Id' where
    mfix f = let a = f (runId' a) in a

myMfix :: MonadFix m => (a -> m a) -> m a
myMfix k = let f ~(_, d) = ((,) d) <$> k d
           in (flip runKleisli () . loop . Kleisli) f

My intuition is yes, it can be used. I reckon that we run into problems only in two cases:

1. k we apply mfix/myMfix to is strict.
2. We apply mfix/myMfix to return.

Both cases are fairly simple and we do not expect any converging result in the first place. I believe that other cases could be forced to WHNF without forcing the feedback.

Is my intuition correct? If not, can one show an example where it fails?

Answer 1

Your definition of Id' isn't a valid monad as it fails the left-unit law:

  return undefined >= const (return 3)
= Id' undefined >>= const (return 3)
= undefined `seq` const (return 3) undefined
= undefined

which does not equal

  const (return 3) undefined
= return 3
= Id' 3

So the discussion of whether your definition of MonadFix for Id' is valid is rather moot, let alone the validity of whether the definition via the Kleisli construction is faithful.

Having said that, if you want to see whether a definition is a faithful implementation of mfix, you need to write down and prove the three laws of strictness, purity, and left-shrinking. If you start with an actual monad (instead of your Id' which fails that test), then you need to establish these three laws to be considered a valid monadic feedback operator. Without doing that work, it's impossible to say how the definition might generalize.

My hunch is that your intuition of definition via the Kleisli construction might very well hold for well-behaved arrows, i.e., those whose loop operator do satisfy the right-tightening law. However, it is well known that an arrow over the Kleisli category of a monad with a left-strict bind operator does not have loop operators that satisfy right tightening. (See Corollary 3.1.7 and the discussion in Section 6.4.1.)

So, any monad with a left-strict bind operator (such as [], Maybe, IO, strict state, etc.) will fail the test. But arrows that arise from monads like environment, lazy state, and those built out of monoids (a.k.a. writer monads) might work out.