Is mfix for Maybe impossible to be nontrivially total?

Question

Since Nothing >>= f = Nothing for every f, the following trivial definition is suitable for mfix:

mfix _ = Nothing

But this has no practical use, so we have the following nontotal definition:

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

It would be nice if mfix f returned Nothing if this let-clause wouldn't halt. (For example, f = Just . (1+))
Is this impossible because the Halting Problem is unsolvable?

Answer 1

One of the MonadFix laws says that the monadic fixpoint must coincide with the pure fixpoint when the monadic action is pure:

mfix (return . f) = return (fix f)

Because of this, the following is required:

mfix (Just . (1+)) = mfix (return . (1+))
                   = return (fix (1+))
                   = Just (fix (1+))

And fix (1+) is indeed bottom. So for your proposed function, the laws specify exactly how mfix must behave (and it does behave this way).

Independently of whether the instance is law-abiding, we can ask whether we like the laws, or perhaps whether it might be useful to have another function, with a different name and different laws, that behaves as you propose; e.g. in particular these two calls should behave like this:

mfix' (Just . (1+)) = Nothing
mfix' (Just . const 1) = Just 1

This is impossible to implement for exactly the reason you say: the halting problem tells us that it's not possible to know for sure whether fix f will loop or finish for arbitrary f. We can approximate this function in a variety of ways, but all will eventually fall short of perfection in this regard.