Add a Hardware description chapter, that describes the language.

This chapter is still far from finished.

diff --git a/Chapters/HardwareDescription.tex b/Chapters/HardwareDescription.tex
new file mode 100644 (file)
index 0000000..a0cc1c5
--- /dev/null
+++ b/Chapters/HardwareDescription.tex
@@ -0,0 +1,179 @@
+\chapter{Hardware description}
+  This chapter will provide an overview of the hardware description language
+  that was created and the issues that have arisen in the process. It will
+  focus on the issues of the language, not the implementation.
+
+  When translating Haskell to hardware, we need to make choices in what kind
+  of hardware to generate for what Haskell constructs. When faced with
+  choices, we've tried to stick with the most obvious choice wherever
+  possible. In a lot of cases, when you look at a hardware description it is
+  comletely clear what hardware is described. We want our translator to
+  generate exactly that hardware whenever possible, to minimize the amount of
+  surprise for people working with it.
+   
+  In this chapter we try to describe how we interpret a Haskell program from a
+  hardware perspective. We provide a description of each Haskell language
+  element that needs translation, to provide a clear picture of what is
+  supported and how.
+
+  \section{Function application}
+  The basic syntactic element of a functional program are functions and
+  function application. These have a single obvious VHDL translation: Each
+  function becomes a hardware component, where each argument is an input port
+  and the result value is the output port.
+
+  Each function application in turn becomes component instantiation. Here, the
+  result of each argument expression is assigned to a signal, which is mapped
+  to the corresponding input port. The output port of the function is also
+  mapped to a signal, which is used as the result of the application.
+
+  An example of a simple program using only function application would be:
+
+  \starthaskell
+  -- | A simple function that returns the and of three bits
+  and3 :: Bit -> Bit -> Bit -> Bit
+  and3 a b c = and (and a b) c
+  \stophaskell
+
+  This results in the following hardware:
+  
+  TODO: Pretty picture
+
+  \subsection{Partial application}
+  It should be obvious that we cannot generate hardware signals for all
+  expressions we can express in Haskell. The most obvious criterium for this
+  is the type of an expression. We will see more of this below, but for now it
+  should be obvious that any expression of a function type cannot be
+  represented as a signal or i/o port to a component.
+
+  From this, we can see that the above translation rules do not apply to a
+  partial application. Let's look at an example:
+
+  \starthaskell
+  -- | Multiply the input word by four.
+  quadruple :: Word -> Word
+  quadruple n = mul (mul n)
+    where
+      mul = (*) 2
+  \stophaskell
+
+  It should be clear that the above code describes the following hardware:
+
+  TODO: Pretty picture
+
+  Here, the definition of mul is a partial function application: It applies
+  \hs{2 :: Word} to the function \hs{(*) :: Word -> Word -> Word} resulting in
+  the expression \hs{(*) 2 :: Word -> Word}. Since this resulting expression
+  is again a function, we can't generate hardware for it directly. This is
+  because the hardware to generate for \hs{mul} depends completely on where
+  and how it is used. In this example, it is even used twice!
+
+  However, it is clear that the above hardware description actually describes
+  valid hardware. In general, we can see that any partial applied function
+  must eventually become completely applied, at which point we can generate
+  hardware for it using the rules for function application above. It might
+  mean that a partial application is passed around quite a bit (even beyond
+  function boundaries), but eventually, the partial application will become
+  completely applied.
+
+  \section{Recursion}
+  An import concept in functional languages is recursion. In it's most basic
+  form, recursion is a function that is defined in terms of itself. This
+  usually requires multiple evaluations of this function, with changing
+  arguments, until eventually an evaluation of the function no longer requires
+  itself.
+
+  Recursion in a hardware description is a bit of a funny thing. Usually,
+  recursion is associated with a lot of nondeterminism, stack overflows, but
+  also flexibility and expressive power.
+
+  Given the notion that each function application will translate to a
+  component instantiation, we are presented with a problem. A recursive
+  function would translate to a component that contains itself. Or, more
+  precisely, that contains an instance of itself. This instance would again
+  contain an instance of itself, and again, into infinity. This is obviously a
+  problem for generating hardware.
+
+  This is expected for functions that describe infinite recursion. In that
+  case, we can't generate hardware that shows correct behaviour in a single
+  cycle (at best, we could generate hardware that needs an infinite number of
+  cycles to complete).
+  
+  However, most recursive hardware descriptions will describe finite
+  recursion. This is because the recursive call is done conditionally. There
+  is usually a case statement where at least one alternative does not contain
+  the recursive call, which we call the "base case". If, for each call to the
+  recursive function, we would be able to detect which alternative applies,
+  we would be able to remove the case expression and leave only the base case
+  when it applies. This will ensure that expanding the recursive functions
+  will terminate after a bounded number of expansions.
+
+  This does imply the extra requirement that the base case is detectable at
+  compile time. In particular, this means that the decision between the base
+  case and the recursive case must not depend on runtime data.
+
+  \subsection{List recursion}
+  The most common deciding factor in recursion is the length of a list that is
+  passed in as an argument. Since we represent lists as vectors that encode
+  the length in the vector type, it seems easy to determine the base case. We
+  can simply look at the argument type for this. However, it turns out that
+  this is rather non-trivial to write down in Haskell in the first place. As
+  an example, we would like to write down something like this:
+ 
+  \starthaskell
+    sum :: Vector n Word -> Word
+    sum xs = case null xs of
+      True -> 0
+      False -> head xs + sum (tail xs)
+  \stophaskell
+
+  However, the typechecker will now use the following reasoning (element type
+  of the vector is left out):
+
+  \startitemize
+  \item tail has the type \hs{(n > 0) => Vector n -> Vector (n - 1)}
+  \item This means that xs must have the type \hs{(n > 0) => Vector n}
+  \item This means that sum must have the type \hs{(n > 0) => Vector n -> a}
+  \item sum is called with the result of tail as an argument, which has the
+  type \hs{Vector n} (since \hs{(n > 0) => n - 1 == m}).
+  \item This means that sum must have the type \hs{Vector n -> a}
+  \item This is a contradiction between the type deduced from the body of sum
+  (the input vector must be non-empty) and the use of sum (the input vector
+  could have any length).
+  \stopitemize
+
+  As you can see, using a simple case at value level causes the type checker
+  to always typecheck both alternatives, which can't be done! This is a
+  fundamental problem, that would seem perfectly suited for a type class.
+  Considering that we need to switch between to implementations of the sum
+  function, based on the type of the argument, this sounds like the perfect
+  problem to solve with a type class. However, this approach has its own
+  problems (not the least of them that you need to define a new typeclass for
+  every recursive function you want to define).
+
+  Another approach tried involved using GADTs to be able to do pattern
+  matching on empty / non empty lists. While this worked partially, it also
+  created problems with more complex expressions.
+
+  TODO: How much detail should there be here? I can probably refer to
+  Christiaan instead.
+
+  Evaluating all possible (and non-possible) ways to add recursion to our
+  descriptions, it seems better to leave out list recursion alltogether. This
+  allows us to focus on other interesting areas instead. By including
+  (builtin) support for a number of higher order functions like map and fold,
+  we can still express most of the things we would use list recursion for.
+ 
+  \subsection{General recursion}
+  Of course there are other forms of recursion, that do not depend on the
+  length (and thus type) of a list. For example, simple recursion using a
+  counter could be expressed, but only translated to hardware for a fixed
+  number of iterations. Also, this would require extensive support for compile
+  time simplification (constant propagation) and compile time evaluation
+  (evaluation constant comparisons), to ensure non-termination. Even then, it
+  is hard to really guarantee termination, since the user (or GHC desugarer)
+  might use some obscure notation that results in a corner case of the
+  simplifier that is not caught and thus non-termination.
+
+  Due to these complications, we leave other forms of recursion as
+  future work as well.