From 84fe38105e3f9da027996515d00f8b7f2d48d8f8 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Daniel=20Hillerstr=C3=B6m?= Date: Thu, 13 May 2021 11:07:36 +0100 Subject: [PATCH] Contributions and outline --- thesis.tex | 92 ++++++++++++++++++++++++++++++++++++++++++++++++++++-- 1 file changed, 89 insertions(+), 3 deletions(-) diff --git a/thesis.tex b/thesis.tex index a199c88..3ce84c0 100644 --- a/thesis.tex +++ b/thesis.tex @@ -372,6 +372,9 @@ the literature as they have been around since the dawn of programming~\cite{DahlMN68,DahlDH72,Knuth97,MouraI09}. Nevertheless coroutines frequently reappear in the literature in various guises. +The common denominator for the aforementioned control constructs is +that they are all second-class. + % Virtually every programming language is equipped with one or more % control flow operators, which enable the programmer to manipulate the % flow of control of programs in interesting ways. The most well-known @@ -400,11 +403,94 @@ Monads have given rise to various popular control-oriented programming abstractions, e.g. async/await originates from monadic programming~\cite{Claessen99,LiZ07,SymePL11}. +\section{Contributions} +The key contributions of this dissertation are the following: +\begin{itemize} + \item A practical design for a programming language equipped with a + structural effect system and deep, shallow, and parameterised effect + handlers. + \item A case study in effect handler oriented programming + demonstrating how to compose the essence of an \UNIX{}-style + operating system with user session management, task parallelism, + and file I/O using standard effects and handlers. + \item A novel generalisation of the notion of continuation known as + \emph{generalised continuation}, which provides a succinct + foundation for implementing deep, shallow, and parameterised + handlers. + \item A higher-order continuation passing style translation based on + generalised continuations, which yields a universal implementation + strategy for effect handlers. + \item An abstract machine semantics based on generalised + continuations, which characterises the low-level stack + manipulations admitted by effect handlers at runtime. + \item A formal proof that deep, shallow, and parameterised handlers + are equi-expressible in the sense of typed macro-expressiveness. + \item A robust mathematical characterisation of the computational + efficiency of effect handlers, which shows that effect handlers + can improve the asymptotic runtime of certain classes of programs. + \item A comprehensive operational characterisation of various + notions of continuations and first-class control phenomena. +\end{itemize} + \section{Thesis outline} -Thesis outline\dots +Chapter~\ref{ch:maths-prep} defines some basic mathematical +notation and constructions that are they pervasively throughout this +dissertation. + +Chapter~\ref{ch:continuations} presents a literature survey of +continuations and first-class control. I classify continuations +according to their operational behaviour and provide an overview of +the various first-class sequential control operators that appear in +the literature. The application spectrum of continuations is discussed +as well as implementation strategies for first-class control. + +Chapter~\ref{ch:base-language} introduces a polymorphic fine-grain +call-by-value core calculus, $\BCalc$, which makes key use of +\citeauthor{Remy93}-style row polymorphism to implement polymorphic +variants, structural records, and a structural effect system. The +calculus distils the essence of the core of the Links programming +language. + +Chapter~\ref{ch:unary-handlers} presents three extensions of $\BCalc$, +which are $\HCalc$ that adds deep handlers, $\SCalc$ that adds shallow +handlers, and $\HPCalc$ that adds parameterised handlers. The chapter +also contains a running case study that demonstrates effect handler +oriented programming in practice by implementing a small operating +system dubbed \OSname{} based on \citeauthor{RitchieT74}'s original +\UNIX{}. + +Chapter~\ref{ch:cps} develops a higher-order continuation passing +style translation for effect handlers through a series of step-wise +refinements of an initial standard continuation passing style +translation for $\BCalc$. Each refinement slightly modifies the notion +of continuation employed by the translation. The development +ultimately leads to the key invention of generalised continuation, +which is used to give a continuation passing style semantics to deep, +shallow, and parameterised handlers. + +Chapter~\ref{ch:abstract-machine} demonstrates an application of +generalised continuations to abstract machine as we plug generalised +continuations into \citeauthor{FelleisenF86}'s CEK machine to obtain +an adequate abstract runtime with simultaneous support for deep, +shallow, and parameterised handlers. + +Chapter~\ref{ch:deep-vs-shallow} shows that deep, shallow, and +parameterised notions of handlers can simulate one another up to +specific notions of administrative reduction. + +Chapter~\ref{ch:handlers-efficiency} studies the fundamental efficiency of effect +handlers. In this chapter, we show that effect handlers enable an +asymptotic improvement in runtime complexity for a certain class of +functions. Specifically, we consider the \emph{generic count} problem +using a pure PCF-like base language $\BPCF$ (a simply typed variation +of $\BCalc$) and its extension with effect handlers $\HPCF$. +% +We show that $\HPCF$ admits an asymptotically more efficient +implementation of generic count than any $\BPCF$ implementation. +% + +Chapter~\ref{ch:conclusions} concludes and discusses future work. -\section{Typographical conventions} -Explain conventions\dots \part{Background} \label{p:background}