WIP

thesis.bib

@@ -27,7 +27,7 @@
                Tom Kelly and
                Sadiq Jaffer and
                Anil Madhavapeddy},
-  title     = {Retrofitting Effect Handlers onto OCaml},
+  title     = {Retrofitting Effect Handlers onto {OCaml}},
   journal   = {CoRR},
   volume    = {abs/2104.00250},
   year      = {2021}
@@ -37,14 +37,14 @@
   title = {Effective Concurrency through Algebraic Effects},
   author = {Stephen Dolan and Leo White and {KC} Sivaramakrishnan and Jeremy Yallop and Anil Madhavapeddy},
   year = 2015,
-  howpublished = {OCaml Workshop}
+  howpublished = {{OCaml} Workshop}
 }
 
 @misc{DolanWM14,
   title = {Multicore {OCaml}},
   author = {Stephen Dolan and Leo White and Anil Madhavapeddy},
   year  = {2014},
-  howpublished = {OCaml Workshop}
+  howpublished = {{OCaml} Workshop}
 }
 
 @inproceedings{DolanEHMSW17,
@@ -67,7 +67,7 @@
 # Delimited control in OCaml
 @article{Kiselyov12,
   author    = {Oleg Kiselyov},
-  title     = {Delimited control in OCaml, abstractly and concretely},
+  title     = {Delimited control in {OCaml}, abstractly and concretely},
   journal   = {Theor. Comput. Sci.},
   volume    = {435},
   pages     = {56--76},
@@ -357,7 +357,7 @@
 @inproceedings{XieL20,
   author    = {Ningning Xie and
                Daan Leijen},
-  title     = {Effect handlers in Haskell, evidently},
+  title     = {Effect handlers in {Haskell}, evidently},
   booktitle = {Haskell@ICFP},
   pages     = {95--108},
   publisher = {{ACM}},
@@ -835,6 +835,16 @@
   year      = {1995}
 }
 
+@article{Sabry98,
+  author    = {Amr Sabry},
+  title     = {What is a Purely Functional Language?},
+  journal   = {J. Funct. Program.},
+  volume    = {8},
+  number    = {1},
+  pages     = {1--22},
+  year      = {1998}
+}
+
 @article{Swierstra08,
   author    = {Wouter Swierstra},
   title     = {Data types {\`{a}} la carte},
@@ -3510,4 +3520,15 @@
   title     = {Abstraction for web programming},
   school    = {The University of Edinburgh, {UK}},
   year      = {2010}
+}
+
+# Functional programming
+@article{Hughes89,
+  author    = {John Hughes},
+  title     = {Why Functional Programming Matters},
+  journal   = {Comput. J.},
+  volume    = {32},
+  number    = {2},
+  pages     = {98--107},
+  year      = {1989}
 }

thesis.tex

@@ -253,7 +253,7 @@
   fortunate to have been supervised by him.
   %
   Secondly, I want to extend my gratitude to John Longley, who has
-  been an admirable second supervisor and who has stimulated my
+  been an excellent second supervisor and who has stimulated my
   mathematical curiosity.
   %
   Thirdly, I want to thank my academic brother Simon Fowler. You have
@@ -277,32 +277,43 @@
   Thanks to James McKinna for always asking intellectually
   interesting, and at times challenging, questions. I have appreciate
   our many conversations even though I spent days, weeks, sometimes
-  months, and in extreme cases years to think about answers to your
+  months, and in some instances years to think about answers to your
-  questions. Also thanks to Brian Campbell and J. Garrett Morris for
+  questions. On the topic of intellectually stimulating conversations,
-  putting up with all the supervision meetings that I had with Sam in
+  I also want to thank Gordon Plotkin for our intriguing impromptu
-  their shared office 5.28.
+  conversations in the level 4 and 5 pantries of Informatics
+  Forum. Thanks to Brian Campbell and J. Garrett Morris for putting up
+  with the supervision meetings that I had with Sam in their shared
+  office 5.28.
 
   Speaking of offices, I also want to thank my peers from my own
   office 5.21 for stimulating my general interest in computer science
   and mathematics beyond programming languages. Also, thanks to my CDT
-  cohort, I want to particularly emphasise my gratitude to Amna
+  cohort, I want to particularly emphasise my gratitude towards Amna
   Shahab, who has been a truly valuable friend.
 
+  Thanks to Ohad Kammar for being a good friend, taking a genuine
+  interest in my work, making it fun to attend virtual conferences,
+  and for agreeing to be the internal examiner for my dissertation. As
+  for external examiners, I am truly humbled and thankful for Andrew
+  Kennedy and Edwin Brady for agreeing to examine my dissertation.
+
   Throughout my studies I have received funding from the
   \href{https://www.ed.ac.uk/informatics}{School of Informatics} at
   The University of Edinburgh, as well as an
   \href{https://www.epsrc.ac.uk/}{EPSRC} grant
   \href{http://pervasiveparallelism.inf.ed.ac.uk}{EP/L01503X/1} (EPSRC
   Centre for Doctoral Training in Pervasive Parallelism), and by ERC
-  Consolidator Grant Skye (grant number 682315).
+  Consolidator Grant Skye (grant number 682315). I finished this
+  dissertation whilst being employed by the UKRI Future Leaders
+  Fellowship ``Effect Handler Oriented Programming'' (reference number
+  MR/T043830/1).
 
   List of people to thank
   \begin{itemize}
     \item Andreas Rossberg
     \item Jeremy Yallop
     \item Paul Piho
-    \item Gordon Plotkin
+    \item Larisa Stoltzfus
-    \item Ohad Kammar
   \end{itemize}
 \end{acknowledgements}
 
@@ -359,75 +370,132 @@
 %%
 \chapter{Introduction}
 \label{ch:introduction}
-Control is a pervasive phenomenon in virtually every programming
-language.  A programming language typically features a variety of
-control constructs, which let the programmer manipulate the control
-flow of programs in interesting ways. The most well-known control
-construct may well be $\If\;V\;\Then\;M\;\Else\;N$, which
-conditionally selects between two possible \emph{continuations} $M$
-and $N$ depending on whether the condition $V$ is $\True$ or $\False$.
 %
-The $\If$ construct offers no means for programmatic manipulation of
+Functional programmers tend to view functions as impenetrable black
-either continuation.
+boxes, whose outputs are determined entirely by their
+inputs~\cite{Hughes89}. This is a compelling view which admits a
+canonical mathematical model of
+computation~\cite{Church32,Church41}.
 %
-More intriguing forms of control exist, which enable the programmer to
+Alas, this view does not capture the reality of practical programs,
-manipulate and reify continuations as first-class data objects. This
+which must interact with their environment (i.e. operating system) to
-kind of control is known as \emph{first-class control}.
+facilitate file I/O\dots
+% Alas, this view does not capture the reality of practical programs, which
+% may use a variety of observable computational effects such as
+% exceptions, state, concurrency, interactive input/output, and so
+% forth.
+% %
+% Instead a view of function as 
 
-The idea of first-class control is old. It was conceived already
+% Alas, this view does not capture
-during the design of the programming language
+% the reality of practical programs. In practice a function may perform
-Algol~\cite{BackusBGKMPRSVWWW60} (one of the early high-level
+% effectful operations such as throwing an exception, referencing
-programming languages along with Fortran~\cite{BackusBBGHHNSSS57} and
+% memory, forking a thread, whose interactions with the function's
-Lisp~\cite{McCarthy60}) when \citet{Landin98} sought to model
+% ambient environment are observable~\cite{CartwrightF92}.
-unrestricted goto-style jumps using an extended $\lambda$-calculus.
 %
-Since then a wide variety of first-class control operators have
+% Practical programs are inherently effectful as they interact with
-appeared. We can coarsely categorise them into two groups:
+% their environment (i.e. operating system) during the extent of their
-\emph{undelimited} and \emph{delimited} (in
+% evaluation.
-Chapter~\ref{ch:continuations} we will perform a finer analysis of
-first-class control). Undelimited control operators are global
-phenomena that let programmers capture the entire control state of
-their programs, whereas delimited control operators are local
-phenomena that provide programmers with fine-grain control over which
-parts of the control state to capture.
-%
-Thus there are good reasons for preferring delimited control over
-undelimited control for practical programming.
-%
-% The most (in)famous control operator
-% \emph{call-with-current-continuation} appeared later during a revision
-% of the programming language Scheme~\cite{AbelsonHAKBOBPCRFRHSHW85}.
-%
-
-Nevertheless, the ability to manipulate continuations programmatically
-is incredibly powerful as it enables programmers to perform non-local
-transfers of control on the demand. This sort of power makes it
-possible to implement a wealth of control idioms such as
-coroutines~\cite{MouraI09}, generators/iterators~\cite{ShawWL77},
-async/await~\cite{SymePL11} as user-definable
-libraries~\cite{FriedmanHK84,FriedmanH85,Leijen17a,Leijen17,Pretnar15}. The
-phenomenon of non-local transfer of control is known as a
-\emph{control effect}. It turns out to be `the universal effect' in
-the sense that it can simulate every other computational effect
-(consult \citet{Filinski96} for a precise characterisation of what it
-means to simulate an effect). More concretely, this means a
-programming language equipped with first-class control is capable of
-implementing effects such as exceptions, mutable state, transactional
-memory, nondeterminism, concurrency, interactive input/output, stream
-redirection, internally.
-%
-
-A whole programming paradigm known as \emph{effectful programming} is
-built around the idea of simulating computational effects using
-control effects.
-
-In this dissertation I also advocate a new programming paradigm, which
-I dub \emph{effect handler oriented programming}.
 
 %
-\dhil{This dissertation is about the operational foundations for
+% Practical programming is inherently effectfulPractical programming involves programming with \emph{computational
-  programming and implementing effect handlers, a particularly modular
+%   effects}, or simply effects.
-  and extensible programming abstraction for effectful programming}
+
+Functional programming offers two distinct, but related, approaches to
+effectful programming, which \citet{Filinski96} succinctly
+characterises as \emph{effects as data} and \emph{effects as
+  behaviour}. The former uses monads to encapsulate
+effects~\cite{Moggi91,Wadler92} which is compelling because it extends
+the black box view to effectful functions, though, at the expense of a
+change of programming style~\cite{JonesW93}. The latter retains the
+usual direct style of programming by way of \emph{first-class
+  control}, which is a powerful facility that can simulate any
+effect~\cite{Filinski94,Filinski96}. First-class control enables the
+programmer to manipulate and reify the control state as a first-class
+data object known as a continuation~\cite{FriedmanHK84}. First-class
+control has the ability pry open function boundaries, which fractures
+the black box view of computation. This ability can significantly
+improve the computational expressiveness and efficiency of programming
+languages~\cite{LongleyN15,HillerstromLL20}.
+
+effect handlers, a recent innovation,
+
+%\citet{Sabry98}
+% Virtually every useful program performs some computational effects
+% such as exceptions, state, concurrency, nondeterminism, interactive
+% input and output during its execution.
+%
+%\citet{Filinski96} \emph{effects as data} and \emph{effects as behaviour}
+
+% Control is a pervasive phenomenon in virtually every programming
+% language.  A programming language typically features a variety of
+% control constructs, which let the programmer manipulate the control
+% flow of programs in interesting ways. The most well-known control
+% construct may well be $\If\;V\;\Then\;M\;\Else\;N$, which
+% conditionally selects between two possible \emph{continuations} $M$
+% and $N$ depending on whether the condition $V$ is $\True$ or $\False$.
+% %
+% The $\If$ construct offers no means for programmatic manipulation of
+% either continuation.
+% %
+% More intriguing forms of control exist, which enable the programmer to
+% manipulate and reify continuations as first-class data objects. This
+% kind of control is known as \emph{first-class control}.
+
+% The idea of first-class control is old. It was conceived already
+% during the design of the programming language
+% Algol~\cite{BackusBGKMPRSVWWW60} (one of the early high-level
+% programming languages along with Fortran~\cite{BackusBBGHHNSSS57} and
+% Lisp~\cite{McCarthy60}) when \citet{Landin98} sought to model
+% unrestricted goto-style jumps using an extended $\lambda$-calculus.
+% %
+% Since then a wide variety of first-class control operators have
+% appeared. We can coarsely categorise them into two groups:
+% \emph{undelimited} and \emph{delimited} (in
+% Chapter~\ref{ch:continuations} we will perform a finer analysis of
+% first-class control). Undelimited control operators are global
+% phenomena that let programmers capture the entire control state of
+% their programs, whereas delimited control operators are local
+% phenomena that provide programmers with fine-grain control over which
+% parts of the control state to capture.
+% %
+% Thus there are good reasons for preferring delimited control over
+% undelimited control for practical programming.
+% %
+% % The most (in)famous control operator
+% % \emph{call-with-current-continuation} appeared later during a revision
+% % of the programming language Scheme~\cite{AbelsonHAKBOBPCRFRHSHW85}.
+% %
+
+% Nevertheless, the ability to manipulate continuations programmatically
+% is incredibly powerful as it enables programmers to perform non-local
+% transfers of control on the demand. This sort of power makes it
+% possible to implement a wealth of control idioms such as
+% coroutines~\cite{MouraI09}, generators/iterators~\cite{ShawWL77},
+% async/await~\cite{SymePL11} as user-definable
+% libraries~\cite{FriedmanHK84,FriedmanH85,Leijen17a,Leijen17,Pretnar15}. The
+% phenomenon of non-local transfer of control is known as a
+% \emph{control effect}. It turns out to be `the universal effect' in
+% the sense that it can simulate every other computational effect
+% (consult \citet{Filinski96} for a precise characterisation of what it
+% means to simulate an effect). More concretely, this means a
+% programming language equipped with first-class control is capable of
+% implementing effects such as exceptions, mutable state, transactional
+% memory, nondeterminism, concurrency, interactive input/output, stream
+% redirection, internally.
+% %
+
+% A whole programming paradigm known as \emph{effectful programming} is
+% built around the idea of simulating computational effects using
+% control effects.
+
+% In this dissertation I also advocate a new programming paradigm, which
+% I dub \emph{effect handler oriented programming}.
+
+% %
+% \dhil{This dissertation is about the operational foundations for
+%   programming and implementing effect handlers, a particularly modular
+%   and extensible programming abstraction for effectful programming}
 
 % Control is an ample ingredient of virtually every programming
 % language. A programming language typically feature a variety of
@@ -630,7 +698,8 @@ The body of the function first retrieves the current value of the
 state cell and binds it to $st$. Subsequently, it destructively
 increments the value of the state cell. Finally, it applies the
 predicate $\even : \Int \to \Bool$ to the original state value to test
-whether its parity is even.
+whether its parity is even (remark: this example function is a slight
+variation of an example by \citet{Gibbons12}).
 %
 We can run this computation as a subcomputation in the context of
 global state cell $st$.
@@ -1668,7 +1737,8 @@ the effect signature $E$.
 This typing discipline fits nicely with the effect handlers-style of
 programming. The $\Do$ construct provides a mechanism for injecting an
 operation into the effect signature, whilst the $\Handle$ construct
-provides a way to eliminate an effect operation from the signature.
+provides a way to eliminate an effect operation from the
+signature~\cite{BauerP13,HillerstromL16}.
 %
 If we instantiate $A = \UnitType$, $B = \Bool$, and $E = \Sigma$, then
 we obtain a type-and-effect signature for the handler version of
@@ -4461,7 +4531,7 @@ 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}
+\part{Programming}
 \label{p:design}
 
 \chapter{An ML-flavoured programming language based on rows}