more more more
authorMart Lubbers <mart@martlubbers.net>
Tue, 29 Nov 2022 14:44:46 +0000 (15:44 +0100)
committerMart Lubbers <mart@martlubbers.net>
Tue, 29 Nov 2022 14:44:46 +0000 (15:44 +0100)
dsl/class.tex
front/motto.tex
front/titlepage.tex
intro/img/blink.png [new file with mode: 0644]
intro/intro.tex
preamble.tex
subfilepreamble.tex
thesis.tex
top/green.tex

index cd5a0af..5931da7 100644 (file)
@@ -1,11 +1,13 @@
 \documentclass[../thesis.tex]{subfiles}
 
-\include{subfilepreamble}
+\input{subfilepreamble}
 
 \begin{document}
 \chapter{Deep embedding with class}%
 \label{chp:classy_deep_embedding}
 
+\input{subfileprefix}
+
 \begin{chapterabstract}
        The two flavours of \gls{DSL} embedding are shallow and deep embedding.
        In functional languages, shallow embedding models the language constructs as functions in which the semantics are embedded.
@@ -21,7 +23,7 @@
 \end{chapterabstract}
 
 \section{Introduction}
-The two flavours of \gls{DSL} embedding are deep and shallow embedding~\citep{boulton_experience_1992}.
+The two flavours of \gls{DSL} embedding are deep and shallow embedding \citep{boulton_experience_1992}.
 In \gls{FP} languages, shallow embedding models language constructs as functions in the host language.
 As a result, adding new language constructs---extra functions---is easy.
 However, the semantics of the language is embedded in these functions, making it troublesome to add semantics since it requires updating all existing language constructs.
@@ -32,7 +34,7 @@ Consequently, adding new semantics, i.e.\ novel functions, is straightforward.
 It can be stated that the language constructs are embedded in the functions that form a semantics.
 If one wants to add a language construct, all semantics functions must be revisited and revised to avoid ending up with partial functions.
 
-This juxtaposition has been known for many years~\citep{reynolds_user-defined_1978} and discussed by many others~\citep{krishnamurthi_synthesizing_1998} but most famously dubbed the \emph{expression problem} by Wadler~\citep{wadler_expression_1998}:
+This juxtaposition has been known for many years \citep{reynolds_user-defined_1978} and discussed by many others \citep{krishnamurthi_synthesizing_1998} but most famously dubbed the \emph{expression problem} by Wadler \citep{wadler_expression_1998}:
 
 \begin{quote}
        The \emph{expression problem} is a new name for an old problem.
@@ -40,16 +42,16 @@ This juxtaposition has been known for many years~\citep{reynolds_user-defined_19
 \end{quote}
 
 In shallow embedding, abstracting the functions to type classes disentangles the language constructs from the semantics, allowing extension both ways.
-This technique is dubbed tagless-final embedding~\citep{carette_finally_2009}, nonetheless it is no silver bullet.
+This technique is dubbed tagless-final embedding \citep{carette_finally_2009}, nonetheless it is no silver bullet.
 Some semantics that require an intensional analysis of the syntax tree, such as transformation and optimisations, are difficult to implement in shallow embedding due to the lack of an explicit data structure representing the abstract syntax tree.
-The semantics of the \gls{DSL} have to be combined and must hold some kind of state or context, so that structural information is not lost~\citep{kiselyov_typed_2012}.
+The semantics of the \gls{DSL} have to be combined and must hold some kind of state or context, so that structural information is not lost \citep{kiselyov_typed_2012}.
 
 \subsection{Research contribution}
 This paper shows how to apply the technique observed in tagless-final embedding to deep embedding.
 The presented basic technique, christened \emph{classy deep embedding}, does not require advanced type system extensions to be used.
 However, it is suitable for type system extensions such as \glspl{GADT}.
 While this paper is written as a literate
-\Gls{HASKELL}~\citep{peyton_jones_haskell_2003} program using some minor extensions provided by \gls{GHC}~\citep{ghc_team_ghc_2021}, the idea is applicable to other languages as well\footnotemark.
+\Gls{HASKELL} \citep{peyton_jones_haskell_2003} program using some minor extensions provided by \gls{GHC} \citep{ghc_team_ghc_2021}, the idea is applicable to other languages as well\footnotemark.
 \footnotetext{Lubbers, M. (2021): Literate Haskell/lhs2\TeX{} source code of the paper ``Deep Embedding
 with Class'': TFP 2022.\ DANS.\ \url{https://doi.org/10.5281/zenodo.5081386}.}
 
@@ -124,7 +126,7 @@ sub_s e1 e2 = e1 - e2
 Adding semantics on the other hand---e.g.\ a printer---is not that simple because the semantics are part of the functions representing the language constructs.
 One way to add semantics is to change all functions to execute both semantics at the same time.
 In our case this means changing the type of \haskelllhstexinline{Sem_s} to be \haskelllhstexinline{(Int, String)} so that all functions operate on a tuple containing the result of the evaluator and the printed representation at the same time. %chktex 36
-Alternatively, a single semantics can be defined that represents a fold over the language constructs~\citep{gibbons_folding_2014}, delaying the selection of semantics to the moment the fold is applied.
+Alternatively, a single semantics can be defined that represents a fold over the language constructs \citep{gibbons_folding_2014}, delaying the selection of semantics to the moment the fold is applied.
 
 \subsection{Tagless-final embedding}\label{sec:tagless-final_embedding}
 Tagless-final embedding overcomes the limitations of standard shallow embedding.
@@ -142,7 +144,7 @@ Semantics become data types implementing these type classes, resulting in the fo
        In this case \haskelllhstexinline{newtype}s are used instead of regular \haskelllhstexinline{data} declarations.
        A \haskelllhstexinline{newtype} is a special data type with a single constructor containing a single value only to which it is isomorphic.
        It allows the programmer to define separate class instances that the instances of the isomorphic type without any overhead.
-       During compilation the constructor is completely removed~\citep[\citesection{4.2.3}]{peyton_jones_haskell_2003}.
+       During compilation the constructor is completely removed \citep[\citesection{4.2.3}]{peyton_jones_haskell_2003}.
 }
 
 \begin{lstHaskellLhstex}
@@ -220,7 +222,7 @@ It is only possible to create an expression with a subtraction on the top level.
 The recursive knot is left untied and as a result, \haskelllhstexinline{Sub_1} can never be reached from an \haskelllhstexinline{Expr_1}.
 
 Luckily, we can reconnect them by adding a special constructor to the \haskelllhstexinline{Expr_1} data type for housing extensions.
-It contains an existentially quantified~\citep{mitchell_abstract_1988} type with type class constraints~\citep{laufer_combining_1994,laufer_type_1996} for all semantics type classes~\citep[\citesection{6.4.6}]{ghc_team_ghc_2021} to allow it to house not just subtraction but any future extension.
+It contains an existentially quantified \citep{mitchell_abstract_1988} type with type class constraints \citep{laufer_combining_1994,laufer_type_1996} for all semantics type classes \citep[\citesection{6.4.6}]{ghc_team_ghc_2021} to allow it to house not just subtraction but any future extension.
 
 \begin{lstHaskellLhstex}
 data Expr_2
@@ -248,7 +250,7 @@ sub_2 e1 e2 = Ext_2 (Sub_2 e1 e2)
 
 In our example this means that the programmer can write\footnotemark:
 \footnotetext{%
-       Backticks are used to use functions or constructors in an infix fashion~\citep[\citesection{4.3.3}]{peyton_jones_haskell_2003}.
+       Backticks are used to use functions or constructors in an infix fashion \citep[\citesection{4.3.3}]{peyton_jones_haskell_2003}.
 }
 \begin{lstHaskellLhstex}
 e2 :: Expr_2
@@ -279,7 +281,7 @@ data Expr_2
 The class alias removes the need for the programmer to visit the main data type when adding additional semantics.
 Unfortunately, the compiler does need to visit the main data type again.
 Some may argue that adding semantics happens less frequently than adding language constructs but in reality it means that we have to concede that the language is not as easily extensible in semantics as in language constructs.
-More exotic type system extensions such as constraint kinds~\citep{bolingbroke_constraint_2011,yorgey_giving_2012} can untangle the semantics from the data types by making the data types parametrised by the particular semantics.
+More exotic type system extensions such as constraint kinds \citep{bolingbroke_constraint_2011,yorgey_giving_2012} can untangle the semantics from the data types by making the data types parametrised by the particular semantics.
 However, by adding some boilerplate, even without this extension, the language constructs can be parametrised by the semantics by putting the semantics functions in a data type.
 First the data types for the language constructs are parametrised by the type variable \haskelllhstexinline{d} as follows.
 
@@ -455,8 +457,8 @@ instance HasOpt_4 d => Opt_4 (Sub_4 d) where
 Pattern matching within datatypes and from an extension to the main data type works out of the box.
 Cross-extensional pattern matching on the other hand---matching on a particular extension---is something that requires a bit of extra care.
 Take for example negation propagation and double negation elimination.
-Pattern matching on values with an existential type is not possible without leveraging dynamic typing~\citep{abadi_dynamic_1991,baars_typing_2002}.
-To enable dynamic typing support, the \haskelllhstexinline{Typeable} type class as provided by \haskelllhstexinline{Data.Dynamic}~\citep{ghc_team_datadynamic_2021} is added to the list of constraints in all places where we need to pattern match across extensions.
+Pattern matching on values with an existential type is not possible without leveraging dynamic typing \citep{abadi_dynamic_1991,baars_typing_2002}.
+To enable dynamic typing support, the \haskelllhstexinline{Typeable} type class as provided by \haskelllhstexinline{Data.Dynamic} \citep{ghc_team_datadynamic_2021} is added to the list of constraints in all places where we need to pattern match across extensions.
 As a result, the \haskelllhstexinline{Typeable} type class constraints are added to the quantified type variable \haskelllhstexinline{x} of the \haskelllhstexinline{Ext_4} constructor and to \haskelllhstexinline{d}s in the smart constructors.
 
 \begin{lstHaskellLhstex}
@@ -547,9 +549,9 @@ e3 = neg_4 (Lit_4 42 `sub_4` Lit_4 38) `Add_4` Lit_4 1
 \end{lstHaskellLhstex}
 
 \section{\texorpdfstring{\Glsxtrlongpl{GADT}}{Generalised algebraic data types}}%
-\Glspl{GADT} are enriched data types that allow the type instantiation of the constructor to be explicitly defined~\citep{cheney_first-class_2003,hinze_fun_2003}.
+\Glspl{GADT} are enriched data types that allow the type instantiation of the constructor to be explicitly defined \citep{cheney_first-class_2003,hinze_fun_2003}.
 Leveraging \glspl{GADT}, deeply embedded \glspl{DSL} can be made statically type safe even when different value types are supported.
-Even when \glspl{GADT} are not supported natively in the language, they can be simulated using embedding-projection pairs or equivalence types~\citep[\citesection{2.2}]{cheney_lightweight_2002}.
+Even when \glspl{GADT} are not supported natively in the language, they can be simulated using embedding-projection pairs or equivalence types \citep[\citesection{2.2}]{cheney_lightweight_2002}.
 Where some solutions to the expression problem do not easily generalise to \glspl{GADT} (see \cref{sec:cde:related}), classy deep embedding does.
 Generalising the data structure of our \gls{DSL} is fairly straightforward and to spice things up a bit, we add an equality and boolean not language construct.
 To make the existing \gls{DSL} constructs more general, we relax the types of those constructors.
@@ -599,7 +601,7 @@ class Opt_g   v where
 
 Now that the shape of the type classes has changed, the dictionary data types and the type classes need to be adapted as well.
 The introduced type variable \haskelllhstexinline{a} is not an argument to the type class, so it should not be an argument to the dictionary data type.
-To represent this type class function, a rank-2 polymorphic function is needed~\citep[\citesection{6.4.15}]{ghc_team_ghc_2021}\citep{odersky_putting_1996}.
+To represent this type class function, a rank-2 polymorphic function is needed \citep[\citesection{6.4.15}]{ghc_team_ghc_2021}\citep{odersky_putting_1996}.
 Concretely, for the evaluatior this results in the following definitions:
 
 \begin{lstHaskellLhstex}
@@ -651,7 +653,7 @@ Defining reusable expressions overloaded in semantics or using multiple semantic
 
 Embedded \gls{DSL} techniques in functional languages have been a topic of research for many years, thus we do not claim a complete overview of related work.
 
-Clearly, classy deep embedding bears most similarity to the \emph{Datatypes \`a la Carte}~\citep{swierstra_data_2008}.
+Clearly, classy deep embedding bears most similarity to the \emph{Datatypes \`a la Carte} \citep{swierstra_data_2008}.
 In \citeauthor{swierstra_data_2008}'s approach, semantics are lifted to type classes similarly to classy deep embedding.
 Each language construct is their own datatype parametrised by a type parameter.
 This parameter contains some type level representation of language constructs that are in use.
@@ -672,7 +674,7 @@ Classy deep embedding works similarly but uses existentially quantified type var
 In classy deep embedding, the extensions do not need to be encoded in the type system and less boilerplate is required.
 Furthermore, pattern matching on extensions becomes a bit more complicated but in return it allows for multiple extensions to be added orthogonally and avoids the necessity for type system extensions.
 
-Tagless-final embedding is the shallowly embedded counterpart of classy deep embedding and was invented for the same purpose; overcoming the issues with standard shallow embedding~\citep{carette_finally_2009}.
+Tagless-final embedding is the shallowly embedded counterpart of classy deep embedding and was invented for the same purpose; overcoming the issues with standard shallow embedding \citep{carette_finally_2009}.
 Classy deep embedding was organically grown from observing the evolution of tagless-final embedding.
 The main difference between tagless-final embedding and classy deep embedding---and in general between shallow and deep embedding---is that intensional analyses of the abstract syntax tree is more difficult because there is no tangible abstract syntax tree data structure.
 In classy deep embedding, it is possible to define transformations even across extensions.
@@ -684,8 +686,8 @@ This paper differs from those approaches in the sense that it does not require a
 
 \subsection{Comparison}
 \todo[inline]{text moet beter}
-There is no silver bullet to embedding \glspl{DSL}.
-\Citet{sun_compositional_2022} provided a thorough comparison of embedding techniques including more axes than just the two statet in the expression problem.
+No \gls{DSL} embedding technique is the silver bullet.
+\Citet{sun_compositional_2022} provided a thorough comparison of embedding techniques including more axes than just the two stated in the expression problem.
 
 \Cref{tbl:dsl_comparison_brief} shows a variant of their comparison table.
 The first two rows describe the two axes of the original expression problem and the third row describes theadded axis of modular dependency handling as stated by \citeauthor{sun_compositional_2022}.
@@ -829,7 +831,7 @@ subst l r = Ext createRecord (l `Subt` r)
 \end{lstHaskellLhstex}
 
 Finally, defining terms in the language can be done immediately if the interpretations are known.
-For example, if we want to print and/or optimise the term $~(~(42+(38-4)))$, we can define it as follows:
+For example, if we want to print and/or optimise the term $\displaystyle ~(~(42+(38-4)))$, we can define it as follows:
 
 \begin{lstHaskellLhstex}
 e0 :: Expr '[Print,Opt]
@@ -841,10 +843,8 @@ This does require enumerating all the \haskelllhstexinline{CreateRecord} type cl
 At the call site, the concrete list of constraints must be known.
 
 \begin{lstHaskellLhstex}
-e1 :: (Typeable c
-       , CreateRecord (Neg c) c
-       , CreateRecord (Subst c) c
-       ) => Expr c
+e1 :: (Typeable c, CreateRecord (Neg c) c, CreateRecord (Subst c) c)
+       => Expr c
 e1 = neg (neg (Lit 42 `Add` (Lit 38 `subt` Lit 4)))
 \end{lstHaskellLhstex}
 
@@ -882,6 +882,7 @@ The source code for this extension can be found here: \url{https://gitlab.com/ml
 
 \section{Data types and definitions}%
 \label{sec:cde:appendix}
+\lstset{basicstyle=\tt\footnotesize}
 \begin{lstHaskellLhstex}[caption={Data type definitions.}]
 data Sub_g d a where
        Sub_g     :: (Eq a, Num a)      => Expr_g d a -> Expr_g d a -> Sub_g d a
@@ -1002,6 +1003,7 @@ instance HasOpt_g d => Opt_g (Eq_g d) where
        opt_g (Eq_g     e1 e2) = Eq_g (opt_g e1) (opt_g e2)
        opt_g (EqLoop_g e)     = EqLoop_g (opt_g e)
 \end{lstHaskellLhstex}
+\lstset{basicstyle=\tt\small}
 
 \end{subappendices}
 
index f721056..32d5e51 100644 (file)
@@ -27,9 +27,7 @@
        R.L. (Robert) Stevenson
 }
 \epigraph{%
-       I never thought, when I used to read books, what work it was to write them\ldots
-       It's work enough to read them sometimes\ldots
-       As to the writing, it has its own charms.
+       I never thought, when I used to read books, what work it was to write them\ldots{} It's work enough to read them sometimes\ldots{} As to the writing, it has its own charms.
 }{%
        C.J.H. (Charles) Dickens
 }
 }{%
        H.M. (Dick) Bruna
 }
-\epigraph{%
-       \ldots and writing can make things a bit more bearable.
-       A book, is a suicide postponed.
-}{%
-       E.M. (Emil) Cioran
-}
+%\epigraph{%
+%      \ldots and writing can make things a bit more bearable.
+%      A book, is a suicide postponed.
+%}{%
+%      E.M. (Emil) Cioran
+%}
 \vspace*{\fill}%
 
 \end{document}
index 9bce0be..a44004b 100644 (file)
@@ -67,9 +67,9 @@
        \item Manuscriptcommissie:
                \begin{itemize}[label={}]
                        \item \ldots%prof.\ dr.\ S.B.\ (Sven-Bodo) Scholz
-                       \item \ldots%prof.\ dr.\ C.U.\ (Clemens) Grelck (Friedrich-Schiller-Universit\"at Jena)
                        \item \ldots%prof.\ dr.\ G.K.\ (Gabrielle) Keller (Universiteit Utrecht)
-%                      \item prof.\ dr.\ M.\ (Mary) Sheeran (Chalmers University of Gothenburg)\todo{Chalmers Tekniska H\"ogskola?}
+                       \item \ldots%prof.\ dr.\ M.\ (Mary) Sheeran (Chalmers University of Gothenburg)\todo{Chalmers Tekniska H\"ogskola?}
+%                      \item \ldots%prof.\ dr.\ C.U.\ (Clemens) Grelck (Friedrich-Schiller-Universit\"at Jena)
 %                      \item prof.\ dr.\ R.T.W.\ (Ralf) Hinze (Technische Universit\"at Kaiserslautern)
                \end{itemize}
 \end{itemize}
diff --git a/intro/img/blink.png b/intro/img/blink.png
new file mode 100644 (file)
index 0000000..55b8c16
Binary files /dev/null and b/intro/img/blink.png differ
index ce27ffa..943ac76 100644 (file)
@@ -19,7 +19,7 @@ Even though there is a substantial variety among these devices, they all have on
 
 An increasing amount of these connected devices are so-called \emph{edge devices} that operate in the \gls{IOT}.
 Typically, these edge devices are powered by microcontrollers.
-Said microcontrollers contain integrated circuits accommodating a microprocessor designed for use in embedded applications.
+These miniature computers contain integrated circuits accommodating a microprocessor designed for use in embedded applications.
 Typical edge devices are therefore tiny in size; have little memory; contain a slow, but energy-efficient processor; and allow for a lot of connectivity to connect peripherals such as sensors and actuators in order to interact with their surroundings.
 %
 %\begin{figure}[ht]
@@ -32,22 +32,22 @@ Typical edge devices are therefore tiny in size; have little memory; contain a s
 Programming and maintaining \gls{IOT} systems is a complex and error-prone process.
 An \gls{IOT} programmer has to program each device and their interoperation using different programming paradigms, programming languages, and abstraction levels resulting in semantic friction.
 
-This thesis describes the research carried out around taming these complex \gls{IOT} systems using \gls{TOP}.
+This thesis describes the research carried out around orchestrating these complex \gls{IOT} systems using \gls{TOP}.
 \Gls{TOP} is an innovative tierless programming paradigm for interactive multi-tier systems.
 By utilising advanced compiler technologies, much of the internals, communication, and interoperation of the applications is automatically generated.
 From a single declarative specification of the work that needs to be done, the compiler makes a ready-for-work application.
 For example, the \gls{TOP} system \gls{ITASK} can be used to program all layers of a multi-user distributed web applications from a single source specification.
-Unfortunately, because the abstraction level is so high, the hardware requirements are too excessive for such systems to be suitable for the average \gls{IOT} edge device.
+Unfortunately, because the abstraction level is so high, the hardware requirements are too excessive for \gls{TOP} systems such as \gls{ITASK} to be suitable for the average \gls{IOT} edge device.
 
 This is where \glspl{DSL} are brought into play.
 \Glspl{DSL} are programming languages created with a specific domain in mind.
 Consequently, jargon does not have to be expressed in the language itself, but they can be built-in features.
 As a result, the hardware requirements can be drastically lower, even with high levels of abstraction for the specified domain.
 
-To bridge the gap between the \gls{IOT} edge devices, the \gls{MTASK} \gls{DSL} is used.
+To incorporate the plethora of edge devices in the orchestra of an \gls{IOT} system, the \gls{MTASK} system is used.
 \Gls{MTASK} is a novel programming language for programming \gls{IOT} edge devices using \gls{TOP}.
+Where \gls{ITASK} abstracts away from the gritty details of multi-tier web applications, \gls{MTASK} has domain-specific abstractions for \gls{IOT} edge devices, maintaining the high abstraction level that \gls{TOP} generally offers.
 As it is integrated with \gls{ITASK}, it allows for all layers of an \gls{IOT} application to be programmed from a single source.
-\todo{Kan deze \P\ weg? Aan\-ge\-zien het ook al in de volgende sectie staat}
 
 \section{Reading guide}%
 \label{lst:reading_guide}
@@ -222,12 +222,12 @@ This approach to software development is called \gls{TOSD} \citep{wang_maintaini
                The \gls{UOD} is explicitly and separately modelled by the relations that exist in the functions of the host language.
 \end{description}
 
-Applying the concepts of \gls{LSOC} to \gls{IOT} systems can be done in two ways.
-Firstly, edge devices can be seen as simple resources, thus accessed through the resource access layer.
-The second view is that edge devices contain miniature \gls{LSOC} systems in itself as well.
-In \gls{TOSD} the same can be applied.
-The individual components in the miniature systems, the tasks, the \glspl{SDS}, are connected to the main system.
-\todo{Is deze \P\ dui\-de\-lijk genoeg of \"uberhaupt nodig?}
+%Applying the concepts of \gls{LSOC} to \gls{IOT} systems can be done in two ways.
+%Firstly, edge devices can be seen as simple resources, thus accessed through the resource access layer.
+%The second view is that edge devices contain miniature \gls{LSOC} systems in itself as well.
+%In \gls{TOSD} the same can be applied.
+%The individual components in the miniature systems, the tasks, the \glspl{SDS}, are connected to the main system.
+%\t odo{Is deze \P\ dui\-de\-lijk genoeg of \"uberhaupt nodig?}
 
 \subsection{\texorpdfstring{\Gls{ITASK}}{ITask}}
 The concept of \gls{TOP} originated from the \gls{ITASK} framework, a declarative interactive systems language and \gls{TOP} engine for defining multi-user distributed web applications implemented as an \gls{EDSL} in the lazy pure \gls{FP} language \gls{CLEAN} \citep{plasmeijer_itasks:_2007,plasmeijer_task-oriented_2012}.
@@ -275,7 +275,7 @@ This feather-light domain-specific \gls{OS} is written in portable \gls{C} with
 \Gls{MTASK} is seamlessly integrated with \gls{ITASK}: \gls{MTASK} tasks are integrated in such a way that they function as \gls{ITASK} tasks, and \glspl{SDS} in on the device can tether an \gls{ITASK} \gls{SDS}.
 Using \gls{MTASK}, the programmer can define all layers of an \gls{IOT} system as a single declarative specification.
 
-\Cref{lst:intro_blink} shows an interactive \gls{MTASK}\slash{}\gls{ITASK} application for blinking \pgls{LED} on the microcontroller every user-specified interval.
+\Cref{lst:intro_blink,fig:intro_blink} shows the code and a screenshot of an interactive \gls{MTASK}\slash{}\gls{ITASK} application for blinking \pgls{LED} on the microcontroller every user-specified interval.
 \Crefrange{lst:intro:itask_fro}{lst:intro:itask_to} show the \gls{ITASK} part.
 First \pgls{SDS} is defined to communicate the blinking interval, then the \gls{MTASK} is connected using \cleaninline{withDevice}.
 Once connected, the \cleaninline{intBlink} task is sent to the device (\cref{lst:intro_liftmtask}) and, in parallel, an editor is shown that updates the value of the interval \gls{SDS} (\cref{lst:intro_editor}).
@@ -285,6 +285,13 @@ This task first defines \gls{GPIO} pin 13 to be of the output type (\cref{lst:in
 The main expression of the program calls the \cleaninline{blink} function with an initial state.
 This function on \crefrange{lst:intro:blink_fro}{lst:intro:blink_to} first reads the interval \gls{SDS}, waits the specified delay, writes the state to the \gls{GPIO} pin and calls itself recursively using the inverse of the state.
 
+\begin{figure}
+       \centering
+       \includegraphics[width=.3\textwidth]{blink}
+       \caption{Screenshot for the interactive blink application.}%
+       \label{fig:intro_blink}
+\end{figure}
+
 \begin{lstClean}[numbers=left,caption={\Gls{MTASK}\slash{}\gls{ITASK} interactive blinking.},label={lst:intro_blink}]
 interactiveBlink :: Task Int[+\label{lst:intro:itask_fro}+]
 interactiveBlink =
@@ -303,93 +310,93 @@ intBlink iInterval =
        In {main = blink true}[+\label{lst:intro:mtask_to}+]
 \end{lstClean}
 
-\todo{Zal ik hier nog een soort conclusie maken van \gls{MTASK}.}
-
 \subsection{Other \texorpdfstring{\glsxtrshort{TOP}}{TOP} languages}
 While \gls{ITASK} conceived \gls{TOP}, it is not the only \gls{TOP} system.
 Some \gls{TOP} systems arose from Master's and Bachelor's thesis projects.
 For example, \textmu{}Task \citep{piers_task-oriented_2016}, a \gls{TOP} language for modelling non-interruptible embedded systems in \gls{HASKELL}, and LTasks \citep{van_gemert_task_2022}, a \gls{TOP} language written in the dynamically typed programming language {LUA}.
-Some \gls{TOP} languages were created to solve a practical problem.Toppyt \citep{lijnse_toppyt_2022} is a general purpose \gls{TOP} language written in \gls{PYTHON} used to host frameworks for modelling C2 systems, and hTask \citep{lubbers_htask_2022}, a vessel for experimenting with asynchronous \glspl{SDS}.
+Some \gls{TOP} languages were created to solve a practical problem.
+Toppyt \citep{lijnse_toppyt_2022} is a general purpose \gls{TOP} language written in \gls{PYTHON} used to host frameworks for modelling C2 systems, and hTask \citep{lubbers_htask_2022}, a vessel for experimenting with asynchronous \glspl{SDS}.
 Finally there are \gls{TOP} languages with strong academic foundations.
 \Gls{TOPHAT} is a fully formally specified \gls{TOP} language designed to capture the essence of \gls{TOP} formally \citep{steenvoorden_tophat_2019}.
 Such a formal specification allows for symbolic execution, hint generation, but also the translation to \gls{ITASK} for actually performing the work \citep{steenvoorden_tophat_2022}.
 
 \section{Contributions}%
 \label{sec:contributions}
-\todo{Dit heb ik sterk ingekort. Ok\'e?}
-This section provides a thorough overview of the relation between the scientific publications and the episodes and chapters.
+This section provides a thorough overview of the relation between the scientific publications and the contents of this thesis.
 
 \subsection{\Fullref{prt:dsl}}
 The \gls{MTASK} system is a heterogeneous \gls{EDSL} and during the development of it, several novel basal techniques for embedding \glspl{DSL} in \gls{FP} languages have been found.
-This episode is paper based.
-
-\Cref{chp:classy_deep_embedding} is based on the paper \emph{Deep Embedding with Class} \citep{lubbers_deep_2022}.
-It shows a novel deep embedding technique for \glspl{DSL} where the resulting language is extendible both in constructs and in interpretation just using type classes and existential data types\footnotemark.
-\footnotetext{%
-The related work section is updated with the research found after publication.
-\Cref{sec:classy_reprise} was added after publication and contains a (yet) unpublished extension of the embedding technique for reducing the required boilerplate at the cost of requiring some advanced type system extensions.
-}
+This episode is paper based and contains the following papers:
+\begin{enumerate}
+       \item \emph{Deep Embedding with Class} \citep{lubbers_deep_2022} is the basis for \cref{chp:classy_deep_embedding}.
+               It shows a novel deep embedding technique for \glspl{DSL} where the resulting language is extendible both in constructs and in interpretation just using type classes and existential data types.
+               The related work section is updated with the research found after publication.
+               \Cref{sec:classy_reprise} was added after publication and contains a (yet) unpublished extension of the embedding technique for reducing the required boilerplate at the cost of requiring some advanced type system extensions.
+       \item \emph{First-Class Data Types in Shallow Embedded Domain-Specific Languages} \citep{lubbers_first-class_2022}\label{enum:first-class} is the basis for \cref{chp:first-class_datatypes}.
+               It shows how to inherit data types from the host language in \glspl{EDSL} using metaprogramming by providing a proof-of-concept implementation using \gls{HASKELL}'s metaprogramming system: \glsxtrlong{TH}.
+               Besides showing the result, the paper also serves as a gentle introduction to, and contains a thorough literature study on \glsxtrlong{TH}.
+\end{enumerate}
 
-\Cref{chp:first-class_datatypes} is based on the paper \emph{First-Class Data Types in Shallow Embedded Domain-Specific Languages} \citep{lubbers_first-class_2022}.
-It shows how to inherit data types from the host language in \glspl{EDSL} using metaprogramming by providing a proof-of-concept implementation using \gls{HASKELL}'s metaprogramming system: \glsxtrlong{TH}.
-Besides showing the result, the paper also serves as a gentle introduction to, and contains a thorough literature study on \glsxtrlong{TH}.
-%The research in this paper and writing the paper was performed by me, though there were weekly meetings with Pieter Koopman and Rinus Plasmeijer in which we discussed and refined the ideas.
+\paragraph{Contribution:}
+The research in these papers and writing the paper was performed by me, though there were weekly meetings with Pieter Koopman and Rinus Plasmeijer in which we discussed and refined the ideas for paper~\ref{enum:first-class}.
 
 \subsection{\Fullref{prt:top}}
-There were many papers and revised lecture notes published on the design, implementation and usage of \gls{MTASK}.
-This episode is a monograph compiled from the following publications and shows all aspects of the \gls{MTASK} system and \gls{TOP} for the \gls{IOT}.
-\todo{Hier een over\-zicht van de chapters geven?}
+This episode is a monograph compiled from the following publications and shows the design, properties, implementation and usage of the \gls{MTASK} system and \gls{TOP} for the \gls{IOT}.
 
-\begin{itemize}
-       \item \emph{A Task-Based \glsxtrshort{DSL} for Microcomputers} \citep{koopman_task-based_2018}.
-               This is the initial \gls{TOP}\slash{}\gls{MTASK} paper.
+\begin{enumerate}[resume]
+       \item \emph{A Task-Based \glsxtrshort{DSL} for Microcomputers} \citep{koopman_task-based_2018}
+               is the initial \gls{TOP}\slash{}\gls{MTASK} paper.
                It provides an overview of the initial \gls{TOP} \gls{MTASK} language and shows first versions of some of the interpretations.
-       \item \emph{Task Oriented Programming for the Internet of Things} \citep{lubbers_task_2018}\footnotetext{This work is an extension of my Master's thesis \citep{lubbers_task_2017}.}.
-               It shows how a simple imperative variant of \gls{MTASK} was integrated with \gls{ITASK}.
+       \item \emph{Task Oriented Programming for the Internet of Things} \citep{lubbers_task_2018}\footnotetext{This work is an extension of my Master's thesis \citep{lubbers_task_2017}.}
+               shows how a simple imperative variant of \gls{MTASK} was integrated with \gls{ITASK}.
                While the language was a lot different from later versions, the integration mechanism is still used in \gls{MTASK} today.
 %              \paragraph{Contribution}
 %              The research in this paper and writing the paper was performed by me, though there were weekly meetings with Pieter Koopman and Rinus Plasmeijer in which we discussed and refined the ideas.
-       \item \emph{Multitasking on Microcontrollers using Task Oriented Programming} \citep{lubbers_multitasking_2019}\footnote{This work acknowledges the support of the \erasmusplus{} project ``Focusing Education on Composability, Comprehensibility and Correctness of Working Software'', no.\ 2017--1--SK01--KA203--035402.}.
-               This is a short paper on the multitasking capabilities of \gls{MTASK} comparing it to traditional multitasking methods for \gls{ARDUINO}.
+       \item \emph{Multitasking on Microcontrollers using Task Oriented Programming} \citep{lubbers_multitasking_2019}\footnote{This work acknowledges the support of the \erasmusplus{} project ``Focusing Education on Composability, Comprehensibility and Correctness of Working Software'', no.\ 2017--1--SK01--KA203--035402.}
+               is a short paper on the multitasking capabilities of \gls{MTASK} comparing it to traditional multitasking methods for \gls{ARDUINO}.
 %              \paragraph{Contribution}
 %              The research in this paper and writing the paper was performed by me, though there were weekly meetings with Pieter Koopman and Rinus Plasmeijer.
-       \item \emph{Simulation of a Task-Based Embedded Domain Specific Language for the Internet of Things} \citep{koopman_simulation_2018}\footnotemark[\value{footnote}].
-               These revised lecture notes are from a course on the \gls{MTASK} simulator was provided at the 2018 \gls{CEFP}\slash{}\gls{3COWS} winter school in Ko\v{s}ice, Slovakia.
+       \item \emph{Simulation of a Task-Based Embedded Domain Specific Language for the Internet of Things} \citep{koopman_simulation_2018}\footnotemark[\value{footnote}]
+               are the revised lecture notes are from a course on the \gls{MTASK} simulator was provided at the 2018 \gls{CEFP}\slash{}\gls{3COWS} winter school in Ko\v{s}ice, Slovakia.
 %              \paragraph{Contribution}
 %              Pieter Koopman wrote and taught it, I helped with the software and research.
-       \item \emph{Writing Internet of Things Applications with Task Oriented Programming} \citep{lubbers_writing_2019}\footnotemark[\value{footnote}].
-               These revised lecture notes are from a course on programming \gls{IOT} systems using \gls{MTASK} provided at the 2019 \gls{CEFP}\slash{}\gls{3COWS} summer school in Budapest, Hungary.
+       \item \emph{Writing Internet of Things Applications with Task Oriented Programming} \citep{lubbers_writing_2019}\footnotemark[\value{footnote}]
+               are the revised lecture notes from a course on programming \gls{IOT} systems using \gls{MTASK} provided at the 2019 \gls{CEFP}\slash{}\gls{3COWS} summer school in Budapest, Hungary.
 %              \paragraph{Contribution}
 %              Pieter Koopman prepared and taught half of the lecture and supervised the practical session.
 %              I taught the other half of the lecture, wrote the lecture notes, made the assignments and supervised the practical session.
-       \item \emph{Interpreting Task Oriented Programs on Tiny Computers} \citep{lubbers_interpreting_2019}.
-               This paper shows an implementation of the byte code compiler and \gls{RTS} of \gls{MTASK}.
+       \item \emph{Interpreting Task Oriented Programs on Tiny Computers} \citep{lubbers_interpreting_2019}
+               shows an implementation of the byte code compiler and \gls{RTS} of \gls{MTASK}.
 %              \paragraph{Contribution}
 %              The research in this paper and writing the paper was performed by me, though there were weekly meetings with Pieter Koopman and Rinus Plasmeijer.
-       \item \emph{Reducing the Power Consumption of IoT with Task-Oriented Programming} \citep{crooijmans_reducing_2022}.
-               This paper shows how to create a scheduler so that devices running \gls{MTASK} tasks can go to sleep more automatically and how interrupts are incorporated in the language.
+       \item \emph{Reducing the Power Consumption of IoT with Task-Oriented Programming} \citep{crooijmans_reducing_2022}
+               shows how to create a scheduler so that devices running \gls{MTASK} tasks can go to sleep more automatically and how interrupts are incorporated in the language.
 %              \paragraph{Contribution}
 %              The research was carried out by \citet{crooijmans_reducing_2021} during his Master's thesis.
 %              I did the daily supervision and helped with the research, Pieter Koopman was the formal supervisor and wrote most of the paper.
-       \item \emph{Green Computing for the Internet of Things} \citep{lubbers_green_2022}\footnote{This work acknowledges the support of the \erasmusplus{} project ``SusTrainable---Promoting Sustainability as a Fundamental Driver in Software Development Training and Education'', no.\ 2020--1--PT01--KA203--078646.}.
-               These revised lecture notes are from a course on sustainable \gls{IOT} programming with \gls{MTASK} provided at the 2022 SusTrainable summer school in Rijeka, Croatia.
+       \item \emph{Green Computing for the Internet of Things} \citep{lubbers_green_2022}\footnote{This work acknowledges the support of the \erasmusplus{} project ``SusTrainable---Promoting Sustainability as a Fundamental Driver in Software Development Training and Education'', no.\ 2020--1--PT01--KA203--078646.}
+               are the revised lecture notes from a course on sustainable \gls{IOT} programming with \gls{MTASK} provided at the 2022 SusTrainable summer school in Rijeka, Croatia.
 
 %              \paragraph{Contribution}
 %              These revised lecture notes are from a course on sustainable programming using \gls{MTASK} provided at the 2022 SusTrainable summer school in Rijeka, Croatia.
 %              Pieter prepared and taught a quarter of the lecture and supervised the practical session.
 %              I prepared and taught the other three quarters of the lecture, made the assignments and supervised the practical session
-\end{itemize}
+\end{enumerate}
 
 \paragraph{Contribution:}
 The original imperative predecessors of the \gls{MTASK} language and their initial interpretations were developed by Pieter Koopman and Rinus Plasmeijer.
 I continued with the language; developed the byte code interpreter, the precursor to the \gls{C} code generation interpretation; the integration with \gls{ITASK}; and the \gls{RTS}.
-The paper of which I am first author are solely written by me.
+The paper of which I am first author are solely written by me, there were weekly meetings with the co-authors in which we discussed and refined the ideas.
 
 \subsection{\nameref{prt:tvt}}
 \Cref{prt:tvt} is based on a journal paper that quantitatively and qualitatively compares traditional \gls{IOT} architectures with \gls{IOT} systems using \gls{TOP} and contains a single chapter.
-This chapter is based on the journal paper: \emph{Could Tierless Programming Reduce IoT Development Grief?} \citep{lubbers_could_2022}\footnote{This work is an extension of the conference article: \emph{Tiered versus Tierless IoT Stacks: Comparing Smart Campus Software Architectures} \citep{lubbers_tiered_2020}\footnotemark.}.
-\footnotetext{This work was partly funded by the 2019 Radboud-Glasgow Collaboration Fund.}
-It compares programming traditional tiered architectures to tierless architectures by showing a qualitative and a quantitative four-way comparison of a smart-campus application.
+This chapter is based on the conference paper and a journal paper extending it:
+\begin{enumerate}[resume]
+       \item \emph{Tiered versus Tierless IoT Stacks: Comparing Smart Campus Software Architectures} \citep{lubbers_tiered_2020}\footnote{This work was partly funded by the 2019 Radboud-Glasgow Collaboration Fund.}\label{enum:iot20} compares traditional tiered programming to tierless architectures by comparing two implementations of a smart-campus application.
+       \item \emph{Could Tierless Programming Reduce IoT Development Grief?} \citep{lubbers_could_2022}
+               is an extended version of the paper~\ref{enum:iot20}.
+               It compares programming traditional tiered architectures to tierless architectures by showing a qualitative and a quantitative four-way comparison of a smart-campus application.
+\end{enumerate}
 
 \paragraph{Contribution:}
 Writing the paper was performed by all authors.
index 34be611..adb6568 100644 (file)
 }
 \usepackage{pdflscape}
 \usepackage{float}
+\usepackage{newfloat}
+\DeclareFloatingEnvironment[
+       fileext=loq,
+       listname={List of definitions},
+       name=Definition,
+       placement=tbp,
+       within=chapter,
+       chapterlistsgaps=on,
+       ]{equ}
 \usepackage{fancyhdr} % Custom headers and footers
 %\pagestyle{headings}
 \pagestyle{fancy}
 \urlstyle{same}
 \usepackage{bookmark}
 \usepackage[noabbrev]{cleveref} % Easy references
+\usepackage{crossreftools} % Easy references
+\crefname{equ}{equation}{equations}
 \crefname{part}{episode}{episodes}
 \crefname{lstlisting}{listing}{listings}
+\crefname{equ}{definition}{definition}
 \usepackage{nameref} % to reference names of chapters
-\newcommand{\fullref}[1]{\cref{#1}: \nameref{#1}}
-\newcommand{\Fullref}[1]{\Cref{#1}: \nameref{#1}}
+\newcommand{\fullref}[1]{\crtcref{#1}: \nameref{#1}}
+\newcommand{\Fullref}[1]{\crtCref{#1}: \nameref{#1}}
 \creflabelformat{equation}{#2\textup{#1}#3}
 
 % Glossaries and acronyms
        \def\Glspl#1{}%
        \def\Glsentrytext#1{}%
        \def\titlecap#1{}%
+       \def\MakeUppercase#1{}%
 }
 
 % Index
 \newcommand{\pkoopman}{Koopman, dr.\ P.\ (Radboud University)}
 \newcommand{\ptrinder}{Trinder, prof.~dr.\ P.\ (University of Glasgow)}
 \newcommand{\rdmentry}[5]{#1 (#2): #3. #4.\ \doifmt{#5}}
-\newcommand{\refreshrate}[2]{\langle{}#1, #2\rangle{}}
+\newcommand{\rewriterate}[2]{\langle{}#1, #2\rangle{}}
 \newcommand{\requiresGHCmod}[2][]{\footnote{Requires \GHCmod{#2} to be enabled. #1}}
 \newcommand{\rplasmeijer}{Plasmeijer, prof.\ dr.\ ir.\ R.\ (Radboud University)}
 \newcommand{\erasmusplus}{ERASMUS\raisebox{.25ex}{+}}
index 13d489a..07b0026 100644 (file)
@@ -1,5 +1,5 @@
 \ifSubfilesClassLoaded{%
        \pagenumbering{arabic}
-       \externaldocument{thesis}
+       \externaldocument{\subfix{thesis}}
 }{%
 }
index 18de889..d0ed9bc 100644 (file)
@@ -69,7 +69,7 @@
 \subfile{dsl/class}    % Deep embedding with class
 \subfile{dsl/first}    % First-class data types
 
-\part[Oratorio --- Task-Oriented Programming for the Internet of Things]{Oratorio\\[2ex]\smaller{}Task-Oriented Programming for the Internet of Things}%
+\part{Orchestrating the IoT using Task-Oriented Programming}%
 \label{prt:top}
 \subfile{top/4iot}  % TOP for the IoT
 \subfile{top/lang}  % mTask DSL
@@ -77,7 +77,7 @@
 \subfile{top/imp}   % Implementation
 \subfile{top/green} % Green computing
 
-\part[Variations --- Tiered vs.\ Tierless Programming]{Transformation\\[2ex]\smaller{}Tiered vs.\ Tierless Programming}%
+\part{Tiered vs.\ Tierless Programming}%
 \label{prt:tvt}
 \subfile{tvt/tvt}   % Could Tierless Languages Reduce IoT Development Grief?
 
index 89dc07b..4fb209a 100644 (file)
@@ -84,7 +84,7 @@ This is very convenient, since the system can inspect the current state of all \
 Even infinite sequences rewrite steps, as in the \cleaninline{blink} example, are perfectly fine.
 The \gls{MTASK} system does proper tail-call optimizations to facilitate this.
 
-\section{Task scheduling in the \gls{MTASK} language}
+\section{Rewrite interval}
 Some \gls{MTASK} examples contain one or more explicit \cleaninline{delay} primitives, offering a natural place for the node executing it to pause.
 However, there are many \gls{MTASK} programs that just specify a repeated set of primitives.
 A typical example is the program that reads the temperature for a sensor and sets the system \gls{LED} if the reading is below some given \cleaninline{goal}.
@@ -92,8 +92,8 @@ A typical example is the program that reads the temperature for a sensor and set
 \begin{lstClean}[caption={A basic thermostat task.},label={lst:thermostat}]
 thermostat :: Main (MTask v Bool) | mtask v
 thermostat = DHT I2Caddr \dht->
-       {main = rpeat ( temperature dht >>~. \temp.
-                       writeD builtInLED (goal <. temp))}
+       {main = rpeat (temperature dht >>~. \temp.
+                      writeD builtInLED (goal <. temp))}
 \end{lstClean}
 
 This program repeatedly reads the \gls{DHT} sensor and sets the on-board \gls{LED} based on the comparison with the \cleaninline{goal} as fast as possible on the \gls{MTASK} node.
@@ -111,101 +111,112 @@ Both solutions rely on an explicit action of the programmer.
 
 Fortunately, \gls{MTASK} also contains machinery to do this automatically.
 The key of this solution is to associate dynamically an evaluation interval with each task.
-The interval $\refreshrate{low}{high}$ indicates that the evaluation can be safely delayed by any number of milliseconds in that range.
+The interval $\rewriterate{low}{high}$ indicates that the evaluation can be safely delayed by any number of milliseconds within that range.
 Such an interval is just a hint for the \gls{RTS}.
 It is not a guarantee that the evaluation takes place in the given interval.
 Other parts of the task expression can force an earlier evaluation of this part of the task.
 When the system is very busy with other work, the task might even be executed after the upper bound of the interval.
-The system calculates the refresh rates from the current task expression.
+The system calculates the rewrite rates from the current task expression.
 This has the advantage that the programmer does not have to deal with them and that they are available in each and every \gls{MTASK} program.
 
 \subsection{Basic tasks}
 
-We start by assigning default refresh rates to basic tasks.
-These refresh rates reflect the expected change rates of sensors and other inputs.
-Writing to basic \gls{GPIO} pins and actuators has refresh rate $\refreshrate{0}{0}$, this is never delayed.
+We start by assigning default rewrite rates to basic tasks.
+These rewrite rates reflect the expected change rates of sensors and other inputs.
+Basic tasks to one-shot set a value of a sensor or actuator usually have a rate of $\rewriterate{0}{0}$, this is never delayed, e.g.\ writing to a \gls{GPIO} pin.
+Basic tasks that continuously read a value or otherwise interact with a peripheral have default rewrite rates that fit standard usage of the sensor.
+\Cref{tbl:rewrite} shows the default values for the basic tasks.
+I.e.\ reading \glspl{SDS} and fast sensors such as sound or light aim for a rewrite every \qty{100}{\ms}, medium slow sensors such as gesture sensors every \qty{1000}{\ms} and slow sensors such as temperature or air quality every \qty{2000}{\ms}.
 
 \begin{table}
        \centering
-       \caption{Default refresh rates of basic tasks.}%
-       \label{tbl:refresh}
+       \caption{Default rewrite rates of basic tasks.}%
+       \label{tbl:rewrite}
        \begin{tabular}{ll}
                \toprule
-               task & default interval \\
+               task & default interval\\
                \midrule
-               reading \pgls{SDS} & $\refreshrate{0}{2000}$ \\
-               slow sensor, like temperature & $\refreshrate{0}{2000}$ \\
-               gesture sensor & $\refreshrate{0}{1000}$ \\
-               fast sensor, like sound or light & $\refreshrate{0}{100}$ \\
-               reading GPIO pins & $\refreshrate{0}{100}$ \\
+               reading \pgls{SDS} & $\rewriterate{0}{2000}$\\
+               slow sensor & $\rewriterate{0}{2000}$\\
+               medium sensor & $\rewriterate{0}{1000}$\\
+               fast sensor & $\rewriterate{0}{100}$\\
                \bottomrule
        \end{tabular}
 \end{table}
 
-\subsection{Deriving refresh rates}\label{sec:deriving_refresh_rates}
-Based on these refresh rates, the system can automatically derive refresh rates for composed \gls{MTASK} expressions using $\mathcal{R}$.
-We use the operator $\cap_{\textit{safe}}$ to compose refresh ranges.
-When the ranges overlap the result is the overlapping range.
-Otherwise, the result is the range with the lowest numbers.
-The rationale is that subtasks should not be delayed longer than their refresh range.
-Evaluating a task earlier should not change its result but can consume more energy.
-
-\begin{align}
-       \cap_{\textit{safe}} :: \refreshrate{\mathit{Int}}{\mathit{Int}} \; \refreshrate{\mathit{Int}}{\mathit{Int}} & \shortrightarrow \refreshrate{\mathit{Int}}{\mathit{Int}} & \notag \\
-       R_1 \cap_{\textit{safe}} R_2 & = R_1 \cap R_2 & \text{if } R_1 \cap R_2 \neq \emptyset \\
-       \refreshrate{l_1}{h_1} \cap_{\textit{safe}} \refreshrate{l_2}{h_2} & = \refreshrate{l_2}{h_2} & \text{if } h_2 < l_1 \\
-       R_1 \cap_{\textit{safe}} R_2 & = R_1  & \text{otherwise}
-\end{align}
-
-\begin{align}
-       \mathcal{R} :: (\mathit{MTask}~v~a)    & \shortrightarrow \refreshrate{\mathit{Int}}{\mathit{Int}} \notag \\
-       \mathcal{R} (t_1~{.||.}~t_2)  & = \mathcal{R}(t_1) \cap_{\textit{safe}} \mathcal{R}(t_2) \label{R:or} \\
-       \mathcal{R}(t_1~{.\&\&.}~t_2) & = \mathcal{R}(t_1) \cap_{\textit{safe}} \mathcal{R}(t_2) \label{R:and}\\
-       \mathcal{R}(t_1~{>\!\!>\!|.}~t_2)   & = \mathcal{R}(t_1) \label{R:seq} \\
-       \mathcal{R}(t~{>\!\!>\!=.}~f)       & = \mathcal{R}(t) \label{R:bind} \\
-       \mathcal{R}(t~{>\!\!>\!\!*.}~[a_1 \ldots a_n]) & = \mathcal{R}(t) \label{R:step} \\
-       \mathcal{R}(\mathit{rpeat}~t)             & = \refreshrate{0}{0} \label{R:rpeat} \\
-       \mathcal{R}(\mathit{rpeatEvery}~d~t)   & = \refreshrate{0}{0} \label{R:rpeatevery} \\
-       \mathcal{R}(delay~d) & = \refreshrate{d}{d} \label{R:delay} \\
-       \mathcal{R}(t) & =
-               \left\{%
+\subsection{Deriving rewrite rates}\label{sec:deriving_rewrite_rates}
+Based on these default rewrite rates, the system automatically derives rewrite rates for composed \gls{MTASK} expressions using the function $\mathcal{R}$ as shown in \cref{equ:r}.
+
+\begin{equ}
+       \begin{align}
+               \mathcal{R} :: (\mathit{MTask}~v~a)    & \shortrightarrow \rewriterate{\mathit{Int}}{\mathit{Int}} \notag \\
+               \mathcal{R} (t_1~{.||.}~t_2)  & = \mathcal{R}(t_1) \cap_{\textit{safe}} \mathcal{R}(t_2) \label{R:or} \\
+               \mathcal{R}(t_1~{.\&\&.}~t_2) & = \mathcal{R}(t_1) \cap_{\textit{safe}} \mathcal{R}(t_2) \label{R:and}\\
+               \mathcal{R}(t~{>\!\!>\!\!*.}~[a_1 \ldots a_n]) & = \mathcal{R}(t) \label{R:step} \\
+               \mathcal{R}(\mathit{rpeat}~t~\mathit{start})   & =
+                       \left\{\begin{array}{ll}
+                               \mathcal{R}(t) & \text{if $t$ is unstable}\\
+                               \rewriterate{r_1-\mathit{start}}{r_2-\mathit{start}} & \text{otherwise}\\
+                       \end{array}\right.\\
+               \mathcal{R} (\mathit{waitUntil}~d) & = \rewriterate{e-\mathit{time}}{e-\mathit{time}}\label{R:delay}\\
+               \mathcal{R} (t) & =
+                       \left\{%
+                               \begin{array}{ll}
+                                       \rewriterate{\infty}{\infty}~& \text{if}~t~\text{is Stable} \\
+                                       \rewriterate{r_l}{r_u} & \text{otherwise}
+                               \end{array}
+                       \right.\label{R:other}
+       \end{align}
+       \caption{Function $\mathcal{R}$ for deriving refresh rates.}%
+       \label{equ:r}
+\end{equ}
+
+\subsubsection{Parallel combinators}
+For parallel combinators, the \emph{or}-combinator (\cleaninline{.\|\|.}) in \cref{R:or} and the \emph{and}-combinator (\cleaninline{.&&.}) in \cref{R:and}, the safe intersection (see \cref{equ:safe_intersect}) of the rewrite rates is taken to determine the rewrite rate of the complete task.
+The conventional intersection does not suffice here because it yields an empty intersection when the intervals do not overlap.
+In that case, the safe intersection behaves will return the range with the lowest numbers.
+The rationale is that subtasks should not be delayed longer than their rewrite range.
+Evaluating a task earlier should not change its result but just consumes more energy.
+
+\begin{equ}
+       \[
+               X \cap_{\textit{safe}} Y = \left\{%
                        \begin{array}{ll}
-                               \refreshrate{\infty}{\infty}~& \text{if}~t~\text{is Stable} \\
-                               \refreshrate{r_l}{r_u} & \text{otherwise}
+                               X\cap Y & X\cap Y \neq \emptyset\\
+                               Y & Y_2 < X_1\\
+                               X & \text{otherwise}\\
                        \end{array}
-               \right.\label{R:other}
-\end{align}
-
-We will briefly discuss the various cases of deriving refresh rates together with the task semantics of the different combinators
-
-\subsubsection{Parallel combinators} For the parallel composition of tasks we compute the intersection of the refresh intervals of the components as outlined in the definition of $\cap_{\textit{safe}}$.
-The operator \cleaninline{.\|\|.} in \cref{R:or} is the \emph{or}-combinator; the first subtask that produces a stable value determines the result of the composition.
-The operator \cleaninline{.&&.} in \cref{R:and} is the \emph{and}-operator. The result is the tuple containing both results when both subtasks have a stable value.
-The refresh rates of the parallel combinators have no direct relation with their task result.
+                       \right.
+       \]
+       \caption{Safe intersection operator}\label{equ:safe_intersect}
+\end{equ}
 
 \subsubsection{Sequential combinators}
-For the sequential composition of tasks we only have to look at the refresh rate of the current task on the left.
-The sequential composition operator \cleaninline{>>\|.} in \cref{R:seq} is similar to the monadic sequence operator \cleaninline{>>\|}.
-The operator \cleaninline{>>=.} in \cref{R:bind} provides the stable task result to the function on the right-hand side, similar to the monadic bind.
-The operator \cleaninline{>>~.} steps on an unstable value and is otherwise equal to \cleaninline{>>=.}.
-The step combinator \cleaninline{>>*.} in \cref{R:step} has a list of conditional actions that specify a new task.
+For the step combinator (\cref{R:step})---and all other derived sequential combinators---the refresh rate of the left-hand side task is taken since that is the only task that is rewritten.
+Only after stepping, the combinator rewrites to the right-hand side.
 
-\subsubsection{Repeat combinators}
+\subsubsection{Repeating combinators}
 The repeat combinators repeats their argument indefinitely.
-The combinator \cleaninline{rpeatEvery} guarantees the given delay between repetitions.
-The refresh rate is equal to the refresh rate of the current argument task.
-Only when \cleaninline{rpeatEvery} waits between the iterations of the argument the refresh interval is equal to the remaining delay time.
-
-\subsubsection{Other combinators}
-The refresh rate of the \cleaninline{delay} in \cref{R:delay} is equal to the remaining delay.
-Refreshing stable tasks can be delayed indefinitely, their value never changes.
-For other basic tasks, the values from \cref{tbl:refresh} apply.
-The values $r_l$ and $r_u$ in \cref{R:other} are the lower and upper bound of the rate.
-
-The refresh intervals associated with various steps of the thermostat program from \cref{lst:thermostat} are given in \cref{tbl:intervals}.
+As the \cleaninline{rpeat} task tree node already includes a rewrite rate (set to $\rewriterate{0}{0}$ for a default \cleaninline{rpeat}), both \cleaninline{rpeat} and \cleaninline{rpeatEvery} use the same task tree node and thus only one entry is required here.
+The derived refresh rate of the repeat combinator is the refresh rate of the child if it is unstable.
+Otherwise, the refresh rate is the embedded rate time minus the start time.
+In case of the \cleaninline{rpeat} task, the default refresh rate is $\rewriterate{0}{0}$ so the task immediately refreshes and starts the task again.
+\todo{netter opschrijven}
+
+\subsubsection{Delay combinators}
+Upon installation, a \cleaninline{delay} task is stored as a \cleaninline{waitUntil} task tree containing the time of installation added to the specified time to wait.
+Execution wise, it waits until the current time exceeds the time is greater than the argument time.
+
+\subsubsection{Other tasks}
+All other tasks are captured by \cref{R:other}.
+If the task is stable, rewriting can be delayed indefinitely since the value will not change anyway.
+In all other cases, the values from \cref{tbl:rewrite} apply where $r_l$ and $r_u$ represent the lower and upper bound of this rate.
+
+The rewrite intervals associated with various steps of the thermostat program from \cref{lst:thermostat} are given in \cref{tbl:intervals}.
 Those rewrite steps and intervals are circular, after step 2 we continue with step 0 again.
 Only the actual reading of the sensor with \cleaninline{temperature dht} offers the possibility for a non-zero delay.
 
+\subsection{Example}
 %%\begin{table}[tb]
 \begin{table}
        \centering
@@ -221,7 +232,7 @@ rpeat ( temperature dht >>~. \temp.
         writeD builtInLED (goal <. temp)
 )\end{lstClean}
                   &
-                  $\refreshrate{0}{0}$ \\
+                  $\rewriterate{0}{0}$ \\
                   %\hline
                1  &
                \begin{lstClean}[aboveskip=-2ex,belowskip=-2ex,frame=]
@@ -230,7 +241,7 @@ writeD builtInLED (goal <. temp) >>|.
 rpeat ( temperature dht >>~. \temp.
         writeD builtInLED (goal <. temp)
 )\end{lstClean}
-                  & $\refreshrate{0}{2000}$ \\
+                  & $\rewriterate{0}{2000}$ \\
                   %\hline
                2  &
                \begin{lstClean}[aboveskip=-2ex,belowskip=-2ex,frame=]
@@ -238,12 +249,12 @@ writeD builtInLED false >>|.
 rpeat ( temperature dht >>~. \temp.
         writeD builtInLED (goal <. temp)
 )\end{lstClean}
-               & $\refreshrate{0}{0}$ \\
+               & $\rewriterate{0}{0}$ \\
                \bottomrule
        \end{tabular}
 \end{table}
 
-\subsection{Tweaking refresh rates}
+\subsection{Tweaking rewrite rates}
 A tailor-made \gls{ADT} (see \cref{lst:interval}) determines the timing intervals for which the value is determined at runtime but the constructor is known at compile time.
 During compilation, the constructor of the \gls{ADT} is checked and code is generated accordingly.
 If it is \cleaninline{Default}, no extra code is generated.
@@ -252,19 +263,19 @@ In the case that there is a lower bound, i.e.\ the task must not be executed bef
 
 \begin{lstClean}[caption={The \gls{ADT} for timing intervals in \gls{MTASK}.},label={lst:interval}]
 :: TimingInterval v = Default
-                    | BeforeMs (v Int)         // yields [+$\refreshrate{0}{x}$+]
-                    | BeforeS  (v Int)         // yields [+$\refreshrate{0}{x \times 1000}$+]
-                    | ExactMs  (v Int)         // yields [+$\refreshrate{x}{x}$+]
-                    | ExactS   (v Int)         // yields [+$\refreshrate{0}{x \times 1000}$+]
-                    | RangeMs  (v Int) (v Int) // yields [+$\refreshrate{x}{y}$+]
-                    | RangeS   (v Int) (v Int) // yields [+$\refreshrate{x \times 1000}{y \times 1000}$+]
+                    | BeforeMs (v Int)         // yields [+$\rewriterate{0}{x}$+]
+                    | BeforeS  (v Int)         // yields [+$\rewriterate{0}{x \times 1000}$+]
+                    | ExactMs  (v Int)         // yields [+$\rewriterate{x}{x}$+]
+                    | ExactS   (v Int)         // yields [+$\rewriterate{0}{x \times 1000}$+]
+                    | RangeMs  (v Int) (v Int) // yields [+$\rewriterate{x}{y}$+]
+                    | RangeS   (v Int) (v Int) // yields [+$\rewriterate{x \times 1000}{y \times 1000}$+]
 \end{lstClean}
 
 \subsubsection{Sensors and \texorpdfstring{\glspl{SDS}}{shared data sources}}
-In some applications, it is necessary to read sensors or \glspl{SDS} at a different rate than the default rate given in \cref{tbl:refresh}, i.e.\ to customise the refresh rate.
-This is achieved by calling the access functions with a custom refresh rate as an additional argument (suffixed with the backtick (\cleaninline{`}))
+In some applications, it is necessary to read sensors or \glspl{SDS} at a different rate than the default rate given in \cref{tbl:rewrite}, i.e.\ to customise the rewrite rate.
+This is achieved by calling the access functions with a custom rewrite rate as an additional argument (suffixed with the backtick (\cleaninline{`}))
 The adaptions to other classes are similar and omitted for brevity.
-\Cref{lst:dht_ext} shows the extended \cleaninline{dht} and \cleaninline{dio} class definition with functions for custom refresh rates.
+\Cref{lst:dht_ext} shows the extended \cleaninline{dht} and \cleaninline{dio} class definition with functions for custom rewrite rates.
 
 \begin{lstClean}[caption={Auxiliary definitions to \cref{lst:gpio,lst:dht} for \gls{DHT} sensors and digital \gls{GPIO} with custom timing intervals.},label={lst:dht_ext}]
 class dht v where
@@ -299,7 +310,7 @@ devTask =
 \subsubsection{Repeating tasks}
 The task combinator \cleaninline{rpeat} restarts the child task in the evaluation if the previous produced a stable result.
 However, in some cases it is desirable to postpone the restart of the child.
-For this, the \cleaninline{rpeatEvery} task is introduced which receives an extra argument, the refresh rate, as shown in \cref{lst:rpeatevery}.
+For this, the \cleaninline{rpeatEvery} task is introduced which receives an extra argument, the rewrite rate, as shown in \cref{lst:rpeatevery}.
 Instead of immediately restarting the child once it yields a stable value, it checks whether the lower bound of the provided timing interval has passed since the start of the task\footnotemark.
 \footnotetext{In reality, it also compensates for time drift by taking into account the upper bound of the timing interval.
 If the task takes longer to stabilise than the upper bound of the timing interval, this upper bound is taken as the start of the task instead of the actual start.}
@@ -337,14 +348,14 @@ timedPulseNaive = declarePin D0 PMOutput \d0->
 \end{lstClean}
 
 \section{Task scheduling in the \texorpdfstring{\gls{MTASK}}{mTask} engine}
-The refresh rates from the previous section only tell us how much the next evaluation of the task can be delayed.
+The rewrite rates from the previous section only tell us how much the next evaluation of the task can be delayed.
 An \gls{IOT} edge devices executes multiple tasks may run interleaved.
 In addition, it has to communicate with a server to collect new tasks and updates of \glspl{SDS}.
-Hence, the refresh intervals cannot be used directly to let the microcontroller sleep.
+Hence, the rewrite intervals cannot be used directly to let the microcontroller sleep.
 Our scheduler has the following objectives.
 \begin{itemize}
        \item
-               Meet the deadline whenever possible, i.e.\ the system tries to execute every task before the end of its refresh interval.
+               Meet the deadline whenever possible, i.e.\ the system tries to execute every task before the end of its rewrite interval.
                Only too much work on the device might cause an overflow of the deadline.
        \item
                Achieve long sleep times. Waking up from sleep consumes some energy and takes some time.
@@ -352,17 +363,17 @@ Our scheduler has the following objectives.
        \item
                The scheduler tries to avoid unnecessary evaluations of tasks as much as possible.
                A task should not be evaluated now when its execution can also be delayed until the next time that the device is active.
-               That is, a task should preferably not be executed before the start of its refresh interval.
-               Whenever possible, task execution should even be delayed when we are inside the refresh interval as long as we can execute the task before the end of the interval.
+               That is, a task should preferably not be executed before the start of its rewrite interval.
+               Whenever possible, task execution should even be delayed when we are inside the rewrite interval as long as we can execute the task before the end of the interval.
        \item
                The optimal power state should be selected.
                Although a system uses less power in a deep sleep mode, it also takes more time and energy to wake up from deep sleep.
                When the system knows that it can sleep only a short time it is better to go to light sleep mode since waking up from light sleep is faster and consumes less energy.
 \end{itemize}
 
-The algorithm $\mathcal{R}$ from \cref{sec:deriving_refresh_rates} computes the evaluation rate of the current tasks.
+The algorithm $\mathcal{R}$ from \cref{sec:deriving_rewrite_rates} computes the evaluation rate of the current tasks.
 For the scheduler, we transform this interval to an absolute evaluation interval; the lower and upper bound of the start time of that task measured in the time of the \gls{IOT} edge device.
-We obtain those bounds by adding the current system time to the bounds of the computed refresh interval by algorithm $\mathcal{R}$.
+We obtain those bounds by adding the current system time to the bounds of the computed rewrite interval by algorithm $\mathcal{R}$.
 
 For the implementation, it is important to note that the evaluation of a task takes time.
 Some tasks are extremely fast, but other tasks require long computations and time-consuming communication with peripherals as well as with the server.
@@ -484,7 +495,7 @@ Only when an interrupt triggers, the program continues, writes the state to the
 #define INTERRUPTPIN 11
 #define DEBOUNCE 30[+\label{lst:arduino_interrupt:defs_to}+]
 
-volatile byte state = LOW;[+\label{lst:arduino_interrupt:state}+]
+volatile int state = LOW;[+\label{lst:arduino_interrupt:state}+]
 volatile bool cooldown = true;[+\label{lst:arduino_interrupt:cooldown}+]
 
 void setup() {[+\label{lst:arduino_interrupt:setup_fro}+]
@@ -519,8 +530,8 @@ class interrupt v where
 :: InterruptMode = Change | Rising | Falling | Low | High
 \end{lstClean}
 
-When the \gls{MTASK} device executes this task, it installs an \gls{ISR} and sets the refresh rate of the task to infinity, $\refreshrate{\infty}{\infty}$.
-The interrupt handler is set up in such a way that the refresh rate is changed to $\refreshrate{0}{0}$ once the interrupt triggers.
+When the \gls{MTASK} device executes this task, it installs an \gls{ISR} and sets the rewrite rate of the task to infinity, $\rewriterate{\infty}{\infty}$.
+The interrupt handler is set up in such a way that the rewrite rate is changed to $\rewriterate{0}{0}$ once the interrupt triggers.
 As a consequence, the task is executed on the next execution cycle.
 
 The \cleaninline{pirSwitch} function in \cref{lst:pirSwitch} creates, given an interval in \unit{\ms}, a task that reacts to motion detection by a \gls{PIR} sensor (connected to \gls{GPIO} pin 0) by lighting the \gls{LED} connected to \gls{GPIO} pin 13 for the given interval.
@@ -532,10 +543,10 @@ pirSwitch :: Int -> Main (MTask v Bool) | mtask v
 pirSwitch =
        declarePin D13 PMOutput \ledpin->
        declarePin D0 PMInput \pirpin->
-       {main = rpeat (      interrupt high pirpin
-                       >>|. writeD ledpin false
-                       >>|. delay (lit interval)
-                       >>|. writeD ledpin true) }
+       {main = rpeat (     interrupt high pirpin
+                      >>|. writeD ledpin false
+                      >>|. delay (lit interval)
+                      >>|. writeD ledpin true) }
 \end{lstClean}
 
 \subsection{\texorpdfstring{\Gls{MTASK}}{MTask} engine}
@@ -564,7 +575,7 @@ Furthermore, as the \gls{ISR} is supposed to be be very short, just a flag in th
 Interrupt event flags are processed at the beginning of the event loop, before tasks are executed.
 For each subscribed task, the task tree is searched for nodes listening for the particular interrupt.
 When found, the node is flagged and the pin status is written.
-Afterwards, the evaluation interval of the task is set to $\refreshrate{0}{0}$ and the task is reinsterted at the front of the scheduling queue to ensure rapid evaluation of the task.
+Afterwards, the evaluation interval of the task is set to $\rewriterate{0}{0}$ and the task is reinsterted at the front of the scheduling queue to ensure rapid evaluation of the task.
 Finally, the event is removed from the registration and the interrupt is disabled.
 The interrupt can be disabled as all tasks waiting for the interrupt become stable after firing.
 More occurrences of the interrupts do not change the value of the task as stable tasks keep the same value forever.