Discussion:
Right Distributivity
(too old to reply)
Philip Wadler
2018-03-22 20:55:19 UTC
Permalink
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
2018-03-22 21:22:23 UTC
Permalink
_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
Philip Wadler
2018-03-22 21:51:05 UTC
Permalink
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
2018-03-22 22:50:51 UTC
Permalink
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
2018-03-22 23:49:27 UTC
Permalink
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
Loading...