From 1c692d8cbf53f9762823c60655f316f9389bf5a5 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Daniel=20Hillerstr=C3=B6m?= Date: Sat, 15 May 2021 13:29:49 +0100 Subject: [PATCH] WIP --- thesis.bib | 20 ++++++++ thesis.tex | 137 ++++++++++++++++++++++++++++++++++++++++++++++++----- 2 files changed, 146 insertions(+), 11 deletions(-) diff --git a/thesis.bib b/thesis.bib index 002b929..5ee9875 100644 --- a/thesis.bib +++ b/thesis.bib @@ -768,6 +768,16 @@ year = {1992} } +@inproceedings{JonesW93, + author = {Simon L. Peyton Jones and + Philip Wadler}, + title = {Imperative Functional Programming}, + booktitle = {{POPL}}, + pages = {71--84}, + publisher = {{ACM} Press}, + year = {1993} +} + @inproceedings{Wadler95, author = {Philip Wadler}, title = {Monads for Functional Programming}, @@ -3167,4 +3177,14 @@ author= {Roshan P James and Amr Sabry}, year = {2011}, booktitle = {{TPDC}} +} + +# Fellowship of the Ring reference +@book{Tolkien54, + title = {The lord of the rings: Part 1: The fellowship of the ring}, + author = {John Ronald Reuel Tolkien}, + publisher = {Allen and Unwin}, + year = 1954, + language = {eng}, + keywords = {Fiction}, } \ No newline at end of file diff --git a/thesis.tex b/thesis.tex index 9d87a4c..4777c9b 100644 --- a/thesis.tex +++ b/thesis.tex @@ -398,11 +398,123 @@ expressiveness. \subsection{Why effect handlers matter} \section{State of effectful programming} -\subsection{Monadic programming} + +\subsection{Dark age of impurity} + +\subsection{Monadic enlightenment} +During the late 80s and early 90s monads rose to prominence as a +practical program structuring idiom for effectful +programming. Notably, they form the foundations for effectful +programming in Haskell, which adds special language-level support for +programming with monads~\cite{JonesABBBFHHHHJJLMPRRW99}. +% +\begin{definition} + A monad is a triple $(T, \Return, \bind)$ where $T$ is some unary + type constructor, $\Return$ is an operation that lifts an arbitrary + value into the monad (sometimes this operation is called `the unit + operation'), and $\bind$ is an application operator the monad (this + operator is pronounced `bind'). Implementations of $\Return$ and + $\bind$ must conform to the following interface. + % + \[ + \bl + \Return : A \to T~A \qquad\quad \bind ~: T~A \to (A \to T~B) \to T~B + \el + \] + % + Interactions between $\Return$ and $\bind$ are governed by the + so-called `monad laws'. + \begin{reductions} + \slab{Left\textrm{ }identity} & \Return\;x \bind k &=& k~x\\ + \slab{Right\textrm{ }identity} & m \bind \Return &=& m\\ + \slab{Associativity} & (m \bind k) \bind f &=& m \bind (\lambda x. k~x \bind f) + \end{reductions} +\end{definition} +% Monads have given rise to various popular control-oriented programming -abstractions, e.g. async/await originates from monadic +abstractions, e.g. the async/await idiom has its origins in monadic programming~\cite{Claessen99,LiZ07,SymePL11}. +\subsection{Option monad} +The $\Option$ type is a unary type constructor with two data +constructors, i.e. $\Option~A \defas [\Some:A|\None]$. + +\begin{definition} The option monad is a monad equipped with a single + failure operation. + % + \[ + \ba{@{~}l@{\qquad}@{~}r} + \multicolumn{2}{l}{T~A \defas \Option~A} \smallskip\\ + \multirow{2}{*}{ + \bl + \Return : A \to T~A\\ + \Return \defas \lambda x.\Some~x + \el} & + \multirow{2}{*}{ + \bl + \bind ~: T~A \to (A \to T~B) \to T~B\\ + \bind ~\defas \lambda m.\lambda k.\Case\;m\;\{\None \mapsto \None;\Some~x \mapsto k~x\} + \el}\\ & \smallskip\\ + \multicolumn{2}{l}{ + \bl + \fail : A \to T~A\\ + \fail \defas \lambda x.\None + \el} + \ea + \] + % +\end{definition} + +\subsection{State monad} + +\subsection{Continuation monad} +As in J.R.R. Tolkien's fictitious Middle-earth~\cite{Tolkien54} there +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}. + +\begin{definition} + The continuation monad is defined over some fixed return type + $R$~\cite{Wadler92}. + % + \[ + \ba{@{~}l@{\qquad\quad}@{~}r} + \multicolumn{2}{l}{T~A \defas (A \to R) \to R} \smallskip\\ + \multirow{2}{*}{ + \bl + \Return : A \to T~A\\ + \Return \defas \lambda x.\lambda k.k~x + \el} & + \multirow{2}{*}{ + \bl + \bind ~: T~A \to (A \to T~B) \to T~B\\ + \bind ~\defas \lambda m.\lambda k.\lambda f.m~(\lambda x.k~x~f) + \el} \\ & % space hack to avoid the next paragraph from + % floating into the math environment. + \ea + \] + % +\end{definition} +% +The $\Return$ operation lifts a value into the monad by using it as an +argument to the continuation $k$. The bind operator applies the monad +$m$ to an anonymous function that accepts a value $x$ of type +$A$. This value $x$ is supplied to the immediate continuation $k$ +alongside the current continuation $f$. + +Scheme's undelimited control operator $\Callcc$ is definable as a +monadic operation on the continuation monad~\cite{Wadler92}. +% +\[ + \bl + \Callcc : ((A \to T~B) \to T~A) \to T~A\\ + \Callcc \defas \lambda f.\lambda k. f\,(\lambda x.\lambda.k'.k~x)~k + \el +\] + +\subsection{Direct-style revolution} + + \section{Contributions} The key contributions of this dissertation are the following: \begin{itemize} @@ -432,7 +544,7 @@ The key contributions of this dissertation are the following: notions of continuations and first-class control phenomena. \end{itemize} -\section{Thesis outline} +\section{Structure of this dissertation} Chapter~\ref{ch:maths-prep} defines some basic mathematical notation and constructions that are they pervasively throughout this dissertation. @@ -16288,19 +16400,22 @@ handlers only get amplified in the setting of multi handlers. \paragraph{Handling linear resources} The implementation of effect handlers in Links makes the language unsound, because the \naive{} -combination of effect handlers and session typing is unsound. For -instance, it is possible to break session fidelity by twice resuming -some resumption that closes over a receive operation. Similarly, it is -possible to break type safety by using a combination of exceptions and -multi-shot resumptions, e.g. suppose some channel first expects an -integer followed by a boolean, then the running the program +combination of effect handlers and session typing is unsound. The +combined power of being able to discard some resumptions and resume +others multiple times can make for bad interactions with sessions. For +instance, suppose some channel supplies only one value, then it is +possible to break session fidelity by twice resuming some resumption +that closes over a receive operation. Similarly, it is possible to +break type safety by using a combination of exceptions and multi-shot +resumptions, e.g. suppose some channel first expects an integer +followed by a boolean, then the running the program $\Do\;\Fork\,\Unit;\keyw{send}~42;\Absurd\;\Do\;\Fail\,\Unit$ under the composition of the nondeterminism handler and default failure handler from Chapter~\ref{ch:unary-handlers} will cause the primitive $\keyw{send}$ operation to supply two integers in succession, thus breaking the session protocol. Figuring out how to safely combine -linear resources, such as channels, and effect handlers with -multi-shot resumptions is an interesting unsolved problem. +linear resources, such as channels, and handlers with multi-shot +resumptions is an interesting unsolved problem. \section{Canonical implementation strategies for handlers} Chapter~\ref{ch:cps} carries out a comprehensive study of CPS