process comments
[phd-thesis.git] / top / lang.tex
1 \documentclass[../thesis.tex]{subfiles}
2
3 \input{subfilepreamble}
4
5 \setcounter{chapter}{4}
6
7 \begin{document}
8 \input{subfileprefix}
9 \chapter{The mTask language}%
10 \label{chp:mtask_dsl}
11 \begin{chapterabstract}
12 This chapter introduces the \gls{TOP} language \gls{MTASK} by:
13 \begin{itemize}
14 \item introducing class-based shallow embedding and the setup of the \gls{MTASK} language;
15 \item describing briefly the various interpretations;
16 \item demonstrating how the type system is leveraged to enforce all constraints;
17 \item showing the language interface for expressions, datatypes, and functions;
18 \item and explaining the tasks, task combinators, and \glspl{SDS}.
19 \end{itemize}
20 \end{chapterabstract}
21
22 Regular \gls{FP} and \gls{TOP} languages do not run on resource-constrained edge devices.
23 A \gls{DSL} is therefore used as the basis of the \gls{MTASK} system, a complete \gls{TOP} programming environment for programming microcontrollers.
24 It is implemented as an \gls{EDSL} in \gls{CLEAN} using class-based---or tagless-final---embedding.
25 This means that the language interface, i.e.\ the language constructs, are a collection of type classes.
26 Interpretations of this interface are data types implementing these classes.
27 Due to the nature of this embedding technique, it is possible to have multiple interpretations for programs written in the \gls{MTASK} language.
28 Furthermore, this particular type of embedding has the property that it is extensible both in language constructs and in interpretations.
29 Adding a language construct is as simple as adding a type class.
30 Adding an interpretation is done by creating a new data type and providing implementations for the various type classes.
31
32 In order to reduce the hardware requirements for devices running \gls{MTASK} programs, several measures have been taken.\todo{by whom? would be good here to be more explicit to make it clear at this point whether that's part of the contribution}
33 Programs in \gls{MTASK} are written in the \gls{MTASK} \gls{DSL}, separating them from the host \gls{ITASK} program.
34 This allows the tasks to be constructed at compile time in order to tailor-make them for the specific work requirements.
35 Furthermore, the \gls{MTASK} language is restricted: there are no recursive data structures, no higher-order functions, strict evaluation, and functions and objects can only be declared at the top level.
36
37 \section{Class-based shallow embedding}
38 Let us illustrate this technique by taking the very simple language of literal values.
39 \todo{show how this relates to the general embedding discussion previously}
40 This language interface can be described using a single type constructor class with a single function \cleaninline{lit}.
41 This function is for lifting values, when it has a \cleaninline{toString} instance, from the host language to our new \gls{DSL}.
42 The type variable \cleaninline{v} of the type class represents the view on the language, the interpretation.
43
44 \begin{lstClean}
45 class literals v where
46 lit :: a -> v a | toString a
47 \end{lstClean}
48
49 Providing an evaluator is straightforward as can be seen in the following listing.
50 The evaluator is just a box holding a value of the computation, but it can also be something more complex such as a monadic computation.
51
52 \begin{lstClean}
53 :: Eval a = Eval a
54
55 runEval :: (Eval a) -> a
56 runEval (Eval a) = a
57
58 instance literals Eval where
59 lit a = Eval a
60 \end{lstClean}
61
62 Extending the language with a printer is done by defining a new data type and providing instances for the type constructor classes.
63 The printer shown below only stores a printed representation and hence the type variable is just a phantom type:
64
65 \begin{lstClean}
66 :: Printer a = Printer String
67
68 runPrinter :: (Printer a) -> String
69 runPrinter (Printer a) = a
70
71 instance literals Printer where
72 lit a = Printer (toString a)
73 \end{lstClean}
74
75 Adding language constructs happens by defining new type classes and giving implementations for the interpretations.
76 The following listing adds an addition construct to the language and shows the implementations for the evaluator and printer.
77
78 \begin{lstClean}
79 class addition v where
80 add :: v a -> v a -> v a | + a
81
82 instance addition Eval where
83 add (Eval l) (Eval r) = Eval (l + r)
84
85 instance addition Printer where
86 add (Printer l) (Printer r) = Printer ("(" +++ l +++ "+" +++ r +++ ")")
87 \end{lstClean}
88
89 Terms in our toy language can be overloaded in their interpretation, they are just an interface.
90 For example, $1+5$ is written as \cleaninline{add (lit 1) (lit 5)} and has the type \cleaninline{v Int \| literals, addition v}.
91 However, due to the way let-polymorphism is implemented in most functional languages, it is not always straightforward to use multiple interpretations in one function.
92 Creating such a function, e.g.\ one that both prints and evaluates an expression, requires rank-2 polymorphism (see \cref{lst:rank2_mtask}).
93
94 \section{Types}
95 The \gls{MTASK} language is a tagless-final \gls{EDSL} as well.
96 As it is shallowly embedded, the types of the terms in the language can be constrained by type classes.
97 Types in the \gls{MTASK} language are expressed as types in the host language, to make the language type safe.
98 However, not all types in the host language are suitable for microcontrollers that may only have \qty{2}{\kibi\byte} of \gls{RAM}, so class constraints are added to the \gls{DSL} functions.
99 \Cref{tbl:mtask-c-datatypes} shows the mapping from \gls{CLEAN} types to \ccpp{} types.
100 The most used class constraint is the \cleaninline{type} class collection containing functions for serialisation, printing, \gls{ITASK} constraints, \etc\ \citep[\citesection{6.9}]{plasmeijer_clean_2021}.
101 Most of these functions are automatically derivable using generic programming but can be specialised when needed.
102 An even stronger restriction is defined for types that have a stack representation.
103 This \cleaninline{basicType} class has instances for many \gls{CLEAN} basic types such as \cleaninline{Int}, \cleaninline{Real} and \cleaninline{Bool}.
104 These class constraints for values in \gls{MTASK} are omnipresent in all functions and therefore usually omitted for brevity and clarity.
105
106 \begin{table}[ht]
107 \centering
108 \caption{Translation from \cmtask{} data types to \ccpp{} datatypes.}%
109 \label{tbl:mtask-c-datatypes}
110 \begin{tabular}{lll}
111 \toprule
112 \cmtask{} & \ccpp{} & \textnumero{}bits\\
113 \midrule
114 \cleaninline{Bool} & \cinline{bool} & 16\\
115 \cleaninline{Char} & \cinline{char} & 16\\
116 \cleaninline{Int} & \cinline{int16_t}\footnotemark{} & 16\\
117 \cleaninline{Real} & \cinline{float} & 32\\
118 \cleaninline{:: Long} & \cinline{int32_t} & 32\\
119 \cleaninline{:: T = A \| B \| C} & \cinline{enum} & 16\\
120 \bottomrule
121 \end{tabular}
122 \end{table}
123
124 \footnotetext{In \gls{ARDUINO} \ccpp{} this usually equals a \cinline{long}.}
125 \Cref{lst:constraints} contains the definitions for the auxiliary types and type constraints (such as \cleaninline{type} and \cleaninline{basicType}) that are used to construct \gls{MTASK} expressions.
126
127 \begin{lstClean}[caption={Classes and class collections for the \gls{MTASK} language.},label={lst:constraints}]
128 class type t | iTask, ... , fromByteCode, toByteCode t
129 class basicType t | type t where ...
130 \end{lstClean}
131
132 The \gls{MTASK} language interface consists of a core collection of type classes bundled in the type class \cleaninline{class mtask} (see \cref{lst:collection}).
133 Every interpretation of \gls{MTASK} terms implements the type classes in the \cleaninline{mtask} class collection.
134 %Optional \gls{MTASK} constructs such as peripherals or lowered \gls{ITASK} \glspl{SDS} are not included in this class collection because not all devices or interpretations support this.
135
136 \begin{lstClean}[caption={Class collection for the \gls{MTASK} language.},label={lst:collection}]
137 class mtask v | expr, ..., int, real, long v
138 \end{lstClean}
139
140 Peripheral, \gls{SDS}, and function definitions are always defined at the top level of \gls{MTASK} programs.
141 This is enforced by the \cleaninline{Main} type.
142 Most top level definitions are defined using \gls{HOAS}.
143 To make their syntax friendlier, the \cleaninline{In} type---an infix tuple---is used to combine these top level definitions.
144 To illustrate the structure of a \gls{MTASK} programs, \cref{lst:mtask_types} shows a skeleton of a program.
145
146 % VimTeX: SynIgnore on
147 \begin{lstClean}[caption={Auxiliary types and example task in the \gls{MTASK} language.},label={lst:mtask_types}]
148 // From the mTask library
149 :: Main a = { main :: a }
150 :: In a b = (In) infix 0 a b
151
152 someTask :: MTask v Int | mtask v & lowerSds v & sensor1 v & ...
153 someTask =
154 sensor1 config1 \sns1->
155 sensor2 config2 \sns2->
156 sds \s1 = initialValue
157 In lowerSds \s2 = someiTaskSDS
158 In fun \fun1 = ( \(a0, a1)->... )
159 In fun \fun2 = ( \a->... )
160 In { main = mainexpr }
161 \end{lstClean}
162 % VimTeX: SynIgnore off
163
164 Expressions in the \gls{MTASK} language are usually overloaded in their interpretation (\cleaninline{v}).
165 In \gls{CLEAN}, all free variables in a type are implicitly universally quantified.
166 In order to use the \gls{MTASK} expressions with multiple interpretations, rank-2 polymorphism is required \citep{odersky_putting_1996}.
167 \Cref{lst:rank2_mtask} shows an example of a function that simulates an \gls{MTASK} expression while showing the pretty printed representation in parallel.
168 Providing a type for the \cleaninline{simulateAndPrint} function is mandatory as the compiler cannot infer the type of rank-2 polymorphic functions \citep[\citesection{3.7.4}]{plasmeijer_clean_2021}.
169
170 \begin{lstClean}[label={lst:rank2_mtask},caption={Rank-2 polymorphism to allow multiple interpretations.}]
171 simulateAndPrint :: (A.v: Main (MTask v a) | mtask v) -> Task a | type a
172 simulateAndPrint mt =
173 simulate mt
174 -|| Hint "Current task:" @>> viewInformation [] (showMain mt)
175 \end{lstClean}
176
177 \section{Expressions}\label{sec:expressions}
178 This section shows all \gls{MTASK} language constructs for expressions.
179 \Cref{lst:expressions} shows the \cleaninline{expr} class containing the functionality to:
180 lift values from the host language to the \gls{MTASK} language (\cleaninline{lit});
181 perform numeric and boolean arithmetics;
182 do comparisons;
183 and perform conditional execution.
184 For every common boolean and arithmetic operator in the host language, an \gls{MTASK} variant is present.
185 The operators are suffixed by a period to not clash with the built-in operators in \gls{CLEAN}.
186
187 \begin{lstClean}[caption={The \gls{MTASK} class for expressions.},label={lst:expressions}]
188 class expr v where
189 lit :: t -> v t | type t
190 (+.) infixl 6 :: (v t) (v t) -> v t | basicType, +, zero t
191 ...
192 (&.) infixr 3 :: (v Bool) (v Bool) -> v Bool
193 (|.) infixr 2 :: (v Bool) (v Bool) -> v Bool
194 Not :: (v Bool) -> v Bool
195 (==.) infix 4 :: (v a) (v a) -> v Bool | Eq, basicType a
196 ...
197 If :: (v Bool) (v t) (v t) -> v t | type t
198 \end{lstClean}
199
200 Conversion to and fro data types is available through the overloaded functions \cleaninline{int}, \cleaninline{long} and \cleaninline{real}.
201 These functions convert the argument to the respective type similar to casting in \gls{C}.
202 For most interpretations, there are instances of these classes for all numeric types.
203
204 \begin{lstClean}[caption={Type conversion functions in \gls{MTASK}.}]
205 class int v a :: (v a) -> v Int
206 class real v a :: (v a) -> v Real
207 class long v a :: (v a) -> v Long
208 \end{lstClean}
209
210 Values from the host language must be explicitly lifted to the \gls{MTASK} language using the \cleaninline{lit} function.
211 For convenience, there are many lower-cased macro definitions for often-used constants such as \cleaninline{true :== lit True}, \cleaninline{false :== lit False}.
212
213 \Cref{lst:example_exprs} shows some examples of expressions in the \gls{MTASK} language.
214 Since they are only expressions, there is no need for a \cleaninline{Main}.
215 \cleaninline{e0} defines the literal \num{42}, \cleaninline{e1} calculates the literal \num{42.0} using real numbers and uses a type conversion.
216 \cleaninline{e2} compares \cleaninline{e0} and \cleaninline{e1} as integers and if they are equal it returns $\nicefrac{\text{\cleaninline{e2}}}{2}$ and \cleaninline{e0} otherwise.
217
218 \begin{lstClean}[label={lst:example_exprs},caption={Example \gls{MTASK} expressions.}]
219 e0 :: v Int | expr v
220 e0 = lit 42
221
222 e1 :: v Real | expr v
223 e1 = lit 38.0 +. real (lit 4)
224
225 e2 :: v Int | expr v
226 e2 = If (e0 ==. int e1)
227 (int e1 /. lit 2) e0
228 \end{lstClean}
229
230 The \gls{MTASK} language is shallowly embedded in \gls{CLEAN} and the terms are constructed and hence compiled at run time.
231 This means that \gls{MTASK} programs can also be tailor-made at run time using \gls{CLEAN} functions, maximising the linguistic reuse \citep{krishnamurthi_linguistic_2001}.
232 The \cleaninline{approxEqual} function in \cref{lst:example_macro} is an example of this.
233 It performs a simple approximate equality---admittedly not taking into account all floating point peculiarities.
234 When calling \cleaninline{approxEqual} in an \gls{MTASK} expression, the resulting code is inlined.
235
236 \begin{lstClean}[label={lst:example_macro},caption={Approximate equality in \gls{MTASK}.}]
237 approxEqual :: (v Real) (v Real) (v Real) -> v Bool | expr v
238 approxEqual x y eps = x ==. y
239 |. If (x >. y)
240 (x -. y <. eps)
241 (y -. x <. eps)
242 \end{lstClean}
243
244 \subsection{Data types}
245 Most of the fixed-size basic types from \gls{CLEAN} are mapped on \gls{MTASK} types (see \cref{tbl:mtask-c-datatypes}).
246 However, it is useful to have access to compound types as well.
247 All types in \gls{MTASK} have a fixed-size representation on the stack, so sum types are not (yet) supported.
248 It is possible to lift any types, e.g.\ tuples, using the \cleaninline{lit} function as long as they have instances for the required type classes.
249 However, you cannot do anything with values of the types besides passing them around.
250 To be able to use types as first-class citizens, constructors, and field selectors or deconstructors are required (see \cref{chp:first-class_datatypes}).
251 \Cref{lst:tuple_exprs} shows the scaffolding required for supporting tuples in \gls{MTASK}.
252 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, a deconstructor.
253 Examples of \gls{MTASK} programs using tuples are seen later in \cref{sec:mtask_functions}.
254
255 \begin{lstClean}[label={lst:tuple_exprs},caption={Tuple constructor and field selectors in \gls{MTASK}.}]
256 class tupl v where
257 tupl :: (v a) (v b) -> v (a, b) | type a & type b
258 first :: (v (a, b)) -> v a | type a & type b
259 second :: (v (a, b)) -> v b | type a & type b
260
261 tupopen :: ((v a, v b) -> v c) -> ((v (a, b)) -> v c)
262 tupopen f :== \v->f (first v, second v)
263 \end{lstClean}
264
265 \subsection{Functions}\label{sec:mtask_functions}
266 Adding functions to the language is achieved by one type class in the \gls{MTASK} \gls{DSL}.
267 By using \gls{HOAS}, both the function definitions and the calls to the functions are controlled by the \gls{DSL} \citep{pfenning_higher-order_1988,chlipala_parametric_2008}.
268 The \gls{MTASK} language enforces all functions to be first-order and forbids partial function application in order to reduce memory use and code size.
269 These restrictions are enforced by using a multi-parameter type class with two parameters instead of a type class with one type variable.
270 The first parameter represents the shape of the arguments, the second parameter the interpretation.
271 An instance is provided for each function arity instead of providing an instance for all possible arities to enforce that all functions are first order.
272 By using argument tuples to represent the arity of the function, it is not possible to create partial function applications.
273 The definition of the type class and some instances for the pretty printer are shown in \cref{lst:fun_mtask}.
274
275 \begin{lstClean}[float=,caption={Functions in \gls{MTASK}.},label={lst:fun_mtask}]
276 class fun a v :: ((a -> v s) -> In (a -> v s) (Main (MTask v u)))
277 -> Main (MTask v u)
278
279 instance fun () Show where ...
280 instance fun (Show a) Show | type a where ...
281 instance fun (Show a, Show b) Show | type a, type b where ...
282 instance fun (Show a, Show b, Show c) Show | type a, ... where ...
283 ...
284 \end{lstClean}
285
286 Deriving how to define and use functions from the type is quite a challenge even though the resulting syntax is made easier using the infix type \cleaninline{In}.
287 Splitting out the function definition for each single arity means that for every function arity and combination of arguments, a separate class constraint is required.
288 Many of the often used functions signatures are in the \cleaninline{mtask} class constraint collection.
289 \Cref{lst:function_examples} show some examples of functions to illustrate the syntax.
290 The \cleaninline{factorial} functions shows a recursive version of the factorial function.
291 The \cleaninline{factorialtail} function is a tail-call optimised version of the above.
292 It also illustrates a manually added class constraint, as they are required when functions are used that have signatures not present in the \cleaninline{mtask} class collection.
293 Zero-arity functions are always called with unit as an argument, which is shown in the \cleaninline{zeroarity} function.
294 Finally, the \cleaninline{swapTuple} function shows an example of a tuple being swapped using the \cleaninline{tupopen} macro (see \cref{lst:tuple_exprs}).
295
296 % VimTeX: SynIgnore on
297 \begin{lstClean}[label={lst:function_examples},caption={Examples of various functions in \gls{MTASK}.}]
298 factorial :: Main (v Int) | mtask v
299 factorial =
300 fun \fac = (\i->If (i <. lit 1)
301 (lit 1)
302 (i *. fac (i -. lit 1)))
303 In {main = fac (lit 5) }
304
305 factorialtail :: Main (v Int) | mtask v & fun (v Int, v Int) v
306 factorialtail =
307 fun \facacc = (\(acc, i)->If (i <. lit 1)
308 acc
309 (fac (acc *. i, i -. lit 1)))
310 In fun \fac = (\i->facacc (lit 1, i))
311 In {main = fac (lit 5) }
312
313 zeroarity :: Main (v Int) | mtask v
314 zeroarity =
315 fun \fourtytwo = (\()->lit 42)
316 In fun \add = (\(x, y)->x +. y)
317 In {main = add (fourtytwo (), lit 9)}
318 [+\pagebreak+]
319 swapTuple :: Main (v (Int, Bool)) | mtask v
320 swapTuple =
321 fun \swap = (tupopen \(x, y)->tupl y x)
322 In {main = swap (tupl true (lit 42)) }
323 \end{lstClean}
324 % VimTeX: SynIgnore off
325
326 \section{Tasks and task combinators}\label{sec:top}
327 This section describes the task language of \gls{MTASK}.
328 \Gls{TOP} languages are programming languages enriched with tasks.
329 Tasks represent abstract pieces of work and can be combined using combinators.
330 Creating tasks is done by evaluating expressions.
331 The result of an evaluated task expression is called a task tree, a run time representation of a task.
332 In order to evaluate a task, the resulting task tree is \emph{rewritten} using small-step reduction, i.e.\ similar to rewrite systems, they perform a bit of work, step by step.
333 With each step, a task value is yielded that is observable by other tasks and can be acted upon.
334
335 The implementation in the \gls{MTASK} \gls{RTS} for task execution is shown in \cref{chp:implementation}.
336 The following sections show the definitions of the functions for creating tasks.
337 They also show the semantics of tasks: their observable value in relation to the work that the task represents.
338 The task language of \gls{MTASK} is divided into three categories:
339
340 \begin{description}
341 \item [Basic tasks] are the leaves in the task trees.
342 In most \gls{TOP} systems, the basic tasks are called editors, modelling the interactivity with the user.
343 In \gls{MTASK}, there are no editors in that sense.
344 Editors in \gls{MTASK} model the interaction with the outside world through peripherals such as sensors and actuators.
345 \item [Task combinators] provide a way of describing the workflow or collaboration.
346 They combine one or more tasks into a compound task.
347 \item [\Glspl{SDS}] are typed references to shared memory in \gls{MTASK}.
348 The data is available for tasks using many-to-many communication but only from within the task language to ensure atomicity.
349 \end{description}
350
351 As \gls{MTASK} is integrated with \gls{ITASK}, a stability distinction is made for task values just as in \gls{ITASK}.
352 A task in \gls{MTASK} is denoted by the \gls{DSL} type synonym shown in \cref{lst:task_type}.
353 A task is an expression of the type \cleaninline{TaskValue a} in interpretation \cleaninline{v}.
354
355 \begin{lstClean}[label={lst:task_type},caption={Task type in \gls{MTASK}.}]
356 :: MTask v a :== v (TaskValue a)
357
358 // From the iTask library
359 :: TaskValue a
360 = NoValue
361 | Value a Bool
362 \end{lstClean}
363
364 \subsection{Basic tasks}
365 The \gls{MTASK} language contains interactive and non-interactive basic tasks.
366 As \gls{MTASK} is integrated in \gls{ITASK}, the same notion of stability is applied to the task values.
367 Task values have either \emph{no value}, or are \emph{unstable} or \emph{stable} (see \cref{fig:taskvalue}).
368 Once a task yields a stable value, it does not change anymore.
369 The most rudimentary non-interactive basic tasks in the task language of \gls{MTASK} are \cleaninline{rtrn} and \cleaninline{unstable}.
370 They lift the value from the \gls{MTASK} expression language to the task domain either as a stable or unstable value.
371 There is also a special type of basic task for delaying execution.
372 The \cleaninline{delay} task---parametrised by a number of milliseconds---yields an unstable value while the time has not passed.
373 Once the specified time has passed, the time it overshot the planned time is yielded as a stable task value.
374 See \cref{sec:repeat} for an example task using \cleaninline{delay}.
375
376 \begin{lstClean}[label={lst:basic_tasks},caption={Non-interactive basic tasks in \gls{MTASK}.}]
377 class rtrn v :: (v t) -> MTask v t
378 class unstable v :: (v t) -> MTask v t
379 class delay v :: (v n) -> MTask v n | long v n
380 \end{lstClean}
381
382 \subsubsection{Peripherals}\label{sssec:peripherals}
383 In order for the edge device to interact with the environment, peripherals such as sensors and actuators are employed.
384 Some peripherals are available on the microcontroller package, others are connected with wires using protocols such as \gls{I2C}.
385 For every supported sensor or actuator, basic tasks are available that allow interaction with the specific peripheral.
386 The type classes for these tasks are not included in the \cleaninline{mtask} class collection as not all devices nor all language interpretations support every peripheral connected.
387
388 An example of a built-in peripheral is the \gls{GPIO} system.
389 This array of digital and analogue pins is controlled through software.
390 \Gls{GPIO} access is divided into three classes: analogue \gls{IO}, digital \gls{IO} and pin mode configuration (see \cref{lst:gpio}).
391 For all pins and pin modes, an \gls{ADT} is available that enumerates the pins.
392 The analogue \gls{GPIO} pins of a microcontroller are connected to an \gls{ADC} that translates the measured voltage to an integer.
393 Digital \gls{GPIO} pins of a microcontroller report either a high or a low value.
394 Both analogue and digital \gls{GPIO} pins can be read or written to, but it is advised to set the pin mode accordingly.
395 The \cleaninline{pin} type class allows functions to be overloaded in either the analogue or digital pins, e.g.\ analogue pins can be considered digital pins as well.
396
397 For digital \gls{GPIO} interaction, the \cleaninline{dio} type class is used.
398 The first argument of the functions in this class is overloaded, i.e.\ it accepts either an \cleaninline{APin} or a \cleaninline{DPin}.
399 Analogue \gls{GPIO} tasks are bundled in the \cleaninline{aio} type class.
400 \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.
401 This setting can be set using the \cleaninline{pinMode} class by hand or by using the \cleaninline{declarePin} \gls{GPIO} pin constructor to declare it at the top level.
402 Setting the pin mode is a task that immediately finishes and yields a stable unit value.
403 Writing to a pin is also a task that immediately finishes, but yields the written value.
404 Reading a pin is a task that yields an unstable value---i.e.\ the value read from the actual pin.
405
406 \begin{lstClean}[label={lst:gpio},caption={The \gls{MTASK} interface for \gls{GPIO} access.}]
407 :: APin = A0 | A1 | A2 | A3 | A4 | A5
408 :: DPin = D0 | D1 | D2 | D3 | D4 | D5 | D6 | D7 | D8 | D9 | D10 | ...
409 :: PinMode = PMInput | PMOutput | PMInputPullup
410 :: Pin = AnalogPin APin | DigitalPin DPin
411
412 class pin p :: p -> Pin
413 instance pin APin, DPin
414
415 class aio v where
416 writeA :: (v APin) (v Int) -> MTask v Int
417 readA :: (v APin) -> MTask v Int
418
419 class dio p v | pin p where
420 writeD :: (v p) (v Bool) -> MTask v Bool
421 readD :: (v p) -> MTask v Bool | pin p
422
423 class pinMode v where
424 pinMode :: (v PinMode) (v p) -> MTask v () | pin p
425 declarePin :: p PinMode ((v p) -> Main (v a)) -> Main (v a) | pin p
426 \end{lstClean}
427
428 \Cref{lst:gpio_examples} shows two examples of \gls{MTASK} tasks using \gls{GPIO} pins.
429 \cleaninline{task1} reads analogue \gls{GPIO} pin 3.
430 This is a task that never terminates.
431 \cleaninline{task2} writes the \cleaninline{true} (\gls{ARDUINO} \arduinoinline{HIGH}) value to digital \gls{GPIO} pin 3.
432 This task finishes immediately after writing to the pin.
433
434 \begin{lstClean}[label={lst:gpio_examples},caption={\Gls{GPIO} example in \gls{MTASK}.}]
435 task1 :: MTask v Int | mtask v
436 task1 = declarePin A3 PMInput \a3->{main=readA a3}
437
438 task2 :: MTask v Int | mtask v
439 task2 = declarePin D3 PMOutput \d3->{main=writeD d3 true}
440 \end{lstClean}
441
442 Peripherals are bundled by their functionality in \gls{MTASK}.
443 For example, \cref{lst:dht} shows the type classes for all supported \gls{DHT} sensors.
444 Currently, two different types of \gls{DHT} sensors are supported, the \emph{DHT} family of sensors connect through the \gls{ONEWIRE} protocol and the \emph{SHT} family of sensors connected using the \gls{I2C} protocol.
445 Creating such a \cleaninline{DHT} object is very similar to creating functions in \gls{MTASK} and uses \gls{HOAS} to make it type safe.
446 When provided a configuration and a configuration function, the \gls{DHT} object can be brought into scope.
447 For the \gls{DHT} sensor there are two basic tasks, \cleaninline{temperature} and \cleaninline{humidity}, that produce a task that yields the observed temperature in \unit{\celcius} or the relative humidity as an unstable value.
448 Other peripherals have similar interfaces, they are available in \cref{sec:aux_peripherals}.
449
450 \begin{lstClean}[float=,label={lst:dht},caption={The \gls{MTASK} interface for \glspl{DHT} sensors.}]
451 :: DHT //abstract
452 :: DHTInfo
453 = DHT_DHT Pin DHTtype
454 | DHT_SHT I2CAddr
455 :: DHTtype = DHT11 | DHT21 | DHT22
456 class dht v where
457 DHT :: DHTInfo ((v DHT) -> Main (v b)) -> Main (v b) | type b
458 temperature :: (v DHT) -> MTask v Real
459 humidity :: (v DHT) -> MTask v Real
460
461 measureTemp :: Main (MTask v Real) | mtask, dht v
462 measureTemp = DHT (DHT_SHT (i2c 0x36)) \dht->{main=temperature dht}
463 \end{lstClean}
464
465 \subsection{Task combinators}
466 Task combinators are used to combine multiple tasks to describe workflows.
467 The \gls{MTASK} language has a set of simpler combinators from which more complicated workflow can be derived.
468 There are three main types of task combinators, namely:
469 \begin{itemize}
470 \item sequential combinators that execute tasks one after the other, possibly using the result of the left-hand side;
471 \item parallel combinators that execute tasks at the same time, combining the result;
472 \item and miscellaneous combinators that change the semantics of a task---for example a combinator that repeats the child task.
473 \end{itemize}
474
475 \subsubsection{Sequential}
476 Sequential task combination allows the right-hand side expression to \emph{observe} the left-hand side task value.
477 All sequential task combinators are defined in the \cleaninline{step} class and are by default defined in terms of the Swiss Army knife step combinator (\cleaninline{>>*.}, \cref{lst:mtask_sequential}).
478 This combinator has a single task on the left-hand side and a list of \emph{task continuations} on the right-hand side.
479 Every rewrite step, the list of task continuations are tested on the task value.
480 If one of the predicates matches, the task continues with the result of these continuations.
481 Several shorthand combinators are derived from the step combinator.
482 The \cleaninline{>>=.} combinator 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.
483 The \cleaninline{>>\|.} combinator is a shorthand for the sequence operation, if the left-hand side is stable, it continues with the right-hand side task.
484 The \cleaninline{>>~.} and \cleaninline{>>..} combinators are variants of the ones above that ignore the stability and continue on an unstable value as well.
485
486 \begin{lstClean}[label={lst:mtask_sequential},caption={Sequential task combinators in \gls{MTASK}.}]
487 class step v | expr v where
488 (>>*.) infixl 1 :: (MTask v t) [Step v t u] -> MTask v u
489 (>>=.) infixl 0 :: (MTask v t) ((v t) -> MTask v u) -> MTask v u
490 (>>|.) infixl 0 :: (MTask v t) (MTask v u) -> MTask v u
491 (>>~.) infixl 0 :: (MTask v t) ((v t) -> MTask v u) -> MTask v u
492 (>>..) infixl 0 :: (MTask v t) (MTask v u) -> MTask v u
493
494 :: Step v t u
495 = IfValue ((v t) -> v Bool) ((v t) -> MTask v u)
496 | IfStable ((v t) -> v Bool) ((v t) -> MTask v u)
497 | IfUnstable ((v t) -> v Bool) ((v t) -> MTask v u)
498 | Always (MTask v u)
499 \end{lstClean}
500
501 \Cref{lst:mtask_readpinbin} shows an example task containing a step.
502 The \cleaninline{readPinBin} function produces an \gls{MTASK} task that classifies the value of an analogue pin into four bins.
503 It also shows that the nature of embedding allows the host language to be used as a macro language.
504
505 \begin{lstClean}[label={lst:mtask_readpinbin},caption={Read an analogue pin and bin the value in \gls{MTASK}.}]
506 readPinBin :: Int -> Main (MTask v Int) | mtask v
507 readPinBin lim = declarePin PMInput A2 \a2->
508 { main = readA a2 >>*.
509 [ IfValue (\x->x <. lim) (\_->rtrn (lit bin))
510 \\ lim <- [64,128,192,256]
511 & bin <- [0..]]}
512 \end{lstClean}
513
514 \subsubsection{Parallel}\label{sssec:combinators_parallel}
515 The result of a parallel task combination is a compound task that executes both tasks at the same time.
516 There are two types of parallel task combinators in the \gls{MTASK} language (see \cref{lst:mtask_parallel}).
517
518 \begin{lstClean}[label={lst:mtask_parallel},caption={Parallel task combinators in \gls{MTASK}.}]
519 class (.&&.) infixr 4 v :: (MTask v a) (MTask v b) -> MTask v (a, b)
520 class (.||.) infixr 3 v :: (MTask v a) (MTask v a) -> MTask v a
521 \end{lstClean}
522
523 The conjunction combinator (\cleaninline{.&&.}) combines the result by putting the values from both sides in a tuple.
524 The stability of the task depends on the stability of both children.
525 If both children are stable, the result is stable, otherwise the result is unstable.
526 The disjunction combinator (\cleaninline{.\|\|.}) combines the results by picking the leftmost, most stable task.
527 The semantics of both parallel combinators are most easily described using the \gls{CLEAN} functions shown in \cref{lst:semantics_con,lst:semantics_dis}.
528
529 \begin{figure}
530 \centering
531 \begin{subfigure}[t]{.5\textwidth}
532 \begin{lstClean}[caption={Semantics of the\\conjunction combinator.},label={lst:semantics_con}]
533 con :: (TaskValue a) (TaskValue b)
534 -> TaskValue (a, b)
535 con NoValue r = NoValue
536 con l NoValue = NoValue
537 con (Value l ls) (Value r rs)
538 = Value (l, r) (ls && rs)
539
540 \end{lstClean}
541 \end{subfigure}%
542 \begin{subfigure}[t]{.5\textwidth}
543 \begin{lstClean}[caption={Semantics of the\\disjunction combinator.},label={lst:semantics_dis}]
544 dis :: (TaskValue a) (TaskValue a)
545 -> TaskValue a
546 dis NoValue r = r
547 dis l NoValue = l
548 dis (Value l ls) (Value r rs)
549 | rs && not ls = Value r rs
550 | otherwise = Value l ls
551 \end{lstClean}
552 \end{subfigure}
553 \end{figure}
554
555 \Cref{lst:mtask_parallel_example} gives an example program that uses the parallel task combinator.
556 This task read two pins at the same time, returning when one of the pins becomes high.
557 If the combinator was the \cleaninline{.&&.}, the type would be \cleaninline{MTask v (Bool, Bool)} and the task would only return when both pins are high but not necessarily at the same time.
558
559 \begin{lstClean}[float=,label={lst:mtask_parallel_example},caption={Parallel task combinator example in \gls{MTASK}.}]
560 task :: MTask v Bool
561 task =
562 declarePin D0 PMInput \d0->
563 declarePin D1 PMInput \d1->
564 fun \monitor = (\pin->readD pin >>*. [IfValue id rtrn])
565 In {main = monitor d0 .||. monitor d1}
566 \end{lstClean}
567
568 \subsubsection{Repeat}\label{sec:repeat}
569 In many workflows, tasks are to be executed repeatedly.
570 The \cleaninline{rpeat} combinator does this by executing the child task until it becomes stable.
571 Once a stable value is observed, the task is reinstated.
572 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 from the blink example from \cref{chp:top4iot}.
573
574 \begin{lstClean}[label={lst:mtask_repeat},caption={Repeat task combinators in \gls{MTASK}.}]
575 class rpeat v where
576 rpeat :: (MTask v a) -> MTask v a
577 \end{lstClean}
578
579 \Cref{lst:mtask_repeat_example} shows an example of a task that uses the \cleaninline{rpeat} combinator.
580 This resulting task mirrors the value read from analogue \gls{GPIO} pin \cleaninline{A1} to pin \cleaninline{A2} by constantly reading the pin and writing the result.
581
582 \begin{lstClean}[label={lst:mtask_repeat_example},caption={Repeat task combinator example in \gls{MTASK}.}]
583 task :: MTask v Int | mtask v
584 task = declarePin A1 PMInput \a1->
585 declarePin A2 PMOutput \a2->
586 {main = rpeat (readA a1 >>~. writeA a2 >>|. delay (lit 1000))}
587 \end{lstClean}
588
589 \subsection{Shared data sources}
590 For some collaborations it is cumbersome to only communicate data using task values.
591 \Glspl{SDS} are a safe abstraction over any data that fill this gap.
592 It allows tasks to safely and atomically read, write and update data stores in order to share data with other tasks.
593 \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}).
594 There are no combinators or user-defined \gls{SDS} types in \gls{MTASK} as there are in \gls{ITASK}.
595 Similar to peripherals and functions, \glspl{SDS} are defined at the top level with the \cleaninline{sds} function.
596 They are accessed through interaction tasks.
597 The \cleaninline{getSds} task yields the current value of the \gls{SDS} as an unstable value.
598 This behaviour is similar to the \cleaninline{watch} task in \gls{ITASK}.
599 Writing a new value to \pgls{SDS} is done using \cleaninline{setSds}.
600 This task yields the written value as a stable result after it is done writing.
601 Getting and immediately setting \pgls{SDS} is not necessarily an \emph{atomic} operation in \gls{MTASK} because it is possible that another task accesses the \gls{SDS} in between.
602 To circumvent this issue, \cleaninline{updSds} is available by which \pgls{SDS} can be atomically updated.
603 The \cleaninline{updSds} task only guarantees atomicity within \gls{MTASK}.
604
605 \begin{lstClean}[label={lst:mtask_sds},caption={\Glspl{SDS} in \gls{MTASK}.}]
606 :: Sds a // abstract
607 class sds v where
608 sds :: ((v (Sds t)) -> In t (Main (MTask v u))) -> Main (MTask v u)
609 getSds :: (v (Sds t)) -> MTask v t
610 setSds :: (v (Sds t)) (v t) -> MTask v t
611 updSds :: (v (Sds t)) ((v t) -> v t) -> MTask v t
612 \end{lstClean}
613
614 \Cref{lst:mtask_sds_examples} shows an example task that uses \glspl{SDS}.
615 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}.
616 In the \cleaninline{main} expression, this function is called twice with a different argument.
617 The results are combined using the parallel disjunction combinator (\cleaninline{.\|\|.}).
618 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.
619
620 \begin{lstClean}[label={lst:mtask_sds_examples},caption={Examples with \glspl{SDS} in \gls{MTASK}.}]
621 task :: MTask v Int | mtask v
622 task =
623 declarePin D3 PMInput \d3->
624 declarePin D5 PMInput \d5->
625 sds \share=0
626 In fun \count=(\pin->
627 readD pin
628 >>* [IfValue id (\_->updSds (\x->x +. lit 1) share)]
629 >>| delay (lit 100) // debounce
630 >>| count pin)
631 In {main=count d3 .||. count d5}
632 \end{lstClean}
633
634 \section{Interpretations}
635 The nature of the \gls{MTASK} \gls{DSL} embedding allows for multiple interpretations of the terms in the language.
636 The \gls{MTASK} language has interpretations to pretty print, simulate, and generate byte code for terms in the language.
637 There are many other interpretations possible such as static analyses or optimisation.
638 Not all these interpretations are necessarily \gls{TOP} engines, i.e.\ not all the interpretations execute the resulting tasks.
639
640 \subsection{Pretty printer}
641 The pretty printer interpretation converts an \gls{MTASK} term to a string representation.
642 As the host language \gls{CLEAN} constructs the \gls{MTASK} expressions at run time, it can be useful to show the constructed expression at run time as well.
643 The only function exposed for this interpretation is the \cleaninline{showMain} function (\cref{lst:showmain}).
644 It runs the pretty printer and returns a list of strings containing the pretty printed result.
645 The pretty printing function does the best it can but obviously cannot reproduce layout, curried functions, and variable names.
646 This shortcoming is illustrated by printing a blink task that contains a function and currying in \cref{lst:showexample}.
647 The output of this action would be \cleaninline{fun f0 a1 = writeD(D13, a1) >>= \\a2.(delay 1000) >>\| (f0 (Not a1)) in (f0 True)}
648
649 \begin{lstClean}[caption={The entry point for the pretty printing interpretation.},label={lst:showmain}]
650 :: Show a // from the mTask pretty printing library
651 showMain :: (Main (Show a)) -> [String]
652 \end{lstClean}
653
654 \begin{lstClean}[caption={Pretty printing interpretation example.},label={lst:showexample}]
655 blinkTask :: Main (MTask v Bool) | mtask v
656 blinkTask =
657 fun \blink=(\state->
658 writeD d13 state >>|. delay (lit 500) >>=. blink o Not
659 ) In {main = blink true}
660 \end{lstClean}
661
662 \subsection{Simulator}
663 In a real microprocessor, it is hard to observe the state and to control the sensors in such a way that the behaviour of interest can be observed.
664 The simulator converts the expression to a ready-for-work \gls{ITASK} simulation to bridge this gap.
665 There is one entry point for this interpretation (see \cref{lst:simulatemain}).
666 The task resulting from the \cleaninline{simulate} function presents the user with an interactive simulation environment (see \cref{fig:sim}).
667 The simulation allows the user to (partially) execute tasks, control the simulated peripherals, inspect the internal state of the tasks, and interact with \glspl{SDS}.
668
669 \begin{lstClean}[caption={The entry point for the simulation interpretation.},label={lst:simulatemain}]
670 :: TraceTask a // from the mTask simulator library
671 simulate :: (Main (TraceTask a)) -> [String]
672 \end{lstClean}
673
674 \begin{figure}
675 \centering
676 \includegraphics[width=\linewidth]{simg}
677 \caption{Simulator interface for a blink program written in \gls{MTASK}.}\label{fig:sim}
678 \end{figure}
679
680 \subsection{Byte code compiler}
681 The main interpretation of the \gls{MTASK} system is the byte code compiler (\cleaninline{:: BCInterpret a}).
682 This interpretation compiles the \gls{MTASK} term at run time to byte code.
683 With it, and a handful of integration functions, \gls{MTASK} tasks can be executed on microcontrollers and integrated in \gls{ITASK} as if they were regular \gls{ITASK} tasks.
684 Furthermore, with a special language construct, \glspl{SDS} can be shared between \gls{MTASK} and \gls{ITASK} programs as well.
685 The integration with \gls{ITASK} is explained thoroughly later in \cref{chp:integration_with_itask}.
686
687 The \gls{MTASK} language together with \gls{ITASK} is a heterogeneous \gls{DSL}.
688 I.e.\ some components---for example the \gls{RTS} on the microcontroller that executes the tasks---is largely unaware of the other components in the system, and it is executed on a completely different architecture.
689 The \gls{MTASK} language is a \gls{TOP} language with basic tasks tailored for \gls{IOT} edge devices (see \cref{sec:top}).
690 It uses expressions based a simply-typed $\lambda$-calculus with support for some basic types, arithmetic operations, and function definitions.
691
692 \section{Conclusion}
693 This chapter gave an overview of the complete \gls{MTASK} \gls{DSL}.
694 The \gls{MTASK} language is a rich \gls{TOP} language tailored for \gls{IOT} edge devices.
695 The language is implemented as a class-based shallowly embedded \gls{DSL} in the pure functional host language \gls{CLEAN}.
696 The language uses an enriched lambda calculus as a host language, providing additional language constructs for arithmetic expressions, conditionals, functions, but also non-interactive basic tasks, task combinators, peripheral support, and integration with \gls{ITASK}.
697 Terms in the language are just interfaces and can be interpreted by one or more interpretations.
698 When using the byte code compiler, terms in the \gls{MTASK} language are type checked at compile time but are constructed and compiled at run time.
699 This facilitates tailor-making tasks for the current work requirements.
700
701 \input{subfilepostamble}
702 \end{document}