[Haskell-cafe] Is (==) commutative?

[wren ng thornton]

On 7/24/12 9:19 PM, Christian Sternagel wrote:
> Dear all,
>
> Thanks for your replies. Just to clarify: I am fully aware that inside
> Haskell there is no guarantee that certain (intended) requirements on
> type class instances are satisfied. I was asking whether the intention
> for Eq is that (==) is commutative, because if it was, I would require
> that as an axiom for the equivalent of Eq in our formal setting (I'm
> using the proof assistant Isabelle/HOLCF [1]). Afterwards only types for
> which one could prove commutativity could be instances of Eq. But if
> there where already "standard" instances which violated this
> requirement, adding it in the formal setting would prevent it from being
> applicable to "standard" Haskell programs.

Indeed, the standard wisdom is that Eq ought to denote an equivalence 
relation.

However, the instance for Double and Float is not an equivalence 
relation. This is "necessary" due to Double/Float vaguely matching the 
IEEE-754 spec which requires that NaN /= NaN. If NaN is removed, I think 
Double/Float ought to behave as desired--- though there was a recent 
kerfluffle about the fact that the CPU-internal representation of 
Double/Float has more bits of precision than the in-memory 
representation, so vagaries about when values leave registers to be 
stored in memory will affect whether two values come out to be equal or 
not. Not to mention that Float/Double violate numerous laws of other 
classes; e.g., Ord is not a total ordering because of NaN; Num is not a 
ring because addition and multiplication are not associative (they are 
commutative though);...

Depending on what your goals are, it may be best to avoid the entire 
cesspool of floating point numbers. It would limit the applicability of 
your work, though if analysis of number crunching isn't your goal then 
it's a legitimately pragmatic option.


Another point to bear in mind is that even though Eq is widely 
recognized as denoting an equivalence relation, people sometimes 
willfully subvert this intention. I'm thinking in particular of the fact 
that the Num class has, until recently, required an Eq instance--- which 
in turn precludes some useful/cute Num instances like lifting Num 
operations over (Num b => a -> b), or implementing powerseries as 
infinite lists, etc.

-- 
Live well,
~wren