Why is `mfix` not total in `MaybeT`

问题:

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.

回答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.

回答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.