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.

You can't implement this, unless relying on concurrency to evaluate both expressions in parallel (or some unsafe functions hiding the parallelism). It exists in a library as por for "parallel or". — chi
@Federico It's the halting problem. Given or x y, you have to evaluate one of them, at least, to determine whether to return True or False. Whichever of x or y you pick, you run the chance of it being a divergent computation, even if the other is not. Concurrency lets you evaluate each of them "a little at a time", so that if there is non-bottom value, you'll find it eventually. — chepner
I don't have a quick reference, but you could try googling for "por" in lambda calculus, and its related failure of full abstraction of denotational semantics. I think there are some Winskel (?) slides around somewhere. — chi
@chepner I would not relate this to the halting problem, since it can be solved with concurrency. This can be misleading I think -- if this problem were undecidable because of the HP, no amount of concurrency would help. Fortunately, we don't have to decide the HP on x or y to compute por x y since we can run the computations concurrently. It's more related to the lack of concurrency in the lambda calculus, in my eye. — chi

chepner chepner · Accepted Answer · 2019-11-28T17:44:25

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.

Is it possible to implement this function in Haskell?

2 Answers