From 15125f206cebf0d791168586d1fbd41aeb143b9f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Daniel=20Hillerstr=C3=B6m?= Date: Thu, 20 May 2021 17:49:38 +0100 Subject: [PATCH] Intro WIP --- thesis.bib | 14 +++++++ thesis.tex | 113 ++++++++++++++++++++++++++++++++--------------------- 2 files changed, 83 insertions(+), 44 deletions(-) diff --git a/thesis.bib b/thesis.bib index 467c2c1..54e6ce0 100644 --- a/thesis.bib +++ b/thesis.bib @@ -3281,6 +3281,20 @@ booktitle = {{TPDC}} } +# Generators / iterators +@article{ShawWL77, + author = {Mary Shaw and + William A. Wulf and + Ralph L. London}, + title = {Abstraction and Verification in Alphard: Defining and Specifying Iteration + and Generators}, + journal = {Commun. {ACM}}, + volume = {20}, + number = {8}, + pages = {553--564}, + year = {1977} +} + # Fellowship of the Ring reference @book{Tolkien54, title = {The lord of the rings: Part 1: The fellowship of the ring}, diff --git a/thesis.tex b/thesis.tex index 5ebd9b4..7f9393a 100644 --- a/thesis.tex +++ b/thesis.tex @@ -349,28 +349,54 @@ 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 + +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. Albeit, the most (in)famous first-class control -operator \emph{call-with-current-continuation} appeared later when it -was introduced by the designers of the programming language -Scheme~\cite{AbelsonHAKBOBPCRFRHSHW85}. -% -The ability to manipulate continuations programmatically is incredibly -powerful as it enables programmers to perform non-local transfers of -control on the -demand. % and it can be used to codify a wealth of control idioms. -% -\dhil{First-class control provides more intriguing forms of control, - which reifies the continuation as a first-class data object.} -% -\dhil{Control effects gives rise to a programming paradigm known as - effectful programming} +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. + % \dhil{This dissertation is about the operational foundations for programming and implementing effect handlers, a particularly modular @@ -636,9 +662,9 @@ State initialisation is simply function application. \] % Programming in state-passing style is laborious and no fun as it is -anti-modular, because effect-free higher-order functions to work with -stateful functions they too must be transformed or at the very least -be duplicated to be compatible with stateful function arguments. +anti-modular, because for effect-free higher-order functions to work +with stateful functions they too must be transformed or at the very +least be duplicated to be compatible with stateful function arguments. % Nevertheless, state-passing is an important technique as it is the secret sauce that enables us to simulate mutable state with other @@ -709,10 +735,10 @@ The body of $\getF$ applies $\shift$ to capture the current continuation, which gets supplied to the anonymous function $(\lambda k.\lambda st. k~st~st)$. The continuation parameter $k$ has type $S \to S \to A \times S$. The continuation is applied to two -instances of the current state value $st$. The instance the value -returned to the caller of $\getF$, whilst the second instance is the -state value available during the next invocation of either $\getF$ or -$\putF$. This aligns with the intuition that accessing a state cell +instances of the current state value $st$. The first instance is the +value returned to the caller of $\getF$, whilst the second instance is +the state value available during the next invocation of either $\getF$ +or $\putF$. This aligns with the intuition that accessing a state cell does not modify its contents. The implementation of $\putF$ is similar, except that the first argument to $k$ is the unit value, because the caller of $\putF$ expects a unit in return. Also, it @@ -776,10 +802,9 @@ The concept of monad has its origins in category theory and its mathematical nature is well-understood~\cite{MacLane71,Borceux94}. The emergence of monads as a programming abstraction began when \citet{Moggi89,Moggi91} proposed to use monads as the basis for -denoting computational effects in denotational semantics such as -exceptions, state, nondeterminism, interactive input and -output. \citet{Wadler92,Wadler95} popularised monadic programming by -putting \citeauthor{Moggi89}'s proposal to use in functional +denoting computational effects in denotational +semantics. \citet{Wadler92,Wadler95} popularised monadic programming +by putting \citeauthor{Moggi89}'s proposal to use in functional programming by demonstrating how monads increase the ease at which programs may be retrofitted with computational effects. % @@ -787,10 +812,10 @@ In practical programming terms, monads may be thought of as constituting a family of design patterns, where each pattern gives rise to a distinct effect with its own operations. % -The part of the appeal of monads is that they provide a structured +Part of the appeal of monads is that they provide a structured interface for programming with effects such as state, exceptions, -nondeterminism, and so forth, whilst preserving the equational style -of reasoning about pure functional +nondeterminism, interactive input and output, and so forth, whilst +preserving the equational style of reasoning about pure functional programs~\cite{GibbonsH11,Gibbons12}. % % Notably, they form the foundations for effectful programming in @@ -800,7 +825,7 @@ programs~\cite{GibbonsH11,Gibbons12}. The presentation of monads here is inspired by \citeauthor{Wadler92}'s presentation of monads for functional programming~\cite{Wadler92}, and -it should be familiar to users of +it ought to be familiar to users of Haskell~\cite{JonesABBBFHHHHJJLMPRRW99}. \begin{definition} @@ -847,8 +872,7 @@ efficient code for monadic programs. The success of monads as a programming idiom is difficult to understate as monads have given rise to several popular control-oriented programming abstractions including the asynchronous -programming idiom async/await has its origins in monadic -programming~\cite{Claessen99,LiZ07,SymePL11}. +programming idiom async/await~\cite{Claessen99,LiZ07,SymePL11}. % \subsection{Option monad} % The $\Option$ type is a unary type constructor with two data @@ -1013,14 +1037,15 @@ exists one monad to rule them all, one monad to realise them, one monad to subsume them all, and in the term language bind them. This powerful monad is the \emph{continuation monad}. -The continuation monad may be regarded as `the universal effect' as it -can simulate any other computational effect~\cite{Filinski99}. It -derives its name from its connection to continuation passing -style~\cite{Wadler92}, which is a particular style of programming -where each function is parameterised by the current continuation (we -will discuss continuation passing style in detail in -Chapter~\ref{ch:cps}). The continuation monad is powerful exactly -because each of its operations has access to the current continuation. +The continuation monad may be regarded as `the universal monad' as it +can embed any other monad, and thereby simulate any computational +effect~\cite{Filinski99}. It derives its name from its connection to +continuation passing style~\cite{Wadler92}, which is a particular +style of programming where each function is parameterised by the +current continuation (we will discuss continuation passing style in +detail in Chapter~\ref{ch:cps}). The continuation monad is powerful +exactly because each of its operations has access to the current +continuation. \begin{definition}\label{def:cont-monad} @@ -1393,7 +1418,7 @@ delimited control variant of $\incrEven$. \subsubsection{Effect tracking} \dhil{Cite \citet{GiffordL86}, \citet{LucassenG88}, \citet{TalpinJ92}, -\citet{TofteT97}, \citet{NielsonN99}.} +\citet{TofteT97}, \citet{NielsonN99}, \citet{WadlerT03}.} A benefit of using monads for effectful programming is that we get effect tracking `for free' (some might object to this statement and