updates
[phd-thesis.git] / top / lang.tex
index 2baed8b..a5916cd 100644 (file)
@@ -5,41 +5,39 @@
 \begin{document}
 \input{subfileprefix}
 
-\chapter{The \texorpdfstring{\gls{MTASK}}{mTask} \texorpdfstring{\glsxtrshort{DSL}}{DSL}}%
+\chapter{The \texorpdfstring{\gls{MTASK}}{mTask} language}%\texorpdfstring{\glsxtrshort{DSL}}{DSL}}%
 \label{chp:mtask_dsl}
 \begin{chapterabstract}
-This chapter introduces the \gls{MTASK} language more technically by:
+       \noindent This chapter introduces the \gls{TOP} language \gls{MTASK} language by:
        \begin{itemize}
                \item introducing the setup of the \gls{EDSL};
-               \item and showing the language interface and examples for:
-                       \begin{itemize}
-                               \item data types
-                               \item expression
-                               \item task and their combinators.
-                       \end{itemize}
+               \item and showing the language interface and examples for the type system, data types, expressions, tasks and their combinators.
        \end{itemize}
 \end{chapterabstract}
 
-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.
+The \gls{MTASK} system is a complete \gls{TOP} programming environment for programming microcontrollers.
+This means that it not only contains a \gls{TOP} language but also a \gls{TOP} engine.
 It is implemented as an \gls{EDSL} in \gls{CLEAN} using class-based---or tagless-final---embedding (see \cref{sec:tagless-final_embedding}).
 Due to the nature of the embedding technique, it is possible to have multiple interpretations for programs written in the \gls{MTASK} language.
+Not all of these intepretations are necessarily \gls{TOP} engines, some may perform an analysis over the program or typeset the program so that the output can be shown after evaluating the expression at run time.
 The following interpretations are available for \gls{MTASK}.
 
 \begin{description}
-       \item[Pretty printer]
+       \item[Printer]
 
                This interpretation converts the expression to a string representation.
+               As the host language \gls{CLEAN} constructs the \gls{MTASK} expressions at run time, it can be useful to show the constructed expression.
        \item[Simulator]
 
                The simulator converts the expression to a ready-for-work \gls{ITASK} simulation in which the user can inspect and control the simulated peripherals and see the internal state of the tasks.
        \item[Byte code compiler]
 
-               The compiler compiles the \gls{MTASK} program at runtime to a specialised byte code.
-               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.
+               The compiler compiles the \gls{MTASK} program to a specialised byte code.
+               Using a handful of integration functions and tasks (see \cref{chp:integration_with_itask}), \gls{MTASK} tasks can be executed on microcontrollers and integrated in \gls{ITASK} as if they were regular \gls{ITASK} tasks.
                Furthermore, with special language constructs, \glspl{SDS} can be shared between \gls{MTASK} and \gls{ITASK} programs.
 \end{description}
 
-When using the compiler interpretation in conjunction with the \gls{ITASK} integration, \gls{MTASK} is a heterogeneous \gls{DSL}.
+When using the byte code compiler interpretation in conjunction with the \gls{ITASK} integration, \gls{MTASK} is a heterogeneous \gls{DSL}.
 I.e.\ some components---e.g.\ the \gls{RTS} on the microcontroller---is largely unaware of the other components in the system, and it is executed on a completely different architecture.
 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}).
 
@@ -54,7 +52,7 @@ The class constraints for values in \gls{MTASK} are omnipresent in all functions
 
 \begin{table}[ht]
        \centering
-       \caption{Mapping from \gls{CLEAN}/\gls{MTASK} data types to \gls{CPP} datatypes.}%
+       \caption{Translation from \gls{CLEAN}/\gls{MTASK} data types to \gls{CPP} datatypes.}%
        \label{tbl:mtask-c-datatypes}
        \begin{tabular}{lll}
                \toprule
@@ -63,14 +61,14 @@ The class constraints for values in \gls{MTASK} are omnipresent in all functions
                \cleaninline{Bool}             & \cinline{bool}    & 16\\
                \cleaninline{Char}             & \cinline{char}    & 16\\
                \cleaninline{Int}              & \cinline{int16_t} & 16\\
-               \cleaninline{:: Long}          & \cinline{int32_t} & 32\\
                \cleaninline{Real}             & \cinline{float}   & 32\\
+               \cleaninline{:: Long}          & \cinline{int32_t} & 32\\
                \cleaninline{:: T = A \| B \| C} & \cinline{enum}    & 16\\
                \bottomrule
        \end{tabular}
 \end{table}
 
-\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.
+\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.
 The \gls{MTASK} language interface consists of a core collection of type classes bundled in the type class \cleaninline{class mtask}.
 Every interpretation implements the type classes in the \cleaninline{mtask} class
 There are also \gls{MTASK} extensions that not every interpretation implements such as peripherals and \gls{ITASK} integration.
@@ -79,7 +77,6 @@ class type t | iTask, ... ,fromByteCode, toByteCode t
 class basicType t | type t where ...
 
 class mtask v | expr, ..., int, real, long v
-
 \end{lstClean}
 
 Sensors, \glspl{SDS}, functions, \etc{} may only be defined at the top level.
@@ -95,14 +92,31 @@ someTask :: MTask v Int | mtask v & liftsds v & sensor1 v & ...
 someTask =
        sensor1 config1 \sns1->
        sensor2 config2 \sns2->
-          sds \s1=initial
-       In liftsds \s2=someiTaskSDS
-       In fun \fun1= ( ... )
-       In fun \fun2= ( ... )
+          sds     \s1  = initialValue
+       In liftsds \s2  = someiTaskSDS
+       In fun     \fun1= ( ... )
+       In fun     \fun2= ( ... )
        In { main = mainexpr }
 \end{lstClean}
 
+\Gls{MTASK} expressions are usually overloaded in their interpretation (\cleaninline{v}).
+In \gls{CLEAN}, all free variables in a type are implicitly universally quantified.
+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}.
+\Cref{lst:rank2_mtask} shows an example of a function that simulates an \gls{MTASK} expression while showing the pretty printed representation in parallel.
+Providing a type for the \cleaninline{simulateAndPrint} function is mandatory as the compiler cannot infer the type of rank-2 polymorphic functions.
+
+\begin{lstClean}[label={lst:rank2_mtask},caption={Rank-2 polymorphism to allow multiple interpretations}]
+prettyPrint :: Main (MTask PrettyPrint a) -> String
+simulate :: Main (MTask Simulate a) -> Task a
+
+simulateAndPrint :: (A.v: Main (MTask v a) | mtask v) -> Task a | type a
+simulateAndPrint mt =
+           simulate mt
+       -|| Hint "Current task:" @>> viewInformation [] (prettyPrint mt)
+\end{lstClean}
+
 \section{Expressions}\label{sec:expressions}
+This section shows all \gls{MTASK} constructs for exppressions.
 \Cref{lst:expressions} shows the \cleaninline{expr} class containing the functionality to lift values from the host language to the \gls{MTASK} language (\cleaninline{lit}); perform number and boolean arithmetics; do comparisons; and conditional execution.
 For every common 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.
 
@@ -120,6 +134,7 @@ class expr v where
 \end{lstClean}
 
 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}.
+For most interpretations, there are instances of these classes for all numeric types.
 
 \begin{lstClean}[caption={Type conversion functions in \gls{MTASK}.}]
 class int  v a :: (v a) -> v Int
@@ -149,7 +164,7 @@ e2 = if' (e0 ==. int e1)
 
 \Gls{MTASK} is shallowly embedded in \gls{CLEAN} and the terms are constructed at runtime.
 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}
-\cleaninline{approxEqual} in \cref{lst:example_macro} performs an approximate equality---albeit not taking into account all floating point pecularities---.
+\cleaninline{approxEqual} in \cref{lst:example_macro} performs a simple approximate equality---albeit without taking into account all floating point pecularities.
 When calling \cleaninline{approxEqual} in an \gls{MTASK} function, the resulting code is inlined.
 
 \begin{lstClean}[label={lst:example_macro},caption={Example linguistic reuse in the \gls{MTASK} language.}]
@@ -162,7 +177,7 @@ approxEqual x y eps = if' (x ==. y) true
 \end{lstClean}
 
 \subsection{Data types}
-Most of \gls{CLEAN}'s basic types have been mapped on \gls{MTASK} types.
+Most of \gls{CLEAN}'s fixed-size basic types are mapped on \gls{MTASK} types.
 However, it can be useful to have access to compound types as well.
 All types in \gls{MTASK} must have a fixed size representation on the stack so sum types are not (yet) supported.
 While it is possible to lift types using the \cleaninline{lit} function, you cannot do anything with the types besides passing them around but they are being produced by some parallel task combinators (see \cref{sssec:combinators_parallel}).
@@ -239,6 +254,7 @@ swapTuple =
 % VimTeX: SynIgnore off
 
 \section{Tasks and task combinators}\label{sec:top}
+This section describes \gls{MTASK}'s task language.
 \Gls{MTASK}'s task language can be divided into three categories, namely
 \begin{enumerate*}
        \item Basic tasks, in most \gls{TOP} systems, the basic tasks are called editors, modelling the interactivity with the user.
@@ -249,10 +265,12 @@ swapTuple =
 \end{enumerate*}
 
 As \gls{MTASK} is integrated with \gls{ITASK}, the same stability distinction is made for task values.
-A task in \gls{MTASK} is denoted by the \gls{DSL} type synonym shown in \cref{lst:task_type}.
+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}.
 
 \begin{lstClean}[label={lst:task_type},caption={Task type in \gls{MTASK}.}]
 :: MTask v a :== v (TaskValue a)
+
+// From the iTask library
 :: TaskValue a
        = NoValue
        | Value a Bool
@@ -275,7 +293,6 @@ class delay v :: (v n) -> MTask v n | long v n
 \subsubsection{Peripherals}\label{sssec:peripherals}
 For every sensor or actuator, basic tasks are available that allow interaction with the specific peripheral.
 The type classes for these tasks are not included in the \cleaninline{mtask} class collection as not all devices nor all language interpretations have such peripherals connected.
-%\todo{Historically, peripheral support has been added \emph{by need}.}
 
 \Cref{lst:dht,lst:gpio} show the type classes for \glspl{DHT} sensors and \gls{GPIO} access.
 Other peripherals have similar interfaces, they are available in the \cref{sec:aux_peripherals}.
@@ -283,7 +300,7 @@ For the \gls{DHT} sensor there are two basic tasks, \cleaninline{temperature} an
 Currently, two different types of \gls{DHT} sensors are supported, the \emph{DHT} family of sensors connect through $1$-wire protocol and the \emph{SHT} family of sensors connected using \gls{I2C} protocol.
 Creating such a \cleaninline{DHT} object is very similar to creating functions in \gls{MTASK} and uses \gls{HOAS} to make it type safe.
 
-\begin{lstClean}[label={lst:dht},caption{The \gls{MTASK} interface for \glspl{DHT} sensors.}]
+\begin{lstClean}[label={lst:dht},caption={The \gls{MTASK} interface for \glspl{DHT} sensors.}]
 :: DHT //abstract
 :: DHTInfo
        = DHT_DHT Pin DHTtype
@@ -299,13 +316,16 @@ measureTemp = DHT (DHT_SHT (i2c 0x36)) \dht->
        {main=temperature dht}
 \end{lstClean}
 
-\Gls{GPIO} access is divided into three classes: analog, digital and pin modes.
+\Gls{GPIO} access is divided into three classes: analog, digital and pin modes (see \cref{lst:gpio}).
 For all pins and pin modes an \gls{ADT} is available that enumerates the pins.
 The analog \gls{GPIO} pins of a microcontroller are connected to an \gls{ADC} that translates the voltage to an integer.
 Analog \gls{GPIO} pins can be either read or written to.
 Digital \gls{GPIO} pins only report a high or a low value.
-The type class definition is a bit more complex since analog \gls{GPIO} pins can be used as digital \gls{GPIO} pins as well.
-Therefore, if the \cleaninline{p} type implements the \cleaninline{pin} class---i.e.\ either \cleaninline{APin} or \cleaninline{DPin}---the \cleaninline{dio} class can be used.
+The \cleaninline{pin} type class allows functions to be overloaded in either the analog or digital pins, e.g.\ analog pins can be considered as digital pins as well.
+
+For digital \gls{GPIO} interaction, the \cleaninline{dio} type class is used.
+The first argument of the functions in this class is overloaded, i.e.\ it accepts either an \cleaninline{APin} or a \cleaninline{DPin}.
+Analog \gls{GPIO} tasks are bundled in the \cleaninline{aio} type class.
 \Gls{GPIO} pins usually operate according to a certain pin mode that states whether the pin acts as an input pin, an input with an internal pull-up resistor or an output pin.
 This setting can be applied using the \cleaninline{pinMode} class by hand or by using the \cleaninline{declarePin} \gls{GPIO} pin constructor.
 Setting the pin mode is a task that immediately finisheds and fields a stable unit value.
@@ -314,10 +334,12 @@ Reading a pin is a task that yields an unstable value---i.e.\ the value read fro
 
 \begin{lstClean}[label={lst:gpio},caption={The \gls{MTASK} interface for \gls{GPIO} access.}]
 :: APin = A0 | A1 | A2 | A3 | A4 | A5
-:: DPin = D0 | D1 | D2 | D3 | D4 | D5 | D6 | D7 | D8 | D9 | D10 | D11 | D12 | D13
+:: DPin = D0 | D1 | D2 | D3 | D4 | D5 | D6 | D7 | D8 | D9 | D10 | ...
 :: PinMode = PMInput | PMOutput | PMInputPullup
 :: Pin = AnalogPin APin | DigitalPin DPin
+
 class pin p :: p -> Pin
+instance pin APin, DPin
 
 class aio v where
        writeA :: (v APin) (v Int) -> MTask v Int
@@ -332,6 +354,12 @@ class pinMode v where
        declarePin :: p PinMode ((v p) -> Main (v a)) -> Main (v a) | pin p
 \end{lstClean}
 
+\Cref{lst:gpio_examples} shows two examples of \gls{MTASK} tasks using \gls{GPIO} pins.
+\cleaninline{task1} reads analog \gls{GPIO} pin 3.
+This is a task that never terminates.
+\cleaninline{task2} writes the \cleaninline{true} (\gls{ARDUINO} \arduinoinline{HIGH}) value to digital \gls{GPIO} pin 3.
+This task finishes immediately after writing to the pin.
+
 \begin{lstClean}[label={lst:gpio_examples},caption={\Gls{GPIO} example in \gls{MTASK}.}]
 task1 :: MTask v Int | mtask v
 task1 = declarePin A3 PMInput \a3->{main=readA a3}
@@ -341,7 +369,7 @@ task2 = declarePin D3 PMOutput \d3->{main=writeD d3 true}
 \end{lstClean}
 
 \subsection{Task combinators}
-Task combinators are used to combine multiple tasks into one to describe workflows.
+Task combinators are used to combine multiple tasks to describe workflows.
 There are three main types of task combinators, namely:
 \begin{enumerate*}
        \item Sequential combinators that execute tasks one after the other, possibly using the result of the left hand side.
@@ -355,7 +383,7 @@ All seqential task combinators are expressed in the \cleaninline{expr} class and
 This combinator has a single task on the left-hand side and a list of \emph{task continuations} on the right-hand side.
 The list of task continuations is checked every rewrite step and if one of the predicates matches, the task continues with the result of this combination.
 \cleaninline{>>=.} is a shorthand for the bind operation, if the left-hand side is stable, the right-hand side function is called to produce a new task.
-\cleaninline{>>|.} is a shorthand for the sequence operation, if the left-hand side is stable, it continues with the right-hand side task.
+\cleaninline{>>\|.} is a shorthand for the sequence operation, if the left-hand side is stable, it continues with the right-hand side task.
 The \cleaninline{>>~.} and \cleaninline{>>..} combinators are variants of the ones above that ignore the stability and continue on an unstable value as well.
 
 \begin{lstClean}[label={lst:mtask_sequential},caption={Sequential task combinators in \gls{MTASK}.}]
@@ -373,8 +401,6 @@ class step v | expr v where
        | Always                                (MTask v u)
 \end{lstClean}
 
-\todo{more examples step?}
-
 The following listing shows an example of a step in action.
 The \cleaninline{readPinBin} function produces an \gls{MTASK} task that classifies the value of an analogue pin into four bins.
 It also shows that the nature of embedding allows the host language to be used as a macro language.
@@ -391,13 +417,18 @@ readPinBin lim = declarePin PMInput A2 \a2->
 
 \subsubsection{Parallel}\label{sssec:combinators_parallel}
 The result of a parallel task combination is a compound that actually executes the tasks at the same time.
-
 There are two types of parallel task combinators (see \cref{lst:mtask_parallel}).
+
+\begin{lstClean}[label={lst:mtask_parallel},caption={Parallel task combinators in \gls{MTASK}.}]
+class (.&&.) infixr 4 v :: (MTask v a) (MTask v b) -> MTask v (a, b)
+class (.||.) infixr 3 v :: (MTask v a) (MTask v a) -> MTask v a
+\end{lstClean}
+
 The conjunction combinator (\cleaninline{.&&.}) combines the result by putting the values from both sides in a tuple.
 The stability of the task depends on the stability of both children.
 If both children are stable, the result is stable, otherwise the result is unstable.
 The disjunction combinator (\cleaninline{.\|\|.}) combines the results by picking the leftmost, most stable task.
-The semantics are easily described using \gls{CLEAN} functions shown in \cref{lst:semantics_con,lst:semantics_dis}.
+The semantics are most easily described using the \gls{CLEAN} functions shown in \cref{lst:semantics_con,lst:semantics_dis}.
 
 \begin{figure}[ht]
        \centering
@@ -405,8 +436,8 @@ The semantics are easily described using \gls{CLEAN} functions shown in \cref{ls
                \begin{lstClean}[caption={Semantics of the\\conjunction combinator.},label={lst:semantics_con}]
 con :: (TaskValue a) (TaskValue b)
        -> TaskValue (a, b)
-con NoValue r       = NoValue
-con l       NoValue = NoValue
+con NoValue r = NoValue
+con l NoValue = NoValue
 con (Value l ls) (Value r rs)
        = Value (l, r) (ls && rs)
 
@@ -416,8 +447,8 @@ con (Value l ls) (Value r rs)
                \begin{lstClean}[caption={Semantics of the\\disjunction combinator.},label={lst:semantics_dis}]
 dis :: (TaskValue a) (TaskValue a)
        -> TaskValue a
-dis NoValue r       = r
-dis l       NoValue = l
+dis NoValue r = r
+dis l NoValue = l
 dis (Value l ls) (Value r rs)
        | rs        = Value r True
        | otherwise = Value l ls
@@ -425,12 +456,7 @@ dis (Value l ls) (Value r rs)
        \end{subfigure}
 \end{figure}
 
-\begin{lstClean}[label={lst:mtask_parallel},caption={Parallel task combinators in \gls{MTASK}.}]
-class (.&&.) infixr 4 v :: (MTask v a) (MTask v b) -> MTask v (a, b)
-class (.||.) infixr 3 v :: (MTask v a) (MTask v a) -> MTask v a
-\end{lstClean}
-
-\Cref{lst:mtask_parallel_example} gives an example of the parallel task combinator.
+\Cref{lst:mtask_parallel_example} gives an example program using the parallel task combinator.
 This program will read two pins at the same time, returning when one of the pins becomes \arduinoinline{HIGH}.
 If the combinator was the \cleaninline{.&&.} instead, the type would be \cleaninline{MTask v (Bool, Bool)} and the task would only return when both pins have been \arduinoinline{HIGH} but not necessarily at the same time.
 
@@ -456,7 +482,7 @@ class rpeat v where
 To demonstrate the combinator, \cref{lst:mtask_repeat_example} show \cleaninline{rpeat} in use.
 This task will mirror the value read from analog \gls{GPIO} pin \cleaninline{A1} to pin \cleaninline{A2} by constantly reading the pin and writing the result.
 
-\begin{lstClean}[label={lst:mtask_repeat_example},caption={Exemplatory repeat task in \gls{MTASK}.}]
+\begin{lstClean}[label={lst:mtask_repeat_example},caption={Exemplary repeat task in \gls{MTASK}.}]
 task :: MTask v Int | mtask v
 task =
        declarePin A1 PMInput \a1->
@@ -486,7 +512,7 @@ class sds v where
 
 \Cref{lst:mtask_sds_examples} shows an example using \glspl{SDS}.
 The \cleaninline{count} function takes a pin and returns a task that counts the number of times the pin is observed as high by incrementing the \cleaninline{share} \gls{SDS}.
-In the \cleaninline{main} expression, this function is called twice and the results are combined using the parallel or combinator (\cleaninline{.||.}).
+In the \cleaninline{main} expression, this function is called twice and the results are combined using the parallel or combinator (\cleaninline{.\|\|.}).
 Using a sequence of \cleaninline{getSds} and \cleaninline{setSds} would be unsafe here because the other branch might write their old increment value immediately after writing, effectively missing a count.\todo{beter opschrijven}
 
 \begin{lstClean}[label={lst:mtask_sds_examples},caption={Examples with \glspl{SDS} in \gls{MTASK}.}]