[SOLVED] Is mfix for Maybe impossible to be nontrivially total?

Is mfix for Maybe impossible to be nontrivially total?

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?

Solution

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.