[Haskell-cafe] Ord methods too strict?

[V.Liepelt]

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 <olf at aatal-apotheke.de> 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
>