haskellmonadsmonadfix

Understanding the sliding law of MonadFix

I intuitively understand the purity, tightening, and nesting laws of MonadFix. However, I'm having a hard time understanding the sliding law.

mfix (fmap h . f) = fmap h (mfix (f . h)) -- for strict h

My first question is that if h has to be strict then won't mfix (f . h) be the bottom value , i.e. ⊥? After all, f . h must not inspect its input until after it returns, so that it doesn't cause a paradox. However, if h is strict then it will have to inspect its input. Perhaps my understanding of a strict function is wrong.

Second, why is this law important? I can understand the significance of the purity, tightening, and nesting laws. However, I don't see why it would be important for mfix to obey the sliding law. Could you provide a code example which demonstrates why the sliding law is important for MonadFix?

Solution

  • I can't fully explain the law, but I think I can provide some insight.

    Let's forget about the monadic part of that equation, and let's pretend that f,h :: A -> A are plain, non-monadic functions. The law then simplifies (informally speaking) to the following:

    fix (h . f) = h (fix (f . h))

    This is a well-known property in fixed point theory I discussed in CS.SE some time ago.

    The informal intuition, though, is that the least fixed point for g :: A->A is something that can be written as

    fix g = g (g (g (g ....))))

    where g is applied "infinitely many times". When g is a composition like h . f in this case, we obtain

    fix (h . f) = h (f (h (f (h (f ...)))))

    and, similarly,

    fix (f . h) = f (h (f (h (f (h ...)))))

    Now, since both applications are infinite, if we apply h on top of the second one we would expect to obtain the first one. In periodic numbers we have that 4.5(78) is the same as 4.57(87), so the same intuition applies. In formulas,

    h (fix (f . h)) = fix (h . f)

    which is exactly the same law we wanted.

    With monads, we can not compose things as easily if f :: A -> M B and h :: B -> A, since we need to use fmap here and there, and of course mfix instead of fix. We have

    fmap h . f :: A -> M A
f . h      :: B -> M B

    so both are candidate for mfix. To apply the "top-level" h after the mfix we also need to fmap it since mfix returns M A. We then obtain

    mfix (fmap h . f) = fmap h (mfix (f . h))

    Now, the above reasoning is not completely rigorous, but I believe it can be properly formalized in domain theory so to make sense even from a mathematical / theoretical point of view.