suggestion: use lazy pattern matching for Monoid instances of tuples

[Petr Pudlák]

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