Theory of effects #165
Theory of effects #165
Conversation
Also begin to link them as `tech` concepts
And distinguish it from effect locality. Also introduce a few more concepts like "pure projection" that may be useful in characterizing effects.
countvajhula
force-pushed
the
theory-of-effects
branch
from
b88fddf
to
2816fa3
Compare
| @; This relation, like the usual strict order relation on numbers, is | ||
| @; irreflexive (f isn't upstream of itself, not f < f), | ||
| @; asymmetric (f < g ⇒ not g < f) | ||
| @; and transitive (f < g and g < h ⇒ f < h) |
There was a problem hiding this comment.
If you want the "not less than character": ≮.
|
|
||
| In general, pure functions (that is, functions free of such effects) are easier to understand and easier to reuse, and favoring their use is considered good functional style. But of course, it's necessary for your code to actually do things besides compute values, too! There are many ways in which you might combine effects and pure functions, from mixing them freely, as you might in Racket, to extracting them completely using monads, as you might in Haskell. Qi encourages using pure functions side by side with what we could call "pure effects." | ||
| In general, pure functions (that is, functions free of such effects) are easier to understand and easier to reuse, and favoring their use is considered good functional style. But of course, it's necessary for your code to actually do things besides compute values, too! There are many ways in which you might combine effects and pure functions, from mixing them freely, as you might in Racket, to extracting them completely using monads, as you might in Haskell. Qi encourages using pure functions side by side with what we could call @deftech{pure effects}. |
There was a problem hiding this comment.
TODO: perhaps "pure effect" is confusing here. With care, it can be read as distinguishing between purely effectful computations and effectful computations which also does something else (what? In the meeting, we proposed "not having output" as being "purely effectful" whereas a computation with outputs is not "purely effectful").
Perhaps we should find a substitute for "pure" to avoid mixing terminology.
|
(possibly unrelated) nit: The following paragraph needlessly ties
—Qi docs, I suggest something more like |
|
An original comment chain on |
|
RE: effects within |
|
RE: "syntax warnings," what produces the "unused identifer" annotations in Racket Mode/DrRacket/racket-langserver? |
|
RE: the effect relation, if the |
|
|
||
| Well-ordering is defined in relation to a source program encoding the intended meaning of the flow, which serves as the point of reference for program translations. Qi guarantees that effects will remain well-ordered through any such translations of the source program that are undertaken during @seclink["It_s_Languages_All_the_Way_Down"]{optimization}. As we will soon see, this guarantee assumes, and prescribes, that effects employed in flows be @tech{local}. | ||
|
|
||
| @definition["Effect locality"]{@tech{Effects} in a flow F are said to be @deftech{local} if the @tech{output} of F is invariant under all @tech{well-orderings} of effects. Specifically, if a @techlink[#:key "well-ordering"]{well-ordered} program translation causes a program to produce different @tech{output}, then the program contains @deftech{nonlocal} effects.} |
There was a problem hiding this comment.
The word "local" for this property is a little confusing to me, because the effects may in fact impact each other at a great syntactic or temporal distance! It's just that they're restricted to be related by the dependency structure of the flows.
There was a problem hiding this comment.
I don't see an explicit definition of what it means to be a well-ordered program transformation, as opposed to effects in a program being well-ordered. At the same time, bringing in the issue of program transformations at all and what properties they need to maintain seems like it should be in separate developer documentation.
| @@ -21,7 +37,7 @@ | |||
|
|
|||
| A @deftech{flow} is either made up of flows, or is a native (e.g. Racket) @seclink["lambda" #:doc '(lib "scribblings/guide/guide.scrbl")]{function}. Flows may be composed using a number of combinators that could yield either linear or nonlinear composite flows. | |||
There was a problem hiding this comment.
Dominik pointed out that this definition identifies flows semantically with functions (and also a couple of paragraphs below). That may not be the case in general, especially if we allow users to indicate the backend.
| @@ -21,7 +37,7 @@ | |||
|
|
|||
| A @deftech{flow} is either made up of flows, or is a native (e.g. Racket) @seclink["lambda" #:doc '(lib "scribblings/guide/guide.scrbl")]{function}. Flows may be composed using a number of combinators that could yield either linear or nonlinear composite flows. | |||
|
|
|||
| A flow in general accepts @code{m} inputs and yields @code{n} outputs, for arbitrary non-negative integers @code{m} and @code{n}. We say that such a flow is @code{m × n}. | |||
| A flow in general accepts @code{m} @deftech{inputs} and yields @code{n} @deftech{outputs}, for arbitrary non-negative integers @code{m} and @code{n}. We say that such a flow is @code{m × n}. Inputs and outputs are ordinary @tech/reference{values}. | |||
There was a problem hiding this comment.
Looks like we do mention "non-negative integers" here so it entails pure effects as we are currently defining them @dzoe.
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:
For more context, see the meeting notes, especially Side Effects Include Confusion and Schrodinger's Probe.
Public Domain Dedication
(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.)