.
authorMart Lubbers <mart@martlubbers.net>
Fri, 14 Oct 2022 11:42:36 +0000 (13:42 +0200)
committerMart Lubbers <mart@martlubbers.net>
Fri, 14 Oct 2022 11:42:36 +0000 (13:42 +0200)
appx/clean_for_haskell_programmers.tex
concl/conclusion.tex
dsl/class_deep_embedding.tex
dsl/dsl_techniques.tex
dsl/first-class_datatypes.tex
intro/introduction.tex
preamble.tex
thesis.tex
top/mtask.tex
tvt/tvt.tex

index 0e713e0..adddcbf 100644 (file)
@@ -12,7 +12,7 @@
 
 This note is meant to give people who are familiar with the \gls{FP} language \gls{HASKELL} a consise overview of \gls{CLEAN} language elements and how they differ from \gls{HASKELL}.
 The goal is to support the reader when reading \gls{CLEAN} code.
-Table~\ref{tbl:syn_clean_haskell} shows frequently occuring \gls{CLEAN} language elements on the left side and their \gls{HASKELL} equivalent on the right side.
+\Cref{tbl:syn_clean_haskell} shows frequently occuring \gls{CLEAN} language elements on the left side and their \gls{HASKELL} equivalent on the right side.
 Obviously, this summary is not exhaustive.
 Some \gls{CLEAN} language elements that are not easily translatable to \gls{HASKELL} and thus do not occur in the summary following below.
 We hope you enjoy these notes and that it aids you in reading \gls{CLEAN} programs.
@@ -71,7 +71,7 @@ f :: v:a u:b -> u:b, [v<=u]  // f works when a is less unique than b
 %:: T = T (Int -> *(*World -> *World)) // Writing :: T = T (Int *World -> *World) won't work
 
 \subsection{Expressions}
-Patterns in \gls{CLEAN} can be used as predicates as well~\citep[Chp.~3.4.3]{plasmeijer_clean_2021}.
+Patterns in \gls{CLEAN} can be used as predicates as well~\citep[\citesection{3.4.3}]{plasmeijer_clean_2021}.
 Using the \cleaninline{=:} operator, a value can be tested against a pattern.
 Variable names are not allowed but wildcard patterns \cleaninline{\_} are.
 
@@ -87,7 +87,7 @@ ifAB x ifa ifb = if (x =: (A _)) ifa ifb
 
 Due to the nature of uniqueness typing, many functions in \gls{CLEAN} are state transition functions with possibly unique states.
 The \emph{let before} construct allows the programmer to specify sequential actions without having to invent unique names for the different versions of the state.
-\Cref{lst:let_before} shows an example of the usage of the \emph{let before} construct (adapted from~\citep[Chp.~3.5.4]{plasmeijer_clean_2021}).
+\Cref{lst:let_before} shows an example of the usage of the \emph{let before} construct (adapted from~\citep[\citesection{3.5.4}]{plasmeijer_clean_2021}).
 
 \begin{lstClean}[label={lst:let_before},caption={Let before expression example.}]
 readChars :: *File -> ([Char], *File)
@@ -99,7 +99,7 @@ readChars file
 \end{lstClean}
 
 \subsection{Generics}
-Polytypic functions~\citep{jeuring_polytypic_1996}---also known as generic or kind-indexed fuctions---are built into \gls{CLEAN}~\citep[Chp.~7.1]{plasmeijer_clean_2021}\citep{alimarine_generic_2005} whereas in \gls{HASKELL} they are implemented as a library~\citep[Chp.~6.19.1]{ghc_team_ghc_2021}.
+Polytypic functions~\citep{jeuring_polytypic_1996}---also known as generic or kind-indexed fuctions---are built into \gls{CLEAN}~\citep[\citesection{7.1}]{plasmeijer_clean_2021}\citep{alimarine_generic_2005} whereas in \gls{HASKELL} they are implemented as a library~\citep[\citesection{6.19.1}]{ghc_team_ghc_2021}.
 The implementation of generics in \gls{CLEAN} is very similar to that of Generic H$\forall$skell~\citep{hinze_generic_2003}.
 %When calling a generic function, the kind must always be specified and depending on the kind, the function may require more arguments.
 
@@ -111,7 +111,7 @@ Metadata about the types is available using the \cleaninline{of} syntax that giv
 
 \subsection{\texorpdfstring{\glsentrytext{GADT}}{GADT}s}
 \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}.
-While \glspl{GADT} are not natively supported in \gls{CLEAN}, they can be simulated using embedding-projection pairs or equivalence types~\citep[Sec.~2.2]{cheney_lightweight_2002}.
+While \glspl{GADT} are not natively supported in \gls{CLEAN}, they can be simulated using embedding-projection pairs or equivalence types~\citep[\citesection{2.2}]{cheney_lightweight_2002}.
 To illustrate this, \cref{lst:gadt_clean} shows an example \gls{GADT} that would be implemented in \gls{HASKELL} as done in \cref{lst:gadt_haskell}\requiresGHCmod{GADTs}.
 
 \lstinputlisting[language=Clean,firstline=4,lastline=24,label={lst:gadt_clean},caption={Expression \gls{GADT} using equivalence types in \gls{CLEAN}.}]{lst/expr_gadt.icl}
index f6b692d..868c30b 100644 (file)
@@ -7,6 +7,7 @@
 
 \chapter{Coda}%
 \label{chp:conclusion}
+\todo{Or finale}
 \section{Conclusion}
 
 \section{Future work}
index 6bda1b1..0542633 100644 (file)
@@ -144,7 +144,7 @@ Semantics become data types\footnotemark{} implementing these type classes, resu
        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[Sec.~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}
@@ -222,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[Chp.~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
@@ -250,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[Sec.~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
@@ -551,7 +551,7 @@ e3 = neg_4 (Lit_4 42 `sub_4` Lit_4 38) `Add_4` Lit_4 1
 \section{\texorpdfstring{\Acrlongpl{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}.
 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[Sec.~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.
@@ -601,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[Chp.~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}
@@ -646,6 +646,7 @@ However, if needed, the technique generalises to \glspl{GADT} as well, adding ra
 Finally, the abstract syntax tree remains observable which makes it suitable for intensional analyses, albeit using occasional dynamic typing for truly cross-extensional transformations.
 
 Defining reusable expressions overloaded in semantics or using multiple semantics on a single expression requires some boilerplate still, getting around this remains future work.
+\Cref{sec:classy_reprise} shows how the boilerplate can be minimised using advanced type system extensions.
 
 \section{Related work}%
 \label{sec:cde:related}
@@ -656,17 +657,17 @@ Clearly, classy deep embedding bears most similarity to the \emph{Datatypes \`a
 In Swierstra'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.
-In classy deep embedding, extensions do not have to be enumerated at the type level but are captured in the extension case.
+In classy deep embedding, extensions only have to be enumerated at the type level when the term is required to be overloaded, in all other cases they are captured in the extension case.
 Because all the constructs are expressed in the type system, nifty type system tricks need to be employed to convince the compiler that everything is type safe and the class constraints can be solved.
 Furthermore, it requires some boilerplate code such as functor instances for the data types.
 In return, pattern matching is easier and does not require dynamic typing.
 Classy deep embedding only strains the programmer with writing the extension case for the main data type and the occasional loopback constructor.
 
-L\"oh and Hinze proposed a language extension that allows open data types and open functions, i.e.\ functions and data types that can be extended with more cases later on~\citep{loh_open_2006}.
+\Citet{loh_open_2006} proposed a language extension that allows open data types and open functions, i.e.\ functions and data types that can be extended with more cases later on.
 They hinted at the possibility of using type classes for open functions but had serious concerns that pattern matching would be crippled because constructors are becoming types, thus ultimately becoming impossible to type.
 In contrast, this paper shows that pattern matching is easily attainable---albeit using dynamic types---and that the terms can be typed without complicated type system extensions.
 
-A technique similar to classy deep embedding was proposed by Najd and Peyton~Jones to tackle a slightly different problem, namely that of reusing a data type for multiple purposes in a slightly different form~\citep{najd_trees_2017}.
+A technique similar to classy deep embedding was proposed by \citet{najd_trees_2017} to tackle a slightly different problem, namely that of reusing a data type for multiple purposes in a slightly different form.
 For example to decorate the abstract syntax tree of a compiler differently for each phase of the compiler.
 They propose to add an extension descriptor as a type variable to a data type and a type family that can be used to decorate constructors with extra information and add additional constructors to the data type using an extension constructor.
 Classy deep embedding works similarly but uses existentially quantified type variables to describe possible extensions instead of type variables and type families.
@@ -677,9 +678,10 @@ Tagless-final embedding is the shallowly embedded counterpart of classy deep emb
 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.
+Furthermore, in classy deep embedding, defining (mutual) dependent interpretations is automatically supported whereas in tagless-final embedding this requires some amount of code duplication \citep{sun_compositional_2022}.
 
 Hybrid approaches between deep and shallow embedding exist as well.
-For example, Svenningson et al.\ show that by expressing the deeply embedded language in a shallowly embedded core language, extensions can be made orthogonally as well~\citep{svenningsson_combining_2013}.
+For example, \citet{svenningsson_combining_2013} show that by expressing the deeply embedded language in a shallowly embedded core language, extensions can be made orthogonally as well.
 This paper differs from those approaches in the sense that it does not require a core language in which all extensions need to be expressible.
 
 \section*{Acknowledgements}
@@ -687,6 +689,134 @@ This research is partly funded by the Royal Netherlands Navy.
 Furthermore, I would like to thank Pieter and Rinus for the fruitful discussions, Ralf for inspiring me to write a functional pearl, and the anonymous reviewers for their valuable and honest comments.
 
 \begin{subappendices}
+\section{Reprise: reducing boilerplate}\label{sec:classy_reprise}
+\todo{Improve text}
+One of the unique selling points of this novel \gls{DSL} embedding technique is that it, in its basic form, does not require advanced type system extensions nor a lot of boilerplate.
+However, generalising the technique to \glspl{GADT} arguably unleashes a cesspool of \emph{unsafe} compiler extensions.
+If we are willing to work with extensions, almost all of the boilerplate can be inferred or generated\footnote{The source code for this extension can be found here: \url{https://gitlab.com/mlubbers/classydeepembedding}.}.
+
+The \gls{DSL} datatype is parametrised by a type variable providing a witness to the interpretation on the language.
+When using multiple interpretations, these need to be bundled in a data type.
+Using the \gls{GHC}'s \GHCmod{ConstraintKind} extension, we can make these witnesses explicit, tying into \gls{HASKELL}'s type system immediately.
+Furthermore, this constraint does not necessarily has to be a single constraint, after enabling \GHCmod{DataKinds} and \GHCmod{TypeOperators}, we can encode lists of witnesses instead.
+The data type for this list of witnesses is \haskelllhstexinline{Record}.
+The \haskelllhstexinline{Record} \gls{GADT} is parametrised by two type variables, the first type variable (\haskelllhstexinline{dt}) is the data type on which the constraints can be applied.
+The second type variable (\haskelllhstexinline{clist}) is the list of constraints itself.
+It is not just a list of \haskelllhstexinline{Constraint} but it is a list containing constraint constructors that will, when given a type of the polymorphic kind \haskelllhstexinline{k}, produce a constraint.
+This means that when \haskelllhstexinline{Cons} is pattern matched, the type class constraint for \haskelllhstexinline{c dt} can be solved by the compiler.
+\GHCmod{KindSignatures} is used to force the kinds of the type parameters and the kind of the data type is polymorphic (\GHCmod{PolyKinds}) so that the \haskelllhstexinline{Record} data type can be used for \glspl{DSL}s using type classes but also type constructor classes (e.g.\ when using \glspl{GADT})..
+
+\begin{lstHaskellLhstex}[caption={Data type for a list of constraints}]
+data Record (dt :: k) (clist :: [k -> Constraint]) where
+       Nil  :: Record dt '[]
+       Cons :: c dt => Record dt cs -> Record dt (c ': cs)
+\end{lstHaskellLhstex}
+
+To incorporate this type in the \haskelllhstexinline{Expr} type, the \haskelllhstexinline{Ext} constructor changes as follows:
+
+\begin{lstHaskellLhstex}[caption={Data type for a list of constraints}]
+data Expr c
+       = Lit Int
+       | Add (Expr c) (Expr c)
+       | Ext (Record x c) x
+\end{lstHaskellLhstex}
+
+Furthermore, we define a type class that allows us to extract explicit dictionaries \haskelllhstexinline{Dict} from these records if the constraint can is present in the list.
+
+\begin{lstHaskellLhstex}[caption={Membership functions for constraints}]
+class c `In` cs where
+       project :: Record dt cs -> Dict (c dt)
+instance {-# OVERLAPPING #-} c `In` (c ': cs) where
+       project (Cons _) = Dict
+instance {-# OVERLAPPING #-} c `In` cs => c `In` (b ': cs) where
+       project (Cons xs) = project xs
+\end{lstHaskellLhstex}
+
+Finally, creating these \haskelllhstexinline{Record} witnesses is a chore so this can be automated as well using a \haskelllhstexinline{CreateRecord} multi-parameter type class (requiring the \GHCmod{MultiParamTypeclasses} and \GHCmod{FlexibleInstances} extension).
+This type class creates a record structure cons by cons if and only if all type class constraints are available in the list of constraints.
+
+\begin{lstHaskellLhstex}[caption={Membership functions for constraints}]
+class CreateRecord dt c where
+       createRecord :: Record dt c
+instance CreateRecord d '[] where
+       createRecord = Nil
+instance (c (d c0), CreateRecord (d c0) cs) =>
+               CreateRecord (d c0) (c ': cs) where
+       createRecord = Cons createRecord
+\end{lstHaskellLhstex}
+
+The class constraints for the interpretation instances can now be greatly simplified, as shown in the evaluation instance for \haskelllhstexinline{Expr}.
+The implementation remains the same, only that for the extension case, a trick needs to be applied to convince the compiler of the correct instances.
+Using \haskelllhstexinline{`In`}'s \haskelllhstexinline{project} function, a dictionary can be brought into scope.
+This dictionary can then subsequently be used to apply the type class function on the extension using the \haskelllhstexinline{withDict} function from the \haskelllhstexinline{Data.Constraint} library\footnote{\haskelllhstexinline{withDict :: Dict c -> (c => r) -> r}}.
+The \GHCmod{ScopedTypeVariables} extension is used to make sure the existentially quantified type variable for the extension is matched to the type of the dictionary.
+Furthermore, because the class constraint is seemingly not smaller than the instance head, \GHCmod{UndecidableInstances} should be enabled.
+
+\begin{lstHaskellLhstex}[caption={Evaluation instance for the main data type}]
+class Eval v where
+       eval :: v -> Int
+
+instance Eval `In` s => Eval (Expr s) where
+       eval (Lit i) = i
+       eval (Add l r) = eval l + eval r
+       eval (Ext r (e :: x)) = withDict (project r :: Dict (Eval x)) eval e
+\end{lstHaskellLhstex}
+
+Smart constructors need to be adapted as well, as can be seen from the smart constructor \haskelllhstexinline{subst}.
+
+\begin{lstHaskellLhstex}[caption={Substitution smart constructor}]
+subst :: (Typeable c, CreateRecord (Subt c) c) => Expr c -> Expr c -> Expr c
+subst l r = Ext createRecord (l `Subt` r)
+\end{lstHaskellLhstex}
+
+Finally, defining terms in the language is 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.
+
+\begin{lstHaskellLhstex}[caption={Substitution smart constructor}]
+e0 :: Expr '[Print,Opt]
+e0 = neg (neg (Lit 42 `Add` (Lit 38 `subt` Lit 4)))
+\end{lstHaskellLhstex}
+
+It is also possible to define terms in the \gls{DSL} as being overloaded in the interpretation.
+This does require enumerating all the \haskelllhstexinline{CreateRecord} type classes for every extension.
+At the call site, the concrete list of constraints must be known.
+
+\begin{lstHaskellLhstex}[caption={Substitution smart constructor}]
+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}
+
+Finally, using the \GHCmod{TypeFamilies} extension, type families can be created for bundling \haskelllhstexinline{`In`} constraints (\haskelllhstexinline{UsingExt}) and \haskelllhstexinline{CreateRecord} constraints (\haskelllhstexinline{DependsOn}), making the syntax even more descriptive.
+E.g.\ \haskelllhstexinline{UsingExt '[A, B, C] c} expands to \haskelllhstexinline{(CreateRecord (A c) c, CreateRecord (B c) c, CreateRecord (C c) c)} and \haskelllhstexinline{DependsOn '[A, B, C] s} expands to \haskelllhstexinline{(A `In` s, B `In` s, C `In` s)}.
+
+\begin{lstHaskellLhstex}
+type family UsingExt cs c :: Constraint where
+       UsingExt '[] c = ()
+       UsingExt (d ': cs) c = (CreateRecord (d c) c, UsingExt cs c)
+
+type family DependsOn cs c :: Constraint where
+       DependsOn '[] c = ()
+       DependsOn (d ': cs) c = (d `In` c, DependsOn cs c)
+\end{lstHaskellLhstex}
+
+Defining the previous expression can now be done with the following shortened type that describes the semantics better:
+
+\begin{lstHaskellLhstex}
+e1 :: (Typeable c, UsingExt '[Neg, Subst]) => Expr c
+\end{lstHaskellLhstex}
+
+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
+       ...
+\end{lstHaskellLhstex}
+
 \section{Data types and definitions}%
 \label{sec:cde:appendix}
 \begin{lstHaskellLhstex}[caption={Data type definitions.}]
@@ -810,101 +940,6 @@ instance HasOpt_g d => Opt_g (Eq_g d) where
        opt_g (EqLoop_g e)     = EqLoop_g (opt_g e)
 \end{lstHaskellLhstex}
 
-\section{Chaining semantics (reprise)}\label{sec:classy_reprise}
-\todo{Verbeteren}
-One of the unique selling points of this novel \gls{DSL} embedding technique is that it, in its basic form, does not require advanced type system extensions.
-However, while generalising the technique to \glspl{GADT} arguably unleashes a cesspool of \emph{unsafe} compiler extensions.
-If we are willing to work with extensions, much of the boilerplate can be either generated or omitted entirely.
-
-The \gls{DSL} datatype is parametrised by a type variable providing a witness to the view on the language.
-Using constraint kinds, we can make these witnesses explicit, tying into \gls{HASKELL}'s type system immediately.
-Furthermore, when resorting to the \GHCmod{DataKinds} and \GHCmod{PolyKinds} extensions, this constraint does not necessarily has to be a single constraint, using a \haskelllhstexinline{Record} auxiliary type, we can encode list of witnesses.
-The data type for this list of witnesses is \haskelllhstexinline{Record}.
-Record is parametrised by two type variables, the first type variable (\haskelllhstexinline{dt}) is the data type on which the constraints can be applied.
-The second type variable (\haskelllhstexinline{clist}) is the list of constraints itself.
-It is not just a list of \haskelllhstexinline{Constraint} but it is a list containing constraint constructors that will, when given a type of kind \haskelllhstexinline{k}, produce a constraint.
-This means that when \haskelllhstexinline{Cons} is pattern matched, the type class constraint for \haskelllhstexinline{c dt} can be solved by the compiler.
-
-\begin{lstHaskellLhstex}[caption={Data type for a list of constraints}]
-data Record (dt :: k) (clist :: [k -> Constraint]) where
-       Nil  :: Record dt '[]
-    Cons :: c dt => Record dt cs -> Record dt (c ': cs)
-\end{lstHaskellLhstex}
-
-To incorporate this type in the \haskelllhstexinline{Expr} type, the \haskelllhstexinline{Ext} constructor changes as follows:
-
-\begin{lstHaskellLhstex}[caption={Data type for a list of constraints}]
-data Expr c
-    = Lit Int
-    | Add (Expr c) (Expr c)
-    | Ext (Record x c) x
-\end{lstHaskellLhstex}
-
-Furthermore, we define a type class that allows us to extract explicit dictionaries \haskelllhstexinline{Dict} from these records if the constraint can is present in the list.
-
-\begin{lstHaskellLhstex}[caption={Membership functions for constraints}]
-class c `In` cs where
-    project :: Record dt cs -> Dict (c dt)
-instance {-# OVERLAPPING #-} c `In` (c ': cs) where
-    project (Cons _) = Dict
-instance {-# OVERLAPPING #-} c `In` cs => c `In` (b ': cs) where
-    project (Cons xs) = project xs
-\end{lstHaskellLhstex}
-
-Finally, creating these \haskelllhstexinline{Record} witnesses is a chore so this can be automated as well using a \haskelllhstexinline{CreateRecord} type class that will create a record structure cell by cell if and only if all type class constraints are available.
-
-\begin{lstHaskellLhstex}[caption={Membership functions for constraints}]
-class CreateRecord dt c where
-    createRecord :: Record dt c
-instance CreateRecord d '[] where
-    createRecord = Nil
-instance (c (d c0), CreateRecord (d c0) cs) =>
-               CreateRecord (d c0) (c ': cs) where
-    createRecord = Cons createRecord
-\end{lstHaskellLhstex}
-
-The class constraints for the interpretation instances can now be greatly simplified, as shown in the evaluation instance for \haskelllhstexinline{Expr}.
-The implementation remains the same, only that for the extension case, a trick needs to be applied to convince the compiler of the correct instances.
-Using \haskelllhstexinline{`In`}'s \haskelllhstexinline{project} function, a dictionary can be brought into scope.
-This dictionary can then subsequently be used to apply the type class function on the extension using the \haskelllhstexinline{withDict} function from the \haskelllhstexinline{Data.Constraint} library\footnote{\haskelllhstexinline{withDict :: Dict c -> (c => r) -> r}}.
-The \GHCmod{ScopedTypeVariables} extension is used to make sure the existentially quantified type variable for the extension is matched to the type of the dictionary.
-
-\begin{lstHaskellLhstex}[caption={Evaluation instance for the main data type}]
-class Eval v where eval :: v -> Int
-
-instance Eval `In` s => Eval (Expr s) where
-    eval (Lit i) = i
-    eval (Add l r) = eval l + eval r
-    eval (Ext r (e :: x)) = withDict (project r :: Dict (Eval x)) eval e
-\end{lstHaskellLhstex}
-
-Smart constructors need to be adapted as well, as can be seen from the smart constructor \haskelllhstexinline{subst}.
-
-\begin{lstHaskellLhstex}[caption={Substitution smart constructor}]
-subst :: (Typeable c, CreateRecord (Subt c) c) => Expr c -> Expr c -> Expr c
-subst l r = Ext createRecord (l `Subt` r)
-\end{lstHaskellLhstex}
-
-Finally, defining terms in the language is can be done immediately if the interpretations are known.
-For example, if we want to print the term $~(~(42+(38-4)))$, we can define it as follows.
-
-\begin{lstHaskellLhstex}[caption={Substitution smart constructor}]
-e0 :: Expr '[Print,Opt]
-e0 = neg (neg (Lit 42 `Add` (Lit 38 `subt` Lit 4)))
-\end{lstHaskellLhstex}
-
-It is also possible to define terms in the \gls{DSL} as being overloaded in the interpretation.
-This does require enumerating all the \haskelllhstexinline{CreateRecord} type classes for every extension.
-At the call site, the concrete list of constraints must be known.
-
-\begin{lstHaskellLhstex}[caption={Substitution smart constructor}]
-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}
-
 \end{subappendices}
 
 \input{subfilepostamble}
index 3e92c03..0164cb2 100644 (file)
@@ -99,7 +99,7 @@ Extending the \gls{ADT} is easy and convenient but extending the views according
 The first downside of this type of \gls{EDSL} can be overcome by using \glspl{GADT}~\citep{cheney_first-class_2003}.
 \Cref{lst:exdeepgadt} shows the same language, but type-safe with a \gls{GADT}.
 \glspl{GADT} are not supported in the current version of \gls{CLEAN} and therefore the syntax is hypothetical (See \todo{insert link to appendix}).
-However, it has been shown that \glspl{GADT} can be simulated using bimaps or projection pairs~\citep[Sec.~2.2]{cheney_lightweight_2002}.
+However, it has been shown that \glspl{GADT} can be simulated using bimaps or projection pairs~\citep[\citesection{2.2}]{cheney_lightweight_2002}.
 Unfortunately the lack of extendability remains a problem.
 If a language construct is added, no compile time guarantee can be given that all views support it.
 
@@ -147,11 +147,11 @@ sub x y = \e->x e - y e
 \end{lstHaskell}
 
 Moreover, the language is type safe as it is directly typed in the host language, i.e.\ \haskellinline{lit True `plus` lit 4} is rejected.
-Another advantage is the intimate link with the host language, allowing for a lot more linguistic reuse such as the support of implicit sharing~\cite{krishnamurthi_linguistic_2001}.
+Another advantage is the intimate link with the host language, allowing for a lot more linguistic reuse such as the support of implicit sharing \citep{krishnamurthi_linguistic_2001}.
 
 The downside of this method is extending the language with views.
 It is nearly impossible to add views to a shallowly embedded language.
-The only way of achieving this is by reimplementing all functions so that they run all backends at the same time or to create a single interpretation that produces a fold function~\citep{gibbons_folding_2014}.
+The only way of achieving this is by reimplementing all functions so that they run all backends at the same time or to create a single interpretation that produces a fold function \citep{gibbons_folding_2014}.
 
 \subsection{Tagless-final embedding}\label{ssec:tagless}
 By lifting the functions representing the \gls{DSL} terms to type classes, interpretations can be added.
@@ -168,7 +168,7 @@ class DSL v where
 
 An interpretation of this view is a data type that implements the type class.
 
-\begin{lstHaskell}[label={lst:extagless},caption={A minimal tagless-final \gls{EDSL}.}]
+\begin{lstHaskell}[label={lst:extaglessprint},caption={A pretty printer for the tagless-final \gls{EDSL}.}]
 data Print a = P {runPrint :: String}
 instance DSL Print where
        lit a = P (show a)
@@ -207,7 +207,7 @@ Both flavours have their strengths and weaknesses and both flavours can be impro
 
 \begin{table}[ht]
        \begin{threeparttable}[b]
-               \caption{Comparison of embedding techniques, adapted from \citet[Sec.~3.6]{sun_compositional_2022}}%
+               \caption{Comparison of embedding techniques, adapted from \citet[\citesection{3.6}]{sun_compositional_2022}}%
                \label{tbl:dsl_comparison}
                \begin{tabular}{lllllll}
                        \toprule
index 9193b82..5585363 100644 (file)
@@ -118,7 +118,7 @@ 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[Sec.~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}:
 
@@ -262,7 +262,7 @@ Metaprogramming is a special flavour of programming where programs have the abil
 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[Sec.~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.
@@ -711,7 +711,7 @@ 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[Chp.~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}.
@@ -796,7 +796,7 @@ In generic programming, types are represented as sums of products and using this
 
 For example, Rhiger showed a method for expressing statically typed pattern matching using typed higher-order functions~\citep{rhiger_type-safe_2009}.
 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.
-Atkey et al.\ 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[Sec.~3.3]{atkey_unembedding_2009}.
+Atkey et al.\ 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}.
 
 McDonell et al.\ extends on this idea, resulting in a very similar but different solution to ours~\citep{mcdonell_embedded_2022}.
 They used the technique that Atkey et al.\ showed and applied it to deep embedding using the concrete syntax of the host language.
index 53d3b15..3897350 100644 (file)
@@ -3,7 +3,7 @@
 \input{subfilepreamble}
 
 \begin{document}
-\chapter{Introduction}%
+\chapter{Prelude}%
 \label{chp:introduction}
 
 \begin{chapterabstract}
@@ -78,7 +78,7 @@ Writing idiomatic domain-specific code in an \gls{DSL} is easy but this may come
 \begin{figure}[ht]
        \centering
        \includestandalone{hyponymy_of_dsls}
-       \caption{Hyponymy of \glspl{DSL} (adapted from \citet[pg.\ 2]{mernik_extensible_2013})}%
+       \caption{Hyponymy of \glspl{DSL} (adapted from \citet[\citepage{2}]{mernik_extensible_2013})}%
        \label{fig:hyponymy_of_dsls}
 \end{figure}
 
@@ -90,7 +90,7 @@ Examples of standalone \glspl{DSL} are regular expressions, make, yacc, XML, SQL
 
 A dichotomous approach is embedding the \gls{DSL} in a host language, i.e.\ \glspl{EDSL}~\citep{hudak_modular_1998}.
 By defining the language as constructs in the host language, much of the machinery is inherited and the cost of creating embedded languages is very low.
-There is more linguistic reuse~\cite{krishnamurthi_linguistic_2001}.
+There is more linguistic reuse \citep{krishnamurthi_linguistic_2001}.
 There are however two sides to the this coin.
 If the syntax of the host language is not very flexible, the syntax of the \gls{DSL} may become clumsy.
 Furthermore, errors shown to the programmer may be larded with host language errors, making it difficult for a non-expert of the host language to work with the \gls{DSL}.
@@ -129,7 +129,7 @@ This approach to software development is called \gls{TOSD}~\citep{wang_maintaini
                \includestandalone{tosd}
                \caption{\Gls{TOSD} approach.}
        \end{subfigure}
-       \caption{Separation of concerns in a traditional setting and in \gls{TOSD} (adapted from~\cite[pg.\ 20]{wang_maintaining_2018}).}%
+       \caption{Separation of concerns in a traditional setting and in \gls{TOSD} (adapted from \citet[\citesection{1}]{wang_maintaining_2018}).}%
        \label{fig:tosd}
 \end{figure}
 
@@ -161,12 +161,11 @@ While \gls{ITASK} conceived \gls{TOP}, it is not the only \gls{TOP} language.
 \citet{piers_task-oriented_2016} created \textmu{}Task, a \gls{TOP} language for specifying non-interruptible embedded systems implemented as an \gls{EDSL} in \gls{HASKELL}.
 \citet{van_gemert_task_2022} created LTasks, a \gls{TOP} language for interactive terminal applications implemented in LUA, a dynamically typed imperative language.
 \citet{lijnse_toppyt_2022} created Toppyt, a \gls{TOP} language based on \gls{ITASK}, implemented in \gls{PYTHON}, but designed to be simpler and smaller.
-Finally there is \gls{MTASK}, \gls{TOP} language designed for defining workflow for \gls{IOT} devices~\cite{koopman_task-based_2018}.
+Finally there is \gls{MTASK}, \gls{TOP} language designed for defining workflow for \gls{IOT} devices \citep{koopman_task-based_2018}.
 It is written in \gls{CLEAN} as an \gls{EDSL} fully integrated with \gls{ITASK} and allows the programmer to define all layers of an \gls{IOT} system from a single source.
 
 \section{Outline}
-\todo[inline]{uitbreiden}
-On Wikipedia, a rhapsody is defined as follows~\citep{wikipedia_contributors_rhapsody_2022}:
+Wikipedia defines a rhapsody as follows \citep{wikipedia_contributors_rhapsody_2022}:
 \begin{quote}
        A \textbf{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. An air of spontaneous inspiration and a sense of improvisation make it freer in form than a set of variations.
 \end{quote}
@@ -180,22 +179,26 @@ This movement is a cumulative---paper-based---movement that focusses on techniqu
 After reading the first chapter, subsequent chapters in this movement are readable independently.
 
 \subsubsection*{\fullref{chp:dsl_embedding_techniques}}
-This chapter shows the basic \gls{DSL} embedding techniques and compares the properties of several embedding methods.
-This chapter is not based on a paper and written as a extra background material for the subsequent chapters in the movement.
+This chapter outlines the basic \gls{DSL} embedding techniques and compares the properties of several embedding methods.
+By example, it provides intuition on shallow embedding, including tagless-final embedding and deep embedding, including deep embedding with \acrshortpl{GADT}.
+It is not based on a paper but written as gentle background material for the subsequent chapters in the movement.
 
 \subsubsection*{\fullref{chp:classy_deep_embedding}}
-This chapter is based on the paper: \bibentry{lubbers_deep_2022}\todo{change in-press when published}.
+This chapter is based on the paper: \citeentry{lubbers_deep_2022}\todo{change in-press when published}
 
 While supervising \citeauthor{amazonas_cabral_de_andrade_developing_2018}'s \citeyear{amazonas_cabral_de_andrade_developing_2018} Master's thesis, focussing on an early version of \gls{MTASK}, a seed was planted for a novel deep embedding technique for \glspl{DSL} where the resulting language is extendible both in constructs and in interpretation using type classes and existential data types.
 Slowly the ideas organically grew to form the technique shown in the paper.
 
 The research from this paper and writing the paper was solely performed by me.
 \Cref{sec:classy_reprise} was added after publication and contains a (yet) unpublished extension of the embedding technique.
+The related work section (\cref{sec:cde:related}) is also brought up to date.\todo{weghalen als dit niet het geval is}
 
 \subsubsection*{\fullref{chp:first-class_datatypes}}
-This chapter is based on the paper: \bibentry{lubbers_first-class_2022}\todo{change when accepted}.
+This chapter is based on the paper: \citeentry{lubbers_first-class_2022}\todo{change when accepted}
 
-It shows how to inherit data types from the host language in \glspl{EDSL} using metaprogramming.
+When embedding \glspl{DSL} many features of the host language can be inherited.
+However, data types from the host are not first-class citizens, in order to use the datatypes, access functions need to be created in the \gls{DSL} resulting in boilerplate.
+This paper shows how to inherit data types from the host language in \glspl{EDSL} using metaprogramming by generating the boilerplate required.
 
 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.
 
@@ -203,12 +206,12 @@ The research in this paper and writing the paper was performed by me, though the
 This part is a monograph focussing on \glspl{TOP} for the \gls{IOT} and hence are the chapters best read in order.
 The monograph is compiled from the following papers and revised lecture notes.
 
-\newcommand{\citeentry}[1]{\begin{NoHyper}\bibentry{#1}\end{NoHyper}. \citep{#1}}
 \begin{itemize}
        \item \citeentry{koopman_task-based_2018}
 
-               This was the initial \gls{TOP}/\gls{MTASK} paper.
-               Pieter Koopman wrote it, I helped with the software and research.
+               While an imperative predecessor of \gls{MTASK} was conceived in 2017 \citep{plasmeijer_shallow_2016}, this paper showed the first \gls{TOP} version of \gls{MTASK}.
+               It shows the design of the language and three intepretations: pretty printing, simulation using \gls{ITASK} and \gls{C} code generation.
+               Pieter Koopman wrote the paper, I helped with the software and research.
        \item \citeentry{lubbers_task_2018}
                
                This paper was an extension of my Master's thesis~\citep{lubbers_task_2017}.
index 392fc22..26b8e42 100644 (file)
 \apptocmd{\thebibliography}{\raggedright}{}{}
 \usepackage{bibentry} % Cite bib entry completely
 \nobibliography*
+\newcommand{\citeentry}[1]{\begin{NoHyper}\bibentry{#1}\end{NoHyper}. \citep{#1}}
+
+\makeatletter
+\newcommand{\citepage}[1]{p.~#1}
+\newcommand{\citepages}[1]{pp.~#1}
+\newcommand{\citechapter}[1]{\cref@chapter@name~#1}
+\newcommand{\citechapters}[1]{\cref@chapter@name@plural~#1}
+\newcommand{\citesection}[1]{\cref@section@name~#1}
+\newcommand{\citesections}[1]{\cref@section@name@plural~#1}
+%\newcommand{\citesection}[1]{\S.~#1}
+%\newcommand{\citesections}[1]{\S\S.~#1}
+\newcommand{\citeparagraph}[1]{\P.~#1}
+\newcommand{\citeparagraphs}[1]{\P\P.~#1}
+\makeatother
 
 % Graphics
 \usepackage{graphicx} % Images
index 9281f2b..4d3cc66 100644 (file)
 \subfile{intro/introduction}
 % DSL
 
-\part[Prelude: Domain-Specific Languages]{Prelude:\\[2ex]\smaller{}Domain-Specific Languages}%
+\part[\'Etude: Domain-Specific Languages]{\'Etude:\\[2ex]\smaller{}Domain-Specific Languages}%
 \label{prt:dsl}
 \subfile{dsl/dsl_techniques}        % DSL Techniques
 \subfile{dsl/class_deep_embedding}  % Deep embedding with class
 \subfile{dsl/first-class_datatypes} % First-class data types
 
-\part[Exposition: Task-Oriented Programming]{Exposition:\\[2ex]\smaller{}Task-Oriented Programming for the Internet of Things}%
+\part[Oratorio: Task-Oriented Programming]{Oratorio\\[2ex]\smaller{}Task-Oriented Programming for the Internet of Things}%
 \label{prt:top}
 \subfile{top/mtask} % MTask tutorial and implementation
 
index 25200c4..95a01c2 100644 (file)
@@ -85,7 +85,7 @@ void loop() {
 Unfortunately, this does not work because the \arduinoinline{delay} function blocks all further execution.
 The resulting program will blink the \glspl{LED} after each other instead of at the same time.
 To overcome this, it is necessary to slice up the blinking behaviour in very small fragments so it can be manually interleaved~\citep{feijs_multi-tasking_2013}.
-Listing~\ref{lst:blinkthread} shows how three different blinking patterns might be achieved in \gls{ARDUINO} using the slicing method.
+\Cref{lst:blinkthread} shows how three different blinking patterns might be achieved in \gls{ARDUINO} using the slicing method.
 If we want the blink function to be a separate parametrizable function we need to explicitly provide all references to the required state.
 Furthermore, the \arduinoinline{delay} function can not be used and polling \arduinoinline{millis} is required.
 The \arduinoinline{millis} function returns the number of milliseconds that have passed since the boot of the microprocessor.
@@ -256,7 +256,7 @@ For convenience, there are many lower-cased macro definitions for often used con
 \Cref{lst:example_exprs} shows some examples of these expressions.
 \cleaninline{e0} defines the literal $42$, \cleaninline{e1} calculates the literal $42.0$ using real numbers.
 \cleaninline{e2} compares \cleaninline{e0} and \cleaninline{e1} as integers and if they are equal it returns the \cleaninline{e2}$/2$ and \cleaninline{e0} otherwise.
-\cleaninline{approxEqual} performs an approximate equality---albeit not taking into account all floating point pecularities---and demonstrates that \gls{CLEAN} can be used as a macro language, i.e.\ maximise linguistic reuse~\cite{krishnamurthi_linguistic_2001}.
+\cleaninline{approxEqual} performs an approximate equality---albeit not taking into account all floating point pecularities---and demonstrates that \gls{CLEAN} can be used as a macro language, i.e.\ maximise linguistic reuse \citep{krishnamurthi_linguistic_2001}.
 \todo{uitzoeken waar dit handig is}
 When calling \cleaninline{approxEqual} in an \gls{MTASK} function, the resulting code is inlined.
 
index 22c7a6f..9679a93 100644 (file)
@@ -943,13 +943,13 @@ The sensor node measures and reports the temperature every ten seconds to the se
        \label{table_t4t:temp}
        \begin{tabular}{llccl}
                \toprule
-               Location      & Functionality & \gls{PWTS} & \gls{CWTS} & Lines (\cref{lst_t4t:mtaskTemp})\\
+               Location      & Functionality      & \gls{PWTS} & \gls{CWTS} & Lines (\cref{lst_t4t:mtaskTemp})\\
                \midrule
-               Sensor Node   & Sensor Interface   &   14       & 3          &~\ref{lst_t4t:mtaskTemp:si0},~\ref{lst_t4t:mtaskTemp:si1},~\ref{lst_t4t:mtaskTemp:si2}\\
-                             & Sensor Node        &    67       & 4          &~\ref{lst_t4t:mtaskTemp:sn0},~\ref{lst_t4t:mtaskTemp:sn1},~\ref{lst_t4t:mtaskTemp:sn2},~\ref{lst_t4t:mtaskTemp:sn3}\\
-               Server        & Web Interface      &    17      & 3          &~\ref{lst_t4t:mtaskTemp:wi0},~\ref{lst_t4t:mtaskTemp:wi1},~\ref{lst_t4t:mtaskTemp:wi2}\\
-                             & Database Interface &     106     & 2          &~\ref{lst_t4t:mtaskTemp:di0},~\ref{lst_t4t:mtaskTemp:di1}\\
-               Communication & Communication      &     94    & 3          &~\ref{lst_t4t:mtaskTemp:co0},~\ref{lst_t4t:mtaskTemp:co1},~\ref{lst_t4t:mtaskTemp:co2}\\
+               Sensor Node   & Sensor Interface   & 14         & 3          & \labelcref{lst_t4t:mtaskTemp:si0,lst_t4t:mtaskTemp:si1,lst_t4t:mtaskTemp:si2}\\
+                             & Sensor Node        & 67         & 4          & \labelcref{lst_t4t:mtaskTemp:sn0,lst_t4t:mtaskTemp:sn1,lst_t4t:mtaskTemp:sn2,lst_t4t:mtaskTemp:sn3}\\
+               Server        & Web Interface      & 17         & 3          & \labelcref{lst_t4t:mtaskTemp:wi0,lst_t4t:mtaskTemp:wi1,lst_t4t:mtaskTemp:wi2}\\
+                             & Database Interface & 106        & 2          & \labelcref{lst_t4t:mtaskTemp:di0,lst_t4t:mtaskTemp:di1}\\
+               Communication & Communication      & 94         & 3          & \labelcref{lst_t4t:mtaskTemp:co0,lst_t4t:mtaskTemp:co1,lst_t4t:mtaskTemp:co2}\\
                \midrule
 %              \multicolumn{2}{c}{Total (\textnumero{} Files)} & 298 (27)    & 15 (1) \\
 Total \gls{SLOC}    &       & 298     & 15  \\
@@ -1160,7 +1160,6 @@ We show that \emph{tierless languages have the potential to significantly reduce
 \begin{enumerate*}
        \item Tierless developers need to manage less interoperation: \gls{CRS} uses a single \gls{DSL} and paradigm, and \gls{CWS} uses two \glspl{DSL} in a single paradigm and three source code files. In contrast, both \gls{PRS} and \gls{PWS} use at least six languages in two paradigms and spread over at least 35 source code files (\cref{table_t4t:multi,table_t4t:languages,table_t4t:paradigms}). Thus, a tierless stack minimises semantic friction.
        \item Tierless developers benefit from automatically generated, and hence correct, communication (\cref{lst_t4t:mtaskTemp}), and write 6$\times$ less communication code (\cref{fig_t4t:multipercentage}).
-%and TODO).%~\ref{lst_t4t:mqtt}).
        \item Tierless developers can exploit powerful high-level declarative and task-oriented \gls{IOT} programming abstractions (\cref{table_t4t:temp}), specifically the composable, higher-order task combinators outlined in \cref{sec_t4t:itasks}. 
 Our empirical results for \gls{IOT} systems are consistent with the benefits claimed for tierless languages in other application domains. Namely that a tierless language provides a \textit{Higher Abstraction Level}, \textit{Improved Software Design}, and improved \textit{Program Comprehension}~\citep{weisenburger2020survey}.
 \end{enumerate*}