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