dhil/phd-dissertation
1
0
Fork 0
mirror of https://github.com/dhil/phd-dissertation synced 2026-03-13 19:18:25 +00:00
Code Issues Releases Wiki Activity

Fix typos in introduction

Browse Source
This commit is contained in:
Daniel Hillerström
2021-05-29 00:28:38 +01:00
parent ee92e3b483
commit 9c2da2c378
1 changed files with 95 additions and 54 deletions
Download Patch File Download Diff File Expand all files Collapse all files

149
thesis.tex
View File

@@ -611,16 +611,33 @@ efficiency.
% expressiveness. % expressiveness.
\section{Why first-class control matters} \section{Why first-class control matters}
First things first, let us settle on the meaning of the qualifier
`first-class'. A programming language entity (or citizen) is regarded
as being first-class if it can be used on an equal footing with other
entities.
%
A familiar example is functions as first-class values. A first-class
function may be treated like any other primitive value, i.e. passed as
an argument to other functions, returned from functions, stored in
data structures, or let-bound.
First-class control makes the control state of the program available
as a first-class value known as a continuation object at any point
during evaluation~\cite{FriedmanHK84}. This object comes equipped with
at least one operation for restoring the control state. As such the
control flow of the program becomes a first-class entity that the
programmer may manipulate to implement interesting control phenomena.
From the perspective of programmers first-class control is a valuable From the perspective of programmers first-class control is a valuable
programming feature because it enables them to implement their own programming feature because it enables them to implement their own
control idioms as if they were native to the programming language (in control idioms, such as async/await~\cite{SymePL11}, as if they were
fact this is the very definition of first-class control). More native to the programming language. More important, with first-class
important, with first-class control programmer-defined control idioms control programmer-defined control idioms are local phenomena which
are local phenomena which can be encapsulated in a library such that can be encapsulated in a library such that the rest of the program
the rest of the program does not need to be made aware of their does not need to be made aware of their existence. Conversely, without
existence. Conversely, without first-class control some control idioms first-class control some control idioms can only be implemented using
can only be implemented using global program restructuring techniques global program restructuring techniques such as continuation passing
such as continuation passing style. style.
From the perspective of compiler engineers first-class control is From the perspective of compiler engineers first-class control is
valuable because it unifies several control-related constructs under valuable because it unifies several control-related constructs under
@@ -678,9 +695,12 @@ intended purpose.
In contrast, effect handlers provide a structured form of delimited In contrast, effect handlers provide a structured form of delimited
control, where programmers can give distinct names to control reifying control, where programmers can give distinct names to control reifying
operations and separate the from their handling. operations and separate them from their handling. Throughout this
dissertation we will see numerous examples of how effect handlers
makes programming with delimited structured (c.f. the following
section, Chapter~\ref{ch:continuations}, and
Chapter~\ref{ch:unary-handlers}).
% %
\dhil{Maybe expand this a bit more to really sell it}
\section{State of effectful programming} \section{State of effectful programming}
\label{sec:state-of-effprog} \label{sec:state-of-effprog}
@@ -690,7 +710,8 @@ boxes, whose outputs are determined entirely by their
inputs~\cite{Hughes89,Howard80}. This is a compelling view which inputs~\cite{Hughes89,Howard80}. This is a compelling view which
admits a canonical mathematical model of admits a canonical mathematical model of
computation~\cite{Church32,Church41}. Alas, this view does not capture computation~\cite{Church32,Church41}. Alas, this view does not capture
the reality of practical programs, which interact their environment. the reality of practical programs, which interact with their
environment.
% %
Functional programming prominently features two distinct, but related, Functional programming prominently features two distinct, but related,
approaches to effectful programming, which \citet{Filinski96} approaches to effectful programming, which \citet{Filinski96}
@@ -705,11 +726,11 @@ style~\cite{JonesW93}. The latter retains the usual direct style of
programming either by hard-wiring the semantics of the effects into programming either by hard-wiring the semantics of the effects into
the language or by more flexible means via first-class control. the language or by more flexible means via first-class control.
In this section I will provide a brief programming perspective on In this section I will provide a brief perspective on different
different approaches to programming with effects along with an approaches to programming with effects along with an informal
informal introduction to the related concepts. We will look at each introduction to the related concepts. We will look at each approach
approach through the lens of global mutable state --- which is the through the lens of global mutable state --- the ``hello world'' of
``hello world'' example of effectful programming. effectful programming.
% how % how
% effectful programming has evolved as well as providing an informal % effectful programming has evolved as well as providing an informal
@@ -730,9 +751,9 @@ approach through the lens of global mutable state --- which is the
% %
We can realise stateful behaviour by either using language-supported We can realise stateful behaviour by either using language-supported
state primitives, globally structure our program to follow a certain state primitives, globally structure our program to follow a certain
style, or use first-class control in the form of delimited control to style, or using first-class control in the form of delimited control
simulate state. We do not consider undelimited control, because it is to simulate state. We do not consider undelimited control, because it
insufficient to express mutable state~\cite{FriedmanS00}. is insufficient to express mutable state~\cite{FriedmanS00}.
% Programming in its infancy was effectful as the idea of first-class % Programming in its infancy was effectful as the idea of first-class
% control was conceived already during the design of the programming % control was conceived already during the design of the programming
% language Algol~\cite{BackusBGKMPRSVWWW60} -- one of the early % language Algol~\cite{BackusBGKMPRSVWWW60} -- one of the early
@@ -777,13 +798,14 @@ It is common to find mutable state builtin into the semantics of
mainstream programming languages. However, different languages vary in mainstream programming languages. However, different languages vary in
their approach to mutable state. For instance, state mutation their approach to mutable state. For instance, state mutation
underpins the foundations of imperative programming languages underpins the foundations of imperative programming languages
belonging to the C family of languages. They do typically not belonging to the C family of languages. They typically do not
distinguish between mutable and immutable values at the level of distinguish between mutable and immutable values at the level of
types. Contrary, programming languages belonging to the ML family of types. On the contrary, programming languages belonging to the ML
languages use types to differentiate between mutable and immutable family of languages use types to differentiate between mutable and
values. They reflect mutable values in types by using a special unary immutable values. They reflect mutable values in types by using a
type constructor $\PCFRef^{\Type \to \Type}$. Furthermore, ML special unary type constructor $\PCFRef^{\Type \to
languages equip the $\PCFRef$ constructor with three operations. \Type}$. Furthermore, ML languages equip the $\PCFRef$ constructor
with three operations.
% %
\[ \[
\refv : S \to \PCFRef~S \qquad\quad \refv : S \to \PCFRef~S \qquad\quad
@@ -815,7 +837,7 @@ The body of the function first retrieves the current value of the
state cell and binds it to $st$. Subsequently, it destructively state cell and binds it to $st$. Subsequently, it destructively
increments the value of the state cell. Finally, it applies the increments the value of the state cell. Finally, it applies the
predicate $\even : \Int \to \Bool$ to the original state value to test predicate $\even : \Int \to \Bool$ to the original state value to test
whether its parity is even (remark: this example function is a slight whether its parity is even (this example function is a slight
variation of an example by \citet{Gibbons12}). variation of an example by \citet{Gibbons12}).
% %
We can run this computation as a subcomputation in the context of We can run this computation as a subcomputation in the context of
@@ -913,8 +935,9 @@ represents the continuation of the invocation of $\shift$ (up to the
innermost reset); it gets passed as a function to the argument of innermost reset); it gets passed as a function to the argument of
$\shift$. $\shift$.
Both primitives are defined over some (globally) fixed result type We define both primitives over some fixed return type $R$ (an actual
$R$. practical implementation would use polymorphism to make them more
flexible).
% %
By instantiating $R = S \to A \times S$, where $S$ is the type of By instantiating $R = S \to A \times S$, where $S$ is the type of
state and $A$ is the type of return values, then we can use shift and state and $A$ is the type of return values, then we can use shift and
@@ -970,11 +993,12 @@ Modulo naming of operations, this version is similar to the version
that uses builtin state. The type signature of the function is even that uses builtin state. The type signature of the function is even
the same. the same.
% %
Before we can apply this function we must first a state initialiser. Before we can apply this function we must first implement a state
initialiser.
% %
\[ \[
\bl \bl
\runState : (\UnitType \to R) \to S \to R \times S\\ \runState : (\UnitType \to A) \to S \to A \times S\\
\runState~m~st_0 \defas \reset{\lambda\Unit.\Let\;x \revto m\,\Unit\;\In\;\lambda st. \Record{x;st}}\,st_0 \runState~m~st_0 \defas \reset{\lambda\Unit.\Let\;x \revto m\,\Unit\;\In\;\lambda st. \Record{x;st}}\,st_0
\bl \bl
\el \el
@@ -994,7 +1018,7 @@ the state-accepting function returned by the reset instance. The
application of the reset instance to $st_0$ effectively causes application of the reset instance to $st_0$ effectively causes
evaluation of each function in this chain to start. evaluation of each function in this chain to start.
After instantiating $R = \Bool$ and $S = \Int$ we can use the After instantiating $A = \Bool$ and $S = \Int$ we can use the
$\runState$ function to apply the $\incrEven$ function. $\runState$ function to apply the $\incrEven$ function.
% %
\[ \[
@@ -1056,8 +1080,8 @@ Haskell~\cite{JonesABBBFHHHHJJLMPRRW99}.
\el \el
\] \]
% %
Interactions between $\Return$ and $\bind$ are governed by the Interactions between $\Return$ and $\bind$ are governed by the monad
so-called `monad laws'. laws.
\begin{reductions} \begin{reductions}
\slab{Left\textrm{ }identity} & \Return\;x \bind k &=& k~x\\ \slab{Left\textrm{ }identity} & \Return\;x \bind k &=& k~x\\
\slab{Right\textrm{ }identity} & m \bind \Return &=& m\\ \slab{Right\textrm{ }identity} & m \bind \Return &=& m\\
@@ -1397,7 +1421,7 @@ operation is another computation tree node.
% %
\[ \[
\bl \bl
\ba{@{~}l@{\qquad}@{~}r} \ba{@{~}l@{\,\quad}@{~}r}
\multicolumn{2}{l}{T~A \defas \Free~F~A} \smallskip\\ \multicolumn{2}{l}{T~A \defas \Free~F~A} \smallskip\\
\multirow{2}{*}{ \multirow{2}{*}{
\bl \bl
@@ -1894,10 +1918,13 @@ polymorphic $\lambda$-calculi for which I give computational
interpretations in terms of contextual operational semantics and interpretations in terms of contextual operational semantics and
realise using two foundational operational techniques: continuation realise using two foundational operational techniques: continuation
passing style and abstract machine semantics. When it comes to passing style and abstract machine semantics. When it comes to
expressivity studies there are multiple complementary notions of expressiveness there are multiple possible dimensions to investigate
expressiveness available in the literature; in this dissertation I and multiple different notions of expressivity available. I focus on
work with typed macro-expressiveness and type-respecting two questions: `are deep, shallow, and parameterised handlers
expressiveness notions. interdefinable?' which I investigate via a syntactic notion of
expressiveness due \citet{Felleisen91}. And, `does effect handlers
admit any essential computational efficiency?' which I investigate
using a semantic notion of expressiveness due to \citet{LongleyN15}.
\subsection{Scope extrusion} \subsection{Scope extrusion}
The literature on effect handlers is rich, and my dissertation is but The literature on effect handlers is rich, and my dissertation is but
@@ -1941,8 +1968,11 @@ theory of scoped effect operations, whilst \citet{BiernackiPPS20}
study them in conjunction with ordinary handlers from a programming study them in conjunction with ordinary handlers from a programming
perspective. perspective.
% \citet{WuSH14} study scoped effects, which are effects whose payloads % \citet{WuSH14} study scoped effects, which are effects whose
% are effectful computations % payloads are effectful computations. Scoped effects are
% non-algebraic, Thinking in terms of computation trees, a scoped
% effect is not an internal node of some computation tree, rather, it
% is itself a whole computation tree.
% Effect handlers were conceived in the realm of category theory to give % Effect handlers were conceived in the realm of category theory to give
% an algebraic treatment of exception handling~\cite{PlotkinP09}. They % an algebraic treatment of exception handling~\cite{PlotkinP09}. They
@@ -1963,9 +1993,9 @@ handlers extension to Prolog; and \citet{Leijen17b} has an imperative
take on effect handlers in C. take on effect handlers in C.
\section{Contributions} \section{Contributions}
The key contributions of this dissertation are scattered across the The key contributions of this dissertation are spread across the four
four main parts. The following listing summarises the contributions of main parts. The following listing summarises the contributions of each
each part. part.
\paragraph{Background} \paragraph{Background}
\begin{itemize} \begin{itemize}
\item A comprehensive operational characterisation of various \item A comprehensive operational characterisation of various
@@ -2010,35 +2040,40 @@ The following is a summary of the chapters belonging to each part of
this dissertation. this dissertation.
\paragraph{Background} \paragraph{Background}
Chapter~\ref{ch:maths-prep} defines some basic mathematical \begin{itemize}
\item Chapter~\ref{ch:maths-prep} defines some basic mathematical
notation and constructions that are they pervasively throughout this notation and constructions that are they pervasively throughout this
dissertation. dissertation.
Chapter~\ref{ch:continuations} presents a literature survey of \item Chapter~\ref{ch:continuations} presents a literature survey of
continuations and first-class control. I classify continuations continuations and first-class control. I classify continuations
according to their operational behaviour and provide an overview of according to their operational behaviour and provide an overview of
the various first-class sequential control operators that appear in the various first-class sequential control operators that appear in
the literature. The application spectrum of continuations is discussed the literature. The application spectrum of continuations is discussed
as well as implementation strategies for first-class control. as well as implementation strategies for first-class control.
\end{itemize}
\paragraph{Programming} \paragraph{Programming}
Chapter~\ref{ch:base-language} introduces a polymorphic fine-grain \begin{itemize}
\item Chapter~\ref{ch:base-language} introduces a polymorphic fine-grain
call-by-value core calculus, $\BCalc$, which makes key use of call-by-value core calculus, $\BCalc$, which makes key use of
\citeauthor{Remy93}-style row polymorphism to implement polymorphic \citeauthor{Remy93}-style row polymorphism to implement polymorphic
variants, structural records, and a structural effect system. The variants, structural records, and a structural effect system. The
calculus distils the essence of the core of the Links programming calculus distils the essence of the core of the Links programming
language. language.
Chapter~\ref{ch:unary-handlers} presents three extensions of $\BCalc$, \item Chapter~\ref{ch:unary-handlers} presents three extensions of $\BCalc$,
which are $\HCalc$ that adds deep handlers, $\SCalc$ that adds shallow which are $\HCalc$ that adds deep handlers, $\SCalc$ that adds shallow
handlers, and $\HPCalc$ that adds parameterised handlers. The chapter handlers, and $\HPCalc$ that adds parameterised handlers. The chapter
also contains a running case study that demonstrates effect handler also contains a running case study that demonstrates effect handler
oriented programming in practice by implementing a small operating oriented programming in practice by implementing a small operating
system dubbed \OSname{} based on \citeauthor{RitchieT74}'s original system dubbed \OSname{} based on \citeauthor{RitchieT74}'s original
\UNIX{}. \UNIX{}.
\end{itemize}
\paragraph{Implementation} \paragraph{Implementation}
Chapter~\ref{ch:cps} develops a higher-order continuation passing \begin{itemize}
\item Chapter~\ref{ch:cps} develops a higher-order continuation passing
style translation for effect handlers through a series of step-wise style translation for effect handlers through a series of step-wise
refinements of an initial standard continuation passing style refinements of an initial standard continuation passing style
translation for $\BCalc$. Each refinement slightly modifies the notion translation for $\BCalc$. Each refinement slightly modifies the notion
@@ -2047,18 +2082,20 @@ ultimately leads to the key invention of generalised continuation,
which is used to give a continuation passing style semantics to deep, which is used to give a continuation passing style semantics to deep,
shallow, and parameterised handlers. shallow, and parameterised handlers.
Chapter~\ref{ch:abstract-machine} demonstrates an application of \item Chapter~\ref{ch:abstract-machine} demonstrates an application of
generalised continuations to abstract machine as we plug generalised generalised continuations to abstract machine as we plug generalised
continuations into \citeauthor{FelleisenF86}'s CEK machine to obtain continuations into \citeauthor{FelleisenF86}'s CEK machine to obtain
an adequate abstract runtime with simultaneous support for deep, an adequate abstract runtime with simultaneous support for deep,
shallow, and parameterised handlers. shallow, and parameterised handlers.
\end{itemize}
\paragraph{Expressiveness} \paragraph{Expressiveness}
Chapter~\ref{ch:deep-vs-shallow} shows that deep, shallow, and \begin{itemize}
\item Chapter~\ref{ch:deep-vs-shallow} shows that deep, shallow, and
parameterised notions of handlers can simulate one another up to parameterised notions of handlers can simulate one another up to
specific notions of administrative reduction. specific notions of administrative reduction.
Chapter~\ref{ch:handlers-efficiency} studies the fundamental efficiency of effect \item Chapter~\ref{ch:handlers-efficiency} studies the fundamental efficiency of effect
handlers. In this chapter, we show that effect handlers enable an handlers. In this chapter, we show that effect handlers enable an
asymptotic improvement in runtime complexity for a certain class of asymptotic improvement in runtime complexity for a certain class of
functions. Specifically, we consider the \emph{generic count} problem functions. Specifically, we consider the \emph{generic count} problem
@@ -2068,9 +2105,12 @@ of $\BCalc$) and its extension with effect handlers $\HPCF$.
We show that $\HPCF$ admits an asymptotically more efficient We show that $\HPCF$ admits an asymptotically more efficient
implementation of generic count than any $\BPCF$ implementation. implementation of generic count than any $\BPCF$ implementation.
% %
\end{itemize}
\paragraph{Conclusions} \paragraph{Conclusions}
Chapter~\ref{ch:conclusions} concludes and discusses future work. \begin{itemize}
\item Chapter~\ref{ch:conclusions} concludes and discusses future work.
\end{itemize}
\part{Background} \part{Background}
@@ -15114,8 +15154,9 @@ $N'$ such that $N' \approxa \sdtrans{N}$ and $M' \reducesto^+ N'$.
% By case analysis on $\reducesto$ and induction on $\approxa$ using % By case analysis on $\reducesto$ and induction on $\approxa$ using
% Lemma~\ref{lem:sdtrans-subst} and Lemma~\ref{lem:sdtrans-admin}. % Lemma~\ref{lem:sdtrans-subst} and Lemma~\ref{lem:sdtrans-admin}.
% %
By induction on $M' \approxa \sdtrans{M}$ and side induction on By induction on $M' \approxa \sdtrans{M}$ and case analysis on
$M \reducesto N$ using Lemma~\ref{lem:sdtrans-subst} and Lemma~\ref{lem:sdtrans-admin}. $M \reducesto N$ using Lemma~\ref{lem:sdtrans-subst} and
Lemma~\ref{lem:sdtrans-admin}.
% %
The interesting case is reflexivity of $\approxa$ where The interesting case is reflexivity of $\approxa$ where
$M \reducesto N$ is an application of $\semlab{Op^\dagger}$, which $M \reducesto N$ is an application of $\semlab{Op^\dagger}$, which