Can you take a look at this section (and its placement) for
correctness and explanatory value? [Matthew and I talked about adding
this at the end of April and I just got around to it.]
Jay
On Wed, May 21, 2014 at 10:14 AM, j...@racket-lang.org wrote:
jay has updated `master' from dd0f0b6141 to aaa892646a.
http://git.racket-lang.org/plt/dd0f0b6141..aaa892646a
=[ One Commit ]=
Directory summary:
100.0% pkgs/racket-pkgs/racket-doc/scribblings/reference/
~~
aaa8926 Jay McCarthy j...@racket-lang.org 2014-05-21 10:14
:
| Add section on separate compilation to reference
:
M .../scribblings/reference/eval-model.scrbl| 140
+++
=[ Overall Diff ]===
pkgs/racket-pkgs/racket-doc/scribblings/reference/eval-model.scrbl
~~
--- OLD/pkgs/racket-pkgs/racket-doc/scribblings/reference/eval-model.scrbl
+++ NEW/pkgs/racket-pkgs/racket-doc/scribblings/reference/eval-model.scrbl
@@ -599,6 +599,146 @@ top-level variables in higher @tech{phases}, while
module
top-levels are in corresponding higher @tech{phase}s.
@;- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
+@subsection[#:tag separate-compilation]{The Separate Compilation Guarantee}
+
+When a module is compiled, its @tech{phase} 1 is instantiated. This
+can, in turn, trigger the transitive instantiation of many other
+modules at other phases, including phase 1. Racket provides a very
+strong guarantee about this instantiation called The Separate
+Compilation Guarantee:
+
+Any @tech{effects} of the instantiation of the module's phase 1 due
+to compilation on the Racket runtime system are @tech{discarded}.
+
+The guarantee concerns @deftech{effects}. There are two different
+kinds of effects: internal and external.
+
+Internal effects are exemplified by mutation. Mutation is the action
+of a function such as @racket[set-box!], which changes the value
+contained in the box. The modified box is not observable outside of
+Racket, so the effect is said to be internal. By definition,
+internal effects is not detectable outside of the Racket program.
+
+External effects are exemplified by input/output (or I/O). I/O is the
+action of a function such as @racket[tcp-connect], which communicates
+with the operating system to send network packets outside of the
+machine running Racket via the electromagnetic spectrum. The
+transmission of these packets is observable outside of Racket, in
+particular by the receiver computer or any routers in
+between. External effects exist to be detectable outside of the Racket
+program and are often detectable using physical processes.
+
+An effect is @deftech{discarded} when it is no longer detectable. For
+instance, a mutation of a box from @racket[3] to @racket[4] would be
+discarded if it ceases to be detectable that it was ever changed, and
+thus would still contain @racket[3]. Because external effects are
+intrinsically observable outside of Racket, they cannot be discarded,
+because Racket lacks a time-reversal mechanism.
+
+Thus, The Separate Compilation Guarantee only concerns effects like
+mutation, because they are exclusively effects on the Racket runtime
+system and not on the physical universe.
+
+There are many things a Racket program can do that appear to be
+internal effects, but are actually external effects. For instance,
+@racket[bytes-set!] is typically an internal effect, except when the
+bytes were created by @racket[make-shared-bytes] which is allocated in
+space observable by other processes. Thus, effects which modify them
+are not discardable, so @racket[bytes-set!], in this case, is an
+external effect.
+
+The opposite is also true: some things which appear to be external are
+actually internal. For instance, if a Racket program starts multiple
+threads and uses mutation to communicate between them, that mutation
+is purely internal, because Racket's threads are defined entirely
+internally.
+
+Furthermore, whenever a Racket program calls an @tech{unsafe}
+function, the Racket runtime system makes no promises about its
+effects. For instance, all foreign calls use
+@racketmodname[ffi/unsafe], so all foreign calls are unsafe and their
+effects cannot be discarded by Racket.
+
+Finally, The Separate Compilation Guarantee only concerns
+instantiations at phase 1 during compilation and not all phase 1
+instantiations generally, such as when its phase 1 is required and
+used for effects via reflective mechanisms.
+
+The practical consequence of this guarantee is that because effects
+are never visible, no module can detect whether a module it
+@racket[require]s is already compiled. Thus, it can never change the
+compilation of one module to have already compiled a different module.
+In particular, if
