Continuation introduction rewrite [WIP]

thesis.bib

@@ -74,6 +74,18 @@
   year      = {1996}
 }
 
+@article{KumarBD98,
+  author    = {Sanjeev Kumar and
+               Carl Bruggeman and
+               R. Kent Dybvig},
+  title     = {Threads Yield Continuations},
+  journal   = {{LISP} Symb. Comput.},
+  volume    = {10},
+  number    = {3},
+  pages     = {223--236},
+  year      = {1998}
+}
+
 # Programming with continuations
 @InProceedings{FriedmanHK84,
   author    = {Daniel P. Friedman
@@ -912,8 +924,6 @@
   year      = {2000}
 }
 
-
-
 # CPS for effect handlers
 @inproceedings{HillerstromLAS17,
   author    = {Daniel Hillerstr{\"{o}}m and
@@ -953,6 +963,23 @@
   year      = {2020}
 }
 
+# SECD machine
+@article{Landin64,
+  author = {Peter J. Landin},
+  title = {The Mechanical Evaluation of Expressions},
+  journal = {The Computer Journal},
+  volume = {6},
+  number = {4},
+  pages = {308-320},
+  year = {1964},
+  month = {01},
+  issn = {0010-4620},
+  OPTdoi = {10.1093/comjnl/6.4.308},
+  OPTurl = {https://doi.org/10.1093/comjnl/6.4.308},
+  OPTeprint = {https://academic.oup.com/comjnl/article-pdf/6/4/308/1067901/6-4-308.pdf},
+}
+
+
 # CEK & C
 @InProceedings{FelleisenF86,
   title={Control Operators, the {SECD}-machine, and the $\lambda$-Calculus},
@@ -2409,3 +2436,17 @@
   publisher = {{ACM}},
   year      = {1987}
 }
+
+# Stack copying technique without direct access to the stack.
+@inproceedings{PettyjohnCMKF05,
+  author    = {Greg Pettyjohn and
+               John Clements and
+               Joe Marshall and
+               Shriram Krishnamurthi and
+               Matthias Felleisen},
+  title     = {Continuations from generalized stack inspection},
+  booktitle = {{ICFP}},
+  pages     = {216--227},
+  publisher = {{ACM}},
+  year      = {2005}
+}

thesis.tex

@@ -514,59 +514,68 @@ handlers.
 
 \chapter{Continuations}
 \label{ch:continuations}
+
+A continuation represents the remainder of computation at a given
+point during evaluation. Continuations are one of those canonical
+ideas, that have been discovered multiple times and whose definition
+predates their use~\cite{Reynolds93}. The term `continuation' was
+coined by \citet{StracheyW74}, who used continuations to give a
+denotational semantics to programming languages with unrestricted
+jumps~\cite{StracheyW00}.
+
 % The significance of continuations in the programming languages
 % literature is inescapable as continuations have found widespread use .
 %
 
-A continuation is an abstract data structure that captures the
-remainder of the computation from some given point in the computation.
-%
-The exact nature of the data structure and the precise point at which
-the remainder of the computation is captured depends largely on the
-exact notion of continuation under consideration.
-%
-It can be difficult to navigate the existing literature on
-continuations as sometimes the terminologies for different notions of
-continuations are overloaded or even conflated.
-%
-As there exist several notions of continuations, there exist several
-mechanisms for programmatic manipulation of continuations. These
-mechanisms are known as control operators.
-%
-A substantial amount of existing literature has been devoted to
-understand how to program with individual control operators, and to a
-lesser extent how the various operators compare.
+% A continuation is an abstract data structure that captures the
+% remainder of the computation from some given point in the computation.
+% %
+% The exact nature of the data structure and the precise point at which
+% the remainder of the computation is captured depends largely on the
+% exact notion of continuation under consideration.
+% %
+% It can be difficult to navigate the existing literature on
+% continuations as sometimes the terminologies for different notions of
+% continuations are overloaded or even conflated.
+% %
+% As there exist several notions of continuations, there exist several
+% mechanisms for programmatic manipulation of continuations. These
+% mechanisms are known as control operators.
+% %
+% A substantial amount of existing literature has been devoted to
+% understand how to program with individual control operators, and to a
+% lesser extent how the various operators compare.
 
-The purpose of this chapter is to provide a contemporary and
-unambiguous characterisation of the notions of continuations in
-literature. This characterisation is used to classify and discuss a
-wide range of control operators from the literature.
+% The purpose of this chapter is to provide a contemporary and
+% unambiguous characterisation of the notions of continuations in
+% literature. This characterisation is used to classify and discuss a
+% wide range of control operators from the literature.
 
-% Undelimited control: Landin's J~\cite{Landin98}, Reynolds'
-% escape~\cite{Reynolds98a}, Scheme75's catch~\cite{SussmanS75} ---
-% which was based the less expressive MacLisp catch~\cite{Moon74},
-% callcc is a procedural variation of catch. It was invented in
-% 1982~\cite{AbelsonHAKBOBPCRFRHSHW85}.
+% % Undelimited control: Landin's J~\cite{Landin98}, Reynolds'
+% % escape~\cite{Reynolds98a}, Scheme75's catch~\cite{SussmanS75} ---
+% % which was based the less expressive MacLisp catch~\cite{Moon74},
+% % callcc is a procedural variation of catch. It was invented in
+% % 1982~\cite{AbelsonHAKBOBPCRFRHSHW85}.
 
-A full formal comparison of the control operators is out of scope of
-this chapter. The literature contains comparisons of various control
-operators along various dimensions, e.g.
-%
-\citet{Thielecke02} studies a handful of operators via double
-barrelled continuation passing style. \citet{ForsterKLP19} compare the
-relative expressiveness of untyped and simply-typed variations of
-effect handlers, shift/reset, and monadic reflection by means of
-whether they are macro-expressible. Their work demonstrates that in an
-untyped setting each operator is macro-expressible, but in most cases
-the macro-translations do not preserve typeability, for instance the
-simple type structure is insufficient to type the image of
-macro-translation between effect handlers and shift/reset.
-%
-However, \citet{PirogPS19} show that with a polymorphic type system
-the translation preserve typeability.
-%
-\citet{Shan04} shows that dynamic delimited control and static
-delimited control is macro-expressible in an untyped setting.
+% A full formal comparison of the control operators is out of scope of
+% this chapter. The literature contains comparisons of various control
+% operators along various dimensions, e.g.
+% %
+% \citet{Thielecke02} studies a handful of operators via double
+% barrelled continuation passing style. \citet{ForsterKLP19} compare the
+% relative expressiveness of untyped and simply-typed variations of
+% effect handlers, shift/reset, and monadic reflection by means of
+% whether they are macro-expressible. Their work demonstrates that in an
+% untyped setting each operator is macro-expressible, but in most cases
+% the macro-translations do not preserve typeability, for instance the
+% simple type structure is insufficient to type the image of
+% macro-translation between effect handlers and shift/reset.
+% %
+% However, \citet{PirogPS19} show that with a polymorphic type system
+% the translation preserve typeability.
+% %
+% \citet{Shan04} shows that dynamic delimited control and static
+% delimited control is macro-expressible in an untyped setting.
 
 \section{Classifying continuations}
 
@@ -2254,7 +2263,7 @@ implementation strategies.
     \hline
     Effekt   & Lexical effect handlers & ??\\
     \hline
-    Frank    & N-ary effect handlers & Abstract machine \\
+    Frank    & N-ary effect handlers & CEK machine \\
     \hline
     Gauche   & callcc, shift/reset & Virtual machine \\
     \hline
@@ -2272,8 +2281,8 @@ implementation strategies.
     \hline
     Racket & callcc, \textCallcomc{}, cupto, fcontrol, control/prompt, shift/reset, splitter, spawn & Segmented stacks\\
     \hline
-    Rhino JavaScript      & JI                & Interpreter \\
-    \hline
+    % Rhino JavaScript      & JI                & Interpreter \\
+    % \hline
     Scala                 & shift/reset       & CPS\\
     \hline
     SML/NJ                & callcc            & CPS\\
@@ -2339,24 +2348,70 @@ slight variation of segmented stacks optimised for one-shot
 continuations, which has been adapted by Multicore
 OCaml~\cite{DolanEHMSW17}.
 
-\dhil{TODO: abstract machines}
-
-Continuation passing style (CPS) is a particular idiomatic notation
-for programs, where every aspect of control flow is made explicit,
-which makes it a good fit for implementing control abstractions.
+Full stack copying and segmented stacks both depend on being able to
+manipulate the stack directly. This is seldom possible if the language
+implementer do not have control over the target runtime,
+e.g. compilation to JavaScript. However, it is possible to emulate
+stack copying and segmented stacks in lieu of direct stack access. For
+example, \citet{PettyjohnCMKF05} describe a technique that emulates
+stack copying by piggybacking on the facile stack inception facility
+provided by exception handlers in order to lazily reify the control
+stack.
 %
-Using trampolines CPS is even a viable strategy in environments that
-lack proper tail calls such as JavaScript~\cite{GanzFW99}.
+\citet{KumarBD98} emulated segmented stacks via threads. Each thread
+has its own local stack, and as such, a collection of threads
+effectively models segmented stacks. To actually implement
+continuations as threads \citeauthor{KumarBD98} also made use of
+standard synchronisation primitives.
+%
+The advantage of these techniques is that they are generally
+applicable and portable. The disadvantage is the performance overhead
+induced by emulation.
 
-% \paragraph{Continuation marks}
+Abstract and virtual machines are a form of full machine emulation. An
+abstract machine is an idealised machine. Abstract machines, such as
+the CEK machine~\cite{FelleisenF86}, are attractive because they
+provide a suitably high-level framework for defining language
+semantics in terms of control string manipulations, whilst admitting a
+direct implementation.
+%
+We will discuss abstract machines in more detail in
+Chapter~\ref{ch:abstract-machine}.
+%
+The term virtual machine typically connotes an abstract machine that
+works on a byte code representation of programs, whereas the default
+connotation of abstract machine is a machine that works on a rich
+abstract syntax tree representation of programs.
+% \citeauthor{Landin64}'s SECD machine was the
+% first abstract machine for evaluating $\lambda$-calculus
+% terms~\cite{Landin64,Danvy04}.
+%
+% Either machine model has an explicit representation of the control
+% state in terms of an environment and a control string. Thus either machine can  to the
+% interpretative overhead.
+The disadvantage of abstract machines is their interpretative
+overhead, although, techniques such as just-in-time compilation can be
+utilised to reduce this overhead.
 
-% \paragraph{Continuation passing style}
-
-% \paragraph{Abstract and virtual machines}
-
-% \paragraph{Segmented stacks}
-
-% \paragraph{Stack copying}
+Continuation passing style (CPS) is a canonical implementation
+strategy for continuations --- the word `continuation' even feature in
+its name.
+%
+CPS is a particular idiomatic notation for programs, where every
+function takes an additional argument, the current continuation, as
+input and every function call appears in tail position. Consequently,
+every aspect of control flow is made explicit, which makes CPS a good
+fit for implementing control abstraction. In classic CPS the
+continuation argument is typically represented as a heap allocated
+closure~\cite{Appel92}, however, as we shall see in
+Chapter~\ref{ch:cps} richer representations of continuations are
+possible.
+%
+At first thought it may seem that CPS will not work well in
+environments that lack proper tail calls such as JavaScript. However,
+the contrary is true, because the stackless nature of CPS means it can
+readily be implemented with a trampoline~\cite{GanzFW99}. Alas, at the
+cost of the indirection induced by the trampoline.
 
 \part{Design}
 
@@ -8391,6 +8446,7 @@ then in the image $\cps{M}\,k \reducesto^\ast k\,\cps{V}$.
 \paragraph{Partial evaluation}
 
 \chapter{Abstract machine semantics}
+\label{ch:abstract-machine}
 \dhil{The text is this chapter needs to be reworked}
 
 In this chapter we develop an abstract machine that supports deep and