Is it possible to implement this function in Haskell?

Question

At the page https://en.wikibooks.org/wiki/Haskell/Denotational_semantics#Pattern_Matching there is the following exercise:

Consider a function or of two boolean arguments with the following properties:

• or ⊥ ⊥ = ⊥
• or True ⊥ = True
• or ⊥ True = True
• or False y = y
• or x False = x

This function is another example of joint strictness, but a much sharper one: the result is only ⊥ if both arguments are (at least when we restrict the arguments to True and ⊥). Can such a function be implemented in Haskell?

The function can be represented with the following table:

      |   ⊥   | False | True
------|-----------------------
  ⊥   |   ⊥   |   ⊥   | True
False |   ⊥   | False | True
True  | True  | True  | True

This function is monotone according to the definition given in https://en.wikibooks.org/wiki/Haskell/Denotational_semantics#Monotonicity, so I don't see a reason to exclude the possibility of implementing this function in Haskell. Nonetheless, I don't see a way to implement it.

What is the answer to the exercise?

PS: I get that the answer is "no, you can't". What I'm looking for is a rigorous proof. I feel I'm missing some important restriction on what functions can be defined. Definitely not all monotone functions.

Answer 1

Suppose you were to try to evaluate or x y. To do so, you have to pick one argument or the other to see if evaluating it leads to True or False. If you guess correctly, you'll figure out if the result should be True or False without having to evaluate the other argument (which might be ⊥).

If you guess wrong, though, you'll never finish evaluating the argument; either you'll get stuck in an infinite loop or you'll get a runtime error.

---

Concurrency lets you evaluate both arguments in parallel[1]. Assuming one of the two arguments evaluates to a proper Boolean, one of the two branches will succeed in finding it. The other branch will either raise an error (in which case you can simply discard that branch and ignore the error) or get stuck in a loop (which you can terminate by force when the other branch succeeds). Either way, you can get the correct answer eventually.

If both arguments lead to ⊥, of course, the implicit result of or will still be ⊥; you can't completely bypass the halting problem.

---

[1] By "parallel", I don't necessarily mean forking another process and evaluating them simultaneously. You can evaluate one argument for N steps (for some value N and whatever "step" means); if an error is raised, give up and try the other argument, and if you haven't terminated yet, suspend this thread and try the other one for N steps. Keep bouncing back and forth between the two until one of them produces a concrete value.