Changeset 1391 for Deliverables/D4.2-4.3/reports/D4-3.tex

Timestamp:

Oct 17, 2011, 1:09:44 PM (9 years ago)

Author:

mulligan

Message:

more added

File:

• Deliverables/D4.2-4.3/reports/D4-3.tex (modified) (2 diffs)

Deliverables/D4.2-4.3/reports/D4-3.tex

@@ -153 +153 @@
 % 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 +201 @@
 \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