--- /dev/null
+\documentclass[../thesis.tex]{subfiles}
+
+\begin{document}
+\ifSubfilesClassLoaded{
+ \pagenumbering{arabic}
+}{}
+
+\chapter{Introduction to \texorpdfstring{\gls{IOT}}{IoT} programming}%
+\label{chp:top4iot}
+\todo{betere chapter naam}
+\begin{chapterabstract}
+ This chapter introduces \gls{MTASK} and puts it into perspective compared to traditional microprocessor programming.
+\end{chapterabstract}
+
+Traditionally, the first program that one writes when trying a new language is the so called \emph{Hello World!} program.
+This program has the single task of printing the text \emph{Hello World!} to the screen and exiting again, useful to become familiarised with the syntax and verify that the toolchain and runtime environment is working.
+On microprocessors, there often is no screen for displaying text.
+Nevertheless, almost always there is a monochrome $1\times1$ pixel screen, namely an---often builtin---\gls{LED}.
+The \emph{Hello World!} equivalent on microprocessors blinks this \gls{LED}.
+
+\Cref{lst:arduinoBlink} shows how the logic of a blink program might look when using \gls{ARDUINO}'s \gls{CPP} dialect.
+Every \gls{ARDUINO} program contains a \arduinoinline{setup} and a \arduinoinline{loop} function.
+The \arduinoinline{setup} function is executed only once on boot, the \arduinoinline{loop} function is continuously called afterwards and contains the event loop.
+After setting the \gls{GPIO} pin to the correct mode, blink's \arduinoinline{loop} function alternates the state of the pin representing the \gls{LED} between \arduinoinline{HIGH} and \arduinoinline{LOW}, turning the \gls{LED} off and on respectively.
+In between it waits for 500 milliseconds so that the blinking is actually visible for the human eye.
+Compiling this results in a binary firmware that needs to be flashed onto the program memory.
+
+Translating the traditional blink program to \gls{MTASK} can almost be done by simply substituting some syntax as seen in \cref{lst:blinkImp}.
+E.g.\ \arduinoinline{digitalWrite} becomes \cleaninline{writeD}, literals are prefixed with \cleaninline{lit} and the pin to blink is changed to represent the actual pin for the builtin \gls{LED} of the device used in the exercises.
+In contrast to the imperative \gls{CPP} dialect, \gls{MTASK} is a \gls{TOP} language and therefore there is no such thing as a loop, only task combinators to combine tasks.
+To simulate a loop, the \cleaninline{rpeat} task can be used, this task executes the argument task and, when stable, reinstates it.
+The body of the \cleaninline{rpeat} contains similarly named tasks to write to the pins and to wait in between.
+The tasks are connected using the sequential \cleaninline{>>|.} combinator that for all current intents and purposes executes the tasks after each other.
+
+\begin{figure}[ht]
+ \begin{subfigure}[b]{.5\linewidth}
+ \begin{lstArduino}[caption={Blink program.},label={lst:arduinoBlink}]
+void setup() {
+ pinMode(D2, OUTPUT);
+}
+
+void loop() {
+ digitalWrite(D2, HIGH);
+ delay(500);
+ digitalWrite(D2, LOW);
+ delay(500);
+}\end{lstArduino}
+ \end{subfigure}%
+ \begin{subfigure}[b]{.5\linewidth}
+ \begin{lstClean}[caption={Blink program.},label={lst:blinkImp}]
+blink :: Main (MTask v ()) | mtask v
+blink =
+ declarePin D2 PMOutput \d2->
+ {main = rpeat (
+ writeD d2 true
+ >>|. delay (lit 500)
+ >>|. writeD d2 false
+ >>|. delay (lit 500)
+ )
+}\end{lstClean}
+ \end{subfigure}
+\end{figure}
+
+\section{Threaded blinking}
+Now say that we want to blink multiple blinking patterns on different \glspl{LED} concurrently.
+For example, blink three \glspl{LED} connected to \gls{GPIO} pins $1,2$ and $3$ at intervals of $500,300$ and $800$ milliseconds.
+Intuitively you want to lift the blinking behaviour to a function and call this function three times with different parameters as done in \cref{lst:blinkthreadno}
+
+\begin{lstArduino}[caption={Naive approach to multiple blinking patterns.},label={lst:blinkthreadno}]
+void setup () { ... }
+
+void blink (int pin, int wait) {
+ digitalWrite(pin, HIGH);
+ delay(wait);
+ digitalWrite(pin, LOW);
+ delay(wait);
+}
+
+void loop() {
+ blink (D1, 500);
+ blink (D2, 300);
+ blink (D3, 800);
+}\end{lstArduino}
+
+Unfortunately, this does not work because the \arduinoinline{delay} function blocks all further execution.
+The resulting program will blink the \glspl{LED} after each other instead of at the same time.
+To overcome this, it is necessary to slice up the blinking behaviour in very small fragments so it can be manually interleaved~\citep{feijs_multi-tasking_2013}.
+Listing~\ref{lst:blinkthread} shows how three different blinking patterns might be achieved in \gls{ARDUINO} using the slicing method.
+If we want the blink function to be a separate parametrizable function we need to explicitly provide all references to the required state.
+Furthermore, the \arduinoinline{delay} function can not be used and polling \arduinoinline{millis} is required.
+The \arduinoinline{millis} function returns the number of milliseconds that have passed since the boot of the microprocessor.
+Some devices use very little energy when in \arduinoinline{delay} or sleep state.
+Resulting in \arduinoinline{millis} potentially affects power consumption since the processor is basically busy looping all the time.
+In the simple case of blinking three \glspl{LED} on fixed intervals, it might be possible to calculate the delays in advance using static analysis and generate the appropriate \arduinoinline{delay} code.
+Unfortunately, this is very hard when for example the blinking patterns are determined at runtime.
+
+\begin{lstArduino}[label={lst:blinkthread},caption={Threading three blinking patterns.}]
+long led1 = 0, led2 = 0, led3 = 0;
+bool st1 = false, st2 = false, st3 = false;
+
+void blink(int pin, int dlay, long *lastrun, bool *st) {
+ if (millis() - *lastrun > dlay) {
+ digitalWrite(pin, *st = !*st);
+ *lastrun += dlay;
+ }
+}
+
+void loop() {
+ blink(D1, 500, &led1, &st1);
+ blink(D2, 300, &led2, &st1);
+ blink(D3, 800, &led3, &st1);
+}\end{lstArduino}
+
+This method is very error prone, requires a lot of pointer juggling and generally results into spaghetti code.
+Furthermore, it is very difficult to represent dependencies between threads, often state machines have to be explicitly programmed by hand to achieve this.
+
+\section{Blinking in \texorpdfstring{\gls{MTASK}}{mTask}}
+The \cleaninline{delay} \emph{task} does not block the execution but \emph{just} emits no value when the target waiting time has not yet passed and emits a stable value when the time is met.
+In contrast, the \arduinoinline{delay()} \emph{function} on the \gls{ARDUINO} is blocking which prohibits interleaving.
+To make code reuse possible and make the implementation more intuitive, the blinking behaviour is lifted to a recursive function instead of using the imperative \cleaninline{rpeat} construct.
+The function is parametrized with the current state, the pin to blink and the waiting time.
+Creating recursive functions like this is not possible in the \gls{ARDUINO} language because the program would run out of stack in an instant and nothing can be interleaved.
+With a parallel combinator, tasks can be executed in an interleaved fashion.
+Therefore, blinking three different blinking patterns is as simple as combining the three calls to the \cleaninline{blink} function with their arguments as seen in \cref{lst:blinkthreadmtask}.
+
+% VimTeX: SynIgnore on
+\begin{lstClean}[label={lst:blinkthreadmtask},caption={Threaded blinking.}]
+blinktask :: MTask v () | mtask v
+blinktask =
+ declarePin D1 PMOutput \d1->
+ declarePin D2 PMOutput \d2->
+ declarePin D3 PMOutput \d3->
+ fun \blink=(\(st, pin, wait)->
+ delay wait
+ >>|. writeD d13 st
+ >>|. blink (Not st, pin, wait)) In
+ {main = blink (true, d1, lit 500)
+ .||. blink (true, d2, lit 300)
+ .||. blink (true, d3, lit 800)
+ }\end{lstClean}
+% VimTeX: SynIgnore off
+
+\chapter{The \texorpdfstring{\gls{MTASK}}{mTask} \texorpdfstring{\gls{DSL}}{DSL}}%
+\label{chp:mtask_dsl}
+\begin{chapterabstract}
+This chapter serves as a complete guide to the \gls{MTASK} language, from an \gls{MTASK} programmer's perspective.
+\end{chapterabstract}
+
+The \gls{MTASK} system is a \gls{TOP} programming environment for programming microprocessors.
+It is implemented as an\gls{EDSL} in \gls{CLEAN} using class-based---or tagless-final---embedding (See \cref{ssec:tagless}).
+Due to the nature of the embedding technique, it is possible to have multiple interpretations of---or views on---programs written in the \gls{MTASK} language.
+The following interpretations are available for \gls{MTASK}.
+
+\begin{itemize}
+ \item Pretty printer
+
+ This interpretation converts the expression to a string representation.
+ \item Simulator
+
+ The simulator converts the expression to a ready-for-work \gls{ITASK} simulation in which the user can inspect and control the simulated peripherals and see the internal state of the tasks.
+ \item Compiler
+
+ The compiler compiles the \gls{MTASK} program at runtime to a specialised bytecode.
+ Using a handful of integration functions and tasks, \gls{MTASK} tasks can be executed on microprocessors and integrated in \gls{ITASK} as if they were regular \gls{ITASK} tasks.
+ Furthermore, with special language constructs, \glspl{SDS} can be shared between \gls{MTASK} and \gls{ITASK} programs.
+\end{itemize}
+
+When using the compiler interpretation in conjunction with the \gls{ITASK} integration, \gls{MTASK} is a heterogeneous \gls{DSL}.
+I.e.\ some components---e.g.\ the \gls{RTS} on the microprocessor---is largely unaware of the other components in the system.
+Furthermore, it is executed on a completely different architecture.
+The \gls{MTASK} language consists of a host language---a simply-typed $\lambda$-calculua with support for some basic types, function definition and data types (see \cref{sec:expressions})---enriched with a task language (see \cref{sec:top}).
+
+\section{Types}
+To leverage the type checker of the host language, types in the \gls{MTASK} language are expressed as types in the host language, to make the language type safe.
+However, not all types in the host language are suitable for microprocessors that may only have \qty{2}{\kibi\byte} of \gls{RAM} so class constraints are therefore added to the \gls{DSL} functions.
+The most used class constraint is the \cleaninline{type} class collection containing functions for serialization, printing, \gls{ITASK} constraints \etc.
+Many of these functions can be derived using generic programming.
+An even stronger restriction on types is defined for types that have a stack representation.
+This \cleaninline{basicType} class has instances for many \gls{CLEAN} basic types such as \cleaninline{Int}, \cleaninline{Real} and \cleaninline{Bool}.
+The class constraints for values in \gls{MTASK} are omnipresent in all functions and therefore often omitted throughout throughout the chapters for brevity and clarity.
+
+\begin{table}[ht]
+ \centering
+ \begin{tabular}{lll}
+ \toprule
+ \gls{CLEAN}/\gls{MTASK} & \gls{CPP} type & \textnumero{}bits\\
+ \midrule
+ \cleaninline{Bool} & \cinline{bool} & 16\\
+ \cleaninline{Char} & \cinline{char} & 16\\
+ \cleaninline{Int} & \cinline{int16_t} & 16\\
+ \cleaninline{:: Long} & \cinline{int32_t} & 32\\
+ \cleaninline{Real} & \cinline{float} & 32\\
+ \cleaninline{:: T = A \| B \| C} & \cinline{enum} & 16\\
+ \bottomrule
+ \end{tabular}
+ \caption{Mapping from \gls{CLEAN}/\gls{MTASK} data types to \gls{CPP} datatypes.}%
+ \label{tbl:mtask-c-datatypes}
+\end{table}
+
+The \gls{MTASK} language consists of a core collection of type classes bundled in the type class \cleaninline{class mtask}.
+Every interpretation implements the type classes in the \cleaninline{mtask} class
+There are also \gls{MTASK} extensions that not every interpretation implements such as peripherals and integration with \gls{ITASK}.
+
+\Cref{lst:constraints} contains the definitions for the type constraints and shows some example type signatures for typical \gls{MTASK} expressions and tasks.
+\todo{uitleggen}
+
+\begin{lstClean}[caption={Classes and class collections for the \gls{MTASK} language.},label={lst:constraints}]
+:: Main a = { main :: a }
+:: In a b = (In) infix 0 a b
+
+class type t | iTask, ... ,fromByteCode, toByteCode t
+class basicType t | type t where ...
+
+class mtask v | expr, ..., int, real, long v
+
+someExpr :: v Int | mtask v
+someExpr = ...
+
+someTask :: MTask v Int | mtask v
+someTask =
+ sensor1 config1 \sns1->
+ sensor2 config2 \sns2->
+ fun \fun1= ( ... )
+ In fun \fun2= ( ... )
+ In {main=mainexpr}
+\end{lstClean}
+
+\section{Expressions}\label{sec:expressions}
+\Cref{lst:expressions} shows the \cleaninline{expr} class containing the functionality to lift values from the host language to the \gls{MTASK} language (\cleaninline{lit}); perform number and boolean arithmetics; do comparisons; and conditional execution.
+For every common arithmetic operator in the host language, an \gls{MTASK} variant is present, suffixed by a period to not clash with \gls{CLEAN}'s builtin operators.
+
+\begin{lstClean}[caption={The \gls{MTASK} class for expressions},label={lst:expressions}]
+class expr v where
+ lit :: t -> v t | type t
+ (+.) infixl 6 :: (v t) (v t) -> v t | basicType, +, zero t
+ ...
+ (&.) infixr 3 :: (v Bool) (v Bool) -> v Bool
+ (|.) infixr 2 :: (v Bool) (v Bool) -> v Bool
+ Not :: (v Bool) -> v Bool
+ (==.) infix 4 :: (v a) (v a) -> v Bool | Eq, basicType a
+ ...
+ If :: (v Bool) (v t) (v t) -> v t | type t
+\end{lstClean}
+
+Conversion to-and-fro data types is available through the overloaded functions \cleaninline{int}, \cleaninline{long} and \cleaninline{real}.
+
+\begin{lstClean}[caption={Type conversion functions in \gls{MTASK}.}]
+class int v a :: (v a) -> v Int
+class real v a :: (v a) -> v Real
+class long v a :: (v a) -> v Long
+\end{lstClean}
+
+Finally, values from the host language must be explicitly lifted to the \gls{MTASK} language using the \cleaninline{lit} function.
+For convenience, there are many lower-cased macro definitions for often used constants such as \cleaninline{true :== lit True}, \cleaninline{false :== lit False}, \etc.
+
+\Cref{lst:example_exprs} shows some examples of these expressions.
+\cleaninline{e0} defines the literal $42$, \cleaninline{e1} calculates the literal $42.0$ using real numbers.
+\cleaninline{e2} compares \cleaninline{e0} and \cleaninline{e1} as integers and if they are equal it returns the \cleaninline{e2}$/2$ and \cleaninline{e0} otherwise.
+\cleaninline{approxEqual} performs an approximate equality---albeit not taking into account all floating point pecularities---and demonstrates that \gls{CLEAN} can be used as a macro language, i.e.\ maximise linguistic reuse~\cite{krishnamurthi_linguistic_2001}.
+\todo{uitzoeken waar dit handig is}
+When calling \cleaninline{approxEqual} in an \gls{MTASK} function, the resulting code is inlined.
+
+\begin{lstClean}[label={lst:example_exprs},caption={Example \gls{MTASK} expressions.}]
+e0 :: v Int | expr v
+e0 = lit 42
+
+e1 :: v Real | expr v
+e1 = lit 38.0 + real (lit 4)
+
+e2 :: v Int | expr v
+e2 = if' (e0 ==. int e1)
+ (int e1 /. lit 2) e0
+
+approxEqual :: (v Real) (v Real) (v Real) -> v Real | expr v
+approxEqual x y eps = if' (x == y) true
+ ( if' (x > y)
+ (y -. x < eps)
+ (x -. y < eps)
+ )
+\end{lstClean}
+
+\subsection{Data Types}
+Most of \gls{CLEAN}'s basic types have been mapped on \gls{MTASK} types.
+However, it can be useful to have access to compound types as well.
+All types in \gls{MTASK} must have a fixed size representation on the stack so sum types are not (yet) supported.
+While it is possible to lift types using the \cleaninline{lit} function, you cannot do anything with the types besides passing them around but they are being produced by some parallel task combinators (see \cref{sssec:combinators_parallel}).
+To be able to use types as first class citizens, constructors and field selectors are required.
+\Cref{lst:tuple_exprs} shows the scaffolding for supporting tuples in \gls{MTASK}.
+Besides the constructors and field selectors, there is also a helper function available that transforms a function from a tuple of \gls{MTASK} expressions to an \gls{MTASK} expression of a tuple.
+
+\begin{lstClean}[label={lst:tuple_exprs},caption={Tuple constructor and field selectors in \gls{MTASK}.}]
+class tupl v where
+ tupl :: (v a) (v b) -> v (a, b) | type a & type b
+ first :: (v (a, b)) -> v a | type a & type b
+ second :: (v (a, b)) -> v b | type a & type b
+
+ tupopen f :== \v->f (first v, second v)
+\end{lstClean}
+
+\subsection{Functions}
+Adding functions to the language is achieved by one multi-parameter class to the \gls{DSL}.
+By using \gls{HOAS}, both the function definition and the calls to the function can be controlled by the \gls{DSL}~\citep{pfenning_higher-order_1988,chlipala_parametric_2008}.
+As \gls{MTASK} only supports first-order functions and does not allow partial function application.
+Using a type class of this form, this restriction can be enforced on the type level.
+Instead of providing one instance for all functions, a single instance per function arity is defined.
+Also, \gls{MTASK} only supports top-level functions which is enforced by the \cleaninline{Main} box.
+The definition of the type class and the instances for an example interpretation are as follows:
+\todo{uitbreiden}
+
+\begin{lstClean}[caption={Functions in \gls{MTASK}.}]
+class fun a v :: ((a -> v s) -> In (a -> v s) (Main (MTask v u)))
+ -> Main (MTask v u)
+
+instance fun () Inter where ...
+instance fun (Inter a) Inter | type a where ...
+instance fun (Inter a, Inter b) Inter | type a where ...
+instance fun (Inter a, Inter b, Inter c) Inter | type a where ...
+...
+\end{lstClean}
+
+Deriving how to define and use functions from the type is quite the challenge even though the resulting syntax is made easier using the infix type \cleaninline{In}.
+\Cref{lst:function_examples} show the factorial function, a tail-call optimised factorial function and a function with zero arguments to demonstrate the syntax.
+Splitting out the function definition for each single arity means that that for every function arity and combination of arguments, a separate class constraint must be created.
+Many of the often used functions are already bundled in the \cleaninline{mtask} class constraint collection.
+\cleaninline{factorialtail} shows a manually added class constraint.
+Definiting zero arity functions is shown in the \cleaninline{zeroarity} expression.
+Finally, \cleaninline{swapTuple} shows an example of a tuple being swapped.
+
+% VimTeX: SynIgnore on
+\begin{lstClean}[label={lst:function_examples},caption={Function examples in \gls{MTASK}.}]
+factorial :: Main (v Int) | mtask v
+factorial =
+ fun \fac=(\i->if' (i <. lit 1)
+ (lit 1)
+ (i *. fac (i -. lit 1)))
+ In {main = fac (lit 5) }
+
+factorialtail :: Main (v Int) | mtask v & fun (v Int, v Int) v
+factorialtail =
+ fun \facacc=(\(acc, i)->if' (i <. lit 1)
+ acc
+ (fac (acc *. i, i -. lit 1)))
+ In fun \fac=(\i->facacc (lit 1, i))
+ In {main = fac (lit 5) }
+
+zeroarity :: Main (v Int) | mtask v
+zeroarity =
+ fun \fourtytwo=(\()->lit 42)
+ In fun \add=(\(x, y)->x +. y)
+ In {main = add (fourtytwo (), lit 9)}
+
+swapTuple :: Main (v (Int, Bool)) | mtask v
+swapTuple =
+ fun \swap=(tupopen \(x, y)->tupl y x)
+ In {main = swap (tupl true (lit 42)) }
+\end{lstClean}
+% VimTeX: SynIgnore off
+
+\section{Tasks}\label{sec:top}
+\Gls{MTASK}'s task language can be divided into three categories, namely
+\begin{enumerate*}
+ \item Basic tasks, in most \gls{TOP} systems, the basic tasks are called editors, modelling the interactivity with the user.
+ In \gls{MTASK}, there are no \emph{editors} in that sense but there is interaction with the outside world through microprocessor peripherals such as sensors and actuators.
+ \item Task combinators provide a way of describing the workflow.
+ They combine one or more tasks into a compound task.
+ \item \glspl{SDS} in \gls{MTASK} can be seen as references to data that can be shared using many-to-many communication and are only accessible from within the task language to ensure atomicity.
+\end{enumerate*}
+
+As \gls{MTASK} is integrated with \gls{ITASK}, the same stability distinction is made for task values.
+A task in \gls{MTASK} is denoted by the \gls{DSL} type synonym shown in \cref{lst:task_type}.
+
+\begin{lstClean}[label={lst:task_type},caption={Task type in \gls{MTASK}.}]
+:: MTask v a :== v (TaskValue a)
+:: TaskValue a
+ = NoValue
+ | Value a Bool
+\end{lstClean}
+
+\subsection{Basic tasks}
+The most rudimentary basic tasks are the \cleaninline{rtrn} and \cleaninline{unstable} tasks.
+They lift the value from the \gls{MTASK} expression language to the task domain either as a stable value or an unstable value.
+There is also a special type of basic task for delaying execution.
+The \cleaninline{delay} task---given a number of milliseconds---yields an unstable value while the time has not passed.
+Once the specified time has passed, the time it overshot the planned time is yielded as a stable task value.
+
+\begin{lstClean}[label={lst:basic_tasks},caption={Function examples in \gls{MTASK}.}]
+class rtrn v :: (v t) -> MTask v t
+class unstable v :: (v t) -> MTask v t
+class delay v :: (v n) -> MTask v n | long v n
+\end{lstClean}
+
+\subsubsection{Peripherals}\label{sssec:peripherals}
+For every sensor or actuator, basic tasks are available that allow interaction with the specific peripheral.
+The type classes for these tasks are not included in the \cleaninline{mtask} class collection as not all devices nor all language interpretations have such peripherals connected.
+\todo{Historically, peripheral support has been added \emph{by need}.}
+
+\Cref{lst:dht} and \cref{lst:gpio} show the type classes for \glspl{DHT} sensors and \gls{GPIO} access.
+Other peripherals have similar interfaces, they are available in the \cref{sec:aux_peripherals}.
+For the \gls{DHT} sensor there are two basic tasks, \cleaninline{temperature} and \cleaninline{humidity}, that---will given a \cleaninline{DHT} object---produce a task that yields the observed temperature in \unit{\celcius} or relative humidity as a percentage as an unstable value.
+Currently, two different types of \gls{DHT} sensors are supported, the \emph{DHT} family of sensors connect through $1$-wire protocol and the \emph{SHT} family of sensors connected using \gls{I2C} protocol.
+Creating such a \cleaninline{DHT} object is very similar to creating functions in \gls{MTASK} and uses \gls{HOAS} to make it type safe.
+
+\begin{lstClean}[label={lst:dht},caption{The \gls{MTASK} interface for \glspl{DHT} sensors.}]
+:: DHT //abstract
+:: DHTInfo
+ = DHT_DHT Pin DHTtype
+ | DHT_SHT I2CAddr
+:: DHTtype = DHT11 | DHT21 | DHT22
+class dht v where
+ DHT :: DHTInfo ((v DHT) -> Main (v b)) -> Main (v b) | type b
+ temperature :: (v DHT) -> MTask v Real
+ humidity :: (v DHT) -> MTask v Real
+
+measureTemp :: Main (MTask v Real) | mtask v & dht v
+measureTemp = DHT (DHT_SHT (i2c 0x36)) \dht->
+ {main=temperature dht}
+\end{lstClean}
+
+\Gls{GPIO} access is divided into three classes: analog, digital and pin modes.
+For all pins and pin modes an \gls{ADT} is available that enumerates the pins.
+The analog \gls{GPIO} pins of a microprocessor are connected to an \gls{ADC} that translates the voltage to an integer.
+Analog \gls{GPIO} pins can be either read or written to.
+Digital \gls{GPIO} pins only report a high or a low value.
+The type class definition is a bit more complex since analog \gls{GPIO} pins can be used as digital \gls{GPIO} pins as well.
+Therefore, if the \cleaninline{p} type implements the \cleaninline{pin} class---i.e.\ either \cleaninline{APin} or \cleaninline{DPin}---the \cleaninline{dio} class can be used.
+\Gls{GPIO} pins usually operate according to a certain pin mode that states whether the pin acts as an input pin, an input with an internal pull-up resistor or an output pin.
+This setting can be applied using the \cleaninline{pinMode} class by hand or by using the \cleaninline{declarePin} \gls{GPIO} pin constructor.
+Setting the pin mode is a task that immediately finisheds and fields a stable unit value.
+Writing to a pin is also a task that immediately finishes but yields the written value instead.
+Reading a pin is a task that yields an unstable value---i.e.\ the value read from the actual pin.
+
+\begin{lstClean}[label={lst:gpio},caption{The \gls{MTASK} interface for \gls{GPIO} access.}]
+:: APin = A0 | A1 | A2 | A3 | A4 | A5
+:: DPin = D0 | D1 | D2 | D3 | D4 | D5 | D6 | D7 | D8 | D9 | D10 | D11 | D12 | D13
+:: PinMode = PMInput | PMOutput | PMInputPullup
+:: Pin = AnalogPin APin | DigitalPin DPin
+class pin p :: p -> Pin
+
+class aio v where
+ writeA :: (v APin) (v Int) -> MTask v Int
+ readA :: (v APin) -> MTask v Int
+
+class dio p v | pin p where
+ writeD :: (v p) (v Bool) -> MTask v Bool
+ readD :: (v p) -> MTask v Bool | pin p
+
+class pinMode v where
+ pinMode :: (v PinMode) (v p) -> MTask v () | pin p
+ declarePin :: p PinMode ((v p) -> Main (v a)) -> Main (v a) | pin p
+\end{lstClean}
+
+\subsection{Task combinators}
+Task combinators are used to combine multiple tasks into one to describe workflows.
+There are three main types of task combinators, namely:
+\begin{enumerate*}
+ \item Sequential combinators that execute tasks one after the other, possibly using the result of the left hand side.
+ \item Parallel combinators that execute tasks at the same time combining the result.
+ \item Miscellaneous combinators that change the semantics of a task---e.g.\ repeat it or delay execution.
+\end{enumerate*}
+
+\subsubsection{Sequential}
+Sequential task combination allows the right-hand side task to observe the left-hand side task value.
+All seqential task combinators are expressed in the \cleaninline{expr} class and can be---and are by default---derived from the Swiss army knife step combinator \cleaninline{>>*.}.
+This combinator has a single task on the left-hand side and a list of \emph{task continuations} on the right-hand side.
+The list of task continuations is checked every rewrite step and if one of the predicates matches, the task continues with the result of this combination.
+\cleaninline{>>=.} is a shorthand for the bind operation, if the left-hand side is stable, the right-hand side function is called to produce a new task.
+\cleaninline{>>|.} is a shorthand for the sequence operation, if the left-hand side is stable, it continues with the right-hand side task.
+The \cleaninline{>>~.} and \cleaninline{>>..} combinators are variants of the ones above that ignore the stability and continue on an unstable value as well.
+
+\begin{lstClean}[label={lst:mtask_sequential},caption={Sequential task combinators in \gls{MTASK}.}]
+class step v | expr v where
+ (>>*.) infixl 1 :: (MTask v t) [Step v t u] -> MTask v u
+ (>>=.) infixl 0 :: (MTask v t) ((v t) -> MTask v u) -> MTask v u
+ (>>|.) infixl 0 :: (MTask v t) (MTask v u) -> MTask v u
+ (>>~.) infixl 0 :: (MTask v t) ((v t) -> MTask v u) -> MTask v u
+ (>>..) infixl 0 :: (MTask v t) (MTask v u) -> MTask v u
+
+:: Step v t u
+ = IfValue ((v t) -> v Bool) ((v t) -> MTask v u)
+ | IfStable ((v t) -> v Bool) ((v t) -> MTask v u)
+ | IfUnstable ((v t) -> v Bool) ((v t) -> MTask v u)
+ | Always (MTask v u)
+\end{lstClean}
+
+\todo{more examples step?}
+
+The following listing shows an example of a step in action.
+The \cleaninline{readPinBin} function produces an \gls{MTASK} task that classifies the value of an analogue pin into four bins.
+It also shows that the nature of embedding allows the host language to be used as a macro language.
+Furthermore
+
+\begin{lstClean}[label={lst:mtask_readpinbin},caption={Read an analog pin and bin the value in \gls{MTASK}.}]
+readPinBin :: Int -> Main (MTask v Int) | mtask v
+readPinBin lim = declarePin PMInput A2 \a2->
+ { main = readA a2 >>*.
+ [ IfValue (\x->x <. lim) (\_->rtrn (lit bin))
+ \\ lim <-[64,128,192,256]
+ & bin <- [0..]]}
+\end{lstClean}
+
+\subsubsection{Parallel}\label{sssec:combinators_parallel}
+The result of a parallel task combination is a compound that actually executes the tasks at the same time.
+
+There are two types of parallel task combinators (see \cref{lst:mtask_parallel}).
+The conjunction combinator (\cleaninline{.&&.}) combines the result by putting the values from both sides in a tuple.
+The stability of the task depends on the stability of both children.
+If both children are stable, the result is stable, otherwise the result is unstable.
+The disjunction combinator (\cleaninline{.\|\|.}) combines the results by picking the leftmost, most stable task.
+The semantics are easily described using \gls{CLEAN} functions shown in \cref{lst:semantics_con,lst:semantics_dis}.
+
+\begin{figure}[ht]
+ \centering
+ \begin{subfigure}[t]{.5\textwidth}
+ \begin{lstClean}[caption={Semantics of the\\conjunction combinator.},label={lst:semantics_con}]
+con :: (TaskValue a) (TaskValue b)
+ -> TaskValue (a, b)
+con NoValue r = NoValue
+con l NoValue = NoValue
+con (Value l ls) (Value r rs)
+ = Value (l, r) (ls && rs)
+
+ \end{lstClean}
+ \end{subfigure}%
+ \begin{subfigure}[t]{.5\textwidth}
+ \begin{lstClean}[caption={Semantics of the\\disjunction combinator.},label={lst:semantics_dis}]
+dis :: (TaskValue a) (TaskValue a)
+ -> TaskValue a
+dis NoValue r = r
+dis l NoValue = l
+dis (Value l ls) (Value r rs)
+ | rs = Value r True
+ | otherwise = Value l ls
+ \end{lstClean}
+ \end{subfigure}
+\end{figure}
+
+\begin{lstClean}[label={lst:mtask_parallel},caption={Parallel task combinators in \gls{MTASK}.}]
+class (.&&.) infixr 4 v :: (MTask v a) (MTask v b) -> MTask v (a, b)
+class (.||.) infixr 3 v :: (MTask v a) (MTask v a) -> MTask v a
+\end{lstClean}
+
+\Cref{lst:mtask_parallel_example} gives an example of the parallel task combinator.
+This program will read two pins at the same time, returning when one of the pins becomes \arduinoinline{HIGH}.
+If the combinator was the \cleaninline{.&&.} instead, the type would be \cleaninline{MTask v (Bool, Bool)} and the task would only return when both pins have been \arduinoinline{HIGH} but not necessarily at the same time.
+
+\begin{lstClean}[label={lst:mtask_parallel_example},caption={Parallel task combinator example in \gls{MTASK}.}]
+task :: MTask v Bool
+task =
+ declarePin D0 PMInput \d0->
+ declarePin D1 PMInput \d1->
+ let monitor pin = readD pin >>*. [IfValue (\x->x) \x->rtrn x]
+ In {main = monitor d0 .||. monitor d1}
+\end{lstClean}
+
+\subsubsection{Repeat}
+The \cleaninline{rpeat} combinator executes the child task.
+If a stable value is observed, the task is reinstated.
+The functionality of \cleaninline{rpeat} can also be simulated by using functions and sequential task combinators and even made to be stateful as can be seen in \cref{lst:blinkthreadmtask}.
+
+\begin{lstClean}[label={lst:mtask_repeat},caption={Repeat task combinators in \gls{MTASK}.}]
+class rpeat v where
+ rpeat :: (MTask v a) -> MTask v a
+\end{lstClean}
+
+To demonstrate the combinator, \cref{lst:mtask_repeat_example} show \cleaninline{rpeat} in use.
+This task will mirror the value read from analog \gls{GPIO} pin \cleaninline{A1} to pin \cleaninline{A2} by constantly reading the pin and writing the result.
+
+\begin{lstClean}[label={lst:mtask_repeat_example},caption={Exemplatory repeat task in \gls{MTASK}.}]
+task :: MTask v Int | mtask v
+task =
+ declarePin A1 PMInput \a1->
+ declarePin A2 PMOutput \a2->
+ {main = rpeat (readA a1 >>~. writeA a2)}
+\end{lstClean}
+
+\subsection{\texorpdfstring{\Acrlongpl{SDS}}{Shared data sources}}
+\Glspl{SDS} in \gls{MTASK} are by default references to shared memory.
+Similar to peripherals (see \cref{sssec:peripherals}), they are constructed at the top level and are accessed through interaction tasks.
+The \cleaninline{getSds} task yields the current value of the \gls{SDS} as an unstable value.
+This behaviour is similar to the \cleaninline{watch} task in \gls{ITASK}.
+Writing a new value to an \gls{SDS} is done using \cleaninline{setSds}.
+This task yields the written value as a stable result after it is done writing.
+Getting and immediately after setting an \gls{SDS} is not an \emph{atomic} operation.
+It is possible that another task accesses the \gls{SDS} in between.
+To circumvent this issue, \cleaninline{updSds} is created, this task atomically updates the value of the \gls{SDS}.
+
+\begin{lstClean}[label={lst:mtask_sds},caption={\Glspl{SDS} in \gls{MTASK}.}]
+:: Sds a // abstract
+class sds v where
+ sds :: ((v (Sds t)) -> In t (Main (MTask v u))) -> Main (MTask v u)
+ getSds :: (v (Sds t)) -> MTask v t
+ setSds :: (v (Sds t)) (v t) -> MTask v t
+ updSds :: (v (Sds t)) ((v t) -> v t) -> MTask v t
+\end{lstClean}
+
+\todo{examples sdss}
+
+\chapter{Green computing with \texorpdfstring{\gls{MTASK}}{mTask}}%
+\label{chp:green_computing_mtask}
+
+\chapter{Integration with \texorpdfstring{\gls{ITASK}}{iTask}}%
+\label{chp:integration_with_itask}
+The \gls{MTASK} language is a multi-view \gls{DSL}, i.e.\ there are multiple interpretations possible for a single \gls{MTASK} term.
+Using the byte code compiler (\cleaninline{BCInterpret}) \gls{DSL} interpretation, \gls{MTASK} tasks are fully integrated in \gls{ITASK} and executed as if they were regular \gls{ITASK} tasks and communicate using \gls{ITASK} \glspl{SDS}.
+\Gls{MTASK} devices contain a domain-specific \gls{OS} (\gls{RTS}) and are little \gls{TOP} servers in their own respect, being able to execute tasks.
+\Cref{fig:mtask_integration} shows the architectural layout of a typical \gls{IOT} system created with \gls{ITASK} and \gls{MTASK}.
+The entire system is written as a single \gls{CLEAN} specification where multiple tasks are executed at the same time.
+Tasks can access \glspl{SDS} according to many-to-many communication and multiple clients can work on the same task.
+Devices are integrated into the system using the \cleaninline{widthDevice} function (see \cref{sec:withdevice}).
+Using \cleaninline{liftmTask}, \gls{MTASK} tasks are lifted to a device (see \cref{sec:liftmtask}).
+\Gls{ITASK} \glspl{SDS} are lifted to the \gls{MTASK} device using \cleaninline{liftsds} (see \cref{sec:liftmtask}).
+
+\begin{figure}[ht]
+ \centering
+ \includestandalone{mtask_integration}
+ \caption{\Gls{MTASK}'s integration with \gls{ITASK}.}%
+ \label{fig:mtask_integration}
+\end{figure}
+
+\section{Devices}\label{sec:withdevice}
+\Gls{MTASK} tasks in the byte code compiler view are always executed on a certain device.
+All communication with this device happens through a so-called \emph{channels} \gls{SDS}.
+The channels contain three fields, a queue of messages that are received, a queue of messages to send and a stop flag.
+Every communication method that implements the \cleaninline{channelSync} class can provide the communication with an \gls{MTASK} device.
+As of now, serial port communication, direct \gls{TCP} communication and \gls{MQTT} over \gls{TCP} are supported as communication providers.
+The \cleaninline{withDevice} function transforms a communication provider and a task that does something with this device to an \gls{ITASK} task.
+This task sets up the communication, exchanges specifications, handles errors and cleans up after closing.
+\Cref{lst:mtask_device} shows the types and interface to connecting devices.
+
+\begin{lstClean}[label={lst:mtask_device},caption={Device communication interface in \gls{MTASK}.}]
+:: MTDevice //abstract
+:: Channels :== ([MTMessageFro], [MTMessageTo], Bool)
+
+class channelSync a :: a (sds () Channels Channels) -> Task () | RWShared sds
+
+withDevice :: (a (MTDevice -> Task b) -> Task b) | iTask b & channelSync, iTask a
+\end{lstClean}
+
+\section{Lifting tasks}\label{sec:liftmtask}
+Once the connection with the device is established, \ldots
+\begin{lstClean}
+liftmTask :: (Main (BCInterpret (TaskValue u))) MTDevice -> Task u | iTask u
+\end{lstClean}
+
+\section{Lifting \texorpdfstring{\acrlongpl{SDS}}{shared data sources}}\label{sec:liftsds}
+\begin{lstClean}[label={lst:mtask_itasksds},caption={Lifted \gls{ITASK} \glspl{SDS} in \gls{MTASK}.}]
+class liftsds v where
+ liftsds :: ((v (Sds t))->In (Shared sds t) (Main (MTask v u)))
+ -> Main (MTask v u) | RWShared sds
+\end{lstClean}
+
+\chapter{Implementation}%
+\label{chp:implementation}
+IFL19 paper, bytecode instructieset~\cref{chp:bytecode_instruction_set}
+
+\section{Integration with \texorpdfstring{\gls{ITASK}}{iTask}}
+IFL18 paper stukken
+
+\chapter{\texorpdfstring{\gls{MTASK}}{mTask} history}
+\section{Generating \texorpdfstring{\gls{C}/\gls{CPP}}{C/C++} code}
+A first throw at a class-based shallowly \gls{EDSL} for microprocessors was made by \citet{plasmeijer_shallow_2016}.
+The language was called \gls{ARDSL} and offered a type safe interface to \gls{ARDUINO} \gls{CPP} dialect.
+A \gls{CPP} code generation backend was available together with an \gls{ITASK} simulation backend.
+There was no support for tasks or even functions.
+Some time later in the 2015 \gls{CEFP} summer school, an extended version was created that allowed the creation of imperative tasks, \glspl{SDS} and the usage of functions~\citep{koopman_type-safe_2019}.
+The name then changed from \gls{ARDSL} to \gls{MTASK}.
+
+\section{Integration with \texorpdfstring{\gls{ITASK}}{iTask}}
+Mart Lubbers extended this in his Master's Thesis by adding integration with \gls{ITASK} and a bytecode compiler to the language~\citep{lubbers_task_2017}.
+\Gls{SDS} in \gls{MTASK} could be accessed on the \gls{ITASK} server.
+In this way, entire \gls{IOT} systems could be programmed from a single source.
+However, this version used a simplified version of \gls{MTASK} without functions.
+This was later improved upon by creating a simplified interface where \glspl{SDS} from \gls{ITASK} could be used in \gls{MTASK} and the other way around~\citep{lubbers_task_2018}.
+It was shown by Matheus Amazonas Cabral de Andrade that it was possible to build real-life \gls{IOT} systems with this integration~\citep{amazonas_cabral_de_andrade_developing_2018}.
+Moreover, a course on the \gls{MTASK} simulator was provided at the 2018 \gls{CEFP}/\gls{3COWS} winter school in Ko\v{s}ice, Slovakia~\citep{koopman_simulation_2018}.
+
+\section{Transition to \texorpdfstring{\gls{TOP}}{TOP}}
+The \gls{MTASK} language as it is now was introduced in 2018~\citep{koopman_task-based_2018}.
+This paper updated the language to support functions, tasks and \glspl{SDS} but still compiled to \gls{CPP} \gls{ARDUINO} code.
+Later the bytecode compiler and \gls{ITASK} integration was added to the language~\citep{lubbers_interpreting_2019}.
+Moreover, it was shown that it is very intuitive to write \gls{MCU} applications in a \gls{TOP} language~\citep{lubbers_multitasking_2019}.
+One reason for this is that a lot of design patterns that are difficult using standard means are for free in \gls{TOP} (e.g.\ multithreading).
+In 2019, the \gls{CEFP} summer school in Budapest, Hungary hosted a course on developing \gls{IOT} applications with \gls{MTASK} as well~\citep{lubbers_writing_2019}.
+
+\section{\texorpdfstring{\gls{TOP}}{TOP}}
+In 2022, the SusTrainable summer school in Rijeka, Croatia hosted a course on developing greener \gls{IOT} applications using \gls{MTASK} as well (the lecture notes are to be written).
+Several students worked on extending \gls{MTASK} with many useful features:
+Erin van der Veen did preliminary work on a green computer analysis, built a simulator and explored the possibilities for adding bounded datatypes~\citep{veen_van_der_mutable_2020}; Michel de Boer investigated the possibilities for secure communication channels~\citep{boer_de_secure_2020}; and Sjoerd Crooijmans added abstractions for low-power operation to \gls{MTASK} such as hardware interrupts and power efficient scheduling~\citep{crooijmans_reducing_2021}.
+Elina Antonova defined a preliminary formal semantics for a subset of \gls{MTASK}~\citep{antonova_MTASK_2022}.
+Moreover, plans for student projects and improvements include exploring integrating \gls{TINYML} into \gls{MTASK}; and adding intermittent computing support to \gls{MTASK}.
+
+In 2023, the SusTrainable summer school in Coimbra, Portugal will host a course on \gls{MTASK} as well.
+
+\section{\texorpdfstring{\gls{MTASK}}{mTask} in practise}
+Funded by the Radboud-Glasgow Collaboration Fund, collaborative work was executed with Phil Trinder, Jeremy Singer and Adrian Ravi Kishore Ramsingh.
+An existing smart campus application was developed using \gls{MTASK} and quantitively and qualitatively compared to the original application that was developed using a traditional \gls{IOT} stack~\citep{lubbers_tiered_2020}.
+The collaboration is still ongoing and a journal article is under review comparing four approaches for the edge layer: \gls{PYTHON}, \gls{MICROPYTHON}, \gls{ITASK} and \gls{MTASK}.
+Furthermore, power efficiency behaviour of traditional versus \gls{TOP} \gls{IOT} stacks is being compared as well adding a \gls{FREERTOS} implementation to the mix as well
+
+\input{subfilepostamble}
+\end{document}
repositories / phd-thesis.git / blobdiff