-\subsection{Implementation}
-The compilation of the code and the serialisation of the data throws away all typing information.
-\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.
-The \gls{ITASK} notification mechanism then takes care of the rest.
-Such \pgls{SDS} is created by using the \cleaninline{mapReadWriteError} which, given a pair of read and write functions with error handling, produces \pgls{SDS} with the lens embedded.
-The read function transforms converts the typed value to a typeless serialised value.
-The write function will, given the new serialised value and the old typed value, produce 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 lowered \gls{ITASK} \glspl{SDS} in \gls{MTASK}.}]
-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{lowerSds} that uses the \cleaninline{lens} function shown earlier.
-First, the \gls{SDS} to be lowered 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 evaluated.
-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 lowered \gls{ITASK} \glspl{SDS} in \gls{MTASK}.}]
-instance lowerSds BCInterpret where
- lowerSds def = {main =
- let (t In _) = def (abort "lowerSds: expression too strict")
- in addSdsIfNotExist (Right $ lens t)
- >>= \sdsi->let (_ In e) = def (pure (Sds sdsi)) in e.main
- }\end{lstClean}
-% VimTeX: SynIgnore off
+\section{Conclusion}
+This chapter explained the integration of \gls{MTASK} programs with \gls{ITASK}.
+Using just three \gls{ITASK} functions, \gls{MTASK} devices are integrated in \gls{ITASK} seamlessly.
+Devices, using any supported type of connection, are integrated in \gls{ITASK} using the \cleaninline{withDevice} function.
+Once connected, \gls{MTASK} tasks are sent to the device for execution using \cleaninline{liftmTask}, lifting them to full-fledged \gls{ITASK} tasks.
+To lower the bandwidth, tasks can also be preloaded.
+Furthermore, the \gls{MTASK} tasks interact with \gls{ITASK} \glspl{SDS} using the \cleaninline{lowerSds} construct.
+All of this together allows programming all layers of an \gls{IOT} system from a single source and in a single paradigm.
+All details regarding interoperation are automatically taken care of.
+The following section contains an elaborate example using all integration functions that has deliberately been placed after the conclusion.