3 ms·
Cool. A Dijkstra note. Thanks for sharing. The distributivity argument is a bit sketchy, though. It defines g.p := p▫q, meaning that g implicitly depends on q,
by xelxebar 2y ago
Cool. A Dijkstra note. Thanks for sharing.
The distributivity argument is a bit sketchy, though. It defines g.p := p▫q, meaning that g implicitly depends on q, but then writes f(y▫z) = f(g.y) and fy▫fz = g.f(y), where in the first instance g.x = x▫y and in the second g.x = x▫fz.
That said, I do see the point. The distributive rule let's us commute the order in which we compute addition and multiplication. Generally, I guess if we have some family of arrows A and B, where all commutative diagrams Bx∘Ay = Az∘Bw hold, then we can say "A and B commute". This can probably be expressed as some literal commutativity using natural transformations, but I'll need to think on it some more.
Thanks for the prod!
- mathgenius 2y agoThis is likely the same as a distributive law of monads... https://ncatlab.org/nlab/show/distributive+law https://ncatlab.org/nlab/show/distributive+law on good days i might understand this stuff.. Another less high-brow connection: associativity of matrix multiplication relies on the usual distributivity law..
- 082349872349872 2y agoYes: the requirement of commutativity in the "addition" for distributivity to work with a noncommutative "multiplication" is exactly why my current model for code* is based on an (anathema to practicing programmers) unordered choice. * and also data; with suitable choices of definitions there are very few differences between the left and right hand arguments to application.