<reponame>mklinik/task-semantics<filename>doc/sections/introduction.tex<gh_stars>0
% !TEX root=../pldi2019.tex



\section{Introduction}

Task-Oriented Programming (\TOP) is a programming paradigm aimed at writing interactive multi-user applications in a declarative way \cite{conf/ppdp/PlasmeijerLMAK12}.
\TOP has two aspects.
Firstly, \TOP defines the primitive building blocks that are useful for high-level descriptions of how users collaborate with each other and with applications.
These building blocks are \emph{editors}, \emph{combinators}, and \emph{shared data sources}.
Secondly, \TOP defines a type-driven way to generate applications, including graphical user interfaces, from workflows modelled with said building blocks.

In this paper we study the essence of Task-Oriented Programming.
We claim that at the heart of \TOP lie modular interactive workflows.
Workflows because \TOP programs coordinate collaboration between people.
Interactive because progress of \TOP programs is driven by user input.
Modular because the embedding in a strongly-typed functional language allows powerful abstractions using type-driven techniques and higher-order functions.

Interactive workflows are called \emph{tasks}.
Tasks stand for units of work in the real world, assigned to people.
People can work together in a number of ways, and this is reflected in \TOP by task combinators.
There is sequential composition, parallel composition, and choice.
People need to communicate in order to engage in these forms of collaboration.
This is reflected in \TOP by three kinds of communication mechanisms.
There is data flow alongside control flow, where the result of a task is passed onto the next.
There is data flow across control flow, where information is shared between multiple tasks.
Finally, there is communication with the outside world, where information is entered into the system via input events.
The end points where the outside world interacts with applications are called editors.
In generated applications, editors can take many forms, like input fields, selection boxes, or map widgets.

iTasks is an implementation of \TOP, in the form of an embedded domain-specific language in the lazy functional programming language Clean.
It is a library that provides editors and monadic combinators.
iTasks uses the generic programming facilities of Clean to derive web applications from workflow models.

iTasks has been used to implement an incident management tool for the Dutch coast guard \cite{conf/iscram/LijnseJP12}.
Furthermore it has been used numerous times to prototype ideas for Command and Control \cite{theses/nlda/Kool17, theses/radboud/Stutterheim17}, and in a case study for the Dutch tax authority \cite{conf/sfp/StutterheimAP17}.

iTasks has many features, and its basic combinators are versatile and powerful.
Simpler combinators are implemented by restricting the powerful ones.
This is useful for everyday programming, where having lots of functionality at one's fingertips is convenient and efficient.

Our language is a strict subset of iTasks.
With iTasks it is possible to express very complicated real-world situations in a comfortable and productive manner.
\TOPHAT tries to cover as many of those use cases as possible, while still being small enough to be open for formal reasoning.
Neither the semantics in \cite{conf/ppdp/PlasmeijerLMAK12} nor iTasks itself lend themselves well for formal reasoning, because of the complicated collaboration patterns that can be expressed.

In this paper, we set out to develop a formal basis for \TOP, with the goal of specifying the basic building blocks of declarative workflows.
We clearly separate them from general purpose programming concepts.
This allows us to prove properties like progress and type preservation.

\paragraph{Contributions}
We present a task calculus for modeling declarative workflows, embedded in a simply typed lambda-calculus.
We develop an operational semantics that is driven by user inputs.
The semantics of the task language is clearly separated from the semantics of the underlying host language.
Furthermore, we present the following semantic observations on tasks: the current value, the current user interface, the accepted inputs, and whether a term is stuck.
All these observations exist in iTasks, albeit combined into one big type.
By separating them in the style of a deep embedding \cite{conf/cefp/Gibbons13}, we make explicit where, and where not, they depend on each other.

Furthermore we compare our calculus with the process algebra \CSP, to show how their concepts like communication, and sequential and parallel composition relate.
