more more more

[phd-thesis.git] / top / int.tex

diff --git a/top/int.tex b/top/int.tex
index 30e74a2..33f7813 100644 (file)
--- a/top/int.tex
+++ b/top/int.tex
@@ -128,34 +128,43 @@ class liftsds v where
 \end{lstClean}
 
 The compilation of the code and the serialisation of the data throws away all typing information.
-\Cref{lst:mtask_itasksds_lens} shows a pseudocode implementation of \cleaninline{liftsds}.
 \Glspl{SDS} are stored in the compiler state as a map from identifiers to either an initial value or an \cleaninline{MTLens}.
 The \cleaninline{MTLens} is a type synonym for a \gls{SDS} that represents the typeless serialised value of the underlying \gls{SDS}.
+This is done so that the \cleaninline{withDevice} task can write the received \gls{SDS} updates to the according \gls{SDS} independently.
+\Gls{ITASK}'s notification mechanism then takes care of the rest.
 Such a \gls{SDS} is created by using the \cleaninline{mapReadWriteError} which, given a pair of read and write functions with error handling, produces a \gls{SDS} with the lens embedded.
 The read function transforms, the function that converts a typed value to a typeless serialised value, just applies the serialisation.
-The write function, the function that, given the new serialised value and the old typed value, produces a new typed value tries do deserialise the value.
-
-First, in similar fashion to how functions are implemented, using fixed points, the \glspl{SDS} is 
+The write function, the function that, given the new serialised value and the old typed value, produces a new typed value.
+It tries to decode the serialised value, if that succeeds, it is written to the underlying \gls{SDS}, an error is thrown otherwise.
+\Cref{lst:mtask_itasksds_lens} provides the implementation for this:
 
 % VimTeX: SynIgnore on
 \begin{lstClean}[label={lst:mtask_itasksds_lens},caption={Lens applied to lifted \gls{ITASK} \glspl{SDS} in \gls{MTASK}.}]
-instance liftsds BCInterpret where
+lens :: (Shared sds a) -> MTLens | type a & RWShared sds
+lens sds = mapReadWriteError
+       ( \r->Ok (fromString (toByteCode{|*|} r)
+       , \w r-> ?Just <$> iTasksDecode (toString w)
+       ) ?None sds
+\end{lstClean}
+% VimTeX: SynIgnore off
+
+\Cref{lst:mtask_itasksds_lift} shows the code for the implementation of \cleaninline{liftsds} that uses the \cleaninline{lens} function shown earlier.
+First, the \gls{SDS} to be lifted is extracted from the expression by bootstrapping the fixed point with a dummy value.
+This is safe because the expression on the right-hand side of the \cleaninline{In} is never used.
+Then, using \cleaninline{addSdsIfNotExist}, the identifier for this particular \gls{SDS} is either retrieved from the compiler state or generated freshly.
+This identifier is then used to provide a reference to the \cleaninline{def} definition to evaluate the main expression.
+
+% VimTeX: SynIgnore on
+\begin{lstClean}[label={lst:mtask_itasksds_lift},caption={Lens applied to lifted \gls{ITASK} \glspl{SDS} in \gls{MTASK}.}]
        liftsds def = {main =
-                       let (t In e) = def (abort "liftsds: expression too strict")
+                       let (t In _) = def (abort "liftsds: expression too strict")
                        in addSdsIfNotExist (Right $ lens t)
-                               >>= \sdsi-> let (t In e) = def (pure (Sds sdsi))
-                                       in e.main
+                               >>= \sdsi->let (_ In e) = def (pure (Sds sdsi)) in e.main
                }
        where
-               lens :: ((Shared sds a) -> MTLens) | type, iTask a & RWShared sds
-               lens = mapReadWriteError
-               ( \r->Ok (fromString (toByteCode{|*|} r)
-                       , \w r-> ?Just <$> iTasksDecode (toString w)
-                       ) ?None
 \end{lstClean}
 % VimTeX: SynIgnore off
 
-
 \section{Conclusion}