[Haskell-cafe] Is (==) commutative?
wren ng thornton
wren at freegeek.org
Mon Jul 30 06:20:39 CEST 2012
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
More information about the Haskell-Cafe
mailing list