<div dir="ltr"><div><div><div><div>This came up elsewhere recently, so I guess I should say something.<br><br></div>Equality does not have anything necessarily to do with some ability to &#39;compare&#39; things decidably. For instance, one can implement the computable real numbers as functions from a precision to a rational approximation at that precision. Given this representation, it is impossible to algorithmically decide that two real numbers are equal; one can only decide that two distinct numbers are not equal. However, that does not mean that a notion of equality does not exist, or that we cannot demonstrate the equality of two real numbers, even if we cannot decide whether two arbitrary numbers are equal or not.<br>

<br></div>undefined is unequal to (undefined, undefined) because certain programs will behave differently when given the two as input. This is true even though (==) isn&#39;t one of those programs.<br><br></div>However, I do think there is a lot to be said toward axioms holding for bottom being a low priority. Roughly, I care about a function&#39;s behavior on undefined with regard to how it governs its behavior on well-defined Haskell programs. That is, examining &#39;f undefined&#39; will tell you how things like &#39;fix f&#39; will work, but I only care about the latter, not the former, in itself. But the situation under discussion here is exactly one where we are talking about making more programs well-defined, which I tend to think trumps, &quot;this fails a required equation with respect to ill-defined values.&quot;<br>

<br></div>The one thing (that I can see) that the laziness breaks is reducing things like &#39;m `mappend` <br>mempty&#39; to just m, and it can only break when the context in which the expression appears requires just the tuple structure to avoid vicious circularity. I&#39;m not sure that&#39;s important enough for instant veto.<br>

</div><div class="gmail_extra"><br><br><div class="gmail_quote">On Sun, Aug 18, 2013 at 2:26 PM, Petr Pudlák <span dir="ltr">&lt;<a href="mailto:petr.mvd@gmail.com" target="_blank">petr.mvd@gmail.com</a>&gt;</span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Sat 17 Aug 2013 10:40:50 PM CEST, Henning Thielemann napsal:<div class="im"><br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<br>
Am 17.08.2013 22:31, schrieb Petr Pudlák:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<br>
Dear haskellers,<br>
<br>
currently the instances are defined as<br>
<br>
|instance (Monoid a,Monoid b) =&gt;Monoid (a,b)where<br>
mempty = (mempty, mempty)<br>
(a1,b1) `mappend` (a2,b2) = (a1 `mappend` a2, b1 `mappend` b2)|<br>
</blockquote>
<br>
<br>
I think that this instance is correct, since it must hold<br>
<br>
forall x. mappend mempty x = x<br>
<br>
With your instance you get for x=undefined:<br>
<br>
mappend mempty undefined = (undefined, undefined)<br>
<br>
<br>
However, the &quot;instance Monoid ()&quot; is too lazy, such that it does not<br>
satisfy the identity law.<br>
<br>
</blockquote></div>
I have some doubts in this reasoning. Here `undefined` isn&#39;t a value we can compare, it represents a non-terminating program. How can we compare two non-terminating programs for equality? I&#39;d say we can only say that two non-terminating programs are unequal, if they produce a partial results that are different. For example, `(undefined, 1)` is unequal `(undefined, 2)`. But how can we observe that `undefined` is distinct from `(undefined, undefined)`? We can&#39;t write a correctly terminating program that would observe this inequality (of course, unless we use IO and exception catching).<br>

<br>
The only thing this additional laziness can change is to make some non-terminating programs terminating. This is very different than from having an instance that fails an equality law with defined values, in such a case we&#39;d be able to observe some programs behave incorrectly.<br>

<br>
I&#39;d say that with `undefined` we can fail other equality laws. For example: For `MonadPlus` we have `m &gt;&gt;= (\x -&gt; mzero) == mzero`. But it clearly fails in<br>
```haskell<br>
undefined &gt;&gt;= (\x -&gt; mzero) :: Maybe Int<br>
```<br>
The result is `undefined` instead of `mzero`. (Or does it mean that Maybe is broken?)<br>
<br>
  Best regards,<br>
  Petr<div class="HOEnZb"><div class="h5"><br>
<br>
<br>
______________________________<u></u>_________________<br>
Libraries mailing list<br>
<a href="mailto:Libraries@haskell.org" target="_blank">Libraries@haskell.org</a><br>
<a href="http://www.haskell.org/mailman/listinfo/libraries" target="_blank">http://www.haskell.org/<u></u>mailman/listinfo/libraries</a><br>
</div></div></blockquote></div><br></div>