From 13d76a146b48f7cec59284df17ee2aa91ccbb695 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Daniel=20Hillerstr=C3=B6m?= Date: Sun, 23 May 2021 22:42:28 +0100 Subject: [PATCH] Update state of effectful programming --- thesis.bib | 21 +++++++ thesis.tex | 170 +++++++++++++++++++++++++++++++---------------------- 2 files changed, 121 insertions(+), 70 deletions(-) diff --git a/thesis.bib b/thesis.bib index 4bd8853..7245e98 100644 --- a/thesis.bib +++ b/thesis.bib @@ -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} } \ No newline at end of file diff --git a/thesis.tex b/thesis.tex index 524350c..a9d5038 100644 --- a/thesis.tex +++ b/thesis.tex @@ -369,75 +369,104 @@ %% \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 -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} +% +Functional programmers tend to view functions as impenetrable black +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}. Alas, this view does not capture +the reality of practical programs. In practice functions may perform +effectful operations such as throwing an exception, referencing +memory, forking a thread, which may have an observable effect on the +program state~\cite{CartwrightF92}. + +Practical programming is in its nature effectful. + +Functional programming offers two dominant approaches to programming +with effects, which \citet{Filinski96} succinctly characterises as +\emph{effects as data} and \emph{effects as behaviour}. + +control effects can pry open function boundaries which have profound +implications for the computational expressiveness and efficiency of + +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 @@ -640,7 +669,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$.