2008/3/11, David Menendez
I think Adrian is just arguing that a == b should imply f a == f b, for all definable f, in which case it doesn't *matter* which of two equal elements you choose, because there's no semantic difference.
(Actually, it's probably not desirable to require it for *all* definable functions, since an implementation might define e.g. an unsafe function that does pointer comparisons. We'd probably also exclude functions using a private, "internal" interface that exposes implementation details.)
I like that property, and it bugs me when I have to use a datatype whose Eq instance doesn't have it (either because (==) throws away information or because the type exposes non-semantic information).
I completely agree that this propriety should be true for all Eq instance exported by a public module. I don't care if it is not the case in a isolated code, but libraries shouldn't break expected invariant (or at least be very cautious and warn the user). Even Eq Double respects this propriety as far as I know. Ord case is less evident, but assuming a propriety like (compare x y = EQ => x == y) seems like a reasonable guess. Doing it in a library (with a warning) doesn't seems all that bad to me. -- Jedaï