diff --git a/macros.tex b/macros.tex index f4c679a..4491800 100644 --- a/macros.tex +++ b/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 diff --git a/thesis.bib b/thesis.bib index f5257b7..84a1346 100644 --- a/thesis.bib +++ b/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}, - 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} + OPTdoi = {10.2168/LMCS-9(4:23)2013} } @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 - and Chris Haynes - and Norman Adams - and Eugene Kohlbecker - and David Bartley - and Don Oxley - and Gary Brooks - and Kent Pitman - and William Clinger - and Jonathan Rees - and Dan Friedman - and Bill Rozas - and Robert Halstead - and Gerald Jey Sussman - and Chris Hanson - and Mitchell Wand}, + author = {William D. Clinger and others}, + @Comment = {Hal Abelson + @Comment and Chris Haynes + @Comment and Norman Adams + @Comment and Eugene Kohlbecker + @Comment and David Bartley + @Comment and Don Oxley + @Comment and Gary Brooks + @Comment and Kent Pitman + @Comment and William Clinger + @Comment and Jonathan Rees + @Comment and Dan Friedman + @Comment and Bill Rozas + @Comment and Robert Halstead + @Comment and Gerald Jey Sussman + @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}, - month = aug, - type = {AI Memo} + number = {AIM-848}, + month = aug } # 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 - and Jim Meyering - and Ross Paterson - and François Pinard - and Karl Berry - and Brian Youmans - and Richard Stallman}, + author = {David MacKenzie and others}, + @Comment = {David MacKenzie + @Comment and Jim Meyering + @Comment and Ross Paterson + @Comment and François Pinard + @Comment and Karl Berry + @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} } \ No newline at end of file diff --git a/thesis.tex b/thesis.tex index ac8abc0..304b53f 100644 --- a/thesis.tex +++ b/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,42 +502,170 @@ 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' -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}. - -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 -earlier by \citet{FelleisenFDM87} and in \citeauthor{Felleisen87}'s -PhD dissertation~\cite{Felleisen87}. The basic idea was teased even -earlier in \citeauthor{Talcott85}'s teased the idea of control -delimiters in her PhD dissertation~\cite{Talcott85}. +A continuation is an abstract data structure that captures the +remainder of the computation from some given point in the computation. % -Common Lisp resumable exceptions (condition system)~\cite{Steele90}, -F~\cite{FelleisenFDM87,Felleisen88}, control/prompt~\cite{SitaramF90}, -shift/reset~\cite{DanvyF89,DanvyF90}, splitter~\cite{QueinnecS91}, -fcontrol~\cite{Sitaram93}, catchcont~\cite{LongleyW08}, effect -handlers~\cite{PlotkinP09}. +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. +% 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{Escape operators} +\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 +earlier by \citet{FelleisenFDM87} and in \citeauthor{Felleisen87}'s +PhD dissertation~\cite{Felleisen87}. The basic idea was teased even +earlier in \citeauthor{Talcott85}'s teased the idea of control +delimiters in her PhD dissertation~\cite{Talcott85}. +% +Common Lisp resumable exceptions (condition system)~\cite{Steele90}, +F~\cite{FelleisenFDM87,Felleisen88}, control/prompt~\cite{SitaramF90}, +shift/reset~\cite{DanvyF89,DanvyF90}, splitter~\cite{QueinnecS91}, +fcontrol~\cite{Sitaram93}, catchcont~\cite{LongleyW08}, effect +handlers~\cite{PlotkinP09}. + 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} -\label{ch:expressiveness} -\section{Notions of expressiveness} -Felleisen's macro-expressiveness, Longley's type-respecting -expressiveness, Kammar's typability-preserving expressiveness. +% \chapter{Computability, complexity, and expressivness} +% \label{ch:expressiveness} +% \section{Notions of expressiveness} +% Felleisen's macro-expressiveness, Longley's type-respecting +% expressiveness, Kammar's typability-preserving expressiveness. -\section{Interdefinability of deep and shallow Handlers} -\section{Encoding parameterised handlers} +% \section{Interdefinability of deep and shallow 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}