fix and elaborate upon parametric lenses
[msc-thesis1617.git] / methods.top.tex
index e83b6b7..aefa35d 100644 (file)
@@ -164,7 +164,7 @@ of the resource. When this happens, all waiting \glspl{Task} looking at the
 resource are notified of the update. However, it may be the case that
 \glspl{Task} were only looking at parts of the structure that was not updated.
 To solve this problem, parametric lenses were
-introduced~~\cite{domoszlai_parametric_2014}.
+introduced~\cite{domoszlai_parametric_2014}.
 
 Parametric lenses add a type variable to the \gls{SDS} that is in the current
 library functions fixed to the void type (i.e. \CI{()}). When a \gls{SDS}
@@ -173,17 +173,32 @@ predicate. This notification predicate is a function \CI{p -> Bool} where
 \CI{p} is the parametric lens type. This allows programmers to create a big
 \gls{SDS}, and have \glspl{Task} only look at parts of the big \gls{SDS}. This
 technique is used in the current system in memory shares. The \CI{IWorld}
-contains a map that is accessible through an \gls{SDS}. While all data is
+contains a map that is accessible through a \gls{SDS}. While all data is
 stored in the map, only \glspl{Task} looking at a specific entry are notified
 when the structure is updated. The type of the parametric lens is the key in
 the map.
 
 Functionality for setting parameters is added in the system. The most important
-function is the \CI{sdsFocus} function. This function is listed in
-Listing~\ref{lst:focus} and allows the programmer to fix the parametric lens to
-a specific value.
+functions are the \CI{sdsFocus} and the \CI{sdsLens} function. These functions
+are listed in Listing~\ref{lst:focus}. \CI{sdsFocus} allows the programmer to
+fix a parametric lens value. \CI{sdsLens} is a kind of \CI{mapReadWrite}
+including access to the parametric lens value. This allows the creation of
+for example \glspl{SDS} that only read and write to parts of the original
+\gls{SDS}.
 
 \begin{lstlisting}[label={lst:focus},
        caption={Parametric lens functions}]
 sdsFocus :: p (RWShared p r w) -> RWShared p` r w | iTask p
+
+:: SDSNotifyPred p :== p -> Bool
+
+:: SDSLensRead p r rs     = SDSRead        (p -> rs -> MaybeError TaskException r)
+                          | SDSReadConst   (p -> r)
+:: SDSLensWrite p w rs ws = SDSWrite       (p -> rs -> w -> MaybeError TaskException (Maybe ws))
+                          | SDSWriteConst  (p -> w -> MaybeError TaskException (Maybe ws))
+:: SDSLensNotify p w rs   = SDSNotify      (p -> rs -> w -> SDSNotifyPred p)
+                          | SDSNotifyConst (p -> w -> SDSNotifyPred p)
+
+sdsLens :: String (p -> ps) (SDSLensRead p r rs) (SDSLensWrite p w rs ws) (SDSLensNotify p w rs)
+       (RWShared ps rs ws) -> RWShared p r w | iTask ps
 \end{lstlisting}