Fix a lot of things following from Jan's comments.
[matthijs/master-project/report.git] / Chapters / HardwareDescription.tex
index ef2533e3bf80f008601ae9b5a69a47cd22209ccd..ada3817f4c94e61cf03810b72d24f379ed026789 100644 (file)
@@ -6,22 +6,23 @@
 
   \todo{Shortshort introduction to Cλash (Bit, Word, and, not, etc.)}
 
-  When translating Haskell to hardware, we need to make choices about what kind
-  of hardware to generate for which 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.
+  To translate Haskell to hardware, every Haskell construct needs a
+  translation to \VHDL. There are often multiple valid translations
+  possible. When faced with choices, the most obvious choice has been
+  chosen wherever possible. In a lot of cases, when a programmer looks
+  at a functional hardware description it is completely clear what
+  hardware is described. We want our translator to generate exactly that
+  hardware whenever possible, to make working with Cλash as intuitive as
+  possible.
    
-  In this chapter we try to describe how we interpret a Haskell program from a
+  In this chapter we describe how to 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[sec:description:application]{Function application}
   \todo{Sidenote: Inputs vs arguments}
-  The basic syntactic element of a functional program are functions and
+  The basic syntactic elements of a functional program are functions and
   function application. These have a single obvious \small{VHDL} translation: Each
   function becomes a hardware component, where each argument is an input port
   and the result value is the (single) output port. This output port can have
@@ -81,15 +82,15 @@ and3 a b c = and (and a b) c
       {\boxedgraphic{And3}}{The architecture described by the Haskell description.}
     \stopcombination
 
-  \note{This section should also mention hierarchy, top level functions and
+  \todo{This section should also mention hierarchy, top level functions and
   subcircuits}
 
   \section{Choice}
     Although describing components and connections allows us to describe a lot of
     hardware designs already, there is an obvious thing missing: Choice. We
     need some way to be able to choose between values based on another value.
-    In Haskell, choice is achieved by \hs{case} expressions, \hs{if} expressions or
-    pattern matching.
+    In Haskell, choice is achieved by \hs{case} expressions, \hs{if}
+    expressions, pattern matching and guards.
 
     An obvious way to add choice to our language without having to recognize
     any of Haskell's syntax, would be to add a primivite \quote{\hs{if}}
@@ -129,8 +130,9 @@ and3 a b c = and (and a b) c
 
     \startbuffer[CaseInv]
     inv :: Bool -> Bool
-    inv True  = False
-    inv False = True
+    inv x = case x of
+      True -> False
+      False -> True
     \stopbuffer
 
     \startuseMPgraphic{CaseInv}
@@ -186,7 +188,7 @@ and3 a b c = and (and a b) c
 
     \placeexample[here][ex:PatternInv]{Simple inverter using pattern matching.
     Describes the same architecture as \in{example}[ex:CaseInv].}
-        {\typebufferhs{CaseInv}}
+        {\typebufferhs{PatternInv}}
 
     The architecture described by \in{example}[ex:PatternInv] is of course the
     same one as the one in \in{example}[ex:CaseInv]. The general interpretation
@@ -296,7 +298,7 @@ and3 a b c = and (and a b) c
         To define an index for the 8 element vector above, we would do:
 
         \starthaskell
-        type Register = RangedWord D7
+        type RegisterIndex = RangedWord D7
         \stophaskell
 
         Here, a type synonym \hs{RegisterIndex} is defined that is equal to
@@ -312,16 +314,20 @@ and3 a b c = and (and a b) c
     \subsection{User-defined types}
       There are three ways to define new types in Haskell: Algebraic
       datatypes with the \hs{data} keyword, type synonyms with the \hs{type}
-      keyword and type renamings with the \hs{newtype} keyword. This
-      explicitly excludes more advanced type creation from \GHC extensions
-      such as type families, existential typing, \small{GADT}s, etc.
-
-      The first of these actually introduces a new type, for which we provide
-      the \VHDL translation below. The latter two only define new names for
+      keyword and type renamings with the \hs{newtype} keyword. \GHC
+      offers a few more advanced ways to introduce types (type families,
+      existential typing, \small{GADT}s, etc.) which are not standard
+      Haskell.  These will be left outside the scope of this research.
+
+      Only an algebraic datatype declaration actually introduces a
+      completely new type, for which we provide the \VHDL translation
+      below. Type synonyms and renamings only define new names for
       existing types (where synonyms are completely interchangeable and
-      renamings need explicit conversion). Therefore, these don't need any
-      particular \VHDL translation, a synonym or renamed type will just use
-      the same representation as the equivalent type.
+      renamings need explicit conversion). Therefore, these don't need
+      any particular \VHDL translation, a synonym or renamed type will
+      just use the same representation as the original type. The
+      distinction between a renaming and a synonym does no longer matter
+      in hardware and can be disregarded in the generated \VHDL.
 
       For algebraic types, we can make the following distinction:
 
@@ -332,16 +338,18 @@ and3 a b c = and (and a b) c
         structure. In fact, the builtin tuple types are just algebraic product
         types (and are thus supported in exactly the same way).
 
-        The "product" in its name refers to the collection of values belonging
+        The \quote{product} in its name refers to the collection of values belonging
         to this type. The collection for a product type is the cartesian
         product of the collections for the types of its fields.
 
-        These types are translated to \VHDL, record types, with one field for
+        These types are translated to \VHDL record types, with one field for
         every field in the constructor. This translation applies to all single
-        constructor algebraic datatypes, including those with no fields (unit
-        types) and just one field (which are technically not a product).
+        constructor algebraic datatypes, including those with just one
+        field (which are technically not a product, but generate a VHDL
+        record for implementation simplicity).
       \stopdesc
       \startdesc{Enumerated types}
+        \defref{enumerated types}
         An enumerated type is an algebraic datatype with multiple constructors, but
         none of them have fields. This is essentially a way to get an
         enum-like type containing alternatives.
@@ -360,6 +368,10 @@ and3 a b c = and (and a b) c
         for our purposes this distinction does not really make a difference,
         so we'll leave it out.
 
+        The \quote{sum} in its name refers again to the collection of values
+        belonging to this type. The collection for a sum type is the
+        union of the the collections for each of the constructors.
+
         Sum types are currently not supported by the prototype, since there is
         no obvious \VHDL alternative. They can easily be emulated, however, as
         we will see from an example:
@@ -384,14 +396,14 @@ and3 a b c = and (and a b) c
         last one if \hs{B}), all the other ones have no useful value.
 
         An obvious problem with this naive approach is the space usage: The
-        example above generates a fairly big \VHDL type. However, we can be
+        example above generates a fairly big \VHDL type. Since we can be
         sure that the two \hs{Word}s in the \hs{Sum} type will never be valid
-        at the same time, so this is a waste of space.
+        at the same time, this is a waste of space.
 
         Obviously, we could do some duplication detection here to reuse a
         particular field for another constructor, but this would only
         partially solve the problem. If I would, for example, have an array of
-        8 bits and a 8 bit unsiged word, these are different types and could
+        8 bits and an 8 bit unsiged word, these are different types and could
         not be shared. However, in the final hardware, both of these types
         would simply be 8 bit connections, so we have a 100\% size increase by
         not sharing these.
@@ -427,7 +439,7 @@ and3 a b c = and (and a b) c
       In general, we can say we can never properly translate recursive types:
       All recursive types have a potentially infinite value (even though in
       practice they will have a bounded value, there is no way for the
-      compiler to determine an upper bound on its size).
+      compiler to automatically determine an upper bound on its size).
 
   \subsection{Partial application}
   Now we've seen how to to translate application, choice and types, we will
@@ -510,12 +522,15 @@ quadruple n = mul (mul n)
     calls to the same function share the same machine code. Having more
     machine code has implications for speed (due to less efficient caching)
     and memory usage. For normal compilation, it is therefore important to
-    keep the amount of functions limited and maximize the code sharing.
+    keep the amount of functions limited and maximize the code sharing
+    (though there is a tradeoff between speed and memory usage here).
 
     When generating hardware, this is hardly an issue. Having more \quote{code
     sharing} does reduce the amount of \small{VHDL} output (Since different
     component instantiations still share the same component), but after
-    synthesis, the amount of hardware generated is not affected.
+    synthesis, the amount of hardware generated is not affected. This
+    means there is no tradeoff between speed and memory (or rather,
+    chip area) usage.
 
     In particular, if we would duplicate all functions so that there is a
     separate function for every application in the program (\eg, each function
@@ -531,12 +546,13 @@ quadruple n = mul (mul n)
 
     \subsection{Specialization}
       \defref{specialization}
-      Given some function that has a \emph{domain} $D$ (\eg, the set of all
-      possible arguments that could be applied), we create a specialized
-      function with exactly the same behaviour, but with a domain $D' \subset
-      D$. This subset can be chosen in all sorts of ways. Any subset is valid
-      for the general definition of specialization, but in practice only some
-      of them provide useful optimization opportunities.
+      Given some function that has a \emph{domain} $D$ (\eg, the set of
+      all possible arguments that the function could be applied to), we
+      create a specialized function with exactly the same behaviour, but
+      with a domain $D' \subset D$. This subset can be chosen in all
+      sorts of ways. Any subset is valid for the general definition of
+      specialization, but in practice only some of them provide useful
+      optimization opportunities.
 
       Common subsets include limiting a polymorphic argument to a single type
       (\ie, removing polymorphism) or limiting an argument to just a single
@@ -599,8 +615,8 @@ quadruple n = mul (mul n)
     many wires will you lay down for a value that could have any type? When
     type classes are involved, what hardware components will you lay down for
     a class method (whose behaviour depends on the type of its arguments)?
-    Note that the language currently does not allow user-defined typeclasses,
-    but does support partly some of the builtin typeclasses (like \hs{Num}).
+    Note that Cλash currently does not allow user-defined typeclasses,
+    but does partly support some of the builtin typeclasses (like \hs{Num}).
 
     Fortunately, we can again use the principle of specialization: Since every
     function application generates a separate piece of hardware, we can know
@@ -615,7 +631,7 @@ quadruple n = mul (mul n)
     specialized to work just for these specific types, removing the
     polymorphism from the applied functions as well.
 
-    Our top level function must not have a polymorphic type (otherwise we
+    \defref{top level function}Our top level function must not have a polymorphic type (otherwise we
     wouldn't know the hardware interface to our top level function).
 
     By induction, this means that all functions that are (indirectly) called
@@ -648,7 +664,7 @@ quadruple n = mul (mul n)
       \todo{Define pure}
 
       This is a perfect match for a combinatoric circuit, where the output
-      also soley depends on the inputs. However, when state is involved, this
+      also solely depends on the inputs. However, when state is involved, this
       no longer holds. Since we're in charge of our own language (or at least
       let's pretend we aren't using Haskell and we are), we could remove this
       purity constraint and allow a function to return different values
@@ -753,7 +769,7 @@ acc in = out
         connected to one of the adder inputs).
 
         This notation has a number of downsides, amongst which are limited
-        readability and ambiguity in the interpretation. \note{Reference
+        readability and ambiguity in the interpretation. \todo{Reference
         Christiaan, who has done further investigation}
         
       \subsubsection{Explicit state arguments and results}
@@ -764,7 +780,7 @@ acc in = out
         the current state is now an argument.
 
         In Haskell, this would look like
-        \in{example}[ex:ExplicitAcc]\footnote[notfinalsyntax]{Note that this example is not in the final
+        \in{example}[ex:ExplicitAcc]\footnote[notfinalsyntax]{This example is not in the final
   Cλash syntax}. \todo{Referencing notfinalsyntax from Introduction.tex doesn't
   work}
 
@@ -788,7 +804,7 @@ acc in s = (s', out)
         variables are used by a function can be completely determined from its
         type signature (as opposed to the stream approach, where a function
         looks the same from the outside, regardless of what state variables it
-        uses (or whether it's stateful at all).
+        uses or whether it's stateful at all).
 
         This approach is the one chosen for Cλash and will be examined more
         closely below.
@@ -803,7 +819,9 @@ acc in s = (s', out)
         has to somehow know the current state for these called functions. The
         only way to do this, is to put these \emph{substates} inside the
         caller's state. This means that a function's state is the sum of the
-        states of all functions it calls, and its own state.
+        states of all functions it calls, and its own state. This sum
+        can be obtained using something simple like a tuple, or possibly
+        custom algebraic types for clarity.
 
         This also means that the type of a function (at least the "state"
         part) is dependent on its own implementation and of the functions it
@@ -882,7 +900,7 @@ acc in s = (s', out)
 
         \todo{Sidenote: One or more state arguments?}
 
-    \subsection{Explicit state annotation}
+    \subsection[sec:description:stateann]{Explicit state annotation}
       To make our stateful descriptions unambigious and easier to translate,
       we need some way for the developer to describe which arguments and
       results are intended to become stateful.
@@ -911,16 +929,12 @@ acc in s = (s', out)
 
   \section[sec:recursion]{Recursion}
   An import concept in functional languages is recursion. In it's most basic
-  form, recursion is a definition that is defined in terms of itself. A
+  form, recursion is a definition that is described in terms of itself. A
   recursive function is thus a function that uses itself in its body. 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
@@ -933,7 +947,7 @@ acc in s = (s', out)
   cycle (at best, we could generate hardware that needs an infinite number of
   cycles to complete).
   
-  However, most recursive hardware descriptions will describe finite
+  However, most recursive definitions will describe finite
   recursion. This is because the recursive call is done conditionally. There
   is usually a \hs{case} expression where at least one alternative does not contain
   the recursive call, which we call the "base case". If, for each call to the
@@ -962,12 +976,13 @@ acc in s = (s', out)
       False -> head xs + sum (tail xs)
   \stophaskell
 
-  However, the Haskell typechecker will now use the following reasoning (element
-  type of the vector is left out). Below, we write conditions on type
-  variables before the \hs{=>} operator. This is not completely valid Haskell
-  syntax, but serves to illustrate the typechecker reasoning. Also note that a
-  vector can never have a negative length, so \hs{Vector n} implicitly means
-  \hs{(n >= 0) => Vector n}.
+  However, the Haskell typechecker will now use the following reasoning.
+  For simplicity, the element type of a vector is left out, all vectors
+  are assumed to have the same element type. Below, we write conditions
+  on type variables before the \hs{=>} operator. This is not completely
+  valid Haskell syntax, but serves to illustrate the typechecker
+  reasoning. Also note that a vector can never have a negative length,
+  so \hs{Vector n} implicitly means \hs{(n >= 0) => Vector n}.
 
   \todo{This typechecker disregards the type signature}
   \startitemize
@@ -984,28 +999,21 @@ acc in s = (s', out)
   \stopitemize
 
   As you can see, using a simple \hs{case} expression  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.
-
-  \note{This should reference Christiaan}
-
-  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.
-  
-  \todo{Expand on this decision a bit}
+  the type checker to always typecheck both alternatives, which can't be
+  done! The typechecker is unable to distinguish the two case
+  alternatives (this is partly possible using \small{GADT}s, but that
+  approach faced other problems \todo{ref christiaan?}).
+
+  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).
+
+  \todo{This should reference Christiaan}
+
   \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
@@ -1017,5 +1025,12 @@ acc in s = (s', out)
   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 and limited time available, we leave other forms
-  of recursion as future work as well.
+  Evaluating all possible (and non-possible) ways to add recursion to
+  our descriptions, it seems better to limit the scope of this research
+  to exclude recursion. This allows for focusing on other interesting
+  areas instead. By including (builtin) support for a number of higher
+  order functions like \hs{map} and \hs{fold}, we can still express most
+  of the things we would use (list) recursion for.
+  
+
+% vim: set sw=2 sts=2 expandtab: