Controlling continuations [WIP]

macros.tex

@@ -13,6 +13,9 @@
 \newcommand{\Z}{\ensuremath{\mathbb{Z}}}
 \newcommand{\B}{\ensuremath{\mathbb{B}}}
 \newcommand{\BB}[1]{\ensuremath{\mathbf{#1}}}
+\newcommand{\CC}{\keyw{C}}
+% \newcommand{\Delim}[1]{\ensuremath{\langle\!\!\mkern-1.5mu\langle#1\rangle\!\!\mkern-1.5mu\rangle}}
+\newcommand{\Delim}[1]{\ensuremath{\langle#1\rangle}}
 
 %%
 %% Partiality

thesis.bib

@@ -16,7 +16,7 @@
     address    =     {Scotland, {UK}},
     optmonth      =     aug,
     year       =     2016,
-    type       = {{MSc(R)} Dissertation}
+    type       = {{MSc(R)} thesis}
 }
 
 # OCaml handlers
@@ -43,7 +43,8 @@
                Leo White},
   title     = {Concurrent System Programming with Effect Handlers},
   booktitle = {{TFP}},
-  series    = {Lecture Notes in Computer Science},
+  OPTseries    = {Lecture Notes in Computer Science},
+  series    = {LNCS},
   volume    = {10788},
   pages     = {98--117},
   publisher = {Springer},
@@ -107,7 +108,8 @@
                Matija Pretnar},
   title     = {Handlers of Algebraic Effects},
   booktitle = {{ESOP}},
-  series    = {Lecture Notes in Computer Science},
+  OPTseries    = {Lecture Notes in Computer Science},
+  series    = {LNCS},
   volume    = {5502},
   pages     = {80--94},
   publisher = {Springer},
@@ -123,10 +125,7 @@
   number    = {4},
   year      = {2013},
   OPTurl       = {http://dx.doi.org/10.2168/LMCS-9(4:23)2013},
-  OPTdoi       = {10.2168/LMCS-9(4:23)2013},
+  OPTdoi       = {10.2168/LMCS-9(4:23)2013}
-  timestamp = {Thu, 31 Aug 4448958 16:06:56 +},
-  biburl    = {http://dblp.uni-trier.de/rec/bib/journals/corr/PlotkinP13},
-  bibsource = {dblp computer science bibliography, http://dblp.org}
 }
 
 @article{PlotkinP03,
@@ -397,7 +396,8 @@
                Andrej Bauer},
   title     = {Runners in Action},
   booktitle = {{ESOP}},
-  series    = {Lecture Notes in Computer Science},
+  OPTseries    = {Lecture Notes in Computer Science},
+  series    = {LNCS},
   volume    = {12075},
   pages     = {29--55},
   publisher = {Springer},
@@ -551,7 +551,8 @@
                Tom Schrijvers},
   title     = {Fusion for Free - Efficient Algebraic Effect Handlers},
   booktitle = {{MPC}},
-  series    = {Lecture Notes in Computer Science},
+  OPTseries    = {Lecture Notes in Computer Science},
+  series    = {LNCS},
   volume    = {9129},
   pages     = {302--322},
   publisher = {Springer},
@@ -675,7 +676,8 @@
                Shin{-}Cheng Mu},
   title     = {Handling Local State with Global State},
   booktitle = {{MPC}},
-  series    = {Lecture Notes in Computer Science},
+  OPTseries    = {Lecture Notes in Computer Science},
+  series    = {LNCS},
   volume    = {11825},
   pages     = {18--44},
   publisher = {Springer},
@@ -925,7 +927,8 @@
                Sam Lindley},
   title     = {Shallow Effect Handlers},
   booktitle = {{APLAS}},
-  series    = {Lecture Notes in Computer Science},
+  OPTseries    = {Lecture Notes in Computer Science},
+  series    = {LNCS},
   volume    = {11275},
   pages     = {415--435},
   publisher = {Springer},
@@ -976,7 +979,8 @@
                Tom Schrijvers},
   title     = {Explicit Effect Subtyping},
   booktitle = {{ESOP}},
-  series    = {Lecture Notes in Computer Science},
+  OPTseries    = {Lecture Notes in Computer Science},
+  series    = {LNCS},
   volume    = {10801},
   pages     = {327--354},
   publisher = {Springer},
@@ -1032,7 +1036,8 @@
  title = {The {OCaml} System Release 4.11: Documentation and user's manual},
  year = 2020,
  month = aug,
- publisher = {Institut National de Recherche en Informatique et en Automatique}
+ OPTpublisher = {Institut National de Recherche en Informatique et en Automatique},
+ publisher = {INRIA}
 }
 
 # Lisp
@@ -1193,7 +1198,7 @@
 # Landin's J operator
 @article{Landin65,
   author    = {Peter J. Landin},
-  title     = {Correspondence between {ALGOL} 60 and Church's Lambda-notation: part
+  title     = {Correspondence between {ALGOL} 60 and {C}hurch's {L}ambda-notation: part
                {I}},
   journal   = {Commun. {ACM}},
   volume    = {8},
@@ -1204,7 +1209,7 @@
 
 @article{Landin65a,
   author    = {Peter J. Landin},
-  title     = {A correspondence between {ALGOL} 60 and Church's Lambda-notations:
+  title     = {A correspondence between {ALGOL} 60 and {C}hurch's {L}ambda-notations:
                Part {II}},
   journal   = {Commun. {ACM}},
   volume    = {8},
@@ -1321,7 +1326,7 @@
 # Simula (coroutines)
 @inproceedings{DahlMN68,
   author    = {Ole-Johan Dahl and Bj\o{}rn Myhrhaug and Kristen Nygaard},
-  title     = {Some Features of the SIMULA 67 Language},
+  title     = {Some Features of the {SIMULA} 67 Language},
   year      = {1968},
   publisher = {Winter Simulation Conference},
   booktitle = {Proceedings of the Second Conference on Applications of Simulations},
@@ -1351,28 +1356,28 @@
 
 # Second-hand reference for call/cc
 @techreport{AbelsonHAKBOBPCRFRHSHW85,
-  author    = {Hal Abelson
+  author    = {William D. Clinger and others},
-               and Chris Haynes
+  @Comment  = {Hal Abelson
-               and Norman Adams
+  @Comment              and Chris Haynes
-               and Eugene Kohlbecker
+  @Comment              and Norman Adams
-               and David Bartley
+  @Comment              and Eugene Kohlbecker
-               and Don Oxley
+  @Comment              and David Bartley
-               and Gary Brooks
+  @Comment              and Don Oxley
-               and Kent Pitman
+  @Comment              and Gary Brooks
-               and William Clinger
+  @Comment              and Kent Pitman
-               and Jonathan Rees
+  @Comment              and William Clinger
-               and Dan Friedman
+  @Comment              and Jonathan Rees
-               and Bill Rozas
+  @Comment              and Dan Friedman
-               and Robert Halstead
+  @Comment              and Bill Rozas
-               and Gerald Jey Sussman
+  @Comment              and Robert Halstead
-               and Chris Hanson
+  @Comment              and Gerald Jey Sussman
-               and Mitchell Wand},
+  @Comment              and Chris Hanson
+  @Comment              and Mitchell Wand},
   title      = {The Revised Revised Report on {Scheme} or An {UnCommon} {Lisp}},
   year        = {1985},
   institution = {MIT},
-  number     = {No. 848},
+  number     = {AIM-848},
-  month      = aug,
+  month      = aug
-  type       = {AI Memo}
 }
 
 # Splitter
@@ -1426,7 +1431,8 @@
   author    = {John C. Reynolds},
   title     = {Towards a theory of type structure},
   booktitle = {Symposium on Programming},
-  series    = {Lecture Notes in Computer Science},
+  OPTseries    = {Lecture Notes in Computer Science},
+  series    = {LNCS},
   volume    = {19},
   pages     = {408--423},
   publisher = {Springer},
@@ -1474,22 +1480,46 @@
 
 # GNU coreutils
 @book{MacKenzieMPPBYS20,
-  author = {David MacKenzie
+  author = {David MacKenzie and others},
-            and Jim Meyering
+  @Comment = {David MacKenzie
-            and Ross Paterson
+  @Comment           and Jim Meyering
-            and François Pinard
+  @Comment           and Ross Paterson
-            and Karl Berry
+  @Comment           and François Pinard
-            and Brian Youmans
+  @Comment           and Karl Berry
-            and Richard Stallman},
+  @Comment           and Brian Youmans
+  @Comment           and Richard Stallman},
   title  = {{GNU} {Coreutils}},
   note   = {For version 8.32},
   month  = feb,
   year   = 2020,
   publisher = {Free Software Foundation},
-  address = {Boston, MA, USA}
+  OPTaddress = {Boston, MA, USA}
 }
 
 # Expressiveness
+@inproceedings{Felleisen90,
+  author    = {Matthias Felleisen},
+  title     = {On the Expressive Power of Programming Languages},
+  booktitle = {{ESOP}},
+  OPTseries    = {Lecture Notes in Computer Science},
+  series    = {LNCS},
+  volume    = {432},
+  pages     = {134--151},
+  publisher = {Springer},
+  year      = {1990}
+}
+
+@article{Felleisen91,
+  author    = {Matthias Felleisen},
+  title     = {On the Expressive Power of Programming Languages},
+  journal   = {Sci. Comput. Program.},
+  volume    = {17},
+  number    = {1-3},
+  pages     = {35--75},
+  year      = {1991},
+  note      = {Revised version}
+}
+
 @inproceedings{CartwrightF92,
   author    = {Robert Cartwright and
                Matthias Felleisen},
@@ -1514,7 +1544,8 @@
   title     = {Interpreting Localized Computational Effects Using Operators of Higher
                Type},
   booktitle = {CiE},
-  series    = {Lecture Notes in Computer Science},
+  OPTseries    = {Lecture Notes in Computer Science},
+  series    = {LNCS},
   volume    = {5028},
   pages     = {389--402},
   publisher = {Springer},
@@ -1638,6 +1669,18 @@
   year      = {1984}
 }
 
+@article{HaynesFW86,
+  author    = {Christopher T. Haynes and
+               Daniel P. Friedman and
+               Mitchell Wand},
+  title     = {Obtaining Coroutines with Continuations},
+  journal   = {Comput. Lang.},
+  volume    = {11},
+  number    = {3/4},
+  pages     = {143--153},
+  year      = {1986}
+}
+
 @techreport{Moggi90,
   title = {An Abstract View of Programming Languages},
   author = {Eugenio Moggi},
@@ -1679,7 +1722,8 @@
   author    = {William L. Harrison},
   title     = {The Essence of Multitasking},
   booktitle = {{AMAST}},
-  series    = {Lecture Notes in Computer Science},
+  OPTseries    = {Lecture Notes in Computer Science},
+  series    = {LNCS},
   volume    = {4019},
   pages     = {158--172},
   publisher = {Springer},
@@ -1693,4 +1737,27 @@
   journal   = {J. Funct. Program.},
   volume    = {25},
   year      = {2015}
+}
+
+# History of continuations
+@article{Reynolds93,
+  author    = {John C. Reynolds},
+  title     = {The Discoveries of Continuations},
+  journal   = {{LISP} Symb. Comput.},
+  volume    = {6},
+  number    = {3-4},
+  pages     = {233--248},
+  year      = {1993}
+}
+
+# Terminology: 'partial' and 'full' continuations
+@inproceedings{JohnsonD88,
+  author    = {Gregory F. Johnson and
+               Dominic Duggan},
+  title     = {Stores and Partial Continuations as First-Class Objects in a Language
+               and its Environment},
+  booktitle = {{POPL}},
+  pages     = {158--168},
+  publisher = {{ACM} Press},
+  year      = {1988}
 }

thesis.tex

@@ -488,9 +488,9 @@ handlers.
 \section{Typed programming languages}
 \label{sec:pls}
 %
-\dhil{Definition of (typed) programming language, conservative extension, macro-expressiveness}
+\dhil{Definition of (typed) programming language, conservative extension, macro-expressiveness~\cite{Felleisen90,Felleisen91}}
 
-\chapter{The state of effectful programming}
+\chapter{State of effectful programming}
 \label{ch:related-work}
 
 \section{Type and effect systems}
@@ -502,13 +502,156 @@ handlers.
 
 \chapter{Controlling continuations}
 \label{ch:continuations}
+% The significance of continuations in the programming languages
+% literature is inescapable as continuations have found widespread use .
+%
 
-Undelimited control: Landin's J~\cite{Landin98}, Reynolds'
+A continuation is an abstract data structure that captures the
-escape~\cite{Reynolds98a}, Scheme75's catch~\cite{SussmanS75} ---
+remainder of the computation from some given point in the computation.
-which was based the less expressive MacLisp catch~\cite{Moon74},
+%
-callcc is a procedural variation of catch. It was invented in
+The exact nature of the data structure and the precise point at which
-1982~\cite{AbelsonHAKBOBPCRFRHSHW85}.
+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.
+
+% 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}.
+
+\section{Notions of continuations}
+
+% \citeauthor{Reynolds93} has written a historical account of the
+% various early discoveries of continuations~\cite{Reynolds93}.
+
+In the literature the term ``continuation'' is often accompanied by a
+qualifier such as full~\cite{JohnsonD88}, partial~\cite{JohnsonD88},
+abortive, escape, undelimited, delimited, composable, or functional.
+%
+Some of these qualifiers are synonyms, and hence redundant, e.g. the
+terms ``full'' and ``undelimited'' refer to the same notion of
+continuation, likewise the terms ``partial'' and ``delimited'' mean
+the same thing, the notions of ``abortive'' and ``escape'' are
+interchangeable too, and ``composable'' and ``functional'' also refer
+to the same notion.
+%
+
+Thus the peloton of distinct continuation notions can be pruned to
+``undelimited'', ``delimited'', ``abortive'', and ``composable''.
+%
+The first two notions concern the introduction of continuations, that
+is how continuations are captured. Dually, the latter two notions
+concern the elimination of continuations, that is how continuations
+interact with the enclosing context.
+%
+Consequently, it is not meaningful to contrast, say, ``undelimited''
+with ``abortive'' continuations, because they are orthogonal notions.
+%
+A common confusion in the literature is to conflate ``undelimited''
+continuations with ``abortive'' continuations.
+% Similarly, often times ``composable'' is taken to imply ``delimited''.
+However, it is perfectly possible to conceive of a continuation that
+is undelimited but not abortive.
+%
+% An educated guess as to why this confusion occurs in the literature
+% may be that it is due to the introduction
+
+To make each notion of continuation concrete I will present its
+characteristic reduction rule. To facilitate this presentation I will
+make use of an abstract control operator $\CC$ to perform an abstract
+capture of continuations, i.e. informally $C\,k.M$ is to be understood
+as a syntactic construct that captures the continuation and reifies it
+as a function which it binds to $k$ in the computation $M$. The
+precise extent of the capture will be given by the characteristic
+reduction rule. I will also make use of an abstract control delimiter
+$\Delim{-}$. The term $\Delim{M}$ encloses the computation $M$ in a
+syntactically identifiable marker. For the intent and purposes of this
+presentation enclosing a value in a delimiter is an idempotent
+operation, i.e.  $\Delim{V} \reducesto V$. I will write $\EC$ to
+denote an evaluation context~\cite{Felleisen87}.
+
+\paragraph{Undelimited continuation}
+%
+\[
+  \EC[\CC\,k.M] \reducesto \EC[M[(\lambda x.\EC[x])/k]]
+\]
+%
+\begin{derivation}
+  & 3 * (\CC\,k. 2 + k\,(k\,1))\\
+  \reducesto& \reason{captures the context $k = 3 * [~]$}\\
+  & 3 * (2 + k\,(k~1))[(\lambda x. 3 * x)/k]\\
+  =& \reason{substitution}\\
+  & 3 * (2 + (\lambda x. 3 * x)((\lambda x. 3 * x)\,1))\\
+  \reducesto& \reason{$\beta$-reduction}\\
+  & 3 * (2 + (\lambda x. 3 * x)(3 * 1))\\
+  \reducesto& \reason{$\beta$-reduction}\\
+  & 3 * (2 + (\lambda x. 3 * x)\,3)\\
+  \reducesto^4& \reason{$\beta$-reductions}\\
+  & 33
+\end{derivation}
+
+\paragraph{Delimited continuation}
+%
+\[
+  \Delim{\EC[\CC\,k.M]} \reducesto \Delim{M[(\lambda x.\Delim{\EC[x]})/k]}
+\]
+%
+\[
+  \Delim{\EC[\CC\,k.M]} \reducesto M[(\lambda x.\Delim{\EC[x]})/k]
+\]
+
+\paragraph{Abortive continuation} An abortive continuation discards the current context.Like delimited continuations, an
+abortive continuation is accompanied by a delimiter. The
+characteristic property of an abortive continuation is that it
+discards its invocation context up to its enclosing delimiter.
+%
+\[
+  \EC[k\,V] \reducesto V, \quad \text{where } k = (\lambda x. \keyw{abort}\;x). 
+\]
+%
+Consequently, composing an abortive continuation with itself is
+meaningless, e.g. in $k (k\,V)$ the innermost application erases the
+outermost application.
+
+\paragraph{Composable continuation} The defining characteristic of a
+composable continuation is that it composes the captured context with
+current context, i.e.
+%
+\[
+  \EC[k\,V] \reducesto \EC[\EC'[V]], \quad \text{where } k = (\lambda x. \EC'[x])
+\]
+
+Escape continuations, undelimited continuations, delimited
+continuations, composable continuations.
+
+Downward and upward use of continuations.
+
+\section{First-Class control operators}
+Describe how effect handlers fit amongst shift/reset, prompt/control,
+callcc, J, catchcont, etc.
+
+\subsection{Abortive operators}
+
+\subsection{Undelimited operators}
+
+\subsection{Delimited operators}
 Delimited control: Control delimiters form the basis for delimited
 control. \citeauthor{Felleisen88} introduced control delimiters in
 1988, although allusions to control delimiters were made a year
@@ -523,21 +666,6 @@ shift/reset~\cite{DanvyF89,DanvyF90}, splitter~\cite{QueinnecS91},
 fcontrol~\cite{Sitaram93}, catchcont~\cite{LongleyW08}, effect
 handlers~\cite{PlotkinP09}.
 
-
-\section{Notions of continuations}
-
-Escape continuations, undelimited continuations, delimited
-continuations, composable continuations.
-
-\section{First-Class control operators}
-Describe how effect handlers fit amongst shift/reset, prompt/control,
-callcc, J, catchcont, etc.
-
-\subsection{Escape operators}
-
-\subsection{Undelimited operators}
-
-\subsection{Delimited operators}
 Comparison of various delimited control
 operators~\cite{Shan04}. Simulation of delimited control using
 undelimited control~\cite{Filinski94}
@@ -550,7 +678,8 @@ Backtracking: Amb~\cite{McCarthy63}.
 Coroutines~\cite{DahlDH72} as introduced by Simula
 67~\cite{DahlMN68}. The notion of coroutines was coined by Melvin
 Conway, who used coroutines as a code idiom in assembly
-programs~\cite{Knuth97}.
+programs~\cite{Knuth97}. Canonical reference for implementing
+coroutines with call/cc~\cite{HaynesFW86}.
 
 \section{Implementation strategies}
 Continuation marks. CPS. Stack inspection.
@@ -7202,16 +7331,16 @@ If $\typc{}{M : A}{E}$ and $M \reducesto^+ N \not\reducesto$, then $M
 
 
 \part{Expressiveness}
-\chapter{Computability, complexity, and expressivness}
+% \chapter{Computability, complexity, and expressivness}
-\label{ch:expressiveness}
+% \label{ch:expressiveness}
-\section{Notions of expressiveness}
+% \section{Notions of expressiveness}
-Felleisen's macro-expressiveness, Longley's type-respecting
+% Felleisen's macro-expressiveness, Longley's type-respecting
-expressiveness, Kammar's typability-preserving expressiveness.
+% expressiveness, Kammar's typability-preserving expressiveness.
 
-\section{Interdefinability of deep and shallow Handlers}
+% \section{Interdefinability of deep and shallow Handlers}
-\section{Encoding parameterised handlers}
+% \section{Encoding parameterised handlers}
 
-\chapter{The asymptotic power of control}
+\chapter{Asymptotic speedup with first-class control}
 \label{ch:handlers-efficiency}
 Describe the methodology\dots
 \section{Generic search}
@@ -7229,7 +7358,7 @@ Describe the methodology\dots
 \subsection{No shortcuts}
 \subsection{No sharing}
 
-\chapter{Robustness of the asymptotic power of control}
+\chapter{Speeding up programs in ML-like programming languages}
 \section{Mutable state}
 \section{Exception handling}
 \section{Effect system}