[Haskell-cafe] Unnecessarily strict implementations

[Albert Y. C. Lai]

On 10-09-02 12:10 PM, Stephen Sinclair wrote:
> Sorry to go a bit off topic, but I find it funny that I never really
> noticed you could perform less-than or greater-than comparisons on
> Bool values.  What's the semantic reasoning behind allowing relative
> comparisons on booleans?  In what context would you use it?  It seems
> to me a throwback to C's somewhat arbitrary assumption that False=0
> and True=1.

A boolean algebra is also a lattice. The lattice order reflects 
implication. If the boolean algebra is furthermore 2-valued, the order 
is total too. The only possible dispute among people is over False<=True 
vs True<=False, i.e., should "<=" be "implies" or "implied by". But it 
is always correct to pick one and stick with it. This is useful wherever 
implication is useful. Suppose you wrote two functions and you now want 
to prove or quickcheck-test that they are extensionally equal, except 
you only care about arguments satisfying an assumption. You are checking

   (p x) implies (f x == g x)

If you follow the Haskell choice, it is directly

   (p x) <= (f x == g x)

Implication is pervasively useful, but people pervasively 
underappreciate it; they avoid to think in terms of implication when the 
essence is implication. For example, some people say: you can use "not 
(p x) || f x == g x". To that, I reply firstly: you can use solely NAND 
too, why don't you try that. And I reply secondly: implication is more 
direct, one single operator for the pervasive assume-guarantee paradigm, 
minimum boilerplate. There is no need to bring in negation.