Generative Programming for Embedded Systems

In the course of this project we have explored generative programming
techniques for designing, implementing and verifying resource
sensitive systems. Our results show that dependently-typed frameworks
provide a suitable representation for heap costs~\cite{dt-framework}
and domain specific languages~\cite{dtpmsp-gpce,fidtp-ccc}.
We have also developed an extensible and
embeddable theorem-proving library \Ivor{}~\cite{ivor} and, using
this, implemented a dependently-typed programming language
\Idris~\cite{idris} and its compiler.

We have developed our dependent-type based approach, and our language
implementation, by applying it to several examples related to embedded
systems and hardware implementation. In addition to the
\emph{extra-functional} heap usage and
resource management problems detailed
in~\cite{dt-framework,fidtp-ccc}, we have investigated the
representation of \emph{functional} properties of realistic problems
such as binary arithmetic~\cite{tfp-ccc} as well as a more general
investigation into the relative merits of dependent type systems and
weaker functional language approaches~\cite{tfp-lightweight}.
We have thus made major progress in deploying advanced type-based
approaches for generative programming in resource-sensitive contexts, as
specified in the original research proposal.

aving developed dependent-type based approaches for program
generation, we found it beneficial to develop a new dependently-typed
language, \Idris{}, based on a theorem-proving system \Ivor{} (also
developed in the course of this project) rather than modifying our
existing Hume language~\cite{Hume-GPCE}. By adopting this approach
rather than the one outlined in our original methodology, we were free
to consider how the dependent-type approach could be applied to the
broader research problem, rather than being forced to solve some
difficult technical problems which arise from adding a new type system
to an already existing language (in this case, transferring dependent
pattern-matching and implicit arguments into the Hume computation and
co-ordination notations).

\Idris{} provided an ideal framework for experimenting with type system
implementation, primarily because using a dependent-type system makes
it possible to \emph{embed} domain-specific type systems within a host
type system, in a similar manner to embedding a domain-specific
language in a host language~\cite{hudak-dsel,yampa}. We implemented a
compiler for \Idris{}, including some optimisations arising
from our previous work~\cite{brady-thesis,mckinnabrady-phase}.

Although we have used a different language notation from that we originally intended (\Idris{} rather than Hume),
program generation techniques have remained central to the research we
have carried out. In particular, we have clearly
demonstrated that \emph{multi-stage programming} (a form of generative
programming) can be applied to
dependent type systems~\cite{dtpmsp-gpce}. The goal of multi-stage
programming is to allow abstraction without the run-time overhead. One
important abstraction is abstract syntax, e.g. of a domain-specific
language. We developed several examples in our system, using the DSL
approach, with direct application to embedded systems and hardware
implementation.


We do believe our methods can ultimately be implemented in a modified
version of Hume, by replacing the computation layer with the \Ivor{}
type theory. This is, however, purely a technical rather than a research problem.

\section{Tools}

In the course of the project we have implemented three interconnected
tools to support our research.

\begin{itemize}
\item \Ivor{}~\cite{ivor}, an implementation of a dependent type theory with
pattern matching and a tactic based theorem prover, accessible as a
library from Haskell, and therefore extensible (by writing tactics
using combinators accessible from Haskell) and embeddable (in
Haskell applications). \Ivor{} was originally intended as a core
language for representing resource bounded programs in the style
of~\cite{dt-framework}, using Haskell to implement domain specific
tactics for reasoning about costs. We have, however, also used
\Ivor{} to experiment with multi-stage
programming~\cite{dtpmsp-gpce} and as the core of a dependently
typed programming language.
\item \Idris{}~\cite{idris}, a language with dependent types. \Idris{}
is built on top of \Ivor{}, compiles via C and provides a foreign
function interface for interacting with C. Being built on top of a
theorem proving library allows easy interaction with the theorem
proving tools, and a clean separation of programs and proofs. The
foreign function interface allows experimentation with realistic
programs executing low level operations such as memory allocation
and concurrency.
\item \Epic{}, a supercombinator language which compiles to executable
code via C, usable as a back end for a functional programming
language. We have used this as a compiler for \Idris{} programs.
\end{itemize}

\noindent
Each of these tools is available to download via the project web site.