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-19 19:26:32 +01:00
parent 09cd57fbce
commit a3e97f9510
1 changed files with 12 additions and 7 deletions
Download Patch File Download Diff File Expand all files Collapse all files

19
thesis.tex
View File

@@ -470,13 +470,19 @@ to manipulate the contents of some global state cell $st$.
\[ \[
\bl \bl
\incrEven : \UnitType \to \Bool\\ \incrEven : \UnitType \to \Bool\\
\incrEven\,\Unit \defas \Let\;v \revto !st\;\In\;st \defnas 1 + v\;\In\;\even~st \incrEven\,\Unit \defas \Let\;v \revto !st\;\In\;st \defnas 1 + v;\,\even~st
\el \el
\] \]
% %
The type signature is oblivious to the fact that the function The type signature is oblivious to the fact that the function
internally makes use of the state effect to compute its return value. internally makes use of the state effect to compute its return value.
% %
The body of the function first retrieves the current value of the
state cell and binds it to $st$. Subsequently, it destructively
increments the value of the state cell. Finally, it applies the
predicate $\even : \Int \to \Bool$ to the original state value to test
whether its parity is even.
%
We can run this computation as a subcomputation in the context of We can run this computation as a subcomputation in the context of
global state cell $st$. global state cell $st$.
% %
@@ -839,12 +845,11 @@ monad $T$~\cite{Moggi91,Wadler92}, i.e. $\getF$ and
$\putF$. Operationally, the function retrieves the current value of $\putF$. Operationally, the function retrieves the current value of
the state cell via the invocation of $\getF$. The bind operator passes the state cell via the invocation of $\getF$. The bind operator passes
this value onto the continuation, which increments the value and this value onto the continuation, which increments the value and
invokes $\putF$. The continuation applies a predicate invokes $\putF$. The continuation applies a predicate the $\even$
$\even : \Int \to \Bool$ to the original state value to test whether predicate to the original state value. The structure of the monad
its parity is even. The structure of the monad means that the result means that the result of running this computation gives us a pair
of running this computation gives us a pair consisting of boolean consisting of boolean value indicating whether the initial state was
value indicating whether the initial state was even and the final even and the final state value.
state value.
The state initialiser and monad runner is simply thunk forcing and The state initialiser and monad runner is simply thunk forcing and
function application combined. function application combined.