Philip Wadler

2018-03-22 20:55:19 UTC

Permalink

In Algebra.FunctionProperties one finds the definitions:Raw Message

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

_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â x y z â ((x + y) * z) â ((x * z) + (y * z))

. \ 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/