From 33781a94e21bc75c93053ef65cfbc532314a8f2c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Daniel=20Hillerstr=C3=B6m?= Date: Wed, 3 Feb 2021 22:26:47 +0000 Subject: [PATCH] Start parameterised handlers. --- macros.tex | 1 + thesis.tex | 78 +++++++++++++++++++++++++++++++----------------------- 2 files changed, 46 insertions(+), 33 deletions(-) diff --git a/macros.tex b/macros.tex index 5535ef8..2176d16 100644 --- a/macros.tex +++ b/macros.tex @@ -41,6 +41,7 @@ \newcommand{\EffCalc}{\ensuremath{\lambda_{\mathsf{eff}}}\xspace} \newcommand{\UCalc}{\ensuremath{\lambda_{\mathsf{u}}}\xspace} \newcommand{\param}{\ensuremath{\ddagger}} +\newcommand{\HPCalc}{\ensuremath{\lambda_{\mathsf{h^\param}}}\xspace} %% %% Calculi terms and types type-setting. diff --git a/thesis.tex b/thesis.tex index f20fc27..f7fa591 100644 --- a/thesis.tex +++ b/thesis.tex @@ -7384,11 +7384,11 @@ file. % The function performs one invocation of $\Await$ to receive the table, and then performs a $\map$ over the table. The function argument to -$\map$ builds a string from the string-integer pair. +$\map$ builds a string from the provided string-integer pair. % Here we make use of an auxiliary function, $\intToString : \Int \to \String$, that turns an integer into a -string. The definition of the function is omitted here for brevity. +string. The definition of this function is omitted here for brevity. % % % \[ @@ -7410,6 +7410,11 @@ string. The definition of the function is omitted here for brevity. % \el % \] % + +We now have all the building blocks to construct a pipeline for +performing string frequency analysis on a file. The following performs +the analysis on the two first lines of Hamlet quote. +% \[ \ba{@{~}l@{~}l} &\bl @@ -7463,35 +7468,48 @@ string. The definition of the function is omitted here for brevity. \ea \] % -% -% \[ -% \bl -% \grep : \String \to \UnitType \eff \{\Await : \UnitType \opto \Char;\Yield : \Char \opto \UnitType\}\\ -% \grep~str \defas -% \bl -% \match\,\Record{\Do\;\Await~\Unit; str; \nil} -% \el -% \el -% \] -% +The pipeline gets bound to the variable $p$. The pipeline starts with +call to $\cat$ which streams the contents of the file +$\strlit{hamlet}$ to the process $\head$ applied to $2$, meaning it +will only forward the first two lines of the file to its +successor. The third process $\paste$ receives the first two lines one +character at a time and joins the characters into strings delimited by +whitespace. The next three instances of $\sed$ perform some string +normalisation. The first instance removes the trailing comma from the +string $\strlit{be,}$; the second normalises the capitalisation of the +word ``to''; and the third removes the trailing colon from the string +$\strlit{question:}$. The seventh process performs the frequency +analysis and outputs a table, which is being rendered as a string by +the eighth process. The output of the pipeline is supplied to the +$\echo$ utility whose output is being redirected to a file named +$\strlit{analysis}$. Contents of the file reside in location $2$ in +the data region. Here we can see that the analysis has found that the +words ``to'', ``be'', and the newline character ``$\nl$'' appear two +times each, whilst the other words appear once each. \section{Parameterised handlers} \label{sec:unary-parameterised-handlers} -Parameterised handlers are a useful idiom for handling stateful -computations. +Parameterised handlers are a variation of ordinary deep handlers with +an embedded functional state cell. This state cell is only accessible +locally within the handler. The use of state within the handler is +opaque to both the ambient context and the context of the computation +being handled. Semantically, parameterised handlers are defined as +folds with state threading over computation trees. + +We take the deep handler calculus $\HCalc$ as our starting point and +extend it with parameterised handlers to yield the calculus $\HPCalc$. \subsection{Syntax and static semantics} +In addition to a computation, a parameterised handler also take a +value as argument. This argument is the initial value of the state +cell embedded inside the handler. % -\begin{figure} - \begin{syntax} - & F &::=& \cdots \mid \Record{C; A} \Rightarrow^\param D\\ - & \delta &::=& \cdots \mid \param\\ - & M,N &::=& \cdots \mid \ParamHandle\; M \;\With\; H^\param(W)\\ - & H^\param &::=& q^A.~H - \end{syntax} - \caption{Syntax extensions for parameterised handlers.}\label{fig:param-syntax} -\end{figure} +\begin{syntax} +\slab{Handler\textrm{ }types} & F &::=& \cdots \mid \Record{C; A} \Rightarrow^\param D\\ +\slab{Computations} & M,N &::=& \cdots \mid \ParamHandle\; M \;\With\; H^\param(W)\\ +\slab{Parameterised\textrm{ }definitions} & H^\param &::=& q^A.~H +\end{syntax} % Figure~\ref{fig:param-syntax} extends the syntax of $\HCalc$ with parameterised handlers. Syntactically a parameterised @@ -7504,20 +7522,17 @@ definition is applied to a value $W$, which is the initial value of the parameter $q$. % -\begin{figure} \begin{mathpar} % Handle - \inferrule*[Lab=\tylab{Param\textrm{-}Handle}] + \inferrule*[Lab=\tylab{Handle^\param}] { % \typ{\Gamma}{V : A} \\ \typ{\Gamma}{M : C} \\ \typ{\Gamma}{W : A} \\ - \typ{\Gamma}{H^\param : \Record{C; A} \Harrow D} + \typ{\Gamma}{H^\param : \Record{C; A} \Harrow^\param D} } {\Gamma \vdash \ParamHandle \; M \; \With\; H^\param(W) : D} -\end{mathpar} -~ -\begin{mathpar} + % Parameterised handler \inferrule*[Lab=\tylab{Handler^\param}] {{\bl @@ -7531,9 +7546,6 @@ the parameter $q$. {\typ{\Delta;\Gamma}{(q^{A'} . H) : \Record{C;A'} \Harrow^\param D}} \end{mathpar} %% - \caption{Typing rules for parameterised handlers.}\label{fig:param-static-semantics} -\end{figure} -% We require two additional rules to type parameterised handlers. The rules are given in Figure~\ref{fig:param-static-semantics}. The main differences between the \tylab{Handler} and \tylab{Handler^\param} are