Cases in which we shall not use monadic bind to write mfix down using loop

Question

I have been trying to write mfix down using Control.Arrow.loop. I came up with different definitions and would like to see which one is mfix's actual workalike.

So, the solution I reckon to be the right one is the following:

mfix' :: MonadFix m => (a -> m a) -> m a
mfix' k = let f ~(_, d) = sequenceA (d, k d)
          in (flip runKleisli () . loop . Kleisli) f

As one can see, the loop . Kleisli's argument works for Applicative instances. I find it to be a good sign as we mostly have our knot-tying ruined by (>>=)'s strictness in the right argument.

Here is another function. I can tell that it is not mfix's total workalike, but the only case I found is not very natural. Take a look:

mfix'' k = let f ~(_, d) = fmap ((,) d) (return d >>= k)
           in (flip runKleisli () . loop . Kleisli) f

As far as I understand, not every strict on the right-hand bind forces its argument entirely. For example, in case of IO:

GHCi> mfix'' ((return :: a -> IO a) . (1:))
[1,1,1,1,1,Interrupted.

So, I decided to fix this. I just took Maybe and forced x in Just x >>= k:

data Maybe' a = Just' a | Nothing' deriving Show

instance Functor Maybe' where
    fmap = liftM

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

instance Monad Maybe' where
    return         = Just'
    Nothing' >>= k = Nothing'
    Just' x  >>= k = x `seq` k x

instance MonadFix Maybe' where
    mfix f = let a = f (unJust' a) in a
             where unJust' (Just' x) = x
                   unJust' Nothing'  = errorWithoutStackTrace "mfix Maybe': Nothing'."

Having this on our hands:

GHCi> mfix ((return :: a -> Maybe' a) . (1:))
[1,1,1,1,1,Interrupted.

GHCi> mfix' ((return :: a -> Maybe' a) . (1:))
[1,1,1,1,1,Interrupted.

GHCi> mfix'' ((return :: a -> Maybe' a) . (1:))
Interrupted.

So, here are my questions:

1. Is there any other example which could show that mfix'' is not totally mfix?
2. Are monads with such a strict bind, like Maybe', interesting in practice?
3. Are there any examples which show that mfix' is not totally mfix that I have not found?

---

A small side note on IO:

mfix3 k' = 
    let 
       k = return . k'
       f ~(_, d) = fmap ((,) d) (d >>= k)
    in (join . flip runKleisli () . loop . Kleisli) f

Do not worry about all the returns and joins - they are here just to have mfix3's and mfix's types match. The idea is that we pass d itself instead of return d to the (>>=) on the right-hand. It gives us the following:

GHCi> mfix3 ((return :: a -> IO a) . (1:))
Interrupted.

Yet, for example (thanks to Li-yao Xia for their comment):

GHCi> mfix3 ((return :: a -> e -> a) . (1:)) ()
[1,1,1,1,1,Interrupted.

---

Edit: thanks to HTNW for an important note on pattern-matching in the comments: it is better to use \ ~(_, d) -> ..., not \ (_, d) -> ....

Answer 1

Here's a partial answer, which I hope is better than no answer.

Is there any other example which could show that mfix'' is not totally mfix?

We can distinguish mfix'' from mfix also by making return strict instead of (>>=).

Are monads with such a strict bind, like Maybe', interesting in practice?

Probably not. (Questions about the existence of "practical" examples are not easy to answer negatively.)

Containers that are strict in their elements might be an example of this. (In case you're wondering about the official containers package, it does not actually define Monad instances for Map and IntMap, and the Monad instance of Seq is lazy in the elements of the sequence).

Note also that it is unclear whether the monad laws take strictness into account. If you do, then such things are not lawfully monads because they break the left identity law: (return x >>= k) = k x for x = undefined.

Are there any examples which show that mfix' is not totally mfix that I have not found?

If you take the definition of loop in the standard library, in terms of mfix, then I think that mfix' = mfix, though I couldn't complete a proof (I could either be missing a good trick, or there's a missing MonadFix law).

The main point of contention, as was hinted at in the comments, is strictness. Both your definition of mfix' and the standard library's definition of loop are careful to expand the argument function to be lazier (using lazy patterns (~(_, d)) and snd respectively; the two techniques are equivalent). mfix and mfix' are still equal if exactly one of those precautions is dropped. There is a mismatch (mfix /= mfix') if both are dropped.