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