2baed8b341156fd5b6a14bd3b6908e694e3421f4
[phd-thesis.git] / top / lang.tex
1 \documentclass[../thesis.tex]{subfiles}
2
3 \input{subfilepreamble}
4
5 \begin{document}
6 \input{subfileprefix}
7
8 \chapter{The \texorpdfstring{\gls{MTASK}}{mTask} \texorpdfstring{\glsxtrshort{DSL}}{DSL}}%
9 \label{chp:mtask_dsl}
10 \begin{chapterabstract}
11 This chapter introduces the \gls{MTASK} language more technically by:
12 \begin{itemize}
13 \item introducing the setup of the \gls{EDSL};
14 \item and showing the language interface and examples for:
15 \begin{itemize}
16 \item data types
17 \item expression
18 \item task and their combinators.
19 \end{itemize}
20 \end{itemize}
21 \end{chapterabstract}
22
23 The \gls{MTASK} system is a complete \gls{TOP} programming environment for programming microcontrollers, i.e.\ it contains a \gls{TOP} language and a \gls{TOP} engine.
24 It is implemented as an \gls{EDSL} in \gls{CLEAN} using class-based---or tagless-final---embedding (see \cref{sec:tagless-final_embedding}).
25 Due to the nature of the embedding technique, it is possible to have multiple interpretations for programs written in the \gls{MTASK} language.
26 The following interpretations are available for \gls{MTASK}.
27
28 \begin{description}
29 \item[Pretty printer]
30
31 This interpretation converts the expression to a string representation.
32 \item[Simulator]
33
34 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.
35 \item[Byte code compiler]
36
37 The compiler compiles the \gls{MTASK} program at runtime to a specialised byte code.
38 Using a handful of integration functions and tasks, \gls{MTASK} tasks can be executed on microcontrollers and integrated in \gls{ITASK} as if they were regular \gls{ITASK} tasks.
39 Furthermore, with special language constructs, \glspl{SDS} can be shared between \gls{MTASK} and \gls{ITASK} programs.
40 \end{description}
41
42 When using the compiler interpretation in conjunction with the \gls{ITASK} integration, \gls{MTASK} is a heterogeneous \gls{DSL}.
43 I.e.\ some components---e.g.\ the \gls{RTS} on the microcontroller---is largely unaware of the other components in the system, and it is executed on a completely different architecture.
44 The \gls{MTASK} language is an enriched simply-typed $\lambda$-calculus with support for some basic types, arithmetic operations, and function definition; and a task language (see \cref{sec:top}).
45
46 \section{Types}
47 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.
48 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 therefore added to the \gls{DSL} functions.
49 The most used class constraint is the \cleaninline{type} class collection containing functions for serialization, printing, \gls{ITASK} constraints, \etc.
50 Many of these functions can be derived using generic programming.
51 An even stronger restriction on types is defined for types that have a stack representation.
52 This \cleaninline{basicType} class has instances for many \gls{CLEAN} basic types such as \cleaninline{Int}, \cleaninline{Real} and \cleaninline{Bool}.
53 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.
54
55 \begin{table}[ht]
56 \centering
57 \caption{Mapping from \gls{CLEAN}/\gls{MTASK} data types to \gls{CPP} datatypes.}%
58 \label{tbl:mtask-c-datatypes}
59 \begin{tabular}{lll}
60 \toprule
61 \gls{CLEAN}/\gls{MTASK} & \gls{CPP} type & \textnumero{}bits\\
62 \midrule
63 \cleaninline{Bool} & \cinline{bool} & 16\\
64 \cleaninline{Char} & \cinline{char} & 16\\
65 \cleaninline{Int} & \cinline{int16_t} & 16\\
66 \cleaninline{:: Long} & \cinline{int32_t} & 32\\
67 \cleaninline{Real} & \cinline{float} & 32\\
68 \cleaninline{:: T = A \| B \| C} & \cinline{enum} & 16\\
69 \bottomrule
70 \end{tabular}
71 \end{table}
72
73 \Cref{lst:constraints} contains the definitions for the auxiliary types and type constraints (such as \cleaninline{type} an \cleaninline{basicType}) that are used to construct \gls{MTASK} expressions.
74 The \gls{MTASK} language interface consists of a core collection of type classes bundled in the type class \cleaninline{class mtask}.
75 Every interpretation implements the type classes in the \cleaninline{mtask} class
76 There are also \gls{MTASK} extensions that not every interpretation implements such as peripherals and \gls{ITASK} integration.
77 \begin{lstClean}[caption={Classes and class collections for the \gls{MTASK} language.},label={lst:constraints}]
78 class type t | iTask, ... ,fromByteCode, toByteCode t
79 class basicType t | type t where ...
80
81 class mtask v | expr, ..., int, real, long v
82
83 \end{lstClean}
84
85 Sensors, \glspl{SDS}, functions, \etc{} may only be defined at the top level.
86 The \cleaninline{Main} type is used that is used to distinguish the top level from the main expression.
87 Some top level definitions, such as functions, are defined using \gls{HOAS}.
88 To make their syntax friendlier, the \cleaninline{In} type---an infix tuple---is used to combine these top level definitions as can be seen in \cleaninline{someTask} (\cref{lst:mtask_types}).
89
90 \begin{lstClean}[caption={Example task and auxiliary types in the \gls{MTASK} language.},label={lst:mtask_types}]
91 :: Main a = { main :: a }
92 :: In a b = (In) infix 0 a b
93
94 someTask :: MTask v Int | mtask v & liftsds v & sensor1 v & ...
95 someTask =
96 sensor1 config1 \sns1->
97 sensor2 config2 \sns2->
98 sds \s1=initial
99 In liftsds \s2=someiTaskSDS
100 In fun \fun1= ( ... )
101 In fun \fun2= ( ... )
102 In { main = mainexpr }
103 \end{lstClean}
104
105 \section{Expressions}\label{sec:expressions}
106 \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.
107 For every common boolean and 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.
108
109 \begin{lstClean}[caption={The \gls{MTASK} class for expressions},label={lst:expressions}]
110 class expr v where
111 lit :: t -> v t | type t
112 (+.) infixl 6 :: (v t) (v t) -> v t | basicType, +, zero t
113 ...
114 (&.) infixr 3 :: (v Bool) (v Bool) -> v Bool
115 (|.) infixr 2 :: (v Bool) (v Bool) -> v Bool
116 Not :: (v Bool) -> v Bool
117 (==.) infix 4 :: (v a) (v a) -> v Bool | Eq, basicType a
118 ...
119 If :: (v Bool) (v t) (v t) -> v t | type t
120 \end{lstClean}
121
122 Conversion to-and-fro data types is available through the overloaded functions \cleaninline{int}, \cleaninline{long} and \cleaninline{real} that will convert the argument to the respective type similar to casting in \gls{C}.
123
124 \begin{lstClean}[caption={Type conversion functions in \gls{MTASK}.}]
125 class int v a :: (v a) -> v Int
126 class real v a :: (v a) -> v Real
127 class long v a :: (v a) -> v Long
128 \end{lstClean}
129
130 Values from the host language must be explicitly lifted to the \gls{MTASK} language using the \cleaninline{lit} function.
131 For convenience, there are many lower-cased macro definitions for often used constants such as \cleaninline{true :== lit True}, \cleaninline{false :== lit False}, \etc.
132
133 \Cref{lst:example_exprs} shows some examples of these expressions.
134 Since they are only expressions, there is no need for a \cleaninline{Main}.
135 \cleaninline{e0} defines the literal $42$, \cleaninline{e1} calculates the literal $42.0$ using real numbers.
136 \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.
137
138 \begin{lstClean}[label={lst:example_exprs},caption={Example \gls{MTASK} expressions.}]
139 e0 :: v Int | expr v
140 e0 = lit 42
141
142 e1 :: v Real | expr v
143 e1 = lit 38.0 + real (lit 4)
144
145 e2 :: v Int | expr v
146 e2 = if' (e0 ==. int e1)
147 (int e1 /. lit 2) e0
148 \end{lstClean}
149
150 \Gls{MTASK} is shallowly embedded in \gls{CLEAN} and the terms are constructed at runtime.
151 This means that \gls{MTASK} programs can also be tailor-made at runtime or constructed using \gls{CLEAN} functions maximising the linguistic reuse \citep{krishnamurthi_linguistic_2001}
152 \cleaninline{approxEqual} in \cref{lst:example_macro} performs an approximate equality---albeit not taking into account all floating point pecularities---.
153 When calling \cleaninline{approxEqual} in an \gls{MTASK} function, the resulting code is inlined.
154
155 \begin{lstClean}[label={lst:example_macro},caption={Example linguistic reuse in the \gls{MTASK} language.}]
156 approxEqual :: (v Real) (v Real) (v Real) -> v Real | expr v
157 approxEqual x y eps = if' (x ==. y) true
158 ( if' (x >. y)
159 (y -. x < eps)
160 (x -. y < eps)
161 )
162 \end{lstClean}
163
164 \subsection{Data types}
165 Most of \gls{CLEAN}'s basic types have been mapped on \gls{MTASK} types.
166 However, it can be useful to have access to compound types as well.
167 All types in \gls{MTASK} must have a fixed size representation on the stack so sum types are not (yet) supported.
168 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}).
169 To be able to use types as first class citizens, constructors and field selectors are required (see \cref{chp:first-class_datatypes}).
170 \Cref{lst:tuple_exprs} shows the scaffolding for supporting tuples in \gls{MTASK}.
171 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.
172 Examples for using tuple can be found in \cref{sec:mtask_functions}.
173
174 \begin{lstClean}[label={lst:tuple_exprs},caption={Tuple constructor and field selectors in \gls{MTASK}.}]
175 class tupl v where
176 tupl :: (v a) (v b) -> v (a, b) | type a & type b
177 first :: (v (a, b)) -> v a | type a & type b
178 second :: (v (a, b)) -> v b | type a & type b
179
180 tupopen f :== \v->f (first v, second v)
181 \end{lstClean}
182
183 \subsection{Functions}\label{sec:mtask_functions}
184 Adding functions to the language is achieved by type class to the \gls{DSL}.
185 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}.
186 The \gls{MTASK} only allows first-order functions and does not allow partial function application.
187 This is restricted by using a multi-parameter type class where the first parameter represents the arguments and the second parameter the view.
188 By providing a single instance per function arity instead of providing one instance for all functions and using tuples for the arguments this constraint can be enforced.
189 Also, \gls{MTASK} only supports top-level functions which is enforced by the \cleaninline{Main} box.
190 The definition of the type class and the instances for an example interpretation (\cleaninline{:: Inter}) are as follows:
191
192 \begin{lstClean}[caption={Functions in \gls{MTASK}.}]
193 class fun a v :: ((a -> v s) -> In (a -> v s) (Main (MTask v u)))
194 -> Main (MTask v u)
195
196 instance fun () Inter where ...
197 instance fun (Inter a) Inter | type a where ...
198 instance fun (Inter a, Inter b) Inter | type a, type b where ...
199 instance fun (Inter a, Inter b, Inter c) Inter | type a, ... where ...
200 ...
201 \end{lstClean}
202
203 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}.
204 \Cref{lst:function_examples} show the factorial function, a tail-call optimised factorial function and a function with zero arguments to demonstrate the syntax.
205 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.
206 Many of the often used functions are already bundled in the \cleaninline{mtask} class constraint collection.
207 \cleaninline{factorialtail} shows a manually added class constraint.
208 Definiting zero arity functions is shown in the \cleaninline{zeroarity} expression.
209 Finally, \cleaninline{swapTuple} shows an example of a tuple being swapped.
210
211 % VimTeX: SynIgnore on
212 \begin{lstClean}[label={lst:function_examples},caption={Function examples in \gls{MTASK}.}]
213 factorial :: Main (v Int) | mtask v
214 factorial =
215 fun \fac=(\i->if' (i <. lit 1)
216 (lit 1)
217 (i *. fac (i -. lit 1)))
218 In {main = fac (lit 5) }
219
220 factorialtail :: Main (v Int) | mtask v & fun (v Int, v Int) v
221 factorialtail =
222 fun \facacc=(\(acc, i)->if' (i <. lit 1)
223 acc
224 (fac (acc *. i, i -. lit 1)))
225 In fun \fac=(\i->facacc (lit 1, i))
226 In {main = fac (lit 5) }
227
228 zeroarity :: Main (v Int) | mtask v
229 zeroarity =
230 fun \fourtytwo=(\()->lit 42)
231 In fun \add=(\(x, y)->x +. y)
232 In {main = add (fourtytwo (), lit 9)}
233
234 swapTuple :: Main (v (Int, Bool)) | mtask v
235 swapTuple =
236 fun \swap=(tupopen \(x, y)->tupl y x)
237 In {main = swap (tupl true (lit 42)) }
238 \end{lstClean}
239 % VimTeX: SynIgnore off
240
241 \section{Tasks and task combinators}\label{sec:top}
242 \Gls{MTASK}'s task language can be divided into three categories, namely
243 \begin{enumerate*}
244 \item Basic tasks, in most \gls{TOP} systems, the basic tasks are called editors, modelling the interactivity with the user.
245 In \gls{MTASK}, there are no \emph{editors} in that sense but there is interaction with the outside world through microcontroller peripherals such as sensors and actuators.
246 \item Task combinators provide a way of describing the workflow.
247 They combine one or more tasks into a compound task.
248 \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.
249 \end{enumerate*}
250
251 As \gls{MTASK} is integrated with \gls{ITASK}, the same stability distinction is made for task values.
252 A task in \gls{MTASK} is denoted by the \gls{DSL} type synonym shown in \cref{lst:task_type}.
253
254 \begin{lstClean}[label={lst:task_type},caption={Task type in \gls{MTASK}.}]
255 :: MTask v a :== v (TaskValue a)
256 :: TaskValue a
257 = NoValue
258 | Value a Bool
259 \end{lstClean}
260
261 \subsection{Basic tasks}
262 The most rudimentary basic tasks are the \cleaninline{rtrn} and \cleaninline{unstable} tasks.
263 They lift the value from the \gls{MTASK} expression language to the task domain either as a stable value or an unstable value.
264 There is also a special type of basic task for delaying execution.
265 The \cleaninline{delay} task---given a number of milliseconds---yields an unstable value while the time has not passed.
266 Once the specified time has passed, the time it overshot the planned time is yielded as a stable task value.
267 See \cref{sec:repeat} for an example task using \cleaninline{delay}.
268
269 \begin{lstClean}[label={lst:basic_tasks},caption={Function examples in \gls{MTASK}.}]
270 class rtrn v :: (v t) -> MTask v t
271 class unstable v :: (v t) -> MTask v t
272 class delay v :: (v n) -> MTask v n | long v n
273 \end{lstClean}
274
275 \subsubsection{Peripherals}\label{sssec:peripherals}
276 For every sensor or actuator, basic tasks are available that allow interaction with the specific peripheral.
277 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.
278 %\todo{Historically, peripheral support has been added \emph{by need}.}
279
280 \Cref{lst:dht,lst:gpio} show the type classes for \glspl{DHT} sensors and \gls{GPIO} access.
281 Other peripherals have similar interfaces, they are available in the \cref{sec:aux_peripherals}.
282 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.
283 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.
284 Creating such a \cleaninline{DHT} object is very similar to creating functions in \gls{MTASK} and uses \gls{HOAS} to make it type safe.
285
286 \begin{lstClean}[label={lst:dht},caption{The \gls{MTASK} interface for \glspl{DHT} sensors.}]
287 :: DHT //abstract
288 :: DHTInfo
289 = DHT_DHT Pin DHTtype
290 | DHT_SHT I2CAddr
291 :: DHTtype = DHT11 | DHT21 | DHT22
292 class dht v where
293 DHT :: DHTInfo ((v DHT) -> Main (v b)) -> Main (v b) | type b
294 temperature :: (v DHT) -> MTask v Real
295 humidity :: (v DHT) -> MTask v Real
296
297 measureTemp :: Main (MTask v Real) | mtask v & dht v
298 measureTemp = DHT (DHT_SHT (i2c 0x36)) \dht->
299 {main=temperature dht}
300 \end{lstClean}
301
302 \Gls{GPIO} access is divided into three classes: analog, digital and pin modes.
303 For all pins and pin modes an \gls{ADT} is available that enumerates the pins.
304 The analog \gls{GPIO} pins of a microcontroller are connected to an \gls{ADC} that translates the voltage to an integer.
305 Analog \gls{GPIO} pins can be either read or written to.
306 Digital \gls{GPIO} pins only report a high or a low value.
307 The type class definition is a bit more complex since analog \gls{GPIO} pins can be used as digital \gls{GPIO} pins as well.
308 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.
309 \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.
310 This setting can be applied using the \cleaninline{pinMode} class by hand or by using the \cleaninline{declarePin} \gls{GPIO} pin constructor.
311 Setting the pin mode is a task that immediately finisheds and fields a stable unit value.
312 Writing to a pin is also a task that immediately finishes but yields the written value instead.
313 Reading a pin is a task that yields an unstable value---i.e.\ the value read from the actual pin.
314
315 \begin{lstClean}[label={lst:gpio},caption={The \gls{MTASK} interface for \gls{GPIO} access.}]
316 :: APin = A0 | A1 | A2 | A3 | A4 | A5
317 :: DPin = D0 | D1 | D2 | D3 | D4 | D5 | D6 | D7 | D8 | D9 | D10 | D11 | D12 | D13
318 :: PinMode = PMInput | PMOutput | PMInputPullup
319 :: Pin = AnalogPin APin | DigitalPin DPin
320 class pin p :: p -> Pin
321
322 class aio v where
323 writeA :: (v APin) (v Int) -> MTask v Int
324 readA :: (v APin) -> MTask v Int
325
326 class dio p v | pin p where
327 writeD :: (v p) (v Bool) -> MTask v Bool
328 readD :: (v p) -> MTask v Bool | pin p
329
330 class pinMode v where
331 pinMode :: (v PinMode) (v p) -> MTask v () | pin p
332 declarePin :: p PinMode ((v p) -> Main (v a)) -> Main (v a) | pin p
333 \end{lstClean}
334
335 \begin{lstClean}[label={lst:gpio_examples},caption={\Gls{GPIO} example in \gls{MTASK}.}]
336 task1 :: MTask v Int | mtask v
337 task1 = declarePin A3 PMInput \a3->{main=readA a3}
338
339 task2 :: MTask v Int | mtask v
340 task2 = declarePin D3 PMOutput \d3->{main=writeD d3 true}
341 \end{lstClean}
342
343 \subsection{Task combinators}
344 Task combinators are used to combine multiple tasks into one to describe workflows.
345 There are three main types of task combinators, namely:
346 \begin{enumerate*}
347 \item Sequential combinators that execute tasks one after the other, possibly using the result of the left hand side.
348 \item Parallel combinators that execute tasks at the same time combining the result.
349 \item Miscellaneous combinators that change the semantics of a task---e.g.\ repeat it or delay execution.
350 \end{enumerate*}
351
352 \subsubsection{Sequential}
353 Sequential task combination allows the right-hand side task to observe the left-hand side task value.
354 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{>>*.}.
355 This combinator has a single task on the left-hand side and a list of \emph{task continuations} on the right-hand side.
356 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.
357 \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.
358 \cleaninline{>>|.} is a shorthand for the sequence operation, if the left-hand side is stable, it continues with the right-hand side task.
359 The \cleaninline{>>~.} and \cleaninline{>>..} combinators are variants of the ones above that ignore the stability and continue on an unstable value as well.
360
361 \begin{lstClean}[label={lst:mtask_sequential},caption={Sequential task combinators in \gls{MTASK}.}]
362 class step v | expr v where
363 (>>*.) infixl 1 :: (MTask v t) [Step v t u] -> MTask v u
364 (>>=.) infixl 0 :: (MTask v t) ((v t) -> MTask v u) -> MTask v u
365 (>>|.) infixl 0 :: (MTask v t) (MTask v u) -> MTask v u
366 (>>~.) infixl 0 :: (MTask v t) ((v t) -> MTask v u) -> MTask v u
367 (>>..) infixl 0 :: (MTask v t) (MTask v u) -> MTask v u
368
369 :: Step v t u
370 = IfValue ((v t) -> v Bool) ((v t) -> MTask v u)
371 | IfStable ((v t) -> v Bool) ((v t) -> MTask v u)
372 | IfUnstable ((v t) -> v Bool) ((v t) -> MTask v u)
373 | Always (MTask v u)
374 \end{lstClean}
375
376 \todo{more examples step?}
377
378 The following listing shows an example of a step in action.
379 The \cleaninline{readPinBin} function produces an \gls{MTASK} task that classifies the value of an analogue pin into four bins.
380 It also shows that the nature of embedding allows the host language to be used as a macro language.
381 Furthermore
382
383 \begin{lstClean}[label={lst:mtask_readpinbin},caption={Read an analog pin and bin the value in \gls{MTASK}.}]
384 readPinBin :: Int -> Main (MTask v Int) | mtask v
385 readPinBin lim = declarePin PMInput A2 \a2->
386 { main = readA a2 >>*.
387 [ IfValue (\x->x <. lim) (\_->rtrn (lit bin))
388 \\ lim <-[64,128,192,256]
389 & bin <- [0..]]}
390 \end{lstClean}
391
392 \subsubsection{Parallel}\label{sssec:combinators_parallel}
393 The result of a parallel task combination is a compound that actually executes the tasks at the same time.
394
395 There are two types of parallel task combinators (see \cref{lst:mtask_parallel}).
396 The conjunction combinator (\cleaninline{.&&.}) combines the result by putting the values from both sides in a tuple.
397 The stability of the task depends on the stability of both children.
398 If both children are stable, the result is stable, otherwise the result is unstable.
399 The disjunction combinator (\cleaninline{.\|\|.}) combines the results by picking the leftmost, most stable task.
400 The semantics are easily described using \gls{CLEAN} functions shown in \cref{lst:semantics_con,lst:semantics_dis}.
401
402 \begin{figure}[ht]
403 \centering
404 \begin{subfigure}[t]{.5\textwidth}
405 \begin{lstClean}[caption={Semantics of the\\conjunction combinator.},label={lst:semantics_con}]
406 con :: (TaskValue a) (TaskValue b)
407 -> TaskValue (a, b)
408 con NoValue r = NoValue
409 con l NoValue = NoValue
410 con (Value l ls) (Value r rs)
411 = Value (l, r) (ls && rs)
412
413 \end{lstClean}
414 \end{subfigure}%
415 \begin{subfigure}[t]{.5\textwidth}
416 \begin{lstClean}[caption={Semantics of the\\disjunction combinator.},label={lst:semantics_dis}]
417 dis :: (TaskValue a) (TaskValue a)
418 -> TaskValue a
419 dis NoValue r = r
420 dis l NoValue = l
421 dis (Value l ls) (Value r rs)
422 | rs = Value r True
423 | otherwise = Value l ls
424 \end{lstClean}
425 \end{subfigure}
426 \end{figure}
427
428 \begin{lstClean}[label={lst:mtask_parallel},caption={Parallel task combinators in \gls{MTASK}.}]
429 class (.&&.) infixr 4 v :: (MTask v a) (MTask v b) -> MTask v (a, b)
430 class (.||.) infixr 3 v :: (MTask v a) (MTask v a) -> MTask v a
431 \end{lstClean}
432
433 \Cref{lst:mtask_parallel_example} gives an example of the parallel task combinator.
434 This program will read two pins at the same time, returning when one of the pins becomes \arduinoinline{HIGH}.
435 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.
436
437 \begin{lstClean}[label={lst:mtask_parallel_example},caption={Parallel task combinator example in \gls{MTASK}.}]
438 task :: MTask v Bool
439 task =
440 declarePin D0 PMInput \d0->
441 declarePin D1 PMInput \d1->
442 let monitor pin = readD pin >>*. [IfValue (\x->x) \x->rtrn x]
443 In {main = monitor d0 .||. monitor d1}
444 \end{lstClean}
445
446 \subsubsection{Repeat}\label{sec:repeat}
447 The \cleaninline{rpeat} combinator executes the child task.
448 If a stable value is observed, the task is reinstated.
449 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}.
450
451 \begin{lstClean}[label={lst:mtask_repeat},caption={Repeat task combinators in \gls{MTASK}.}]
452 class rpeat v where
453 rpeat :: (MTask v a) -> MTask v a
454 \end{lstClean}
455
456 To demonstrate the combinator, \cref{lst:mtask_repeat_example} show \cleaninline{rpeat} in use.
457 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.
458
459 \begin{lstClean}[label={lst:mtask_repeat_example},caption={Exemplatory repeat task in \gls{MTASK}.}]
460 task :: MTask v Int | mtask v
461 task =
462 declarePin A1 PMInput \a1->
463 declarePin A2 PMOutput \a2->
464 {main = rpeat (readA a1 >>~. writeA a2 >>|. delay (lit 1000))}
465 \end{lstClean}
466
467 \subsection{\texorpdfstring{\Glsxtrlongpl{SDS}}{Shared data sources}}
468 \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}).
469 Similar to peripherals (see \cref{sssec:peripherals}), they are constructed at the top level and are accessed through interaction tasks.
470 The \cleaninline{getSds} task yields the current value of the \gls{SDS} as an unstable value.
471 This behaviour is similar to the \cleaninline{watch} task in \gls{ITASK}.
472 Writing a new value to \pgls{SDS} is done using \cleaninline{setSds}.
473 This task yields the written value as a stable result after it is done writing.
474 Getting and immediately after 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.
475 To circumvent this issue, \cleaninline{updSds} is created, this task atomically updates the value of the \gls{SDS}.
476 The \cleaninline{updSds} task only guarantees atomicity within \gls{MTASK}.
477
478 \begin{lstClean}[label={lst:mtask_sds},caption={\Glspl{SDS} in \gls{MTASK}.}]
479 :: Sds a // abstract
480 class sds v where
481 sds :: ((v (Sds t)) -> In t (Main (MTask v u))) -> Main (MTask v u)
482 getSds :: (v (Sds t)) -> MTask v t
483 setSds :: (v (Sds t)) (v t) -> MTask v t
484 updSds :: (v (Sds t)) ((v t) -> v t) -> MTask v t
485 \end{lstClean}
486
487 \Cref{lst:mtask_sds_examples} shows an example using \glspl{SDS}.
488 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}.
489 In the \cleaninline{main} expression, this function is called twice and the results are combined using the parallel or combinator (\cleaninline{.||.}).
490 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}
491
492 \begin{lstClean}[label={lst:mtask_sds_examples},caption={Examples with \glspl{SDS} in \gls{MTASK}.}]
493 task :: MTask v Int | mtask v
494 task = declarePin D3 PMInput \d3->
495 declarePin D5 PMInput \d5->
496 sds \share=0
497 In fun \count=(\pin->
498 readD pin
499 >>* [IfValue (\x->x) (\_->updSds (\x->x +. lit 1) share)]
500 >>| delay (lit 100) // debounce
501 >>| count pin)
502 In {main=count d3 .||. count d5}
503 \end{lstClean}
504
505 \section{Conclusion}
506 \Gls{MTASK} is a rich \gls{TOP} language tailored for \gls{IOT} systems.
507 It is embedded in the pure functional language \gls{CLEAN} and uses an enriched lambda calculus as a host language.
508 It provides support for all common arithmetic expressions, conditionals, functions, but also several basic tasks, task combinators, peripheral support and integration with \gls{ITASK}.
509 By embedding domain-specific knowledge in the language itself, it achieves the same abstraction level and dynamicity as other \gls{TOP} languages while targetting tiny computers instead.
510 As a result, a single declarative specification can describe an entire \gls{IOT} system.
511
512 \input{subfilepostamble}
513 \end{document}