<div dir="ltr">Fair enough. Thanks! -- P</div><div class="gmail_extra"><br clear="all"><div><div class="gmail_signature" data-smartmail="gmail_signature"><div dir="ltr"><div><div dir="ltr">.   \ Philip Wadler, Professor of Theoretical Computer Science,<br>.   /\ School of Informatics, University of Edinburgh<br></div><div>.  /  \ and Senior Research Fellow, IOHK<br></div><div dir="ltr">. <span><a href="http://homepages.inf.ed.ac.uk/wadler/" target="_blank">http://homepages.inf.ed.ac.uk/wadler/</a></span></div></div></div></div></div>
<br><div class="gmail_quote">On 22 March 2018 at 19:50, Matthew Daggitt <span dir="ltr"><<a href="mailto:matthewdaggitt@gmail.com" target="_blank">matthewdaggitt@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr">Hi Philip,<div> 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.</div><div>Apologies,<br>Matthew</div></div><div class="gmail_extra"><br><div class="gmail_quote"><div><div class="h5">On Thu, Mar 22, 2018 at 9:51 PM, Philip Wadler <span dir="ltr"><<a href="mailto:wadler@inf.ed.ac.uk" target="_blank">wadler@inf.ed.ac.uk</a>></span> wrote:<br></div></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div><div class="h5"><div dir="ltr">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</div><div class="gmail_extra"><span><br clear="all"><div><div class="m_1492972585768529481m_1683360328282268682gmail_signature" data-smartmail="gmail_signature"><div dir="ltr"><div><div dir="ltr">.   \ Philip Wadler, Professor of Theoretical Computer Science,<br>.   /\ School of Informatics, University of Edinburgh<br></div><div>.  /  \ and Senior Research Fellow, IOHK<br></div><div dir="ltr">. <span><a href="http://homepages.inf.ed.ac.uk/wadler/" target="_blank">http://homepages.inf.ed.ac.uk/<wbr>wadler/</a></span></div></div></div></div></div>
<br></span><span><div class="gmail_quote">On 22 March 2018 at 18:22, Nils Anders Danielsson <span dir="ltr"><<a href="mailto:nad@cse.gu.se" target="_blank">nad@cse.gu.se</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><span>On 2018-03-22 21:55, Philip Wadler wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
In Algebra.FunctionProperties one finds the definitions:<br>
<br>
    _DistributesOverˡ_ : Op₂ A → Op₂ A → Set _<br>
    _*_ DistributesOverˡ _+_ =<br>
       ∀ x y z → (x * (y + z)) ≈ ((x * y) + (x * z))<br>
<br>
    _DistributesOverʳ_ : Op₂ A → Op₂ A → Set _<br>
    _*_ DistributesOverʳ _+_ =<br>
       ∀ x y z → ((y + z) * x) ≈ ((y * x) + (z * x))<br>
<br>
To me, the  second of these appears ass-backwards. I would expect<br>
<br>
    _DistributesOverʳ_ : Op₂ A → Op₂ A → Set _<br>
    _*_ DistributesOverʳ _+_ =<br>
       ∀ x y z → ((x + y) * z) ≈ ((x * z) + (y * z))<br>
<br>
<br>
What is the rationale for the current definition?<br>
</blockquote>
<br></span>
I wrote that code more than ten years ago. My guess would be that I<br>
copied the first definition,<br>
<br>
  (x * (y + z)) ≈ ((x * y) + (x * z)),<br>
<br>
and then simply swapped the arguments of every instance of _*_:<br>
<br>
  ((y + z) * x) ≈ ((y * x) + (z * x)).<span class="m_1492972585768529481m_1683360328282268682HOEnZb"><font color="#888888"><br>
<br>
-- <br>
/NAD<br>
<br>
</font></span></blockquote></div><br></span></div>
<br></div></div>The University of Edinburgh is a charitable body, registered in<br>
Scotland, with registration number SC005336.<br>
<br>______________________________<wbr>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mail<wbr>man/listinfo/agda</a><br>
<br></blockquote></div><br></div>
</blockquote></div><br></div>