[Agda] Right Distributivity

[Matthew Daggitt]

Hi Philip,
 I agree, it should be the other way round, but I'm afraid changing it
would not only break large sections of the library, it'd also break
everyone else's code. I'm afraid it's just one of those things we're going
to have to live with and chalk up to being sub-optimal.
Apologies,
Matthew

On Thu, Mar 22, 2018 at 9:51 PM, Philip Wadler <wadler at inf.ed.ac.uk> wrote:

> Thanks, Nils. I can see how that definition makes a little of the code
> easier to write, but it makes the library harder to use. I'd be happy to
> update the relevant files appropriately, but I don't know how much that
> would break elsewhere. Do you think it would be worthwhile to attempt a
> fix? Cheers, -- P
>
> .   \ Philip Wadler, Professor of Theoretical Computer Science,
> .   /\ School of Informatics, University of Edinburgh
> .  /  \ and Senior Research Fellow, IOHK
> . http://homepages.inf.ed.ac.uk/wadler/
>
> On 22 March 2018 at 18:22, Nils Anders Danielsson <nad at cse.gu.se> wrote:
>
>> On 2018-03-22 21:55, Philip Wadler wrote:
>>
>>> In Algebra.FunctionProperties one finds the definitions:
>>>
>>>     _DistributesOverˡ_ : Op₂ A → Op₂ A → Set _
>>>     _*_ DistributesOverˡ _+_ =
>>>        ∀ x y z → (x * (y + z)) ≈ ((x * y) + (x * z))
>>>
>>>     _DistributesOverʳ_ : Op₂ A → Op₂ A → Set _
>>>     _*_ DistributesOverʳ _+_ =
>>>        ∀ x y z → ((y + z) * x) ≈ ((y * x) + (z * x))
>>>
>>> To me, the  second of these appears ass-backwards. I would expect
>>>
>>>     _DistributesOverʳ_ : Op₂ A → Op₂ A → Set _
>>>     _*_ DistributesOverʳ _+_ =
>>>        ∀ x y z → ((x + y) * z) ≈ ((x * z) + (y * z))
>>>
>>>
>>> What is the rationale for the current definition?
>>>
>>
>> I wrote that code more than ten years ago. My guess would be that I
>> copied the first definition,
>>
>>   (x * (y + z)) ≈ ((x * y) + (x * z)),
>>
>> and then simply swapped the arguments of every instance of _*_:
>>
>>   ((y + z) * x) ≈ ((y * x) + (z * x)).
>>
>> --
>> /NAD
>>
>>
>
> The University of Edinburgh is a charitable body, registered in
> Scotland, with registration number SC005336.
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180322/f8fd246c/attachment.html>