From: Mart Lubbers Date: Thu, 15 Sep 2022 13:31:39 +0000 (+0200) Subject: many updates X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;h=c15776f71f5efe186708e2604ff8f32115c8ac3d;p=phd-thesis.git many updates --- diff --git a/.chktexrc b/.chktexrc index 44ec2fd..bf386c6 100644 --- a/.chktexrc +++ b/.chktexrc @@ -2,11 +2,13 @@ CmdLine { -v } VerbEnvir { - lstinline lstlisting algorithm code spec lstClean lstHaskell lstHaskellLhstex + lstinline lstlisting algorithm code spec lstClean lstHaskell lstHaskellLhstex lstArduino } WipeArg { \cleaninline:{} \haskellinline:{} + \haskelllshtexinline:{} + \arduinoinline:{} \texttt:{} \url:{} \only:{} diff --git a/Exported Items.bib b/Exported Items.bib deleted file mode 100644 index 1212c7d..0000000 --- a/Exported Items.bib +++ /dev/null @@ -1,19 +0,0 @@ - -@inproceedings{hentschel_supersensors:_2016, - address = {Vienna, Austria}, - title = {Supersensors: {Raspberry} {Pi} {Devices} for {Smart} {Campus} {Infrastructure}}, - isbn = {978-1-5090-4052-0}, - shorttitle = {Supersensors}, - url = {http://ieeexplore.ieee.org/document/7575844/}, - doi = {10.1109/FiCloud.2016.16}, - abstract = {We describe an approach for developing a campuswide sensor network using commodity single board computers. We sketch various use cases for environmental sensor data, for different university stakeholders. Our key premise is that supersensors—sensors with significant compute capability—enable more flexible data collection, processing and reaction. In this paper, we describe the initial prototype deployment of our supersensor system in a single department at the University of Glasgow.}, - language = {en}, - urldate = {2019-09-04}, - booktitle = {2016 {IEEE} 4th {International} {Conference} on {Future} {Internet} of {Things} and {Cloud} ({FiCloud})}, - publisher = {IEEE}, - author = {Hentschel, Kristian and Jacob, Dejice and Singer, Jeremy and Chalmers, Matthew}, - month = aug, - year = {2016}, - pages = {58--62}, - file = {Hentschel et al. - 2016 - Supersensors Raspberry Pi Devices for Smart Campu.pdf:/home/mrl/.local/share/zotero/storage/ATK53FN2/Hentschel et al. - 2016 - Supersensors Raspberry Pi Devices for Smart Campu.pdf:application/pdf}, -} diff --git a/appendix/bytecode.tex b/appendix/bytecode.tex new file mode 100644 index 0000000..44ad97e --- /dev/null +++ b/appendix/bytecode.tex @@ -0,0 +1,107 @@ +\documentclass[../thesis.tex]{subfiles} + +\begin{document} +\ifSubfilesClassLoaded{ + \pagenumbering{arabic} +}{} + +\chapter{Bytecode instruction set}% +\label{chp:bytecode_instruction_set} +\todo[inline]{formatting} + +\begin{tabular}{ll} + $l$ & label\\ + $w_r$ & return width\\ + $w_a$ & argument width\\ + $fp$ & frame pointer\\ + $sp$ & stack pointer\\ + $pc$ & program counter\\ +\end{tabular} + +Bytecode is byte encoded, stack has 16-bit cells. +Longs and reals are stored with the MSB first. + +\footnotesize +\begin{longtable}{lllll} + \caption{\normalsize Semantics for the bytecode instructions\label{tbl:instr_task}} + \endfirsthead% + \caption{\normalsize Semantics for the bytecode instructions (cont.)} + \endhead% + \endfoot% + \endlastfoot% + \toprule + Instr. & Args & Semantics & sp & pc\\ + + \midrule + \texttt{return} & $w_r~w_a$ & $st[fp\shortminus{}w_a\shortminus{}3+i] = st[fp+1]$ & $st[fp\shortminus{}w_a\shortminus{}3+w_r]$ & $st[fp\shortminus{}w_a\shortminus{}1]$\\ + & & {\bf for all} $i\in\{0..w_r\}$\\ + & & $fp = st[fp\shortminus{}w_a\shortminus{}2]$\\ + \texttt{jumpF} & $l$ & & $sp\shortminus{}1$ & $\left\{\begin{array}{ll} pc+1 & \textrm{\bf if } st[sp\shortminus{}1]\\l & \textrm{\bf otherwise}\end{array}\right.$\\ + \texttt{jump} & $l$ & & $sp\shortminus{}1$ & $l$\\ + \texttt{jumpSR} & $w_a~l$ & $st[sp\shortminus{}w_a\shortminus{}1]=pc+2$ & & $l$\\ + \texttt{tailCall} & $w_{a_1}~w_{a_2}~l$ & $rotate\:(w_{a_1}+3+w_{a_2},w_{a_2})$ & $fp$ & $jl$\\ + & & $fp = fp-w_{a_1}+w_{a_2}$\\ + & & \multicolumn{3}{l}{{\bf where} $w_{a_1}$ is the width of the current function and $w_{a_2}$ the width of the called function}\\ + \texttt{arg} & $i$ & $st[sp] = st[fp-1-i]$ & $sp+1$\\ + \texttt{push} & $n~b_0\ldots b_n$ & $st[sp+i] = s[i]$ & $sp+n$ & $pc+2+n$\\ + & & {\bf for all} $i\in\{0..n\}$\\ +% \midrule + \texttt{pop} & $n$ & & $sp-n$ & $pc+2$\\ +% \midrule + \texttt{rot} & $d~n$ & $rotate\:(d, n)$ & $sp$ & $pc+3$\\ +% \midrule + \texttt{dup} & & $st[sp] = st[sp-1]$ & $sp+1$ & $pc+1$\\ +% \midrule + \texttt{pushPtrs} & & $st[sp] = sp$ & $sp+3$ & $pc+1$\\ + & & $st[sp+1] = fp$\\ + & & $st[sp+2] = 0$\\ +% \midrule + \texttt{unOp} & & $st[sp-1] = \diamond{}st[sp-1]$ & $sp$ & $pc+1$\\ + & & \multicolumn{3}{l}{{\bf for all} $\diamond\in\{\neg\}$}\\ +% \midrule + \texttt{binOp} & & $st[sp-2] = st[sp-2] \mathbin{\oplus} st[sp-1]$ & $sp-1$ & $pc+1$\\ + & & \multicolumn{3}{l}{{\bf for all} $\oplus\in\{+, -, *, /, \wedge, \vee, \equiv, \not\equiv, \leq, \geq, <, >\}$}\\ +% \midrule + \texttt{mkTask} & \texttt{Stable\textsubscript{n}} & $st[sp-n-1] = node (stable,$ & $sp-n+1$ & $pc+2$\\ + & & $\qquad\qquad st[sp-1], \ldots, st[sp-n-1])$\\ + \texttt{mkTask} & \texttt{Unstable\textsubscript{n}} & $st[sp-n-1] = node (unstable,$ & $sp-n+1$ & $pc+2$\\ + & & $\qquad\qquad st[sp-1], \ldots, st[sp-n-1])$\\ +% \midrule +% & \multicolumn{3}{l}{Unstable\textsubscript{n}} & st[sp-n-1] = node (unstable, & sp-n+1 & pc+2\\ +% & \multicolumn{3}{l}{} & \qquad\qquad st[sp-1], \textrm{\ldots}, st[sp-n-1])\\ +% \midrule +% +% & \multicolumn{3}{l}{ReadD } & st[sp-1] \ \ = node (readd, st[sp-1]) & & pc+2\\ +% \midrule +% & \multicolumn{3}{l}{ReadA } & st[sp-1] \ \ = node (reada, st[sp-1]) & & pc+2\\ +% \midrule +% & \multicolumn{3}{l}{Repeat } & st[sp-1] \ \ = node (repeat, st[sp-1]) & & pc+2\\ +% \midrule +% & \multicolumn{3}{l}{Delay } & st[sp-1] \ \ = node (delay, st[sp-1]) & & pc+2\\ +% \midrule +% +% & \multicolumn{3}{l}{WriteD } & st[sp-2] \ \ = node (writed, st[sp-1], st[sp-2]) & sp-1 & pc+2\\ +% \midrule +% & \multicolumn{3}{l}{WriteA } & st[sp-2] \ \ = node (writea, st[sp-1], st[sp-2]) & sp-1 & pc+2\\ +% \midrule +% & \multicolumn{3}{l}{And } & st[sp-2] \ \ = node (and, st[sp-1], st[sp-2]) & sp-1 & pc+2\\ +% \midrule +% & \multicolumn{3}{l}{Or } & st[sp-2] \ \ = node (or, st[sp-1], st[sp-2]) & sp-1 & pc+2\\ +% \midrule +% +% & \multicolumn{3}{l}{SdsSet i } & st[sp-1] \ \ = node (sdsset,i, st[sp-1]) & & pc+3\\ +% \midrule +% +% & \multicolumn{3}{l}{SdsGet i } & st[sp]\ \ \ \ \ = node (sdsget, i) & sp+1 & pc+3\\ +% \midrule +% & \multicolumn{3}{l}{DHTTemp i } & st[sp-1] \ \ = node (dhttemp, i) & sp+1 & pc+3\\ +% \midrule +% & \multicolumn{3}{l}{DHTHumid i } & st[sp-1] \ \ = node (dhthumid, i) & sp+1 & pc+3\\ +% \midrule +% +% & \multicolumn{3}{l}{Step aw jl } & st[sp-1] \ \ = node (step, aw, jl, st[sp-1]) & sp-1 & pc+5\\ + \bottomrule +\end{longtable} + +\input{subfilepostamble} +\end{document} diff --git a/appendix/clean_for_haskell_programmers.tex b/appendix/clean_for_haskell_programmers.tex index 521e2d6..65dfb87 100644 --- a/appendix/clean_for_haskell_programmers.tex +++ b/appendix/clean_for_haskell_programmers.tex @@ -3,32 +3,18 @@ \begin{document} \ifSubfilesClassLoaded{ - \author{% - Mart Lubbers\\ - \texttt{mart@cs.ru.nl} - \and - Peter Achten\\ - \texttt{peter@cs.ru.nl} - } - \title{Clean for Haskell Programmers} - \date{\today} - - \stopthumb{}% - \setcounter{chapter}{1} - \pagenumbering{arabic} - \maketitle - \tableofcontents }{ - \chapter{\texorpdfstring{\glsentrytext{CLEAN}}{Clean} for \texorpdfstring{\glsentrytext{HASKELL}}{Haskell} Programmers}% - \label{chp:clean_for_haskell_programmers} } +\chapter{\texorpdfstring{\glsentrytext{CLEAN}}{Clean} for \texorpdfstring{\glsentrytext{HASKELL}}{Haskell} Programmers}% +\label{chp:clean_for_haskell_programmers} + This note is meant to give people who are familiar with the functional programming 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. 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 follow below. +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. While \gls{CLEAN} and \gls{HASKELL} were both conceived around 1987 and have similar syntax, there are some subtle differences in syntax and functionality. @@ -44,7 +30,7 @@ However, over the years, the syntax got friendlier and it currently it looks a l In the past, a \emph{double-edged} fronted even existed that allowed \gls{CLEAN} to be extended with \gls{HASKELL98} syntax and vice versa, however this frontend is no longer maintained~\cite{groningen_exchanging_2010}. This chapter therefore gives a brief syntactical and functional comparison, a complete specification of the \gls{CLEAN} language can be found in the latest language report~\cite{plasmeijer_clean_2021}. Many of this is based on work by Achten although that was based on \gls{CLEAN} 2.1 and \gls{HASKELL98}~\cite{achten_clean_2007}. -When \gls{HASKELL} is mentioned we actually mean \gls{GHC}'s \gls{HASKELL} and by \gls{CLEAN} we mean \gls{CLEAN} 3.1's \gls{ITASK} compiler. +When \gls{HASKELL} is mentioned we actually mean \gls{GHC}'s \gls{HASKELL}\footnote{If an extension is enabled, a footnote is added stating that \GHCmod{SomeExtension} is required.} this is denoted and by \gls{CLEAN} we mean \gls{CLEAN} 3.1's compiler with the \gls{ITASK} extensions. \section{Features} \subsection{Modules} @@ -57,17 +43,17 @@ Choosing what is exported in \gls{HASKELL} is done using the \haskellinline{modu \subsection{Strictness} In \gls{CLEAN}, by default, all expressions are evaluated lazily. -Types can be annotated with a strictness attribute (\cleaninline{!}), resulting in the values being evaluated to head-normal form before the function is entered. +Types can be annotated with a strictness attributes (\cleaninline{!}), resulting in the values being evaluated to head-normal form before the function is entered. In \gls{HASKELL}, in patterns, strictness can be enforced using \haskellinline{!}\requiresGHCmod{BangPatterns}. Within functions the strict let (\cleaninline{#!}) can be used to force evaluate an expression, in \gls{HASKELL} \haskellinline{seq} or \haskellinline{\$!} is used for this. \subsection{Uniqueness typing} -Types in \gls{CLEAN} may be \emph{unique}, which means that they may not be shared\todo{cite}. +Types in \gls{CLEAN} may be \emph{unique}, which means that they may not be shared~\cite{barendsen_uniqueness_1996}. The uniqueness type system allows the compiler to generate efficient code because unique data structures can be destructively updated. -Furthermore, uniqueness typing serves as a model for side effects as well. -\Gls{CLEAN} uses the \emph{world-as-value} paradigm where \cleaninline{World} represents the external environment and is always unique. +Furthermore, uniqueness typing serves as a model for side effects as well~\cite{achten_high_1993,achten_ins_1995}. +\Gls{CLEAN} uses the \emph{world-as-value} paradigm where \cleaninline{World} represents the external environment and is always unique~\cite{backus_introduction_1990}. A program with side effects is characterised by a \cleaninline{Start :: *World -> *World} start function. -In \gls{HASKELL}, interaction with the world is done using the \haskellinline{IO} monad. +In \gls{HASKELL}, interaction with the world is done using the \haskellinline{IO} monad~\cite{peyton_jones_imperative_1993}. The \haskellinline{IO} monad could very well be---and actually is---implemented in \gls{CLEAN} using a state monad with the \cleaninline{World} as a state. Besides marking types as unique, it is also possible to mark them with uniqueness attributes variables \cleaninline{u:} and define constraints on them. For example, to make sure that an argument of a function is at least as unique as another argument. @@ -75,7 +61,7 @@ Finally, using \cleaninline{.} (a dot), it is possible to state that several var Uniqueness is propagated automatically in function types but must be marked manually in data types. Examples can be seen in \cref{lst:unique_examples}. -\begin{lstClean}[label={lst:unique_examples},caption={Examples of uniqueness annotations in \gls{CLEAN}.}] +\begin{lstClean}[label={lst:unique_examples},caption={Examples of uniqueness annotations.}] f :: *a -> *a // f works on unique values only f :: .a -> .a // f works on unique and non-unique values f :: v:a u:b -> u:b, [v<=u] // f works when a is less unique than b @@ -85,9 +71,32 @@ 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} -\todo[inline]{Matches pattern expression \texttt{=:}} +Patterns in \gls{CLEAN} can be used as predicates as well~\cite[Chp.~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. + +\begin{lstClean}[label={lst:matches_pattern_expression},caption={Examples of \emph{matches pattern} expressions.}] +isNil :: [a] -> Bool +isNil l = l=:[] + +:: T = A Int | B Bool -\todo[inline]{Let before} +ifAB :: T a a -> a +ifAB x ifa ifb = if (x =: (A _)) ifa ifb +\end{lstClean} + +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~\cite[Chp.~3.5.4]{plasmeijer_clean_2021}). + +\begin{lstClean}[label={lst:let_before},caption={Let before expression example.}] +readChars :: *File -> ([Char], *File) +readChars file +# (ok, char, file) = freadc file +| not ok = ([], file) +# (chars, file) = readChars file += ([char:chars], file) +\end{lstClean} \subsection{Generics} Polytypic functions~\cite{jeuring_polytypic_1996}---also known as generic or kind-indexed fuctions---are built into \gls{CLEAN}~\cite[Chp.~7.1]{plasmeijer_clean_2021}\cite{alimarine_generic_2005} whereas in \gls{HASKELL} they are implemented as a library~\cite[Chp.~6.19.1]{ghc_team_ghc_2021}. @@ -101,7 +110,7 @@ Metadata about the types is available using the \cleaninline{of} syntax that giv \lstinputlisting[language=Clean,firstline=4,label={lst:generic_print},caption={Generic print function in \gls{CLEAN}.}]{lst/generic_print.icl} \subsection{\texorpdfstring{\glsentrytext{GADT}}{GADT}s} -GADTs are enriched data types that allow the type instantiation of the constructor to be explicitly defined~\cite{cheney_first-class_2003,hinze_fun_2003}. +\Glspl{GADT} are enriched data types that allow the type instantiation of the constructor to be explicitly defined~\cite{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~\cite[Sec.~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}. diff --git a/backmatter/acknowledgements.tex b/backmatter/acknowledgements.tex index 804daab..61f46ab 100644 --- a/backmatter/acknowledgements.tex +++ b/backmatter/acknowledgements.tex @@ -12,20 +12,24 @@ Funding: Teun de Groot, Ton van Heusden Supervisors: Pieter Koopman, Rinus Plasmeijer, Jan-Martin Jansen -Colleagues: Jurriën Stutterheim, Laszlo Domoslai, Arjan Oortgiese, Bas Lijnse, Steffen Michels, Markus Klinik, Tim Steenvoorden, Camil Staps, Hans-Nikolai Vie\ss{}mann, John van Groningen, Sven-Bodo Scholz, Sjaak Smetsers, Fok Bolderheij, Simone Meeuwsen, Peter Achten - -Co-authors: Jeremy Singer, Phil Trinder, Adrian Ramsingh - -\todo{Second assessor clients weglaten?: Willem, Dave, Gijs} -Students: Matheus Amazonas Cabral de Andrade, Haye B\"ohm, Erin van der Veen, Colin de Roos, Willem de Vos, Michel de Boer, Dave Artz, Sjoerd Crooijmans, Gijs Alberts, Arjen Nederveen - -Mentors: Jos Baack, Francisco Torreira, Franc Grootjen, the late Louis Vuurpijl, Ralf Hinze - -Friends: Pieter Wolfert and Annerieke Wessels; Chris Kamphuis and Maudy Bijen; Koen Dercksen and Michelle Everard; George Gregoire; Larry Caruthers; Tim Hirschler; Emma Dahl. - -Family: Parents (in law), brothers (in law), oma, - -Marie-José van Diem, Elly Koopman +Co-authors: Jeremy Singer, Phil Trinder, Adrian Ramsingh, Sustrainable group + +%Colleagues: Jurriën Stutterheim, Laszlo Domoslai, Arjan Oortgiese, Bas Lijnse, Steffen Michels, Markus Klinik, Tim Steenvoorden, Camil Staps, Hans-Nikolai Vie\ss{}mann, John van Groningen, Sven-Bodo Scholz, Sjaak Smetsers, Fok Bolderheij, Simone Meeuwsen, Peter Achten, Ingrid Berenbroek +% +% +%\todo{Second assessor clients weglaten?: Willem, Dave, Gijs} +%Students: Matheus Amazonas Cabral de Andrade, Haye B\"ohm, Erin van der Veen, Colin de Roos, Willem de Vos, Michel de Boer, Dave Artz, Sjoerd Crooijmans, Gijs Alberts, Arjen Nederveen, Elina Antonova +% +%Mentors: Jos Baack, Francisco Torreira, Franc Grootjen, the late Louis Vuurpijl, Ralf Hinze +% +%Friends: Pieter Wolfert (and Annerieke Wessels); Chris Kamphuis and Maudy Bijen; Koen Dercksen and Michelle Everard; George Gregoire; Larry Caruthers; Tim Hirschler; Emma Dahl; Truman Crandell; +%\selectlanguage{russian} +%Александер Барков; +%\selectlanguage{british} +% +%Family: Parents (in law), brothers (in law), oma, +% +%Marie-José van Diem, Ellie Kimenai \end{center} \input{subfilepostamble} \end{document} diff --git a/backmatter/curriculum_vitae.tex b/backmatter/curriculum_vitae.tex index 25ea235..30524cd 100644 --- a/backmatter/curriculum_vitae.tex +++ b/backmatter/curriculum_vitae.tex @@ -12,7 +12,7 @@ Mart Lubbers \noindent% \begin{tabular}{rp{.75\linewidth}} - 1992 & Born on the 27th of May, Oldenzaal\\ + 1992 & Born May 27th, Oldenzaal\\ 2004{--}2011 & VWO at the Twents Carmelcollege De Thij, Oldenzaal\\ 2011{--}2015 & Bachelor's Degree Artificial Intelligence at the Radboud University, Nijmegen\\ 2013{--}2015 & Research Assistant at the Max Planck Institute for Psycholinguistics\\ @@ -21,7 +21,14 @@ Mart Lubbers 2017 & Researcher at the Netherlands Defense Academy, Den Helder in the faculty of Military Sciences (fMIL).\\ 2018 & Researcher at the Radboud University, Nijmegen in the Institute for Computing and Information Sciences (iCIS).\\ 2018{--}2023 & PhD Candidate at the Radboud University, Nijmegen in the Institute for Computing and Information Sciences (iCIS). +% & Educational programmes participated in during PhD track:\\ +% & Education in a Nutshell\\ +% & Effective Writing Strategies\\ +% & Kinderen Enthousiasmeren voor de Wetenschap\\ +% & University Teaching Qualification\\ \end{tabular} +\todo[inline]{include educational programmes participated in during the PhD track?} + \input{subfilepostamble} \end{document} diff --git a/backmatter/research_data_management.tex b/backmatter/research_data_management.tex index 53e2701..430d5fb 100644 --- a/backmatter/research_data_management.tex +++ b/backmatter/research_data_management.tex @@ -14,6 +14,11 @@ The following research datasets have been produced during this PhD research: \todo{reference correct chapters} \begin{itemize} \item \ldots + \item \rdmentry{Chapter 0} + {\mlubbers} + {2022} + {Literate Haskell/lhs2TeX source code for the paper ``Deep Embedding with Class'': TFP 2022} + {Zenodo}{10.5281/zenodo.6650880} %chktex 8 \item \rdmentry{Chapter 0} {\mlubbers; \pkoopman; \rplasmeijer} {2021} diff --git a/backmatter/samenvatting.tex b/backmatter/samenvatting.tex index dab0c29..0c1ee31 100644 --- a/backmatter/samenvatting.tex +++ b/backmatter/samenvatting.tex @@ -7,12 +7,14 @@ \chapter{Samenvatting}% \label{chp:samenvatting} +\selectlanguage{dutch} \begin{center} \noindent% -Dit is een samenvatting. +Dit is een samenvatting van 350--400 woorden. \end{center} \input{subfilepostamble} +\selectlanguage{british} \end{document} diff --git a/backmatter/summary.tex b/backmatter/summary.tex index 5657a67..7e4f260 100644 --- a/backmatter/summary.tex +++ b/backmatter/summary.tex @@ -10,7 +10,7 @@ \begin{center} \noindent% -This is a summary. +This is a summary of 350--400 words. \end{center} diff --git a/conclusion/conclusion.tex b/conclusion/conclusion.tex index 568d51f..ea20f10 100644 --- a/conclusion/conclusion.tex +++ b/conclusion/conclusion.tex @@ -5,7 +5,7 @@ \pagenumbering{arabic} }{} -\chapter{Conclusion}% +\chapter{Coda}% \label{chp:conclusion} \input{subfilepostamble} diff --git a/domain-specific_languages/class_deep_embedding.tex b/domain-specific_languages/class_deep_embedding.tex index 3e43cbb..8c96393 100644 --- a/domain-specific_languages/class_deep_embedding.tex +++ b/domain-specific_languages/class_deep_embedding.tex @@ -8,7 +8,7 @@ \chapter{Deep embedding with class}% \label{chp:classy_deep_embedding} -\begin{quote} +\begin{chapterabstract} The two flavours of DSL embedding are shallow and deep embedding. In functional languages, shallow embedding models the language constructs as functions in which the semantics are embedded. Adding semantics is therefore cumbersome while adding constructs is a breeze. @@ -20,7 +20,7 @@ This paper shows that by abstracting the semantics functions in deep embedding to type classes, it is possible to easily add language constructs as well. So-called classy deep embedding results in DSLs that are extensible both in language constructs and in semantics while maintaining a concrete abstract syntax tree. Additionally, little type-level trickery or complicated boilerplate code is required to achieve this. -\end{quote} +\end{chapterabstract} \section{Introduction}% The two flavours of DSL embedding are deep and shallow embedding~\cite{boulton_experience_1992}. @@ -125,7 +125,7 @@ sub_s e1 e2 = e1 - e2 Adding semantics on the other hand---e.g.\ a printer---is not that simple because the semantics are part of the functions representing the language constructs. One way to add semantics is to change all functions to execute both semantics at the same time. -In our case this means changing the type of \haskelllhstexinline{Sem_s} to be \haskellinline{(Int, String)} so that all functions operate on a tuple containing the result of the evaluator and the printed representation at the same time. %chktex 36 +In our case this means changing the type of \haskelllhstexinline{Sem_s} to be \haskelllhstexinline{(Int, String)} so that all functions operate on a tuple containing the result of the evaluator and the printed representation at the same time. %chktex 36 Alternatively, a single semantics can be defined that represents a fold over the language constructs~\cite{gibbons_folding_2014}, delaying the selection of semantics to the moment the fold is applied. \subsection{Tagless-final embedding} @@ -141,7 +141,7 @@ class Expr_t s where Semantics become data types\footnotemark{} implementing these type classes, resulting in the following instance for the evaluator. \footnotetext{% - In this case \haskelllhstexinline{newtype}s are used instead of regular \haskellinline{data} declarations. + 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~\cite[Sec.~4.2.3]{peyton_jones_haskell_2003}. @@ -179,7 +179,6 @@ instance Sub_t Printer_t where \end{lstHaskellLhstex} \section{Lifting the backends}% - Let us rethink the deeply embedded DSL design. Remember that in shallow embedding, the semantics are embedded in the language construct functions. Obtaining extensibility both in constructs and semantics was accomplished by abstracting the semantics functions to type classes, making the constructs overloaded in the semantics. @@ -219,7 +218,7 @@ instance Eval_1 Sub_1 where The astute reader might have noticed that we have dissociated ourselves from the original data type. 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 \haskellinline{Expr_1}. +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~\cite{mitchell_abstract_1988} type with type class constraints~\cite{laufer_combining_1994,laufer_type_1996} for all semantics type classes~\cite[Chp.~6.4.6]{ghc_team_ghc_2021} to allow it to house not just subtraction but any future extension. @@ -264,7 +263,7 @@ e2p = Ext_2 (Lit_2 42 `Sub_2` Lit_2 1) \subsection{Unbraiding the semantics from the data} This approach does reveal a minor problem. Namely, that all semantics type classes are braided into our datatypes via the \haskelllhstexinline{Ext_2} constructor. -Say if we add the printer again, the \haskelllhstexinline{Ext_2} constructor has to be modified to contain the printer type class constraint as well\footnote{Resulting in the following constructor: \haskellinline{forall x.(Eval_2 x, Print_2 x) => Ext_2 x}.}. %chktex 36 +Say if we add the printer again, the \haskelllhstexinline{Ext_2} constructor has to be modified to contain the printer type class constraint as well\footnote{Resulting in the following constructor: \haskelllhstexinline{forall x.(Eval_2 x, Print_2 x) => Ext_2 x}.}. %chktex 36 Thus, if we add semantics, the main data type's type class constraints in the \haskelllhstexinline{Ext_2} constructor need to be updated. To avoid this, the type classes can be bundled in a type class alias or type class collection as follows. @@ -287,15 +286,13 @@ First the data types for the language constructs are parametrised by the type va data Expr_3 d = Lit_3 Int | Add_3 (Expr_3 d) (Expr_3 d) | forall x. Ext_3 (d x) x -\end{lstHaskellLhstex} -\begin{lstHaskellLhstex} data Sub_3 d = Sub_3 (Expr_3 d) (Expr_3 d) \end{lstHaskellLhstex} The \haskelllhstexinline{d} type variable is inhabited by an explicit dictionary for the semantics, i.e.\ a witness to the class instance. Therefore, for all semantics type classes, a data type is made that contains the semantics function for the given semantics. -This means that for \haskelllhstexinline{Eval_3}, a dictionary with the function \haskellinline{EvalDict_3} is defined, a type class \haskellinline{HasEval_3} for retrieving the function from the dictionary and an instance for \haskellinline{HasEval_3} for \haskellinline{EvalDict_3}. +This means that for \haskelllhstexinline{Eval_3}, a dictionary with the function \haskelllhstexinline{EvalDict_3} is defined, a type class \haskelllhstexinline{HasEval_3} for retrieving the function from the dictionary and an instance for \haskelllhstexinline{HasEval_3} for \haskelllhstexinline{EvalDict_3}. \begin{lstHaskellLhstex} newtype EvalDict_3 v = EvalDict_3 (v -> Int) @@ -308,7 +305,7 @@ instance HasEval_3 EvalDict_3 where \end{lstHaskellLhstex} The instances for the type classes change as well according to the change in the datatype. -Given that there is a \haskelllhstexinline{HasEval_3} instance for the witness type \haskellinline{d}, we can provide an implementation of \haskellinline{Eval_3} for \haskellinline{Expr_3 d}. +Given that there is a \haskelllhstexinline{HasEval_3} instance for the witness type \haskelllhstexinline{d}, we can provide an implementation of \haskelllhstexinline{Eval_3} for \haskelllhstexinline{Expr_3 d}. \begin{lstHaskellLhstex} instance HasEval_3 d => Eval_3 (Expr_3 d) where @@ -320,7 +317,7 @@ instance HasEval_3 d => Eval_3 (Sub_3 d) where eval_3 (Sub_3 e1 e2) = eval_3 e1 - eval_3 e2 \end{lstHaskellLhstex} -Because the \haskelllhstexinline{Ext_3} constructor from \haskellinline{Expr_3} now contains a value of type \haskellinline{d}, the smart constructor for \haskellinline{Sub_3} must somehow come up with this value. +Because the \haskelllhstexinline{Ext_3} constructor from \haskelllhstexinline{Expr_3} now contains a value of type \haskelllhstexinline{d}, the smart constructor for \haskelllhstexinline{Sub_3} must somehow come up with this value. To achieve this, a type class is introduced that allows the generation of such a dictionary. \begin{lstHaskellLhstex} @@ -414,7 +411,7 @@ instance HasOpt_3 d => Opt_3 (Expr_3 d) where opt_3 (Ext_3 d x) = Ext_3 d (getOpt_3 d x) \end{lstHaskellLhstex} -Replicating this for the \haskelllhstexinline{Opt_3} instance of \haskellinline{Sub_3} seems a clear-cut task at first glance. +Replicating this for the \haskelllhstexinline{Opt_3} instance of \haskelllhstexinline{Sub_3} seems a clear-cut task at first glance. \begin{lstHaskellLhstex} instance HasOpt_3 d => Opt_3 (Sub_3 d) where @@ -430,7 +427,7 @@ To overcome this problem we add a convolution constructor. \subsection{Convolution}% -Adding a loopback case or convolution constructor to \haskelllhstexinline{Sub_3} allows the removal of the \haskellinline{Sub_3} constructor while remaining the \haskellinline{Sub_3} type. +Adding a loopback case or convolution constructor to \haskelllhstexinline{Sub_3} allows the removal of the \haskelllhstexinline{Sub_3} constructor while remaining the \haskelllhstexinline{Sub_3} type. It should be noted that a loopback case is \emph{only} required if the transformation actually removes tags. This changes the \haskelllhstexinline{Sub_3} data type as follows. @@ -459,8 +456,8 @@ Pattern matching within datatypes and from an extension to the main data type wo Cross-extensional pattern matching on the other hand---matching on a particular extension---is something that requires a bit of extra care. Take for example negation propagation and double negation elimination. Pattern matching on values with an existential type is not possible without leveraging dynamic typing~\cite{abadi_dynamic_1991,baars_typing_2002}. -To enable dynamic typing support, the \haskelllhstexinline{Typeable} type class as provided by \haskellinline{Data.Dynamic}~\cite{ghc_team_datadynamic_2021} is added to the list of constraints in all places where we need to pattern match across extensions. -As a result, the \haskelllhstexinline{Typeable} type class constraints are added to the quantified type variable \haskellinline{x} of the \haskellinline{Ext_4} constructor and to \haskellinline{d}s in the smart constructors. +To enable dynamic typing support, the \haskelllhstexinline{Typeable} type class as provided by \haskelllhstexinline{Data.Dynamic}~\cite{ghc_team_datadynamic_2021} is added to the list of constraints in all places where we need to pattern match across extensions. +As a result, the \haskelllhstexinline{Typeable} type class constraints are added to the quantified type variable \haskelllhstexinline{x} of the \haskelllhstexinline{Ext_4} constructor and to \haskelllhstexinline{d}s in the smart constructors. \begin{lstHaskellLhstex} data Expr_4 d = Lit_4 Int @@ -497,16 +494,18 @@ If the sub expression is again a negation, something that can only be found out \begin{lstHaskellLhstex} instance (Typeable d, GDict (d (Neg_4 d)), HasOpt_4 d) => Opt_4 (Neg_4 d) where - opt_4 (Neg_4 (Add_4 e1 e2)) = NegLoop_4 (Add_4 (opt_4 (neg_4 e1)) (opt_4 (neg_4 e2))) - opt_4 (Neg_4 (Ext_4 d x)) = case fromDynamic (toDyn (getOpt_4 d x)) of - Just (Neg_4 e) -> NegLoop_4 e - _ -> Neg_4 (Ext_4 d (getOpt_4 d x)) - opt_4 (Neg_4 e) = Neg_4 (opt_4 e) - opt_4 (NegLoop_4 e) = NegLoop_4 (opt_4 e) + opt_4 (Neg_4 (Add_4 e1 e2)) + = NegLoop_4 (Add_4 (opt_4 (neg_4 e1)) (opt_4 (neg_4 e2))) + opt_4 (Neg_4 (Ext_4 d x)) + = case fromDynamic (toDyn (getOpt_4 d x)) of + Just (Neg_4 e) -> NegLoop_4 e + _ -> Neg_4 (Ext_4 d (getOpt_4 d x)) + opt_4 (Neg_4 e) = Neg_4 (opt_4 e) + opt_4 (NegLoop_4 e) = NegLoop_4 (opt_4 e) \end{lstHaskellLhstex} Loopback cases do make cross-extensional pattern matching less modular in general. -For example, \haskelllhstexinline{Ext_4 d (SubLoop_4 (Lit_4 0))} is equivalent to \haskellinline{Lit_4 0} in the optimisation semantics and would require an extra pattern match. +For example, \haskelllhstexinline{Ext_4 d (SubLoop_4 (Lit_4 0))} is equivalent to \haskelllhstexinline{Lit_4 0} in the optimisation semantics and would require an extra pattern match. Fortunately, this problem can be mitigated---if required---by just introducing an additional optimisation semantics that removes loopback cases. Luckily, one does not need to resort to these arguably blunt matters often. Dependent language functionality often does not need to span extensions, i.e.\ it is possible to group them in the same data type. @@ -528,7 +527,7 @@ instance (Opt_4 v, Print_4 v) => GDict (OptPrintDict_4 v) where gdict = OPD_4 gdict gdict \end{lstHaskellLhstex} -And this allows us to write \haskelllhstexinline{print_4 (opt_4 e1)} resulting in \verb|"((~42)+(~38))"| when \haskellinline{e1} represents $(\sim(42+38))-0$ and is thus defined as follows. +And this allows us to write \haskelllhstexinline{print_4 (opt_4 e1)} resulting in \verb|"((~42)+(~38))"| when \haskelllhstexinline{e1} represents $(\sim(42+38))-0$ and is thus defined as follows. \begin{lstHaskellLhstex} e1 :: Expr_4 OptPrintDict_4 @@ -553,9 +552,9 @@ Where some solutions to the expression problem do not easily generalise to GADTs Generalising the data structure of our DSL is fairly straightforward and to spice things up a bit, we add an equality and boolean not language construct. To make the existing DSL constructs more general, we relax the types of those constructors. For example, operations on integers now work on all numerals instead. -Moreover, the \haskelllhstexinline{Lit_g} constructor can be used to lift values of any type to the DSL domain as long as they have a \haskellinline{Show} instance, required for the printer. -Since some optimisations on \haskelllhstexinline{Not_g} remove constructors and therefore use cross-extensional pattern matches, \haskellinline{Typeable} constraints are added to \haskellinline{a}. -Furthermore, because the optimisations for \haskelllhstexinline{Add_g} and \haskellinline{Sub_g} are now more general, they do not only work for \haskellinline{Int}s but for any type with a \haskellinline{Num} instance, the \haskellinline{Eq} constraint is added to these constructors as well. +Moreover, the \haskelllhstexinline{Lit_g} constructor can be used to lift values of any type to the DSL domain as long as they have a \haskelllhstexinline{Show} instance, required for the printer. +Since some optimisations on \haskelllhstexinline{Not_g} remove constructors and therefore use cross-extensional pattern matches, \haskelllhstexinline{Typeable} constraints are added to \haskelllhstexinline{a}. +Furthermore, because the optimisations for \haskelllhstexinline{Add_g} and \haskelllhstexinline{Sub_g} are now more general, they do not only work for \haskelllhstexinline{Int}s but for any type with a \haskelllhstexinline{Num} instance, the \haskelllhstexinline{Eq} constraint is added to these constructors as well. Finally, not to repeat ourselves too much, we only show the parts that substantially changed. The omitted definitions and implementation can be found in \cref{sec:cde:appendix}. @@ -572,18 +571,20 @@ data Not_g d a where NotLoop_g :: Expr_g d a -> Not_g d a \end{lstHaskellLhstex} -The smart constructors for the language extensions inherit the class constraints of their data types and include a \haskelllhstexinline{Typeable} constraint on the \haskellinline{d} type variable for it to be usable in the \haskellinline{Ext_g} constructor as can be seen in the smart constructor for \haskellinline{Neg_g}: +The smart constructors for the language extensions inherit the class constraints of their data types and include a \haskelllhstexinline{Typeable} constraint on the \haskelllhstexinline{d} type variable for it to be usable in the \haskelllhstexinline{Ext_g} constructor as can be seen in the smart constructor for \haskelllhstexinline{Neg_g}: \begin{lstHaskellLhstex} -neg_g :: (Typeable d, GDict (d (Neg_g d)), Typeable a, Num a) => Expr_g d a -> Expr_g d a +neg_g :: (Typeable d, GDict (d (Neg_g d)), Typeable a, Num a) => + Expr_g d a -> Expr_g d a neg_g e = Ext_g gdict (Neg_g e) -not_g :: (Typeable d, GDict (d (Not_g d))) => Expr_g d Bool -> Expr_g d Bool +not_g :: (Typeable d, GDict (d (Not_g d))) => + Expr_g d Bool -> Expr_g d Bool not_g e = Ext_g gdict (Not_g e) \end{lstHaskellLhstex} Upgrading the semantics type classes to support GADTs is done by an easy textual search and replace. -All occurrences of \haskelllhstexinline{v} are now parametrised by type variable \haskellinline{a}: +All occurrences of \haskelllhstexinline{v} are now parametrised by type variable \haskelllhstexinline{a}: \begin{lstHaskellLhstex} class Eval_g v where @@ -608,7 +609,7 @@ instance HasEval_g EvalDict_g where \end{lstHaskellLhstex} The \haskelllhstexinline{GDict} type class is general enough, so the instances can remain the same. -The \haskelllhstexinline{Eval_g} instance of \haskellinline{GDict} looks as follows: +The \haskelllhstexinline{Eval_g} instance of \haskelllhstexinline{GDict} looks as follows: \begin{lstHaskellLhstex} instance Eval_g v => GDict (EvalDict_g v) where @@ -619,11 +620,12 @@ Finally, the implementations for the instances can be ported without complicatio \begin{lstHaskellLhstex} instance (Typeable d, GDict (d (Not_g d)), HasOpt_g d) => Opt_g (Not_g d) where - opt_g (Not_g (Ext_g d x)) = case fromDynamic (toDyn (getOpt_g d x)) :: Maybe (Not_g d Bool) of + opt_g (Not_g (Ext_g d x)) + = case fromDynamic (toDyn (getOpt_g d x)) :: Maybe (Not_g d Bool) of Just (Not_g e) -> NotLoop_g e _ -> Not_g (Ext_g d (getOpt_g d x)) - opt_g (Not_g e) = Not_g (opt_g e) - opt_g (NotLoop_g e) = NotLoop_g (opt_g e) + opt_g (Not_g e) = Not_g (opt_g e) + opt_g (NotLoop_g e) = NotLoop_g (opt_g e) \end{lstHaskellLhstex} \section{Conclusion}% @@ -791,8 +793,10 @@ instance HasOpt_g d => Opt_g (Sub_g d) where opt_g (SubLoop_g e) = SubLoop_g (opt_g e) instance (Typeable d, GDict (d (Neg_g d)), HasOpt_g d) => Opt_g (Neg_g d) where - opt_g (Neg_g (Add_g e1 e2)) = NegLoop_g (Add_g (opt_g (neg_g e1)) (opt_g (neg_g e2))) - opt_g (Neg_g (Ext_g d x)) = case fromDynamic (toDyn (getOpt_g d x)) of + opt_g (Neg_g (Add_g e1 e2)) + = NegLoop_g (Add_g (opt_g (neg_g e1)) (opt_g (neg_g e2))) + opt_g (Neg_g (Ext_g d x)) + = case fromDynamic (toDyn (getOpt_g d x)) of Just (Neg_g e) -> NegLoop_g e _ -> Neg_g (Ext_g d (getOpt_g d x)) opt_g (Neg_g e) = Neg_g (opt_g e) diff --git a/domain-specific_languages/dsl_techniques.tex b/domain-specific_languages/dsl_techniques.tex index fae4ec3..e603d09 100644 --- a/domain-specific_languages/dsl_techniques.tex +++ b/domain-specific_languages/dsl_techniques.tex @@ -60,11 +60,11 @@ eval :: Expr -> Value eval (Lit i) = i eval (Plus l r) = case (eval l, eval r) of (Lit (I l), Lit (I r)) -> I (l+r)) - (l, r) -> error $ "Cannot add " ++ show l ++ " to " ++ show r + (l, r) -> error ("Can't add " ++ show l ++ " to " ++ show r) eval (Eq l r) = case (eval l, eval r) of (Lit (I l), Lit (I r)) -> B (l==r) (Lit (B l), Lit (B r)) -> B (l==r) - (l, r) -> error $ "Cannot compare " ++ show l ++ " to " ++ show r + (l, r) -> error ("Can't compare " ++ show l ++ " to " ++ show r) \end{lstHaskell} Luckily this problem can be overcome by switching from regular \glspl{ADT} to \glspl{GADT}, resulting in the following data type and evaluator. @@ -88,7 +88,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}~\cite{cheney_first-class_2003}. Example~\ref{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. +\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~\cite{cheney_first-class_2003}. 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. @@ -136,7 +136,7 @@ This will mean that every component will have to implement all views rendering i \section{Shallow embedding} -\subsection{Tagless-final embedding} +\subsection{Tagless-final embedding}\label{ssec:tagless} \section{Comparison} diff --git a/domain-specific_languages/first-class_datatypes.tex b/domain-specific_languages/first-class_datatypes.tex index 6e36cf8..e897e00 100644 --- a/domain-specific_languages/first-class_datatypes.tex +++ b/domain-specific_languages/first-class_datatypes.tex @@ -5,7 +5,7 @@ \pagenumbering{arabic} }{} -\chapter{First-class datatypes}% +\chapter{First-class datatypes \ldots}% \label{chp:first-class_datatypes} TFP22 diff --git a/frontmatter/motto.tex b/frontmatter/motto.tex index 1c96bbe..bf9dcb6 100644 --- a/frontmatter/motto.tex +++ b/frontmatter/motto.tex @@ -19,9 +19,9 @@ (Manuscripts don't burn) }{% \selectlanguage{russian} - Михаил Афанасьевич Булгаков\\ + М.А. (Mихаил) Булгаков\\ \selectlanguage{british} - (Mikhail Afanesyevich Bulgakov) + (M.A. (Mikhail) Bulgakov) } \epigraph{% You start a question, and it's like starting a stone. diff --git a/frontmatter/titlepage.tex b/frontmatter/titlepage.tex index 1412d9f..c5011d5 100644 --- a/frontmatter/titlepage.tex +++ b/frontmatter/titlepage.tex @@ -37,7 +37,7 @@ \vspace{0.5cm} - op donderdag 1 juni 2023 \\ + op donderdag 1 juni 2023\\ om 12:00 uur precies \vspace{0.5cm} diff --git a/glossaries.tex b/glossaries.tex index fea90a3..9922387 100644 --- a/glossaries.tex +++ b/glossaries.tex @@ -11,9 +11,11 @@ \newacronym{CWS}{PWS}{clean wemos supersensor} \newacronym{FP}{FP}{functional programming} \newacronym{GRS}{GRS}{graph rewriting system} +\newacronym{GPIO}{GPIO}{general-purpose \acrlong{IO}} \newacronym{GUI}{GUI}{graphical \acrlong{UI}} \newacronym{IOT}{IoT}{internet of things} \newacronym{LEAN}{LEAN}{language of East-Anglia and Nijmegen} +\newacronym{LED}{LED}{light-emitting diode} \newacronym{TOP}{TOP}{task-oriented programming} \newacronym{TOSD}{TOSD}{task-oriented software development} \newacronym{TRS}{TRS}{term rewriting system} @@ -22,7 +24,9 @@ \newacronym{BLE}{BLE}{Bluetooth low energy} \newacronym{API}{API}{application programming interface} \newacronym{OS}{OS}{operating system} +\newacronym{IO}{IO}{input/output} \newacronym{RTOS}{RTOS}{real-time \acrshort{OS}} +\newacronym{RAM}{RAM}{random-access memory} \newacronym{OTA}{OTA}{over-the-air} \newacronym{MCU}{MCU}{microcontroller unit} \newacronym{UI}{UI}{user interface} @@ -50,3 +54,19 @@ name=Haskell98, description={is a standardised version of \gls{HASKELL}} } +\newglossaryentry{ARDUINO}{% + name=Arduino, + description={is a widely used framework for programming microprocessors} +} +\newglossaryentry{CPP}{ + name=C\texttt{++}, + description={is a general-purpose imperative programming language based on \gls{C}} +} +\newglossaryentry{C}{ + name=C, + description={is a general-purpose imperative programming} +} +\newglossaryentry{I2C}{ + name=I\textsuperscript{2}C, + description={is a simple serial communication protocol often used to connect sensors to microprocessors} +} diff --git a/img/orcid.png b/introduction/img/orcid.png similarity index 100% rename from img/orcid.png rename to introduction/img/orcid.png diff --git a/introduction/introduction.tex b/introduction/introduction.tex index 9a0282f..384fe48 100644 --- a/introduction/introduction.tex +++ b/introduction/introduction.tex @@ -162,63 +162,132 @@ This approach to software development is also called \gls{TOSD}~\cite{wang_maint \end{description} \section{Outline} +\todo[inline]{uitbreiden} %\epigraph{% % \textbf{rhapsody} /\textipa{['r\ae{}ps@di]}/ \emph{noun} (pl.\ \textbf{-ies}) a piece of music that is full of feeling and is not regular in form: Liszt's Hungarian Rhapsodies. %}{% % Oxford Advanced Learners Dictionary~\cite{margaret_deuter_rhapsody_2015}. %} -Wikipedia defines a \emph{rhapsody} as follows~\cite{wikipedia_contributors_rhapsody_2022}: +This thesis is structured as a purely functional rhapsody. +On Wikipedia, a rhapsody is defined as follows~\cite{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} This thesis follows the tradition and consists of three movements that are episodic yet integrated. -The first movement is about embedded \gls{DSL} techniques, the second movement elaborates on \gls{TOP} for the \gls{IOT} and the third and last movement compares traditional tiered \gls{IOT} architectures to a tierless architectures such as \gls{TOP}. +\Cref{prt:dsl} is about \gls{EDSL} techniques, \cref{prt:top} elaborates on \gls{TOP} for the \gls{IOT} and \cref{prt:tvt} compares traditional tiered \gls{IOT} architectures to a tierless architectures such as \gls{TOP}. The movements are readable independently if the reader is familiarised with the background material provided in \cref{chp:introduction}. +The thesis wraps up with \cref{chp:conclusion} that provides a conclusion and an outlook on future work. -\paragraph{\Cref{prt:dsl}} is a cumulative or paper-based movement that focusses on techniques for embedding \glspl{DSL} in functional programming lanugages. +\subsection{\Cref{prt:dsl}: Domain-specific languages} +This movement is a cumulative or paper-based movement that focusses on techniques for embedding \glspl{DSL} in functional programming lanugages. After reading the first chapter, subsequent chapters in this movement are readable as independently. -\subparagraph{\Cref{chp:dsl_embedding_techniques}} shows all the basic techniques and compares the properties. +\subsubsection{\Cref{chp:dsl_embedding_techniques}} +This chapter shows all the basic techniques and compares the properties of several embedding methods. This chapter is not based on a paper and written as a background for the subsequent chapters in the movement. -\subparagraph{\Cref{chp:classy_deep_embedding}} -This chapter is based on the paper: \emph{Deep Embedding with Class}~\todo[inline]{cite when published}. +\subsubsection{\Cref{chp:classy_deep_embedding}} +This chapter is based on the paper: \emph{Deep Embedding with Class}~\todo{cite when published}. + During a Master's thesis supervision~\cite{amazonas_cabral_de_andrade_developing_2018}, 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. -\subparagraph{\Cref{chp:first-class_datatypes}} shows how to inherit data types in embedded \glspl{DSL} using metaprogramming. -This chapter is based on the paper: \emph{First-Class Data Types in Shallow Embedded Domain-Specific Languages using Metaprogramming}~\todo[inline]{cite when accepted}. +\subsubsection{\Cref{chp:first-class_datatypes}} shows how to inherit data types in \glspl{EDSL} using metaprogramming. +This chapter is based on the paper: \emph{First-Class Data Types in Shallow Embedded Domain-Specific Languages using Metaprogramming}~\todo{cite when accepted}. -The research in this paper and writing the paper was performed by me, though there were weekly meetings with Pieter Koopman an Rinus Plasmeijer in which we discussed and refined the ideas. +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. -\subparagraph{\Cref{chp:strongly-typed_multi-view_stack-based_computations}} shows how to use advanced \gls{DSL} techniques to embed type safe stack-based computations in a host language. -This chapter is based on the paper: \emph{Strongly-Typed Multi-View Stack-Based Computations}~\todo[inline]{cite when accepted}. +\subsubsection{\Cref{chp:strongly-typed_multi-view_stack-based_computations}} shows how to use advanced \gls{DSL} techniques to embed type safe stack-based computations in a host language. +This chapter is based on the paper: \emph{Strongly-Typed Multi-View Stack-Based Computations}~\todo{cite when accepted}. +\todo{Zal ik dit paper wel opnemen? Aangezien Pieter het grotendeels gedaan heeft?} -I supported Pieter Koopman in performing the research in this paper. -The paper was mostly written by Pieter Koopman\todo{probably}. +I supported Pieter Koopman in performing the research in this paper by writing some of the software. +The paper was mostly written by Pieter Koopman\todo{probably will be}. -\paragraph{\Cref{prt:top}} is a monograph focussing on \glspl{TOP} for the \gls{IOT}. +\subsection{\Cref{prt:top}: Task-oriented \texorpdfstring{\acrlong{IOT}}{internet of things} programming } +This part is a monograph focussing on \glspl{TOP} for the \gls{IOT}. Therefore, the chapters depend on eachother and are best read in order. The monograph is compiled from the following papers and revised lecture notes. \begin{itemize} \item \bibentry{koopman_task-based_2018}. - \item \bibentry{lubbers_task_2017} (extension of Master's thesis~\cite{lubbers_task_2018}). + + This was the initial \gls{TOP}/\gls{MTASK} paper. + Pieter Koopman wrote it but I helped with the software and research. + \item \bibentry{lubbers_task_2018}. + + This paper was an extension of my Master's thesis~\cite{lubbers_task_2017}. + It shows how a simple imperative variant of \gls{MTASK} was integrated with \gls{ITASK}. + While the language was a lot different than later versions, the integration mechanism is still used in \gls{MTASK} today. + + The research in this paper and writing the paper was performed by me, though there were weekly meetings with Pieter Koopman and Rinus Plasmeijer in which we discussed and refined the ideas. \item \bibentry{lubbers_multitasking_2019}. - \item \emph{Simulation of a Task-Based Embedded Domain Specific Language for the Internet of Things}~\todo[inline]{cite when published} - \item \emph{Writing Internet of Things applications with Task Oriented Programming}~\todo[inline]{cite when published} + + This paper was a short paper on the multitasking capabilities of \gls{MTASK} in contrast to traditional multitasking methods for \gls{ARDUINO}. + \item \emph{Simulation of a Task-Based Embedded Domain Specific Language for the Internet of Things}~\todo{cite when published} + + These revised lecture notes are from a course on the \gls{MTASK} simulator was provided at the 2018 CEFP/3COWS winter school in Ko\v{s}ice, Slovakia. + + Pieter Koopman wrote and taught it though I helped with the software and research. + \item \emph{Writing Internet of Things applications with Task Oriented Programming}~\todo{cite when published} + + These revised lecture notes are from a course on programming in \gls{MTASK} provided at the 2019 CEFP/3COWS summer school in Budapest, Hungary. + + Pieter prepared half of the lecture. I wrote the lecture notes, prepared the other half of the lecture, the assignments and practical session. \item \bibentry{lubbers_interpreting_2019}. - \item \emph{Reducing the Power Consumption of IoT with Task-Oriented Programming}~\todo[inline]{cite when published} (extensios of Master's thesis by Sjoerd Crooijmans~\cite{crooijmans_reducing_2021}). - \item \emph{Asynchronous Shared Data Sources}~\todo[inline]{cite when accepted} + + This paper showed an implementation for \gls{MTASK} for microcontrollers in the form of a compilation scheme and informal semantics description. + + The research in this paper and writing the paper was performed by me, though there were weekly meetings with Pieter Koopman and Rinus Plasmeijer in which we discussed and refined the ideas. + \item \emph{Reducing the Power Consumption of IoT with Task-Oriented Programming}~\todo{cite when published} + + This paper shows how to create a scheduler so that devices running \gls{MTASK} tasks can go to sleep more automatically. + Furthermore, it shows how to integrate hardware interrupts into \gls{MTASK}. + The research was carried out by Sjoerd Crooijmans during his Master's thesis~\cite{crooijmans_reducing_2021}. + I did the daily supervision and helped with the research, Pieter Koopman was the formal supervisor and wrote most of the paper. + \item \emph{Asynchronous Shared Data Sources}~\todo{cite when accepted} + + \todo[inline]{This paper could in theory be dropped in favour of being done sooner with the thesis} + + Asynchronous \glspl{SDS} are used in the current \gls{ITASK} system and allow bigger \gls{IOT} devices such as raspberry pi's to be used in a tierless \gls{ITASK} system. + The example application shown in \cref{prt:tvt} heavily uses asynchronous \glspl{SDS}. + This paper shows how to lift \glspl{SDS} to operate asynchronously independent of \gls{ITASK} or another \gls{TOP} implementation. + + The initial research was carried out by Haye B\"ohm during his Master's thesis~\cite{bohm_asynchronous_2019}. + I did the daily supervision and helped with the research, Pieter Koopman and Rinus Plasmeijer were the formal supervisors. + I extended and generalised the research and wrote the paper. \item \emph{Green Computing for the Internet of Things}~\todo[inline]{cite when done} - \item \emph{T.B.A.}~\todo[inline]{cite when done} + + These revised lecture notes are from a course on sustainable programming using \gls{MTASK} provided at the 2022 Sustrainable summer school in Rijeka, Croatia. + + Pieter prepared half of the lecture. I wrote the lecture notes, prepared the other half of the lecture, the assignments and the practical session. \end{itemize} -\paragraph{\Cref{prt:tvt}} -This chapter focusses on comparing traditional tiered architectures to tierless architectures and is based on a single journal paper that extensed on a conference paper. +The movement is made up out of the following chapters +\todo[inline]{preliminary} + +\begin{itemize} + \item The mTask language (includes informal semantics) + \begin{itemize} + \item Expressions + \item Functions + \item Tasks + \item Shares + \item Peripherals + \end{itemize} + \item Interpretations/views/backends\todo{decide on terminology} + \item Green computing + \item Integration with iTask + \item Implementation (based on IFL19 paper) + \item TOP for IoT beyond microprocessors +\end{itemize} + +\subsection{\Cref{prt:tvt}: Tiered versus tierless programming} +These chapters focus on comparing traditional tiered architectures to tierless architectures and are based on a single journal paper that extended on a conference paper. +The conference paper was partly funded by the Radboud-Glasgow Collaboration Fund. It does both a qualitative and a quantitative four-way comparison of a smart campus application. The research in these papers and writing them was performed by all authors. @@ -230,8 +299,6 @@ Adrian Ramsingh created the micropython implementation (\acrshort{PWS}), the ori \item \emph{Could Tierless Languages Reduce IoT Development Grief?}~\todo[inline]{cite when accepted} \end{itemize} -\paragraph{\Cref{chp:conclusion}} finally concludes and provides an outlook on future work. - \newcounter{secondauthorcnt} \newcounter{underreviewcnt} \newcounter{plannedcnt} @@ -240,6 +307,7 @@ Adrian Ramsingh created the micropython implementation (\acrshort{PWS}), the ori \newcommand{\underreview}{\textsuperscript{$\dagger$}\stepcounter{underreviewcnt}} \newcommand{\planned}{\textsuperscript{$\ddagger$}\stepcounter{plannedcnt}} +\subsection{List of publications} \begin{enumerate} \item \secondauthor{} A Task-Based DSL for Microcomputers @@ -293,9 +361,6 @@ Adrian Ramsingh created the micropython implementation (\acrshort{PWS}), the ori \item \planned{} Green Computing for the Internet of Things M. Lubbers, P. Koopman (Sustrainable 2022 planned). - \item \planned{} T.B.A. - - M. Lubbers, P. Koopman (Sustrainable 2023 planned). \setcounter{publicationscnt}{\value{enumi}} \end{enumerate} diff --git a/lstlangarduino.sty b/lstlangarduino.sty new file mode 100644 index 0000000..a802906 --- /dev/null +++ b/lstlangarduino.sty @@ -0,0 +1,7 @@ +\lstdefinelanguage[Arduino]{C++}[11]{C++}{% + morekeywords={HIGH,LOW,OUTPUT,INPUT,INPUT\_PULLUP,% + D0,D1,D2,D3,D4,D5,D6,D7,D7,D8,D9,D10,D11,D12,D13,A0,A1,A2,A3,A4,A5,A6,A7,% + pinMode,digitalWrite,digitalRead,delay,millis,% + }, + basewidth=.6em, +} diff --git a/lstlanghaskell.sty b/lstlanghaskell.sty index d8f1d6b..5a74664 100644 --- a/lstlanghaskell.sty +++ b/lstlanghaskell.sty @@ -5,9 +5,10 @@ Bool,Int,Integer,Float,Double,String,% Maybe,Nothing,Just,% zip,length,Show,show,Num,Eq,print,% - id}, + error,id}, morekeywords={forall}, literate=% + {forall}{{$\forall$}}1 {\_}{{\raisebox{.15ex}{\_}}}1 {~}{{\raisebox{-.6ex}{\textasciitilde}}}1 {\\}{{$\lambda\:$}}1 @@ -15,6 +16,5 @@ {<-}{{$\shortleftarrow$}}2 {=>}{{$\Rightarrow$}}2 {<=}{{$\Leftarrow$}}2 - {'}{{`}}1 {...}{{$\cdots$}}1 %chktex 11 } diff --git a/lstlanghaskelllhstex.sty b/lstlanghaskelllhstex.sty index 0a51849..0239d37 100644 --- a/lstlanghaskelllhstex.sty +++ b/lstlanghaskelllhstex.sty @@ -5,9 +5,10 @@ Bool,Int,Integer,Float,Double,String,% Maybe,Nothing,Just,% zip,length,Show,show,Num,Eq,print,% - id}, + error,id}, morekeywords={forall}, literate=% + {forall}{{$\forall$}}1 {\_}{{\raisebox{.15ex}{\_}}}1 {~}{{\raisebox{-.6ex}{\textasciitilde}}}1 {\\}{{$\lambda\:$}}1 @@ -15,16 +16,6 @@ {<-}{{$\shortleftarrow$}}2 {=>}{{$\Rightarrow$}}2 {<=}{{$\Leftarrow$}}2 - {'}{{`}}1 - {...}{{$\cdots$}}1 %chktex 11 - {\_}{{\raisebox{.15ex}{\_}}}1 - {~}{{\raisebox{-.6ex}{\textasciitilde}}}1 - {\\}{{$\lambda\:$}}1 - {->}{{$\shortrightarrow$}}2 - {<-}{{$\shortleftarrow$}}2 - {=>}{{$\Rightarrow$}}2 - {<=}{{$\Leftarrow$}}2 - {'}{{`}}1 {...}{{$\cdots$}}1 %chktex 11 {e1}{{e\textsubscript{1}}}2 {e2}{{e\textsubscript{2}}}2 diff --git a/task_oriented_programming/beyond_microprocessors.tex b/mtask/beyond_microprocessors.tex similarity index 100% rename from task_oriented_programming/beyond_microprocessors.tex rename to mtask/beyond_microprocessors.tex diff --git a/task_oriented_programming/integration.tex b/mtask/integration.tex similarity index 100% rename from task_oriented_programming/integration.tex rename to mtask/integration.tex diff --git a/task_oriented_programming/interpreting.tex b/mtask/interpreting.tex similarity index 100% rename from task_oriented_programming/interpreting.tex rename to mtask/interpreting.tex diff --git a/mtask/mtask.tex b/mtask/mtask.tex new file mode 100644 index 0000000..7e54b3f --- /dev/null +++ b/mtask/mtask.tex @@ -0,0 +1,192 @@ +\documentclass[../thesis.tex]{subfiles} + +\begin{document} +\ifSubfilesClassLoaded{ + \pagenumbering{arabic} +}{} + +\chapter{\Gls{TOP} for the \gls{IOT}} +\begin{chapterabstract} + This chapter introduces \gls{MTASK} and puts it into perspective compared to traditional microprocessor programming. +\end{chapterabstract} +Traditionally, the first program that one writes when trying a new language is the so called \emph{Hello World!} program. +This program has the single task of printing the text \emph{Hello World!} to the screen and exiting again, useful to become familiarised with the syntax and verify that the toolchain and runtime environment is working. +On microprocessors, there often is no screen for displaying text. +Nevertheless, almost always there is a monochrome $1\times1$ pixel screen, namely an---often builtin---\gls{LED}. +The \emph{Hello World!} equivalent on microprocessors blinks this \gls{LED}. + +\Cref{lst:arduinoBlink} shows how the logic of a blink program might look when using \gls{ARDUINO}'s \gls{CPP} dialect. +Every \gls{ARDUINO} program contains a \arduinoinline{setup} and a \arduinoinline{loop} function. +The \arduinoinline{setup} function is executed only once on boot, the \arduinoinline{loop} function is continuously called afterwards and contains the event loop. +After setting the \gls{GPIO} pin to the correct mode, blink's \arduinoinline{loop} function alternates the state of the pin representing the \gls{LED} between \arduinoinline{HIGH} and \arduinoinline{LOW}, turning the \gls{LED} off and on respectively. +In between it waits for 500 milliseconds so that the blinking is actually visible for the human eye. +Compiling this results in a binary firmware that needs to be flashed onto the program memory. + +Translating the traditional blink program to \gls{MTASK} can almost be done by simply substituting some syntax as seen in \cref{lst:blinkImp}. +E.g.\ \cleaninline{digitalWrite} becomes \cleaninline{writeD}, literals are prefixed with \cleaninline{lit} and the pin to blink is changed to represent the actual pin for the builtin \gls{LED} of the device used in the exercises. +In contrast to the imperative \gls{CPP} dialect, \gls{MTASK} is a \gls{TOP} language and therefore there is no such thing as a loop, only task combinators to combine tasks. +To simulate a loop, the \cleaninline{rpeat} task can be used, this task executes the argument task and, when stable, reinstates it. +The body of the \cleaninline{rpeat} contains similarly named tasks to write to the pins and to wait in between. +The tasks are connected using the sequential \cleaninline{>>|.} combinator that for all current intents and purposes executes the tasks after each other. + +\begin{figure}[!ht] + \begin{subfigure}[b]{.5\linewidth} + \begin{lstArduino}[caption={Blink program.},label={lst:arduinoBlink}] +void setup() { + pinMode(D2, OUTPUT); +} + +void loop() { + digitalWrite(D2, HIGH); + delay(500); + digitalWrite(D2, LOW); + delay(500); +}\end{lstArduino} + \end{subfigure}% + \begin{subfigure}[b]{.5\linewidth} + \begin{lstClean}[caption={Blink program.},label={lst:blinkImp}] + +blink :: Main (MTask v ()) | mtask v +blink = + declarePin D4 PMOutput \d4-> + {main = rpeat ( + writeD d4 true + >>|. delay (lit 500) + >>|. writeD d4 false + >>|. delay (lit 500) + )}\end{lstClean} + \end{subfigure} +\end{figure} + +\chapter{The \gls{MTASK} \gls{DSL}} +\begin{chapterabstract} +This chapter serves as a complete guide to the \gls{MTASK} language, from an \gls{MTASK} programmer's perspective. +\end{chapterabstract} + +The \gls{MTASK} system is a \gls{TOP} programming environment for programming microprocessors. +It is implemented as an \gls{EDSL} in \gls{CLEAN} using class-based---or tagless-final---embedding (See~\cref{ssec:tagless}). +Due to the nature of the embedding technique, it is possible to have multiple interpretations of---or views on---programs written in the \gls{MTASK} language. + +\begin{itemize} + \item Pretty printer + + This interpretation converts the expression to a string representation. + \item Simulator + + The simulator converts the expression to a ready-for-work \gls{ITASK} simulation in which the user can inspect and control the simulated peripherals and see the internal state of the tasks. + \item Compiler + + The compiler compiles the \gls{MTASK} program at runtime to a specialised bytecode. + Using a handful of integration functions and tasks, \gls{MTASK} tasks can be executed on microprocessors and integrated in \gls{ITASK} as if they were regular \gls{ITASK} tasks. + Furthermore, with special language constructs, \glspl{SDS} can be shared between \gls{MTASK} and \gls{ITASK} programs. +\end{itemize} + +\section{Types} +To leverage the type checker of the host language, types in the \gls{MTASK} language are expressed as types in the host language, to make the language type safe. +However, not all types in the host language are suitable for microprocessors that may only have 2KiB of \gls{RAM} so class constraints are therefore added to the \gls{DSL} functions. +The most used class constraint is the \cleaninline{type} class collection containing functions for serialization, printing, \gls{ITASK} constraints etc. +Many of these functions can be derived using generic programming. +An even stronger restriction on types is defined for types that have a stack representation. +This \cleaninline{basicType} class has instances for many \gls{CLEAN} basic types such as \cleaninline{Int}, \cleaninline{Real} and \cleaninline{Bool}. +The class constraints for values in \gls{MTASK} are omnipresent in all functions and therefore often omitted throughout throughout the chapters for brevity and clarity. + +\begin{table}[ht] + \centering + \begin{tabular}{lll} + \toprule + \gls{CLEAN}/\gls{MTASK} & \gls{CPP} type & \textnumero{}bits\\ + \midrule + \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{:: T = A | B | C} & \cinline{enum} & 16\\ + \bottomrule + \end{tabular} + \caption{Mapping from \gls{CLEAN}/\gls{MTASK} data types to \gls{CPP} datatypes.}% + \label{tbl:mtask-c-datatypes} +\end{table} + +The \gls{MTASK} language 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 integration with \gls{ITASK}. + +\Cref{lst:constraints} contains the definitions for the type constraints and shows some example type signatures for typical \gls{MTASK} expressions and tasks. + +\begin{lstClean}[caption={Classes and class collections for the \gls{MTASK} language.},label={lst:constraints}] +class type t | iTask, ... ,fromByteCode, toByteCode t +class basicType t | type t where ... + +class mtask v | expr, ..., int, real, long v + +someExpr :: v Int | mtask v +tempTask :: MTask v Bool | mtask, dht v +\end{lstClean} + +\section{Expressions} +\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}), to do basic arithmetics and conditional execution. +For every common arithmetic operator in the host language, an \gls{MTASK} variant is present, suffixed by a period to not clash with \gls{CLEAN}'s builtin operators. + +\begin{lstClean}[caption={The \gls{MTASK} class for expressions},label={lst:expressions}] +class expr v where + lit :: t -> v t | type t + (+.) infixl 6 :: (v t) (v t) -> v t | basicType, +, zero t + (-.) infixl 6 :: (v t) (v t) -> v t | basicType, -, zero t + (*.) infixl 7 :: (v t) (v t) -> v t | basicType, *, zero, one t + (/.) infixl 7 :: (v t) (v t) -> v t | basicType, /, zero t + (&.) infixr 3 :: (v Bool) (v Bool) -> v Bool + (|.) infixr 2 :: (v Bool) (v Bool) -> v Bool + Not :: (v Bool) -> v Bool + (==.) infix 4 :: (v a) (v a) -> v Bool | Eq, basicType a + (!=.) infix 4 :: (v a) (v a) -> v Bool | Eq, basicType a + (<.) infix 4 :: (v a) (v a) -> v Bool | Ord, basicType a + (>.) infix 4 :: (v a) (v a) -> v Bool | Ord, basicType a + (<=.) infix 4 :: (v a) (v a) -> v Bool | Ord, basicType a + (>=.) infix 4 :: (v a) (v a) -> v Bool | Ord, basicType a + If :: (v Bool) (v t) (v t) -> v t | type t +\end{lstClean} + +Conversion to-and-fro data types is available through the overloaded functions \cleaninline{int}, \cleaninline{long} and \cleaninline{real}. + +\begin{lstClean} +class int v a :: (v a) -> v Int +class real v a :: (v a) -> v Real +class long v a :: (v a) -> v Long +\end{lstClean} + +Finally, values from the host language must be explicitly lifted to the \gls{MTASK} language using the \cleaninline{lit} function. +For convenience, there are many lower-cased macro definitions for often used constants as can be seen in \cref{lst:convenience_lits} + +\begin{lstClean}[label={lst:convenience_lits}] +// Booleans +true :== lit True +false :== lit False +\end{lstClean} + +\subsection{Functions} + +\section{Tasks} +\subsection{Basic tasks} +\subsubsection{Peripherals} +\subsection{Task combinators} +\subsubsection{Parallel} +\subsubsection{Sequential} +\subsubsection{Miscellaneous} +\subsection{\glspl{SDS}} + +\chapter{Green computing with \gls{MTASK}} + +\chapter{Integration with \gls{ITASK}} +\section{Devices} +\section{Lift tasks} +\section{Lift \glspl{SDS}} + +\chapter{Implementation} +IFL19 paper, bytecode instructieset~\cref{chp:bytecode_instruction_set} + +\section{Integration with \gls{ITASK}} +IFL18 paper stukken + +\input{subfilepostamble} +\end{document} diff --git a/task_oriented_programming/mtask_by_example.tex b/mtask/mtask_by_example.tex similarity index 100% rename from task_oriented_programming/mtask_by_example.tex rename to mtask/mtask_by_example.tex diff --git a/other.bib b/other.bib index 7ef32eb..4668fcb 100644 --- a/other.bib +++ b/other.bib @@ -1,4 +1,15 @@ +@mastersthesis{crooijmans_reducing_2021, + address = {Nijmegen}, + title = {Reducing the {Power} {Consumption} of {IoT} {Devices} in {Task}-{Oriented} {Programming}}, + language = {en}, + school = {Radboud University}, + author = {Crooijmans, Sjoerd}, + month = jul, + year = {2021}, + file = {Crooijmans - 2021 - Reducing the Power Consumption of IoT Devices in T.pdf:/home/mrl/.local/share/zotero/storage/98LY9YHH/Crooijmans - 2021 - Reducing the Power Consumption of IoT Devices in T.pdf:application/pdf}, +} + @inproceedings{plasmeijer_task-oriented_2012, address = {New York, NY, USA}, series = {{PPDP} '12}, @@ -202,7 +213,7 @@ author = {Löh, Andres and Hinze, Ralf}, year = {2006}, note = {event-place: Venice, Italy}, - keywords = {expression problem, extensible data types, extensible exceptions, extensible functions, functional programming, generic programming, Haskell, mutually recursive modules}, + keywords = {functional programming, Haskell, expression problem, extensible data types, extensible exceptions, extensible functions, generic programming, mutually recursive modules}, pages = {133--144}, file = {OpenDatatypes.pdf:/home/mrl/.local/share/zotero/storage/NEP9GZ9N/OpenDatatypes.pdf:application/pdf}, } @@ -384,6 +395,53 @@ Publisher: Association for Computing Machinery}, file = {Stutterheim et al. - 2018 - Maintaining Separation of Concerns Through Task Or.pdf:/home/mrl/.local/share/zotero/storage/4GXJEM2U/Stutterheim et al. - 2018 - Maintaining Separation of Concerns Through Task Or.pdf:application/pdf}, } +@mastersthesis{bohm_asynchronous_2019, + address = {Nijmegen}, + title = {Asynchronous {Actions} in a {Synchronous} {World}}, + abstract = {This thesis introduces a system for asynchronous communication in the iTasks framework. The +framework is written in Clean, a pure, lazy, functional language. Tasks need to be able to access +data in the system and retrieve data from all kinds of data sources. The share system allows +tasks to read arbitrary data sources and provides a simple interface that allows composition of +different data sources. This system allows tasks to share and store data in an efficient, re-usable +way. +A disadvantage of the share system is that it does not allow asynchronous evaluation. When +one task is using a share, other tasks have to wait for the full evaluation of this share before they +can be evaluated. This has the effect that users in the iTasks framework must wait on other +users. This results in poor user experience. +We implement a share system which, by way of share rewriting, allows asynchronous evalua- +tion. The system can be used to communicate with arbitrary services on the internet, as well as +to communicate between different iTasks servers in a distributed context. +We show how asynchronous shares are implemented and what the limitations are. We also +show multiple practical examples of using asynchronous shares. The new system can be effectively +used to consume services on the internet. It fits nicely into existing iTasks programs and requires +few changes in existing programs.}, + language = {en}, + school = {Radboud University}, + author = {Böhm, Haye}, + month = jan, + year = {2019}, + file = {Bohm - Asynchronous Actions in a Synchronous World.pdf:/home/mrl/.local/share/zotero/storage/D3IYPAM5/Bohm - Asynchronous Actions in a Synchronous World.pdf:application/pdf}, +} + +@inproceedings{hentschel_supersensors:_2016, + address = {Vienna, Austria}, + title = {Supersensors: {Raspberry} {Pi} {Devices} for {Smart} {Campus} {Infrastructure}}, + isbn = {978-1-5090-4052-0}, + shorttitle = {Supersensors}, + url = {http://ieeexplore.ieee.org/document/7575844/}, + doi = {10.1109/FiCloud.2016.16}, + abstract = {We describe an approach for developing a campuswide sensor network using commodity single board computers. We sketch various use cases for environmental sensor data, for different university stakeholders. Our key premise is that supersensors—sensors with significant compute capability—enable more flexible data collection, processing and reaction. In this paper, we describe the initial prototype deployment of our supersensor system in a single department at the University of Glasgow.}, + language = {en}, + urldate = {2019-09-04}, + booktitle = {2016 {IEEE} 4th {International} {Conference} on {Future} {Internet} of {Things} and {Cloud} ({FiCloud})}, + publisher = {IEEE}, + author = {Hentschel, Kristian and Jacob, Dejice and Singer, Jeremy and Chalmers, Matthew}, + month = aug, + year = {2016}, + pages = {58--62}, + file = {Hentschel et al. - 2016 - Supersensors Raspberry Pi Devices for Smart Campu.pdf:/home/mrl/.local/share/zotero/storage/ATK53FN2/Hentschel et al. - 2016 - Supersensors Raspberry Pi Devices for Smart Campu.pdf:application/pdf}, +} + @misc{achten_clean_2007, title = {Clean for {Haskell98} {Programmers}}, url = {https://www.mbsd.cs.ru.nl/publications/papers/2007/achp2007-CleanHaskellQuickGuide.pdf}, @@ -412,6 +470,17 @@ Publisher: Association for Computing Machinery}, file = {Baccelli et al. - Scripting Over-The-Air Towards Containers on Low-.pdf:/home/mrl/.local/share/zotero/storage/98UTMFAC/Baccelli et al. - Scripting Over-The-Air Towards Containers on Low-.pdf:application/pdf}, } +@mastersthesis{amazonas_cabral_de_andrade_developing_2018, + address = {Nijmegen}, + title = {Developing {Real} {Life}, {Task} {Oriented} {Applications} for the {Internet} of {Things}}, + shorttitle = {Developing {Real} {Life}, {TOP} {Applications} for the {IOT}}, + language = {en}, + school = {Radboud University}, + author = {Amazonas Cabral De Andrade, Matheus}, + year = {2018}, + file = {Lubbers - prof. dr. dr.h.c. ir. M.J. Plasmeijer.pdf:/home/mrl/.local/share/zotero/storage/JXPEWS85/Lubbers - prof. dr. dr.h.c. ir. M.J. Plasmeijer.pdf:application/pdf}, +} + @article{swierstra_data_2008, title = {Data types à la carte}, volume = {18}, @@ -579,7 +648,7 @@ Publisher: Association for Computing Machinery}, author = {Gibbons, Jeremy and Wu, Nicolas}, year = {2014}, note = {event-place: Gothenburg, Sweden}, - keywords = {deep and shallow embedding, domain-specific languages, folds}, + keywords = {domain-specific languages, deep and shallow embedding, folds}, pages = {339--347}, file = {Gibbons and Wu - 2014 - Folding Domain-Specific Languages Deep and Shallo.pdf:/home/mrl/.local/share/zotero/storage/6WNWSLFJ/Gibbons and Wu - 2014 - Folding Domain-Specific Languages Deep and Shallo.pdf:application/pdf}, } @@ -809,32 +878,74 @@ Publisher: Association for Computing Machinery}, @misc{wikipedia_contributors_rhapsody_2022, title = {Rhapsody (music) — {Wikipedia}, {The} {Free} {Encyclopedia}}, - url = {https://en.wikipedia.org/w/index.php?title=Rhapsody_(music)\&oldid=1068385257}, + url = {https://en.wikipedia.org/w/index.php?title=Rhapsody_(music)&oldid=1068385257}, urldate = {2022-09-06}, journal = {Wikipedia}, author = {{Wikipedia contributors}}, year = {2022}, note = {accessed on: 2022-09-06}, } +@article{barendsen_uniqueness_1996, + title = {Uniqueness typing for functional languages with graph rewriting semantics}, + volume = {6}, + number = {6}, + journal = {Mathematical structures in computer science}, + author = {Barendsen, Erik and Smetsers, Sjaak}, + year = {1996}, + pages = {579--612}, + file = {Barendsen and Smetsers - 1996 - Uniqueness typing for functional languages with gr.pdf:/home/mrl/.local/share/zotero/storage/BPRC6KJK/Barendsen and Smetsers - 1996 - Uniqueness typing for functional languages with gr.pdf:application/pdf}, +} -@mastersthesis{crooijmans_reducing_2021, - address = {Nijmegen}, - title = {Reducing the {Power} {Consumption} of {IoT} {Devices} in {Task}-{Oriented} {Programming}}, - language = {en}, - school = {Radboud University}, - author = {Crooijmans, Sjoerd}, - month = jul, - year = {2021}, - file = {Crooijmans - 2021 - Reducing the Power Consumption of IoT Devices in T.pdf:/home/mrl/.local/share/zotero/storage/98LY9YHH/Crooijmans - 2021 - Reducing the Power Consumption of IoT Devices in T.pdf:application/pdf}, +@incollection{backus_introduction_1990, + address = {USA}, + title = {An {Introduction} to the {Programming} {Language} {FL}}, + isbn = {0-201-17236-4}, + booktitle = {Research {Topics} in {Functional} {Programming}}, + publisher = {Addison-Wesley Longman Publishing Co., Inc.}, + author = {Backus, John and Williams, John H. and Wimmers, Edward L.}, + year = {1990}, + pages = {219--247}, } -@mastersthesis{amazonas_cabral_de_andrade_developing_2018, - address = {Nijmegen}, - title = {Developing {Real} {Life}, {Task} {Oriented} {Applications} for the {Internet} of {Things}}, - shorttitle = {Developing {Real} {Life}, {TOP} {Applications} for the {IOT}}, - language = {en}, - school = {Radboud University}, - author = {Amazonas Cabral De Andrade, Matheus}, - year = {2018}, - file = {Lubbers - prof. dr. dr.h.c. ir. M.J. Plasmeijer.pdf:/home/mrl/.local/share/zotero/storage/JXPEWS85/Lubbers - prof. dr. dr.h.c. ir. M.J. Plasmeijer.pdf:application/pdf}, +@article{achten_ins_1995, + title = {The ins and outs of {Clean} {I}/{O}}, + volume = {5}, + doi = {10.1017/S0956796800001258}, + number = {1}, + journal = {Journal of Functional Programming}, + author = {Achten, Peter and Plasmeijer, Rinus}, + year = {1995}, + note = {Publisher: Cambridge University Press}, + pages = {81--110}, +} + +@inproceedings{peyton_jones_imperative_1993, + address = {New York, NY, USA}, + series = {{POPL} '93}, + title = {Imperative {Functional} {Programming}}, + isbn = {0-89791-560-7}, + url = {https://doi.org/10.1145/158511.158524}, + doi = {10.1145/158511.158524}, + abstract = {We present a new model, based on monads, for performing input/output in a non-strict, purely functional language. It is composable, extensible, efficient, requires no extensions to the type system, and extends smoothly to incorporate mixed-language working and in-place array updates.}, + booktitle = {Proceedings of the 20th {ACM} {SIGPLAN}-{SIGACT} {Symposium} on {Principles} of {Programming} {Languages}}, + publisher = {Association for Computing Machinery}, + author = {Peyton Jones, Simon L. and Wadler, Philip}, + year = {1993}, + note = {event-place: Charleston, South Carolina, USA}, + pages = {71--84}, + file = {Peyton Jones and Wadler - 1993 - Imperative Functional Programming.pdf:/home/mrl/.local/share/zotero/storage/9DQ5V3N3/Peyton Jones and Wadler - 1993 - Imperative Functional Programming.pdf:application/pdf}, +} + +@inproceedings{achten_high_1993, + address = {London}, + title = {High {Level} {Specification} of {I}/{O} in {Functional} {Languages}}, + isbn = {978-1-4471-3215-8}, + abstract = {The interface with the outside world has always been one of the weakest points of functional languages. It is not easy to incorporate I/O without being allowed to do side-effects. Furthermore, functional languages allow redexes to be evaluated in any order while I/O generally has to be performed in a very specific order. In this paper we present a new solution for the I/O problem which we have incorporated in the language Concurrent Clean. Concurrent Clean offers a linear type system called Unique Types. It makes it possible to define functions with side-effects without violating the functional semantics. Now it is possible to change any object in the world in the way we wanted: e.g. arrays can be updated in-situ, arbitrary file manipulation is possible. We have used this powerful tool among others to create a library for window based I/O. Using an explicit environment passing scheme provides a high-level and elegant functional specification method for I/O, called Event I/O. Now the specification of I/O has become one of the strengths of functional languages: interactive programs written in Concurrent Clean are concise, easy to write and comprehend as well as efficient. The presented solution can in principle be applied for any other functional language as well provided that it actually uses graph rewriting semantics in the implementation.}, + booktitle = {Functional {Programming}, {Glasgow} 1992}, + publisher = {Springer London}, + author = {Achten, Peter and van Groningen, John and Plasmeijer, Rinus}, + editor = {Launchbury, John and Sansom, Patrick}, + year = {1993}, + pages = {1--17}, + file = {Achten et al. - 1993 - High Level Specification of IO in Functional Lang.pdf:/home/mrl/.local/share/zotero/storage/4QVH7AYC/Achten et al. - 1993 - High Level Specification of IO in Functional Lang.pdf:application/pdf}, } diff --git a/preamble.tex b/preamble.tex index 9f36877..6c3ec94 100644 --- a/preamble.tex +++ b/preamble.tex @@ -1,7 +1,22 @@ -% Input encoding -\usepackage[utf8]{inputenc} +% Fonts +\usepackage[utf8]{inputenc} % Input encoding +\usepackage[T1]{fontenc} % Font encoding +\usepackage{lmodern} % Nicer font +\usepackage{microtype} % Better kerning +\usepackage{tipa} % IPA symbols +\usepackage{stmaryrd} % short arrows +\usepackage{textcomp} % upquote +\usepackage{titlecaps} % titlecase commands +\usepackage{amsmath} % extra math +\usepackage{amssymb} % extra math symbols +\everymath{\it\/} +\DeclareMathSymbol{\shortminus}{\mathbin}{AMSa}{"39} %chktex 18 -% Papersize +% Internationalisation +\usepackage[dutch,russian,british]{babel} +%\babelfont[russian]{rm}{Liberation Serif} + +% Papersize and layout \usepackage{geometry} \geometry{ inner=25mm, @@ -13,87 +28,89 @@ paperwidth=17cm, paperheight=24cm, } +\usepackage[ + height={1.5cm}, + width={12mm}, + distance={1.55cm}, + topthumbmargin={auto}, + bottomthumbmargin={auto}, + eventxtindent={.5cm}, + oddtxtexdent={.3cm}]{thumbs} % thumb marks +\usepackage{fancyhdr} % Custom headers and footers +%\pagestyle{fancy} +\pagestyle{headings} +\usepackage{etoolbox} % To patch the chapter command +% Have better page numbering in chapters +\patchcmd{\chapter}{plain}{headings}{}{} +\usepackage{epigraph} % Epigraph +\renewcommand\partname{Movement} % Rename parts to movements (rhapsody uhu) +\newenvironment{chapterabstract} + {\begin{quote}} + {\end{quote}} -% Font encoding -\usepackage[T1,T2A]{fontenc} - -% standalone figures -\usepackage[subpreambles=true]{standalone} - -% Less bad boxes -\usepackage{microtype} - -% No more room for a new \write -\usepackage{morewrites} - -% Internationalisation -\usepackage[dutch,russian,british]{babel} -%\babelfont[russian]{rm}{Liberation Serif} +% Increase the depth for the table of contents +\setcounter{secnumdepth}{3} +\renewcommand{\contentsname}{Table of Contents} % change the name of the TOC +\AtBeginDocument{\addtocontents{toc}{\protect\thispagestyle{empty}}} % to remove page numbering from the TOC -% Appendices (used for subappendices, appendices per chapter) -\usepackage{appendix} +% (file) structure +\usepackage[subpreambles=true]{standalone} % standalone figures +\usepackage{morewrites} % fix no more room for a new \write +\usepackage{appendix} % subappendices, appendices per chapter -% Cite bib entry completely -\usepackage{bibentry} +% Bibliography +\usepackage{bibentry} % Cite bib entry completely \nobibliography* +\bibliographystyle{alpha} -% Hyperlinks -\usepackage{bookmark,hyperref} -%\usepackage[pagebackref]{bookmark,hyperref} -% Setup pdf parameters: TODO +% Hyperlinks and metadata +\usepackage[pagebackref]{hyperref} % hyperlinks +\renewcommand*{\backref}[1]{} +\renewcommand*{\backrefalt}[4]{[{% + \ifcase #1 not cited.\or p.~#2.\else pp. #2.\fi%chktex 1 +}]} \hypersetup{% pdftitle={\mytitle}, pdfauthor={\myauthor}, - pdfsubject={}, -% pdfcreator={}, -% pdfproducer={}, pdfkeywords={task-oriented programming, functional programming, domain specific languages, internet of things}, hidelinks, } +\usepackage[nodayofweek]{datetime} % Use a fixed document date \urlstyle{same} -\usepackage{xmpincl} -\includexmp{CC_Attribution-NoDerivatives_4.0_International} +\usepackage{bookmark} +\usepackage{cleveref} % Easy references +\crefname{part}{movement}{movements} +\crefname{lstlisting}{listing}{listing} % Graphics -\usepackage{graphicx} -% Images directory -\graphicspath{{img/}} -%subfigures -\usepackage{caption} +\usepackage{graphicx} % Images +\graphicspath{{img/},{introduction/img}} +\usepackage{caption} % subfigures \usepackage{subcaption} - -% Nice tables -\usepackage{booktabs} -% Multirow cells -\usepackage{multirow} - -% orcid icon -\usepackage{academicons} \newcommand{\orcid}[1]{\href{https://orcid.org/#1}{\hspace{1mm}\includegraphics[width=1em]{orcid}\hspace{2mm} https://orcid.org/#1}} -% IPA symbols -\usepackage{tipa} - -% Automatically wrapping tables -\usepackage{tabularx} - -% Use a fixed document date -\usepackage[nodayofweek]{datetime} +% Tables +\usepackage{booktabs} % Nicer tables +\usepackage{multirow} % Multirow cells +\usepackage{tabularx} % Automatically wrapping tables +\usepackage{longtable} % Tables spanning pages % Code -\usepackage{stmaryrd} % Short arrow -\usepackage{textcomp} % upquote +% Pseudocode +\usepackage[algochapter]{algorithm2e} +% Fix the algorithm font +\renewcommand\AlCapFnt{\normalfont} \usepackage{listings} % General listings settings \lstset{% - basewidth=0.45em, + basewidth=0.5em, basicstyle=\tt\small, breakatwhitespace=false, breaklines=true, captionpos=b, columns=[c]fixed, commentstyle=\sl, - escapeinside={(+}{+)}, % chktex 9 +% escapeinside={(+}{+)}, % chktex 9 frame=L, keepspaces=true, keywordstyle=\bf, @@ -108,6 +125,9 @@ \usepackage{lstlangclean} \usepackage{lstlanghaskell} \usepackage{lstlanghaskelllhstex} +\usepackage{lstlangarduino} +\newcommand{\cinline}[1]{\lstinline[language=c,postbreak=]|#1|} +\newcommand{\arduinoinline}[1]{\lstinline[language={[Arduino]C++},postbreak=]|#1|} \newcommand{\cleaninline}[1]{\lstinline[language=Clean,postbreak=]|#1|} \newcommand{\haskellinline}[1]{\lstinline[language=Haskell,style=haskell,postbreak=]|#1|} \newcommand{\haskelllhstexinline}[1]{\lstinline[language=Haskell,style=haskelllhstex,postbreak=]|#1|} @@ -124,24 +144,34 @@ \lstnewenvironment{lstClean}[1][] {% \lstset{language=Clean, #1} - \renewcommand*{\lstlistingname}{Listing (Clean)} + \renewcommand*{\lstlistingname}{Listing (\gls{CLEAN})} + } + {} +\lstnewenvironment{lstArduino}[1][] + {% + \lstset{language={[Arduino]C++}, #1} + \renewcommand*{\lstlistingname}{Listing (\gls{ARDUINO})} } {} \lstnewenvironment{lstHaskell}[1][] {% \lstset{language=Haskell,style=haskell,#1}% - \renewcommand*{\lstlistingname}{Listing (Haskell)} + \renewcommand*{\lstlistingname}{Listing (\gls{HASKELL})} } {} \lstnewenvironment{lstHaskellLhstex}[1][] {% \lstset{language=Haskell,style=haskelllhstex,#1}% - \renewcommand*{\lstlistingname}{Listing (Haskell)} + \renewcommand*{\lstlistingname}{Listing (\gls{HASKELL})} } {} % Glossaries and acronyms \usepackage[acronym,nonumberlist]{glossaries} +\Addlcwords{of} +% Titlecase glossary commands +\newcommand{\glst}[1]{\titlecap{\glsentrylong{#1}}} +\newcommand{\Glst}[1]{\glst{#1}} % Fix gls in hyperlink errors \pdfstringdefDisableCommands{% \def\acrlong#1{}% @@ -165,66 +195,26 @@ \def\titlecap#1{}% } -% Titlecase commands -\usepackage{titlecaps} -\Addlcwords{of} -% Titlecase glossary command -\newcommand{\glst}[1]{\titlecap{\glsentrylong{#1}}} -\newcommand{\Glst}[1]{\glst{#1}} - -% Pseudocode -\usepackage[algochapter]{algorithm2e} -% Fix the algorithm font -\renewcommand\AlCapFnt{\normalfont} - % Index \usepackage{makeidx} -% Enable the index -\makeindex% +\makeindex% Enable the index % Custom enumerations \usepackage[inline,shortlabels]{enumitem} \setlist{noitemsep} \setlist[description]{leftmargin=\parindent} -% Epigraph -\usepackage{epigraph} - -% Thumb marks on the page -\usepackage[ - height={1.5cm}, - width={12mm}, - distance={1.55cm}, - topthumbmargin={auto}, - bottomthumbmargin={auto}, - eventxtindent={.5cm}, - oddtxtexdent={.3cm}]{thumbs} - -% Custom headers and footers -\usepackage{fancyhdr} -%\pagestyle{fancy} -\pagestyle{headings} - -% Tables spanning pages -\usepackage{longtable} - -% Easy references -\usepackage{cleveref} - -% To patch the chapter command -\usepackage{etoolbox} -% Have better page numbering in chapters -\patchcmd{\chapter}{plain}{headings}{}{} - -% Increase the depth for the table of contents -\setcounter{secnumdepth}{3} -\renewcommand{\contentsname}{Table of Contents} % change the name of the TOC -\AtBeginDocument{\addtocontents{toc}{\protect\thispagestyle{empty}}} % to remove page numbering from the TOC - % Initialize the glossaries \makeglossaries% \input{glossaries} +\usepackage{subfiles} + +\ifSubfilesClassLoaded{}{ + \usepackage{xmpincl} + \includexmp{CC_Attribution-NoDerivatives_4.0_International} +} + % Custom commands \newcommand{\GHCmod}[1]{\texttt{#1}} \newcommand{\requiresGHCmod}[1]{\footnote{Requires \GHCmod{#1} to be enabled.}} @@ -233,7 +223,3 @@ \newcommand{\mlubbers}{Lubbers, M.\ (Radboud University)} \newcommand{\pkoopman}{Koopman, dr.\ P.\ (Radboud University)} \newcommand{\rplasmeijer}{Plasmeijer, prof.\ dr.\ ir.\ R.\ (Radboud University)} - -\bibliographystyle{alpha} - -\usepackage{subfiles} diff --git a/subfilepostamble.tex b/subfilepostamble.tex index a39661c..e44f9e6 100644 --- a/subfilepostamble.tex +++ b/subfilepostamble.tex @@ -1,5 +1,5 @@ \ifSubfilesClassLoaded{% - \bibliography{../thesis} + \bibliography{../other,../self} }{ } diff --git a/task_oriented_programming/mtask.tex b/task_oriented_programming/mtask.tex deleted file mode 100644 index 9fc93af..0000000 --- a/task_oriented_programming/mtask.tex +++ /dev/null @@ -1,12 +0,0 @@ -\documentclass[../thesis.tex]{subfiles} - -\begin{document} -\ifSubfilesClassLoaded{ - \pagenumbering{arabic} -}{} - -\chapter{The mTask DSL} -RWDSL paper - -\input{subfilepostamble} -\end{document} diff --git a/thesis.tex b/thesis.tex index 0537c34..4949745 100644 --- a/thesis.tex +++ b/thesis.tex @@ -1,9 +1,9 @@ \documentclass[twoside,10pt]{book} -\def\mytitle{Task-Oriented Internet of Things Programming} +\def\mytitle{Orchestrating the Internet of Things with Task-Oriented Programming} \def\mysubtitle{a purely functional rhapsody} \def\myauthor{Mart Lubbers} -\def\mydate{\formatdate{1}{6}{2023}} +\def\mydate{\formatdate{31}{12}{2022}} \input{preamble} @@ -38,8 +38,9 @@ \subfile{frontmatter/motto} % Table of contents -\setcounter{tocdepth}{1} +%\setcounter{tocdepth}{1} \tableofcontents +\todo{reduce tocdepth to 1 before finishing} \newpage% % Dedication @@ -52,7 +53,6 @@ % The actual document \mainmatter% -\renewcommand\partname{Movement} % Rename parts to movements (rhapsody uhu) \addthumb{Chapters}{\arabic{chapter}}{white}{gray} % Arabic chapter thumbs \setcounter{chapter}{-1} @@ -60,7 +60,7 @@ \subfile{introduction/introduction} % DSL -\part{Domain-Specific Languages}% +\part[Prelude: Domain-Specific Languages]{Prelude\\Domain-Specific Languages}% \label{prt:dsl} % DSL Techniques @@ -72,33 +72,21 @@ % First-class data types \subfile{domain-specific_languages/first-class_datatypes} +% Stack computations? \subfile{domain-specific_languages/strongly-typed_multi-view_stack-based_computations} -\part{Task-Oriented Programming for the Internet of Things}% +\part[Exposition: Task-Oriented Internet of Things Programming]{Exposition\\Task-Oriented Internet of Things Programming}% \label{prt:top} -% mTask by example -\subfile{task_oriented_programming/mtask_by_example} +\subfile{mtask/mtask} -% Interpreting -\subfile{task_oriented_programming/interpreting} - -% Integration -\subfile{task_oriented_programming/integration} - -% Beyond microprocessors -\subfile{task_oriented_programming/beyond_microprocessors} - -\part{Tiered vs.\ tierless programming}% +\part[Transformation: Tiered vs.\ tierless programming]{Transformation\\Tiered vs.\ tierless programming}% \label{prt:tvt} \subfile{tiered_vs._tierless_programming/smart_campus} -\chapter{Modelling naval scenaries using \acrshort{TOP} and \acrshort{IOT}} -Waarschijnlijk geen tijd voor - -\bookmarksetup{startatroot}% this is it -\addtocontents{toc}{\bigskip}% perhaps as well +\bookmarksetup{startatroot} % descend back out of the previous part +\addtocontents{toc}{\bigskip}% Insert some whitespace to make the TOC better \subfile{conclusion/conclusion} % Start appendix @@ -107,9 +95,11 @@ Waarschijnlijk geen tijd voor \addcontentsline{toc}{part}{Appendix} \addthumb{Appendices}{\Alph{chapter}}{white}{gray} % Alpha appendix thumbs -\subfile{appendix/clean_for_haskell_programmers.tex} +\subfile{appendix/clean_for_haskell_programmers} +\subfile{appendix/bytecode} \backmatter% +\bookmarksetup{startatroot} % descend back out of the appendix \addtitlethumb{Backmatter}{}{white}{gray}{pagesLTS.0} % Empty backmatter thumbs % Bibliography