From: Mart Lubbers Date: Thu, 1 Dec 2022 10:26:26 +0000 (+0100) Subject: george comments X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;h=3369704052f2381076b72efb24d57a943172e729;p=phd-thesis.git george comments --- diff --git a/back/research_data_management.tex b/back/research_data_management.tex index 52de648..1481159 100644 --- a/back/research_data_management.tex +++ b/back/research_data_management.tex @@ -10,25 +10,25 @@ This thesis research has been carried out under the research data management pol The following research datasets have been produced during this PhD research: \begin{itemize} - \item \fullref{chp:classy_deep_embedding} + \item \Fullref{chp:classy_deep_embedding} \begin{itemize} \item \rdmentry{\mlubbers}{2022} {Literate Haskell/lhs2\TeX{} source code for the paper ``Deep Embedding with Class'': TFP 2022} {Zenodo}{10.5281/zenodo.6650880} %chktex 8 - \item \fullref{sec:classy_reprise}: + \item \Fullref{sec:classy_reprise}: \begin{itemize} \item \rdmentry{\mlubbers}{2022} {\todo[inline]{replace with actual name}} {Zenodo}{10.5281/zenodo.7277498} %chktex 8 \end{itemize} \end{itemize} - \item \fullref{chp:first-class_datatypes}: + \item \Fullref{chp:first-class_datatypes}: \begin{itemize} \item \rdmentry{\mlubbers}{2022} {Code for the paper ``First-Class Data Types in Shallow Embedded Domain-Specific Languages using Metaprogramming'': IFL 2022} {Zenodo}{10.5281/zenodo.6416747} \end{itemize} - \item \fullref{prt:top}: + \item \Fullref{prt:top}: \begin{itemize} \item \rdmentry{\mlubbers; \pkoopman; \rplasmeijer}{2020} {Source code for the mTask language} @@ -43,7 +43,7 @@ The following research datasets have been produced during this PhD research: {Source code for the interpreted mTask language} {DANS}{10.17026/dans-zrn-2wv3} %chktex 8 \end{itemize} - \item \fullref{prt:tvt}: + \item \Fullref{prt:tvt}: \begin{itemize} \item \rdmentry{\mlubbers; \pkoopman; \aramsingh; \jsinger; \ptrinder}{2021} {Source code, line counts and memory statistics for CRS, CWS, CRTS and CWTS} diff --git a/dsl/class.tex b/dsl/class.tex index 5931da7..542403b 100644 --- a/dsl/class.tex +++ b/dsl/class.tex @@ -870,9 +870,8 @@ e1 :: (Typeable c, UsingExt '[Neg, Subst]) => Expr c Giving an instance for \haskelllhstexinline{Interp} for \haskelllhstexinline{DataType} that uses the extensions \haskelllhstexinline{e_1, e2, ...} and depends on interpretations \haskelllhstexinline{i_1,i_2, ...} is done as follows: \begin{lstHaskellLhstex} -instance ( UsingExt '[e_1, e_2, ...] s - , DependsOn '[i_1, i_2, ...] s - ) => Interp (DataType s) where +instance ( UsingExt '[e_1, e_2, ...] s, DependsOn '[i_1, i_2, ...] s) + => Interp (DataType s) where ... \end{lstHaskellLhstex} diff --git a/dsl/first.tex b/dsl/first.tex index 4b508c5..33e7478 100644 --- a/dsl/first.tex +++ b/dsl/first.tex @@ -29,7 +29,7 @@ In contrast, adding language constructs requires changing the data type and upda Shallow embedding on the other hand models the language constructs as functions with the semantics embedded. Consequently, adding a construct is easy, i.e.\ it only entails adding another function. Contrarily, adding semantics requires adapting all language constructs. -Lifting the functions to type classes, i.e.\ parametrising the constructs over the semantics, allows extension of the language both in constructs and in semantics orthogonally. This advanced style of embedding is called tagless-final or class-based shallow embedding~\citep{kiselyov_typed_2012}. +Lifting the functions to type classes, i.e.\ parametrising the constructs over the semantics, allows extension of the language both in constructs and in semantics orthogonally. This advanced style of embedding is called tagless-final or class-based shallow embedding \citep{kiselyov_typed_2012}. While it is often possible to lift values of a user-defined data type to a value in the \gls{DSL}, it is not possible to interact with it using \gls{DSL} constructs, they are not first-class citizens. @@ -41,7 +41,7 @@ Concretely, it is not possible to \end{enumerate*} The functions for this are simply not available automatically in the embedded language. For some semantics---such as an interpreter---it is possible to directly lift the functions from the host language to the \gls{DSL}. -In other cases---e.g.\ \emph{compiling} \glspl{DSL} such as a compiler or a printer---this is not possible~\citep{elliott_compiling_2003}. %the torget this is not possible. cannot just be lifted from the host language to the \gls{DSL} so it requires a lot of boilerplate to define and implement them. +In other cases---e.g.\ \emph{compiling} \glspl{DSL} such as a compiler or a printer---this is not possible \citep{elliott_compiling_2003}. %the torget this is not possible. cannot just be lifted from the host language to the \gls{DSL} so it requires a lot of boilerplate to define and implement them. Thus, all of the operations on the data type have to be defined by hand requiring a lot of plumbing and resulting in a lot of boilerplate code. To relieve the burden of adding all these functions, metaprogramming\nobreak---\nobreak\hskip0pt and custom quasiquoters---can be used. @@ -60,7 +60,7 @@ Tagless-final embedding is an upgrade to standard shallow embedding achieved by As a result, views on the \gls{DSL} are data types implementing these classes. To illustrate the technique, a simple \gls{DSL}, a language consisting of literals and addition, is outlined. -This language, implemented according to the tagless-final style~\citep{carette_finally_2009} in \gls{HASKELL}~\citep{peyton_jones_haskell_2003} consists initially only of one type class containing two functions. +This language, implemented according to the tagless-final style \citep{carette_finally_2009} in \gls{HASKELL} \citep{peyton_jones_haskell_2003} consists initially only of one type class containing two functions. The \haskellinline{lit} function lifts values from the host language to the \gls{DSL} domain. The class constraint \haskellinline{Show} is enforced on the type variable \haskellinline{a} to make sure that the value can be printed. The infix function \haskellinline{+.} represents the addition of two expressions in the \gls{DSL}. @@ -117,9 +117,9 @@ First a data type representing the semantics is defined. In this case, the print \footnotetext{% In this case a \haskellinline{newtype} is used instead of regular \haskellinline{data} declarations. \haskellinline{newtype}s are special data types only consisting a single constructor with one field to which the type is isomorphic. - During compilation the constructor is completely removed resulting in no overhead~\citep[\citesection{4.2.3}]{peyton_jones_haskell_2003}. + During compilation the constructor is completely removed resulting in no overhead \citep[\citesection{4.2.3}]{peyton_jones_haskell_2003}. } -Since the language is typed, the printer data type has to have a type variable but it is only used during typing---i.e.\ a phantom type~\citep{leijen_domain_2000}: +Since the language is typed, the printer data type has to have a type variable but it is only used during typing---i.e.\ a phantom type \citep{leijen_domain_2000}: \begin{lstHaskell} newtype Printer a = P { runPrinter :: String } @@ -131,18 +131,18 @@ The class instances for \haskellinline{Expr} and \haskellinline{Div} for the pre instance Expr Printer where lit a = P (show a) (+.) l r = P ("(" ++ runPrinter l - ++ "+" ++ runPrinter r ++ ")") + ++ "+" ++ runPrinter r ++ ")") instance Div Printer where (/.) l r = P ("(" ++ runPrinter l - ++ "/" ++ runPrinter r ++ ")") + ++ "/" ++ runPrinter r ++ ")") \end{lstHaskell} \subsection{Functions} Adding functions to the language is achieved by adding a multi-parameter class to the \gls{DSL}. The type of the class function allows for the implementation to only allow first order function by supplying the arguments in a tuple. Furthermore, with the \haskellinline{:-} operator the syntax becomes usable. -Finally, by defining the functions as a \gls{HOAS} type safety is achieved~\citep{pfenning_higher-order_1988,chlipala_parametric_2008}. +Finally, by defining the functions as a \gls{HOAS} type safety is achieved \citep{pfenning_higher-order_1988,chlipala_parametric_2008}. The complete definition looks as follows: \begin{lstHaskell} @@ -222,8 +222,7 @@ class ListDSL v where cons :: v a -> v (List a) -> v (List a) -- deconstructors unNil :: v (List a) -> v b -> v b - unCons :: v (List a) - -> (v a -> v (List a) -> v b) -> v b + unCons :: v (List a) -> (v a -> v (List a) -> v b) -> v b -- constructor predicates isNil :: v (List a) -> v Bool isCons :: v (List a) -> v Bool @@ -239,8 +238,7 @@ instance ListDSL Maybe where nil = Just Nil cons hd tl = Cons <$> hd <*> tl unNil d f = d >>= \Nil->f - unCons d f = d - >>= \(Cons hd tl)->f (Just hd) (Just tl) + unCons d f = d >>= \(Cons hd tl)->f (Just hd) (Just tl) isNil d = d >>= \case[+\footnotemark+] Nil -> Just True _ -> Just False @@ -253,23 +251,23 @@ instance ListDSL Maybe where } Adding these classes and their corresponding instances is tedious and results in boilerplate code. -We therefore resort to metaprogramming, and in particular \gls{TH}~\citep{sheard_template_2002} to alleviate this burden. +We therefore resort to metaprogramming, and in particular \gls{TH} \citep{sheard_template_2002} to alleviate this burden. \section{Template metaprogramming} Metaprogramming is a special flavour of programming where programs have the ability to treat and manipulate programs or program fragments as data. -There are several techniques to facilitate metaprogramming, moreover it has been around for many years now~\citep{lilis_survey_2019}. -Even though it has been around for many years, it is considered complex~\citep{sheard_accomplishments_2001}. +There are several techniques to facilitate metaprogramming, moreover it has been around for many years now \citep{lilis_survey_2019}. +Even though it has been around for many years, it is considered complex \citep{sheard_accomplishments_2001}. -\gls{TH} is GHC's de facto metaprogramming system, implemented as a compiler extension together with a library~\citep{sheard_template_2002}\citep[\citesection{6.13.1}]{ghc_team_ghc_2021}. +\gls{TH} is GHC's de facto metaprogramming system, implemented as a compiler extension together with a library \citep{sheard_template_2002}\citep[\citesection{6.13.1}]{ghc_team_ghc_2021}. Readers already familiar with \gls{TH} can safely skip this section. \gls{TH} adds four main concepts to the language, na\-me\-ly AST data types, splicing, quasiquotation and reification. With this machinery, regular \gls{HASKELL} functions can be defined that are called at compile time, inserting generated code into the {AST}. These functions are monadic functions operating in the \haskellinline{Q} monad. -The \haskellinline{Q} monad facilitates failure, reification and fresh identifier generation for hygienic macros~\citep{kohlbecker_hygienic_1986}. +The \haskellinline{Q} monad facilitates failure, reification and fresh identifier generation for hygienic macros \citep{kohlbecker_hygienic_1986}. Within the \haskellinline{Q} monad, capturable and non-capturable identifiers can be generated using the \haskellinline{mkName} and \haskellinline{newName} functions respectively. The \emph{Peter Parker principle}\footnote{With great power comes great responsibility.} holds for the \haskellinline{Q} monad as well because it executes at compile time and is very powerful. -For example it can subvert module boundaries, thus accessing constructors that were hidden; access the structure of abstract types; and it may cause side effects during compilation because it is possible to call \haskellinline{IO} operations~\citep{terei_safe_2012}. +For example it can subvert module boundaries, thus accessing constructors that were hidden; access the structure of abstract types; and it may cause side effects during compilation because it is possible to call \haskellinline{IO} operations \citep{terei_safe_2012}. To achieve the goal of embedding data types in a \gls{DSL} we refrain from using these \emph{unsafe} features. \subsubsection{Data types} @@ -279,17 +277,15 @@ Often, a data type is suffixed with the context, e.g.\ there is a \haskellinline To give an impression of these data types, a selection of data types available in \gls{TH} is given below: \begin{lstHaskell} -data Dec = FunD Name [Clause] | DataD Cxt Name ... - | SigD Name Type | ClassD Cxt Name | ... +data Dec = FunD Name [Clause] | DataD Cxt Name ... | SigD Name Type + | ClassD Cxt Name | ... data Clause = Clause [Pat] Body [Dec] -data Pat = LitP Lit | VarP Name | TupP [Pat] - | WildP | ListP [Pat] | ... +data Pat = LitP Lit | VarP Name | TupP [Pat] | WildP | ListP [Pat] | ... data Body = GuardedB [(Guard, Exp)] | NormalB Exp data Guard = NormalG Exp | PatG [Stmt] -data Exp = VarE Name | LitE Lit | AppE Exp Exp - | TupE [Maybe Exp] | LamE [Pat] Exp | ... -data Lit = CharL Char | StringL String - | IntegerL Integer | ... +data Exp = VarE Name | LitE Lit | AppE Exp Exp | TupE [Maybe Exp] + | LamE [Pat] Exp | ... +data Lit = CharL Char | StringL String | IntegerL Integer | ... \end{lstHaskell} To ease creating AST data types in the \haskellinline{Q} monad, lowercase variants of the constructors are available that lift the constructor to the \haskellinline{Q} monad as. @@ -318,7 +314,7 @@ tsel field total = do \end{lstHaskell} \subsubsection{Quasiquotation} -Another key concept of \gls{TH} is Quasiquotation, the dual of splicing~\citep{bawden_quasiquotation_1999}. +Another key concept of \gls{TH} is Quasiquotation, the dual of splicing \citep{bawden_quasiquotation_1999}. While it is possible to construct entire programs using the provided data types, it is a little cumbersome. Using \emph{Oxford brackets} (\verb#[|# \ldots\verb#|]#) or single or double apostrophes, verbatim \gls{HASKELL} code can be entered that is converted automatically to the corresponding AST nodes easing the creation of language constructs. Depending on the context, different quasiquotes are used: @@ -332,7 +328,7 @@ Depending on the context, different quasiquotes are used: \end{itemize*}. It is possible to escape the quasiquotes again by splicing. Variables defined within quasiquotes are always fresh---as if defined with \haskellinline{newName}---but it is possible to capture identifiers using \haskellinline{mkName}. -For example, \haskellinline{[|\\x->x|]} translates to \haskellinline{newName "x" >>= \\x->lamE [varP x] (varE x)} and does not interfere with other \haskellinline{x}s already defined. +For example, \haskellinline{[\|\\x->x\|]} translates to \haskellinline{newName "x" >>= \\x->lamE [varP x] (varE x)} and does not interfere with other \haskellinline{x}s already defined. \subsubsection{Reification} Reification is the act of querying the compiler for information about a certain name. @@ -366,22 +362,17 @@ From this structure of the type, \haskellinline{genDSL'} generates a list of dec \begin{lstHaskell} genDSL :: Name -> Q [Dec] genDSL name = reify name >>= \case - TyConI (DataD cxt typeName tvs mkind - constructors derives) - -> mapM getConsName constructors - >>= \d->genDSL' tvs typeName d + TyConI (DataD cxt typeName tvs mkind constructors derives) + -> mapM getConsName constructors >>= \d->genDSL' tvs typeName d t -> fail ("genDSL does not support: " ++ show t) getConsName :: Con -> Q (Name, [VarBangType]) getConsName (NormalC consName fs) = pure (consName, - [(adtFieldName consName i, b, t) - | (i, (b, t))<-[0..] `zip` fs]) + [(adtFieldName consName i, b, t) | (i, (b, t))<-[0..] `zip` fs]) getConsName (RecC consName fs) = pure (consName, fs) -getConsName c - = fail ("genDSL does not support: " ++ show c) +getConsName c = fail ("genDSL does not support: " ++ show c) -genDSL' :: [TyVarBndr] -> Name -> [(Name, [VarBangType])] - -> Q [Dec] +genDSL' :: [TyVarBndr] -> Name -> [(Name, [VarBangType])] -> Q [Dec] genDSL' typeVars typeName constructors = sequence [ mkClass, mkInterpreter, mkPrinter, ... ] where @@ -439,8 +430,7 @@ Then, the constructor type is constructed by folding over the lifted field types \begin{lstHaskell} mkConstructor :: Name -> [VarBangType] -> Q Dec -mkConstructor n fs - = sigD (constructorName n) (mkCFun fs res) +mkConstructor n fs = sigD (constructorName n) (mkCFun fs res) mkCFun :: [VarBangType] -> Q Type -> Q Type mkCFun fs res = foldr (\x y->[t|$x -> $y|]) @@ -468,8 +458,7 @@ They all have the same type: \begin{lstHaskell} mkPredicate :: Name -> Q Dec -mkPredicate n = sigD (predicateName n) - [t|$res -> $v Bool|] +mkPredicate n = sigD (predicateName n) [t|$res -> $v Bool|] \end{lstHaskell} \subsection{Interpreter instance generation}\label{sec_fcd:interpreter} @@ -531,8 +520,7 @@ mkDeconstructor consName fs = do fresh <- mapM (newName . nameBase . fst3) fs fun (deconstructorName consName) [varP d, varP f] [|$(varE d) >>= \($(match f))->$(fapp f fresh)|] - where fapp f = foldl appE (varE f) - . map (\f->[|pure $(varE f)|]) + where fapp f = foldl appE (varE f) . map (\f->[|pure $(varE f)|]) match f = pure (ConP consName (map VarP f)) \end{lstHaskell} @@ -669,7 +657,7 @@ main = sum (Cons 38 (Cons 4 Nil)) \subsection{Custom quasiquoters} The syntax burden of \glspl{EDSL} can be reduced using quasiquotation. In \gls{TH}, quasiquotation is a convenient way to create \gls{HASKELL} language constructs by entering them verbatim using Oxford brackets. -However, it is also possible to create so-called custom quasiquoters~\citep{mainland_why_2007}. +However, it is also possible to create so-called custom quasiquoters \citep{mainland_why_2007}. If the programmer writes down a fragment of code between tagged \emph{Oxford brackets}, the compiler executes the associated quasiquoter functions at compile time. A quasiquoter is a value of the following data type: @@ -709,10 +697,10 @@ bin = QuasiQuoter { quoteExp = parseBin } Custom quasiquoters allow the \gls{DSL} user to enter fragments verbatim, bypassing the syntax of the host language. Pattern matching in general is not suitable for a custom quasiquoter because it does not really fit in one of the four syntactic categories for which custom quasiquoter support is available. However, a concrete use of pattern matching, interesting enough to be beneficial, but simple enough for a demonstration is the \emph{simple case expression}, a case expression that does not contain nested patterns and is always exhaustive. -They correspond to a multi-way conditional expressions and can thus be converted to \gls{DSL} constructs straightforwardly~\citep[\citesection{4.4}]{peyton_jones_implementation_1987}. +They correspond to a multi-way conditional expressions and can thus be converted to \gls{DSL} constructs straightforwardly \citep[\citesection{4.4}]{peyton_jones_implementation_1987}. In contrast to the binary literal quasiquoter example, we do not create the parser by hand. -The parser combinator library \emph{parsec} is used instead to ease the creation of the parser~\citep{leijen_parsec_2001}. +The parser combinator library \emph{parsec} is used instead to ease the creation of the parser \citep{leijen_parsec_2001}. First the location of the quasiquoted code is retrieved using the \haskellinline{location} function that operates in the \haskellinline{Q} monad. This location is inserted in the parsec parser so that errors are localised in the source code. Then, the \haskellinline{expr} parser is called that returns an \haskellinline{Exp} in the \haskellinline{Q} monad. @@ -787,14 +775,14 @@ program \end{lstHaskell} \section{Related work} -Generic or polytypic programming is a promising technique at first glance for automating the generation of function implementations~\citep{lammel_scrap_2003}. +Generic or polytypic programming is a promising technique at first glance for automating the generation of function implementations \citep{lammel_scrap_2003}. However, while it is possible to define a function that works on all first-order types, adding a new function with a new name to the language is not possible. This does not mean that generic programming is not useable for embedding pattern matches. In generic programming, types are represented as sums of products and using this representation it is possible to define pattern matching functions. For example, \citet{rhiger_type-safe_2009} showed a method for expressing statically typed pattern matching using typed higher-order functions. If not the host language but the \gls{DSL} contains higher order functions, the same technique could be applied to port pattern matching to \glspl{DSL} though using an explicit sums of products representation. -\Citeauthor{atkey_unembedding_2009} describe embedding pattern matching in a \gls{DSL} by giving patterns an explicit representation in the \gls{DSL} by using pairs, sums and injections~\citep[\citesection{3.3}]{atkey_unembedding_2009}. +\Citeauthor{atkey_unembedding_2009} describe embedding pattern matching in a \gls{DSL} by giving patterns an explicit representation in the \gls{DSL} by using pairs, sums and injections \citep[\citesection{3.3}]{atkey_unembedding_2009}. \Citet{mcdonell_embedded_2022} extends on this idea, resulting in a very similar but different solution to ours. They used the technique that \citeauthor{atkey_unembedding_2009} showed and applied it to deep embedding using the concrete syntax of the host language. @@ -818,7 +806,7 @@ They all differ slightly in functionality from our domain and can be divided int \subsubsection{Generating extra code} Using \gls{TH} or other metaprogramming systems it is possible to add extra code to your program. -The original \gls{TH} paper showed that it is possible to create variadic functions such as \haskellinline{printf} using \gls{TH} that would be almost impossible to define without~\citep{sheard_template_2002}. +The original \gls{TH} paper showed that it is possible to create variadic functions such as \haskellinline{printf} using \gls{TH} that would be almost impossible to define without \citep{sheard_template_2002}. \Citet{hammond_automatic_2003} used \gls{TH} to generate parallel programming skeletons. In practise, this means that the programmer selects a skeleton and, at compile time, the code is massaged to suit the pattern and information about the environment is inlined for optimisation. @@ -828,7 +816,7 @@ From a specification of the grammar, given in verbatim using a custom quasiquote \Citet{shioda_libdsl_2014} used metaprogramming in the D programming language to create a \gls{DSL} toolkit. They also programmatically generate parsers and a backend for either compiling or interpreting the \gls{IR}. \Citet{blanchette_liquid_2022} use \gls{TH} to simplify the development of Liquid \gls{HASKELL} proofs. -\Citet{folmer_high-level_2022} used \gls{TH} to synthesize C$\lambda$aSH~\citep{baaij_digital_2015} abstract syntax trees to be processed. +\Citet{folmer_high-level_2022} used \gls{TH} to synthesize C$\lambda$aSH \citep{baaij_digital_2015} abstract syntax trees to be processed. In similar fashion, \citet{materzok_generating_2022} used \gls{TH} to translate YieldFSM programs to {C$\lambda$aSH}. \subsubsection{Optimisation} @@ -859,7 +847,7 @@ They created a meta level \gls{DSL} to describe rewrite rules on \gls{HASKELL} s \subsubsection{Quasiquotation} By means of quasiquotation, the host language syntax that usually seeps through the embedding can be hidden. -The original \gls{TH} quasiquotation paper~\citep{mainland_why_2007} shows how this can be done for regular expressions, not only resulting in a nicer syntax but syntax errors are also lifted to compile time instead of run time. +The original \gls{TH} quasiquotation paper \citep{mainland_why_2007} shows how this can be done for regular expressions, not only resulting in a nicer syntax but syntax errors are also lifted to compile time instead of run time. Also, \citet{kariotis_making_2008} used \gls{TH} to automatically construct monad stacks without having to resort to the monad transformers library which requires advanced type system extensions. \Citet{najd_everything_2016} uses the compile time to be able to do normalisation for a \gls{DSL}, dubbing it \glspl{QDSL}. @@ -868,10 +856,10 @@ They utilise the quasiquation facilities of \gls{TH} to convert \gls{HASKELL} \g Using quasiquotation, they make a complicated embedding of non-linear pattern matching available through a simple lens. \subsubsection{\texorpdfstring{\glsxtrlong{TTH}}{Typed Template Haskell}}\label{ssec_fcd:typed_template_haskell} -\gls{TTH} is a very recent extension/alternative to normal \gls{TH}~\citep{pickering_multi-stage_2019,xie_staging_2022}. +\gls{TTH} is a very recent extension/alternative to normal \gls{TH} \citep{pickering_multi-stage_2019,xie_staging_2022}. Where in \gls{TH} you can manipulate arbitrary parts of the syntax tree, add top-level splices of data types, definitions and functions, in \gls{TTH} the programmer can only splice expressions but the abstract syntax tree fragments representing the expressions are well-typed by construction instead of untyped. -\Citet{pickering_staged_2020} implemented staged compilation for the \emph{generics-sop}~\citep{de_vries_true_2014} generics library to improve the efficiency of the code using \gls{TTH}. +\Citet{pickering_staged_2020} implemented staged compilation for the \emph{generics-sop} \citep{de_vries_true_2014} generics library to improve the efficiency of the code using \gls{TTH}. \Citet{willis_staged_2020} used \gls{TTH} to remove the overhead of parsing combinators. \section{Discussion} @@ -891,11 +879,11 @@ However, by making use of modern parser combinator libraries, this overhead is l For future work, it would be interesting to see how generating boilerplate for user-defined data types translates from shallow embedding to deep embedding. In deep embedding, the language constructs are expressed as data types in the host language. Adding new constructs, e.g.\ constructors, deconstructors, and constructor tests, for the user-defined data type therefore requires extending the data type. -Techniques such as data types \`a la carte~\citep{swierstra_data_2008} and open data types~\citep{loh_open_2006} show that it is possible to extend data types orthogonally but whether metaprogramming can still readily be used is something that needs to be researched. +Techniques such as data types \`a la carte \citep{swierstra_data_2008} and open data types \citep{loh_open_2006} show that it is possible to extend data types orthogonally but whether metaprogramming can still readily be used is something that needs to be researched. It may also be possible to implemented (parts) of the boilerplate generation using \gls{TTH} (see \cref{ssec_fcd:typed_template_haskell}) to achieve more confidence in the type correctness of the implementation. Another venue of research is to try to find the limits of this technique regarding richer data type definitions. -It would be interesting to see whether it is possible to apply the technique on data types with existentially quantified type variables or full-fledged generalised \glspl{ADT}~\citep{hinze_fun_2003}. +It would be interesting to see whether it is possible to apply the technique on data types with existentially quantified type variables or full-fledged generalised \glspl{ADT} \citep{hinze_fun_2003}. It is not possible to straightforwardly lift the deconstructors to type classes because existentially quantified type variables will escape. Rank-2 polymorphism offers tools to define the types in such a way that this is not the case anymore. However, implementing compiling views on the \gls{DSL} is complicated because it would require inventing values of an existentially quantified type variable to satisfy the type system which is difficult. diff --git a/glossaries.tex b/glossaries.tex index 3184d45..ccc274e 100644 --- a/glossaries.tex +++ b/glossaries.tex @@ -3,12 +3,12 @@ % \newacronym[type=\glsdefaulttype,#1]{#2}{#3}{#4} \newabbreviation[#1]{#2}{#3}{#4} } -\myacronym{3COWS}{3COWS}{The three ``CO'' (Composability, Comprehensibility, Correctness) winter school} +\myacronym[category=noexpand]{3COWS}{3COWS}{The three ``CO'' (Composability, Comprehensibility, Correctness) winter school} \myacronym{ADC}{ADC}{analog-to-digital converter} \myacronym{ADT}{ADT}{algebraic data type} \myacronym{API}{API}{application programming interface} \myacronym{ARDSL}{ARDSL}{\gls{ARDUINO} \glsxtrshort{DSL}} -\myacronym{CEFP}{CEFP}{central European summer school of \glsxtrlong{FP}} +\myacronym[category=noexpand]{CEFP}{CEFP}{Central European Summer School of \glsxtrlong{FP}} \myacronym{CRS}{CRS}{\gls{CLEAN} Raspberry Pi system} \myacronym{CRTS}{CRTS}{\gls{CLEAN} Raspberry Pi temperature sensor} \myacronym{CWS}{CWS}{\gls{CLEAN} \gls{WEMOS} system} @@ -27,14 +27,14 @@ \myacronym{GUI}{GUI}{graphical \glsxtrlong{UI}} \myacronym{HOAS}{HOAS}{high-order abstract syntax} \myacronym{IOT}{Io\kern-.3mmT}{internet of things} -\myacronym{IDE}{IDE}{integrated development environment} -\myacronym{IO}{I/O}{input/output} +\myacronym[category=noexpand]{IDE}{IDE}{integrated development environment} +\myacronym[category=noexpand]{IO}{I/O}{input/output} \myacronym{IR}{IR}{intermediate representation} \myacronym{ISR}{ISR}{interrupt service routine} \myacronym{LEAN}{LEAN}{language of East-Anglia and Nijmegen} \myacronym[prefixfirst={a\ },prefix={an\ }]{LED}{LED}{light-emitting diode} \myacronym{OLED}{OLED}{organic \glsxtrlong{LED}} -\myacronym{OS}{OS}{operating system} +\myacronym[category=noexpand]{OS}{OS}{operating system} \myacronym{OTA}{OTA}{over-the-air} \myacronym{PIR}{PIR}{passive infrared} \myacronym{PRS}{PRS}{\gls{PYTHON} Raspberry Pi system} @@ -42,7 +42,7 @@ \myacronym{PRTS}{PRTS}{\gls{PYTHON} Raspberry Pi temperature sensor} \myacronym{PWTS}{PWTS}{\gls{MICROPYTHON} \gls{WEMOS} temperature sensor} \myacronym{QDSL}{QDSL}{quoted \glsxtrshort{DSL}} -\myacronym{RAM}{RAM}{random-access memory} +\myacronym[category=noexpand]{RAM}{RAM}{random-access memory} \myacronym{RFID}{RFID}{radio-frequency identification} \myacronym{RTOS}{RTOS}{real-time \glsxtrshort{OS}} \myacronym{RTS}{RTS}{run-time system} @@ -50,7 +50,7 @@ \myacronym[prefixfirst={a\ },prefix={an\ }]{SN}{SN}{sensor network} \myacronym{SLOC}{SLOC}{source lines of code} \myacronym{TH}{TH}{Template \gls{HASKELL}} -\myacronym{TCP}{TCP}{transmission control protocol} +\myacronym[category=noexpand]{TCP}{TCP}{transmission control protocol} \myacronym{TOP}{TOP}{task-oriented programming} \myacronym{TOSD}{TOSD}{task-oriented software development} \myacronym{LSOC}{LSOC}{layered separation of concerns} @@ -64,94 +64,85 @@ % Glossaries \newglossaryentry{ABC}{% name=ABC, - description={is \gls{CLEAN}'s intermediate graph-rewriting language}, + description={- \gls{CLEAN}'s intermediate graph-rewriting language}, } \newglossaryentry{MTASK}{% name=mTask, - description={is a \glsxtrshort{TOP} \glsxtrshort{EDSL} for microcontrollers integrated with the \gls{ITASK} system}, + description={- a \glsxtrshort{TOP} \glsxtrshort{EDSL} for microcontrollers integrated with the \gls{ITASK} system}, } \newglossaryentry{ITASK}{% name=iTask, - description={is a \glsxtrshort{TOP} \glsxtrshort{EDSL} for creating distributed multi-user collaborative web applications}, + description={- a \glsxtrshort{TOP} \glsxtrshort{EDSL} for creating distributed multi-user collaborative web applications}, } \newglossaryentry{TOPHAT}{% name=TopHat, - description={is a \glsxtrshort{TOP} language designed to formally capture the essence of \gls{TOP}} + description={- a \glsxtrshort{TOP} language designed to formally capture the essence of \gls{TOP}} } \newglossaryentry{CLEAN}{% name=Clean, - description={Clean \glsxtrlong{LEAN}, a pure lazy \glsxtrlong{FP} language based on graph rewriting} + description={- Clean \glsxtrlong{LEAN}, a pure lazy \glsxtrlong{FP} language based on graph rewriting} } \newglossaryentry{HASKELL}{% name=Haskell, - description={is a pure lazy \glsxtrlong{FP} language designed by a committe as a concept language} + description={- a pure lazy \glsxtrlong{FP} language designed by a committe as a concept language} } \newglossaryentry{HASKELL98}{% name=Haskell98, - description={is a standardised version of \gls{HASKELL}}, + description={- a standardised version of \gls{HASKELL}}, } \newglossaryentry{ARDUINO}{% name=Arduino, - description={is a widely used framework for programming microcontrollers} + description={- a widely used framework for programming microcontrollers} } \newglossaryentry{MBED}{% name=mbed, - description={is a widely used framework for programming microcontrollers designed for ARM cortex-M} + description={- a widely used framework for programming microcontrollers designed for ARM cortex-M} } \newglossaryentry{CPP}{ name=C\texttt{++}, - description={is a general-purpose imperative programming language based on \gls{C}} + description={- a general-purpose imperative programming language based on \gls{C}} } \newglossaryentry{C}{ name=C, - description={is a general-purpose imperative programming} + description={- a general-purpose imperative programming} } \newglossaryentry{I2C}{ name=I\textsuperscript{2}C, - description={(Inter-Integrated Circuit) is a simple serial communication protocol often used to connect sensors to microcontrollers} + description={(Inter-Integrated Circuit) {-} a simple serial communication protocol often used to connect sensors to microcontrollers} } \newglossaryentry{SPI}{ name=SPI, - description={(Serial Peripheral Interface) is a synchronous serial communication protocol often used to connect sensors to microcontrollers} + description={(Serial Peripheral Interface) {-} a synchronous serial communication protocol often used to connect sensors to microcontrollers} } \newglossaryentry{TINYML}{ name=TinyML, - description={is a deep learning framework for microcontrollers} + description={- a deep learning framework for microcontrollers} } \newglossaryentry{PYTHON}{ name=Python, - description={is a multi-paradigm interpreted programming language} + description={- a multi-paradigm interpreted programming language} } \newglossaryentry{MICROPYTHON}{ name=MicroPython, - description={is a \gls{PYTHON} implementation tailored for microcontrollers} + description={- a \gls{PYTHON} implementation tailored for microcontrollers} } \newglossaryentry{FREERTOS}{ name=FreeRTOS, - description={is an open-source \gls{RTOS} for microcontrollers} + description={- an open-source \gls{RTOS} for microcontrollers} } \newglossaryentry{ONEWIRE}{ name=1-wire, - description={is simple single wire communication protocol often used to connect sensors to microcontrollers} + description={- a simple single wire communication protocol often used to connect sensors to microcontrollers} } \newglossaryentry{JSON}{ name=JSON, - description={(JavaScript Object Notation) is a open data interchange format using human readable text} + description={(JavaScript Object Notation) {-} a open data interchange format using human readable text} } \newglossaryentry{MQTT}{ name=MQTT, - description={(MQ Telemetry Transport) is a publish-subscribe network protocol designed for resource constrained devices} + description={(MQ Telemetry Transport) {-} a publish-subscribe network protocol designed for resource constrained devices} } \newglossaryentry{WEMOS}{ name=WEMOS, - description={is a popular ESP8266 microcontroller based prototyping platform supporting \gls{ARDUINO}.} + description={- a popular ESP8266 microcontroller based prototyping platform supporting \gls{ARDUINO}.} } - -% Never expand -\glsunset{3COWS} -\glsunset{CEFP} -\glsunset{TCP} -\glsunset{IDE} -\glsunset{IO} -\glsunset{OS} -\glsunset{RAM} diff --git a/hyphenation.tex b/hyphenation.tex index 2c581e7..bba16d1 100644 --- a/hyphenation.tex +++ b/hyphenation.tex @@ -6,4 +6,5 @@ me-ta-pro-gram-ming re-i-fi-ca-tion pro-gram-mer + Nij-me-gen } diff --git a/img/1.png b/img/1.png new file mode 100644 index 0000000..92eb237 Binary files /dev/null and b/img/1.png differ diff --git a/img/2.png b/img/2.png new file mode 100644 index 0000000..2ec874c Binary files /dev/null and b/img/2.png differ diff --git a/img/3.png b/img/3.png new file mode 100644 index 0000000..ca1fefd Binary files /dev/null and b/img/3.png differ diff --git a/intro/intro.tex b/intro/intro.tex index 943ac76..fcf191b 100644 --- a/intro/intro.tex +++ b/intro/intro.tex @@ -14,13 +14,14 @@ \end{chapterabstract} There are at least 13.4 billion devices connected to the internet at the time of writing\footnote{\url{https://transformainsights.com/research/tam/market}, accessed on: \formatdate{13}{10}{2022}}. -Each and every one of those devices senses, acts, or otherwise interacts with people, other computers, and the environment surrounding us. -Even though there is a substantial variety among these devices, they all have one thing in common: they are all computers and hence require software to operate. +Each of these senses, acts, or otherwise interacts with people, other computers, and the environment surrounding us. +Despite their immense diversity, they all have one thing in common. +They are all computers, and as computers, they they require software to operate. 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. -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. +These miniature computers contain integrated circuits that accomodates a microprocessor designed for use in embedded applications. +Typically, microcontrollers 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] % \centering @@ -30,19 +31,21 @@ Typical edge devices are therefore tiny in size; have little memory; contain a s %\end{figure} Programming and maintaining \gls{IOT} systems is a complex and error-prone process. +Unlike the conductor in the orchestra waving their baton to orchestrate the ensemble of instruments in an orchestra, in the universe of software there is room for little error. 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 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. +By utilising advanced compiler technologies, much of the internals, communications, and interoperations of the applications are automatically generated. +From a single declarative specification of the work required, 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 \gls{TOP} systems such as \gls{ITASK} to be suitable for the average \gls{IOT} edge device. +Unfortunately, because the abstraction level is so demanding, the hardware requirements are overly excessive for \gls{TOP} systems such as \gls{ITASK}. +Hence, impractical for the average edge device. -This is where \glspl{DSL} are brought into play. +This is where \glspl{DSL} are must be 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. +As a result, hardware requirements can be drastically lowered, even with high levels of abstraction for the specified domain. 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}. @@ -51,7 +54,7 @@ As it is integrated with \gls{ITASK}, it allows for all layers of an \gls{IOT} a \section{Reading guide}% \label{lst:reading_guide} -The thesis is structured as a purely functional rhapsody. +This work is is structured as a purely functional rhapsody. On Wikipedia, a musical rhapsody is defined as follows \citep{wikipedia_contributors_rhapsody_2022}: \begin{quote}\emph{% A \emph{rhapsody} in music is a one-movement work that is episodic yet integrated, free-flowing in structure, featuring a range of highly contrasted moods, colour, and tonality.} @@ -78,8 +81,8 @@ While the term \gls{IOT} briefly gained interest around 1999 to describe the com \emph{The \glsxtrlong{IOT}, or \glsxtrshort{IOT}, is the integration of people, processes and technology with connectable devices and sensors to enable remote monitoring, status, manipulation and evaluation of trends of such devices.} \end{quote} -CISCO states that the \gls{IOT} started when there where as many connected devices as there were people on the globe, i.e.\ around 2008 \citep{evans_internet_2011}. -Today, \gls{IOT} is the term for a system of devices that sense the environment, act upon it and communicate with each other and the world. +CISCO states that the \gls{IOT} started when there were as many connected devices as there were people on the globe, i.e.\ around 2008 \citep{evans_internet_2011}. +Today, \gls{IOT} is the term for a system of devices that sense the environment, act upon it and communicate with each other and the world they live in. These connected devices are already in households all around us in the form of smart electricity meters, fridges, phones, watches, home automation, \etc. When describing \gls{IOT} systems, a tiered---or layered---architecture is often used for compartmentalisation. @@ -93,32 +96,33 @@ The number of tiers heavily depends on the required complexity of the model but \end{figure} To explain the tiers, an example \gls{IOT} application---home automation---is dissected accordingly. -Closest to the end-user is the presentation layer, it provides the interface between the user and the \gls{IOT} system. -In home automation this may be a web interface or an app used on a phone or wall-mounted tablet to interact with the edge devices and view the sensor data. +Closest to the end-user is the presentation layer, it provides the interface between the user and \gls{IOT} systems. +In home automation this may be a web interface, or an app used on a phone or wall-mounted tablet to interact with edge devices and view sensor data. -The application layer provides the \glspl{API}, data interfaces, data processing, and data storage of the \gls{IOT} system. +The application layer provides the \glspl{API}, data interfaces, data processing, and data storage of \gls{IOT} systems. A cloud server or local server provides this layer in a typical home automation application. The perception layer---also called edge layer---collects the data and interacts with the environment. It consists of edge devices such as microcontrollers equipped with various sensors and actuators. -In home automation this layer consists of all the devices hosting the sensors and actuators such as smart light bulbs, actuators to open doors or a temperature and humidity sensors. +In home automation this layer consists of all the devices hosting sensors and actuators such as smart light bulbs, actuators to open doors or a temperature and humidity sensors. All layers are connected using the network layer. In some applications this is implemented using conventional networking techniques such as WiFi or Ethernet. -However, networks or layers on top of it---tailored to the needs of the specific interconnection between layers---have been increasingly popular. -Examples of this are BLE, LoRa, ZigBee, LTE-M, or \gls{MQTT} for connecting the perception layer to the application layer and techniques such as HTTP, AJAX, and WebSocket for connecting the presentation layer to the application layer. +However, networks or layers on top of it---tailored to the needs of the specific interconnection between layers---have become increasingly popular. +Examples of this are BLE, LoRa, ZigBee, LTE-M, or \gls{MQTT} for connecting perception layers to application layers and techniques such as HTTP, AJAX, and WebSocket for connecting presentation layers to application layers. Across the layers, the devices are a large heterogeneous collection of different platforms, protocols, paradigms, and programming languages often resulting in impedance problems or semantic friction between layers when programming \citep{ireland_classification_2009}. -Even more so, the perception layer itself often is a heterogeneous collections of microcontrollers in itself as well, each having their own peculiarities, language of choice, and hardware interfaces. -Moreover, as the edge hardware needs to be cheap, small-scale, and energy efficient, the microcontrollers used to power these devices do not have a lot of computational power, only a soup\c{c}on of memory, and little communication bandwidth. -Typically the devices are unable to run a full-fledged general-purpose \gls{OS} but use compiled firmwares that are written in an imperative language. -While devices are getting a bit faster, smaller, and cheaper, they keep these properties to an extent, greatly reducing the flexibility for dynamic systems where tasks are created on the fly, executed on demand, or require parallel execution. -As program memory is mostly flash based and only lasts a couple of thousand writes before it wears out, it is not suitable for rapid reconfiguring and reprogramming. +Even more so, the perception layer itself is often a heterogeneous collections of microcontrollers in itself, each having their own peculiarities, language of choice, and hardware interfaces. +Insofar, as edge hardware needs to be cheap, small-scale, and energy efficient, the microcontrollers used to power them do not have a lot of computational power, only a soup\c{c}on of memory, and little communication bandwidth. +Typically these devices are unable to run a full-fledged general-purpose \gls{OS}. +Rather they employ compiled firmware written in imperative languages. +While devices are getting a bit faster, smaller, and cheaper, they keep these properties to an extent, greatly reducing the flexibility for dynamic systems when tasks are created on the fly, executed on demand, or require parallel execution. +As program memory is mostly flash-based and only lasts a couple of thousand writes before it wears out, it is not suitable for rapid reconfiguring and reprogramming. These problems can be mitigated by dynamically sending code to be interpreted to the microcontroller. -With interpretation, a specialized interpreter is flashed in the program memory once that receives the program code to execute at runtime. +With interpretation, a specialized interpreter is flashed in the program memory once it receives the program code to execute at run time. Interpretation always comes with an overhead, making it challenging to create them for small edge devices. -However, the hardware requirements can be reduced by embedding domain-specific data into the programming language to be interpreted, so called \glspl{DSL}. +However, the hardware requirements can be reduced by embedding domain-specific data into the programming language to be interpreted, so-called \glspl{DSL}. \section{\texorpdfstring{\Glsxtrlongpl{DSL}}{Domain-specific languages}}% \label{sec:back_dsl} @@ -269,7 +273,7 @@ To bridge this gap, \gls{MTASK} was developed, a \gls{TOP} system for \gls{IOT} On the other hand, \gls{MTASK} offers abstractions for edge layer-specific details such as the heterogeneity of architectures, platforms, and frameworks; peripheral access; (multi) task scheduling; and lowering energy consumption. The \gls{MTASK} language is written in \gls{CLEAN} as a multi-view \gls{EDSL} and hence there are multiple interpretations possible. The byte code compiler is the most relevant for this thesis. -From an \gls{MTASK} task constructed at runtime, a compact binary representation of the work that needs to be done is compiled. +From an \gls{MTASK} task constructed at run time, a compact binary representation of the work that needs to be done is compiled. This byte code is then sent to a device that running the \gls{MTASK} \gls{RTS}. This feather-light domain-specific \gls{OS} is written in portable \gls{C} with a minimal device specific interface and functions as a \gls{TOP} engine. \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}. @@ -357,11 +361,11 @@ This episode is a monograph compiled from the following publications and shows t % \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}] - 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. + 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, January 22--26, 2018. % \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}] - 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. + 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, June 17--21, 2019. % \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. @@ -375,7 +379,7 @@ This episode is a monograph compiled from the following publications and shows t % 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.} - 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. + 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, July 4--8, 2022. % \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. @@ -384,7 +388,7 @@ This episode is a monograph compiled from the following publications and shows t \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. +The original imperative predecessors, 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, there were weekly meetings with the co-authors in which we discussed and refined the ideas. @@ -395,7 +399,7 @@ This chapter is based on the conference paper and a journal paper extending it: \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. + It compares programming traditional tiered architectures to tierless architectures by illustrating a qualitative and a quantitative four-way comparison of a smart-campus application. \end{enumerate} \paragraph{Contribution:} diff --git a/other.bib b/other.bib index 586d6be..5e26061 100644 --- a/other.bib +++ b/other.bib @@ -122,7 +122,7 @@ language = {English}, urldate = {2021-02-24}, publisher = {Release}, - author = {GHC Team}, + author = {{GHC Team}}, year = {2021}, file = {GHC Team - 2021 - GHC User’s Guide Documentation.pdf:/home/mrl/.local/share/zotero/storage/87ZT5VXL/GHC Team - 2021 - GHC User’s Guide Documentation.pdf:application/pdf}, } @@ -133,7 +133,7 @@ language = {English}, urldate = {2021-02-24}, publisher = {Release}, - author = {GHC Team}, + author = {{GHC Team}}, year = {2021}, } diff --git a/preamble.tex b/preamble.tex index adb6568..2606a8c 100644 --- a/preamble.tex +++ b/preamble.tex @@ -215,9 +215,9 @@ \newcommand{\arduinoinline}[1]{\lstinline[language={[Arduino]C++},postbreak=]|#1|} \newcommand{\pythoninline}[1]{\lstinline[language=Python,postbreak=]|#1|} \newcommand{\cleaninline}[1]{\lstinline[language=Clean,postbreak=]|#1|} -\newcommand{\cleaninputlisting}[2][]{\renewcommand*{\lstlistingname}{Listing (\gls{CLEAN})}\lstinputlisting[language=Clean,#1]{#2}} +\newcommand{\cleaninputlisting}[2][]{\renewcommand*{\lstlistingname}{Listing (\gls{CLEAN})}\lstinputlisting[language=Clean,#1]{\subfix{#2}}} \newcommand{\haskellinline}[1]{\lstinline[language={[Regular]Haskell},postbreak=]|#1|} -\newcommand{\haskellinputlisting}[2][]{\renewcommand*{\lstlistingname}{Listing (\gls{HASKELL})}\lstinputlisting[language={[Regular]Haskell},#1]{#2}} +\newcommand{\haskellinputlisting}[2][]{\renewcommand*{\lstlistingname}{Listing (\gls{HASKELL})}\lstinputlisting[language={[Regular]Haskell},#1]{\subfix{#2}}} \newcommand{\haskelllhstexinline}[1]{\lstinline[language={[Lhs2Tex]Haskell},postbreak=]|#1|} %For storing listings in footnotes \newsavebox{\LstBox} @@ -291,11 +291,9 @@ % Glossaries and acronyms \usepackage[nolangwarn,abbreviations,nonumberlist,prefix]{glossaries-extra} -\setabbreviationstyle[acronym]{long-short} +\setabbreviationstyle{long-short} +\setabbreviationstyle[noexpand]{short-nolong} \Addlcwords{of} -% Titlecase glossary commands -\newcommand{\glst}[1]{\titlecap{\glsentrylong{#1}}} -\newcommand{\Glst}[1]{\glst{#1}} \usepackage{glossary-mcols} \pdfstringdefDisableCommands{% \def\glsxtrlong#1{}% diff --git a/subfileprefix.tex b/subfileprefix.tex index 4ff83ee..536397b 100644 --- a/subfileprefix.tex +++ b/subfileprefix.tex @@ -1,3 +1 @@ -\ifSubfilesClassLoaded{% - \tableofcontents -}{} +\ifSubfilesClassLoaded{\tableofcontents}{} diff --git a/top/4iot.tex b/top/4iot.tex index dc6b6dc..10457ba 100644 --- a/top/4iot.tex +++ b/top/4iot.tex @@ -19,7 +19,7 @@ \end{itemize} \end{chapterabstract} -The edge layer of \gls{IOT} system mostly consists of microcontrollers. +The edge layer of \gls{IOT} systems predominantly contains of microcontrollers. Microcontrollers are tiny computers designed specifically for embedded applications. They therefore only have a soup\c{c}on of memory, have a slow processor, come with many energy efficient sleep modes and have a lot of peripheral support such as \gls{GPIO} pins. Usually, programming microcontrollers requires an elaborate multi-step toolchain of compilation, linkage, binary image creation, and burning this image onto the flash memory of the microcontroller in order to compile and run a program. @@ -44,7 +44,8 @@ The programs are usually cyclic executives instead of tasks running in an operat \end{tabular} \end{table} -Each type of microcontrollers comes with vendor-provided drivers, compilers and \glspl{RTS} but there are many platform that abstract away from this such as \gls{MBED} and \gls{ARDUINO} of which \gls{ARDUINO} is specifically designed for education and prototyping and hence used here. +Different models of microcontrollers require their own vendor-provided drivers, hardware abstraction layer, compilers and \glspl{RTS}. +There are many platforms that abstract away from this such as \gls{MBED} and \gls{ARDUINO} of which \gls{ARDUINO} is specifically designed for education and prototyping and hence used here. The popular \gls{ARDUINO} \gls{C}\slash\gls{CPP} dialect and accompanying libraries provide an abstraction layer for common microcontroller behaviour allowing the programmer to program multiple types of microcontrollers using a single language. Originally it was designed for the in-house developed open-source hardware with the same name but the setup allows porting to many architectures. It provides an \gls{IDE} and toolchain automation to perform all steps of the toolchain with a single command. @@ -90,8 +91,7 @@ void loop() { delay(500); digitalWrite(D2, LOW); delay(500); -} - \end{lstArduino} +}\end{lstArduino} \end{subfigure}% \begin{subfigure}[b]{.5\linewidth} \begin{lstClean}[caption={Blink program.},label={lst:blinkImp}] @@ -104,8 +104,7 @@ blink = >>|. writeD d2 false >>|. delay (lit 500) ) -} - \end{lstClean} +}\end{lstClean} \end{subfigure} \end{figure} @@ -191,9 +190,9 @@ blinktask = % VimTeX: SynIgnore off \section{Conclusion} -The edge layer of \gls{IOT} systems are powered by microcontrollers. -Programming them happens through compiled firmwares using low-level imperative programming languages and do usually not come with an \gls{OS}. -Consequently, writing applications that perform multiple tasks at the same time is error prone, and complex; and requires a lot of boilerplate and manual scheduling code. +The edge layer of \gls{IOT} systems is powered by microcontrollers. +Programming them happens through compiled firmwares using low-level imperative programming languages. +Due to the lack of an \gls{OS}, writing applications that perform multiple tasks at the same time is error prone, and complex; and requires a lot of boilerplate and manual scheduling code. With the \gls{MTASK} system, a \gls{TOP} programming language for \gls{IOT} edge devices, this limitation can be overcome. \todo{uit\-breiden} @@ -238,7 +237,7 @@ An existing smart campus application was developed using \gls{MTASK} and quantit This research was later extended to include a four-way comparison: \gls{PYTHON}, \gls{MICROPYTHON}, \gls{ITASK}, and \gls{MTASK} \citep{lubbers_could_2022}. Currently, power efficiency behaviour of traditional versus \gls{TOP} \gls{IOT} stacks is being compared as well adding a \gls{FREERTOS} implementation to the mix as well. -\subsection*{Future} +\subsection*{Future work} Plans for extensions and improvements include exploring integrating \gls{TINYML} into \gls{MTASK}; adding intermittent computing support to \gls{MTASK}; and extending the formal semantics to cover the entirety of the language. In 2023, the SusTrainable summer school in Coimbra, Portugal will host a course on \gls{MTASK} as well. diff --git a/top/img/home_auto1.png b/top/img/home_auto1.png new file mode 100644 index 0000000..92eb237 Binary files /dev/null and b/top/img/home_auto1.png differ diff --git a/top/img/home_auto2.png b/top/img/home_auto2.png new file mode 100644 index 0000000..2ec874c Binary files /dev/null and b/top/img/home_auto2.png differ diff --git a/top/img/home_auto3.png b/top/img/home_auto3.png new file mode 100644 index 0000000..ca1fefd Binary files /dev/null and b/top/img/home_auto3.png differ diff --git a/top/int.tex b/top/int.tex index 33f7813..10ce549 100644 --- a/top/int.tex +++ b/top/int.tex @@ -56,6 +56,8 @@ withDevice :: a (MTDevice -> Task b) -> Task b | iTask b & channelSync, iTask a \end{lstClean} +\todo{v.b.\ voor withDevice} + \subsection{Implementation} The \cleaninline{MTDevice} abstract type is internally represented as three \gls{ITASK} \gls{SDS} that contain all the current information about the tasks. The first \gls{SDS} is the information about the \gls{RTS} of the device, i.e.\ metadata on the tasks that are executing, the hardware specification and capabilities, and a list of fresh task identifiers. @@ -113,6 +115,8 @@ Under the hood, \cleaninline{liftmTask}: The task value of the \cleaninline{liftmTask} task is the task value of the task on the edge device. +\todo{v.b.\ voor liftmtask} + \section{Lifting \texorpdfstring{\gls{ITASK}}{iTask} \texorpdfstring{\glsxtrlongpl{SDS}}{shared data sources}}\label{sec:liftsds} Lifting \gls{ITASK} \glspl{SDS} to \gls{MTASK} \glspl{SDS} is something that mostly happens at the compiler level using the \cleaninline{liftsds} function (see \cref{lst:mtask_itasksds}). \Glspl{SDS} in \gls{MTASK} must always have an initial value. @@ -165,6 +169,48 @@ This identifier is then used to provide a reference to the \cleaninline{def} def \end{lstClean} % VimTeX: SynIgnore off +\todo{v.b.\ voor lifted sdss} + +\section{Home automation} +This section presents a interactive home automation program (\Cref{lst:example_home_automation}) to illustrate \gls{MTASK}'s integration with \gls{ITASK}. +It consists of a web interface for the user to control which tasks may be executed on either of two connected devices: an \gls{ARDUINO} UNO, connected via a serial port; and an ESP8266 based prototyping board called NodeMCU, connected via \gls{TCP} over WiFi. + +\Crefrange{lst:example:spec1}{lst:example:spec2} show the specification for the devices followed by \crefrange{lst:example:task1}{lst:example:task2} containing the actual task. +This task first connects the devices (\crefrange{lst:example:conn1}{lst:example:conn2}) followed by a \cleaninline{parallel} task that is visualized as a tabbed window with a shutdown button to terminate the program (\crefrange{lst:example:par1}{lst:example:par2}). +The \cleaninline{chooseTask} task (\crefrange{lst:example:ct1}{lst:example:ct2}) allows the user to pick a task, sending it to the specified device. +Tasks are picked from the \cleaninline{tasks} list (\crefrange{lst:example:tasks1}{lst:example:tasks2}). +For example, the \cleaninline{temperature} task shows the current temperature to the user. +When the temperature changes, the \gls{DHT} sensor reports it and the task value for the \cleaninline{temperature} task changes. +This change in task value is reflected in the \gls{ITASK} server and the task value of the \cleaninline{liftmTask} task changes accordingly. +The task is lifted to an \gls{ITASK} task and the \cleaninline{>\&>}\footnotemark{} \gls{ITASK} combinator transforms the task value into an \gls{SDS} that is displayed to the user using \cleaninline{viewSharedInformation}. +\footnotetext{\cleaninline{(>\&>) infixl 1 :: (Task a) ((SDSLens () (? a) ()) -> Task b) -> Task b \| iTask a \& iTask b}} +Screenshots of the application are given in \cref{fig:example_screenshots}. + +\begin{figure}[ht] + \centering + \begin{subfigure}[b]{.3\linewidth} + \includegraphics[width=\linewidth]{home_auto1} + \caption{Select task.} + \end{subfigure} + \begin{subfigure}[b]{.3\linewidth} + \includegraphics[width=\linewidth]{home_auto2} + \caption{Select device.} + \end{subfigure} + \begin{subfigure}[b]{.3\linewidth} + \includegraphics[width=\linewidth]{home_auto3} + \caption{View result.} + \end{subfigure} + \caption{Screenshots of the home automation example program in action.}% + \label{fig:example_screenshots} +\end{figure} + +\begin{figure} + \cleaninputlisting[firstline=12,lastline=52,numbers=left,belowskip=0pt,escapeinside={/*}{*/}]{lst/example.icl} + \begin{lstClean}[numbers=left,firstnumber=42,aboveskip=0pt,caption={An example of a home automation program.},label={lst:example_home_automation}] + , ...][+\label{lst:example:tasks2}+] + \end{lstClean} +\end{figure} + \section{Conclusion} diff --git a/top/lang.tex b/top/lang.tex index 1e1b02c..a5916cd 100644 --- a/top/lang.tex +++ b/top/lang.tex @@ -15,15 +15,18 @@ \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. @@ -34,7 +37,7 @@ The following interpretations are available for \gls{MTASK}. 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}). @@ -49,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 @@ -58,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. @@ -96,6 +99,22 @@ someTask = 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. @@ -115,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 @@ -280,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 @@ -296,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. @@ -311,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 @@ -329,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} @@ -352,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}.}] @@ -386,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 @@ -420,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. @@ -451,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-> @@ -481,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}.}] diff --git a/top/lst/.gitignore b/top/lst/.gitignore new file mode 100644 index 0000000..d97038b --- /dev/null +++ b/top/lst/.gitignore @@ -0,0 +1,6 @@ +nitrile-packages +Clean System Files +example +*.bc +*.pbc +*-www diff --git a/top/lst/example.icl b/top/lst/example.icl new file mode 100644 index 0000000..7d15baa --- /dev/null +++ b/top/lst/example.icl @@ -0,0 +1,57 @@ +module example + +import StdEnv +import Data.Func +import iTasks +import mTask.Interpret +import mTask.Interpret.Device.TCP +import mTask.Interpret.Device.Serial + +Start w = doTasks autoHome w + +arduino = {TTYSettings | zero & devicePath="/dev/ttyACM0"}/*\label{lst:example:spec1}*/ +nodeMCU = {TCPSettings | host="192.168.0.1", port=8123, pingTimeout= ?None}/*\label{lst:example:spec2}*/ + +autoHome :: Task ()/*\label{lst:example:task1}*/ +autoHome = withDevice arduino \dev1-> /*\label{lst:example:conn1}*/ + withDevice nodeMCU \dev2-> /*\label{lst:example:conn2}*/ + parallel [(Embedded, chooseTask dev1 dev2)] [] <<@ ArrangeWithTabs True/*\label{lst:example:par1}*/ + >>* [OnAction (Action "Shutdown") (always (shutDown 0))]/*\label{lst:example:task2}\label{lst:example:par2}*/ + +chooseTask :: MTDevice MTDevice (SharedTaskList ()) -> Task ()/*\label{lst:example:ct1}*/ +chooseTask dev1 dev2 stl = tune (Title "Run a task") + $ enterChoice [] (zip2 [0..] (map fst tasks)) + <<@ Hint "Choose a task" + >>? \(i, n)->enterChoice [] ["arduino", "node"] + <<@ Hint "Which device?" + >>? \device->appendTask Embedded (mkTask n i device) stl + >-| chooseTask dev1 dev2 stl +where + mkTask n i device stl + # dev = if (device == "node") dev2 dev1 + = ((snd (tasks !! i) $ dev) + >>* [OnAction ActionClose $ always $ return ()]) <<@ Title n/*\label{lst:example:ct2}*/ + +tasks :: [(String, MTDevice -> Task ())]/*\label{lst:example:tasks1}*/ +tasks = + [ ("temp", \dev-> + liftmTask ( DHT (DHT_DHT (DigitalPin D6) DHT22) \dht-> + {main=temperature dht}) dev + >&> \t->viewSharedInformation + [ViewAs \i->toString (fromMaybe 0.0 i) +++ "C"] t + <<@ Hint "Current Temperature" + @! ()) + , ("lightswitch", \dev-> + withShared False \sh-> + liftmTask (lightswitch sh) dev + -|| updateSharedInformation [] sh <<@ Hint "Switch") + , ("factorial", \dev-> + updateInformation [] 5 <<@ Hint "Factorial of what?" + >>? \i->liftmTask (factorial i) dev + >>- \r->viewInformation [] r <<@ Hint "Result" + @! ()) + ] + +factorial i = {main=rtrn (lit i)} +blink d = {main=writeD (lit d) (lit True)} +lightswitch sh = {main=rtrn (lit ())} diff --git a/top/lst/nitrile-lock.json b/top/lst/nitrile-lock.json new file mode 100644 index 0000000..ebd8e50 --- /dev/null +++ b/top/lst/nitrile-lock.json @@ -0,0 +1,40 @@ +{"packages":{"linux-x64":[{"name":"abc-interpreter" + ,"version":"1.0.0"} + ,{"name":"argenv" + ,"version":"1.0.1"} + ,{"name":"base" + ,"version":"1.0.0"} + ,{"name":"base-clm" + ,"version":"1.4.2"} + ,{"name":"base-code-generator" + ,"version":"1.0.0"} + ,{"name":"base-compiler" + ,"version":"2.0.1"} + ,{"name":"base-compiler-itasks" + ,"version":"1.0.0"} + ,{"name":"base-rts" + ,"version":"1.1.0"} + ,{"name":"base-stdenv" + ,"version":"1.0.0"} + ,{"name":"clean-platform" + ,"version":"0.3.4"} + ,{"name":"gast" + ,"version":"0.2.1"} + ,{"name":"gentype" + ,"version":"1.1.0"} + ,{"name":"graph-copy" + ,"version":"2.0.1"} + ,{"name":"itasks" + ,"version":"0.2.0"} + ,{"name":"itasks-mqttclient" + ,"version":"1.0.2"} + ,{"name":"itasks-serial" + ,"version":"0.1.0"} + ,{"name":"lib-compiler-itasks" + ,"version":"2.0.1"} + ,{"name":"mtask-server" + ,"version":"0.1.0"} + ,{"name":"serial" + ,"version":"0.1.1"} + ,{"name":"tcpip" + ,"version":"2.0.1"}]}} \ No newline at end of file diff --git a/top/lst/nitrile.yml b/top/lst/nitrile.yml new file mode 100644 index 0000000..d79e8ec --- /dev/null +++ b/top/lst/nitrile.yml @@ -0,0 +1,37 @@ +name: mtask-examples +url: https://gitlab.com/mtask/server +maintainer: Mart Lubbers +contact_email: mart@cs.ru.nl +description: mTask server side library +version: 1.0 +license: BSD-2-Clause +type: Application + +clm_options: + bytecode: prelinked + compiler: cocl-itasks + export_local_labels: true + fusion: GenericFusion + generate_descriptors: true + post_link: web-resource-collector + print_result: false + print_time: false + strip: false + +# Dependencies +dependencies: + base: ^1.0 + base-compiler-itasks: ^1.0 + mtask-server: ^0.1 + itasks: ^0.2.0 + +# Sources +src: + - . + +build: + example: + script: + - clm: + main: example + target: ./example