qi
qi copied to clipboard
Theory of effects
Summary of Changes
This PR elaborates Qi's theory of effects. The main result is the following:
"Qi guarantees that the output of execution of the compiled program is the same as that of the source program, assuming effects are local, and further, it guarantees that the effects will be well-ordered in relation to the source program."
The rest of these changes are supporting explanations, examples and advice, including:
- introduces the concept of "well ordering" of effects as being a natural functional guarantee
- explains how this guarantee is well behaved with "local" effects
- improves the discussion of Schrodinger's probe
- misc other improvements, including linking defined concepts
For more context, see the meeting notes, especially Side Effects Include Confusion and Schrodinger's Probe.
Public Domain Dedication
- [x] In contributing, I relinquish any copyright claims on my contribution and freely release it into the public domain in the simple hope that it will provide value.
(Why: The freely released, copyright-free work in this repository represents an investment in a better way of doing things called attribution-based economics. Attribution-based economics is based on the simple idea that we gain more by giving more, not by holding on to things that, truly, we could only create because we, in our turn, received from others. As it turns out, an economic system based on attribution -- where those who give more are more empowered -- is significantly more efficient than capitalism while also being stable and fair (unlike capitalism, on both counts), giving it transformative power to elevate the human condition and address the problems that face us today along with a host of others that have been intractable since the beginning. You can help make this a reality by releasing your work in the same way -- freely into the public domain in the simple hope of providing value. Learn more about attribution-based economics at drym.org, tell your friends, do your part.)
(possibly unrelated) nit: The following paragraph needlessly ties effect
to the semantics of tee
(the equivalences in the preceding paragraph are useful, but explaining the implementation seems gratuitous):
Remember that, as the side-effect flow is based on a tee junction, it must handle as many inputs as the main flow. For instance, if you were to use displayln as the side-effect, it wouldn’t work if more than one value were flowing, and you’d get an inscrutable error resembling:
—Qi docs, effect
form
I suggest something more like
The effect flow must handle as many inputs as the main flow `flo`. For instance, if you were to use…
An original comment chain on readout
, Shrodinger's probe, and effects: https://github.com/drym-org/qi/pull/152#discussion_r1526209817
RE: effects within esc
: https://github.com/drym-org/qi/pull/152#discussion_r1465021409, https://github.com/drym-org/qi/pull/152#discussion_r1466456812. I think some of these were addressed, but I also think the conversation re-arose during today's meeting.
RE: "syntax warnings," what produces the "unused identifer" annotations in Racket Mode/DrRacket/racket-langserver?
RE: the effect relation, if the ordering
function (judgement?) Michael proposed is writable: it will likely to be easier with a smaller core syntax.