<p>Forgot to copy the list. Sorry for the duplicates :(</p>
<div class="gmail_quote">On Jul 24, 2012 1:35 PM, &quot;Tristan Seligmann&quot; &lt;<a href="mailto:mithrandi@mithrandi.net">mithrandi@mithrandi.net</a>&gt; wrote:<br type="attribution"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<p>On Jul 24, 2012 12:32 PM, &quot;Twan van Laarhoven&quot; &lt;<a href="mailto:twanvl@gmail.com" target="_blank">twanvl@gmail.com</a>&gt; wrote:<br>
&gt;<br>
&gt; On 2012-07-24 10:10, Christian Sternagel wrote:<br>
&gt;&gt;<br>
&gt;&gt; Dear all,<br>
&gt;&gt;<br>
&gt;&gt; with respect to formal verification of Haskell code I was wondering whether (==)<br>
&gt;&gt; of the Eq class is intended to be commutative (for many classes such<br>
&gt;&gt; requirements are informally stated in their description, since Eq does not have<br>
&gt;&gt; such a statement, I&#39;m asking here). Or are there any known cases where<br>
&gt;&gt; commutativity of (==) is violated (due to strictness issues)?<br>
&gt;<br>
&gt;<br>
&gt; Strictness plays no role for Eq, since to test for equality both sides will have to be fully evaluated.</p>
<p>I don&#39;t think this is necessarily true.  For example:</p>
<p>(==)  :: (Eq a)  =&gt; Maybe a -&gt; Maybe a -&gt; Bool<br>
Nothing == Nothing = True <br>
Nothing == Just _ = False<br>
Just _ == Nothing = False <br>
Just x == Just y = x == y</p>
<p>This particular example is still commutative, however (at least I think it is). </p>
</blockquote></div>