[Agda] Right Distributivity

[Philip Wadler]

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
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180322/a8301487/attachment.html>
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180322/a8301487/attachment.ksh>