[Agda] Right Distributivity

[Philip Wadler]

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? 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/

[Nils Anders Danielsson]

_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)).

[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/

Post by Nils Anders Danielsson

Post by Philip Wadler
_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)),
((y + z) * x) ≈ ((y * x) + (z * x)).
--
/NAD

[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

Post by 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/

Post by Nils Anders Danielsson

Post by Philip Wadler
_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)),
((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
https://lists.chalmers.se/mailman/listinfo/agda

[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/

Post by 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

Post by 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/

Post by Nils Anders Danielsson

Post by Philip Wadler
_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)),
((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
https://lists.chalmers.se/mailman/listinfo/agda