Why is `mfix` not total in `MaybeT`

Question

The transformers implementation of MonadFix for MaybeT fails if the function ever evaluates to Nothing. Why is Nothing not propagating over mfix?

mfix' :: MonadFix m => (a -> MaybeT m a) -> MaybeT m a
mfix' f = MaybeT $ mfix $ \case
  Nothing -> return Nothing
  Just x -> runMaybeT $ f x

There must be a good reason that I do not see because ListT does not implement MonadFix at all, and Maybe implements it in the same way as above.

Kinesiology

Clarification: by "in the same way as above", I suppose you mean "fails if the function ever evaluates to Nothing"? – Symonds

Can you give a concrete function which causes the existing MaybeT implementation of mfix to throw its error, witnessing the partiality? I tried, and returning Nothing simply wasn't enough; e.g. mfix (\x -> MaybeT [Nothing]) :: MaybeT [] () works just fine. On the other hand, it is easy to observe your implementation being partial; e.g. mfix' (\x -> MaybeT [Nothing]) :: MaybeT [] () (the exact same call, but with mfix' instead of mfix) never returns. – Crinum

Yes. I have a theory: the argument of mfix :: Maybe a -> m (Maybe a) can only be one of 2 kinds of functions: it can either pattern match over the argument in which case mfix evaluates to bottom, or it is a constant function in which case we mfix just evaluates to the value. The implementation I present above wraps the function in a pattern match, thereby making mfix always a bottom. – Kinesiology

Answer 1

I think the issue is just that the error message is misleading. Let's just focus on MonadFix Maybe. The argument to mfix can be one of four things.

1. It can be strict in the input: f _|_ = _|_ or "f needs to evaluate its input to decide whether it will return Nothing or Just"

   \x -> if x then Nothing else Just True
   \x -> x `seq` Nothing
   \x -> x `seq` Just x
   

2. It can be const Nothing.

3. It can be Just . f where f is not strict.

   Just . (1:)
   

4. It can be Just . f where f is strict.

   Just
   

If the function is strict, then the whole thing blows up in an infinite loop (just like fix), and the error isn't seen because we don't know whether we would have had a Nothing or a Just. If it is const Nothing, the function never actually tries to evaluate the error and nothing happens. If it is Just . f and f is not strict, then it's just Just $ fix f (as per the laws: mfix $ return . f = return $ fix f). And, if f is strict, we get Just _|_ (again, per the laws). Notice that we never see the error triggered.

Similar reasoning works for MonadFix (MaybeT m). I think this time it's better just with an example:

runMaybeT $ mfix $ \x -> MaybeT $
             (x `seq` Nothing) :
             Nothing           :
             (Just (1:x))      :
             (Just x)          :
             (x `seq` [])

Each of the four cases I listed above are in that list. The first element of the result is an infinite loop. The second is Nothing. The third is repeat 1, and the fourth is Just an infinite loop. Trying to access the "elements" beyond that triggers another infinite loop, this time caused by []'s MonadFix and not MaybeT's. Again, I don't believe it's possible to trigger the error, because the function would have to force the argument after already deciding that the result was Nothing.

Computation

Answer 2

The definition of bomb is indeed very confusing in the quoted library definition, though the function itself is correctly implemented. By monotonicity, any function f that satisfies f undefined = Nothing has to equal const Nothing. Thus, the fixed-point computation will simply produce the correct answer of Nothing wrapped up in the transformer stack.

For details, see section 4.9 of this work, though the original definition omits the constructors for clarity and the name ErrT is used instead of MaybeT. (MTL didn't exist back in those days!) The definition there is given as follows:

mfixErrM :: (α → ErrT m α) → ErrT m α
mfixErrM f = mfixM (f · unErr)
     where unErr (Ok a) = a

There's also a proof in appendix B.7 to show that this is a valid value-recursion operator for ErrT m whenever the underlying mfixM is a valid value-recursion operator for m.

Nicosia

While you're here.... Would you care to check that the MonadFix Tree instance in the latest version of containers is valid? I waved my hands a bit and added it without a proper proof. – Les

@Les That definition looks good to me! While I haven't carried out the proof, I'm also confident it is also the unique such operator. It would be a nice exercise to show uniqueness using a similar argument to the one given for the list monad in Proposition 4.3.3 of leventerkok.github.io/papers/erkok-thesis.pdf – Nicosia

thanks! I'm confident that it's unique up to laziness details. However, there may be some wiggle room in the laziness. – Les

One can imagine using a lazier version of (!!) as you walk through the children. Is that what you're referring to as the laziness details? I doubt it'd make any difference though, since the spine of the list is well defined at that point. – Nicosia

For lists, the next cons is calculated from the current element. In a tree, perhaps the next cons in a forest could be calculated from the left instead of from above. I don't know if it makes any difference; I don't have much intuition about MonadFix. I also find it hard to imagine a situation where the instances for lists, trees, etc., would be useful. – Les

Once you compute f undefined, you will know exactly what the shape of that forest is at the top-level, i.e., exactly how many elements it has or if it's terminating etc. by monotonicity. So, it doesn't matter at all. I do, however, agree that the tree/list/rose-tree etc. instances are unlikely to be useful. All examples I've seen for such esoteric cases are more or less artificial. The only example I know that is "useful" is that for Fudgets, which is a kind of a "tree" and models a term-semantics for basic IO; discussed in Section 4.8 of the thesis. – Nicosia