someTask =
sensor1 config1 \sns1->
sensor2 config2 \sns2->
- sds \s1 = initialValue
- In lowerSds \s2 = someiTaskSDS
- In fun \fun1= ( \(a0, a1)->... )
- In fun \fun2= ( \a->... )
+ sds \s1 = initialValue
+ In lowerSds \s2 = someiTaskSDS
+ In fun \fun1 = ( \(a0, a1)->... )
+ In fun \fun2 = ( \a->... )
In { main = mainexpr }
\end{lstClean}
% VimTeX: SynIgnore off
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}.
\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\citep[\citesection{3.7.4}]{plasmeijer_clean_2021}.
+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}.
\begin{lstClean}[label={lst:rank2_mtask},caption={Rank-2 polymorphism to allow multiple interpretations.}]
simulateAndPrint :: (A.v: Main (MTask v a) | mtask v) -> Task a | type a
\Cref{lst:example_exprs} shows some examples of expressions in the \gls{MTASK} language.
Since they are only expressions, there is no need for a \cleaninline{Main}.
\cleaninline{e0} defines the literal \num{42}, \cleaninline{e1} calculates the literal \num{42.0} using real numbers and uses a type conversion.
-\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.
+\cleaninline{e2} compares \cleaninline{e0} and \cleaninline{e1} as integers and if they are equal it returns $\nicefrac{\text{\cleaninline{e2}}}{2}$ and \cleaninline{e0} otherwise.
\begin{lstClean}[label={lst:example_exprs},caption={Example \gls{MTASK} expressions.}]
e0 :: v Int | expr v
It performs a simple approximate equality---admittedly not taking into account all floating point peculiarities.
When calling \cleaninline{approxEqual} in an \gls{MTASK} expression, the resulting code is inlined.
-\begin{lstClean}[label={lst:example_macro},caption={Approximate equality as an example of linguistic reuse in \gls{MTASK}.}]
+\begin{lstClean}[label={lst:example_macro},caption={Approximate equality in \gls{MTASK}.}]
approxEqual :: (v Real) (v Real) (v Real) -> v Bool | expr v
-approxEqual x y eps = x ==. y |. If (x >. y)
- (x -. y <. eps)
- (y -. x <. eps)
+approxEqual x y eps = x ==. y
+ |. If (x >. y)
+ (x -. y <. eps)
+ (y -. x <. eps)
\end{lstClean}
\subsection{Data types}
\end{lstClean}
\subsection{Functions}\label{sec:mtask_functions}
-Adding functions to the language is achieved by one type class to the \gls{DSL}.
-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}.
-The \gls{MTASK} language only allows first-order functions and no partial function application.
-To restrict this, a multi-parameter type class is used instead of a type class with one type variable.
+Adding functions to the language is achieved by one type class in the \gls{MTASK} \gls{DSL}.
+By using \gls{HOAS}, both the function definitions and the calls to the functions are controlled by the \gls{DSL} \citep{pfenning_higher-order_1988,chlipala_parametric_2008}.
+The \gls{MTASK} language enforces all functions to be first-order and forbids partial function application in order to reduce memory use and code size.
+These restrictions are enforced by using a multi-parameter type class with two parameters instead of a type class with one type variable.
The first parameter represents the shape of the arguments, the second parameter the interpretation.
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.
-By using argument tuples to represent the arity of the function, partial function applications are eradicated.
-The definition of the type class and some instances for the pretty printer are as follows:
+By using argument tuples to represent the arity of the function, it is not possible to create partial function applications.
+The definition of the type class and some instances for the pretty printer are shown in \cref{lst:fun_mtask}.
-\begin{lstClean}[caption={Functions in \gls{MTASK}.}]
+\begin{lstClean}[float=,caption={Functions in \gls{MTASK}.},label={lst:fun_mtask}]
class fun a v :: ((a -> v s) -> In (a -> v s) (Main (MTask v u)))
-> Main (MTask v u)
\end{lstClean}
Deriving how to define and use functions from the type is quite a challenge even though the resulting syntax is made easier using the infix type \cleaninline{In}.
+Splitting out the function definition for each single arity means that for every function arity and combination of arguments, a separate class constraint is required.
+Many of the often used functions signatures are in the \cleaninline{mtask} class constraint collection.
\Cref{lst:function_examples} show some examples of functions to illustrate the syntax.
-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.
-Many of the often used functions are already bundled in the \cleaninline{mtask} class constraint collection.
The \cleaninline{factorial} functions shows a recursive version of the factorial function.
-The \cleaninline{factorialtail} function is a tail-call optimised version of the factorial function.
+The \cleaninline{factorialtail} function is a tail-call optimised version of the above.
It also illustrates a manually added class constraint, as they are required when functions are used that have signatures not present in the \cleaninline{mtask} class collection.
-Zero-arity functions are always called with unit as an argument.
-An illustration of this is seen in the \cleaninline{zeroarity} expression.
-Finally, \cleaninline{swapTuple} shows an example of a tuple being swapped.
+Zero-arity functions are always called with unit as an argument, which is shown in the \cleaninline{zeroarity} function.
+Finally, the \cleaninline{swapTuple} function shows an example of a tuple being swapped using the \cleaninline{tupopen} macro (see \cref{lst:tuple_exprs}).
% VimTeX: SynIgnore on
\begin{lstClean}[label={lst:function_examples},caption={Examples of various functions in \gls{MTASK}.}]
factorial :: Main (v Int) | mtask v
factorial =
- fun \fac=(\i->If (i <. lit 1)
+ fun \fac = (\i->If (i <. lit 1)
(lit 1)
(i *. fac (i -. lit 1)))
In {main = fac (lit 5) }
factorialtail :: Main (v Int) | mtask v & fun (v Int, v Int) v
factorialtail =
- fun \facacc=(\(acc, i)->If (i <. lit 1)
+ fun \facacc = (\(acc, i)->If (i <. lit 1)
acc
(fac (acc *. i, i -. lit 1)))
- In fun \fac=(\i->facacc (lit 1, i))
+ In fun \fac = (\i->facacc (lit 1, i))
In {main = fac (lit 5) }
zeroarity :: Main (v Int) | mtask v
zeroarity =
- fun \fourtytwo=(\()->lit 42)
- In fun \add=(\(x, y)->x +. y)
+ fun \fourtytwo = (\()->lit 42)
+ In fun \add = (\(x, y)->x +. y)
In {main = add (fourtytwo (), lit 9)}
-
+ [+\pagebreak+]
swapTuple :: Main (v (Int, Bool)) | mtask v
swapTuple =
- fun \swap=(tupopen \(x, y)->tupl y x)
+ fun \swap = (tupopen \(x, y)->tupl y x)
In {main = swap (tupl true (lit 42)) }
\end{lstClean}
% VimTeX: SynIgnore off
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.
Other peripherals have similar interfaces, they are available in \cref{sec:aux_peripherals}.
-\begin{lstClean}[label={lst:dht},caption={The \gls{MTASK} interface for \glspl{DHT} sensors.}]
+\begin{lstClean}[float=,label={lst:dht},caption={The \gls{MTASK} interface for \glspl{DHT} sensors.}]
:: DHT //abstract
:: DHTInfo
= DHT_DHT Pin DHTtype
\begin{itemize}
\item sequential combinators that execute tasks one after the other, possibly using the result of the left-hand side;
\item parallel combinators that execute tasks at the same time, combining the result;
- \item miscellaneous combinators that change the semantics of a task---for example a combinator that repeats the child task.
+ \item and miscellaneous combinators that change the semantics of a task---for example a combinator that repeats the child task.
\end{itemize}
\subsubsection{Sequential}
Every rewrite step, the list of task continuations are tested on the task value.
If one of the predicates matches, the task continues with the result of these continuations.
Several shorthand combinators are derived from the step combinator.
-\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.
+The \cleaninline{>>=.} combinator is a shorthand for the bind operation, if the left-hand side is stable, the right-hand side function is called to produce a new task.
+The \cleaninline{>>\|.} combinator is a shorthand for the sequence operation, if the left-hand side is stable, it continues with the right-hand side task.
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}.}]
| Always (MTask v u)
\end{lstClean}
-The following listing shows an example of a step in action.
+\Cref{lst:mtask_readpinbin} shows an example task containing a step.
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.
The disjunction combinator (\cleaninline{.\|\|.}) combines the results by picking the leftmost, most stable task.
The semantics of both parallel combinators are most easily described using the \gls{CLEAN} functions shown in \cref{lst:semantics_con,lst:semantics_dis}.
-\begin{figure}[ht]
+\begin{figure}
\centering
\begin{subfigure}[t]{.5\textwidth}
\begin{lstClean}[caption={Semantics of the\\conjunction combinator.},label={lst:semantics_con}]
This task read two pins at the same time, returning when one of the pins becomes high.
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.
-\begin{lstClean}[label={lst:mtask_parallel_example},caption={Parallel task combinator example in \gls{MTASK}.}]
+\begin{lstClean}[float=,label={lst:mtask_parallel_example},caption={Parallel task combinator example in \gls{MTASK}.}]
task :: MTask v Bool
task =
declarePin D0 PMInput \d0->
declarePin D1 PMInput \d1->
- let monitor pin = readD pin >>*. [IfValue id rtrn]
+ fun \monitor = (\pin->readD pin >>*. [IfValue id rtrn])
In {main = monitor d0 .||. monitor d1}
\end{lstClean}
It runs the pretty printer and returns a list of strings containing the pretty printed result.
The pretty printing function does the best it can but obviously cannot reproduce layout, curried functions, and variable names.
This shortcoming is illustrated by printing a blink task that contains a function and currying in \cref{lst:showexample}.
+The output of this action would be \cleaninline{fun f0 a1 = writeD(D13, a1) >>= \\a2.(delay 1000) >>\| (f0 (Not a1)) in (f0 True)}
\begin{lstClean}[caption={The entry point for the pretty printing interpretation.},label={lst:showmain}]
:: Show a // from the mTask pretty printing library
fun \blink=(\state->
writeD d13 state >>|. delay (lit 500) >>=. blink o Not
) In {main = blink true}
-
-// output when printing:
-// fun f0 a1 = writeD(D13, a1) >>= \a2.(delay 1000)
-// >>| (f0 (Not a1)) in (f0 True)
\end{lstClean}
\subsection{Simulator}
repositories / phd-thesis.git / blobdiff