\myacronym{DSL}{DSL}{domain-specific language}
\myacronym{ECO2}{eCO\textsubscript{2}}{equivalent carbon dioxide}
\myacronym{EDSL}{eDSL}{embedded \glsxtrlong{DSL}}
-\myacronym[prefixfirst={a\ },prefix={an\ }]{FP}{FP}{functional programming}
+\myacronym[prefixfirst={a\ },prefix={an\ }]{FP}{functional programming}{functional programming}
\myacronym[prefixfirst={a\ },prefix={an\ }]{FRP}{FRP}{functional reactive programming}
\myacronym{GADT}{GADT}{generalised \glsxtrshort{ADT}}
\myacronym{GHC}{GHC}{Glasgow \gls{HASKELL} Compiler}
\begin{itemize}
\item introduces the topic and research ventures of this dissertation;
\item shows a reading guide;
- \item provides background material on \glsxtrlong{IOT}, \glsxtrlongpl{DSL}, \glsxtrlong{TOP}, and the \gls{TOP} languages \gls{ITASK} and \gls{MTASK} in particular;
+ \item provides background material on the \glsxtrlong{IOT}, \glsxtrlongpl{DSL}, \glsxtrlong{TOP}, \gls{ITASK}, and \gls{MTASK}.
\item and concludes with a detailed overview of the contributions.
\end{itemize}
\end{chapterabstract}
There are at least 13.4 billion devices connected to the internet at the time of writing.\footnote{\url{https://transformainsights.com/research/tam/market}, accessed on: \formatdate{13}{10}{2022}}
Each and every one of those devices senses, acts, or otherwise interacts with people, other computers, and the environment surrounding us.
-Even though there is a substantial variety among these devices, they have one thing in common: they all computers to some degree and for this reason require software to operate.
+Even though there is a substantial variety among these devices, they have one thing in common: they are all computers to some degree and hence require software to operate.
An increasing amount of these connected devices are so-called \emph{edge devices} that operate in the \gls{IOT}.
-Typically, these edge devices are powered by microcontrollers
-Microcontrollers contain integrated circuits accommodating a microprocessor designed for use in embedded applications.
-Typical microprocessors therefore are tiny in size; have little memory; contain a slow, but energy efficient processor; and allow for a lot of connectivity to connect peripherals such as sensors and actuators to interact with their surroundings.
+Typically, these edge devices are powered by microcontrollers.
+Said microcontrollers contain integrated circuits accommodating a microprocessor designed for use in embedded applications.
+Typical edge devices are therefore tiny in size; have little memory; contain a slow, but energy-efficient processor; and allow for a lot of connectivity to connect peripherals such as sensors and actuators to interact with their surroundings.
%
%\begin{figure}[ht]
% \centering
% \label{fig:esp_prototype}
%\end{figure}
-Edge devices come in numerous types, differing substantially from the other devices in the system.
An \gls{IOT} programmer has to program each device and their interoperation using different programming paradigms, programming languages, and abstraction levels resulting in semantic friction.
Programming and maintaining \gls{IOT} systems is therefore a very complex and an error-prone process.
-This thesis introduces research on taming these complex \gls{IOT} systems using \gls{TOP}.
+This thesis describes the research carried out around taming these complex \gls{IOT} systems using \gls{TOP}.
\Gls{TOP} is an innovative tierless programming paradigm for programming multi-tier interactive systems using a single declarative specification of the work that needs to be done.
-By utilising advanced compiler technologies, much of the internals, communication, and interoperation of the multi-tier applications is automatically generated.
+By utilising advanced compiler technologies, much of the internals, communication, and interoperation of the multi-tiered applications is automatically generated.
The result of this compilation is a ready-for-work application.
Unfortunately, because the abstraction level is so high, the hardware requirements are too excessive for a general purpose \gls{TOP} system to be suitable for the average edge device.
This is where \glspl{DSL} are brought into play.
\Glspl{DSL} are programming languages created with a specific domain in mind.
-Consequently, domain jargon does not have to be expressed in the language itself, but they can be built-in features.
-As a result, the hardware requirements can be drastically lower even with high levels of abstraction.
+Consequently, jargon does not have to be expressed in the language itself, but they can be built-in features.
+As a result, the hardware requirements can be drastically lower, even with high levels of abstraction.
Using \gls{MTASK}, a novel domain-specific \gls{TOP} \gls{DSL} fully integrated with \gls{ITASK}, all layers of the \gls{IOT} can be orchestrated from a single source.
+\todo[inline]{uitbreiden}
\section{Reading guide}
-The thesis is presented as a purely functional rhapsody.
+The thesis is structured as a purely functional rhapsody.
On Wikipedia, a musical rhapsody is defined as follows \citep{wikipedia_contributors_rhapsody_2022}:
\begin{quote}\emph{%
A \emph{rhapsody} in music is a one-movement work that is episodic yet integrated, free-flowing in structure, featuring a range of highly contrasted moods, colour, and tonality.}
\end{quote}
-The three episodes are barded by the introduction and conclusion (\cref{chp:introduction,chp:conclusion}).
-\Cref{prt:dsl} is a paper-based---otherwise known as cumulative---episode providing insight in advanced \gls{DSL} embedding techniques for \glspl{FP}.
+The three episodes in this thesis are barded by the introduction and conclusion (\cref{chp:introduction,chp:conclusion}).
+\Cref{prt:dsl} is a paper-based---otherwise known as cumulative---episode providing insights in advanced \gls{DSL} embedding techniques for \gls{FP} languages.
The chapters are readable independently.
\Cref{prt:top} is a monograph showing \gls{MTASK}, a \gls{TOP} \gls{DSL} for the \gls{IOT}.
Hence, the chapters are best read in order.
The following sections provide background material on the \gls{IOT}, \glspl{DSL}, and \gls{TOP} after which a detailed overview of the contributions is presented.
Text typeset as \texttt{teletype} represents source code.
-Standalone source code listings are used are marked by the programming language used.
+Standalone source code listings are marked by the programming language used.
Specifically for the \gls{FP} language \gls{CLEAN}, a guide tailored to \gls{HASKELL} programmers is available in \cref{chp:clean_for_haskell_programmers}.
\section{\texorpdfstring{\Glsxtrlong{IOT}}{Internet of things}}\label{sec:back_iot}
Today, \gls{IOT} is the term for a system of devices that sense the environment, act upon it and communicate with each other and the world.
These connected devices are already in households all around us in the form of smart electricity meters, fridges, phones, watches, home automation, \etc.
-When describing \gls{IOT} systems, a tiered---or layered---architecture is often used to compartmentalize the technology.
-The number of tiers heavily depends on the required complexity of the model but for the intents and purposes of this thesis, the four layer architecture as shown in \cref{fig:iot-layers} is used.
+When describing \gls{IOT} systems, a tiered---or layered---architecture is often used for compartmentalisation.
+The number of tiers heavily depends on the required complexity of the model but for the intents and purposes of this thesis, the layered architecture as shown in \cref{fig:iot-layers} is used.
\begin{figure}[ht]
\centering
\includestandalone{iot-layers}
- \caption{A four-tier \gls{IOT} architecture.}%
+ \caption{A layered \gls{IOT} architecture.}%
\label{fig:iot-layers}
\end{figure}
To explain the tiers, an example \gls{IOT} application---home automation---is dissected accordingly.
Closest to the end-user is the presentation layer, it provides the interface between the user and the \gls{IOT} system.
-In home automation this may be a web interface or an app used on a phone or mounted tablet to interact with the edge devices and view the sensor data.
+In home automation this may be a web interface or an app used on a phone or wall-mounted tablet to interact with the edge devices and view the sensor data.
-The application layer provides the \glspl{API}, data interfaces, and data storage of the \gls{IOT} system.
+The application layer provides the \glspl{API}, data interfaces, data processing, and data storage of the \gls{IOT} system.
A cloud server or local server provides this layer in a typical home automation application.
The perception layer---also called edge layer---collects the data and interacts with the environment.
It consists of edge devices such as microcontrollers equipped with various sensors and actuators.
-In home automation this layer consists of all the devices hosting the sensors and actuators such as a smart light bulb, an actuator to open a door or a temperature and humidity sensor.
+In home automation this layer consists of all the devices hosting the sensors and actuators such as smart light bulbs, actuators to open doors or a temperature and humidity sensors.
All layers are connected using the network layer.
-In many applications this is implemented using conventional networking techniques such as WiFi or Ethernet.
+In some applications this is implemented using conventional networking techniques such as WiFi or Ethernet.
However, networks or layers on top of it---tailored to the needs of the specific interconnection between layers---have been increasingly popular.
Examples of this are BLE, LoRa, ZigBee, LTE-M, or \gls{MQTT} for connecting the perception layer to the application layer and techniques such as HTTP, AJAX, and WebSocket for connecting the presentation layer to the application layer.
Across the layers, the devices are a large heterogeneous collection of different platforms, protocols, paradigms, and programming languages often resulting in impedance problems or semantic friction between layers when programming \citep{ireland_classification_2009}.
-Even more so, perception layer itself often is a heterogeneous collections of microcontrollers in itself as well, each having their own peculiarities, language of choice, and hardware interfaces.
-As the edge hardware needs to be cheap, small-scale, and energy efficient, the microcontrollers used to power these devices do not have a lot of computational power, only a soup\c{c}on of memory, and little communication bandwidth.
+Even more so, the perception layer itself often is a heterogeneous collections of microcontrollers in itself as well, each having their own peculiarities, language of choice, and hardware interfaces.
+Moreover, as the edge hardware needs to be cheap, small-scale, and energy efficient, the microcontrollers used to power these devices do not have a lot of computational power, only a soup\c{c}on of memory, and little communication bandwidth.
Typically the devices are unable to run a full-fledged general-purpose \gls{OS} but use compiled firmwares that are written in an imperative language.
While devices are getting a bit faster, smaller, and cheaper, they keep these properties to an extent, greatly reducing the flexibility for dynamic systems where tasks are created on the fly, executed on demand, or require parallel execution.
As program memory is mostly flash based and only lasts a couple of thousand writes before it wears out, it is not suitable for rapid reconfiguring and reprogramming.
>>! \result->Hint "You Entered:" @>> viewInformation [] result[+\label{lst:task_comb}+]
\end{lstClean}
+Functional languages are excellent hosts for \gls{TOP} language
+\Gls{ITASK} is embedded in a functional language
+
\subsection{\texorpdfstring{\Gls{MTASK}}{MTask}}
This thesis uses \gls{ITASK} in conjunction with \gls{MTASK}, an innovative \gls{TOP} language designed for defining interactive systems for \gls{IOT} edge devices \citep{koopman_task-based_2018}.
-Where \gls{ITASK} abstracts away from details such as user interfaces, data storage, and persistent workflows, \gls{MTASK} offers abstractions for edge layer-specific details such as the heterogeneity of architectures, platforms and frameworks; peripheral access; multitasking; task scheduling; and energy consumption.
-It is written in \gls{CLEAN} as a multi-view \gls{EDSL} and hence there are multiple interpretations of the language of which the byte code compiler is the most relevant for this thesis.
-From the terms in the \gls{TOP} language, a very compact binary representation of the work that needs to be done is compiled.
-This specification is then sent to a device that runs the \gls{MTASK} \gls{RTS}, a domain-specific \gls{TOP} engine implemented as a feather-light domain-specific \gls{OS}.
-\Gls{MTASK} is seamlessly integrated with \gls{ITASK}, it allows the programmer to define all layers of an \gls{IOT} system from a single declarative specification.
+Where \gls{ITASK} abstracts away from details such as user interfaces, data storage, client-side platforms, and persistent workflows.
+On the other hand, \gls{MTASK} offers abstractions for edge layer-specific details such as the heterogeneity of architectures, platforms and frameworks; peripheral access; (multi) task scheduling; and lowering energy consumption.
+The \gls{MTASK} language is written in \gls{CLEAN} as a multi-view \gls{EDSL} and hence there are multiple interpretations of the language of which the byte code compiler is the most relevant for this thesis.
+From \gls{MTASK} term constructed at runtime, a very compact binary representation of the work that needs to be done is compiled.
+This byte code is then sent to a device that running the \gls{MTASK} \gls{RTS}, a domain-specific \gls{TOP} engine implemented as a feather-light domain-specific \gls{OS}.
+\Gls{MTASK} is seamlessly integrated with \gls{ITASK}: \gls{MTASK} tasks are integrated in such a way that they function as \gls{ITASK} tasks, and \glspl{SDS} in on the device can tether an \gls{ITASK} \gls{SDS}.
+Using \gls{MTASK}, the programmer defines all layers of an \gls{IOT} system as a single declarative specification.
\todo[inline]{Is this example useful? I think it's too technical}
\Cref{lst:intro_blink} shows an interactive \gls{MTASK}\slash{}\gls{ITASK} application for blinking \pgls{LED} on the microcontroller every user-specified interval.
% \paragraph{Contribution}
% The research was carried out by \citet{crooijmans_reducing_2021} during his Master's thesis.
% I did the daily supervision and helped with the research, Pieter Koopman was the formal supervisor and wrote most of the paper.
- \item \emph{Green Computing for the Internet of Things}.\footnote{
+ \item \emph{Green Computing for the Internet of Things} \citep{lubbers_green_2022}.\footnote{
This work acknowledges the support of the Erasmus+ project ``SusTrainable---Promoting Sustainability as a Fundamental Driver in Software Development Training and Education'', no. 2020--1--PT01--KA203--078646}
+ These revised lecture notes are from a course on sustainable \gls{IOT} programming in \gls{MTASK} provided at the 2022 SusTrainable summer school in Rijeka, Croatia.
+
% \paragraph{Contribution}
% These revised lecture notes are from a course on sustainable programming using \gls{MTASK} provided at the 2022 SusTrainable summer school in Rijeka, Croatia.
% Pieter prepared and taught a quarter of the lecture and supervised the practical session.
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,%
+ %pinMode,digitalWrite,digitalRead,delay,millis,%
},
columns=fullflexible,
}
series = {{PPDP} '12},
title = {Task-{Oriented} {Programming} in a {Pure} {Functional} {Language}},
isbn = {978-1-4503-1522-7},
- url = {https://doi.org/10.1145/2370776.2370801},
doi = {10.1145/2370776.2370801},
abstract = {Task-Oriented Programming (TOP) is a novel programming paradigm for the construction of distributed systems where users work together on the internet. When multiple users collaborate, they need to interact with each other frequently. TOP supports the definition of tasks that react to the progress made by others. With TOP, complex multi-user interactions can be programmed in a declarative style just by defining the tasks that have to be accomplished, thus eliminating the need to worry about the implementation detail that commonly frustrates the development of applications for this domain. TOP builds on four core concepts: tasks that represent computations or work to do which have an observable value that may change over time, data sharing enabling tasks to observe each other while the work is in progress, generic type driven generation of user interaction, and special combinators for sequential and parallel task composition. The semantics of these core concepts is defined in this paper. As an example we present the iTask3 framework, which embeds TOP in the functional programming language Clean.},
booktitle = {Proceedings of the 14th {Symposium} on {Principles} and {Practice} of {Declarative} {Programming}},
series = {{POPL} '96},
title = {Revisiting {Catamorphisms} over {Datatypes} with {Embedded} {Functions} (or, {Programs} from {Outer} {Space})},
isbn = {0-89791-769-3},
- url = {https://doi.org/10.1145/237721.237792},
doi = {10.1145/237721.237792},
abstract = {We revisit the work of Paterson and of Meijer \& Hutton, which describes how to construct catamorphisms for recursive datatype definitions that embed contravariant occurrences of the type being defined. Their construction requires, for each catamorphism, the definition of an anamorphism that has an inverse-like relationship to that catamorphism. We present an alternative construction, which replaces the stringent requirement that an inverse anamorphism be defined for each catamorphism with a more lenient restriction. The resulting construction has a more efficient implementation than that of Paterson, Meijer, and Hutton and the relevant restriction can be enforced by a Hindley-Milner type inference algorithm. We provide numerous examples illustrating our method.},
booktitle = {Proceedings of the 23rd {ACM} {SIGPLAN}-{SIGACT} {Symposium} on {Principles} of {Programming} {Languages}},
series = {{PLDI} '88},
title = {Higher-{Order} {Abstract} {Syntax}},
isbn = {0-89791-269-1},
- url = {https://doi.org/10.1145/53990.54010},
doi = {10.1145/53990.54010},
abstract = {We describe motivation, design, use, and implementation of higher-order abstract syntax as a central representation for programs, formulas, rules, and other syntactic objects in program manipulation and other formal systems where matching and substitution or unification are central operations. Higher-order abstract syntax incorporates name binding information in a uniform and language generic way. Thus it acts as a powerful link integrating diverse tools in such formal environments. We have implemented higher-order abstract syntax, a supporting matching and unification algorithm, and some clients in Common Lisp in the framework of the Ergo project at Carnegie Mellon University.},
booktitle = {Proceedings of the {ACM} {SIGPLAN} 1988 {Conference} on {Programming} {Language} {Design} and {Implementation}},
series = {{ICFP} '08},
title = {Parametric {Higher}-{Order} {Abstract} {Syntax} for {Mechanized} {Semantics}},
isbn = {978-1-59593-919-7},
- url = {https://doi.org/10.1145/1411204.1411226},
doi = {10.1145/1411204.1411226},
abstract = {We present parametric higher-order abstract syntax (PHOAS), a new approach to formalizing the syntax of programming languages in computer proof assistants based on type theory. Like higher-order abstract syntax (HOAS), PHOAS uses the meta language's binding constructs to represent the object language's binding constructs. Unlike HOAS, PHOAS types are definable in general-purpose type theories that support traditional functional programming, like Coq's Calculus of Inductive Constructions. We walk through how Coq can be used to develop certified, executable program transformations over several statically-typed functional programming languages formalized with PHOAS; that is, each transformation has a machine-checked proof of type preservation and semantic preservation. Our examples include CPS translation and closure conversion for simply-typed lambda calculus, CPS translation for System F, and translation from a language with ML-style pattern matching to a simpler language with no variable-arity binding constructs. By avoiding the syntactic hassle associated with first-order representation techniques, we achieve a very high degree of proof automation.},
booktitle = {Proceedings of the 13th {ACM} {SIGPLAN} {International} {Conference} on {Functional} {Programming}},
address = {New York, NY},
title = {User-{Defined} {Types} and {Procedural} {Data} {Structures} as {Complementary} {Approaches} to {Data} {Abstraction}},
isbn = {978-1-4612-6315-9},
- url = {https://doi.org/10.1007/978-1-4612-6315-9_22},
abstract = {User-defined types (or modes) and procedural (or functional) data structures are complementary methods for data abstraction, each providing a capability lacked by the other. With user-defined types, all information about the representation of a particular kind of data is centralized in a type definition and hidden from the rest of the program. With procedural data structures, each part of the program which creates data can specify its own representation, independently of any representations used elsewhere for the same kind of data. However, this decentralization of the description of data is achieved at the cost of prohibiting primitive operations from accessing the representations of more than one data item. The contrast between these approaches is illustrated by a simple example.},
booktitle = {Programming {Methodology}: {A} {Collection} of {Articles} by {Members} of {IFIP} {WG2}.3},
publisher = {Springer New York},
series = {{PPDP} '06},
title = {Open {Data} {Types} and {Open} {Functions}},
isbn = {1-59593-388-3},
- url = {https://doi.org/10.1145/1140335.1140352},
doi = {10.1145/1140335.1140352},
abstract = {The problem of supporting the modular extensibility of both data and functions in one programming language at the same time is known as the expression problem. Functional languages traditionally make it easy to add new functions, but extending data (adding new data constructors) requires modifying existing code. We present a semantically and syntactically lightweight variant of open data types and open functions as a solution to the expression problem in the Haskell language. Constructors of open data types and equations of open functions may appear scattered throughout a program with several modules. The intended semantics is as follows: the program should behave as if the data types and functions were closed, defined in one place. The order of function equations is determined by best-fit pattern matching, where a specific pattern takes precedence over an unspecific one. We show that our solution is applicable to the expression problem, generic programming, and exceptions. We sketch two implementations: a direct implementation of the semantics, and a scheme based on mutually recursive modules that permits separate compilation},
booktitle = {Proceedings of the 8th {ACM} {SIGPLAN} {International} {Conference} on {Principles} and {Practice} of {Declarative} {Programming}},
series = {{ICFP} '98},
title = {Fold and {Unfold} for {Program} {Semantics}},
isbn = {1-58113-024-4},
- url = {https://doi.org/10.1145/289423.289457},
doi = {10.1145/289423.289457},
abstract = {In this paper we explain how recursion operators can be used to structure and reason about program semantics within a functional language. In particular, we show how the recursion operator fold can be used to structure denotational semantics, how the dual recursion operator unfold can be used to structure operational semantics, and how algebraic properties of these operators can be used to reason about program semantics. The techniques are explained with the aid of two main examples, the first concerning arithmetic expressions, and the second concerning Milner's concurrent language CCS. The aim of the paper is to give functional programmers new insights into recursion operators, program semantics, and the relationships between them.},
booktitle = {Proceedings of the {Third} {ACM} {SIGPLAN} {International} {Conference} on {Functional} {Programming}},
title = {Dynamic {Typing} in a {Statically} {Typed} {Language}},
volume = {13},
issn = {0164-0925},
- url = {https://doi.org/10.1145/103135.103138},
doi = {10.1145/103135.103138},
abstract = {Statically typed programming languages allow earlier error checking, better enforcement of diciplined programming styles, and the generation of more efficient object code than languages where all type consistency checks are performed at run time. However, even in statically typed languages, there is often the need to deal with datawhose type cannot be determined at compile time. To handle such situations safely, we propose to add a type Dynamic whose values are pairs of a value v and a type tag T where v has the type denoted by T. Instances of Dynamic are built with an explicit tagging construct and inspected with a type safe typecase construct.This paper explores the syntax, operational semantics, and denotational semantics of a simple language that includes the type Dynamic. We give examples of how dynamically typed values can be used in programming. Then we discuss an operational semantics for our language and obtain a soundness theorem. We present two formulations of the denotational semantics of this language and relate them to the operational semantics. Finally, we consider the implications of polymorphism and some implementation issues.},
number = {2},
title = {Abstract {Types} {Have} {Existential} {Type}},
volume = {10},
issn = {0164-0925},
- url = {https://doi.org/10.1145/44501.45065},
doi = {10.1145/44501.45065},
abstract = {Abstract data type declarations appear in typed programming languages like Ada, Alphard, CLU and ML. This form of declaration binds a list of identifiers to a type with associated operations, a composite “value” we call a data algebra. We use a second-order typed lambda calculus SOL to show how data algebras may be given types, passed as parameters, and returned as results of function calls. In the process, we discuss the semantics of abstract data type declarations and review a connection between typed programming languages and constructive logic.},
number = {3},
series = {{TLDI} '12},
title = {Giving {Haskell} a {Promotion}},
isbn = {978-1-4503-1120-5},
- url = {https://doi.org/10.1145/2103786.2103795},
doi = {10.1145/2103786.2103795},
abstract = {Static type systems strive to be richly expressive while still being simple enough for programmers to use. We describe an experiment that enriches Haskell's kind system with two features promoted from its type system: data types and polymorphism. The new system has a very good power-to-weight ratio: it offers a significant improvement in expressiveness, but, by re-using concepts that programmers are already familiar with, the system is easy to understand and implement.},
booktitle = {Proceedings of the 8th {ACM} {SIGPLAN} {Workshop} on {Types} in {Language} {Design} and {Implementation}},
series = {Haskell '09},
title = {Unembedding {Domain}-{Specific} {Languages}},
isbn = {978-1-60558-508-6},
- url = {https://doi.org/10.1145/1596638.1596644},
doi = {10.1145/1596638.1596644},
abstract = {Higher-order abstract syntax provides a convenient way of embedding domain-specific languages, but is awkward to analyse and manipulate directly. We explore the boundaries of higher-order abstract syntax. Our key tool is the unembedding of embedded terms as de Bruijn terms, enabling intensional analysis. As part of our solution we present techniques for separating the definition of an embedded program from its interpretation, giving modular extensions of the embedded language, and different ways to encode the types of the embedded language.},
booktitle = {Proceedings of the 2nd {ACM} {SIGPLAN} {Symposium} on {Haskell}},
address = {Cham},
title = {Functional {Programming} for {Domain}-{Specific} {Languages}},
isbn = {978-3-319-15940-9},
- url = {https://doi.org/10.1007/978-3-319-15940-9_1},
abstract = {Domain-specific languages are a popular application area for functional programming; and conversely, functional programming is a popular implementation vehicle for domain-specific languages—at least, for embedded ones. Why is this? The appeal of embedded domain-specific languages is greatly enhanced by the presence of convenient lightweight tools for defining, implementing, and optimising new languages; such tools represent one of functional programming's strengths. In these lectures we discuss functional programming techniques for embedded domain-specific languages; we focus especially on algebraic datatypes and higher-order functions, and their influence on deep and shallow embeddings.},
booktitle = {Central {European} {Functional} {Programming} {School}: 5th {Summer} {School}, {CEFP} 2013, {Cluj}-{Napoca}, {Romania}, {July} 8-20, 2013, {Revised} {Selected} {Papers}},
publisher = {Springer International Publishing},
file = {Gibbons - 2015 - Functional Programming for Domain-Specific Languag.pdf:/home/mrl/.local/share/zotero/storage/ARUBLFU6/Gibbons - 2015 - Functional Programming for Domain-Specific Languag.pdf:application/pdf},
}
-@mastersthesis{veen_van_der_mutable_2020,
+@mastersthesis{van_der_veen_mutable_2020,
address = {Nijmegen},
title = {Mutable {Collection} {Types} in {Shallow} {Embedded} {DSLs}},
language = {en},
school = {Radboud University},
- author = {Veen, van der, Erin},
+ author = {van der Veen, Erin},
month = jun,
year = {2020},
file = {thesis_final.pdf:/home/mrl/.local/share/zotero/storage/Y9QWGGB9/thesis_final.pdf:application/pdf},
file = {Alimarine - Generic Functional Programming.pdf:/home/mrl/.local/share/zotero/storage/PDTS3SGX/Alimarine - Generic Functional Programming.pdf:application/pdf},
}
-@phdthesis{boer_de_secure_2020,
+@phdthesis{de_boer_secure_2020,
address = {Nijmegen},
type = {Bachelor's {Thesis}},
title = {Secure {Communication} {Channels} for the {mTask} {System}.},
language = {en},
school = {Radboud University},
- author = {Boer, de, Michel},
+ author = {de Boer, Michel},
month = jun,
year = {2020},
file = {Boer, de - 2020 - Secure Communication Channels for the mTask System.pdf:/home/mrl/.local/share/zotero/storage/C46E3FBF/Boer, de - 2020 - Secure Communication Channels for the mTask System.pdf:application/pdf},
title = {Maintaining {Separation} of {Concerns} {Through} {Task} {Oriented} {Software} {Development}},
volume = {10788},
isbn = {978-3-319-89718-9 978-3-319-89719-6},
- url = {http://link.springer.com/10.1007/978-3-319-89719-6_2},
abstract = {Task Oriented Programming is a programming paradigm that enhances ‘classic’ functional programming with means to express the coordination of work among people and computer systems, the distribution and control of data sources, and the human-machine interfaces. To make the creation process of such applications feasible, it is important to have separation of concerns. In this paper we demonstrate how this is achieved within the Task Oriented Software Development process and illustrate the approach by means of a case study.},
language = {en},
urldate = {2019-01-14},
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},
title = {A {Shallow} {Embedded} {Type} {Safe} {Extendable} {DSL} for the {Arduino}},
volume = {9547},
isbn = {978-3-319-39110-6},
- url = {http://link.springer.com/10.1007/978-3-319-39110-6},
urldate = {2017-02-22},
booktitle = {Trends in {Functional} {Programming}},
publisher = {Springer International Publishing},
@inproceedings{cheney_lightweight_2002,
title = {A lightweight implementation of generics and dynamics},
- url = {http://dl.acm.org/citation.cfm?id=581698},
doi = {10.1145/581690.581698},
urldate = {2017-05-15},
booktitle = {Proceedings of the 2002 {ACM} {SIGPLAN} workshop on {Haskell}},
title = {A {Survey} of {Metaprogramming} {Languages}},
volume = {52},
issn = {0360-0300},
- url = {https://doi.org/10.1145/3354584},
doi = {10.1145/3354584},
abstract = {Metaprogramming is the process of writing computer programs that treat programs as data, enabling them to analyze or transform existing programs or generate new ones. While the concept of metaprogramming has existed for several decades, activities focusing on metaprogramming have been increasing rapidly over the past few years, with most languages offering some metaprogramming support and the amount of metacode being developed growing exponentially. In this article, we introduce a taxonomy of metaprogramming languages and present a survey of metaprogramming languages and systems based on the taxonomy. Our classification is based on the metaprogramming model adopted by the language, the phase of the metaprogram evaluation, the metaprogram source location, and the relation between the metalanguage and the object language.},
number = {6},
series = {Haskell '07},
title = {Why {It}'s {Nice} to {Be} {Quoted}: {Quasiquoting} for {Haskell}},
isbn = {978-1-59593-674-5},
- url = {https://doi.org/10.1145/1291201.1291211},
doi = {10.1145/1291201.1291211},
abstract = {Quasiquoting allows programmers to use domain specific syntax to construct program fragments. By providing concrete syntax for complex data types, programs become easier to read, easier to write, and easier to reason about and maintain. Haskell is an excellent host language for embedded domain specific languages, and quasiquoting ideally complements the language features that make Haskell perform so well in this area. Unfortunately, until now no Haskell compiler has provided support for quasiquoting. We present an implementation in GHC and demonstrate that by leveraging existing compiler capabilities, building a full quasiquoter requires little more work than writing a parser. Furthermore, we provide a compile-time guarantee that all quasiquoted data is type-correct.},
booktitle = {Proceedings of the {ACM} {SIGPLAN} {Workshop} on {Haskell} {Workshop}},
title = {Domain {Specific} {Language} {Implementation} via {Compile}-{Time} {Meta}-{Programming}},
volume = {30},
issn = {0164-0925},
- url = {https://doi.org/10.1145/1391956.1391958},
doi = {10.1145/1391956.1391958},
abstract = {Domain specific languages (DSLs) are mini-languages that are increasingly seen as being a valuable tool for software developers and non-developers alike. DSLs must currently be created in an ad-hoc fashion, often leading to high development costs and implementations of variable quality. In this article, I show how expressive DSLs can be hygienically embedded in the Converge programming language using its compile-time meta-programming facility, the concept of DSL blocks, and specialised error reporting techniques. By making use of pre-existing facilities, and following a simple methodology, DSL implementation costs can be significantly reduced whilst leading to higher quality DSL implementations.},
number = {6},
series = {Haskell '08},
title = {Making {Monads} {First}-{Class} with {Template} {Haskell}},
isbn = {978-1-60558-064-7},
- url = {https://doi.org/10.1145/1411286.1411300},
doi = {10.1145/1411286.1411300},
abstract = {Monads as an organizing principle for programming and semantics are notoriously difficult to grasp, yet they are a central and powerful abstraction in Haskell. This paper introduces a domain-specific language, MonadLab, that simplifies the construction of monads, and describes its implementation in Template Haskell. MonadLab makes monad construction truly first class, meaning that arcane theoretical issues with respect to monad transformers are completely hidden from the programmer. The motivation behind the design of MonadLab is to make monadic programming in Haskell simpler while providing a tool for non-Haskell experts that will assist them in understanding this powerful abstraction.},
booktitle = {Proceedings of the {First} {ACM} {SIGPLAN} {Symposium} on {Haskell}},
series = {Haskell '02},
title = {Template {Meta}-{Programming} for {Haskell}},
isbn = {1-58113-605-6},
- url = {https://doi.org/10.1145/581690.581691},
doi = {10.1145/581690.581691},
abstract = {We propose a new extension to the purely functional programming language Haskell that supports compile-time meta-programming. The purpose of the system is to support the algorithmic construction of programs at compile-time.The ability to generate code at compile time allows the programmer to implement such features as polytypic programs, macro-like expansion, user directed optimization (such as inlining), and the generation of supporting data structures and functions from existing data structures and functions.Our design is being implemented in the Glasgow Haskell Compiler, ghc.},
booktitle = {Proceedings of the 2002 {ACM} {SIGPLAN} {Workshop} on {Haskell}},
@article{hammond_automatic_2003,
title = {{AUTOMATIC} {SKELETONS} {IN} {TEMPLATE} {HASKELL}},
volume = {13},
- url = {https://doi.org/10.1142/S0129626403001380},
doi = {10.1142/S0129626403001380},
abstract = {This paper uses Template Haskell to automatically select appropriate skeleton implementations in the Eden parallel dialect of Haskell. The approach allows implementation parameters to be statically tuned according to architectural cost models based on source analyses. This permits us to target a range of parallel architecture classes from a single source specification. A major advantage of the approach is that cost models are user-definable and can be readily extended to new data or computation structures etc.},
number = {03},
series = {Haskell '12},
title = {Template {Your} {Boilerplate}: {Using} {Template} {Haskell} for {Efficient} {Generic} {Programming}},
isbn = {978-1-4503-1574-6},
- url = {https://doi.org/10.1145/2364506.2364509},
doi = {10.1145/2364506.2364509},
abstract = {Generic programming allows the concise expression of algorithms that would otherwise require large amounts of handwritten code. A number of such systems have been developed over the years, but a common drawback of these systems is poor runtime performance relative to handwritten, non-generic code. Generic-programming systems vary significantly in this regard, but few consistently match the performance of handwritten code. This poses a dilemma for developers. Generic-programming systems offer concision but cost performance. Handwritten code offers performance but costs concision.This paper explores the use of Template Haskell to achieve the best of both worlds. It presents a generic-programming system for Haskell that provides both the concision of other generic-programming systems and the efficiency of handwritten code. Our system gives the programmer a high-level, generic-programming interface, but uses Template Haskell to generate efficient, non-generic code that outperforms existing generic-programming systems for Haskell.This paper presents the results of benchmarking our system against both handwritten code and several other generic-programming systems. In these benchmarks, our system matches the performance of handwritten code while other systems average anywhere from two to twenty times slower.},
booktitle = {Proceedings of the 2012 {Haskell} {Symposium}},
address = {Berlin, Heidelberg},
title = {Embedding a {Hardware} {Description} {Language} in {Template} {Haskell}},
isbn = {978-3-540-25935-0},
- url = {https://doi.org/10.1007/978-3-540-25935-0_9},
abstract = {Hydra is a domain-specific language for designing digital circuits, which is implemented by embedding within Haskell. Many features required for hardware specification fit well within functional languages, leading in many cases to a perfect embedding. There are some situations, including netlist generation and software logic probes, where the DSL does not fit exactly within the host functional language. A new solution to these problems is based on program transformations performed automatically by metaprograms in Template Haskell.},
booktitle = {Domain-{Specific} {Program} {Generation}: {International} {Seminar}, {Dagstuhl} {Castle}, {Germany}, {March} 23-28, 2003. {Revised} {Papers}},
publisher = {Springer Berlin Heidelberg},
address = {Berlin, Heidelberg},
title = {{DSL} {Implementation} in {MetaOCaml}, {Template} {Haskell}, and {C}++},
isbn = {978-3-540-25935-0},
- url = {https://doi.org/10.1007/978-3-540-25935-0_4},
abstract = {A wide range of domain-specific languages (DSLs) has been implemented successfully by embedding them in general purpose languages. This paper reviews embedding, and summarizes how two alternative techniques – staged interpreters and templates – can be used to overcome the limitations of embedding. Both techniques involve a form of generative programming. The paper reviews and compares three programming languages that have special support for generative programming. Two of these languages (MetaOCaml and Template Haskell) are research languages, while the third (C++) is already in wide industrial use. The paper identifies several dimensions that can serve as a basis for comparing generative languages.},
booktitle = {Domain-{Specific} {Program} {Generation}: {International} {Seminar}, {Dagstuhl} {Castle}, {Germany}, {March} 23-28, 2003. {Revised} {Papers}},
publisher = {Springer Berlin Heidelberg},
series = {{LFP} '86},
title = {Hygienic {Macro} {Expansion}},
isbn = {0-89791-200-4},
- url = {https://doi.org/10.1145/319838.319859},
doi = {10.1145/319838.319859},
booktitle = {Proceedings of the 1986 {ACM} {Conference} on {LISP} and {Functional} {Programming}},
publisher = {Association for Computing Machinery},
series = {{TLDI} '03},
title = {Scrap {Your} {Boilerplate}: {A} {Practical} {Design} {Pattern} for {Generic} {Programming}},
isbn = {1-58113-649-8},
- url = {https://doi.org/10.1145/604174.604179},
doi = {10.1145/604174.604179},
abstract = {We describe a design pattern for writing programs that traverse data structures built from rich mutually-recursive data types. Such programs often have a great deal of "boilerplate" code that simply walks the structure, hiding a small amount of "real" code that constitutes the reason for the traversal.Our technique allows most of this boilerplate to be written once and for all, or even generated mechanically, leaving the programmer free to concentrate on the important part of the algorithm. These generic programs are much more adaptive when faced with data structure evolution because they contain many fewer lines of type-specific code.Our approach is simple to understand, reasonably efficient, and it handles all the data types found in conventional functional programming languages. It makes essential use of rank-2 polymorphism, an extension found in some implementations of Haskell. Further it relies on a simple type-safe cast operator.},
booktitle = {Proceedings of the 2003 {ACM} {SIGPLAN} {International} {Workshop} on {Types} in {Languages} {Design} and {Implementation}},
series = {{GPCE} 2014},
title = {{LibDSL}: {A} {Library} for {Developing} {Embedded} {Domain} {Specific} {Languages} in d via {Template} {Metaprogramming}},
isbn = {978-1-4503-3161-6},
- url = {https://doi.org/10.1145/2658761.2658770},
doi = {10.1145/2658761.2658770},
abstract = {This paper presents a library called LibDSL that helps the implementer of an embedded domain specific language (EDSL) effectively develop it in D language. The LibDSL library accepts as input some kinds of “specifications” of the EDSL that the implementer is going to develop and a D program within which an EDSL source program written by the user is embedded. It produces the front-end code of an LALR parser for the EDSL program and back-end code of the execution engine. LibDSL is able to produce two kinds of execution engines, namely compiler-based and interpreter-based engines, either of which the user can properly choose depending on whether an EDSL program is known at compile time or not. We have implemented the LibDSL system by using template metaprogramming and other advanced facilities such as compile-time function execution of D language. EDSL programs developed by means of LibDSL have a nice integrativeness with the host language.},
booktitle = {Proceedings of the 2014 {International} {Conference} on {Generative} {Programming}: {Concepts} and {Experiences}},
series = {Haskell '11},
title = {Embedded {Parser} {Generators}},
isbn = {978-1-4503-0860-1},
- url = {https://doi.org/10.1145/2034675.2034689},
doi = {10.1145/2034675.2034689},
abstract = {We present a novel method of embedding context-free grammars in Haskell, and to automatically generate parsers and pretty-printers from them. We have implemented this method in a library called BNFC-meta (from the BNF Converter, which it is built on). The library builds compiler front ends using metaprogramming instead of conventional code generation. Parsers are built from labelled BNF grammars that are defined directly in Haskell modules. Our solution combines features of parser generators (static grammar checks, a highly specialised grammar DSL) and adds several features that are otherwise exclusive to combinatory libraries such as the ability to reuse, parameterise and generate grammars inside Haskell.To allow writing grammars in concrete syntax, BNFC-meta provides a quasi-quoter that can parse grammars (embedded in Haskell files) at compile time and use metaprogramming to replace them with their abstract syntax. We also generate quasi-quoters so that the languages we define with BNFC-meta can be embedded in the same way. With a minimal change to the grammar, we support adding anti-quotation to the generated quasi-quoters, which allows users of the defined language to mix concrete and abstract syntax almost seamlessly. Unlike previous methods of achieving anti-quotation, the method used by BNFC-meta is simple, efficient and avoids polluting the abstract syntax types.},
booktitle = {Proceedings of the 4th {ACM} {Symposium} on {Haskell}},
series = {Haskell '14},
title = {Promoting {Functions} to {Type} {Families} in {Haskell}},
isbn = {978-1-4503-3041-1},
- url = {https://doi.org/10.1145/2633357.2633361},
doi = {10.1145/2633357.2633361},
abstract = {Haskell, as implemented in the Glasgow Haskell Compiler (GHC), is enriched with many extensions that support type-level programming, such as promoted datatypes, kind polymorphism, and type families. Yet, the expressiveness of the type-level language remains limited. It is missing many features present at the term level, including case expressions, anonymous functions, partially-applied functions, and let expressions. In this paper, we present an algorithm - with a proof of correctness - to encode these term-level constructs at the type level. Our approach is automated and capable of promoting a wide array of functions to type families. We also highlight and discuss those term-level features that are not promotable. In so doing, we offer a critique on GHC's existing type system, showing what it is already capable of and where it may want improvement.We believe that delineating the mismatch between GHC's term level and its type level is a key step toward supporting dependently typed programming.},
booktitle = {Proceedings of the 2014 {ACM} {SIGPLAN} {Symposium} on {Haskell}},
series = {{IFL} 2018},
title = {A {Staged} {Embedding} of {Attribute} {Grammars} in {Haskell}},
isbn = {978-1-4503-7143-8},
- url = {https://doi.org/10.1145/3310232.3310235},
doi = {10.1145/3310232.3310235},
abstract = {In this paper, we present an embedding of attribute grammars in Haskell, that is both modular and type-safe, while providing the user with domain specific error messages.Our approach involves to delay part of the safety checks to runtime. When a grammar is correct, we are able to extract a function that can be run without expecting any runtime error related to the EDSL.},
booktitle = {Proceedings of the 30th {Symposium} on {Implementation} and {Application} of {Functional} {Languages}},
address = {Berlin, Heidelberg},
title = {Typed {Tagless} {Final} {Interpreters}},
isbn = {978-3-642-32202-0},
- url = {https://doi.org/10.1007/978-3-642-32202-0_3},
abstract = {The so-called `typed tagless final' approach of [6] has collected and polished a number of techniques for representing typed higher-order languages in a typed metalanguage, along with type-preserving interpretation, compilation and partial evaluation. The approach is an alternative to the traditional, or `initial' encoding of an object language as a (generalized) algebraic data type. Both approaches permit multiple interpretations of an expression, to evaluate it, pretty-print, etc. The final encoding represents all and only typed object terms without resorting to generalized algebraic data types, dependent or other fancy types. The final encoding lets us add new language forms and interpretations without breaking the existing terms and interpreters.},
booktitle = {Generic and {Indexed} {Programming}: {International} {Spring} {School}, {SSGIP} 2010, {Oxford}, {UK}, {March} 22-26, 2010, {Revised} {Lectures}},
publisher = {Springer Berlin Heidelberg},
series = {Haskell '12},
title = {Safe {Haskell}},
isbn = {978-1-4503-1574-6},
- url = {https://doi.org/10.1145/2364506.2364524},
doi = {10.1145/2364506.2364524},
abstract = {Though Haskell is predominantly type-safe, implementations contain a few loopholes through which code can bypass typing and module encapsulation. This paper presents Safe Haskell, a language extension that closes these loopholes. Safe Haskell makes it possible to confine and safely execute untrusted, possibly malicious code. By strictly enforcing types, Safe Haskell allows a variety of different policies from API sandboxing to information-flow control to be implemented easily as monads. Safe Haskell is aimed to be as unobtrusive as possible. It enforces properties that programmers tend to meet already by convention. We describe the design of Safe Haskell and an implementation (currently shipping with GHC) that infers safety for code that lies in a safe subset of the language. We use Safe Haskell to implement an online Haskell interpreter that can securely execute arbitrary untrusted code with no overhead. The use of Safe Haskell greatly simplifies this task and allows the use of a large body of existing code and tools.},
booktitle = {Proceedings of the 2012 {Haskell} {Symposium}},
series = {{ICFP} '14},
title = {Folding {Domain}-{Specific} {Languages}: {Deep} and {Shallow} {Embeddings} ({Functional} {Pearl})},
isbn = {978-1-4503-2873-9},
- url = {https://doi.org/10.1145/2628136.2628138},
doi = {10.1145/2628136.2628138},
abstract = {A domain-specific language can be implemented by embedding within a general-purpose host language. This embedding may be deep or shallow, depending on whether terms in the language construct syntactic or semantic representations. The deep and shallow styles are closely related, and intimately connected to folds; in this paper, we explore that connection.},
booktitle = {Proceedings of the 19th {ACM} {SIGPLAN} {International} {Conference} on {Functional} {Programming}},
series = {Haskell '05},
title = {{TypeCase}: {A} {Design} {Pattern} for {Type}-{Indexed} {Functions}},
isbn = {1-59593-071-X},
- url = {https://doi.org/10.1145/1088348.1088358},
doi = {10.1145/1088348.1088358},
abstract = {A type-indexed function is a function that is defined for each member of some family of types. Haskell's type class mechanism provides collections of open type-indexed functions, in which the indexing family can be extended by defining a new type class instance but the collection of functions is fixed. The purpose of this paper is to present TypeCase: a design pattern that allows the definition of closed type-indexed functions, in which the index family is fixed but the collection of functions is extensible. It is inspired by Cheney and Hinze's work on lightweight approaches to generic programming. We generalise their techniques as a design pattern. Furthermore, we show that type-indexed functions with type-indexed types, and consequently generic functions with generic types, can also be encoded in a lightweight manner, thereby overcoming one of the main limitations of the lightweight approaches.},
booktitle = {Proceedings of the 2005 {ACM} {SIGPLAN} {Workshop} on {Haskell}},
series = {{POPL} '96},
title = {Putting {Type} {Annotations} to {Work}},
isbn = {0-89791-769-3},
- url = {https://doi.org/10.1145/237721.237729},
doi = {10.1145/237721.237729},
abstract = {We study an extension of the Hindley/Milner system with explicit type scheme annotations and type declarations. The system can express polymorphic function arguments, user-defined data types with abstract components, and structure types with polymorphic fields. More generally, all programs of the polymorphic lambda calculus can be encoded by a translation between typing derivations. We show that type reconstruction in this system can be reduced to the decidable problem of first-order unification under a mixed prefix.},
booktitle = {Proceedings of the 23rd {ACM} {SIGPLAN}-{SIGACT} {Symposium} on {Principles} of {Programming} {Languages}},
series = {{PEPM} '16},
title = {Everything {Old} is {New} {Again}: {Quoted} {Domain}-{Specific} {Languages}},
isbn = {978-1-4503-4097-7},
- url = {https://doi.org/10.1145/2847538.2847541},
doi = {10.1145/2847538.2847541},
abstract = {We describe a new approach to implementing Domain-Specific Languages(DSLs), called Quoted DSLs (QDSLs), that is inspired by two old ideas:quasi-quotation, from McCarthy's Lisp of 1960, and the subformula principle of normal proofs, from Gentzen's natural deduction of 1935. QDSLs reuse facilities provided for the host language, since host and quoted terms share the same syntax, type system, and normalisation rules. QDSL terms are normalised to a canonical form, inspired by the subformula principle, which guarantees that one can use higher-order types in the source while guaranteeing first-order types in the target, and enables using types to guide fusion. We test our ideas by re-implementing Feldspar, which was originally implemented as an Embedded DSL (EDSL), as a QDSL; and we compare the QDSL and EDSL variants. The two variants produce identical code.},
booktitle = {Proceedings of the 2016 {ACM} {SIGPLAN} {Workshop} on {Partial} {Evaluation} and {Program} {Manipulation}},
series = {{DSL} '99},
title = {Domain {Specific} {Embedded} {Compilers}},
isbn = {1-58113-255-7},
- url = {https://doi.org/10.1145/331960.331977},
doi = {10.1145/331960.331977},
abstract = {Domain-specific embedded languages (DSELs) expressed in higher-order, typed (HOT) languages provide a composable framework for domain-specific abstractions. Such a framework is of greater utility than a collection of stand-alone domain-specific languages. Usually, embedded domain specific languages are build on top of a set of domain specific primitive functions that are ultimately implemented using some form of foreign function call. We sketch a general design pattern/or embedding client-server style services into Haskell using a domain specific embedded compiler for the server's source language. In particular we apply this idea to implement Haskell/DB, a domain specific embdedded compiler that dynamically generates of SQL queries from monad comprehensions, which are then executed on an arbitrary ODBC database server.},
booktitle = {Proceedings of the 2nd {Conference} on {Domain}-{Specific} {Languages}},
address = {Hershey, PA, USA},
title = {Extensible {Languages}: {Blurring} the {Distinction} between {DSL} and {GPL}},
isbn = {978-1-4666-2092-6},
- url = {https://services.igi-global.com/resolvedoi/resolve.aspx?doi=10.4018/978-1-4666-2092-6.ch001},
abstract = {Out of a concern for focus and concision, domain-specific languages (DSLs) are usually very different from general purpose programming languages (GPLs), both at the syntactic and the semantic levels. One approach to DSL implementation is to write a full language infrastructure, including parser, interpreter, or even compiler. Another approach however, is to ground the DSL into an extensible GPL, giving you control over its own syntax and semantics. The DSL may then be designed merely as an extension to the original GPL, and its implementation may boil down to expressing only the differences with it. The task of DSL implementation is hence considerably eased. The purpose of this chapter is to provide a tour of the features that make a GPL extensible, and to demonstrate how, in this context, the distinction between DSL and GPL can blur, sometimes to the point of complete disappearance.},
booktitle = {Formal and {Practical} {Aspects} of {Domain}-{Specific} {Languages}: {Recent} {Developments}},
publisher = {IGI Global},
series = {{PPDP} '19},
title = {{TopHat}: {A} {Formal} {Foundation} for {Task}-{Oriented} {Programming}},
isbn = {978-1-4503-7249-7},
- url = {https://doi.org/10.1145/3354166.3354182},
doi = {10.1145/3354166.3354182},
abstract = {Software that models how people work is omnipresent in today's society. Current languages and frameworks often focus on usability by non-programmers, sacrificing flexibility and high level abstraction. Task-oriented programming (TOP) is a programming paradigm that aims to provide the desired level of abstraction while still being expressive enough to describe real world collaboration. It prescribes a declarative programming style to specify multi-user workflows. Workflows can be higher-order. They communicate through typed values on a local and global level. Such specifications can be turned into interactive applications for different platforms, supporting collaboration during execution. TOP has been around for more than a decade, in the forms of iTasks and mTasks, which are tailored for real-world usability. So far, it has not been given a formalisation which is suitable for formal reasoning.In this paper we give a description of the TOP paradigm and then decompose its rich features into elementary language elements, which makes them suitable for formal treatment. We use the simply typed lambda-calculus, extended with pairs and references, as a base language. On top of this language, we develop TopHat, a language for modular interactive workflows. We describe TopHat by means of a layered semantics. These layers consist of multiple big-step evaluations on expressions, and two labelled transition systems, handling user inputs.With TopHat we prepare a way to formally reason about TOP languages and programs. This approach allows for comparison with other work in the field. We have implemented the semantic rules of TopHat in Haskell, and the task layer on top of the iTasks framework. This shows that our approach is feasible, and lets us demonstrate the concepts by means of illustrative case studies. TOP has been applied in projects with the Dutch coast guard, tax office, and navy. Our work matters because formal program verification is important for mission-critical software, especially for systems with concurrency.},
booktitle = {Proceedings of the 21st {International} {Symposium} on {Principles} and {Practice} of {Declarative} {Programming}},
address = {Cham},
title = {Type-{Safe} {Functions} and {Tasks} in a {Shallow} {Embedded} {DSL} for {Microprocessors}},
isbn = {978-3-030-28346-9},
- url = {https://doi.org/10.1007/978-3-030-28346-9_8},
abstract = {The Internet of Things, IoT, brings us large amounts of connected computing devices that are equipped with dedicated sensors and actuators. These computing devices are typically driven by a cheap microprocessor system with a relatively slow processor and a very limited amount of memory. Due to the special input-output capabilities of IoT devices and their connections it is very attractive to execute (parts of) programs on these microcomputers.},
booktitle = {Central {European} {Functional} {Programming} {School}: 6th {Summer} {School}, {CEFP} 2015, {Budapest}, {Hungary}, {July} 6–10, 2015, {Revised} {Selected} {Papers}},
publisher = {Springer International Publishing},
series = {{ICFP} '02},
title = {Typing {Dynamic} {Typing}},
isbn = {1-58113-487-8},
- url = {https://doi.org/10.1145/581478.581494},
doi = {10.1145/581478.581494},
abstract = {Even when programming in a statically typed language we every now and then encounter statically untypable values; such values result from interpreting values or from communicating with the outside world. To cope with this problem most languages include some form of dynamic types. It may be that the core language has been explicitly extended with such a type, or that one is allowed to live dangerously by using functions like unsafeCoerce. We show how, by a careful use of existentially and universally quantified types, one may achievem the same effect, without extending the language with new or unsafe features. The techniques explained are universally applicable, provided the core language is expressive enough; this is the case for the common implementations of Haskell. The techniques are used in the description of a type checking compiler that, starting from an expression term, constructs a typed function representing the semantics of that expression. In this function the overhead associated with the type checking is only once being paid for; in this sense we have thus achieved static type checking.},
booktitle = {Proceedings of the {Seventh} {ACM} {SIGPLAN} {International} {Conference} on {Functional} {Programming}},
address = {Berlin, Heidelberg},
title = {On {Adding} {Pattern} {Matching} to {Haskell}-{Based} {Deeply} {Embedded} {Domain} {Specific} {Languages}},
isbn = {978-3-030-67437-3},
- url = {https://doi.org/10.1007/978-3-030-67438-0_2},
doi = {10.1007/978-3-030-67438-0_2},
abstract = {Capturing control flow is the Achilles heel of Haskell-based deeply embedded domain specific languages. Rather than use the builtin control flow mechanisms, artificial control flow combinators are used instead. However, capturing traditional control flow in a deeply embedded domain specific language would support the writing of programs in a natural style by allowing the programmer to use the constructs that are already builtin to the base language, such as pattern matching and recursion. In this paper, we expand the capabilities of Haskell-based deep embeddings with a compiler extension for reifying conditionals and pattern matching. With this new support, the subset of Haskell that we use for expressing deeply embedded domain specific languages can be cleaner, Haskell-idiomatic, and more declarative in nature.},
booktitle = {Practical {Aspects} of {Declarative} {Languages}: 23rd {International} {Symposium}, {PADL} 2021, {Copenhagen}, {Denmark}, {January} 18-19, 2021, {Proceedings}},
address = {Berlin, Heidelberg},
title = {Generic {Haskell}: {Practice} and {Theory}},
isbn = {978-3-540-45191-4},
- url = {https://doi.org/10.1007/978-3-540-45191-4_1},
abstract = {Generic Haskell is an extension of Haskell that supports the construction of generic programs. These lecture notes describe the basic constructs of Generic Haskell and highlight the underlying theory.},
booktitle = {Generic {Programming}: {Advanced} {Lectures}},
publisher = {Springer Berlin Heidelberg},
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}},
series = {Haskell 2020},
title = {Staged {Sums} of {Products}},
isbn = {978-1-4503-8050-8},
- url = {https://doi.org/10.1145/3406088.3409021},
doi = {10.1145/3406088.3409021},
abstract = {Generic programming libraries have historically traded efficiency in return for convenience, and the generics-sop library is no exception. It offers a simple, uniform, representation of all datatypes precisely as a sum of products, making it easy to write generic functions. We show how to finally make generics-sop fast through the use of staging with Typed Template Haskell.},
booktitle = {Proceedings of the 13th {ACM} {SIGPLAN} {International} {Symposium} on {Haskell}},
@article{xie_staging_2022,
title = {Staging with {Class}: {A} {Specification} for {Typed} {Template} {Haskell}},
volume = {6},
- url = {https://doi.org/10.1145/3498723},
doi = {10.1145/3498723},
abstract = {Multi-stage programming using typed code quotation is an established technique for writing optimizing code generators with strong type-safety guarantees. Unfortunately, quotation in Haskell interacts poorly with type classes, making it difficult to write robust multi-stage programs. We study this unsound interaction and propose a resolution, staged type class constraints, which we formalize in a source calculus λ⇒ that elaborates into an explicit core calculus F. We show type soundness of both calculi, establishing that well-typed, well-staged source programs always elaborate to well-typed, well-staged core programs, and prove beta and eta rules for code quotations. Our design allows programmers to incorporate type classes into multi-stage programs with confidence. Although motivated by Haskell, it is also suitable as a foundation for other languages that support both overloading and quotation.},
number = {POPL},
series = {{WGP} '14},
title = {True {Sums} of {Products}},
isbn = {978-1-4503-3042-8},
- url = {https://doi.org/10.1145/2633628.2633634},
doi = {10.1145/2633628.2633634},
abstract = {We introduce the sum-of-products (SOP) view for datatype-generic programming (in Haskell). While many of the libraries that are commonly in use today represent datatypes as arbitrary combinations of binary sums and products, SOP reflects the structure of datatypes more faithfully: each datatype is a single n-ary sum, where each component of the sum is a single n-ary product. This representation turns out to be expressible accurately in GHC with today's extensions. The resulting list-like structure of datatypes allows for the definition of powerful high-level traversal combinators, which in turn encourage the definition of generic functions in a compositional and concise style. A major plus of the SOP view is that it allows to separate function-specific metadata from the main structural representation and recombining this information later.},
booktitle = {Proceedings of the 10th {ACM} {SIGPLAN} {Workshop} on {Generic} {Programming}},
@article{willis_staged_2020,
title = {Staged {Selective} {Parser} {Combinators}},
volume = {4},
- url = {https://doi.org/10.1145/3409002},
doi = {10.1145/3409002},
abstract = {Parser combinators are a middle ground between the fine control of hand-rolled parsers and the high-level almost grammar-like appearance of parsers created via parser generators. They also promote a cleaner, compositional design for parsers. Historically, however, they cannot match the performance of their counterparts. This paper describes how to compile parser combinators into parsers of hand-written quality. This is done by leveraging the static information present in the grammar by representing it as a tree. However, in order to exploit this information, it will be necessary to drop support for monadic computation since this generates dynamic structure. Selective functors can help recover lost functionality in the absence of monads, and the parser tree can be partially evaluated with staging. This is implemented in a library called Parsley.},
number = {ICFP},
series = {Haskell 2019},
title = {Multi-{Stage} {Programs} in {Context}},
isbn = {978-1-4503-6813-1},
- url = {https://doi.org/10.1145/3331545.3342597},
doi = {10.1145/3331545.3342597},
abstract = {Cross-stage persistence is an essential aspect of multi-stage programming that allows a value defined in one stage to be available in another. However, difficulty arises when implicit information held in types, type classes and implicit parameters needs to be persisted. Without a careful treatment of such implicit information—which are pervasive in Haskell—subtle yet avoidable bugs lurk beneath the surface. This paper demonstrates that in multi-stage programming care must be taken when representing quoted terms so that important implicit information is kept in context and not discarded. The approach is formalised with a type-system, and an implementation in GHC is presented that fixes problems of the previous incarnation.},
booktitle = {Proceedings of the 12th {ACM} {SIGPLAN} {International} {Symposium} on {Haskell}},
@article{pickering_specification_2021,
title = {A {Specification} for {Typed} {Template} {Haskell}},
volume = {abs/2112.03653},
- url = {https://arxiv.org/abs/2112.03653},
doi = {10.48550/arXiv.2112.03653},
journal = {CoRR},
author = {Pickering, Matthew and Löh, Andres and Wu, Nicolas},
@article{materzok_generating_2022,
title = {Generating {Circuits} with {Generators}},
volume = {6},
- url = {https://doi.org/10.1145/3549821},
doi = {10.1145/3549821},
abstract = {The most widely used languages and methods used for designing digital hardware fall into two rough categories. One of them, register transfer level (RTL), requires specifying each and every component in the designed circuit. This gives the designer full control, but burdens the designer with many trivial details. The other, the high-level synthesis (HLS) method, allows the designer to abstract the details of hardware away and focus on the problem being solved. This method however cannot be used for a class of hardware design problems because the circuit's clock is also abstracted away. We present YieldFSM, a hardware description language that uses the generator abstraction to represent clock-level timing in a digital circuit. It represents a middle ground between the RTL and HLS approaches: the abstraction level is higher than in RTL, but thanks to explicit information about clock-level timing, it can be used in applications where RTL is traditionally used. We also present the YieldFSM compiler, which uses methods developed by the functional programming community – including continuation-passsing style translation and defunctionalization – to translate YieldFSM programs to Mealy machines. It is implemented using Template Haskell and the Clash functional hardware description language. We show that this approach leads to short and conceptually simple hardware descriptions.},
number = {ICFP},
title = {Embedding {Non}-linear {Pattern} {Matching} with {Backtracking} for {Non}-free {Data} {Types} into {Haskell}},
volume = {40},
issn = {1882-7055},
- url = {https://doi.org/10.1007/s00354-022-00177-z},
doi = {10.1007/s00354-022-00177-z},
abstract = {Pattern matching is an important language construct for data abstraction. Many pattern-match extensions have been developed for extending the range of data types to which pattern matching is applicable. Among them, the pattern-match system proposed by Egi and Nishiwaki features practical pattern matching for non-free data types by providing a user-customizable non-linear pattern-match facility with backtracking. However, they implemented their proposal only in dynamically typed programming languages, and there were no proposals that allow programmers to benefit from both static type systems and expressive pattern matching. This paper proposes a method for implementing this pattern-match facility by meta-programming in Haskell. There are two technical challenges: (i) we need to design a set of typing rules for the pattern-match facility; (ii) we need to embed these typing rules in Haskell to make types of the pattern-match expressions inferable by the Haskell type system. We propose a set of typing rules and show that several GHC extensions, such as multi-parameter type classes, datatype promotion, GADTs, existential types, and view patterns, play essential roles for embedding these typing rules into Haskell. The implementation has already been distributed as a Haskell library miniEgison via Hackage.},
number = {2},
series = {Haskell 2022},
title = {Liquid {Proof} {Macros}},
isbn = {978-1-4503-9438-3},
- url = {https://doi.org/10.1145/3546189.3549921},
doi = {10.1145/3546189.3549921},
abstract = {Liquid Haskell is a popular verifier for Haskell programs, leveraging the power of SMT solvers to ease users' burden of proof. However, this power does not come without a price: convincing Liquid Haskell that a program is correct often necessitates giving hints to the underlying solver, which can be a tedious and verbose process that sometimes requires intricate knowledge of Liquid Haskell's inner workings. In this paper, we present Liquid Proof Macros, an extensible metaprogramming technique and framework for simplifying the development of Liquid Haskell proofs. We describe how to leverage Template Haskell to generate Liquid Haskell proof terms, via a tactic-inspired DSL interface for more concise and user-friendly proofs, and we demonstrate the capabilities of this framework by automating a wide variety of proofs from an existing Liquid Haskell benchmark.},
booktitle = {Proceedings of the 15th {ACM} {SIGPLAN} {International} {Haskell} {Symposium}},
series = {Haskell 2022},
title = {Embedded {Pattern} {Matching}},
isbn = {978-1-4503-9438-3},
- url = {https://doi.org/10.1145/3546189.3549917},
doi = {10.1145/3546189.3549917},
abstract = {Haskell is a popular choice for hosting deeply embedded languages. A recurring challenge for these embeddings is how to seamlessly integrate user defined algebraic data types. In particular, one important, convenient, and expressive feature for creating and inspecting data—pattern matching—is not directly available on embedded terms. We present a novel technique, embedded pattern matching, which enables a natural and user friendly embedding of user defined algebraic data types into the embedded language, and allows programmers to pattern match on terms in the embedded language in much the same way they would in the host language.},
booktitle = {Proceedings of the 15th {ACM} {SIGPLAN} {International} {Haskell} {Symposium}},
author = {Lubbers, Mart},
year = {2022},
}
+
+@article{nizetic_internet_2020,
+ title = {Internet of {Things} ({IoT}): {Opportunities}, issues and challenges towards a smart and sustainable future},
+ volume = {274},
+ issn = {0959-6526},
+ doi = {https://doi.org/10.1016/j.jclepro.2020.122877},
+ abstract = {The rapid development and implementation of smart and IoT (Internet of Things) based technologies have allowed for various possibilities in technological advancements for different aspects of life. The main goal of IoT technologies is to simplify processes in different fields, to ensure a better efficiency of systems (technologies or specific processes) and finally to improve life quality. Sustainability has become a key issue for population where the dynamic development of IoT technologies is bringing different useful benefits, but this fast development must be carefully monitored and evaluated from an environmental point of view to limit the presence of harmful impacts and ensure the smart utilization of limited global resources. Significant research efforts are needed in the previous sense to carefully investigate the pros and cons of IoT technologies. This review editorial is partially directed on the research contributions presented at the 4th International Conference on Smart and Sustainable Technologies held in Split and Bol, Croatia, in 2019 (SpliTech 2019) as well as on recent findings from literature. The SpliTech2019 conference was a valuable event that successfully linked different engineering professions, industrial experts and finally researchers from academia. The focus of the conference was directed towards key conference tracks such as Smart City, Energy/Environment, e-Health and Engineering Modelling. The research presented and discussed at the SpliTech2019 conference helped to understand the complex and intertwined effects of IoT technologies on societies and their potential effects on sustainability in general. Various application areas of IoT technologies were discussed as well as the progress made. Four main topical areas were discussed in the herein editorial, i.e. latest advancements in the further fields: (i) IoT technologies in Sustainable Energy and Environment, (ii) IoT enabled Smart City, (iii) E-health – Ambient assisted living systems (iv) IoT technologies in Transportation and Low Carbon Products. The main outcomes of the review introductory article contributed to the better understanding of current technological progress in IoT application areas as well as the environmental implications linked with the increased application of IoT products.},
+ journal = {Journal of Cleaner Production},
+ author = {Nižetić, Sandro and Šolić, Petar and González-de-Artaza, Diego López-de-Ipiña and Patrono, Luigi},
+ year = {2020},
+ keywords = {Energy, Environment, IoT, Smart city, SpliTech2020, Sustainability},
+ pages = {122877},
+}
in-press},
keywords = {access control, internet-of-things, policy language, privilege escalation, Smart home system},
}
+@incollection{lubbers_green_2022,
+ address = {Cham},
+ title = {Green {Computing} for the {Internet} of {Things}},
+ language = {en},
+ booktitle = {{SusTrainable} {Summer} {School} 2022, {Rijeka}, {Croatia}, {July} 4–5, 2022, {Revised} {Selected} {Papers}},
+ publisher = {Springer International Publishing},
+ author = {Lubbers, Mart and Koopman, Pieter},
+ year = {2022},
+ note = {in-press},
+ pages = {1},
+}
\part[\'Etude --- Domain-Specific Languages]{\'Etude\\[2ex]\smaller{}Domain-Specific Languages}%
\label{prt:dsl}
-\subfile{dsl/class_deep_embedding} % Deep embedding with class
-\subfile{dsl/first-class_datatypes} % First-class data types
+\subfile{dsl/class} % Deep embedding with class
+\subfile{dsl/first} % First-class data types
\part[Oratorio --- Task-Oriented Programming]{Oratorio\\[2ex]\smaller{}Task-Oriented Programming for the Internet of Things}%
\label{prt:top}
}
@inproceedings{epstein2011towards,
- author = {Epstein, Jeff and Black, Andrew P. and Peyton-Jones, Simon},
+ author = {Epstein, Jeff and Black, Andrew P. and Peyton Jones, Simon},
title = {Towards Haskell in the Cloud},
year = {2011},
isbn = {9781450308601},
keywords = {distributed systems, web applications, network communication}
}
-@article{jones_1992, title={Implementing lazy functional languages on stock hardware: the Spineless Tagless G-machine}, volume={2}, DOI={10.1017/S0956796800000319}, number={2}, journal={Journal of Functional Programming}, publisher={Cambridge University Press}, author={Jones, Simon L. Peyton}, year={1992}, pages={127–202}}
+@article{jones_1992, title={Implementing lazy functional languages on stock
+ hardware: the Spineless Tagless G-machine}, volume={2},
+ DOI={10.1017/S0956796800000319}, number={2}, journal={Journal of Functional
+ Programming},
+publisher={Cambridge University Press}, author={Peyton Jones, Simon}, year={1992}, pages={127–202}}
@article{domoszlai_implementing_2011,
--- /dev/null
+\documentclass[../thesis.tex]{subfiles}
+
+\input{subfilepreamble}
+
+\begin{document}
+\input{subfileprefix}
+
+\chapter{\texorpdfstring{\Glsxtrshort{TOP} for the \glsxtrshort{IOT}}{TOP for the IoT}}%
+\label{chp:top4iot}
+\begin{chapterabstract}
+ This chapter:
+ \begin{itemize}
+ \item introduces the problems with \gls{TOP} for the \gls{IOT}.
+ \item shows how to create the \emph{Hello World!} application for microcontrollers using \gls{ARDUINO};
+ \item extends this idea with multithreading, demonstrating the difficulty programming multi-tasking applications;
+ \item describes a comparative variant in \gls{MTASK} and shows that upgrading to a multi-tasking variant is straightforward
+ \item demonstrates that the complexity of running multiple tasks;
+ \item and concludes with the history of \gls{MTASK}'s development.
+ \end{itemize}
+\end{chapterabstract}
+
+The edge layer of \gls{IOT} system mostly consists of microcontrollers.
+Microcontrollers are tiny computers designed specifically for embedded applications.
+They therefore only have a soup\c{c}on of memory, have a slow processor, come with many energy efficient sleep modes and have a lot of peripheral support such as \gls{GPIO} pins.
+Usually, programming microcontrollers requires an elaborate multi-step toolchain of compilation, linkage, binary image creation, and burning this image onto the flash memory of the microcontroller in order to compile and run a program.
+The programs are usually cyclic executives instead of tasks running in an operating system, i.e.\ there is only a single task that continuously runs on the bare metal.
+\Cref{tbl:mcu_laptop} compares the hardware properties of a typical laptop with two very popular microcontrollers.
+
+\begin{table}
+ \caption{Hardware characteristics of typical microcontrollers compared to laptops.}%
+ \label{tbl:mcu_laptop}
+ \begin{tabular}{llll}
+ \toprule
+ & Laptop & Atmega328P & ESP8266\\
+ \midrule
+ CPU speed & \qtyrange{2}{4}{\giga\hertz} & \qty{16}{\mega\hertz} & \qty{80}{\mega\hertz} or \qty{160}{\mega\hertz}\\
+ \textnumero{} cores & \numrange{4}{8} & 1 & 1\\
+ Storage & \qty{1}{\tebi\byte} & \qty{32}{\kibi\byte} & \qtyrange{0.5}{4}{\mebi\byte}\\
+ \gls{RAM} & \qtyrange{4}{16}{\gibi\byte} & \qty{2}{\kibi\byte} & \qty{160}{\kibi\byte}\\
+ Power & \qtyrange{50}{100}{\watt} & \qtyrange{0.13}{250}{\milli\watt} & \qtyrange{0.1}{350}{\milli\watt}\\
+ Price & \euro{1500} & \euro{3} & \euro{4}\\
+ \bottomrule
+ \end{tabular}
+\end{table}
+
+Each type of microcontrollers comes with vendor-provided drivers, compilers and \glspl{RTS} but there are many platform that abstract away from this such as \gls{MBED} and \gls{ARDUINO} of which \gls{ARDUINO} is specifically designed for education and prototyping and hence used here.
+The popular \gls{ARDUINO} \gls{C}\slash\gls{CPP} dialect and accompanying libraries provide an abstraction layer for common microcontroller behaviour allowing the programmer to program multiple types of microcontrollers using a single language.
+Originally it was designed for the in-house developed open-source hardware with the same name but the setup allows porting to many architectures.
+It provides an \gls{IDE} and toolchain automation to perform all steps of the toolchain with a single command.
+
+\section{\texorpdfstring{\Glsxtrlong{TOP}}{Task-oriented programming}}
+\Gls{TOP} is a programming paradigm that allows multi-tier systems to be generated from a single declarative source.
+\Gls{ITASK} is a general-purpose \gls{TOP} system for programming distributed web applications.
+These distributed web applications often form the core of \gls{IOT} applications as well but integrating these devices in \gls{ITASK} is not straightforward.
+\Gls{ITASK} targets relatively fast but energy-hungry systems with large amounts of \gls{RAM} and a speedy connections.
+Edge devices in \gls{IOT} systems are typically slow but energy efficient and do not have the memory to run the naturally heap-heavy functional programs that \gls{ITASK} results in.
+\Gls{MTASK} bridges this gap by providing a \gls{TOP} \gls{DSL} for \gls{IOT} edge devices that can, because domain-specific knowledge is built in, run on hardware with much less memory and processor speed.
+The following sections compare traditional microcontroller programming with programming the devices using \gls{MTASK}.
+
+\section{Hello world!}
+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 microcontrollers, there usually is no screen for displaying text.
+Nevertheless, almost always there is a built-in monochrome $1\times1$ pixel screen, namely \pgls{LED}.
+The \emph{Hello World!} equivalent on microcontrollers blinks this \gls{LED}.
+
+\Cref{lst:arduinoBlink} shows how the logic of a blink program might look when using \gls{ARDUINO}'s \gls{C}\slash\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 \qty{500}{\ms} so that the blinking is actually visible for the human eye.
+
+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.\ \arduinoinline{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 combinator can be used as this task combinator 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 D2 PMOutput \d2->
+ {main = rpeat (
+ writeD d2 true
+ >>|. delay (lit 500)
+ >>|. writeD d2 false
+ >>|. delay (lit 500)
+ )
+}
+ \end{lstClean}
+ \end{subfigure}
+\end{figure}
+
+\section{Threaded blinking}
+Now say that we want to blink multiple blinking patterns on different \glspl{LED} concurrently.
+For example, blink three \glspl{LED} connected to \gls{GPIO} pins $1,2$ and $3$ at intervals of \qtylist{500;300;800}{\ms}.
+Intuitively you want to lift the blinking behaviour to a function and call this function three times with different parameters as done in \cref{lst:blinkthreadno}
+
+\begin{lstArduino}[caption={Naive approach to multiple blinking patterns.},label={lst:blinkthreadno}]
+void setup () { ... }
+
+void blink (int pin, int wait) {
+ digitalWrite(pin, HIGH);
+ delay(wait);
+ digitalWrite(pin, LOW);
+ delay(wait);
+}
+
+void loop() {
+ blink (D1, 500);
+ blink (D2, 300);
+ blink (D3, 800);
+}\end{lstArduino}
+
+Unfortunately, this does not work because the \arduinoinline{delay} function blocks all further execution.
+The resulting program will blink the \glspl{LED} after each other instead of at the same time.
+To overcome this, it is necessary to slice up the blinking behaviour in very small fragments so it can be manually interleaved \citep{feijs_multi-tasking_2013}.
+Listing~\ref{lst:blinkthread} shows how three different blinking patterns might be achieved in \gls{ARDUINO} using the slicing method.
+If we want the blink function to be a separate parametrizable function we need to explicitly provide all references to the required state.
+Furthermore, the \arduinoinline{delay} function can not be used and polling \arduinoinline{millis} is required.
+The \arduinoinline{millis} function returns the number of milliseconds that have passed since the boot of the microcontroller.
+Some devices use very little energy when in \arduinoinline{delay} or sleep state.
+Resulting in \arduinoinline{millis} potentially affects power consumption since the processor is basically busy looping all the time.
+In the simple case of blinking three \glspl{LED} on fixed intervals, it might be possible to calculate the delays in advance using static analysis and generate the appropriate \arduinoinline{delay} code.
+Unfortunately, this is very hard when for example the blinking patterns are determined at runtime.
+
+\begin{lstArduino}[label={lst:blinkthread},caption={Threading three blinking patterns.}]
+long led1 = 0, led2 = 0, led3 = 0;
+bool st1 = false, st2 = false, st3 = false;
+
+void blink(int pin, int interval, long *lastrun, bool *st) {
+ if (millis() - *lastrun > interval) {
+ digitalWrite(pin, *st = !*st);
+ *lastrun += interval;
+ }
+}
+
+void loop() {
+ blink(D1, 500, &led1, &st1);
+ blink(D2, 300, &led2, &st1);
+ blink(D3, 800, &led3, &st1);
+}\end{lstArduino}
+
+This method is very error prone, requires a lot of pointer juggling and generally results into spaghetti code.
+Furthermore, it is very difficult to represent dependencies between threads, often state machines have to be explicitly programmed by hand to achieve this.
+
+\section{Threaded blinking in \texorpdfstring{\gls{MTASK}}{mTask}}
+The \cleaninline{delay} \emph{task} does not block the execution but \emph{just} emits no value when the target waiting time has not yet passed and emits a stable value when the time is met.
+In contrast, the \arduinoinline{delay()} \emph{function} on the \gls{ARDUINO} is blocking which prohibits interleaving.
+To make code reuse possible and make the implementation more intuitive, the blinking behaviour is lifted to a recursive function instead of using the imperative \cleaninline{rpeat} construct.
+The function is parametrized with the current state, the pin to blink and the waiting time.
+Creating recursive functions like this is not possible in the \gls{ARDUINO} language because the program would run out of stack in an instant and nothing can be interleaved.
+With a parallel combinator, tasks can be executed in an interleaved fashion.
+Therefore, blinking three different blinking patterns is as simple as combining the three calls to the \cleaninline{blink} function with their arguments as seen in \cref{lst:blinkthreadmtask}.
+
+% VimTeX: SynIgnore on
+\begin{lstClean}[label={lst:blinkthreadmtask},caption={Threaded blinking.}]
+blinktask :: MTask v () | mtask v
+blinktask =
+ declarePin D1 PMOutput \d1->
+ declarePin D2 PMOutput \d2->
+ declarePin D3 PMOutput \d3->
+ fun \blink=(\(st, pin, wait)->
+ delay wait
+ >>|. writeD d13 st
+ >>|. blink (Not st, pin, wait))
+ In {main =
+ blink (true, d1, lit 500)
+ .||. blink (true, d2, lit 300)
+ .||. blink (true, d3, lit 800)
+ }
+\end{lstClean}
+% VimTeX: SynIgnore off
+
+\section{Conclusion}
+\todo[inline]{write}
+
+\begin{subappendices}
+\section{History of \texorpdfstring{\gls{MTASK}}{mTask}}
+The development of \gls{MTASK} or its predecessors has been going on for almost seven years now though it really set off during my master's thesis.
+This section provides an exhaustive overview of the work on \gls{MTASK} and its predecessors.
+
+\subsection*{Generating \texorpdfstring{\gls{C}/\gls{CPP}}{C/C++} code}
+A first throw at a class-based shallowly \gls{EDSL} for microcontrollers was made by \citet{plasmeijer_shallow_2016}.
+The language was called \gls{ARDSL} and offered a type safe interface to \gls{ARDUINO} \gls{CPP} dialect.
+A \gls{CPP} code generation backend was available together with an \gls{ITASK} simulation backend.
+There was no support for tasks nor even functions.
+Some time later in the 2015 \gls{CEFP} summer school, an extended version was created that allowed the creation of imperative tasks, local \glspl{SDS} and the usage of functions \citep{koopman_type-safe_2019}.
+The name then changed from \gls{ARDSL} to \gls{MTASK}.
+
+\subsection*{Integration with \texorpdfstring{\gls{ITASK}}{iTask}}
+\Citet{lubbers_task_2017} extended this in his Master's Thesis by adding integration with \gls{ITASK} and a bytecode compiler to the language.
+\Gls{SDS} in \gls{MTASK} could be accessed on the \gls{ITASK} server.
+In this way, entire \gls{IOT} systems could be programmed from a single source.
+However, this version used a simplified version of \gls{MTASK} without functions.
+This was later improved upon by creating a simplified interface where \glspl{SDS} from \gls{ITASK} could be used in \gls{MTASK} and the other way around \citep{lubbers_task_2018}.
+It was shown by \citet{amazonas_cabral_de_andrade_developing_2018} that it was possible to build real-life \gls{IOT} systems with this integration.
+Moreover, a course on the \gls{MTASK} simulator was provided at the 2018 \gls{CEFP}/\gls{3COWS} winter school in Ko\v{s}ice, Slovakia \citep{koopman_simulation_2018}.
+
+\subsection*{Transition to \texorpdfstring{\gls{TOP}}{TOP}}
+The \gls{MTASK} language as it is now was introduced in 2018 \citep{koopman_task-based_2018}.
+This paper updated the language to support functions, simple tasks, and \glspl{SDS} but still compiled to \gls{ARDUINO} \gls{CPP} code.
+Later the byte code compiler and \gls{ITASK} integration was added to the language \citep{lubbers_interpreting_2019}.
+Moreover, it was shown that it is very intuitive to write microcontroller applications in a \gls{TOP} language \citep{lubbers_multitasking_2019}.
+One reason for this is that a lot of design patterns that are difficult using standard means are for free in \gls{TOP} (e.g.\ multithreading).
+In 2019, the \gls{CEFP} summer school in Budapest, Hungary hosted a course on developing \gls{IOT} applications with \gls{MTASK} as well \citep{lubbers_writing_2019}.
+
+\subsection*{\texorpdfstring{\Glsxtrshort{TOP}}{TOP}}
+In 2022, the SusTrainable summer school in Rijeka, Croatia hosted a course on developing greener \gls{IOT} applications using \gls{MTASK} as well \citep{lubbers_green_2022}.
+Several students worked on extending \gls{MTASK} with many useful features:
+\Citet{van_der_veen_mutable_2020} did preliminary work on a green computing analysis, built a simulator, and explored the possibilities for adding bounded datatypes; \citet{de_boer_secure_2020} investigated the possibilities for secure communication channels; \citeauthor{crooijmans_reducing_2021} \citeyearpar{crooijmans_reducing_2021,crooijmans_reducing_2022} added abstractions for low-power operation to \gls{MTASK} such as hardware interrupts and power efficient scheduling; and \citet{antonova_mtask_2022} defined a preliminary formal semantics for a subset of \gls{MTASK}.
+
+\subsection*{\texorpdfstring{\gls{MTASK}}{mTask} in practise}
+Funded by the Radboud-Glasgow Collaboration Fund, collaborative work was executed with Phil Trinder, Jeremy Singer, and Adrian Ravi Kishore Ramsingh.
+An existing smart campus application was developed using \gls{MTASK} and quantitively and qualitatively compared to the original application that was developed using a traditional \gls{IOT} stack \citep{lubbers_tiered_2020}.
+This research was later extended to include a four-way comparison: \gls{PYTHON}, \gls{MICROPYTHON}, \gls{ITASK}, and \gls{MTASK} \citep{lubbers_could_2022}.
+Currently, power efficiency behaviour of traditional versus \gls{TOP} \gls{IOT} stacks is being compared as well adding a \gls{FREERTOS} implementation to the mix as well.
+
+\subsection*{Future}
+Plans for extensions and improvements include exploring integrating \gls{TINYML} into \gls{MTASK}; adding intermittent computing support to \gls{MTASK}; and extending the formal semantics to cover the entirety of the language.
+In 2023, the SusTrainable summer school in Coimbra, Portugal will host a course on \gls{MTASK} as well.
+
+\end{subappendices}
+
+\input{subfilepostamble}
+\end{document}
The edge layer of the \gls{IOT} contains small devices that sense and interact with the world and it is crucial to lower their energy consumption.
While individual devices consume little energy, the sheer number of devices in total amounts to a lot.
-Furthermore, many \gls{IOT} devices operate on batteries and higher energy consumption increases the amount of e-waste as \gls{IOT} edge devices are often hard to reach and consequently hard to replace \citep{NIZETIC2020122877}.
+Furthermore, many \gls{IOT} devices operate on batteries and higher energy consumption increases the amount of e-waste as \gls{IOT} edge devices are often hard to reach and consequently hard to replace \citep{nizetic_internet_2020}.
To reduce the power consumption of an \gls{IOT} device, the specialized low-power sleep modes of the microprocessors can be leveraged.
Different sleep modes achieve different power reductions because of their different run time characteristics.
The system calculates the refresh rates from the current task expression.
This has the advantage that the programmer does not have to deal with them and that they are available in each and every \gls{MTASK} program.
-\subsection{Basic Refresh Rates}
+\subsection{Basic tasks}
We start by assigning default refresh rates to basic tasks.
These refresh rates reflect the expected change rates of sensors and other inputs.
\end{tabular}
\end{table}
-\subsection{Deriving Refresh Rates}\label{sec:deriving_refresh_rates}
+\subsection{Deriving refresh rates}\label{sec:deriving_refresh_rates}
Based on these refresh rates, the system can automatically derive refresh rates for composed \gls{MTASK} expressions using $\mathcal{R}$.
We use the operator $\cap_{\textit{safe}}$ to compose refresh ranges.
When the ranges overlap the result is the overlapping range.
We will briefly discuss the various cases of deriving refresh rates together with the task semantics of the different combinators
-\subsubsection{Parallel Combinators} For the parallel composition of tasks we compute the intersection of the refresh intervals of the components as outlined in the definition of $\cap_{\textit{safe}}$.
+\subsubsection{Parallel combinators} For the parallel composition of tasks we compute the intersection of the refresh intervals of the components as outlined in the definition of $\cap_{\textit{safe}}$.
The operator \cleaninline{.\|\|.} in \cref{R:or} is the \emph{or}-combinator; the first subtask that produces a stable value determines the result of the composition.
The operator \cleaninline{.&&.} in \cref{R:and} is the \emph{and}-operator. The result is the tuple containing both results when both subtasks have a stable value.
The refresh rates of the parallel combinators have no direct relation with their task result.
-\subsubsection{Sequential Combinators}
+\subsubsection{Sequential combinators}
For the sequential composition of tasks we only have to look at the refresh rate of the current task on the left.
The sequential composition operator \cleaninline{>>\|.} in \cref{R:seq} is similar to the monadic sequence operator \cleaninline{>>\|}.
The operator \cleaninline{>>=.} in \cref{R:bind} provides the stable task result to the function on the right-hand side, similar to the monadic bind.
The operator \cleaninline{>>~.} steps on an unstable value and is otherwise equal to \cleaninline{>>=.}.
The step combinator \cleaninline{>>*.} in \cref{R:step} has a list of conditional actions that specify a new task.
-\subsubsection{Repeat Combinators}
+\subsubsection{Repeat combinators}
The repeat combinators repeats their argument indefinitely.
The combinator \cleaninline{rpeatEvery} guarantees the given delay between repetitions.
The refresh rate is equal to the refresh rate of the current argument task.
Only when \cleaninline{rpeatEvery} waits between the iterations of the argument the refresh interval is equal to the remaining delay time.
-\subsubsection{Other Combinators}
+\subsubsection{Other combinators}
The refresh rate of the \cleaninline{delay} in \cref{R:delay} is equal to the remaining delay.
Refreshing stable tasks can be delayed indefinitely, their value never changes.
For other basic tasks, the values from \cref{tbl:refresh} apply.
\end{tabular}
\end{table}
-\subsection{User Defined Refresh Rates}
+\subsection{Tweaking refresh rates}
A tailor-made \gls{ADT} (see \cref{lst:interval}) determines the timing intervals for which the value is determined at runtime but the constructor is known at compile time.
During compilation, the constructor of the \gls{ADT} is checked and code is generated accordingly.
If it is \cleaninline{Default}, no extra code is generated.
\begin{lstClean}[caption={Repeat task combinator with a timing interval.},label={lst:rpeatevery}]
class rpeat v where
- rpeatEvery v :: (TimingInterval v) (MTask v t) -> MTask v t
rpeat :: (MTask v t) -> MTask v t
+ rpeatEvery v :: (TimingInterval v) (MTask v t) -> MTask v t
\end{lstClean}
\Cref{lst:rpeateveryex} shows an example of an \gls{MTASK} task utilising the \cleaninline{rpeatEvery} combinator that would be impossible to create with the regular \cleaninline{rpeat}.
--- /dev/null
+\documentclass[../thesis.tex]{subfiles}
+
+\input{subfilepreamble}
+
+\begin{document}
+\input{subfileprefix}
+
+\chapter{The \texorpdfstring{\gls{MTASK}}{mTask} \texorpdfstring{\glsxtrshort{DSL}}{DSL}}%
+\label{chp:mtask_dsl}
+\begin{chapterabstract}
+This chapter introduces the \gls{MTASK} language more technically by:
+ \begin{itemize}
+ \item introducing the setup of the \gls{EDSL};
+ \item and showing the language interface and examples for:
+ \begin{itemize}
+ \item data types
+ \item expression
+ \item task and their combinators.
+ \end{itemize}
+ \end{itemize}
+\end{chapterabstract}
+
+The \gls{MTASK} system is a complete \gls{TOP} programming environment for programming microcontrollers, i.e.\ it contains a \gls{TOP} language and a \gls{TOP} engine.
+It is implemented as an \gls{EDSL} in \gls{CLEAN} using class-based---or tagless-final---embedding (see \cref{sec:tagless-final_embedding}).
+Due to the nature of the embedding technique, it is possible to have multiple interpretations for programs written in the \gls{MTASK} language.
+The following interpretations are available for \gls{MTASK}.
+
+\begin{description}
+ \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[Byte code compiler]
+
+ The compiler compiles the \gls{MTASK} program at runtime to a specialised byte code.
+ Using a handful of integration functions and tasks, \gls{MTASK} tasks can be executed on microcontrollers 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{description}
+
+When using the compiler interpretation in conjunction with the \gls{ITASK} integration, \gls{MTASK} is a heterogeneous \gls{DSL}.
+I.e.\ some components---e.g.\ the \gls{RTS} on the microcontroller---is largely unaware of the other components in the system, and it is executed on a completely different architecture.
+The \gls{MTASK} language is an enriched simply-typed $\lambda$-calculus with support for some basic types, arithmetic operations, and function definition; and a task language (see \cref{sec:top}).
+
+\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 microcontrollers that may only have \qty{2}{\kibi\byte} 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
+ \caption{Mapping from \gls{CLEAN}/\gls{MTASK} data types to \gls{CPP} datatypes.}%
+ \label{tbl:mtask-c-datatypes}
+ \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}
+\end{table}
+
+\Cref{lst:constraints} contains the definitions for the auxiliary types and type constraints (such as \cleaninline{type} an \cleaninline{basicType}) that are used to construct \gls{MTASK} expressions.
+The \gls{MTASK} language interface consists of a core collection of type classes bundled in the type class \cleaninline{class mtask}.
+Every interpretation implements the type classes in the \cleaninline{mtask} class
+There are also \gls{MTASK} extensions that not every interpretation implements such as peripherals and \gls{ITASK} integration.
+\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
+
+\end{lstClean}
+
+Sensors, \glspl{SDS}, functions, \etc{} may only be defined at the top level.
+The \cleaninline{Main} type is used that is used to distinguish the top level from the main expression.
+Some top level definitions, such as functions, are defined using \gls{HOAS}.
+To make their syntax friendlier, the \cleaninline{In} type---an infix tuple---is used to combine these top level definitions as can be seen in \cleaninline{someTask} (\cref{lst:mtask_types}).
+
+\begin{lstClean}[caption={Example task and auxiliary types in the \gls{MTASK} language.},label={lst:mtask_types}]
+:: Main a = { main :: a }
+:: In a b = (In) infix 0 a b
+
+someTask :: MTask v Int | mtask v & liftsds v & sensor1 v & ...
+someTask =
+ sensor1 config1 \sns1->
+ sensor2 config2 \sns2->
+ sds \s1=initial
+ In liftsds \s2=someiTaskSDS
+ In fun \fun1= ( ... )
+ In fun \fun2= ( ... )
+ In { main = mainexpr }
+\end{lstClean}
+
+\section{Expressions}\label{sec: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}); perform number and boolean arithmetics; do comparisons; and conditional execution.
+For every common boolean and 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
+ ...
+ (&.) 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
+ ...
+ 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} that will convert the argument to the respective type similar to casting in \gls{C}.
+
+\begin{lstClean}[caption={Type conversion functions in \gls{MTASK}.}]
+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}
+
+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 such as \cleaninline{true :== lit True}, \cleaninline{false :== lit False}, \etc.
+
+\Cref{lst:example_exprs} shows some examples of these expressions.
+Since they are only expressions, there is no need for a \cleaninline{Main}.
+\cleaninline{e0} defines the literal $42$, \cleaninline{e1} calculates the literal $42.0$ using real numbers.
+\cleaninline{e2} compares \cleaninline{e0} and \cleaninline{e1} as integers and if they are equal it returns the \cleaninline{e2}$/2$ and \cleaninline{e0} otherwise.
+
+\begin{lstClean}[label={lst:example_exprs},caption={Example \gls{MTASK} expressions.}]
+e0 :: v Int | expr v
+e0 = lit 42
+
+e1 :: v Real | expr v
+e1 = lit 38.0 + real (lit 4)
+
+e2 :: v Int | expr v
+e2 = if' (e0 ==. int e1)
+ (int e1 /. lit 2) e0
+\end{lstClean}
+
+\Gls{MTASK} is shallowly embedded in \gls{CLEAN} and the terms are constructed at runtime.
+This means that \gls{MTASK} programs can also be tailor-made at runtime or constructed using \gls{CLEAN} functions maximising the linguistic reuse \citep{krishnamurthi_linguistic_2001}
+\cleaninline{approxEqual} in \cref{lst:example_macro} performs an approximate equality---albeit not taking into account all floating point pecularities---.
+When calling \cleaninline{approxEqual} in an \gls{MTASK} function, the resulting code is inlined.
+
+\begin{lstClean}[label={lst:example_macro},caption={Example linguistic reuse in the \gls{MTASK} language.}]
+approxEqual :: (v Real) (v Real) (v Real) -> v Real | expr v
+approxEqual x y eps = if' (x ==. y) true
+ ( if' (x >. y)
+ (y -. x < eps)
+ (x -. y < eps)
+ )
+\end{lstClean}
+
+\subsection{Data types}
+Most of \gls{CLEAN}'s basic types have been mapped on \gls{MTASK} types.
+However, it can be useful to have access to compound types as well.
+All types in \gls{MTASK} must have a fixed size representation on the stack so sum types are not (yet) supported.
+While it is possible to lift types using the \cleaninline{lit} function, you cannot do anything with the types besides passing them around but they are being produced by some parallel task combinators (see \cref{sssec:combinators_parallel}).
+To be able to use types as first class citizens, constructors and field selectors are required (see \cref{chp:first-class_datatypes}).
+\Cref{lst:tuple_exprs} shows the scaffolding for supporting tuples in \gls{MTASK}.
+Besides the constructors and field selectors, there is also a helper function available that transforms a function from a tuple of \gls{MTASK} expressions to an \gls{MTASK} expression of a tuple.
+Examples for using tuple can be found in \cref{sec:mtask_functions}.
+
+\begin{lstClean}[label={lst:tuple_exprs},caption={Tuple constructor and field selectors in \gls{MTASK}.}]
+class tupl v where
+ tupl :: (v a) (v b) -> v (a, b) | type a & type b
+ first :: (v (a, b)) -> v a | type a & type b
+ second :: (v (a, b)) -> v b | type a & type b
+
+ tupopen f :== \v->f (first v, second v)
+\end{lstClean}
+
+\subsection{Functions}\label{sec:mtask_functions}
+Adding functions to the language is achieved by type class to the \gls{DSL}.
+By using \gls{HOAS}, both the function definition and the calls to the function can be controlled by the \gls{DSL} \citep{pfenning_higher-order_1988,chlipala_parametric_2008}.
+The \gls{MTASK} only allows first-order functions and does not allow partial function application.
+This is restricted by using a multi-parameter type class where the first parameter represents the arguments and the second parameter the view.
+By providing a single instance per function arity instead of providing one instance for all functions and using tuples for the arguments this constraint can be enforced.
+Also, \gls{MTASK} only supports top-level functions which is enforced by the \cleaninline{Main} box.
+The definition of the type class and the instances for an example interpretation (\cleaninline{:: Inter}) are as follows:
+
+\begin{lstClean}[caption={Functions in \gls{MTASK}.}]
+class fun a v :: ((a -> v s) -> In (a -> v s) (Main (MTask v u)))
+ -> Main (MTask v u)
+
+instance fun () Inter where ...
+instance fun (Inter a) Inter | type a where ...
+instance fun (Inter a, Inter b) Inter | type a, type b where ...
+instance fun (Inter a, Inter b, Inter c) Inter | type a, ... where ...
+...
+\end{lstClean}
+
+Deriving how to define and use functions from the type is quite the challenge even though the resulting syntax is made easier using the infix type \cleaninline{In}.
+\Cref{lst:function_examples} show the factorial function, a tail-call optimised factorial function and a function with zero arguments to demonstrate the syntax.
+Splitting out the function definition for each single arity means that that for every function arity and combination of arguments, a separate class constraint must be created.
+Many of the often used functions are already bundled in the \cleaninline{mtask} class constraint collection.
+\cleaninline{factorialtail} shows a manually added class constraint.
+Definiting zero arity functions is shown in the \cleaninline{zeroarity} expression.
+Finally, \cleaninline{swapTuple} shows an example of a tuple being swapped.
+
+% VimTeX: SynIgnore on
+\begin{lstClean}[label={lst:function_examples},caption={Function examples in \gls{MTASK}.}]
+factorial :: Main (v Int) | mtask v
+factorial =
+ fun \fac=(\i->if' (i <. lit 1)
+ (lit 1)
+ (i *. fac (i -. lit 1)))
+ In {main = fac (lit 5) }
+
+factorialtail :: Main (v Int) | mtask v & fun (v Int, v Int) v
+factorialtail =
+ fun \facacc=(\(acc, i)->if' (i <. lit 1)
+ acc
+ (fac (acc *. i, i -. lit 1)))
+ In fun \fac=(\i->facacc (lit 1, i))
+ In {main = fac (lit 5) }
+
+zeroarity :: Main (v Int) | mtask v
+zeroarity =
+ fun \fourtytwo=(\()->lit 42)
+ In fun \add=(\(x, y)->x +. y)
+ In {main = add (fourtytwo (), lit 9)}
+
+swapTuple :: Main (v (Int, Bool)) | mtask v
+swapTuple =
+ fun \swap=(tupopen \(x, y)->tupl y x)
+ In {main = swap (tupl true (lit 42)) }
+\end{lstClean}
+% VimTeX: SynIgnore off
+
+\section{Tasks and task combinators}\label{sec:top}
+\Gls{MTASK}'s task language can be divided into three categories, namely
+\begin{enumerate*}
+ \item Basic tasks, in most \gls{TOP} systems, the basic tasks are called editors, modelling the interactivity with the user.
+ In \gls{MTASK}, there are no \emph{editors} in that sense but there is interaction with the outside world through microcontroller peripherals such as sensors and actuators.
+ \item Task combinators provide a way of describing the workflow.
+ They combine one or more tasks into a compound task.
+ \item \glspl{SDS} in \gls{MTASK} can be seen as references to data that can be shared using many-to-many communication and are only accessible from within the task language to ensure atomicity.
+\end{enumerate*}
+
+As \gls{MTASK} is integrated with \gls{ITASK}, the same stability distinction is made for task values.
+A task in \gls{MTASK} is denoted by the \gls{DSL} type synonym shown in \cref{lst:task_type}.
+
+\begin{lstClean}[label={lst:task_type},caption={Task type in \gls{MTASK}.}]
+:: MTask v a :== v (TaskValue a)
+:: TaskValue a
+ = NoValue
+ | Value a Bool
+\end{lstClean}
+
+\subsection{Basic tasks}
+The most rudimentary basic tasks are the \cleaninline{rtrn} and \cleaninline{unstable} tasks.
+They lift the value from the \gls{MTASK} expression language to the task domain either as a stable value or an unstable value.
+There is also a special type of basic task for delaying execution.
+The \cleaninline{delay} task---given a number of milliseconds---yields an unstable value while the time has not passed.
+Once the specified time has passed, the time it overshot the planned time is yielded as a stable task value.
+See \cref{sec:repeat} for an example task using \cleaninline{delay}.
+
+\begin{lstClean}[label={lst:basic_tasks},caption={Function examples in \gls{MTASK}.}]
+class rtrn v :: (v t) -> MTask v t
+class unstable v :: (v t) -> MTask v t
+class delay v :: (v n) -> MTask v n | long v n
+\end{lstClean}
+
+\subsubsection{Peripherals}\label{sssec:peripherals}
+For every sensor or actuator, basic tasks are available that allow interaction with the specific peripheral.
+The type classes for these tasks are not included in the \cleaninline{mtask} class collection as not all devices nor all language interpretations have such peripherals connected.
+%\todo{Historically, peripheral support has been added \emph{by need}.}
+
+\Cref{lst:dht,lst:gpio} show the type classes for \glspl{DHT} sensors and \gls{GPIO} access.
+Other peripherals have similar interfaces, they are available in the \cref{sec:aux_peripherals}.
+For the \gls{DHT} sensor there are two basic tasks, \cleaninline{temperature} and \cleaninline{humidity}, that---will given a \cleaninline{DHT} object---produce a task that yields the observed temperature in \unit{\celcius} or relative humidity as a percentage as an unstable value.
+Currently, two different types of \gls{DHT} sensors are supported, the \emph{DHT} family of sensors connect through $1$-wire protocol and the \emph{SHT} family of sensors connected using \gls{I2C} protocol.
+Creating such a \cleaninline{DHT} object is very similar to creating functions in \gls{MTASK} and uses \gls{HOAS} to make it type safe.
+
+\begin{lstClean}[label={lst:dht},caption{The \gls{MTASK} interface for \glspl{DHT} sensors.}]
+:: DHT //abstract
+:: DHTInfo
+ = DHT_DHT Pin DHTtype
+ | DHT_SHT I2CAddr
+:: DHTtype = DHT11 | DHT21 | DHT22
+class dht v where
+ DHT :: DHTInfo ((v DHT) -> Main (v b)) -> Main (v b) | type b
+ temperature :: (v DHT) -> MTask v Real
+ humidity :: (v DHT) -> MTask v Real
+
+measureTemp :: Main (MTask v Real) | mtask v & dht v
+measureTemp = DHT (DHT_SHT (i2c 0x36)) \dht->
+ {main=temperature dht}
+\end{lstClean}
+
+\Gls{GPIO} access is divided into three classes: analog, digital and pin modes.
+For all pins and pin modes an \gls{ADT} is available that enumerates the pins.
+The analog \gls{GPIO} pins of a microcontroller are connected to an \gls{ADC} that translates the voltage to an integer.
+Analog \gls{GPIO} pins can be either read or written to.
+Digital \gls{GPIO} pins only report a high or a low value.
+The type class definition is a bit more complex since analog \gls{GPIO} pins can be used as digital \gls{GPIO} pins as well.
+Therefore, if the \cleaninline{p} type implements the \cleaninline{pin} class---i.e.\ either \cleaninline{APin} or \cleaninline{DPin}---the \cleaninline{dio} class can be used.
+\Gls{GPIO} pins usually operate according to a certain pin mode that states whether the pin acts as an input pin, an input with an internal pull-up resistor or an output pin.
+This setting can be applied using the \cleaninline{pinMode} class by hand or by using the \cleaninline{declarePin} \gls{GPIO} pin constructor.
+Setting the pin mode is a task that immediately finisheds and fields a stable unit value.
+Writing to a pin is also a task that immediately finishes but yields the written value instead.
+Reading a pin is a task that yields an unstable value---i.e.\ the value read from the actual pin.
+
+\begin{lstClean}[label={lst:gpio},caption={The \gls{MTASK} interface for \gls{GPIO} access.}]
+:: APin = A0 | A1 | A2 | A3 | A4 | A5
+:: DPin = D0 | D1 | D2 | D3 | D4 | D5 | D6 | D7 | D8 | D9 | D10 | D11 | D12 | D13
+:: PinMode = PMInput | PMOutput | PMInputPullup
+:: Pin = AnalogPin APin | DigitalPin DPin
+class pin p :: p -> Pin
+
+class aio v where
+ writeA :: (v APin) (v Int) -> MTask v Int
+ readA :: (v APin) -> MTask v Int
+
+class dio p v | pin p where
+ writeD :: (v p) (v Bool) -> MTask v Bool
+ readD :: (v p) -> MTask v Bool | pin p
+
+class pinMode v where
+ pinMode :: (v PinMode) (v p) -> MTask v () | pin p
+ declarePin :: p PinMode ((v p) -> Main (v a)) -> Main (v a) | pin p
+\end{lstClean}
+
+\begin{lstClean}[label={lst:gpio_examples},caption={\Gls{GPIO} example in \gls{MTASK}.}]
+task1 :: MTask v Int | mtask v
+task1 = declarePin A3 PMInput \a3->{main=readA a3}
+
+task2 :: MTask v Int | mtask v
+task2 = declarePin D3 PMOutput \d3->{main=writeD d3 true}
+\end{lstClean}
+
+\subsection{Task combinators}
+Task combinators are used to combine multiple tasks into one to describe workflows.
+There are three main types of task combinators, namely:
+\begin{enumerate*}
+ \item Sequential combinators that execute tasks one after the other, possibly using the result of the left hand side.
+ \item Parallel combinators that execute tasks at the same time combining the result.
+ \item Miscellaneous combinators that change the semantics of a task---e.g.\ repeat it or delay execution.
+\end{enumerate*}
+
+\subsubsection{Sequential}
+Sequential task combination allows the right-hand side task to observe the left-hand side task value.
+All seqential task combinators are expressed in the \cleaninline{expr} class and can be---and are by default---derived from the Swiss army knife step combinator \cleaninline{>>*.}.
+This combinator has a single task on the left-hand side and a list of \emph{task continuations} on the right-hand side.
+The list of task continuations is checked every rewrite step and if one of the predicates matches, the task continues with the result of this combination.
+\cleaninline{>>=.} is a shorthand for the bind operation, if the left-hand side is stable, the right-hand side function is called to produce a new task.
+\cleaninline{>>|.} is a shorthand for the sequence operation, if the left-hand side is stable, it continues with the right-hand side task.
+The \cleaninline{>>~.} and \cleaninline{>>..} combinators are variants of the ones above that ignore the stability and continue on an unstable value as well.
+
+\begin{lstClean}[label={lst:mtask_sequential},caption={Sequential task combinators in \gls{MTASK}.}]
+class step v | expr v where
+ (>>*.) infixl 1 :: (MTask v t) [Step v t u] -> MTask v u
+ (>>=.) infixl 0 :: (MTask v t) ((v t) -> MTask v u) -> MTask v u
+ (>>|.) infixl 0 :: (MTask v t) (MTask v u) -> MTask v u
+ (>>~.) infixl 0 :: (MTask v t) ((v t) -> MTask v u) -> MTask v u
+ (>>..) infixl 0 :: (MTask v t) (MTask v u) -> MTask v u
+
+:: Step v t u
+ = IfValue ((v t) -> v Bool) ((v t) -> MTask v u)
+ | IfStable ((v t) -> v Bool) ((v t) -> MTask v u)
+ | IfUnstable ((v t) -> v Bool) ((v t) -> MTask v u)
+ | Always (MTask v u)
+\end{lstClean}
+
+\todo{more examples step?}
+
+The following listing shows an example of a step in action.
+The \cleaninline{readPinBin} function produces an \gls{MTASK} task that classifies the value of an analogue pin into four bins.
+It also shows that the nature of embedding allows the host language to be used as a macro language.
+Furthermore
+
+\begin{lstClean}[label={lst:mtask_readpinbin},caption={Read an analog pin and bin the value in \gls{MTASK}.}]
+readPinBin :: Int -> Main (MTask v Int) | mtask v
+readPinBin lim = declarePin PMInput A2 \a2->
+ { main = readA a2 >>*.
+ [ IfValue (\x->x <. lim) (\_->rtrn (lit bin))
+ \\ lim <-[64,128,192,256]
+ & bin <- [0..]]}
+\end{lstClean}
+
+\subsubsection{Parallel}\label{sssec:combinators_parallel}
+The result of a parallel task combination is a compound that actually executes the tasks at the same time.
+
+There are two types of parallel task combinators (see \cref{lst:mtask_parallel}).
+The conjunction combinator (\cleaninline{.&&.}) combines the result by putting the values from both sides in a tuple.
+The stability of the task depends on the stability of both children.
+If both children are stable, the result is stable, otherwise the result is unstable.
+The disjunction combinator (\cleaninline{.\|\|.}) combines the results by picking the leftmost, most stable task.
+The semantics are easily described using \gls{CLEAN} functions shown in \cref{lst:semantics_con,lst:semantics_dis}.
+
+\begin{figure}[ht]
+ \centering
+ \begin{subfigure}[t]{.5\textwidth}
+ \begin{lstClean}[caption={Semantics of the\\conjunction combinator.},label={lst:semantics_con}]
+con :: (TaskValue a) (TaskValue b)
+ -> TaskValue (a, b)
+con NoValue r = NoValue
+con l NoValue = NoValue
+con (Value l ls) (Value r rs)
+ = Value (l, r) (ls && rs)
+
+ \end{lstClean}
+ \end{subfigure}%
+ \begin{subfigure}[t]{.5\textwidth}
+ \begin{lstClean}[caption={Semantics of the\\disjunction combinator.},label={lst:semantics_dis}]
+dis :: (TaskValue a) (TaskValue a)
+ -> TaskValue a
+dis NoValue r = r
+dis l NoValue = l
+dis (Value l ls) (Value r rs)
+ | rs = Value r True
+ | otherwise = Value l ls
+ \end{lstClean}
+ \end{subfigure}
+\end{figure}
+
+\begin{lstClean}[label={lst:mtask_parallel},caption={Parallel task combinators in \gls{MTASK}.}]
+class (.&&.) infixr 4 v :: (MTask v a) (MTask v b) -> MTask v (a, b)
+class (.||.) infixr 3 v :: (MTask v a) (MTask v a) -> MTask v a
+\end{lstClean}
+
+\Cref{lst:mtask_parallel_example} gives an example of the parallel task combinator.
+This program will read two pins at the same time, returning when one of the pins becomes \arduinoinline{HIGH}.
+If the combinator was the \cleaninline{.&&.} instead, the type would be \cleaninline{MTask v (Bool, Bool)} and the task would only return when both pins have been \arduinoinline{HIGH} but not necessarily at the same time.
+
+\begin{lstClean}[label={lst:mtask_parallel_example},caption={Parallel task combinator example in \gls{MTASK}.}]
+task :: MTask v Bool
+task =
+ declarePin D0 PMInput \d0->
+ declarePin D1 PMInput \d1->
+ let monitor pin = readD pin >>*. [IfValue (\x->x) \x->rtrn x]
+ In {main = monitor d0 .||. monitor d1}
+\end{lstClean}
+
+\subsubsection{Repeat}\label{sec:repeat}
+The \cleaninline{rpeat} combinator executes the child task.
+If a stable value is observed, the task is reinstated.
+The functionality of \cleaninline{rpeat} can also be simulated by using functions and sequential task combinators and even made to be stateful as can be seen in \cref{lst:blinkthreadmtask}.
+
+\begin{lstClean}[label={lst:mtask_repeat},caption={Repeat task combinators in \gls{MTASK}.}]
+class rpeat v where
+ rpeat :: (MTask v a) -> MTask v a
+\end{lstClean}
+
+To demonstrate the combinator, \cref{lst:mtask_repeat_example} show \cleaninline{rpeat} in use.
+This task will mirror the value read from analog \gls{GPIO} pin \cleaninline{A1} to pin \cleaninline{A2} by constantly reading the pin and writing the result.
+
+\begin{lstClean}[label={lst:mtask_repeat_example},caption={Exemplatory repeat task in \gls{MTASK}.}]
+task :: MTask v Int | mtask v
+task =
+ declarePin A1 PMInput \a1->
+ declarePin A2 PMOutput \a2->
+ {main = rpeat (readA a1 >>~. writeA a2 >>|. delay (lit 1000))}
+\end{lstClean}
+
+\subsection{\texorpdfstring{\Glsxtrlongpl{SDS}}{Shared data sources}}
+\Glspl{SDS} in \gls{MTASK} are by default references to shared memory but can also be references to \glspl{SDS} in \gls{ITASK} (see \cref{sec:liftsds}).
+Similar to peripherals (see \cref{sssec:peripherals}), they are constructed at the top level and are accessed through interaction tasks.
+The \cleaninline{getSds} task yields the current value of the \gls{SDS} as an unstable value.
+This behaviour is similar to the \cleaninline{watch} task in \gls{ITASK}.
+Writing a new value to \pgls{SDS} is done using \cleaninline{setSds}.
+This task yields the written value as a stable result after it is done writing.
+Getting and immediately after setting \pgls{SDS} is not necessarily an \emph{atomic} operation in \gls{MTASK} because it is possible that another task accesses the \gls{SDS} in between.
+To circumvent this issue, \cleaninline{updSds} is created, this task atomically updates the value of the \gls{SDS}.
+The \cleaninline{updSds} task only guarantees atomicity within \gls{MTASK}.
+
+\begin{lstClean}[label={lst:mtask_sds},caption={\Glspl{SDS} in \gls{MTASK}.}]
+:: Sds a // abstract
+class sds v where
+ sds :: ((v (Sds t)) -> In t (Main (MTask v u))) -> Main (MTask v u)
+ getSds :: (v (Sds t)) -> MTask v t
+ setSds :: (v (Sds t)) (v t) -> MTask v t
+ updSds :: (v (Sds t)) ((v t) -> v t) -> MTask v t
+\end{lstClean}
+
+\Cref{lst:mtask_sds_examples} shows an example using \glspl{SDS}.
+The \cleaninline{count} function takes a pin and returns a task that counts the number of times the pin is observed as high by incrementing the \cleaninline{share} \gls{SDS}.
+In the \cleaninline{main} expression, this function is called twice and the results are combined using the parallel or combinator (\cleaninline{.||.}).
+Using a sequence of \cleaninline{getSds} and \cleaninline{setSds} would be unsafe here because the other branch might write their old increment value immediately after writing, effectively missing a count.\todo{beter opschrijven}
+
+\begin{lstClean}[label={lst:mtask_sds_examples},caption={Examples with \glspl{SDS} in \gls{MTASK}.}]
+task :: MTask v Int | mtask v
+task = declarePin D3 PMInput \d3->
+ declarePin D5 PMInput \d5->
+ sds \share=0
+ In fun \count=(\pin->
+ readD pin
+ >>* [IfValue (\x->x) (\_->updSds (\x->x +. lit 1) share)]
+ >>| delay (lit 100) // debounce
+ >>| count pin)
+ In {main=count d3 .||. count d5}
+\end{lstClean}
+
+\section{Conclusion}
+\Gls{MTASK} is a rich \gls{TOP} language tailored for \gls{IOT} systems.
+It is embedded in the pure functional language \gls{CLEAN} and uses an enriched lambda calculus as a host language.
+It provides support for all common arithmetic expressions, conditionals, functions, but also several basic tasks, task combinators, peripheral support and integration with \gls{ITASK}.
+By embedding domain-specific knowledge in the language itself, it achieves the same abstraction level and dynamicity as other \gls{TOP} languages while targetting tiny computers instead.
+As a result, a single declarative specification can describe an entire \gls{IOT} system.
+
+\input{subfilepostamble}
+\end{document}
\begin{document}
\input{subfileprefix}
-\chapter{Edge device programming}%
-\label{chp:top4iot}
-\begin{chapterabstract}
- This chapter:
- \begin{itemize}
- \item shows how to create the \emph{Hello World!} application for microcontrollers using \gls{ARDUINO};
- \item extends this idea with multithreading, demonstrating the difficulty programming multi-tasking applications;
- \item describes a comparative variant in \gls{MTASK} and shows that upgrading to a multi-tasking variant is straightforward
- \item demonstrates that the complexity of running multiple tasks;
- \item and concludes with the history of \gls{MTASK}'s development.
- \end{itemize}
-\end{chapterabstract}
-
-The edge layer of \gls{IOT} system mostly consists of microcontrollers.
-Microcontrollers are tiny computers designed specifically for embedded applications.
-They therefore only have a soup\c{c}on of memory, have a slow processor, come with many energy efficient sleep modes and have a lot of peripheral support such as \gls{GPIO} pins.
-Usually, programming microcontrollers requires an elaborate multi-step toolchain of compilation, linkage, binary image creation, and burning this image onto the flash memory of the microcontroller in order to compile and run a program.
-The programs are usually cyclic executives instead of tasks running in an operating system, i.e.\ there is only a single task that continuously runs on the bare metal.
-\Cref{tbl:mcu_laptop} compares the hardware properties of a typical laptop with two very popular microcontrollers.
-
-\begin{table}
- \caption{Hardware characteristics of typical microcontrollers and laptops.}%
- \label{tbl:mcu_laptop}
- \begin{tabular}{llll}
- \toprule
- & Laptop & Atmega328P & ESP8266\\
- \midrule
- CPU speed & \qtyrange{2}{4}{\giga\hertz} & \qty{16}{\mega\hertz} & \qty{80}{\mega\hertz} or \qty{160}{\mega\hertz}\\
- \textnumero{} cores & \numrange{4}{8} & 1 & 1\\
- Storage & \qty{1}{\tebi\byte} & \qty{32}{\kibi\byte} & \qtyrange{0.5}{4}{\mebi\byte}\\
- \gls{RAM} & \qtyrange{4}{16}{\gibi\byte} & \qty{2}{\kibi\byte} & \qty{160}{\kibi\byte}\\
- Power & \qtyrange{50}{100}{\watt} & \qtyrange{0.13}{250}{\milli\watt} & \qtyrange{0.1}{350}{\milli\watt}\\
- Price & \euro{1500} & \euro{3} & \euro{4}\\
- \bottomrule
- \end{tabular}
-\end{table}
-
-Each type of microcontrollers comes with vendor-provided drivers, compilers and \glspl{RTS} but there are many platform that abstract away from this such as \gls{MBED} and \gls{ARDUINO} of which \gls{ARDUINO} is specifically designed for education and prototyping and hence used here.
-The popular \gls{ARDUINO} \gls{C}\slash\gls{CPP} dialect and accompanying libraries provide an abstraction layer for common microcontroller behaviour allowing the programmer to program multiple types of microcontrollers using a single language.
-Originally it was designed for the in-house developed open-source hardware with the same name but the setup allows porting to many architectures.
-It provides an \gls{IDE} and toolchain automation to perform all steps of the toolchain with a single command.
-
-\section{Hello world!}
-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 microcontrollers, there usually is no screen for displaying text.
-Nevertheless, almost always there is a built-in monochrome $1\times1$ pixel screen, namely \pgls{LED}.
-The \emph{Hello World!} equivalent on microcontrollers blinks this \gls{LED}.
-
-\Cref{lst:arduinoBlink} shows how the logic of a blink program might look when using \gls{ARDUINO}'s \gls{C}\slash\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 \qty{500}{\ms} so that the blinking is actually visible for the human eye.
-
-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.\ \arduinoinline{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 combinator can be used as this task combinator 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 D2 PMOutput \d2->
- {main = rpeat (
- writeD d2 true
- >>|. delay (lit 500)
- >>|. writeD d2 false
- >>|. delay (lit 500)
- )
-}
- \end{lstClean}
- \end{subfigure}
-\end{figure}
-
-\section{Threaded blinking}
-Now say that we want to blink multiple blinking patterns on different \glspl{LED} concurrently.
-For example, blink three \glspl{LED} connected to \gls{GPIO} pins $1,2$ and $3$ at intervals of \qtylist{500;300;800}{\ms}.
-Intuitively you want to lift the blinking behaviour to a function and call this function three times with different parameters as done in \cref{lst:blinkthreadno}
-
-\begin{lstArduino}[caption={Naive approach to multiple blinking patterns.},label={lst:blinkthreadno}]
-void setup () { ... }
-
-void blink (int pin, int wait) {
- digitalWrite(pin, HIGH);
- delay(wait);
- digitalWrite(pin, LOW);
- delay(wait);
-}
-
-void loop() {
- blink (D1, 500);
- blink (D2, 300);
- blink (D3, 800);
-}\end{lstArduino}
-
-Unfortunately, this does not work because the \arduinoinline{delay} function blocks all further execution.
-The resulting program will blink the \glspl{LED} after each other instead of at the same time.
-To overcome this, it is necessary to slice up the blinking behaviour in very small fragments so it can be manually interleaved \citep{feijs_multi-tasking_2013}.
-Listing~\ref{lst:blinkthread} shows how three different blinking patterns might be achieved in \gls{ARDUINO} using the slicing method.
-If we want the blink function to be a separate parametrizable function we need to explicitly provide all references to the required state.
-Furthermore, the \arduinoinline{delay} function can not be used and polling \arduinoinline{millis} is required.
-The \arduinoinline{millis} function returns the number of milliseconds that have passed since the boot of the microcontroller.
-Some devices use very little energy when in \arduinoinline{delay} or sleep state.
-Resulting in \arduinoinline{millis} potentially affects power consumption since the processor is basically busy looping all the time.
-In the simple case of blinking three \glspl{LED} on fixed intervals, it might be possible to calculate the delays in advance using static analysis and generate the appropriate \arduinoinline{delay} code.
-Unfortunately, this is very hard when for example the blinking patterns are determined at runtime.
-
-\begin{lstArduino}[label={lst:blinkthread},caption={Threading three blinking patterns.}]
-long led1 = 0, led2 = 0, led3 = 0;
-bool st1 = false, st2 = false, st3 = false;
-
-void blink(int pin, int dlay, long *lastrun, bool *st) {
- if (millis() - *lastrun > dlay) {
- digitalWrite(pin, *st = !*st);
- *lastrun += dlay;
- }
-}
-
-void loop() {
- blink(D1, 500, &led1, &st1);
- blink(D2, 300, &led2, &st1);
- blink(D3, 800, &led3, &st1);
-}\end{lstArduino}
-
-This method is very error prone, requires a lot of pointer juggling and generally results into spaghetti code.
-Furthermore, it is very difficult to represent dependencies between threads, often state machines have to be explicitly programmed by hand to achieve this.
-
-\section{Blinking in \texorpdfstring{\gls{MTASK}}{mTask}}
-The \cleaninline{delay} \emph{task} does not block the execution but \emph{just} emits no value when the target waiting time has not yet passed and emits a stable value when the time is met.
-In contrast, the \arduinoinline{delay()} \emph{function} on the \gls{ARDUINO} is blocking which prohibits interleaving.
-To make code reuse possible and make the implementation more intuitive, the blinking behaviour is lifted to a recursive function instead of using the imperative \cleaninline{rpeat} construct.
-The function is parametrized with the current state, the pin to blink and the waiting time.
-Creating recursive functions like this is not possible in the \gls{ARDUINO} language because the program would run out of stack in an instant and nothing can be interleaved.
-With a parallel combinator, tasks can be executed in an interleaved fashion.
-Therefore, blinking three different blinking patterns is as simple as combining the three calls to the \cleaninline{blink} function with their arguments as seen in \cref{lst:blinkthreadmtask}.
-
-% VimTeX: SynIgnore on
-\begin{lstClean}[label={lst:blinkthreadmtask},caption={Threaded blinking.}]
-blinktask :: MTask v () | mtask v
-blinktask =
- declarePin D1 PMOutput \d1->
- declarePin D2 PMOutput \d2->
- declarePin D3 PMOutput \d3->
- fun \blink=(\(st, pin, wait)->
- delay wait
- >>|. writeD d13 st
- >>|. blink (Not st, pin, wait)) In
- {main = blink (true, d1, lit 500)
- .||. blink (true, d2, lit 300)
- .||. blink (true, d3, lit 800)
- }\end{lstClean}
-% VimTeX: SynIgnore off
-
-\section{\texorpdfstring{\Gls{MTASK}}{MTask} history}
-\subsection{Generating \texorpdfstring{\gls{C}/\gls{CPP}}{C/C++} code}
-A first throw at a class-based shallowly \gls{EDSL} for microcontrollers was made by \citet{plasmeijer_shallow_2016}.
-The language was called \gls{ARDSL} and offered a type safe interface to \gls{ARDUINO} \gls{CPP} dialect.
-A \gls{CPP} code generation backend was available together with an \gls{ITASK} simulation backend.
-There was no support for tasks or even functions.
-Some time later in the 2015 \gls{CEFP} summer school, an extended version was created that allowed the creation of imperative tasks, \glspl{SDS} and the usage of functions \citep{koopman_type-safe_2019}.
-The name then changed from \gls{ARDSL} to \gls{MTASK}.
-
-\subsection{Integration with \texorpdfstring{\gls{ITASK}}{iTask}}
-\Citet{lubbers_task_2017} extended this in his Master's Thesis by adding integration with \gls{ITASK} and a bytecode compiler to the language.
-\Gls{SDS} in \gls{MTASK} could be accessed on the \gls{ITASK} server.
-In this way, entire \gls{IOT} systems could be programmed from a single source.
-However, this version used a simplified version of \gls{MTASK} without functions.
-This was later improved upon by creating a simplified interface where \glspl{SDS} from \gls{ITASK} could be used in \gls{MTASK} and the other way around \citep{lubbers_task_2018}.
-It was shown by \citet{amazonas_cabral_de_andrade_developing_2018} that it was possible to build real-life \gls{IOT} systems with this integration.
-Moreover, a course on the \gls{MTASK} simulator was provided at the 2018 \gls{CEFP}/\gls{3COWS} winter school in Ko\v{s}ice, Slovakia \citep{koopman_simulation_2018}.
-
-\section{Transition to \texorpdfstring{\gls{TOP}}{TOP}}
-The \gls{MTASK} language as it is now was introduced in 2018 \citep{koopman_task-based_2018}.
-This paper updated the language to support functions, tasks and \glspl{SDS} but still compiled to \gls{CPP} \gls{ARDUINO} code.
-Later the bytecode compiler and \gls{ITASK} integration was added to the language \citep{lubbers_interpreting_2019}.
-Moreover, it was shown that it is very intuitive to write microcontroller applications in a \gls{TOP} language \citep{lubbers_multitasking_2019}.
-One reason for this is that a lot of design patterns that are difficult using standard means are for free in \gls{TOP} (e.g.\ multithreading).
-In 2019, the \gls{CEFP} summer school in Budapest, Hungary hosted a course on developing \gls{IOT} applications with \gls{MTASK} as well \citep{lubbers_writing_2019}.
-
-\subsection{\texorpdfstring{\Glsxtrshort{TOP}}{TOP}}
-In 2022, the SusTrainable summer school in Rijeka, Croatia hosted a course on developing greener \gls{IOT} applications using \gls{MTASK} as well (the lecture notes are to be written).
-Several students worked on extending \gls{MTASK} with many useful features:
-\Citet{veen_van_der_mutable_2020} did preliminary work on a green computer analysis, built a simulator and explored the possibilities for adding bounded datatypes; \citet{boer_de_secure_2020} investigated the possibilities for secure communication channels; and \citet{crooijmans_reducing_2021} added abstractions for low-power operation to \gls{MTASK} such as hardware interrupts and power efficient scheduling (resulting in a paper as well \citet{crooijmans_reducing_2022}).
-\Citet{antonova_mtask_2022} defined a preliminary formal semantics for a subset of \gls{MTASK}.
-Moreover, plans for student projects and improvements include exploring integrating \gls{TINYML} into \gls{MTASK}; and adding intermittent computing support to \gls{MTASK}.
-
-In 2023, the SusTrainable summer school in Coimbra, Portugal will host a course on \gls{MTASK} as well.
-
-\subsection{\texorpdfstring{\gls{MTASK}}{mTask} in practise}
-Funded by the Radboud-Glasgow Collaboration Fund, collaborative work was executed with Phil Trinder, Jeremy Singer, and Adrian Ravi Kishore Ramsingh.
-An existing smart campus application was developed using \gls{MTASK} and quantitively and qualitatively compared to the original application that was developed using a traditional \gls{IOT} stack \citep{lubbers_tiered_2020}.
-This research was later extended to include a four-way comparison: \gls{PYTHON}, \gls{MICROPYTHON}, \gls{ITASK} and \gls{MTASK} \citep{lubbers_could_2022}.
-Currently, power efficiency behaviour of traditional versus \gls{TOP} \gls{IOT} stacks is being compared as well adding a \gls{FREERTOS} implementation to the mix as well.
-
-\chapter{The \texorpdfstring{\gls{MTASK}}{mTask} \texorpdfstring{\glsxtrshort{DSL}}{DSL}}%
-\label{chp:mtask_dsl}
-\begin{chapterabstract}
-This chapter introduces the \gls{MTASK} language more technically by:
- \begin{itemize}
- \item introducing the setup of the \gls{EDSL};
- \item and showing the language interface and examples for:
- \begin{itemize}
- \item data types
- \item expression
- \item task and their combinators.
- \end{itemize}
- \end{itemize}
-\end{chapterabstract}
-
-The \gls{MTASK} system is a complete \gls{TOP} programming environment for programming microcontrollers.
-It is implemented as an \gls{EDSL} in \gls{CLEAN} using class-based---or tagless-final---embedding (see \cref{sec:tagless-final_embedding}).
-
-Due to the nature of the embedding technique, it is possible to have multiple views on-programs written in the \gls{MTASK} language.
-The following interpretations are available for \gls{MTASK}.
-
-\begin{description}
- \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[Byte code compiler]
-
- The compiler compiles the \gls{MTASK} program at runtime to a specialised byte code.
- Using a handful of integration functions and tasks, \gls{MTASK} tasks can be executed on microcontrollers 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{description}
-
-When using the compiler interpretation in conjunction with the \gls{ITASK} integration, \gls{MTASK} is a heterogeneous \gls{DSL}.
-I.e.\ some components---e.g.\ the \gls{RTS} on the microcontroller---is largely unaware of the other components in the system, and it is executed on a completely different architecture.
-The \gls{MTASK} language is an enriched simply-typed $\lambda$-calculus with support for some basic types, arithmetic operations, and function definition; and a task language (see \cref{sec:top}).
-
-\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 microcontrollers that may only have \qty{2}{\kibi\byte} 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
- \caption{Mapping from \gls{CLEAN}/\gls{MTASK} data types to \gls{CPP} datatypes.}%
- \label{tbl:mtask-c-datatypes}
- \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}
-\end{table}
-
-\Cref{lst:constraints} contains the definitions for the auxiliary types and type constraints (such as \cleaninline{type} an \cleaninline{basicType}) that are used to construct \gls{MTASK} expressions.
-The \gls{MTASK} language interface consists of a core collection of type classes bundled in the type class \cleaninline{class mtask}.
-Every interpretation implements the type classes in the \cleaninline{mtask} class
-There are also \gls{MTASK} extensions that not every interpretation implements such as peripherals and \gls{ITASK} integration.
-\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
-
-\end{lstClean}
-
-Sensors, \glspl{SDS}, functions, \etc{} may only be defined at the top level.
-The \cleaninline{Main} type is used that is used to distinguish the top level from the main expression.
-Some top level definitions, such as functions, are defined using \gls{HOAS}.
-To make their syntax friendlier, the \cleaninline{In} type---an infix tuple---is used to combine these top level definitions as can be seen in \cleaninline{someTask} (\cref{lst:mtask_types}).
-
-\begin{lstClean}[caption={Example task and auxiliary types in the \gls{MTASK} language.},label={lst:mtask_types}]
-:: Main a = { main :: a }
-:: In a b = (In) infix 0 a b
-
-someTask :: MTask v Int | mtask v & liftsds v & sensor1 v & ...
-someTask =
- sensor1 config1 \sns1->
- sensor2 config2 \sns2->
- sds \s1=initial
- In liftsds \s2=someiTaskSDS
- In fun \fun1= ( ... )
- In fun \fun2= ( ... )
- In { main = mainexpr }
-\end{lstClean}
-
-\section{Expressions}\label{sec: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}); perform number and boolean arithmetics; do comparisons; and conditional execution.
-For every common boolean and 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
- ...
- (&.) 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
- ...
- 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} that will convert the argument to the respective type similar to casting in \gls{C}.
-
-\begin{lstClean}[caption={Type conversion functions in \gls{MTASK}.}]
-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}
-
-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 such as \cleaninline{true :== lit True}, \cleaninline{false :== lit False}, \etc.
-
-\Cref{lst:example_exprs} shows some examples of these expressions.
-Since they are only expressions, there is no need for a \cleaninline{Main}.
-\cleaninline{e0} defines the literal $42$, \cleaninline{e1} calculates the literal $42.0$ using real numbers.
-\cleaninline{e2} compares \cleaninline{e0} and \cleaninline{e1} as integers and if they are equal it returns the \cleaninline{e2}$/2$ and \cleaninline{e0} otherwise.
-
-\begin{lstClean}[label={lst:example_exprs},caption={Example \gls{MTASK} expressions.}]
-e0 :: v Int | expr v
-e0 = lit 42
-
-e1 :: v Real | expr v
-e1 = lit 38.0 + real (lit 4)
-
-e2 :: v Int | expr v
-e2 = if' (e0 ==. int e1)
- (int e1 /. lit 2) e0
-\end{lstClean}
-
-\Gls{MTASK} is shallowly embedded in \gls{CLEAN} and the terms are constructed at runtime.
-This means that \gls{MTASK} programs can also be tailor-made at runtime or constructed using \gls{CLEAN} functions maximising the linguistic reuse \citep{krishnamurthi_linguistic_2001}
-\cleaninline{approxEqual} in \cref{lst:example_macro} performs an approximate equality---albeit not taking into account all floating point pecularities---.
-When calling \cleaninline{approxEqual} in an \gls{MTASK} function, the resulting code is inlined.
-
-\begin{lstClean}[label={lst:example_macro},caption={Example linguistic reuse in the \gls{MTASK} language.}]
-approxEqual :: (v Real) (v Real) (v Real) -> v Real | expr v
-approxEqual x y eps = if' (x ==. y) true
- ( if' (x >. y)
- (y -. x < eps)
- (x -. y < eps)
- )
-\end{lstClean}
-
-\subsection{Data types}
-Most of \gls{CLEAN}'s basic types have been mapped on \gls{MTASK} types.
-However, it can be useful to have access to compound types as well.
-All types in \gls{MTASK} must have a fixed size representation on the stack so sum types are not (yet) supported.
-While it is possible to lift types using the \cleaninline{lit} function, you cannot do anything with the types besides passing them around but they are being produced by some parallel task combinators (see \cref{sssec:combinators_parallel}).
-To be able to use types as first class citizens, constructors and field selectors are required (see \cref{chp:first-class_datatypes}).
-\Cref{lst:tuple_exprs} shows the scaffolding for supporting tuples in \gls{MTASK}.
-Besides the constructors and field selectors, there is also a helper function available that transforms a function from a tuple of \gls{MTASK} expressions to an \gls{MTASK} expression of a tuple.
-Examples for using tuple can be found in \cref{sec:mtask_functions}.
-
-\begin{lstClean}[label={lst:tuple_exprs},caption={Tuple constructor and field selectors in \gls{MTASK}.}]
-class tupl v where
- tupl :: (v a) (v b) -> v (a, b) | type a & type b
- first :: (v (a, b)) -> v a | type a & type b
- second :: (v (a, b)) -> v b | type a & type b
-
- tupopen f :== \v->f (first v, second v)
-\end{lstClean}
-
-\subsection{Functions}\label{sec:mtask_functions}
-Adding functions to the language is achieved by type class to the \gls{DSL}.
-By using \gls{HOAS}, both the function definition and the calls to the function can be controlled by the \gls{DSL} \citep{pfenning_higher-order_1988,chlipala_parametric_2008}.
-The \gls{MTASK} only allows first-order functions and does not allow partial function application.
-This is restricted by using a multi-parameter type class where the first parameter represents the arguments and the second parameter the view.
-By providing a single instance per function arity instead of providing one instance for all functions and using tuples for the arguments this constraint can be enforced.
-Also, \gls{MTASK} only supports top-level functions which is enforced by the \cleaninline{Main} box.
-The definition of the type class and the instances for an example interpretation (\cleaninline{:: Inter}) are as follows:
-
-\begin{lstClean}[caption={Functions in \gls{MTASK}.}]
-class fun a v :: ((a -> v s) -> In (a -> v s) (Main (MTask v u)))
- -> Main (MTask v u)
-
-instance fun () Inter where ...
-instance fun (Inter a) Inter | type a where ...
-instance fun (Inter a, Inter b) Inter | type a, type b where ...
-instance fun (Inter a, Inter b, Inter c) Inter | type a, ... where ...
-...
-\end{lstClean}
-
-Deriving how to define and use functions from the type is quite the challenge even though the resulting syntax is made easier using the infix type \cleaninline{In}.
-\Cref{lst:function_examples} show the factorial function, a tail-call optimised factorial function and a function with zero arguments to demonstrate the syntax.
-Splitting out the function definition for each single arity means that that for every function arity and combination of arguments, a separate class constraint must be created.
-Many of the often used functions are already bundled in the \cleaninline{mtask} class constraint collection.
-\cleaninline{factorialtail} shows a manually added class constraint.
-Definiting zero arity functions is shown in the \cleaninline{zeroarity} expression.
-Finally, \cleaninline{swapTuple} shows an example of a tuple being swapped.
-
-% VimTeX: SynIgnore on
-\begin{lstClean}[label={lst:function_examples},caption={Function examples in \gls{MTASK}.}]
-factorial :: Main (v Int) | mtask v
-factorial =
- fun \fac=(\i->if' (i <. lit 1)
- (lit 1)
- (i *. fac (i -. lit 1)))
- In {main = fac (lit 5) }
-
-factorialtail :: Main (v Int) | mtask v & fun (v Int, v Int) v
-factorialtail =
- fun \facacc=(\(acc, i)->if' (i <. lit 1)
- acc
- (fac (acc *. i, i -. lit 1)))
- In fun \fac=(\i->facacc (lit 1, i))
- In {main = fac (lit 5) }
-
-zeroarity :: Main (v Int) | mtask v
-zeroarity =
- fun \fourtytwo=(\()->lit 42)
- In fun \add=(\(x, y)->x +. y)
- In {main = add (fourtytwo (), lit 9)}
-
-swapTuple :: Main (v (Int, Bool)) | mtask v
-swapTuple =
- fun \swap=(tupopen \(x, y)->tupl y x)
- In {main = swap (tupl true (lit 42)) }
-\end{lstClean}
-% VimTeX: SynIgnore off
-
-\section{Tasks and task combinators}\label{sec:top}
-\Gls{MTASK}'s task language can be divided into three categories, namely
-\begin{enumerate*}
- \item Basic tasks, in most \gls{TOP} systems, the basic tasks are called editors, modelling the interactivity with the user.
- In \gls{MTASK}, there are no \emph{editors} in that sense but there is interaction with the outside world through microcontroller peripherals such as sensors and actuators.
- \item Task combinators provide a way of describing the workflow.
- They combine one or more tasks into a compound task.
- \item \glspl{SDS} in \gls{MTASK} can be seen as references to data that can be shared using many-to-many communication and are only accessible from within the task language to ensure atomicity.
-\end{enumerate*}
-
-As \gls{MTASK} is integrated with \gls{ITASK}, the same stability distinction is made for task values.
-A task in \gls{MTASK} is denoted by the \gls{DSL} type synonym shown in \cref{lst:task_type}.
-
-\begin{lstClean}[label={lst:task_type},caption={Task type in \gls{MTASK}.}]
-:: MTask v a :== v (TaskValue a)
-:: TaskValue a
- = NoValue
- | Value a Bool
-\end{lstClean}
-
-\subsection{Basic tasks}
-The most rudimentary basic tasks are the \cleaninline{rtrn} and \cleaninline{unstable} tasks.
-They lift the value from the \gls{MTASK} expression language to the task domain either as a stable value or an unstable value.
-There is also a special type of basic task for delaying execution.
-The \cleaninline{delay} task---given a number of milliseconds---yields an unstable value while the time has not passed.
-Once the specified time has passed, the time it overshot the planned time is yielded as a stable task value.
-See \cref{sec:repeat} for an example task using \cleaninline{delay}.
-
-\begin{lstClean}[label={lst:basic_tasks},caption={Function examples in \gls{MTASK}.}]
-class rtrn v :: (v t) -> MTask v t
-class unstable v :: (v t) -> MTask v t
-class delay v :: (v n) -> MTask v n | long v n
-\end{lstClean}
-
-\subsubsection{Peripherals}\label{sssec:peripherals}
-For every sensor or actuator, basic tasks are available that allow interaction with the specific peripheral.
-The type classes for these tasks are not included in the \cleaninline{mtask} class collection as not all devices nor all language interpretations have such peripherals connected.
-%\todo{Historically, peripheral support has been added \emph{by need}.}
-
-\Cref{lst:dht,lst:gpio} show the type classes for \glspl{DHT} sensors and \gls{GPIO} access.
-Other peripherals have similar interfaces, they are available in the \cref{sec:aux_peripherals}.
-For the \gls{DHT} sensor there are two basic tasks, \cleaninline{temperature} and \cleaninline{humidity}, that---will given a \cleaninline{DHT} object---produce a task that yields the observed temperature in \unit{\celcius} or relative humidity as a percentage as an unstable value.
-Currently, two different types of \gls{DHT} sensors are supported, the \emph{DHT} family of sensors connect through $1$-wire protocol and the \emph{SHT} family of sensors connected using \gls{I2C} protocol.
-Creating such a \cleaninline{DHT} object is very similar to creating functions in \gls{MTASK} and uses \gls{HOAS} to make it type safe.
-
-\begin{lstClean}[label={lst:dht},caption{The \gls{MTASK} interface for \glspl{DHT} sensors.}]
-:: DHT //abstract
-:: DHTInfo
- = DHT_DHT Pin DHTtype
- | DHT_SHT I2CAddr
-:: DHTtype = DHT11 | DHT21 | DHT22
-class dht v where
- DHT :: DHTInfo ((v DHT) -> Main (v b)) -> Main (v b) | type b
- temperature :: (v DHT) -> MTask v Real
- humidity :: (v DHT) -> MTask v Real
-
-measureTemp :: Main (MTask v Real) | mtask v & dht v
-measureTemp = DHT (DHT_SHT (i2c 0x36)) \dht->
- {main=temperature dht}
-\end{lstClean}
-
-\Gls{GPIO} access is divided into three classes: analog, digital and pin modes.
-For all pins and pin modes an \gls{ADT} is available that enumerates the pins.
-The analog \gls{GPIO} pins of a microcontroller are connected to an \gls{ADC} that translates the voltage to an integer.
-Analog \gls{GPIO} pins can be either read or written to.
-Digital \gls{GPIO} pins only report a high or a low value.
-The type class definition is a bit more complex since analog \gls{GPIO} pins can be used as digital \gls{GPIO} pins as well.
-Therefore, if the \cleaninline{p} type implements the \cleaninline{pin} class---i.e.\ either \cleaninline{APin} or \cleaninline{DPin}---the \cleaninline{dio} class can be used.
-\Gls{GPIO} pins usually operate according to a certain pin mode that states whether the pin acts as an input pin, an input with an internal pull-up resistor or an output pin.
-This setting can be applied using the \cleaninline{pinMode} class by hand or by using the \cleaninline{declarePin} \gls{GPIO} pin constructor.
-Setting the pin mode is a task that immediately finisheds and fields a stable unit value.
-Writing to a pin is also a task that immediately finishes but yields the written value instead.
-Reading a pin is a task that yields an unstable value---i.e.\ the value read from the actual pin.
-
-\begin{lstClean}[label={lst:gpio},caption={The \gls{MTASK} interface for \gls{GPIO} access.}]
-:: APin = A0 | A1 | A2 | A3 | A4 | A5
-:: DPin = D0 | D1 | D2 | D3 | D4 | D5 | D6 | D7 | D8 | D9 | D10 | D11 | D12 | D13
-:: PinMode = PMInput | PMOutput | PMInputPullup
-:: Pin = AnalogPin APin | DigitalPin DPin
-class pin p :: p -> Pin
-
-class aio v where
- writeA :: (v APin) (v Int) -> MTask v Int
- readA :: (v APin) -> MTask v Int
-
-class dio p v | pin p where
- writeD :: (v p) (v Bool) -> MTask v Bool
- readD :: (v p) -> MTask v Bool | pin p
-
-class pinMode v where
- pinMode :: (v PinMode) (v p) -> MTask v () | pin p
- declarePin :: p PinMode ((v p) -> Main (v a)) -> Main (v a) | pin p
-\end{lstClean}
-
-\begin{lstClean}[label={lst:gpio_examples},caption={\Gls{GPIO} example in \gls{MTASK}.}]
-task1 :: MTask v Int | mtask v
-task1 = declarePin A3 PMInput \a3->{main=readA a3}
+%\chapter{\texorpdfstring{\Glsxtrshort{TOP} for the \glsxtrshort{IOT}}{TOP for the IoT}}%
+\subfile{4iot}
-task2 :: MTask v Int | mtask v
-task2 = declarePin D3 PMOutput \d3->{main=writeD d3 true}
-\end{lstClean}
-
-\subsection{Task combinators}
-Task combinators are used to combine multiple tasks into one to describe workflows.
-There are three main types of task combinators, namely:
-\begin{enumerate*}
- \item Sequential combinators that execute tasks one after the other, possibly using the result of the left hand side.
- \item Parallel combinators that execute tasks at the same time combining the result.
- \item Miscellaneous combinators that change the semantics of a task---e.g.\ repeat it or delay execution.
-\end{enumerate*}
-
-\subsubsection{Sequential}
-Sequential task combination allows the right-hand side task to observe the left-hand side task value.
-All seqential task combinators are expressed in the \cleaninline{expr} class and can be---and are by default---derived from the Swiss army knife step combinator \cleaninline{>>*.}.
-This combinator has a single task on the left-hand side and a list of \emph{task continuations} on the right-hand side.
-The list of task continuations is checked every rewrite step and if one of the predicates matches, the task continues with the result of this combination.
-\cleaninline{>>=.} is a shorthand for the bind operation, if the left-hand side is stable, the right-hand side function is called to produce a new task.
-\cleaninline{>>|.} is a shorthand for the sequence operation, if the left-hand side is stable, it continues with the right-hand side task.
-The \cleaninline{>>~.} and \cleaninline{>>..} combinators are variants of the ones above that ignore the stability and continue on an unstable value as well.
-
-\begin{lstClean}[label={lst:mtask_sequential},caption={Sequential task combinators in \gls{MTASK}.}]
-class step v | expr v where
- (>>*.) infixl 1 :: (MTask v t) [Step v t u] -> MTask v u
- (>>=.) infixl 0 :: (MTask v t) ((v t) -> MTask v u) -> MTask v u
- (>>|.) infixl 0 :: (MTask v t) (MTask v u) -> MTask v u
- (>>~.) infixl 0 :: (MTask v t) ((v t) -> MTask v u) -> MTask v u
- (>>..) infixl 0 :: (MTask v t) (MTask v u) -> MTask v u
-
-:: Step v t u
- = IfValue ((v t) -> v Bool) ((v t) -> MTask v u)
- | IfStable ((v t) -> v Bool) ((v t) -> MTask v u)
- | IfUnstable ((v t) -> v Bool) ((v t) -> MTask v u)
- | Always (MTask v u)
-\end{lstClean}
-
-\todo{more examples step?}
-
-The following listing shows an example of a step in action.
-The \cleaninline{readPinBin} function produces an \gls{MTASK} task that classifies the value of an analogue pin into four bins.
-It also shows that the nature of embedding allows the host language to be used as a macro language.
-Furthermore
-
-\begin{lstClean}[label={lst:mtask_readpinbin},caption={Read an analog pin and bin the value in \gls{MTASK}.}]
-readPinBin :: Int -> Main (MTask v Int) | mtask v
-readPinBin lim = declarePin PMInput A2 \a2->
- { main = readA a2 >>*.
- [ IfValue (\x->x <. lim) (\_->rtrn (lit bin))
- \\ lim <-[64,128,192,256]
- & bin <- [0..]]}
-\end{lstClean}
-
-\subsubsection{Parallel}\label{sssec:combinators_parallel}
-The result of a parallel task combination is a compound that actually executes the tasks at the same time.
-
-There are two types of parallel task combinators (see \cref{lst:mtask_parallel}).
-The conjunction combinator (\cleaninline{.&&.}) combines the result by putting the values from both sides in a tuple.
-The stability of the task depends on the stability of both children.
-If both children are stable, the result is stable, otherwise the result is unstable.
-The disjunction combinator (\cleaninline{.\|\|.}) combines the results by picking the leftmost, most stable task.
-The semantics are easily described using \gls{CLEAN} functions shown in \cref{lst:semantics_con,lst:semantics_dis}.
-
-\begin{figure}[ht]
- \centering
- \begin{subfigure}[t]{.5\textwidth}
- \begin{lstClean}[caption={Semantics of the\\conjunction combinator.},label={lst:semantics_con}]
-con :: (TaskValue a) (TaskValue b)
- -> TaskValue (a, b)
-con NoValue r = NoValue
-con l NoValue = NoValue
-con (Value l ls) (Value r rs)
- = Value (l, r) (ls && rs)
-
- \end{lstClean}
- \end{subfigure}%
- \begin{subfigure}[t]{.5\textwidth}
- \begin{lstClean}[caption={Semantics of the\\disjunction combinator.},label={lst:semantics_dis}]
-dis :: (TaskValue a) (TaskValue a)
- -> TaskValue a
-dis NoValue r = r
-dis l NoValue = l
-dis (Value l ls) (Value r rs)
- | rs = Value r True
- | otherwise = Value l ls
- \end{lstClean}
- \end{subfigure}
-\end{figure}
-
-\begin{lstClean}[label={lst:mtask_parallel},caption={Parallel task combinators in \gls{MTASK}.}]
-class (.&&.) infixr 4 v :: (MTask v a) (MTask v b) -> MTask v (a, b)
-class (.||.) infixr 3 v :: (MTask v a) (MTask v a) -> MTask v a
-\end{lstClean}
-
-\Cref{lst:mtask_parallel_example} gives an example of the parallel task combinator.
-This program will read two pins at the same time, returning when one of the pins becomes \arduinoinline{HIGH}.
-If the combinator was the \cleaninline{.&&.} instead, the type would be \cleaninline{MTask v (Bool, Bool)} and the task would only return when both pins have been \arduinoinline{HIGH} but not necessarily at the same time.
-
-\begin{lstClean}[label={lst:mtask_parallel_example},caption={Parallel task combinator example in \gls{MTASK}.}]
-task :: MTask v Bool
-task =
- declarePin D0 PMInput \d0->
- declarePin D1 PMInput \d1->
- let monitor pin = readD pin >>*. [IfValue (\x->x) \x->rtrn x]
- In {main = monitor d0 .||. monitor d1}
-\end{lstClean}
-
-\subsubsection{Repeat}\label{sec:repeat}
-The \cleaninline{rpeat} combinator executes the child task.
-If a stable value is observed, the task is reinstated.
-The functionality of \cleaninline{rpeat} can also be simulated by using functions and sequential task combinators and even made to be stateful as can be seen in \cref{lst:blinkthreadmtask}.
-
-\begin{lstClean}[label={lst:mtask_repeat},caption={Repeat task combinators in \gls{MTASK}.}]
-class rpeat v where
- rpeat :: (MTask v a) -> MTask v a
-\end{lstClean}
-
-To demonstrate the combinator, \cref{lst:mtask_repeat_example} show \cleaninline{rpeat} in use.
-This task will mirror the value read from analog \gls{GPIO} pin \cleaninline{A1} to pin \cleaninline{A2} by constantly reading the pin and writing the result.
-
-\begin{lstClean}[label={lst:mtask_repeat_example},caption={Exemplatory repeat task in \gls{MTASK}.}]
-task :: MTask v Int | mtask v
-task =
- declarePin A1 PMInput \a1->
- declarePin A2 PMOutput \a2->
- {main = rpeat (readA a1 >>~. writeA a2 >>|. delay (lit 1000))}
-\end{lstClean}
-
-\subsection{\texorpdfstring{\Glsxtrlongpl{SDS}}{Shared data sources}}
-\Glspl{SDS} in \gls{MTASK} are by default references to shared memory but can also be references to \glspl{SDS} in \gls{ITASK} (see \cref{sec:liftsds}).
-Similar to peripherals (see \cref{sssec:peripherals}), they are constructed at the top level and are accessed through interaction tasks.
-The \cleaninline{getSds} task yields the current value of the \gls{SDS} as an unstable value.
-This behaviour is similar to the \cleaninline{watch} task in \gls{ITASK}.
-Writing a new value to \pgls{SDS} is done using \cleaninline{setSds}.
-This task yields the written value as a stable result after it is done writing.
-Getting and immediately after setting \pgls{SDS} is not necessarily an \emph{atomic} operation in \gls{MTASK} because it is possible that another task accesses the \gls{SDS} in between.
-To circumvent this issue, \cleaninline{updSds} is created, this task atomically updates the value of the \gls{SDS}.
-The \cleaninline{updSds} task only guarantees atomicity within \gls{MTASK}.
-
-\begin{lstClean}[label={lst:mtask_sds},caption={\Glspl{SDS} in \gls{MTASK}.}]
-:: Sds a // abstract
-class sds v where
- sds :: ((v (Sds t)) -> In t (Main (MTask v u))) -> Main (MTask v u)
- getSds :: (v (Sds t)) -> MTask v t
- setSds :: (v (Sds t)) (v t) -> MTask v t
- updSds :: (v (Sds t)) ((v t) -> v t) -> MTask v t
-\end{lstClean}
-
-\Cref{lst:mtask_sds_examples} shows an example using \glspl{SDS}.
-The \cleaninline{count} function takes a pin and returns a task that counts the number of times the pin is observed as high by incrementing the \cleaninline{share} \gls{SDS}.
-In the \cleaninline{main} expression, this function is called twice and the results are combined using the parallel or combinator (\cleaninline{.||.}).
-Using a sequence of \cleaninline{getSds} and \cleaninline{setSds} would be unsafe here because the other branch might write their old increment value immediately after writing, effectively missing a count.\todo{beter opschrijven}
-
-\begin{lstClean}[label={lst:mtask_sds_examples},caption={Examples with \glspl{SDS} in \gls{MTASK}.}]
-task :: MTask v Int | mtask v
-task = declarePin D3 PMInput \d3->
- declarePin D5 PMInput \d5->
- sds \share=0
- In fun \count=(\pin->
- readD pin
- >>* [IfValue (\x->x) (\_->updSds (\x->x +. lit 1) share)]
- >>| delay (lit 100) // debounce
- >>| count pin)
- In {main=count d3 .||. count d5}
-\end{lstClean}
+%\chapter{The \texorpdfstring{\gls{MTASK}}{mTask} \texorpdfstring{\glsxtrshort{DSL}}{DSL}}%
+\subfile{lang}
\chapter{Integration with \texorpdfstring{\gls{ITASK}}{iTask}}%
\label{chp:integration_with_itask}
\section{Integration with \texorpdfstring{\gls{ITASK}}{iTask}}
IFL18 paper stukken
+% Green computing
\subfile{green}
\input{subfilepostamble}
However many tierless languages have yet to provide a comprehensive set of security technologies, despite its importance in domains like web and \gls{IOT} applications. For example Erlang and many Erlang-based systems \citep{shibanai_distributed_2018,sivieri2012drop}, lack important security measures. Indeed security is not covered in a recent, otherwise comprehensive, survey of tierless technologies \citep{weisenburger2020survey}.
-\Gls{CLEAN}\slash\gls{ITASK} and \gls{CLEAN}/\gls{ITASK}/\gls{MTASK} are typical in this respect: little effort has yet been expended on improving their security. Of course as tierless languages they benefit from static type safety and automatically generated communication and placement. Some preliminary work shows that, as the communication between layers is protocol agnostic, more secure alternatives can be used. One example is to run the \gls{ITASK} server behind a reverse proxy implementing TLS/SSL encryption \citep{wijkhuizen_security_2018}. A second is to add integrity checks or even encryption to the communication protocol for resource-rich sensor nodes \citep{boer_de_secure_2020}.
+\Gls{CLEAN}\slash\gls{ITASK} and \gls{CLEAN}/\gls{ITASK}/\gls{MTASK} are typical in this respect: little effort has yet been expended on improving their security. Of course as tierless languages they benefit from static type safety and automatically generated communication and placement. Some preliminary work shows that, as the communication between layers is protocol agnostic, more secure alternatives can be used. One example is to run the \gls{ITASK} server behind a reverse proxy implementing TLS/SSL encryption \citep{wijkhuizen_security_2018}. A second is to add integrity checks or even encryption to the communication protocol for resource-rich sensor nodes \citep{de_boer_secure_2020}.
\section{Task-oriented and \texorpdfstring{\glsxtrshort{IOT}}{IoT} programming in \texorpdfstring{\glsentrytext{CLEAN}}{Clean}}
repositories / phd-thesis.git / commitdiff
