Suppose there exists a Haskel-function realizing the halt-problem:
halt :: Integer->Bool
that evaluates to True if x is defined and to False otherwise.
Let's assume we are calling this function in Haskell in another function as
fHalt x = halt (x+1)
I'm wondering what would happen in this situation and if fHalt is monotone. 2 possible answers arise for me:
Haskell uses strict-evaluation for pre-defined operators - i.e. also for (+). If fHalt is now evaluated with BOT, my guess is that BOT+1 has to be evaluated first (resulting in BOT) and thus the overall evaluation does not terminate and also results in BOT.
If somehow Haskell would determine that the inner (x+1) does not terminate (which is impossible due to the halt-problem) the result would be False and fHalt would violate monotonicity.
At this point, I'm irritated since my question already implied a non-realizable halt-function defined in Haskell. Though I would suppose that answer 1. is correct.
The question's presupposition is, of course, false.
But we should at least be sure that
fHalt undefined = halt (undefined + 1)
just because we expect the beta-law to hold without exception.
Now, if this hypothetical halt existed, it should be able to detect that
undefined + 1 = undefined
shouldn't it? Of course, it wouldn't be Haskell which figures that out, but the magic in the halt function.