diff --git a/thesis.bib b/thesis.bib index 68c5426..e33534d 100644 --- a/thesis.bib +++ b/thesis.bib @@ -1248,6 +1248,14 @@ volume = {33} } +@book{Church41, + author = {Alonzo Church}, + title = {The Calculi of Lambda Conversion. (AM-6) (Annals of Mathematics Studies)}, + year = {1941}, + publisher = {Princeton University Press}, + address = {USA} +} + # Termination analysis. @article{Walther94, author = {Christoph Walther}, @@ -2501,4 +2509,11 @@ volume = {108}, pages = {106--142}, year = {1963} +} + +# Scott encoding +@unpublished{Scott62, + author = {Dana Scott}, + title = {A system of functional abstraction}, + note = {Lectures delivered at University of California, Berkeley, California, USA, 1962/63} } \ No newline at end of file diff --git a/thesis.tex b/thesis.tex index 36ae468..7c59929 100644 --- a/thesis.tex +++ b/thesis.tex @@ -6654,19 +6654,23 @@ $1$ in the data region. Bob makes a soft copy of the file directory where the two filenames point to the same i-node (with index $2$), whose link counter has value $2$. -\paragraph{Summary} Starting from a simple file I/O model we seen how -the modularity of effect handlers enable us to develop a \UNIX{}-style -operating system in an incremental way by composing several handlers -to implement a basic file system, multi-user environments, and -multi-tasking support. Each incremental change to the system has been -backwards compatible with previous changes in the sense that we have -not modified any previously defined interfaces in order to support a -new feature. It serves as a testament to demonstrate the versatility -of effect handlers, and it suggests that handlers can be a viable -option to use with legacy code bases to retrofit functionality. The -operating system uses a total of 14 operations, which are being -handled by 12 handlers, some of which are used multiple times, -e.g. the $\environment$ and $\redirect$ handlers. +\paragraph{Summary} Throughout this section we have used effect +handlers to give a semantics to a \UNIX{}-style operating system by +treating system calls as effectful operations, whose semantics are +given by handlers, acting as composable micro-kernels. Starting from a +simple bare minimum file I/O model we seen how the modularity of +effect handlers enable us to develop a feature-rich operating system +in an incremental way by composing several handlers to implement a +basic file system, multi-user environments, and multi-tasking +support. Each incremental change to the system has been backwards +compatible with previous changes in the sense that we have not +modified any previously defined interfaces in order to support a new +feature. It serves as a testament to demonstrate the versatility of +effect handlers, and it suggests that handlers can be a viable option +to use with legacy code bases to retrofit functionality. The operating +system makes use of fourteen operations, which are being handled by +twelve handlers, some of which are used multiple times, e.g. the +$\environment$ and $\redirect$ handlers. % \begin{figure}[t] @@ -6963,9 +6967,86 @@ e.g. the $\environment$ and $\redirect$ handlers. \section{Shallow handlers} \label{sec:unary-shallow-handlers} +Shallow handlers are an alternative to deep handlers. Shallow handlers +are defined as case-splits over computation trees, whereas deep +handlers are defined as folds. Consequently, a shallow handler +application unfolds only a single layer of the computation tree. +% +Semantically, the difference between deep and shallow handlers is +similar to the difference between \citet{Church41} and \citet{Scott62} +encoding techniques for data types in the sense that the recursion is +intrinsic to the former, whilst recursion is extrinsic to the latter. +% +Often deep handlers are attractive because they are semantically +well-behaved and provide appropriate structure for efficient +implementations using optimisations such as fusion~\cite{WuS15}, and +as we saw in the previous they codify a wide variety of applications. +% +However, they are not always convenient for implementing other +structural recursion schemes such as mutual recursion. + \subsection{Syntax and static semantics} +\begin{syntax} +\slab{Computations} &M,N \in \CompCat &::=& \cdots \mid \ShallowHandle \; M \; \With \; H\\[1ex] +\end{syntax} +% +% +\begin{mathpar} + \inferrule*[Lab=\tylab{Handle}] + { + \typ{\Gamma}{M : C} \\ + \typ{\Gamma}{H : C \Harrow D} + } + {\Gamma \vdash \ShallowHandle \; M \; \With\; H : D} + + +%\mprset{flushleft} + \inferrule*[Lab=\tylab{Handler}] + {{\bl + C = A \eff \{(\ell_i : A_i \opto B_i)_i; R\} \\ + D = B \eff \{(\ell_i : P_i)_i; R\}\\ + H = \{\Return\;x \mapsto M\} \uplus \{ \OpCase{\ell_i}{p_i}{r_i} \mapsto N_i \}_i + \el}\\\\ + \typ{\Delta;\Gamma, x : A}{M : D}\\\\ + [\typ{\Delta;\Gamma,p_i : A_i, r_i : B_i \to C}{N_i : D}]_i + } + {\typ{\Delta;\Gamma}{H : C \Harrow D}} +\end{mathpar} +% +The \tylab{Handle} rule is simply the application rule for handlers. +% +The \tylab{Handler} rule is where most of the work happens. The effect +rows on the input computation type $C$ and the output computation type +$D$ must mention every operation in the domain of the handler. In the +output row those operations may be either present ($\Pre{A}$), absent +($\Abs$), or polymorphic in their presence ($\theta$), whilst in the +input row they must be mentioned with a present type as those types +are used to type operation clauses. +% +In each operation clause the resumption $r_i$ must have the same +return type, $D$, as its handler. In the return clause the binder $x$ +has the same type, $C$, as the result of the input computation. + + \subsection{Dynamic semantics} +We augment the operational semantics with two new reduction rules: one +for handling return values and another for handling operations. +%{\small{ +\begin{reductions} +\semlab{Ret} & + \ShallowHandle \; (\Return \; V) \; \With \; H &\reducesto& N[V/x], \hfill\text{where } \hret = \{ \Return \; x \mapsto N \} \\ +\semlab{Op} & + \ShallowHandle \; \EC[\Do \; \ell \, V] \; \With \; H + &\reducesto& N[V/p, \lambda y . \, \EC[\Return \; y]/r], \\ +\multicolumn{4}{@{}r@{}}{ + \hfill\ba[t]{@{~}r@{~}l} + \text{where}& \hell = \{ \OpCase{\ell}{p}{r} \mapsto N \}\\ + \text{and} & \ell \notin \BL(\EC) + \ea +} +\end{reductions}%}}% + \subsection{\UNIX{}-style pipes} \label{sec:pipes} @@ -7030,14 +7111,6 @@ If the producer performs the $\Yield$ operation, then $\Pipe$ is invoked with the resumption of the producer along with a thunk that applies the consumer's resumption to the yielded value. -\begin{example}[Inversion of control] - foo -\end{example} - -\begin{example}[Communicating pipes] - bar -\end{example} - \section{Parameterised handlers} \label{sec:unary-parameterised-handlers}