Fix references to the inverter examples.
[matthijs/master-project/report.git] / Chapters / HardwareDescription.tex
1 \chapter[chap:description]{Hardware description}
2   In this chapter an overview will be provided of the hardware
3   description language that was created and the issues that have arisen
4   in the process. The focus will be on the issues of the language, not
5   the implementation. The prototype implementation will be discussed in
6   \in{chapter}[chap:prototype].
7
8   To translate Haskell to hardware, every Haskell construct needs a
9   translation to \VHDL. There are often multiple valid translations
10   possible. When faced with choices, the most obvious choice has been
11   chosen wherever possible. In a lot of cases, when a programmer looks
12   at a functional hardware description it is completely clear what
13   hardware is described. We want our translator to generate exactly that
14   hardware whenever possible, to make working with Cλash as intuitive as
15   possible.
16    
17   \placeintermezzo{}{
18     \defref{reading examples}
19     \startframedtext[width=9cm,background=box,frame=no]
20     \startalignment[center]
21       {\tfa Reading the examples}
22     \stopalignment
23     \blank[medium]
24       In this thesis, a lot of functional code will be presented. Part of this
25       will be valid Cλash code, but others will just be small Haskell or Core
26       snippets to illustrate a concept.
27
28       In these examples, some functions and types will be used, without
29       properly defining every one of them. These functions (like \hs{and},
30       \hs{not}, \hs{add}, \hs{+}, etc.) and types (like \hs{Bit}, \hs{Word},
31       \hs{Bool}, etc.) are usually pretty self-explanatory.
32
33       The special type \hs{[t]} means \quote{list of \hs{t}'s}, where \hs{t}
34       can be any other type.
35
36       Of particular note is the use of the \hs{::} operator. It is used in
37       Haskell to explicitly declare the type of function or let binding. In
38       these examples and the text, we will occasionally use this operator to
39       show the type of arbitrary expressions, even where this would not
40       normally be valid. Just reading the \hs{::} operator as \quote{and also
41       note that \emph{this} expression has \emph{this} type} should work out.
42     \stopframedtext
43   }
44
45   In this chapter we describe how to interpret a Haskell program from a
46   hardware perspective. We provide a description of each Haskell language
47   element that needs translation, to provide a clear picture of what is
48   supported and how.
49
50
51   \section[sec:description:application]{Function application}
52   The basic syntactic elements of a functional program are functions and
53   function application. These have a single obvious \small{VHDL}
54   translation: each top level function becomes a hardware component, where each
55   argument is an input port and the result value is the (single) output
56   port. This output port can have a complex type (such as a tuple), so
57   having just a single output port does not pose a limitation.
58
59   Each function application in turn becomes component instantiation. Here, the
60   result of each argument expression is assigned to a signal, which is mapped
61   to the corresponding input port. The output port of the function is also
62   mapped to a signal, which is used as the result of the application.
63
64   Since every top level function generates its own component, the
65   hierarchy of of function calls is reflected in the final \VHDL\ output
66   as well, creating a hierarchical \VHDL\ description of the hardware.
67   This separation in different components makes the resulting \VHDL\
68   output easier to read and debug.
69
70   \in{Example}[ex:And3] shows a simple program using only function
71   application and the corresponding architecture.
72
73 \startbuffer[And3]
74 -- A simple function that returns 
75 -- conjunction of three bits
76 and3 :: Bit -> Bit -> Bit -> Bit
77 and3 a b c = and (and a b) c
78 \stopbuffer
79
80   \startuseMPgraphic{And3}
81     save a, b, c, anda, andb, out;
82
83     % I/O ports
84     newCircle.a(btex $a$ etex) "framed(false)";
85     newCircle.b(btex $b$ etex) "framed(false)";
86     newCircle.c(btex $c$ etex) "framed(false)";
87     newCircle.out(btex $out$ etex) "framed(false)";
88
89     % Components
90     newCircle.anda(btex $and$ etex);
91     newCircle.andb(btex $and$ etex);
92
93     a.c    = origin;
94     b.c    = a.c + (0cm, 1cm);
95     c.c    = b.c + (0cm, 1cm);
96     anda.c = midpoint(a.c, b.c) + (2cm, 0cm);
97     andb.c = midpoint(b.c, c.c) + (4cm, 0cm);
98
99     out.c   = andb.c + (2cm, 0cm);
100
101     % Draw objects and lines
102     drawObj(a, b, c, anda, andb, out);
103
104     ncarc(a)(anda) "arcangle(-10)";
105     ncarc(b)(anda);
106     ncarc(anda)(andb);
107     ncarc(c)(andb);
108     ncline(andb)(out);
109   \stopuseMPgraphic
110
111   \startbuffer[And3VHDL]
112     entity and3Component_0 is
113          port (\azMyG2\ : in std_logic;
114                \bzMyI2\ : in std_logic;
115                \czMyK2\ : in std_logic;
116                \foozMySzMyS2\ : out std_logic;
117                clock : in std_logic;
118                resetn : in std_logic);
119     end entity and3Component_0;
120
121
122     architecture structural of and3Component_0 is
123          signal \argzMyMzMyM2\ : std_logic;
124     begin
125          \argzMyMzMyM2\ <= \azMyG2\ and \bzMyI2\;
126
127          \foozMySzMyS2\ <= \argzMyMzMyM2\ and \czMyK2\;
128     end architecture structural;
129   \stopbuffer
130
131   \placeexample[][ex:And3]{Simple three input and gate.}
132     \startcombination[2*1]
133       {\typebufferhs{And3}}{Haskell description using function applications.}
134       {\boxedgraphic{And3}}{The architecture described by the Haskell description.}
135     \stopcombination
136
137   \placeexample[][ex:And3VHDL]{\VHDL\ generated for \hs{and3} from \in{example}[ex:And3]}
138       {\typebuffervhdl{And3VHDL}}
139
140   \placeintermezzo{}{
141     \defref{top level binder}
142     \defref{top level function}
143     \startframedtext[width=8cm,background=box,frame=no]
144     \startalignment[center]
145       {\tfa Top level binders and functions}
146     \stopalignment
147     \blank[medium]
148       A top level binder is any binder (variable) that is declared in
149       the \quote{global} scope of a Haskell program (as opposed to a
150       binder that is bound inside a function.
151
152       In Haskell, there is no sharp distinction between a variable and a
153       function: a function is just a variable (binder) with a function
154       type. This means that a top level function is just any top level
155       binder with a function type.
156
157       As an example, consider the following Haskell snippet:
158
159       \starthaskell
160         foo :: Int -> Int
161         foo x = inc x
162           where
163             inc = \y -> y + 1
164       \stophaskell
165
166       Here, \hs{foo} is a top level binder, whereas \hs{inc} is a
167       function (since it is bound to a lambda extraction, indicated by
168       the backslash) but is not a top level binder or function.  Since
169       the type of \hs{foo} is a function type, namely \hs{Int -> Int},
170       it is also a top level function.
171     \stopframedtext
172   }
173   \section{Choice}
174     Although describing components and connections allows us to describe a lot of
175     hardware designs already, there is an obvious thing missing: choice. We
176     need some way to be able to choose between values based on another value.
177     In Haskell, choice is achieved by \hs{case} expressions, \hs{if}
178     expressions, pattern matching and guards.
179
180     An obvious way to add choice to our language without having to recognize
181     any of Haskell's syntax, would be to add a primivite \quote{\hs{if}}
182     function. This function would take three arguments: the condition, the
183     value to return when the condition is true and the value to return when
184     the condition is false.
185
186     This \hs{if} function would then essentially describe a multiplexer and
187     allows us to describe any architecture that uses multiplexers.
188
189     However, to be able to describe our hardware in a more convenient way, we
190     also want to translate Haskell's choice mechanisms. The easiest of these
191     are of course case expressions (and \hs{if} expressions, which can be very
192     directly translated to \hs{case} expressions). A \hs{case} expression can in turn
193     simply be translated to a conditional assignment, where the conditions use
194     equality comparisons against the constructors in the \hs{case} expressions.
195
196     In \in{example}[ex:Inv] two versions of an inverter are shown. The first
197     uses a simple \hs{case} expression, scrutinizing a boolean value.  The
198     corresponding architecture has a comparator to determine which of the
199     constructors is on the \hs{in} input. There is a multiplexer to select the
200     output signal (which is just a conditional assignment in the generated
201     \VHDL). The two options for the output signals are just constants,
202     but these could have been more complex expressions (in which case also
203     both of them would be working in parallel, regardless of which output
204     would be chosen eventually). The \VHDL\ generated for (both versions of)
205     this inverter is shown in \in{example}[ex:InvVHDL].
206
207     If we would translate a Boolean to a bit value, we could of course remove
208     the comparator and directly feed 'in' into the multiplexer (or even use an
209     inverter instead of a multiplexer).  However, we will try to make a
210     general translation, which works for all possible \hs{case} expressions.
211     Optimizations such as these are left for the \VHDL\ synthesizer, which
212     handles them very well.
213
214     \placeintermezzo{}{
215       \startframedtext[width=8cm,background=box,frame=no]
216       \startalignment[center]
217         {\tfa Arguments / results vs. inputs / outputs}
218       \stopalignment
219       \blank[medium]
220         Due to the translation chosen for function application, there is a
221         very strong relation between arguments, results, inputs and outputs.
222         For clarity, the former two will always refer to the arguments and
223         results in the functional description (either Haskell or Core). The
224         latter two will refer to input and output ports in the generated
225         \VHDL.
226
227         Even though these concepts seem to be nearly identical, when stateful
228         functions are introduces we will see arguments and results that will
229         not get translated into input and output ports, making this
230         distinction more important.
231       \stopframedtext
232     }
233
234     A slightly more complex (but very powerful) form of choice is pattern
235     matching. A function can be defined in multiple clauses, where each clause
236     specifies a pattern. When the arguments match the pattern, the
237     corresponding clause will be used.
238
239     \in{Example}[ex:Inv] also shows an inverter that uses pattern matching.
240     The architecture it describes is of course the
241     same one as the description with a case expression. The general interpretation
242     of pattern matching is also similar to that of \hs{case} expressions: generate
243     hardware for each of the clauses (like each of the clauses of a \hs{case}
244     expression) and connect them to the function output through (a number of
245     nested) multiplexers. These multiplexers are driven by comparators and
246     other logic, that check each pattern in turn.
247
248     In these examples we have seen only binary case expressions and pattern
249     matches (\ie, with two alternatives). In practice, case expressions can
250     choose between more than two values, resulting in a number of nested
251     multiplexers.
252
253     \startbuffer[CaseInv]
254     inv :: Bool -> Bool
255     inv x = case x of
256       True -> False
257       False -> True
258     \stopbuffer
259
260     \startbuffer[PatternInv]
261     inv :: Bool -> Bool
262     inv True = False
263     inv False = True
264     \stopbuffer
265
266     \startuseMPgraphic{Inv}
267       save in, truecmp, falseout, trueout, out, cmp, mux;
268
269       % I/O ports
270       newCircle.in(btex $in$ etex) "framed(false)";
271       newCircle.out(btex $out$ etex) "framed(false)";
272       % Constants
273       newBox.truecmp(btex $True$ etex) "framed(false)";
274       newBox.trueout(btex $True$ etex) "framed(false)";
275       newBox.falseout(btex $False$ etex) "framed(false)";
276
277       % Components
278       newCircle.cmp(btex $==$ etex);
279       newMux.mux;
280
281       in.c       = origin;
282       cmp.c      = in.c + (3cm, 0cm);
283       truecmp.c  = cmp.c + (-1cm, 1cm);
284       mux.sel    = cmp.e + (1cm, -1cm);
285       falseout.c = mux.inpa - (2cm, 0cm);
286       trueout.c  = mux.inpb - (2cm, 0cm);
287       out.c      = mux.out + (2cm, 0cm);
288
289       % Draw objects and lines
290       drawObj(in, out, truecmp, trueout, falseout, cmp, mux);
291
292       ncline(in)(cmp);
293       ncarc(truecmp)(cmp);
294       nccurve(cmp.e)(mux.sel) "angleA(0)", "angleB(-90)";
295       ncline(falseout)(mux) "posB(inpa)";
296       ncline(trueout)(mux) "posB(inpb)";
297       ncline(mux)(out) "posA(out)";
298     \stopuseMPgraphic
299     
300     \startbuffer[InvVHDL]
301       entity invComponent_0 is
302            port (\xzAMo2\ : in boolean;
303                  \reszAMuzAMu2\ : out boolean;
304                  clock : in std_logic;
305                  resetn : in std_logic);
306       end entity invComponent_0;
307
308
309       architecture structural of invComponent_0 is
310       begin
311            \reszAMuzAMu2\ <= false when \xzAMo2\ = true else
312                              true;
313       end architecture structural; 
314     \stopbuffer
315
316     \placeexample[][ex:Inv]{Simple inverter.}{
317       % Use placesidebyside, since nesting combinations doesn't seem to work
318       % here. This does break centering, but well...
319       \placesidebyside
320         % Use 2*2 instead of 1*2 to insert some extra space (\placesidebyside
321         % places stuff very close together)
322         {\startcombination[2*2]
323           {\typebufferhs{CaseInv}}{Haskell description using a Case expression.}
324           {}{}
325           {\typebufferhs{PatternInv}}{Haskell description using Pattern matching expression.}
326           {}{}
327         \stopcombination}
328         % Use a 1*1 combination to add a caption
329         {\startcombination[1*1]
330           {\boxedgraphic{Inv}}{The architecture described by the Haskell descriptions.}
331         \stopcombination}
332       }
333
334 %    \placeexample[][ex:Inv]{Simple inverter.}{
335 %        \startcombination[2*2]
336 %          {\typebufferhs{CaseInv}}{Haskell description using a Case expression.}
337 %          {}{}
338 %          {\typebufferhs{PatternInv}}{Haskell description using Pattern matching expression.}
339 %          {\boxedgraphic{Inv}}{The architecture described by the Haskell description.}
340 %        \stopcombination
341 %    }
342     \placeexample[][ex:InvVHDL]{\VHDL\ generated for (both versions of) \hs{inv} from \in{example}[ex:Inv]}
343         {\typebuffervhdl{InvVHDL}}
344
345   \section{Types}
346     Translation of two most basic functional concepts has been
347     discussed: function application and choice. Before looking further
348     into less obvious concepts like higher-order expressions and
349     polymorphism, the possible types that can be used in hardware
350     descriptions will be discussed.
351
352     Some way is needed to translate every values used to its hardware
353     equivalents. In particular, this means a hardware equivalent for
354     every \emph{type} used in a hardware description is needed
355
356     Since most functional languages have a lot of standard types that
357     are hard to translate (integers without a fixed size, lists without
358     a static length, etc.), a number of \quote{built-in} types will be
359     defined first. These types are built-in in the sense that our
360     compiler will have a fixed VHDL type for these. User defined types,
361     on the other hand, will have their hardware type derived directly
362     from their Haskell declaration automatically, according to the rules
363     sketched here.
364
365     \todo{Introduce Haskell type syntax (type constructors, type application,
366     :: operator?)}
367
368     \subsection{Built-in types}
369       The language currently supports the following built-in types. Of these,
370       only the \hs{Bool} type is supported by Haskell out of the box (the
371       others are defined by the Cλash package, so they are user-defined types
372       from Haskell's point of view).
373
374       \startdesc{\hs{Bit}}
375         This is the most basic type available. It is mapped directly onto
376         the \type{std_logic} \small{VHDL} type. Mapping this to the
377         \type{bit} type might make more sense (since the Haskell version
378         only has two values), but using \type{std_logic} is more standard
379         (and allowed for some experimentation with don't care values)
380
381         \todo{Sidenote bit vs stdlogic}
382       \stopdesc
383       \startdesc{\hs{Bool}}
384         This is the only built-in Haskell type supported and is translated
385         exactly like the Bit type (where a value of \hs{True} corresponds to a
386         value of \hs{High}). Supporting the Bool type is particularly
387         useful to support \hs{if ... then ... else ...} expressions, which
388         always have a \hs{Bool} value for the condition.
389
390         A \hs{Bool} is translated to a \type{std_logic}, just like \hs{Bit}.
391       \stopdesc
392       \startdesc{\hs{SizedWord}, \hs{SizedInt}}
393         These are types to represent integers. A \hs{SizedWord} is unsigned,
394         while a \hs{SizedInt} is signed. These types are parameterized by a
395         length type, so you can define an unsigned word of 32 bits wide as
396         follows:
397         
398         \starthaskell
399           type Word32 = SizedWord D32
400         \stophaskell
401
402         Here, a type synonym \hs{Word32} is defined that is equal to the
403         \hs{SizedWord} type constructor applied to the type \hs{D32}. \hs{D32}
404         is the \emph{type level representation} of the decimal number 32,
405         making the \hs{Word32} type a 32-bit unsigned word.
406
407         These types are translated to the \small{VHDL} \type{unsigned} and
408         \type{signed} respectively.
409         \todo{Sidenote on dependent typing?}
410       \stopdesc
411       \startdesc{\hs{Vector}}
412         This is a vector type, that can contain elements of any other type and
413         has a fixed length. It has two type parameters: its
414         length and the type of the elements contained in it. By putting the
415         length parameter in the type, the length of a vector can be determined
416         at compile time, instead of only at runtime for conventional lists.
417
418         The \hs{Vector} type constructor takes two type arguments: the length
419         of the vector and the type of the elements contained in it. The state
420         type of an 8 element register bank would then for example be:
421
422         \starthaskell
423         type RegisterState = Vector D8 Word32
424         \stophaskell
425
426         Here, a type synonym \hs{RegisterState} is defined that is equal to
427         the \hs{Vector} type constructor applied to the types \hs{D8} (The type
428         level representation of the decimal number 8) and \hs{Word32} (The 32
429         bit word type as defined above). In other words, the
430         \hs{RegisterState} type is a vector of 8 32-bit words.
431
432         A fixed size vector is translated to a \small{VHDL} array type.
433       \stopdesc
434       \startdesc{\hs{RangedWord}}
435         This is another type to describe integers, but unlike the previous
436         two it has no specific bitwidth, but an upper bound. This means that
437         its range is not limited to powers of two, but can be any number.
438         A \hs{RangedWord} only has an upper bound, its lower bound is
439         implicitly zero. There is a lot of added implementation complexity
440         when adding a lower bound and having just an upper bound was enough
441         for the primary purpose of this type: typesafely indexing vectors.
442
443         To define an index for the 8 element vector above, we would do:
444
445         \starthaskell
446         type RegisterIndex = RangedWord D7
447         \stophaskell
448
449         Here, a type synonym \hs{RegisterIndex} is defined that is equal to
450         the \hs{RangedWord} type constructor applied to the type \hs{D7}. In
451         other words, this defines an unsigned word with values from
452         {\definedfont[Serif*normalnum]0 to 7} (inclusive). This word can be be used to index the
453         8 element vector \hs{RegisterState} above.
454
455         This type is translated to the \type{unsigned} \small{VHDL} type.
456       \stopdesc
457
458       The integer and vector built-in types are discussed in more detail
459       in \cite[baaij09].
460
461     \subsection{User-defined types}
462       There are three ways to define new types in Haskell: algebraic
463       datatypes with the \hs{data} keyword, type synonyms with the \hs{type}
464       keyword and type renamings with the \hs{newtype} keyword. \GHC\
465       offers a few more advanced ways to introduce types (type families,
466       existential typing, \small{GADT}s, etc.) which are not standard
467       Haskell.  These will be left outside the scope of this research.
468
469       Only an algebraic datatype declaration actually introduces a
470       completely new type, for which we provide the \VHDL\ translation
471       below. Type synonyms and renamings only define new names for
472       existing types (where synonyms are completely interchangeable and
473       renamings need explicit conversion). Therefore, these do not need
474       any particular \VHDL\ translation, a synonym or renamed type will
475       just use the same representation as the original type. The
476       distinction between a renaming and a synonym does no longer matter
477       in hardware and can be disregarded in the generated \VHDL.
478
479       For algebraic types, we can make the following distinction:
480
481       \startdesc{Product types}
482         A product type is an algebraic datatype with a single constructor with
483         two or more fields, denoted in practice like (a,b), (a,b,c), etc. This
484         is essentially a way to pack a few values together in a record-like
485         structure. In fact, the built-in tuple types are just algebraic product
486         types (and are thus supported in exactly the same way).
487
488         The \quote{product} in its name refers to the collection of values belonging
489         to this type. The collection for a product type is the Cartesian
490         product of the collections for the types of its fields.
491
492         These types are translated to \VHDL\ record types, with one field for
493         every field in the constructor. This translation applies to all single
494         constructor algebraic datatypes, including those with just one
495         field (which are technically not a product, but generate a VHDL
496         record for implementation simplicity).
497       \stopdesc
498       \startdesc{Enumerated types}
499         \defref{enumerated types}
500         An enumerated type is an algebraic datatype with multiple constructors, but
501         none of them have fields. This is essentially a way to get an
502         enum-like type containing alternatives.
503
504         Note that Haskell's \hs{Bool} type is also defined as an
505         enumeration type, but we have a fixed translation for that.
506         
507         These types are translated to \VHDL\ enumerations, with one value for
508         each constructor. This allows references to these constructors to be
509         translated to the corresponding enumeration value.
510       \stopdesc
511       \startdesc{Sum types}
512         A sum type is an algebraic datatype with multiple constructors, where
513         the constructors have one or more fields. Technically, a type with
514         more than one field per constructor is a sum of products type, but
515         for our purposes this distinction does not really make a
516         difference, so this distinction is note made.
517
518         The \quote{sum} in its name refers again to the collection of values
519         belonging to this type. The collection for a sum type is the
520         union of the the collections for each of the constructors.
521
522         Sum types are currently not supported by the prototype, since there is
523         no obvious \VHDL\ alternative. They can easily be emulated, however, as
524         we will see from an example:
525
526         \starthaskell
527         data Sum = A Bit Word | B Word 
528         \stophaskell
529
530         An obvious way to translate this would be to create an enumeration to
531         distinguish the constructors and then create a big record that
532         contains all the fields of all the constructors. This is the same
533         translation that would result from the following enumeration and
534         product type (using a tuple for clarity):
535
536         \starthaskell
537         data SumC = A | B
538         type Sum = (SumC, Bit, Word, Word)
539         \stophaskell
540
541         Here, the \hs{SumC} type effectively signals which of the latter three
542         fields of the \hs{Sum} type are valid (the first two if \hs{A}, the
543         last one if \hs{B}), all the other ones have no useful value.
544
545         An obvious problem with this naive approach is the space usage: the
546         example above generates a fairly big \VHDL\ type. Since we can be
547         sure that the two \hs{Word}s in the \hs{Sum} type will never be valid
548         at the same time, this is a waste of space.
549
550         Obviously, duplication detection could be used to reuse a
551         particular field for another constructor, but this would only
552         partially solve the problem. If two fields would be, for
553         example, an array of 8 bits and an 8 bit unsiged word, these are
554         different types and could not be shared. However, in the final
555         hardware, both of these types would simply be 8 bit connections,
556         so we have a 100\% size increase by not sharing these.
557       \stopdesc
558
559       Another interesting case is that of recursive types. In Haskell, an
560       algebraic datatype can be recursive: any of its field types can be (or
561       contain) the type being defined. The most well-known recursive type is
562       probably the list type, which is defined is:
563       
564       \starthaskell
565       data List t = Empty | Cons t (List t)
566       \stophaskell
567
568       Note that \hs{Empty} is usually written as \hs{[]} and \hs{Cons} as
569       \hs{:}, but this would make the definition harder to read.  This
570       immediately shows the problem with recursive types: what hardware type
571       to allocate here? 
572       
573       If the naive approach for sum types described above would be used,
574       a record would be created where the first field is an enumeration
575       to distinguish \hs{Empty} from \hs{Cons}. Furthermore, two more
576       fields would be added: one with the (\VHDL\ equivalent of) type
577       \hs{t} (assuming this type is actually known at compile time, this
578       should not be a problem) and a second one with type \hs{List t}.
579       The latter one is of course a problem: this is exactly the type
580       that was to be translated in the first place.
581       
582       The resulting \VHDL\ type will thus become infinitely deep. In
583       other words, there is no way to statically determine how long
584       (deep) the list will be (it could even be infinite).
585       
586       In general, recursive types can never be properly translated: all
587       recursive types have a potentially infinite value (even though in
588       practice they will have a bounded value, there is no way for the
589       compiler to automatically determine an upper bound on its size).
590
591   \subsection{Partial application}
592   Now the translation of application, choice and types has been
593   discussed, a more complex concept can be considered: partial
594   applications. A \emph{partial application} is any application whose
595   (return) type is (again) a function type.
596
597   From this, it should be clear that the translation rules for full
598   application does not apply to a partial application: there are not
599   enough values for all the input ports in the resulting \VHDL.
600   \in{Example}[ex:Quadruple] shows an example use of partial application
601   and the corresponding architecture.
602
603 \startbuffer[Quadruple]
604 -- Multiply the input word by four.
605 quadruple :: Word -> Word
606 quadruple n = mul (mul n)
607   where
608     mul = (*) 2
609 \stopbuffer
610
611   \startuseMPgraphic{Quadruple}
612     save in, two, mula, mulb, out;
613
614     % I/O ports
615     newCircle.in(btex $n$ etex) "framed(false)";
616     newCircle.two(btex $2$ etex) "framed(false)";
617     newCircle.out(btex $out$ etex) "framed(false)";
618
619     % Components
620     newCircle.mula(btex $\times$ etex);
621     newCircle.mulb(btex $\times$ etex);
622
623     two.c    = origin;
624     in.c     = two.c + (0cm, 1cm);
625     mula.c  = in.c + (2cm, 0cm);
626     mulb.c  = mula.c + (2cm, 0cm);
627     out.c   = mulb.c + (2cm, 0cm);
628
629     % Draw objects and lines
630     drawObj(in, two, mula, mulb, out);
631
632     nccurve(two)(mula) "angleA(0)", "angleB(45)";
633     nccurve(two)(mulb) "angleA(0)", "angleB(45)";
634     ncline(in)(mula);
635     ncline(mula)(mulb);
636     ncline(mulb)(out);
637   \stopuseMPgraphic
638
639   \placeexample[][ex:Quadruple]{Simple three port and.}
640     \startcombination[2*1]
641       {\typebufferhs{Quadruple}}{Haskell description using function applications.}
642       {\boxedgraphic{Quadruple}}{The architecture described by the Haskell description.}
643     \stopcombination
644
645   Here, the definition of mul is a partial function application: it applies
646   the function \hs{(*) :: Word -> Word -> Word} to the value \hs{2 :: Word},
647   resulting in the expression \hs{(*) 2 :: Word -> Word}. Since this resulting
648   expression is again a function, hardware cannot be generated for it
649   directly.  This is because the hardware to generate for \hs{mul}
650   depends completely on where and how it is used. In this example, it is
651   even used twice.
652
653   However, it is clear that the above hardware description actually
654   describes valid hardware. In general, any partial applied function
655   must eventually become completely applied, at which point hardware for
656   it can be generated using the rules for function application given in
657   \in{section}[sec:description:application]. It might mean that a
658   partial application is passed around quite a bit (even beyond function
659   boundaries), but eventually, the partial application will become
660   completely applied. An example of this principe is given in
661   \in{section}[sec:normalization:defunctionalization].
662
663   \section{Costless specialization}
664     Each (complete) function application in our description generates a
665     component instantiation, or a specific piece of hardware in the final
666     design. It is interesting to note that each application of a function
667     generates a \emph{separate} piece of hardware. In the final design, none
668     of the hardware is shared between applications, even when the applied
669     function is the same (of course, if a particular value, such as the result
670     of a function application, is used twice, it is not calculated twice).
671
672     This is distinctly different from normal program compilation: two separate
673     calls to the same function share the same machine code. Having more
674     machine code has implications for speed (due to less efficient caching)
675     and memory usage. For normal compilation, it is therefore important to
676     keep the amount of functions limited and maximize the code sharing
677     (though there is a tradeoff between speed and memory usage here).
678
679     When generating hardware, this is hardly an issue. Having more \quote{code
680     sharing} does reduce the amount of \small{VHDL} output (Since different
681     component instantiations still share the same component), but after
682     synthesis, the amount of hardware generated is not affected. This
683     means there is no tradeoff between speed and memory (or rather,
684     chip area) usage.
685
686     In particular, if we would duplicate all functions so that there is a
687     separate function for every application in the program (\eg, each function
688     is then only applied exactly once), there would be no increase in hardware
689     size whatsoever.
690     
691     Because of this, a common optimization technique called
692     \emph{specialization} can be applied to hardware generation without any
693     performance or area cost (unlike for software). 
694    
695    \fxnote{Perhaps these next three sections are a bit too
696    implementation-oriented?}
697
698     \subsection{Specialization}
699       \defref{specialization}
700       Given some function that has a \emph{domain} $D$ (\eg, the set of
701       all possible arguments that the function could be applied to), we
702       create a specialized function with exactly the same behaviour, but
703       with a domain $D' \subset D$. This subset can be chosen in all
704       sorts of ways. Any subset is valid for the general definition of
705       specialization, but in practice only some of them provide useful
706       optimization opportunities.
707
708       Common subsets include limiting a polymorphic argument to a single type
709       (\ie, removing polymorphism) or limiting an argument to just a single
710       value (\ie, cross-function constant propagation, effectively removing
711       the argument). 
712       
713       Since we limit the argument domain of the specialized function, its
714       definition can often be optimized further (since now more types or even
715       values of arguments are already known). By replacing any application of
716       the function that falls within the reduced domain by an application of
717       the specialized version, the code gets faster (but the code also gets
718       bigger, since we now have two versions instead of one). If we apply
719       this technique often enough, we can often replace all applications of a
720       function by specialized versions, allowing the original function to be
721       removed (in some cases, this can even give a net reduction of the code
722       compared to the non-specialized version).
723
724       Specialization is useful for our hardware descriptions for functions
725       that contain arguments that cannot be translated to hardware directly
726       (polymorphic or higher-order arguments, for example). If we can create
727       specialized functions that remove the argument, or make it translatable,
728       we can use specialization to make the original, untranslatable, function
729       obsolete.
730
731   \section{Higher order values}
732     What holds for partial application, can be easily generalized to any
733     higher-order expression. This includes partial applications, plain
734     variables (e.g., a binder referring to a top level function), lambda
735     expressions and more complex expressions with a function type (a \hs{case}
736     expression returning lambda's, for example).
737
738     Each of these values cannot be directly represented in hardware (just like
739     partial applications). Also, to make them representable, they need to be
740     applied: function variables and partial applications will then eventually
741     become complete applications, applied lambda expressions disappear by
742     applying β-reduction, etc.
743
744     So any higher-order value will be \quote{pushed down} towards its
745     application just like partial applications. Whenever a function boundary
746     needs to be crossed, the called function can be specialized.
747     
748     \fxnote{This section needs improvement and an example}
749
750   \section{Polymorphism}
751     In Haskell, values can be \emph{polymorphic}: they can have multiple types. For
752     example, the function \hs{fst :: (a, b) -> a} is an example of a
753     polymorphic function: it works for tuples with any two element types. Haskell
754     type classes allow a function to work on a specific set of types, but the
755     general idea is the same. The opposite of this is a \emph{monomorphic}
756     value, which has a single, fixed, type.
757
758 %    A type class is a collection of types for which some operations are
759 %    defined. It is thus possible for a value to be polymorphic while having
760 %    any number of \emph{class constraints}: the value is not defined for
761 %    every type, but only for types in the type class. An example of this is
762 %    the \hs{even :: (Integral a) => a -> Bool} function, which can map any
763 %    value of a type that is member of the \hs{Integral} type class 
764
765     When generating hardware, polymorphism cannot be easily translated. How
766     many wires will you lay down for a value that could have any type? When
767     type classes are involved, what hardware components will you lay down for
768     a class method (whose behaviour depends on the type of its arguments)?
769     Note that Cλash currently does not allow user-defined type classes,
770     but does partly support some of the built-in type classes (like \hs{Num}).
771
772     Fortunately, we can again use the principle of specialization: since every
773     function application generates a separate piece of hardware, we can know
774     the types of all arguments exactly. Provided that existential typing
775     (which is a \GHC\ extension) is not used typing, all of the
776     polymorphic types in a function must depend on the types of the
777     arguments (In other words, the only way to introduce a type variable
778     is in a lambda abstraction).
779
780     If a function is monomorphic, all values inside it are monomorphic as
781     well, so any function that is applied within the function can only be
782     applied to monomorphic values. The applied functions can then be
783     specialized to work just for these specific types, removing the
784     polymorphism from the applied functions as well.
785
786     \defref{entry function}The entry function must not have a
787     polymorphic type (otherwise no hardware interface could be generated
788     for the entry function).
789
790     By induction, this means that all functions that are (indirectly) called
791     by our top level function (meaning all functions that are translated in
792     the final hardware) become monomorphic.
793
794   \section{State}
795     A very important concept in hardware designs is \emph{state}. In a
796     stateless (or, \emph{combinational}) design, every output is  directly and solely dependent on the
797     inputs. In a stateful design, the outputs can depend on the history of
798     inputs, or the \emph{state}. State is usually stored in \emph{registers},
799     which retain their value during a clockcycle, and are typically updated at
800     the start of every clockcycle. Since the updating of the state is tightly
801     coupled (synchronized) to the clock signal, these state updates are often
802     called \emph{synchronous} behaviour.
803
804     \todo{Sidenote? Registers can contain any (complex) type}
805   
806     To make Cλash useful to describe more than simple combinational
807     designs, it needs to be able to describe state in some way.
808
809     \subsection{Approaches to state}
810       In Haskell, functions are always pure (except when using unsafe
811       functions with the \hs{IO} monad, which is not supported by Cλash). This
812       means that the output of a function solely depends on its inputs. If you
813       evaluate a given function with given inputs, it will always provide the
814       same output.
815
816       \placeintermezzo{}{
817         \defref{purity}
818         \startframedtext[width=8cm,background=box,frame=no]
819         \startalignment[center]
820           {\tfa Purity}
821         \stopalignment
822         \blank[medium]
823
824         A function is said to be pure if it satisfies two conditions:
825
826         \startitemize[KR]
827         \item When a pure function is called with the same arguments twice, it should
828         return the same value in both cases.
829         \item When a pure function is called, it should have not
830         observable side-effects.
831         \stopitemize
832
833         Purity is an important property in functional languages, since
834         it enables all kinds of mathematical reasoning and
835         optimizattions with pure functions, that are not guaranteed to
836         be correct for impure functions.
837
838         An example of a pure function is the square root function
839         \hs{sqrt}. An example of an impure function is the \hs{today}
840         function that returns the current date (which of course cannot
841         exist like this in Haskell).
842         \stopframedtext
843       }
844
845       This is a perfect match for a combinational circuit, where the output
846       also solely depends on the inputs. However, when state is involved, this
847       no longer holds. Of course this purity constraint cannot just be
848       removed from Haskell. But even when designing a completely new (hardware
849       description) language, it does not seem to be a good idea to
850       remove this purity. This would that all kinds of interesting properties of
851       the functional language get lost, and all kinds of transformations
852       and optimizations are no longer be meaning preserving.
853
854       So our functions must remain pure, meaning the current state has
855       to be present in the function's arguments in some way. There seem
856       to be two obvious ways to do this: adding the current state as an
857       argument, or including the full history of each argument.
858
859       \subsubsection{Stream arguments and results}
860         Including the entire history of each input (\eg, the value of that
861         input for each previous clockcycle) is an obvious way to make outputs
862         depend on all previous input. This is easily done by making every
863         input a list instead of a single value, containing all previous values
864         as well as the current value.
865
866         An obvious downside of this solution is that on each cycle, all the
867         previous cycles must be resimulated to obtain the current state. To do
868         this, it might be needed to have a recursive helper function as well,
869         which might be hard to be properly analyzed by the compiler.
870
871         A slight variation on this approach is one taken by some of the other
872         functional \small{HDL}s in the field: \todo{References to Lava,
873         ForSyDe, ...} Make functions operate on complete streams. This means
874         that a function is no longer called on every cycle, but just once. It
875         takes stream as inputs instead of values, where each stream contains
876         all the values for every clockcycle since system start. This is easily
877         modeled using an (infinite) list, with one element for each clock
878         cycle. Since the function is only evaluated once, its output must also
879         be a stream. Note that, since we are working with infinite lists and
880         still want to be able to simulate the system cycle-by-cycle, this
881         relies heavily on the lazy semantics of Haskell.
882
883         Since our inputs and outputs are streams, all other (intermediate)
884         values must be streams. All of our primitive operators (\eg, addition,
885         substraction, bitwise operations, etc.) must operate on streams as
886         well (note that changing a single-element operation to a stream
887         operation can done with \hs{map}, \hs{zipwith}, etc.).
888
889         This also means that primitive operations from an existing
890         language such as Haskell cannot be used directly (including some
891         syntax constructs, like \hs{case} expressions and \hs{if}
892         expressions).  This mkes this approach well suited for use in
893         \small{EDSL}s, since those already impose these same
894         limitations. \refdef{EDSL}
895
896         Note that the concept of \emph{state} is no more than having some way
897         to communicate a value from one cycle to the next. By introducing a
898         \hs{delay} function, we can do exactly that: delay (each value in) a
899         stream so that we can "look into" the past. This \hs{delay} function
900         simply outputs a stream where each value is the same as the input
901         value, but shifted one cycle. This causes a \quote{gap} at the
902         beginning of the stream: what is the value of the delay output in the
903         first cycle? For this, the \hs{delay} function has a second input, of
904         which only a single value is used.
905
906         \in{Example}[ex:DelayAcc] shows a simple accumulator expressed in this
907         style.
908
909 \startbuffer[DelayAcc]
910 acc :: Stream Word -> Stream Word
911 acc in = out
912   where
913     out = (delay out 0) + in
914 \stopbuffer
915
916 \startuseMPgraphic{DelayAcc}
917   save in, out, add, reg;
918
919   % I/O ports
920   newCircle.in(btex $in$ etex) "framed(false)";
921   newCircle.out(btex $out$ etex) "framed(false)";
922
923   % Components
924   newReg.reg("") "dx(4mm)", "dy(6mm)", "reflect(true)";
925   newCircle.add(btex + etex);
926   
927   in.c    = origin;
928   add.c   = in.c + (2cm, 0cm);
929   out.c   = add.c + (2cm, 0cm);
930   reg.c   = add.c + (0cm, 2cm);
931
932   % Draw objects and lines
933   drawObj(in, out, add, reg);
934
935   nccurve(add)(reg) "angleA(0)", "angleB(180)", "posB(d)";
936   nccurve(reg)(add) "angleA(180)", "angleB(-45)", "posA(out)";
937   ncline(in)(add);
938   ncline(add)(out);
939 \stopuseMPgraphic
940
941
942         \placeexample[][ex:DelayAcc]{Simple accumulator architecture.}
943           \startcombination[2*1]
944             {\typebufferhs{DelayAcc}}{Haskell description using streams.}
945             {\boxedgraphic{DelayAcc}}{The architecture described by the Haskell description.}
946           \stopcombination
947
948
949         This notation can be confusing (especially due to the loop in the
950         definition of out), but is essentially easy to interpret. There is a
951         single call to delay, resulting in a circuit with a single register,
952         whose input is connected to \hs{out} (which is the output of the
953         adder), and its output is the expression \hs{delay out 0} (which is
954         connected to one of the adder inputs).
955
956       \subsubsection{Explicit state arguments and results}
957         A more explicit way to model state, is to simply add an extra argument
958         containing the current state value. This allows an output to depend on
959         both the inputs as well as the current state while keeping the
960         function pure (letting the result depend only on the arguments), since
961         the current state is now an argument.
962
963         In Haskell, this would look like
964         \in{example}[ex:ExplicitAcc]\footnote[notfinalsyntax]{This
965         example is not in the final Cλash syntax}. \todo{Referencing
966         notfinalsyntax from Introduction.tex doesn't work}
967
968 \startbuffer[ExplicitAcc]
969 -- input -> current state -> (new state, output)
970 acc :: Word -> Word -> (Word, Word)
971 acc in s = (s', out)
972   where
973     out = s + in
974     s'  = out
975 \stopbuffer
976
977         \placeexample[][ex:ExplicitAcc]{Simple accumulator architecture.}
978           \startcombination[2*1]
979             {\typebufferhs{ExplicitAcc}}{Haskell description using explicit state arguments.}
980             % Picture is identical to the one we had just now.
981             {\boxedgraphic{DelayAcc}}{The architecture described by the Haskell description.}
982           \stopcombination
983
984         This approach makes a function's state very explicit, which state
985         variables are used by a function can be completely determined from its
986         type signature (as opposed to the stream approach, where a function
987         looks the same from the outside, regardless of what state variables it
988         uses or whether it is stateful at all).
989         
990         This approach to state has been one of the initial drives behind
991         this research. Unlike a stream based approach it is well suited
992         to completely use existing code and language features (like
993         \hs{if} and \hs{case} expressions) because it operates on normal
994         values. Because of these reasons, this is the approach chosen
995         for Cλash. It will be examined more closely below.
996
997     \subsection{Explicit state specification}
998       The concept of explicit state has been introduced with some
999       examples above, but what are the implications of this approach?
1000
1001       \subsubsection{Substates}
1002         Since a function's state is reflected directly in its type signature,
1003         if a function calls other stateful functions (\eg, has subcircuits), it
1004         has to somehow know the current state for these called functions. The
1005         only way to do this, is to put these \emph{substates} inside the
1006         caller's state. This means that a function's state is the sum of the
1007         states of all functions it calls, and its own state. This sum
1008         can be obtained using something simple like a tuple, or possibly
1009         custom algebraic types for clarity.
1010
1011         This also means that the type of a function (at least the "state"
1012         part) is dependent on its own implementation and of the functions it
1013         calls.
1014
1015         This is the major downside of this approach: the separation between
1016         interface and implementation is limited. However, since Cλash is not
1017         very suitable for separate compilation (see
1018         \in{section}[sec:prototype:separate]) this is not a big problem in
1019         practice.
1020
1021         Additionally, when using a type synonym for the state type
1022         of each function, we can still provide explicit type signatures
1023         while keeping the state specification for a function near its
1024         definition only.
1025         \todo{Example}
1026     
1027       \subsubsection{Which arguments and results are stateful?}
1028         \fxnote{This section should get some examples}
1029         We need some way to know which arguments should become input ports and
1030         which argument(s?) should become the current state (\eg, be bound to
1031         the register outputs). This does not hold just for the top
1032         level function, but also for any subfunction. Or could we perhaps
1033         deduce the statefulness of subfunctions by analyzing the flow of data
1034         in the calling functions?
1035
1036         To explore this matter, the following observeration is interesting: we
1037         get completely correct behaviour when we put all state registers in
1038         the top level entity (or even outside of it). All of the state
1039         arguments and results on subfunctions are treated as normal input and
1040         output ports. Effectively, a stateful function results in a stateless
1041         hardware component that has one of its input ports connected to the
1042         output of a register and one of its output ports connected to the
1043         input of the same register.
1044
1045         \todo{Example}
1046
1047         Of course, even though the hardware described like this has the
1048         correct behaviour, unless the layout tool does smart optimizations,
1049         there will be a lot of extra wire in the design (since registers will
1050         not be close to the component that uses them). Also, when working with
1051         the generated \small{VHDL} code, there will be a lot of extra ports
1052         just to pass on state values, which can get quite confusing.
1053
1054         To fix this, we can simply \quote{push} the registers down into the
1055         subcircuits. When we see a register that is connected directly to a
1056         subcircuit, we remove the corresponding input and output port and put
1057         the register inside the subcircuit instead. This is slightly less
1058         trivial when looking at the Haskell code instead of the resulting
1059         circuit, but the idea is still the same.
1060
1061         \todo{Example}
1062
1063         However, when applying this technique, we might push registers down
1064         too far. When you intend to store a result of a stateless subfunction
1065         in the caller's state and pass the current value of that state
1066         variable to that same function, the register might get pushed down too
1067         far. It is impossible to distinguish this case from similar code where
1068         the called function is in fact stateful. From this we can conclude
1069         that we have to either:
1070
1071         \todo{Example of wrong downpushing}
1072
1073         \startitemize
1074         \item accept that the generated hardware might not be exactly what we
1075         intended, in some specific cases. In most cases, the hardware will be
1076         what we intended.
1077         \item explicitly annotate state arguments and results in the input
1078         description.
1079         \stopitemize
1080
1081         The first option causes (non-obvious) exceptions in the language
1082         intepretation. Also, automatically determining where registers should
1083         end up is easier to implement correctly with explicit annotations, so
1084         for these reasons we will look at how this annotations could work.
1085
1086         \todo{Sidenote: one or more state arguments?}
1087
1088     \subsection[sec:description:stateann]{Explicit state annotation}
1089       To make our stateful descriptions unambigious and easier to translate,
1090       we need some way for the developer to describe which arguments and
1091       results are intended to become stateful.
1092     
1093       Roughly, we have two ways to achieve this:
1094       \startitemize[KR]
1095         \item Use some kind of annotation method or syntactic construction in
1096         the language to indicate exactly which argument and (part of the)
1097         result is stateful. This means that the annotation lives
1098         \quote{outside} of the function, it is completely invisible when
1099         looking at the function body.
1100         \item Use some kind of annotation on the type level, \ie\ give stateful
1101         arguments and stateful (parts of) results a different type. This has the
1102         potential to make this annotation visible inside the function as well,
1103         such that when looking at a value inside the function body you can
1104         tell if it is stateful by looking at its type. This could possibly make
1105         the translation process a lot easier, since less analysis of the
1106         program flow might be required.
1107       \stopitemize
1108
1109       From these approaches, the type level \quote{annotations} have been
1110       implemented in Cλash. \in{Section}[sec:prototype:statetype] expands on
1111       the possible ways this could have been implemented.
1112
1113   \todo{Note about conditions on state variables and checking them}
1114
1115   \section[sec:recursion]{Recursion}
1116   An important concept in functional languages is recursion. In its most basic
1117   form, recursion is a definition that is described in terms of itself. A
1118   recursive function is thus a function that uses itself in its body. This
1119   usually requires multiple evaluations of this function, with changing
1120   arguments, until eventually an evaluation of the function no longer requires
1121   itself.
1122
1123   Given the notion that each function application will translate to a
1124   component instantiation, we are presented with a problem. A recursive
1125   function would translate to a component that contains itself. Or, more
1126   precisely, that contains an instance of itself. This instance would again
1127   contain an instance of itself, and again, into infinity. This is obviously a
1128   problem for generating hardware.
1129
1130   This is expected for functions that describe infinite recursion. In that
1131   case, we cannot generate hardware that shows correct behaviour in a single
1132   cycle (at best, we could generate hardware that needs an infinite number of
1133   cycles to complete).
1134   
1135   \placeintermezzo{}{
1136     \startframedtext[width=8cm,background=box,frame=no]
1137     \startalignment[center]
1138       {\tfa \hs{null}, \hs{head} and \hs{tail}}
1139     \stopalignment
1140     \blank[medium]
1141       The functions \hs{null}, \hs{head} and \hs{tail} are common list
1142       functions in Haskell. The \hs{null} function simply checks if a list is
1143       empty. The \hs{head} function returns the first element of a list. The
1144       \hs{tail} function returns containing everything \emph{except} the first
1145       element of a list.
1146
1147       In Cλash, there are vector versions of these functions, which do exactly
1148       the same.
1149     \stopframedtext
1150   }
1151
1152   However, most recursive definitions will describe finite
1153   recursion. This is because the recursive call is done conditionally. There
1154   is usually a \hs{case} expression where at least one alternative does not contain
1155   the recursive call, which we call the "base case". If, for each call to the
1156   recursive function, we would be able to detect at compile time which
1157   alternative applies, we would be able to remove the \hs{case} expression and
1158   leave only the base case when it applies. This will ensure that expanding
1159   the recursive functions will terminate after a bounded number of expansions.
1160
1161   This does imply the extra requirement that the base case is detectable at
1162   compile time. In particular, this means that the decision between the base
1163   case and the recursive case must not depend on runtime data.
1164
1165   \subsection{List recursion}
1166   The most common deciding factor in recursion is the length of a list that is
1167   passed in as an argument. Since we represent lists as vectors that encode
1168   the length in the vector type, it seems easy to determine the base case. We
1169   can simply look at the argument type for this. However, it turns out that
1170   this is rather non-trivial to write down in Haskell already, not even
1171   looking at translation. As an example, we would like to write down something
1172   like this:
1173  
1174   \starthaskell
1175     sum :: Vector n Word -> Word
1176     sum xs = case null xs of
1177       True -> 0
1178       False -> head xs + sum (tail xs)
1179   \stophaskell
1180
1181   However, the Haskell typechecker will now use the following reasoning.
1182   For simplicity, the element type of a vector is left out, all vectors
1183   are assumed to have the same element type. Below, we write conditions
1184   on type variables before the \hs{=>} operator. This is not completely
1185   valid Haskell syntax, but serves to illustrate the typechecker
1186   reasoning. Also note that a vector can never have a negative length,
1187   so \hs{Vector n} implicitly means \hs{(n >= 0) => Vector n}.
1188
1189   \todo{This typechecker disregards the type signature}
1190   \startitemize
1191   \item tail has the type \hs{(n > 0) => Vector n -> Vector (n - 1)}
1192   \item This means that xs must have the type \hs{(n > 0) => Vector n}
1193   \item This means that sum must have the type \hs{(n > 0) => Vector n -> a}
1194   (The type \hs{a} is can be anything at this stage, we will not try to finds
1195   its actual type in this example).
1196   \item sum is called with the result of tail as an argument, which has the
1197   type \hs{Vector n} (since \hs{(n > 0) => Vector (n - 1)} is the same as \hs{(n >= 0)
1198   => Vector n}, which is the same as just \hs{Vector n}).
1199   \item This means that sum must have the type \hs{Vector n -> a}
1200   \item This is a contradiction between the type deduced from the body of sum
1201   (the input vector must be non-empty) and the use of sum (the input vector
1202   could have any length).
1203   \stopitemize
1204
1205   As you can see, using a simple \hs{case} expression  at value level causes
1206   the type checker to always typecheck both alternatives, which cannot be
1207   done. The typechecker is unable to distinguish the two case
1208   alternatives (this is partly possible using \small{GADT}s, but that
1209   approach faced other problems \todo{ref christiaan?}).
1210
1211   This is a fundamental problem, that would seem perfectly suited for a
1212   type class.  Considering that we need to switch between to
1213   implementations of the sum function, based on the type of the
1214   argument, this sounds like the perfect problem to solve with a type
1215   class. However, this approach has its own problems (not the least of
1216   them that you need to define a new type class for every recursive
1217   function you want to define).
1218
1219   \todo{This should reference Christiaan}
1220
1221   \subsection{General recursion}
1222   Of course there are other forms of recursion, that do not depend on the
1223   length (and thus type) of a list. For example, simple recursion using a
1224   counter could be expressed, but only translated to hardware for a fixed
1225   number of iterations. Also, this would require extensive support for compile
1226   time simplification (constant propagation) and compile time evaluation
1227   (evaluation of constant comparisons), to ensure non-termination.
1228   Supporting general recursion will probably require strict conditions
1229   on the input descriptions. Even then, it will be hard (if not
1230   impossible) to really guarantee termination, since the user (or \GHC\
1231   desugarer) might use some obscure notation that results in a corner
1232   case of the simplifier that is not caught and thus non-termination.
1233
1234   Evaluating all possible (and non-possible) ways to add recursion to
1235   our descriptions, it seems better to limit the scope of this research
1236   to exclude recursion. This allows for focusing on other interesting
1237   areas instead. By including (built-in) support for a number of
1238   higher-order functions like \hs{map} and \hs{fold}, we can still
1239   express most of the things we would use (list) recursion for.
1240   
1241
1242 % vim: set sw=2 sts=2 expandtab: