Index: Deliverables/D4.24.3/reports/D43.tex
===================================================================
 Deliverables/D4.24.3/reports/D43.tex (revision 1375)
+++ Deliverables/D4.24.3/reports/D43.tex (revision 1391)
@@ 153,19 +153,46 @@
% SECTION. %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Use of dependent types}
\label{subsect.use.of.dependent.types}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% SECTION. %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{What we do not implement}
\label{subsect.what.we.do.not.implement}

There are a number of features that are not yet implemented in the semantics, and some routine axioms remaining.
We summarise them here:
\begin{itemize}
+\subsection{Use of monads}
+\label{subsect.use.of.monads}
+
+Monads are a categorical notion that have recently gained an amount of traction in functional programming circles.
+In particular, it was noted by Moggi that monads could be used to sequence \emph{effectful} computations in a pure manner.
+Here, `effectful computations' cover a lot of ground, from writing to files, generating fresh names, or updating an ambient notion of state.
+
+In the semantics of both front and backend intermediate languages, we make use of monads.
+In particular, we make use of two forms of monad:
+\begin{enumerate}
\item
Like in the
\end{itemize}
+An `error monad', which signals that a computation either has completed successfully, or returns with an error message.
+The sequencing operation of the error monad ensures that the result of chained computations in return the error message of the first failed computation.
+This monad is used extensively in the semantics to signal a state which cannot be recovered from.
+For instance, in the semantics of RTLabs, we make use of the error monad to signal bad final states:
+\begin{lstlisting}
+...
+ Returnstate v dst fs m $\Rightarrow$
+ match fs with
+ [ nil ⇒ Error $\ldots$ (msg FinalState) (* Already in final state *)
+  cons f fs' $\Rightarrow$
+ ! locals $\leftarrow$ match dst with
+ [ None $\Rightarrow$
+ match v with
+ [ None $\Rightarrow$ OK $\ldots$ (locals f)
+  _ $\Rightarrow$ Error $\ldots$ (msg ReturnMismatch)
+ ]
+  Some d $\Rightarrow$
+ match v with
+ [ None $\Rightarrow$ Error $\ldots$ (msg ReturnMismatch)
+  Some v' $\Rightarrow$ reg_store d v' (locals f)
+ ]
+ ];
+ ret $\ldots$ $\langle$E0, State (mk_frame (func f) locals (next f) (sp f) (retdst f)) fs' m$\rangle$
+ ]
+...
+\end{lstlisting}
+\item
+An `IO' monad, signalling the emission or reading of data to some external location or memory address.
+Here, the monads sequencing operation ensures that emissions and reads are maintained in the correct order (i.e. it maintains a `trace', or ordered sequence of IO events).
+Most functions in the intermediate language semantics fall into the IO monad.
+\end{enumerate}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ 174,4 +201,9 @@
\section{Future work}
\label{sect.future.work}
+
+A few small axioms remain to be closed.
+These relate to fetching the next instruction to be interpreted from the control flow graph, or linearised representation, of the language.
+Closing these axioms should not be a problem.
+No further work remains, aside from `tidying up' the code.
\newpage