From 9959b211e4d40cd6a17e6fbf247ca00fcd9835a2 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Daniel=20Hillerstr=C3=B6m?= Date: Mon, 8 Feb 2021 15:01:29 +0000 Subject: [PATCH] Bits and edits --- thesis.tex | 106 +++++++++++++++++++++++++++++++++++++++++++++++------ 1 file changed, 95 insertions(+), 11 deletions(-) diff --git a/thesis.tex b/thesis.tex index 4b0698e..39a2045 100644 --- a/thesis.tex +++ b/thesis.tex @@ -166,15 +166,25 @@ programming with first-class control by separating control reifying operations from their handling. - In this thesis I develop operational foundations for programming and - implementing effect handlers. - - The first strand develops the core calculus of a programming - language with a \emph{structural} notion of effects, as opposed to - the dominant \emph{nominal} notion of effects. + This thesis is composed of three strands in which I develop + operational foundations for programming and implementing effect + handlers as well as investigating the expressive power of effect + handlers. - By making crucial use of \emph{row polymorphism} to build and track - effect signatures. + The first strand develops the core calculus of a statically typed + programming language a \emph{structural} notion of effects, as + opposed to the dominant \emph{nominal} notion of effects. + % + With the structural approach, effects need not be declared before + use. The usual safety properties of statically typed programming are + retained by making crucial use of \emph{row polymorphism} to build + and track effect signatures. + % + The calculus features three forms of handlers: deep, shallow, and + parameterised. They each offer a different approach to manipulate + the control state of programs. + % + To demonstrate the usefulness of effect\dots The second strand studies \emph{continuation passing style} and \emph{abstract machine semantics}, which are foundational techniques @@ -4717,7 +4727,7 @@ computation normal forms as there are now two ways in which a computation term can terminate: successfully returning a value or getting stuck on an unhandled operation. % -\begin{definition}[Computation normal forms] +\begin{definition}[Computation normal forms]\ref{def:comp-normal-form} We say that a computation term $N$ is normal with respect to an effect signature $E$, if $N$ is either of the form $\Return\;V$, or $\EC[\Do\;\ell\,W]$ where $\ell \in E$ and $\ell \notin \BL(\EC)$. @@ -4728,12 +4738,19 @@ getting stuck on an unhandled operation. Suppose $\typ{}{M : C}$, then either there exists $\typ{}{N : C}$ such that $M \reducesto^+ N$ and $N$ is normal, or $M$ diverges. \end{theorem} - % -\begin{theorem}[Preservation] +\begin{proof} + By induction on typing derivations. +\end{proof} +% +\begin{theorem}[Subject reduction] Suppose $\typ{\Gamma}{M : C}$ and $M \reducesto M'$, then $\typ{\Gamma}{M' : C}$. \end{theorem} +% +\begin{proof} + By induction on typing derivations. +\end{proof} \section{Composing \UNIX{} with effect handlers} \label{sec:deep-handlers-in-action} @@ -7083,6 +7100,27 @@ handler as in the setting of deep handlers, meaning is up to the programmer to supply the handler the next invocation of $\ell$ inside $\EC$. This handler may be different from $H$. +The basic metatheoretic properties of $\SCalc$ are a carbon copy of +the basic properties of $\HCalc$. +% +\begin{theorem}[Progress] + Suppose $\typ{}{M : C}$, then either there exists $\typ{}{N : C}$ + such that $M \reducesto^+ N$ and $N$ is normal, or $M$ diverges. +\end{theorem} +% +\begin{proof} + By induction on typing derivations. +\end{proof} +% +\begin{theorem}[Subject reduction] + Suppose $\typ{\Gamma}{M : C}$ and $M \reducesto M'$, then + $\typ{\Gamma}{M' : C}$. +\end{theorem} +% +\begin{proof} + By induction on typing derivations. +\end{proof} + \subsection{\UNIX{}-style pipes} \label{sec:pipes} @@ -7621,6 +7659,25 @@ rather than the original value $W$. This achieves the effect of state passing as the value of $q'$ becomes available upon the next activation of the handler. +The metatheoretic properties of $\HCalc$ carries over to $\HPCalc$. +\begin{theorem}[Progress] + Suppose $\typ{}{M : C}$, then either there exists $\typ{}{N : C}$ + such that $M \reducesto^+ N$ and $N$ is normal, or $M$ diverges. +\end{theorem} +% +\begin{proof} + By induction on typing derivations. +\end{proof} +% +\begin{theorem}[Subject reduction] + Suppose $\typ{\Gamma}{M : C}$ and $M \reducesto M'$, then + $\typ{\Gamma}{M' : C}$. +\end{theorem} +% +\begin{proof} + By induction on typing derivations. +\end{proof} + \subsection{Process synchronisation} % In Section~\ref{sec:tiny-unix-time} we implemented a time-sharing @@ -7937,6 +7994,33 @@ status list that Alice's process is the first to complete, and the second to complete is Bob's process, whilst the last process to complete is the $\init$ process. +\paragraph{Retrofitting fork} In the previous program we replaced the +original implementation of $\timeshare$ +(Section~\ref{sec:tiny-unix-time}), which handles invocations of +$\Fork : \UnitType \opto \Bool$, by $\timesharee$, which handles the +more general operation $\UFork : \UnitType \opto \Int$. In practice, +we may be unable to dispense of the old interface so easily, meaning +we have to retain support for, say, legacy reasons. As we have seen +previously we can an operation in terms of another operation. Thus to +retain support for $\Fork$ we simply have to insert a handler under +$\timesharee$ which interprets $\Fork$ in terms of $\UFork$. The +operation case of this handler would be akin to the following. +% +\[ + \OpCase{\Fork}{\Unit}{resume} \mapsto + \bl + \Let\;pid \revto \Do\;\UFork~\Unit\;\In\\ + resume\,(pid \neq 0) + \el +\] +% +The interpretation of $\Fork$ inspects the process identifier returned +by the $\UFork$ to determine the role of the current process in the +parent-child relationship. If the identifier is nonzero, then the +process is a parent, hence $\Fork$ should return $\True$ to its +caller. Otherwise it should return $\False$. This preserves the +functionality of the legacy code. + \section{Related work} \label{sec:unix-related-work}