[Agda] Right Distributivity

[Philip Wadler]

Fair enough. Thanks! -- 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 19:50, Matthew Daggitt <matthewdaggitt at gmail.com> wrote:

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