suggestion: use lazy pattern matching for Monoid instances of tuples

[Dan Doel]

This came up elsewhere recently, so I guess I should say something.

Equality does not have anything necessarily to do with some ability to
'compare' 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.

undefined is unequal to (undefined, undefined) because certain programs
will behave differently when given the two as input. This is true even
though (==) isn't one of those programs.

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's behavior on
undefined with regard to how it governs its behavior on well-defined
Haskell programs. That is, examining 'f undefined' will tell you how things
like 'fix f' 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, "this fails a required equation with respect to ill-defined values."

The one thing (that I can see) that the laziness breaks is reducing things
like 'm `mappend`
mempty' 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'm not sure that's important enough for instant veto.


On Sun, Aug 18, 2013 at 2:26 PM, Petr Pudlák <petr.mvd at gmail.com> wrote:

> Sat 17 Aug 2013 10:40:50 PM CEST, Henning Thielemann napsal:
>
>
>> Am 17.08.2013 22:31, schrieb Petr Pudlák:
>>
>>>
>>> Dear haskellers,
>>>
>>> currently the instances are defined as
>>>
>>> |instance (Monoid a,Monoid b) =>Monoid (a,b)where
>>> mempty = (mempty, mempty)
>>> (a1,b1) `mappend` (a2,b2) = (a1 `mappend` a2, b1 `mappend` b2)|
>>>
>>
>>
>> I think that this instance is correct, since it must hold
>>
>> forall x. mappend mempty x = x
>>
>> With your instance you get for x=undefined:
>>
>> mappend mempty undefined = (undefined, undefined)
>>
>>
>> However, the "instance Monoid ()" is too lazy, such that it does not
>> satisfy the identity law.
>>
>>  I have some doubts in this reasoning. Here `undefined` isn't a value we
> can compare, it represents a non-terminating program. How can we compare
> two non-terminating programs for equality? I'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't write a correctly terminating program that would
> observe this inequality (of course, unless we use IO and exception
> catching).
>
> 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'd be able to observe some programs behave incorrectly.
>
> I'd say that with `undefined` we can fail other equality laws. For
> example: For `MonadPlus` we have `m >>= (\x -> mzero) == mzero`. But it
> clearly fails in
> ```haskell
> undefined >>= (\x -> mzero) :: Maybe Int
> ```
> The result is `undefined` instead of `mzero`. (Or does it mean that Maybe
> is broken?)
>
>   Best regards,
>   Petr
>
>
>
> ______________________________**_________________
> Libraries mailing list
> Libraries at haskell.org
> http://www.haskell.org/**mailman/listinfo/libraries<http://www.haskell.org/mailman/listinfo/libraries>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/libraries/attachments/20130818/f0af7df3/attachment.htm>