Hi Olaf, these are great thoughts, but are we talking about the same thing? I was merely wondering why Ord methods are strict. Best, Vilem

On 2 Jan 2019, at 21:51, Olaf Klinke wrote:

Information-theoretically 'compare' must be stricter than <= because is gives more information: It decides equality, which <= doesn't. Therefore compare must be strict in both arguments. What follows is an argument that there can not be a lazy implementation of <= that behaves like logical implication.

We try to model <= after the logical implication operator. Order-theoretically, the binary operation (<=) should be antitone in the first and monotone in the second argument. The preceding sentence only makes sense once we define a mathematical order on the semantics of Bool. Let's declare the "logical" order

False < undefined < True.

I give a formal justification in Appendix A below. Arrange all nine combinations of type (Bool,Bool) in a 3x3 grid where the first dimension is descending and the second dimension is ascending in the logical order. Now we consider:

(undefined,True) must map to True because (True,True) maps to True and descending in the first argument means ascending in the result.

(False,undefined) must map to True because (False,False) maps to True and ascending in the second argument means ascending in the result.

Further we require (True,False) mapping to False.

But now we're in trouble: A function giving the above three return values requires ambiguous choice, which we don't have available in pure, sequential Haskell, q.e.d. It's the same reason why we can't have (&&) or (||) operators which behave symmetrically w.r.t. the logical order.

Olaf

========== Appendix A

Let R be a binary relation on a set A. The Egli-Milner-lifting of R is a binary relation on the powerset of A. Among several possible liftings, it is the one with the most pleasing properties [1, Theorem 2.12]. Identify the "undefined" value of a type A with the maximal element of the powerset of A, which expresses that "undefined" may evaluate to anything. In Haskell terms:

{-# LANGUAGE Rank2Types #-} module RelationLifting where import Prelude hiding (undefined) type Relation a = a -> a -> Bool type Lifting = forall a. Relation a -> Relation [a] egliMilner :: Lifting egliMilner r xs ys = hoare && smyth where hoare = all (\x -> any (\y -> r x y) ys) xs smyth = all (\y -> any (\x -> r x y) xs) ys true, false, undefined :: [Bool] true = [True] false = [False] undefined = [False,True]

RelationLifting> egliMilner (<=) false undefined True RelationLifting> egliMilner (<=) undefined true True

[1] https://www.cs.le.ac.uk/people/akurz/Papers/kv-relation-lifting.pdf