No, &#39;=&#39; 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. <br>
<br><div class="gmail_quote">On Mon, Mar 10, 2008 at 9:09 PM, Daniel Fischer &lt;<a href="mailto:daniel.is.fischer@web.de">daniel.is.fischer@web.de</a>&gt; wrote:<br><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">
But antisymmetry means that (x &lt;= y) &amp;&amp; (y &lt;= x) ==&gt; x = y, where &#39;=&#39; means<br>
identity. Now what does (should) &#39;identity&#39; mean?<br>
Depends on the type, I dare say. For e.g. Int, it should mean &#39;identical bit<br>
pattern&#39;, shouldn&#39;t it? For IntSet it should mean &#39;x and y contain exactly<br>
the same elements&#39;, the internal tree-structure being irrelevant. But that<br>
means IntSet shouldn&#39;t export functions that allow to distinguish (other than<br>
by performance) between x and y.<br>
<br>
In short, I would consider code where for some x, y and a function f we have<br>
(x &lt;= y) &amp;&amp; (y &lt;= x) [or, equivalently, compare x y == EQ] but f x /= f y<br>
broken indeed.<br>
<br>
So for<br>
data Foo = Foo Int (Int -&gt; Int),<br>
an Ord instance via compare (Foo a _) (Foo b _) = compare a b<br>
is okay if Foo is an abstract datatype and outside the defining module it&#39;s<br>
guaranteed that<br>
compare (Foo a f) (Foo b g) == EQ implies (forall n. f n == g n), but not if<br>
the data-constructor Foo is exported.<br>
<div><div></div><div class="Wj3C7c"><br>
</div></div></blockquote></div><br>