<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"><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 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 class="">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="HOEnZb"><font color="#888888"><br>
<br>
-- <br>
/NAD<br>
<br>
</font></span></blockquote></div><br></div>