diff --git a/macros.tex b/macros.tex index e833595..e978e74 100644 --- a/macros.tex +++ b/macros.tex @@ -69,6 +69,8 @@ \newcommand{\Fail}{\dec{Fail}} \newcommand{\Read}{\dec{Read}} \newcommand{\Write}{\dec{Write}} +\newcommand{\Char}{\dec{Char}} +\newcommand{\String}{\dec{String}} \newcommand{\True}{\mathsf{true}} \newcommand{\False}{\mathsf{false}} @@ -324,4 +326,17 @@ \newcommand{\inv}[1]{\llparenthesis #1 \rrparenthesis} % configurations -\newcommand{\conf}{\mathcal{C}} \ No newline at end of file +\newcommand{\conf}{\mathcal{C}} + +% UNIX example +\newcommand{\OSname}[0]{Tiny UNIX} +\newcommand{\Uexit}{\dec{exit}} +\newcommand{\basicIO}{\dec{basicIO}} +\newcommand{\Putc}{\dec{Putc}} +\newcommand{\putc}{\dec{putc}} +\newcommand{\UFile}{\dec{File}} +\newcommand{\UFD}{\dec{FileDescr}} +\newcommand{\fwrite}{\dec{fwrite}} +\newcommand{\iter}{\dec{iter}} +\newcommand{\stdout}{\dec{stdout}} +\newcommand{\IO}{\dec{IO}} \ No newline at end of file diff --git a/thesis.bib b/thesis.bib index 487eac5..a5af29f 100644 --- a/thesis.bib +++ b/thesis.bib @@ -1015,4 +1015,13 @@ number = {7}, pages = {365--375}, year = {1974} -} \ No newline at end of file +} + +@book{Raymond03, + author = {Eric Steven Raymond}, + title = {The Art of {UNIX} Programming}, + year = {2003}, + isbn = {0131429019}, + publisher = {Pearson Education} +} + diff --git a/thesis.tex b/thesis.tex index 6f48b4d..1775e2f 100644 --- a/thesis.tex +++ b/thesis.tex @@ -1991,280 +1991,417 @@ getting stuck on an unhandled operation. $\typ{\Gamma}{M' : C}$. \end{theorem} -\subsection{Deep handlers in action} +\section{Deep handlers in action: \OSname} \label{sec:deep-handlers-in-action} -The existing literature already covers an extensive amounts of -examples of programming with deep effect -handlers~\cite{KammarLO13,KiselyovSS13,Leijen17}. - - -\subsubsection{Exception handling} -\label{sec:exn-handling-in-action} - -Effect handlers subsume a variety of control abstractions, and -arguably the simplest such abstraction is exception handling. - -\begin{example}[Option monad, directly] - % - To handle the possibility of failure in a pure functional - programming language (e.g. Haskell~\cite{JonesABBBFHHHHJJLMPRRW99}), - a computation is run under a particular monad $m$ with some monadic - operation $\fail : \Unit \to m~\alpha$ for signalling failure. - % - Concretely, one can use the \emph{option monad} which interprets the - success of as $\Some$ value and failure as $\None$. - % - For good measure, let us first define the option type constructor. - % - \[ - \Option~\alpha \defas [\Some:\alpha;\None] - \] - % - The constructor is parameterised by a type variable $\alpha$. The - data constructor $\Some$ carries a payload of type $\alpha$, whilst - the other data constructor $\None$ carries no payload. - % - The monadic interface and its implementation for $\Option$ is as - follows. - % - \[ - \bl - \return : \alpha \to \Option~\alpha\\ - \return~x \defas \Some~x \smallskip\\ - - \bind - : \Option~\alpha \to (\alpha \to \Option~\beta) \to \Option~\beta\\ - m \bind k \defas \Case\;m\;\{ - \ba[t]{@{}l@{~}c@{~}l} - \None &\mapsto& \None\\ - \Some~x &\mapsto& k~x \} - \ea \smallskip\\ - \fail : \Unit \to \Option~\alpha\\ - \fail~\Unit \defas \None - \el - \] - % - The $\return$ operation lifts a given value into monad by tagging it - with $\Some$. The $\bind$ operation (pronounced bind) is the monadic - sequencing operation. It takes $m$, an instance of the monad, along - with a continuation $k$ and pattern matches on $m$ to determine - whether to apply the continuation. If $m$ is $\None$ then (a new - instance of) $\None$ is returned -- this essentially models - short-circuiting of failed computations. Otherwise if $m$ is $\Some$ - we apply the continuation $k$ to the payload $x$. The $\fail$ - operation is simply the constant $\None$. - % - - Let us put the monad to use. An illustrative example is safe - division. Mathematical division is not defined when the denominator - is zero. It is standard for implementations of division in safe - programming languages to raise an exception, which we can code - monadically as follows. - % - \[ - \bl - -/_{\dec{m}}- : \Record{\Float, \Float} \to \Option~\Float\\ - n/_{\dec{m}}\,d \defas - \If\;d = 0 \;\Then\;\fail~\Unit\; - \Else\;\return~(n \div d) - \el - \] - % - If the provided denominator $d$ is zero, then the implementation - signals failure by invoking the $\fail$ operation. Otherwise, the - implementation performs the mathematical division and lifts the - result into the monad via $\return$. - % - A monadic reading of the type signature tells us not only that the - computation may fail, but also that failure is interpreted using the - $\Option$ monad. - - Let us use this safe implementation of division to implement a safe - function for computing the reciprocal plus one for a given number - $x$, i.e. $\frac{1}{x} + 1$. - % - \[ - \bl - \dec{rpo_m} : \Float \to \Option~\Float\\ - \dec{rpo_m}~x \defas (1.0 /_{\dec{m}}\,x) \bind (\lambda y. \return~(y + 1.0)) - \el - \] - % - The implementation first computes the (monadic) result of dividing 1 - by $x$, and subsequently sequences this result with a continuation - that adds one to the result. - % - Consider some example evaluations. - % - \[ - \ba{@{~}l@{~}c@{~}l} - \dec{rpo_m}~1.0 &\reducesto^+& \Some~2.0\\ - \dec{rpo_m}~(-1.0) &\reducesto^+& \Some~0.0\\ - \dec{rpo_m}~0.0 &\reducesto^+& \None - \el - \] - % - The first (respectively second) evaluation follows because - $1.0/_{\dec{m}}\,1.0$ returns $\Some~1.0$ (respectively - $\Some~(-1.0)$), meaning that $\bind$ applies the continuation to - produce the result $\Some~2.0$ (respectively $\Some~0.0$). - % - The last evaluation follows because $1.0/_{\dec{m}}\,0.0$ returns - $\None$, consequently $\bind$ does not apply the continuation, thus - producing the result $\None$. - - This idea of using a monad to model failure stems from denotational - semantics and is due to Moggi~\cite{Moggi89}. - - Let us now change perspective and reimplement the above example - using effect handlers. We can translate the monadic interface into - an effect signature consisting of a single operation $\Fail$, whose - codomain is the empty type $\Zero$. We also define an auxiliary - function $\fail$ which packages an invocation of $\Fail$. - % - \[ - \bl - \Exn \defas \{\Fail: \Unit \opto \Zero\} \medskip\\ - \fail : \Unit \to \alpha \eff \Exn\\ - \fail \defas \lambda\Unit.\Absurd\;(\Do\;\Fail) - \el - \] - % - The $\Absurd$ computation term is used to coerce the return type - $\Zero$ of $\Fail$ into $\alpha$. This coercion is safe, because an - invocation of $\Fail$ can never return as there are no inhabitants - of type $\Zero$. - - We can now reimplement the safe division operator. - % - \[ - \bl - -/- : \Record{\Float, \Float} \to \Float \eff \Exn\\ - n/d \defas - \If\;d = 0 \;\Then\;\fail~\Unit\; - \Else\;n \div d - \el - \] - % - The primary difference is that the interpretation of failure is no - longer fixed. The type signature conveys that the computation may - fail, but it says nothing about how failure is interpreted. - % - It is straightforward to implement the reciprocal function. - % - \[ - \bl - \dec{rpo} : \Float \to \Float \eff \Exn\\ - \dec{rpo}~x \defas (1.0 / x) + 1.0 - \el - \] - % - The monadic bind and return are now gone. We still need to provide - an interpretation of $\Fail$. We do this by way of a handler that - interprets success as $\Some$ and failure as $\None$. - \[ - \bl - \optionalise : (\Unit \to \alpha \eff \Exn) \to \Option~\alpha\\ - \optionalise \defas \lambda m. - \ba[t]{@{~}l} - \Handle\;m~\Unit\;\With\\ - ~\ba{@{~}l@{~}c@{~}l} - \Return\;x &\mapsto& \Some~x\\ - \Fail~\Unit~resume &\mapsto& \None - \ea - \ea - \el - \] - % - The $\Return$-case injects the result of $m~\Unit$ into the option - type. The $\Fail$-case discards the provided resumption and returns - $\None$. Discarding the resumption effectively short-circuits the - handled computation. In fact, there is no alternative to discard the - resumption in this case as $resume : \Zero \to \Option~\alpha$ - cannot be invoked. Let us use this handler to interpret the - examples. - % - \[ - \ba{@{~}l@{~}c@{~}l} - \optionalise\,(\lambda\Unit.\dec{rpo}~1.0) &\reducesto^+& \Some~2.0\\ - \optionalise\,(\lambda\Unit.\dec{rpo}~(-1.0)) &\reducesto^+& \Some~0.0\\ - \optionalise\,(\lambda\Unit.\dec{rpo}~0.0) &\reducesto^+& \None - \el - \] - % - The first two evaluations follow because $\dec{rpo}$ returns - successfully, and hence, the handler tags the respective results - with $\Some$. The last evaluation follows because the safe division - operator ($-/-$) inside $\dec{rpo}$ performs an invocation of $\Fail$, - causing the handler to halt the computation and return $\None$. - - It is worth noting that we are free to choose another the - interpretation of $\Fail$. To conclude this example, let us exercise - this freedom and interpret failure outside of $\Option$. For - example, we can interpret failure as some default constant. - % - \[ - \bl - \faild : \Record{\alpha,\Unit \to \alpha \eff \Exn} \to \alpha\\ - \faild \defas \lambda \Record{default,m}. - \ba[t]{@{~}l} - \Handle\;m~\Unit\;\With\\ +A systems software engineering reading of effect handlers may be to +understand them as modular ``tiny operating systems''. Operationally, +how an \emph{operating system} interprets a set of \emph{system + commands} performed via \emph{system calls} is similar to how an +effect handler interprets a set of abstract operations performed via +operation invocations. +% +This reading was suggested to me by James McKinna (personal +communication). In this section I will take this reading literally, +and demonstrate how we can use the power of (deep) effect handlers to +implement a small operating system that supports multiple users, +time-sharing, and file i/o. +% +The operating system will be a variation of UNIX~\cite{RitchieT74}, +which we will call \OSname{}. +% +To make the task tractable we will occasionally jump some hops and +make some simplifying assumptions, nevertheless the resulting +implementation will capture the essence of a UNIX-like operating +system. +% +The implementation will be composed of several small modular effect +handlers, that each handles a particular set of system commands. In +this respect, we will truly realise \OSname{} in the spirit of the +UNIX philosophy~\cite[Section~1.6]{Raymond03}. The implementation of +the operating system will showcase several computational effects in +action including \emph{dynamic binding}, \emph{nondeterminism}, and +\emph{state}. + +\subsection{Basic i/o} +\label{sec:tiny-unix-bio} + +The file system is a cornerstone of UNIX as the notion of \emph{file} +in UNIX provides a unified abstraction for storing text, interprocess +communication, and access to devices such as terminals, printers, +network, etc. +% +Initially, we shall take a rather basic view of the file system. In +fact, our initial system will only contain a single file, and +moreover, the system will only support writing operations. This system +hardly qualifies as a UNIX file system. Nevertheless, it serves a +crucial role for development of \OSname{}, because it provides the +only means for us to be able to observe the effects of processes. +% +We defer development of a more advanced file system to +Section~\ref{sec:tiny-unix-io}. + +Much like UNIX we shall model a file as a list of characters, that is +$\UFile \defas \List~\Char$. For convenience we will use the same +model for strings, $\String \defas \List~\Char$, such that we can use +string literal notation to denote the $\texttt{"contents of a file"}$. +% +The signature of the basic file system will consist of a single +operation $\Putc$ for writing a single character to the file. +% +\[ + \IO \defas \{\Putc : \Record{\UFD;\Char} \opto \UnitType\} +\] +% +The operation is parameterised by a file descriptor ($\UFD$) and a +character. We will leave the file descriptor type abstract until +Section~\ref{sec:tiny-unix-io}, however, we will assume the existence +of a term $\stdout : \UFD$ such that we perform invocations of +$\Putc$. +% +Let us define a suitable handler for this operation. +% +\[ + \bl + \basicIO : (\UnitType \to \alpha \eff \IO) \to \Record{\alpha; \UFile}\\ + \basicIO~m \defas + \ba[t]{@{~}l} + \Handle\;m\,\Unit\;\With\\ ~\ba{@{~}l@{~}c@{~}l} - \Return\;x &\mapsto& x\\ - \Fail~\Unit~\_ &\mapsto& default - \ea - \ea - \el - \] - % - Now the $\Return$-case is just the identity and $\Fail$ is - interpreted as the provided default value. - % - We can reinterpret the above examples using $\faild$ and, for - instance, choose the constant $0.0$ as the default value. - % - \[ - \ba{@{~}l@{~}c@{~}l} - \faild\,\Record{0.0,\lambda\Unit.\dec{rpo}~1.0} &\reducesto^+& 2.0\\ - \faild\,\Record{0.0,\lambda\Unit.\dec{rpo}~(-1.0)} &\reducesto^+& 0.0\\ - \faild\,\Record{0.0,\lambda\Unit.\dec{rpo}~0.0} &\reducesto^+& 0.0 - \el - \] - % - Since failure is now interpreted as $0.0$ the second and third - computations produce the same result, even though the second - computation is successful and the third computation is failing. -\end{example} - -\begin{example}[Catch~\cite{SussmanS75}] -\end{example} - -\subsubsection{Blind and non-blind backtracking} - -\begin{example}[Non-blind backtracking] - \dhil{Nondeterminism} -\end{example} - -\subsubsection{Stateful computation} - -\begin{example}[Dynamic binding] - \dhil{Reader} -\end{example} - -\begin{example}[State handling] - \dhil{State} -\end{example} - -\subsubsection{Generators and iterators} - -\begin{example}[Inversion of control] - \dhil{Inversion of control: generator from iterator} -\end{example} + \Return\;res &\mapsto& \Record{res;\nil}\\ + \Putc~\Record{\_;c}~resume &\mapsto& + \Let\; \Record{res;file} = resume\,\Unit\;\In\; + \Record{res; c \cons file} + \ea + \ea + \el +\] +% +The handler takes as input a computation that produces some value +$\alpha$, and in doing so may perform the $\IO$ effect. +% +The handler ultimately returns a pair consisting of the return value +$\alpha$ and the final state of the file. +% +The $\Return$-case pairs the result $res$ with the empty file $\nil$ +which models the scenario where the computation $m$ performed no +$\Putc$-operations, e.g. +$\basicIO\,(\lambda\Unit.\Unit) \reducesto^+ +\Record{\Unit;\texttt{""}}$. +% +The $\Putc$-case extends the file by first invoking the resumption, +whose return type is the same as the handler's return type, thus it +returns a pair containing the result of $m$ and the file state. The +file gets extended with the character $c$ before it is returned along +with the original result of $m$. The file is effectively built bottom +up starting with the last character. -\begin{example}[Cooperative routines] - \dhil{Coop} -\end{example} +Let us define an auxiliary function that writes a string to a given +file. +% +\[ + \bl + \fwrite : \Record{\UFD;\String} \to \UnitType \eff \{\Putc : \Record{\UFD;\Char} \opto \UnitType\}\\ + \fwrite~\Record{fd;cs} \defas \iter\,(\lambda c.\Do\;\Putc\,\Record{fd;c})\,cs + \el +\] +% +The function $\fwrite$ invokes the operation $\Putc$ point-wise on the +list of characters $cs$ by using the list iteration function $\iter$. +% +We can now write some contents to the file and observe the effects. +% +\[ + \ba{@{~}l@{~}l} + &\basicIO\,(\lambda\Unit. \fwrite\,\Record{\stdout;\texttt{"Hello"}}; \fwrite\,\Record{\stdout;\texttt{"World"}})\\ + \reducesto^+& \Record{\Unit;\texttt{"HelloWorld"}} : \Record{\UnitType;\UFile} + \ea +\] -\subsection{Coding nontermination} +\subsection{Exceptions: non-local exits} +\label{sec:tiny-unix-exit} + +\subsection{Dynamic binding: the environment} +\label{sec:tiny-unix-env} + +\subsection{Nondeterminism: time sharing} +\label{sec:tiny-unix-time} + +\subsection{State: file i/o} +\label{sec:tiny-unix-io} + + +% The existing literature already contain an extensive amount of +% introductory examples of programming with (deep) effect +% handlers~\cite{KammarLO13,Pretnar15,Leijen17}. + + +% \subsubsection{Exception handling} +% \label{sec:exn-handling-in-action} + +% Effect handlers subsume a variety of control abstractions, and +% arguably the simplest such abstraction is exception handling. + +% \begin{example}[Option monad, directly] +% % +% To handle the possibility of failure in a pure functional +% programming language (e.g. Haskell~\cite{JonesABBBFHHHHJJLMPRRW99}), +% a computation is run under a particular monad $m$ with some monadic +% operation $\fail : \Unit \to m~\alpha$ for signalling failure. +% % +% Concretely, one can use the \emph{option monad} which interprets the +% success of as $\Some$ value and failure as $\None$. +% % +% For good measure, let us first define the option type constructor. +% % +% \[ +% \Option~\alpha \defas [\Some:\alpha;\None] +% \] +% % +% The constructor is parameterised by a type variable $\alpha$. The +% data constructor $\Some$ carries a payload of type $\alpha$, whilst +% the other data constructor $\None$ carries no payload. +% % +% The monadic interface and its implementation for $\Option$ is as +% follows. +% % +% \[ +% \bl +% \return : \alpha \to \Option~\alpha\\ +% \return~x \defas \Some~x \smallskip\\ +% - \bind - : \Option~\alpha \to (\alpha \to \Option~\beta) \to \Option~\beta\\ +% m \bind k \defas \Case\;m\;\{ +% \ba[t]{@{}l@{~}c@{~}l} +% \None &\mapsto& \None\\ +% \Some~x &\mapsto& k~x \} +% \ea \smallskip\\ +% \fail : \Unit \to \Option~\alpha\\ +% \fail~\Unit \defas \None +% \el +% \] +% % +% The $\return$ operation lifts a given value into monad by tagging it +% with $\Some$. The $\bind$ operation (pronounced bind) is the monadic +% sequencing operation. It takes $m$, an instance of the monad, along +% with a continuation $k$ and pattern matches on $m$ to determine +% whether to apply the continuation. If $m$ is $\None$ then (a new +% instance of) $\None$ is returned -- this essentially models +% short-circuiting of failed computations. Otherwise if $m$ is $\Some$ +% we apply the continuation $k$ to the payload $x$. The $\fail$ +% operation is simply the constant $\None$. +% % + +% Let us put the monad to use. An illustrative example is safe +% division. Mathematical division is not defined when the denominator +% is zero. It is standard for implementations of division in safe +% programming languages to raise an exception, which we can code +% monadically as follows. +% % +% \[ +% \bl +% -/_{\dec{m}}- : \Record{\Float, \Float} \to \Option~\Float\\ +% n/_{\dec{m}}\,d \defas +% \If\;d = 0 \;\Then\;\fail~\Unit\; +% \Else\;\return~(n \div d) +% \el +% \] +% % +% If the provided denominator $d$ is zero, then the implementation +% signals failure by invoking the $\fail$ operation. Otherwise, the +% implementation performs the mathematical division and lifts the +% result into the monad via $\return$. +% % +% A monadic reading of the type signature tells us not only that the +% computation may fail, but also that failure is interpreted using the +% $\Option$ monad. + +% Let us use this safe implementation of division to implement a safe +% function for computing the reciprocal plus one for a given number +% $x$, i.e. $\frac{1}{x} + 1$. +% % +% \[ +% \bl +% \dec{rpo_m} : \Float \to \Option~\Float\\ +% \dec{rpo_m}~x \defas (1.0 /_{\dec{m}}\,x) \bind (\lambda y. \return~(y + 1.0)) +% \el +% \] +% % +% The implementation first computes the (monadic) result of dividing 1 +% by $x$, and subsequently sequences this result with a continuation +% that adds one to the result. +% % +% Consider some example evaluations. +% % +% \[ +% \ba{@{~}l@{~}c@{~}l} +% \dec{rpo_m}~1.0 &\reducesto^+& \Some~2.0\\ +% \dec{rpo_m}~(-1.0) &\reducesto^+& \Some~0.0\\ +% \dec{rpo_m}~0.0 &\reducesto^+& \None +% \el +% \] +% % +% The first (respectively second) evaluation follows because +% $1.0/_{\dec{m}}\,1.0$ returns $\Some~1.0$ (respectively +% $\Some~(-1.0)$), meaning that $\bind$ applies the continuation to +% produce the result $\Some~2.0$ (respectively $\Some~0.0$). +% % +% The last evaluation follows because $1.0/_{\dec{m}}\,0.0$ returns +% $\None$, consequently $\bind$ does not apply the continuation, thus +% producing the result $\None$. + +% This idea of using a monad to model failure stems from denotational +% semantics and is due to Moggi~\cite{Moggi89}. + +% Let us now change perspective and reimplement the above example +% using effect handlers. We can translate the monadic interface into +% an effect signature consisting of a single operation $\Fail$, whose +% codomain is the empty type $\Zero$. We also define an auxiliary +% function $\fail$ which packages an invocation of $\Fail$. +% % +% \[ +% \bl +% \Exn \defas \{\Fail: \Unit \opto \Zero\} \medskip\\ +% \fail : \Unit \to \alpha \eff \Exn\\ +% \fail \defas \lambda\Unit.\Absurd\;(\Do\;\Fail) +% \el +% \] +% % +% The $\Absurd$ computation term is used to coerce the return type +% $\Zero$ of $\Fail$ into $\alpha$. This coercion is safe, because an +% invocation of $\Fail$ can never return as there are no inhabitants +% of type $\Zero$. + +% We can now reimplement the safe division operator. +% % +% \[ +% \bl +% -/- : \Record{\Float, \Float} \to \Float \eff \Exn\\ +% n/d \defas +% \If\;d = 0 \;\Then\;\fail~\Unit\; +% \Else\;n \div d +% \el +% \] +% % +% The primary difference is that the interpretation of failure is no +% longer fixed. The type signature conveys that the computation may +% fail, but it says nothing about how failure is interpreted. +% % +% It is straightforward to implement the reciprocal function. +% % +% \[ +% \bl +% \dec{rpo} : \Float \to \Float \eff \Exn\\ +% \dec{rpo}~x \defas (1.0 / x) + 1.0 +% \el +% \] +% % +% The monadic bind and return are now gone. We still need to provide +% an interpretation of $\Fail$. We do this by way of a handler that +% interprets success as $\Some$ and failure as $\None$. +% \[ +% \bl +% \optionalise : (\Unit \to \alpha \eff \Exn) \to \Option~\alpha\\ +% \optionalise \defas \lambda m. +% \ba[t]{@{~}l} +% \Handle\;m~\Unit\;\With\\ +% ~\ba{@{~}l@{~}c@{~}l} +% \Return\;x &\mapsto& \Some~x\\ +% \Fail~\Unit~resume &\mapsto& \None +% \ea +% \ea +% \el +% \] +% % +% The $\Return$-case injects the result of $m~\Unit$ into the option +% type. The $\Fail$-case discards the provided resumption and returns +% $\None$. Discarding the resumption effectively short-circuits the +% handled computation. In fact, there is no alternative to discard the +% resumption in this case as $resume : \Zero \to \Option~\alpha$ +% cannot be invoked. Let us use this handler to interpret the +% examples. +% % +% \[ +% \ba{@{~}l@{~}c@{~}l} +% \optionalise\,(\lambda\Unit.\dec{rpo}~1.0) &\reducesto^+& \Some~2.0\\ +% \optionalise\,(\lambda\Unit.\dec{rpo}~(-1.0)) &\reducesto^+& \Some~0.0\\ +% \optionalise\,(\lambda\Unit.\dec{rpo}~0.0) &\reducesto^+& \None +% \el +% \] +% % +% The first two evaluations follow because $\dec{rpo}$ returns +% successfully, and hence, the handler tags the respective results +% with $\Some$. The last evaluation follows because the safe division +% operator ($-/-$) inside $\dec{rpo}$ performs an invocation of $\Fail$, +% causing the handler to halt the computation and return $\None$. + +% It is worth noting that we are free to choose another the +% interpretation of $\Fail$. To conclude this example, let us exercise +% this freedom and interpret failure outside of $\Option$. For +% example, we can interpret failure as some default constant. +% % +% \[ +% \bl +% \faild : \Record{\alpha,\Unit \to \alpha \eff \Exn} \to \alpha\\ +% \faild \defas \lambda \Record{default,m}. +% \ba[t]{@{~}l} +% \Handle\;m~\Unit\;\With\\ +% ~\ba{@{~}l@{~}c@{~}l} +% \Return\;x &\mapsto& x\\ +% \Fail~\Unit~\_ &\mapsto& default +% \ea +% \ea +% \el +% \] +% % +% Now the $\Return$-case is just the identity and $\Fail$ is +% interpreted as the provided default value. +% % +% We can reinterpret the above examples using $\faild$ and, for +% instance, choose the constant $0.0$ as the default value. +% % +% \[ +% \ba{@{~}l@{~}c@{~}l} +% \faild\,\Record{0.0,\lambda\Unit.\dec{rpo}~1.0} &\reducesto^+& 2.0\\ +% \faild\,\Record{0.0,\lambda\Unit.\dec{rpo}~(-1.0)} &\reducesto^+& 0.0\\ +% \faild\,\Record{0.0,\lambda\Unit.\dec{rpo}~0.0} &\reducesto^+& 0.0 +% \el +% \] +% % +% Since failure is now interpreted as $0.0$ the second and third +% computations produce the same result, even though the second +% computation is successful and the third computation is failing. +% \end{example} + +% \begin{example}[Catch~\cite{SussmanS75}] +% \end{example} + +% \subsubsection{Blind and non-blind backtracking} + +% \begin{example}[Non-blind backtracking] +% \dhil{Nondeterminism} +% \end{example} + +% \subsubsection{Stateful computation} + +% \begin{example}[Dynamic binding] +% \dhil{Reader} +% \end{example} + +% \begin{example}[State handling] +% \dhil{State} +% \end{example} + +% \subsubsection{Generators and iterators} + +% \begin{example}[Inversion of control] +% \dhil{Inversion of control: generator from iterator} +% \end{example} + +% \begin{example}[Cooperative routines] +% \dhil{Coop} +% \end{example} + +% \subsection{Coding nontermination} \section{Parameterised handlers} \label{sec:unary-parameterised-handlers}