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

\documentclass[../thesis.tex]{subfiles}

\input{subfilepreamble}

\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.
See \cref{sec:repeat} for an example task using \cleaninline{delay}.

\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,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}

\begin{lstClean}[label={lst:gpio_examples},caption={\Gls{GPIO} example in \gls{MTASK}.}]
task1 :: MTask v Int | mtask v
task1 = declarePin A3 PMInput \a3->{main=readA a3}

task2 :: MTask v Int | mtask v
task2 = declarePin D3 PMOutput \d3->{main=writeD d3 true}
\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}\label{sec: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 >>|. delay (lit 1000))}
\end{lstClean}

\subsection{\texorpdfstring{\Glsxtrlongpl{SDS}}{Shared data sources}}
\Glspl{SDS} in \gls{MTASK} are by default references to shared memory but can also be references to \glspl{SDS} in \gls{ITASK} (see \cref{sec:liftsds}).
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 necessarily an \emph{atomic} operation in \gls{MTASK} because 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}.
The \cleaninline{updSds} task only guarantees atomicity within \gls{MTASK}.

\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}

\Cref{lst:mtask_sds_examples} shows an example using \glspl{SDS}.
The \cleaninline{count} function takes a pin and returns a task that counts the number of times the pin is observed as high by incrementing the \cleaninline{share} \gls{SDS}.
In the \cleaninline{main} expression, this function is called twice and the results are combined using the parallel or combinator (\cleaninline{.||.}).
Using a sequence of \cleaninline{getSds} and \cleaninline{setSds} would be unsafe here because the other branch might write their old increment value immediately after writing, effectively missing a count.\todo{beter opschrijven}

\begin{lstClean}[label={lst:mtask_sds_examples},caption={Examples with \glspl{SDS} in \gls{MTASK}.}]
task :: MTask v Int | mtask v
task = declarePin D3 PMInput \d3->
        declarePin D5 PMInput \d5->
           sds \share=0
        In fun \count=(\pin->
                    readD pin
                >>* [IfValue (\x->x) (\_->updSds (\x->x +. lit 1) share)]
                >>| delay (lit 100) // debounce
                >>| count pin)
        In {main=count d3 .||. count d5}
\end{lstClean}

\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{\glsxtrlongpl{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 microprocessor 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}