[Haskell-cafe] Ord methods too strict?

[Olaf Klinke]

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