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