
No, '=' should not mean an identity but any equivalence relation. Therefore,
we can use whatever equivalence relation suits us. The reasoning you
provided is IMHO rather blur. Anyway, having possibility of using different
equivalence relations is great because they mean different abstraction
classes - and not all of them are isomorphic.
On Mon, Mar 10, 2008 at 9:09 PM, Daniel Fischer
But antisymmetry means that (x <= y) && (y <= x) ==> x = y, where '=' means identity. Now what does (should) 'identity' mean? Depends on the type, I dare say. For e.g. Int, it should mean 'identical bit pattern', shouldn't it? For IntSet it should mean 'x and y contain exactly the same elements', the internal tree-structure being irrelevant. But that means IntSet shouldn't export functions that allow to distinguish (other than by performance) between x and y.
In short, I would consider code where for some x, y and a function f we have (x <= y) && (y <= x) [or, equivalently, compare x y == EQ] but f x /= f y broken indeed.
So for data Foo = Foo Int (Int -> Int), an Ord instance via compare (Foo a _) (Foo b _) = compare a b is okay if Foo is an abstract datatype and outside the defining module it's guaranteed that compare (Foo a f) (Foo b g) == EQ implies (forall n. f n == g n), but not if the data-constructor Foo is exported.