dhil/phd-dissertation
1
0
Fork 0
mirror of https://github.com/dhil/phd-dissertation synced 2026-03-13 02:58:26 +00:00
Code Issues Releases Wiki Activity

WIP

Browse Source
This commit is contained in:
Daniel Hillerström
2021-05-25 00:20:51 +01:00
parent 8fad146499
commit 696266922a
1 changed files with 153 additions and 43 deletions
Download Patch File Download Diff File Expand all files Collapse all files

196
thesis.tex
View File

@@ -6500,49 +6500,158 @@ getting stuck on an unhandled operation.
\subsection{Effect sugar} \subsection{Effect sugar}
\label{sec:effect-sugar} \label{sec:effect-sugar}
The class of second-order functions capture many familiar and useful Every effect row which share the same effect variable must mention the
functions (although, it should be noted that there exist useful exact same operations to be complete. Their presence information may
functions at higher order, e.g. in differ. In higher-order effectful programming this can lead to
duplication of information, and thus verbose effect
signature. Verbosity can be a real nuisance in larger codebases.
%
We can retrospectively fix this issue with some syntactic sugar rather
than redesigning the entire effect system to rectify this problem.
%
I will describe an ad-hoc elaboration scheme, which is designed to
work well for first-order and second-order functions, but might not
work so well for third-order and above. The reason for focusing on
first-order and second-order functions is that many familiar and
useful functions are either first-order or second-order, and in the
following sections we will mostly be working with first-order and
second-order functions (although, it should be noted that there exist
useful functions at higher order, e.g. in
Chapter~\ref{ch:handlers-efficiency} we shall use third-order Chapter~\ref{ch:handlers-efficiency} we shall use third-order
functions; for an example of a sixth order function see functions; for an example of a sixth order function see
\citet{Okasaki98}). \citet{Okasaki98}).
First, let us consider some small instances of the kind of incomplete
effect rows we would like to be able to write. Consider the type of
$\map$ function for lists.
% %
\[ \[
\bl \map : \Record{\alpha \to \beta;\List~\alpha} \to \List~\beta
\pp : \EffectCat \to \EffectCat\\
\ba{@{}l@{~}c@{~}l}
\pp(\{\cdot\}) &\defas& \{\cdot\}\\
\pp(\{\varepsilon\}) &\defas& \{\varepsilon\}\\
\pp(\{\ell : A \opto B\} \cup E) &\defas& \{\ell : \theta \} \cup \pp(E),\quad \text{fresh}~\theta
\ea\\
\el
\] \]
% %
For this type to be correct in $\HCalc$ (and $\BCalc$ for that matter)
we must annotate the arrows with their effect signatures, e.g.
%
\[ \[
\bl \map : \Record{\alpha \to \beta \eff \{\varepsilon\};\List~\alpha}
\trcomp{-} : \ValTypeCat \times \EffectCat \to \ValTypeCat\\ \to \List~\beta \eff \{\varepsilon\}
\trcomp{A \to B}_E \defas \trval{A}_{E} \to \trval{B}_{\{\varepsilon\}} \eff E,\quad \text{fresh}~\varepsilon\\
\trcomp{A \to B \eff E}_{E'} \defas \trval{A}_{E \cup E'} \to \trval{B}_{\{\varepsilon\}} \eff E \cup E',\quad \text{fresh}~\varepsilon \smallskip\\
\trcomp{-} : \HandlerTypeCat \to \HandlerTypeCat\\
\trcomp{A \Harrow B} \defas \trcomp{B}_{\{\varepsilon\}} \eff \{\varepsilon\} \Harrow \trcomp{B}_{\{\varepsilon\}} \eff \{\varepsilon\},\quad \text{fresh}~\varepsilon\\
\trcomp{A \eff E_A \Harrow B} \defas \trcomp{A}_{E_A} \Harrow \trcomp{B}_{\{\varepsilon\}} \eff \pp(E),\quad \text{fresh}~\varepsilon\\
\trcomp{A \Harrow B \eff E_B} \defas \trcomp{A}_{E_B} \Harrow \trcomp{B}_{\{\varepsilon\}} \eff E_B\\
\trcomp{A \eff E_A \Harrow B \eff E_B} \defas \trcomp{A}_{E_A \cup E_B} \eff E_A \cup E_B \Harrow \trcomp{B}_{\{\varepsilon\}} \eff \pp(E_A) \cup E_B,\quad \text{fresh}~\varepsilon\\
% \trcomp{(A_1 \to B_1 \eff E_1) \to B_2 \eff E_2} \defas (\trval{A_1} \to \trval{B_1} \eff E_1 \cup E_2) \to \trval{B_2} \eff E_1 \cup E_2
% \trcomp{A \to B \eff \varepsilon} \defas A \to B \eff \{\varepsilon\}\\
% \trcomp{A \to B \eff E} \defas A' \to \trval{B}_{\{\varepsilon\}} \eff E''\\
% \quad\where~\bl
% (E', A') = \trval{A}_{\treff{E}}\;\keyw{and}\; E'' = \treff{E \cup E'}
% \el\\
% \val{A \to B \eff E} \defas A' \to B' \eff E'\\
% ~\where~\bl
% (E_A, A') = \val{A}\\
% (E_B,
% \ea
\map : \Record{\alpha \to \beta;\List~\alpha} \to \List~\beta\\
% \map : \Record{\alpha \to \beta \eff \{\varepsilon\};\List~\alpha} \to \List~\beta \eff \{\varepsilon\}
\el
\] \]
%
The effect annotations do not convey any additional information,
because the function is entirely parametric in all effects, thus the
ink spent on the effect annotations is really wasted in this instance.
%
To fix this we simply need to instantiate each computation type with
the same effect variable $\varepsilon$.
A slight variation of this example is an effectful second-order
function that is parametric in its argument's effects.
%
\[
(A \to B_1 \eff \{\varepsilon\}) \to B_2 \eff \{\ell : A' \opto B';\varepsilon\} \simeq (A \to B_1 \eff \{\ell : A' \opto B';\varepsilon\}) \to B_2 \eff \{\ell : A' \opto B';\varepsilon\}
\]
%
For the effect row of the functional parameter to be correct it must
mention the $\ell$ operation.
%
The idea here is to push the effect signature inwards. The following
infix function $\vartriangleleft$ copies operations and their presence
information from its right argument to its left argument.
%
\begin{equations}
\vartriangleleft &:& \EffectCat \times \EffectCat \to \EffectCat\\
E \vartriangleleft \{\cdot\} &\defas& E\\
E \vartriangleleft \{\varepsilon\} &\defas& E\\
E \vartriangleleft \{\ell : P;R\} &\defas&
\begin{cases}
\{\ell : P\} \uplus (E \vartriangleleft \{R\}) & \text{if } \ell \notin E\\
\{R\} \vartriangleleft E & \text{otherwise}
\end{cases}\\
\end{equations}
%
This function essentially computes the union of the two effect rows.
Another example is an observably pure function whose input is
effectful, meaning the function must be handling the effects of its
argument internally (or not apply its argument at all). To capture the
intuition that operations have been handled, we would like to not
mention the handled operations in the function's effect signature,
however, the underlying row polymorphism formalism requires us to
explicitly mention handled operations as being polymorphic in their
presence, e.g.
%
\[
(A \to B_1 \eff \{\ell : A' \opto B';\varepsilon\}) \to B_2 \eff \{\varepsilon\} \simeq (A \to B_1 \eff \{\ell : A' \opto B';\varepsilon\}) \to B_2 \eff \{\ell : \theta;\varepsilon\}
\]
%
The idea is to extract the effect signature of the domain $A$ and then
copy every operation from this signature into the function's signature
as polymorphic in its presence if it is not mentioned by the
function's signature. The following function implements the copy
aspect of this idea.
%
\begin{equations}
\vartriangleright &:& \EffectCat \times \EffectCat \to \EffectCat\\
\{\cdot\} \vartriangleright E &\defas& E\\
\{\varepsilon\} \vartriangleright E &\defas& E\\
\{\ell : A \opto B;R\} \vartriangleright E &\defas&
\begin{cases}
\{\ell : \theta\} \uplus (\{R\} \vartriangleright E) & \text{if } \ell \notin E\\
\{R\} \vartriangleright E & \text{otherwise}
\end{cases}\\
\{\ell : P;R\} \vartriangleright E &\defas&
\begin{cases}
\{\ell : P\} \uplus (\{R\} \vartriangleright E) & \text{if } \ell \notin E\\
\{R\} \vartriangleright E & \text{otherwise}
\end{cases}
\end{equations}
%
The only subtlety occur in the interesting case which is when an
operation is present in the left signature, but not in the right
signature. In this case we instantiate the operation with a fresh
presence variable in the output signature.
%
\begin{equations}
\trval{-} &:& \ValTypeCat \to \ValTypeCat\\
\trval{A \to B \eff E} &\defas& A' \to B' \eff E'\\
\multicolumn{3}{l}{\quad\where~(A', E_A) \defas \trval{A}_{E}\;\keyw{and}\;(B', \_) = \trval{B}_{\{\varepsilon\}}\;\keyw{and}\; E' = E_A \vartriangleright E} \medskip\\
\trval{-} &:& \ValTypeCat \times \EffectCat \to \ValTypeCat \times \EffectCat\\
\trval{\UnitType}_{E_{amb}} &\defas& (\UnitType, \{\cdot\})\\
\trval{A \to B \eff E}_{E_{amb}} &\defas& (A' \to B' \eff E', E_A \vartriangleright E)\\
\multicolumn{3}{l}{\quad\where~E' = E \vartriangleleft E_{amb}\;\keyw{and}\;(A', E_A) = \trval{A}_{E'}\;\keyw{and}\;(B', \_) = \trval{B}_{\{\varepsilon\}}}
\end{equations}
% which can be a real nuisance for programming as it scales poorly to large codebases.
% The idea is to push the effects inwards.
%
% \begin{equations}
% \pp &:& \EffectCat \to \EffectCat\\
% \pp(\{\cdot\}) &\defas& \{\cdot\}\\
% \pp(\{\varepsilon\}) &\defas& \{\varepsilon\}\\
% \pp(\{\ell : A \opto B;R\}) &\defas& \{\ell : \theta \} \cup \pp(\{R\}),\quad \text{fresh}~\theta
% \end{equations}
% %
% \[
% \bl
% \trcomp{-} : \ValTypeCat \to \ValTypeCat\\
% \trcomp{A} \defas \trcomp{A}_{\{\varepsilon\}} \smallskip\\
% \ba{@{}r@{~}c@{~}l}
% \trcomp{-} &:& \ValTypeCat \times \EffectCat \to \ValTypeCat \times \EffectCat\\
% \trcomp{A \to B}_E &\defas& (A' \to B' \eff E', E')\\
% \multicolumn{3}{l}{\quad\where~(A', E_A) = \trval{A}_E\;\keyw{and}\;(B', \_) = \trval{B}_{\{\varepsilon\}}\;\keyw{and}\;E' = E \cup \pp(E_A)}\\
% \trcomp{A \to B \eff E}_{E'} &\defas& \trval{A}_{E \cup E'} \to \trval{B}_{\{\varepsilon\}} \eff E \cup E'
% \ea\smallskip\\
% %
% \ba{@{}r@{~}c@{~}l}
% \trcomp{-} &:& \HandlerTypeCat \to \HandlerTypeCat\\
% \trcomp{A \Harrow B} &\defas& \trcomp{B}_{\{\varepsilon\}} \eff \{\varepsilon\} \Harrow \trcomp{B}_{\{\varepsilon\}} \eff \{\varepsilon\}\\
% \trcomp{A \eff E_A \Harrow B} &\defas& \trcomp{A}_{E_A} \Harrow \trcomp{B}_{\{\varepsilon\}} \eff \pp(E),\quad \text{fresh}~\varepsilon\\
% \trcomp{A \Harrow B \eff E_B} &\defas& \trcomp{A}_{E_B} \Harrow \trcomp{B}_{\{\varepsilon\}} \eff E_B\\
% \trcomp{A \eff E_A \Harrow B \eff E_B} &\defas& \trcomp{A}_{E} \eff E \Harrow \trcomp{B}_{\{\varepsilon\}} \eff E'\\
% \multicolumn{3}{l}{\quad \where~E = E_A \cup E_B\;\keyw{and}\;E' = \pp(E_A) \cup E_B}
% \ea\\
% \el
% \]
\section{Composing \UNIX{} with effect handlers} \section{Composing \UNIX{} with effect handlers}
\label{sec:deep-handlers-in-action} \label{sec:deep-handlers-in-action}
@@ -8298,7 +8407,7 @@ an unique entry.
\bl \bl
\If\;inode.lno > 1\;\Then\\ \If\;inode.lno > 1\;\Then\\
\quad\bl \quad\bl
\Let\;inode' \revto \Record{inode\;\With\;lno = inode.lno - 1}\\ \Let\;inode' \revto \Record{\bl inode\;\With\\lno = inode.lno - 1}\el\\
\In\;\Record{\modify\,\Record{ino;inode';fs.ilist};fs.dreg} \In\;\Record{\modify\,\Record{ino;inode';fs.ilist};fs.dreg}
\el\\ \el\\
\Else\; \Else\;
@@ -8476,7 +8585,8 @@ We can now plug it all together.
\Record{3; \Record{3;
\ba[t]{@{}l@{}l} \ba[t]{@{}l@{}l}
\texttt{"}&\texttt{UNIX is basically a simple operating system, }\\ \texttt{"}&\texttt{UNIX is basically a simple operating system, }\\
&\texttt{but you have to be a genius to understand the simplicity.\nl{"}}}, &\texttt{but you have to be a genius }\\
&\texttt{to understand the simplicity.\nl{"}}},
\ea\\ \ea\\
\Record{2; \Record{2;
\ba[t]{@{}l@{}l} \ba[t]{@{}l@{}l}
@@ -9128,25 +9238,25 @@ analysis utility need not operate on the low level of characters.
\paste : \UnitType \to \UnitType \eff \{\Await : \UnitType \opto \Char;\Yield : \String \opto \UnitType\}\\ \paste : \UnitType \to \UnitType \eff \{\Await : \UnitType \opto \Char;\Yield : \String \opto \UnitType\}\\
\paste\,\Unit \defas \paste\,\Unit \defas
\bl \bl
paste'\,\Record{\Do\;\Await~\Unit;\strlit{}}\\ pst\,\Record{\Do\;\Await~\Unit;\strlit{}}\\
\where \where
\ba[t]{@{~}l@{~}c@{~}l} \ba[t]{@{~}l@{~}c@{~}l}
paste'\,\Record{\charlit{\textnil};str} &\defas& \Do\;\Yield~str;\Do\;\Yield~\strlit{\textnil}\\ pst\,\Record{\charlit{\textnil};str} &\defas& \Do\;\Yield~str;\Do\;\Yield~\strlit{\textnil}\\
paste'\,\Record{\charlit{\nl};str} &\defas& \Do\;\Yield~str;\Do\;\Yield~\strlit{\nl};paste'\,\Record{\Do\;\Await~\Unit;\strlit{}}\\ pst\,\Record{\charlit{\nl};str} &\defas& \Do\;\Yield~str;\Do\;\Yield~\strlit{\nl};pst\,\Record{\Do\;\Await~\Unit;\strlit{}}\\
paste'\,\Record{\charlit{~};str} &\defas& \Do\;\Yield~str;paste'\,\Record{\Do\;\Await~\Unit;\strlit{}}\\ pst\,\Record{\charlit{~};str} &\defas& \Do\;\Yield~str;pst\,\Record{\Do\;\Await~\Unit;\strlit{}}\\
paste'\,\Record{c;str} &\defas& paste'\,\Record{\Do\;\Await~\Unit;str \concat [c]} pst\,\Record{c;str} &\defas& pst\,\Record{\Do\;\Await~\Unit;str \concat [c]}
\ea \ea
\el \el
\el \el
\] \]
% %
The heavy-lifting is delegated to the recursive function $paste'$ The heavy-lifting is delegated to the recursive function $pst$
which accepts two parameters: 1) the next character in the input which accepts two parameters: 1) the next character in the input
stream, and 2) a string buffer for building the output string. The stream, and 2) a string buffer for building the output string. The
function is initially applied to the first character from the stream function is initially applied to the first character from the stream
(returned by the invocation of $\Await$) and the empty string (returned by the invocation of $\Await$) and the empty string
buffer. The function $paste'$ is defined by pattern matching on the buffer. The function $pst$ is defined by pattern matching on the
character parameter. The first three definitions handle the special character parameter. The first three definitions handle the special
cases when the received character is nil, newline, and space, cases when the received character is nil, newline, and space,
respectively. If the character is nil, then the function yields the respectively. If the character is nil, then the function yields the