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
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
