Put CaseInv and PatternInv in the same float.
[matthijs/master-project/report.git] / Chapters / Future.tex
1 \chapter[chap:future]{Future work}
2 \section{New language}
3 During the development of the prototype, it has become clear that Haskell is
4 not the perfect language for this work. There are two main problems:
5 \startitemize
6 \item Haskell is not expressive enough. Haskell is still quite new in the area
7 of dependent typing, something we use extensively. Also, Haskell has some
8 special syntax to write monadic composition and arrow composition, which is
9 well suited to normal Haskell programs. However, for our hardware
10 descriptions, we could use some similar, but other, syntactic sugar (as we
11 have seen above).
12 \item Haskell is too expressive. There are some things that Haskell can
13 express, but we can never properly translate. There are certain types (both
14 primitive types and certain type constructions like recursive types) we can
15 never translate, as well as certain forms of recursion.
16 \stopitemize
17
18 It might be good to reevaluate the choice of language for Cλash, perhaps there
19 are other languages which are better suited to describe hardware, now that
20 we have learned a lot about it.
21
22 Perhaps Haskell (or some other language) can be extended by using a
23 preprocessor. There has been some (point of proof) work on a the Strathclyde
24 Haskell Enhancement (\small{SHE}) preprocessor for type-level programming,
25 perhaps we can extend that, or create something similar for hardware-specific
26 notation.
27
28 It is not unlikely that the most flexible way
29 forward would be to define a completely new language with exactly the needed
30 features. This is of course an enormous effort, which should not be taken
31 lightly.
32
33 \section{Correctness proofs of the normalization system}
34 As stated in \in{section}[sec:normalization:properties], there are a
35 number of properties we would like to see verified about the
36 normalization system.  In particular, the \emph{termination} and
37 \emph{completeness} of the system would be a good candidate for future
38 research. Specifying formal semantics for the Core language in
39 order to verify the \emph{soundness} of the system would be an even more
40 challenging task.
41
42 \section{Improved notation for hierarchical state}
43 The hierarchical state model requires quite some boilerplate code for unpacking
44 and distributing the input state and collecting and repacking the output
45 state.
46
47 \in{Example}[ex:NestedState] shows a simple composition of two stateful
48 functions, \hs{funca} and \hs{funcb}. The state annotation using the
49 \hs{State} newtype has been left out, for clarity and because the proposed
50 approach below cannot handle that (yet).
51
52 \startbuffer[NestedState]
53   type FooState = ( AState, BState )
54   foo :: Word -> FooState -> (FooState, Word)
55   foo in s = (s', outb)
56     where
57       (sa, sb) = s
58       (sa', outa) = funca in sa
59       (sb', outb) = funcb outa sb
60       s' = (sa', sb')
61 \stopbuffer
62 \placeexample[here][ex:NestedState]{Simple function composing two stateful
63                                     functions.}{\typebufferhs{NestedState}}
64
65 Since state handling always follows strict rules, there is really no other way
66 in which this state handling can be done (you can of course move some things
67 around from the where clause to the pattern or vice versa, but it would still
68 be effectively the same thing). This means it makes extra sense to hide this
69 boilerplate away. This would incur no flexibility cost at all, since there are
70 no other ways that would work.
71
72 One particular notation in Haskell that seems promising, is the \hs{do}
73 notation. This is meant to simplify Monad notation by hiding away some
74 details. It allows one to write a list of expressions, which are composited
75 using the monadic \emph{bind} operator, written in Haskell as \hs{>>}. For
76 example, the snippet:
77
78 \starthaskell
79 do
80   somefunc a
81   otherfunc b
82 \stophaskell
83
84 will be desugared into:
85
86 \starthaskell
87 (somefunc a) >> (otherfunc b)
88 \stophaskell
89
90 The main reason to have the monadic notation, is to be able to wrap
91 results of functions in a datatype (the \emph{monad}) that can contain
92 extra information, and hide extra behaviour in the binding operators.
93
94 The \hs{>>=} operator allows extracting the actual result of a function
95 and passing it to another function. The following snippet should
96 illustrate this:
97
98 \starthaskell
99 do
100   x <- somefunc a
101   otherfunc x
102 \stophaskell
103
104 will be desugared into:
105
106 \starthaskell
107 (somefunc a) >>= (\x -> otherfunc x)
108 \stophaskell
109
110 The \hs{\x -> ...} notation creates a lambda abstraction in Haskell,
111 that binds the \hs{x} variable. Here, the \hs{>>=} operator is supposed
112 to extract whatever result somefunc has and pass it to the lambda
113 expression created. This will probably not make the monadic notation
114 completely clear to a reader without prior experience with Haskell, but
115 it should serve to understand the following discussion.
116
117 The monadic notation could perhaps be used to compose a number of
118 stateful functions into another stateful computation. Perhaps this could
119 move all the boilerplate code into the \hs{>>} and \hs{>>=} operators.
120 Because the boilerplate is still there (it has not magically disappeared,
121 just moved into these functions), the compiler should still be able to compile
122 these descriptions without any special magic (though perhaps it should
123 always inline the binding operators to reveal the flow of values).
124
125 This highlights an important aspect of using a functional language for our
126 descriptions: we can use the language itself to provide abstractions of common
127 patterns, making our code smaller and easier to read.
128
129 \subsection{Breaking out of the Monad}
130 However, simply using the monad notation is not as easy as it sounds. The main
131 problem is that the Monad type class poses a number of limitations on the
132 bind operator \hs{>>}. Most importantly, it has the following type signature:
133
134 \starthaskell
135 (>>) :: (Monad m) => m a -> m b -> m b
136 \stophaskell
137
138 This means that any expression in our composition must use the same Monad
139 instance as its type, only the "return" value can be different between
140 expressions. 
141
142 Ideally, we would like the \hs{>>} operator to have a type like the following
143 \starthaskell
144 type Stateful s r = s -> (s, r)
145 (>>) :: Stateful s1 r1 -> Stateful s2 r2 -> Stateful (s1, s2) r2
146 \stophaskell
147
148 What we see here, is that when we compose two stateful functions (that
149 have already been applied to their inputs, leaving just the state
150 argument to be applied to), the result is again a stateful function
151 whose state is composed of the two \emph{substates}. The return value is
152 simply the return value of the second function, discarding the first (to
153 preserve that result, the \hs{>>=} operator can be used).
154
155 There is a trick we can apply to change the signature of the \hs{>>} operator.
156 \small{GHC} does not require the bind operators to be part of the \hs{Monad}
157 type class, as long as it can use them to translate the do notation. This
158 means we can define our own \hs{>>} and \hs{>>=} operators, outside of the
159 \hs{Monad} type class. This does conflict with the existing methods of the
160 \hs{Monad} type class, so we should prevent \small{GHC} from loading those (and
161 all of the Prelude) by passing \type{-XNoImplicitPrelude} to \type{ghc}. This
162 is slightly inconvenient, but since we hardly using anything from the prelude,
163 this is not a big problem. We might even be able to replace some of the
164 Prelude with hardware-translateable versions by doing this.
165
166 The binding operators can now be defined exactly as they are needed. For
167 completeness, the \hs{return} function is also defined. It is not called
168 by \small{GHC} implicitly, but can be called explicitly by a hardware
169 description. \in{Example}[ex:StateMonad] shows these definitions.
170
171 \startbuffer[StateMonad]
172 (>>) :: Stateful s1 r1 -> Stateful s2 r2 -> Stateful (s1, s2) r2
173 f1 >> f2 = f1 >>= \_ -> f2
174
175 (>>=) :: Stateful s1 r1 -> (r1 -> Stateful s2 r2) -> Stateful (s1, s2) r2
176 f1 >>= f2 = \(s1, s2) -> let (s1', r1) = f1 s1
177                              (s2', r2) = f2 r1 s2
178                          in ((s1', s2'), r2)
179                
180 return :: r -> Stateful () r
181 return r = \s -> (s, r)
182 \stopbuffer
183 \placeexample[here][ex:StateMonad]{Binding operators to compose stateful computations}
184   {\typebufferhs{StateMonad}}
185
186 These definitions closely resemble the boilerplate of unpacking state,
187 passing it to two functions and repacking the new state. With these
188 definitions, we could have writting \in{example}[ex:NestedState] a lot
189 shorter, see \in{example}[ex:DoState]. In this example the type signature of
190 foo is the same (though it is now written using the \hs{Stateful} type
191 synonym, it is still completely equivalent to the original: \hs{foo :: Word ->
192 FooState -> (FooState, Word)}.
193
194 Note that the \hs{FooState} type has changed (so indirectly the type of
195 \hs{foo} as well). Since the state composition by the \hs{>>} works on two
196 stateful functions at a time, the final state consists of nested two-tuples.
197 The final \hs{()} in the state originates from the fact that the \hs{return}
198 function has no real state, but is part of the composition. We could have left
199 out the return expression (and the \hs{outb <-} part) to make \hs{foo}'s return
200 value equal to \hs{funcb}'s, but this approach makes it clearer what is
201 happening.
202
203 \startbuffer[DoState]
204   type FooState = ( AState, (BState, ()) )
205   foo :: Word -> Stateful FooState Word
206   foo in = do
207       outa <- funca in
208       outb <- funcb outa
209       return outb
210 \stopbuffer
211 \placeexample[][ex:DoState]{Simple function composing two stateful
212                                 functions, using do notation.}
213                                {\typebufferhs{DoState}}
214
215 An important implication of this approach is that the order of writing
216 function applications affects the state type. Fortunately, this problem can be
217 localized by consistently using type synonyms for state types, which should
218 prevent changes in other function's source when a function changes.
219
220 A less obvous implications of this approach is that the scope of variables
221 produced by each of these expressions (using the \hs{<-} syntax) is limited to
222 the expressions that come after it. This prevents values from flowing between
223 two functions (components) in two directions. For most Monad instances, this
224 is a requirement, but here it could have been different.
225
226 \todo{Add examples or reference for state synonyms}
227
228 \subsection{Alternative syntax}
229 Because of these typing issues, misusing Haskell's do notation is probably not
230 the best solution here. However, it does show that using fairly simple
231 abstractions, we could hide a lot of the boilerplate code. Extending
232 \small{GHC} with some new syntax sugar similar to the do notation might be a
233 feasible.
234
235 \subsection{Arrows}
236 Another abstraction mechanism offered by Haskell are arrows. Arrows are
237 a generalisation of monads \cite[hughes98], for which \GHC\ also supports
238 some syntax sugar \cite[paterson01]. Their use for hiding away state
239 boilerplate is not directly evident, but since arrows are a complex
240 concept further investigation is appropriate.
241
242 \section[sec:future:pipelining]{Improved notation or abstraction for pipelining}
243 Since pipelining is a very common optimization for hardware systems, it should
244 be easy to specify a pipelined system. Since it introduces quite some registers
245 into an otherwise regular combinational system, we might look for some way to
246 abstract away some of the boilerplate for pipelining.
247
248 Something similar to the state boilerplate removal above might be appropriate:
249 Abstract away some of the boilerplate code using combinators, then hide away
250 the combinators in special syntax. The combinators will be slightly different,
251 since there is a (typing) distinction between a pipeline stage and a pipeline
252 consisting of multiple stages. Also, it seems necessary to treat either the
253 first or the last pipeline stage differently, to prevent an off-by-one error
254 in the amount of registers (which is similar to the extra \hs{()} state type
255 in \in{example}[ex:DoState], which is harmless there, but would be a problem
256 if it introduced an extra, useless, pipeline stage).
257
258 This problem is slightly more complex than the problem we have seen before. One
259 significant difference is that each variable that crosses a stage boundary
260 needs a register. However, when a variable crosses multiple stage boundaries,
261 it must be stored for a longer period and should receive multiple registers.
262 Since we cannot find out from the combinator code where the result of the
263 combined values is used (at least not without using Template Haskell to
264 inspect the \small{AST}), there seems to be no easy way to find how much
265 registers are needed.
266
267 There seem to be two obvious ways of handling this problem:
268
269 \startitemize
270   \item Limit the scoping of each variable produced by a stage to the next
271   stage only. This means that any variables that are to be used in subsequent
272   stages should be passed on explicitly, which should allocate the required
273   number of registers.
274
275   This produces cumbersome code, where there is still a lot of explicitness
276   (though this could be hidden in syntax sugar).
277   \todo{The next sentence is unclear}
278   \item Scope each variable over every subsequent pipeline stage and allocate
279   the maximum number of registers that \emph{could} be needed. This means we
280   will allocate registers that are never used, but those could be optimized
281   away later. This does mean we need some way to introduce a variable number
282   of variables (depending on the total number of stages), assign the output of
283   a different register to each (\eg., a different part of the state) and scope
284   a different one of them over each the subsequent stages.
285
286   This also means that when adding a stage to an existing pipeline will change
287   the state type of each of the subsequent pipeline stages, and the state type
288   of the added stage depends on the number of subsequent stages.
289
290   Properly describing this will probably also require quite explicit syntax,
291   meaning this is not feasible without some special syntax.
292 \stopitemize
293
294 Some other interesting issues include pipeline stages which are already
295 stateful, mixing pipelined with normal computation, etc.
296
297 \section{Recursion}
298 The main problems of recursion have been described in
299 \in{section}[sec:recursion]. In the current implementation, recursion is
300 therefore not possible, instead we rely on a number of implicitly list-recursive
301 built-in functions.
302
303 Since recursion is a very important and central concept in functional
304 programming, it would very much improve the flexibility and elegance of our
305 hardware descriptions if we could support (full) recursion.
306
307 For this, there are two main problems to solve:
308
309 \startitemize
310 \item For list recursion, how to make a description type check? It is quite
311 possible that improvements in the \small{GHC} typechecker will make this
312 possible, though it will still stay a challenge. Further advances in
313 dependent typing support for Haskell will probably help here as well.
314
315 \todo{Reference Christiaan and other type-level work
316 (http://personal.cis.strath.ac.uk/conor/pub/she/)}
317 \item For all recursion, there is the obvious challenge of deciding when
318 recursion is finished. For list recursion, this might be easier (Since the
319 base case of the recursion influences the type signatures). For general
320 recursion, this requires a complete set of simplification and evaluation
321 transformations to prevent infinite expansion. The main challenge here is how
322 to make this set complete, or at least define the constraints on possible
323 recursion that guarantee it will work.
324
325 \todo{Reference Christian for loop unrolling?}
326 \stopitemize
327
328 \section{Multiple clock domains and asynchronicity}
329 Cλash currently only supports synchronous systems with a single clock domain.
330 In a lot of real-world systems, both of these limitations pose problems.
331
332 There might be asynchronous events to which a system wants to respond. The
333 most obvious asynchronous event is of course a reset signal. Though a reset
334 signal can be synchronous, that is less flexible (and a hassle to describe in
335 Cλash, currently). Since every function in Cλash describes the behaviour on
336 each cycle boundary, we really cannot fit in asynchronous behaviour easily.
337
338 Due to the same reason, multiple clock domains cannot be easily supported. There is
339 currently no way for the compiler to know in which clock domain a function
340 should operate and since the clock signal is never explicit, there is also no
341 way to express circuits that synchronize various clock domains.
342
343 A possible way to express more complex timing behaviour would be to make
344 functions more generic event handlers, where the system generates a stream of
345 events (Like \quote{clock up}, \quote{clock down}, \quote{input A changed},
346 \quote{reset}, etc.). When working with multiple clock domains, each domain
347 could get its own clock events.
348
349 \startbuffer[AsyncDesc]
350 data Event = ClockUp | Reset | ...
351
352 type MainState = State Word
353
354 -- Initial state
355 initstate :: MainState
356 initstate = State 0
357
358 main :: Word -> Event -> MainState -> (MainState, Word)
359 main inp event (State acc) = (State acc', acc')
360   where
361     acc' = case event of
362       -- On a reset signal, reset the accumulator and output
363       Reset -> initstate
364       -- On a normal clock cycle, accumulate the result of func
365       ClockUp -> acc + (func inp event)
366       -- On any other event, leave state and output unchanged
367       _ -> acc
368
369 -- func is some combinational expression
370 func :: Word -> Event -> Word
371 func inp _ = inp * 2 + 3
372 \stopbuffer
373
374 \placeexample[][ex:AsyncDesc]{Hardware description using asynchronous events.}
375   {\typebufferhs{AsyncDesc}}
376
377 \todo{Picture}
378
379 \in{Example}[ex:AsyncDesc] shows a simple example of this event-based
380 approach. In this example we see that every function takes an input of
381 type \hs{Event}. The function \hs{main} that takes the output of
382 \hs{func} and accumulates it on every clock cycle. On a reset signal,
383 the accumulator is reset. The function \hs{func} is just a combinational
384 function, with no synchronous elements.  We can see this because there
385 is no state and the event input is completely ignored. If the compiler
386 is smart enough, we could even leave the event input out for functions
387 that do not use it, either because they are completely combinational (like
388 in this example), or because they rely on the the caller to select the
389 clock signal.
390
391 This structure is similar to the event handling structure used to perform I/O
392 in languages like Amanda. \todo{ref} There is a top level case expression that
393 decides what to do depending on the current input event.
394
395 A slightly more complex example is show in
396 \in{example}[ex:MulticlockDesc]. It shows a system with two clock
397 domains. There is no real integration between the clock domains in this
398 example (there is one input and one output for each clock domain), but
399 it does show how multiple clocks can be distinguished.
400
401 \startbuffer[MulticlockDesc]
402 data Event = ClockUpA | ClockUpB | ...
403
404 type MainState = State (SubAState, SubBState)
405
406 -- Initial state
407 initstate :: MainState
408 initstate = State (initsubastate, initsubbstate)
409
410 main :: Word -> Word -> Event -> MainState -> (MainState, Word, Word)
411 main inpa inpb event (State (sa, sb)) = (State (sa', sb'), outa, outb)
412   where
413     -- Only update the substates if the corresponding clock has an up
414     -- transition.
415     sa' = case event of
416       ClockUpA -> sa''
417       _ -> sa
418     sb' = case event of
419       ClockUpB -> sb''
420       _ -> sb
421     -- Always call suba and subb, so we can always have a value for our output
422     -- ports.
423     (sa'', outa) = suba inpa sa
424     (sb'', outb) = subb inpb sb
425
426 type SubAState = State ...
427 suba :: Word -> SubAState -> (SubAState, Word)
428 suba = ...
429
430 type SubBState = State ...
431 subb :: Word -> SubAState -> (SubAState, Word)
432 subb = ...
433 \stopbuffer
434
435 \placeexample[][ex:MulticlockDesc]{Hardware description with multiple clock domains through events.}
436   {\typebufferhs{MulticlockDesc}}
437
438 Note that in \in{example}[ex:MulticlockDesc] the \hs{suba} and \hs{subb}
439 functions are \emph{always} called, to get at their combinational
440 outputs. The new state is calculated as well, but only saved when the
441 right clock has an up transition.
442
443 As you can see, there is some code duplication in the case expression that
444 selects the right clock. One of the advantages of an explicit approach like
445 this, is that some of this duplication can be extracted away into helper
446 functions. For example, we could imagine a \hs{select_clock} function, which
447 takes a stateful function that is not aware of events, and changes it into a
448 function that only updates its state on a specific (clock) event. Such a
449 function is shown in \in{example}[ex:SelectClock].
450
451 \startbuffer[SelectClock]
452 select_clock :: Event
453                 -> (input -> State s -> (State s, output))
454                 -> (input -> State s -> Event -> (State s, output))
455 select_clock clock func inp state event = (state', out)
456   where
457     state' = if clock == event then state'' else state
458     (state'', out) = func inp state
459
460 main :: Word -> Word -> Event -> MainState -> (MainState, Word, Word)
461 main inpa inpb event (State (sa, sb)) = (State (sa', sb'), outa, outb)
462   where
463     (sa'', outa) = (select_clock ClockUpA suba) inpa sa event
464     (sb'', outb) = (select_clock ClockUpB subb) inpb sb event
465 \stopbuffer
466 \placeexample[][ex:SelectClock]{A function to filter clock events.}
467   {\typebufferhs{SelectClock}}
468
469 As you can see, this can greatly reduce the length of the main function, while
470 increasing the readability. As you might also have noted, the select\_clock
471 function takes any stateful function from the current Cλash prototype and
472 turns it into an event-aware function!
473
474 Going along this route for more complex timing behaviour seems promising,
475 espicially since it seems possible to express very advanced timing behaviours,
476 while still allowing simple functions without any extra overhead when complex
477 behaviour is not needed.
478
479 The main cost of this approach will probably be extra complexity in the
480 compiler: the paths (state) data can take become very non-trivial, and it
481 is probably hard to properly analyze these paths and produce the
482 intended \VHDL\ description.
483
484 \section{Multiple cycle descriptions}
485 In the current Cλash prototype, every description is a single-cycle
486 description. In other words, every function describes behaviour for each
487 separate cycle and any recursion (or folds, maps, etc.) is expanded in space.
488
489 Sometimes, you might want to have a complex description that could possibly
490 take multiple cycles. Some examples include:
491
492 \startitemize
493   \item Some kind of map or fold over a list that could be expanded in time
494   instead of space. This would result in a function that describes n cycles
495   instead of just one, where n is the lenght of the list.
496   \item A large combinational expressions that would introduce a very long
497   combinational path and thus limit clock frequency. Such an expression could
498   be broken up into multiple stages, which effectively results in a pipelined
499   system (see also \in{section}[sec:future:pipelining]) with a known delay.
500   There should probably be some way for the developer to specify the cycle
501   division of the expression, since automatically deciding on such a division
502   is too complex and contains too many tradeoffs, at least initially.
503   \item Unbounded recursion. It is not possible to expand unbounded (or even
504   recursion with a depth that is not known at compile time) in space, since
505   there is no way to tell how much hardware to create (it might even be
506   infinite).
507
508   When expanding infinite recursion over time, each step of the recursion can
509   simply become a single clockcycle. When expanding bounded but unknown
510   recursion, we probably need to add an extra data valid output bit or
511   something similar.
512 \stopitemize
513
514 Apart from translating each of these multiple cycle descriptions into a per-cycle
515 description, we also need to somehow match the type signature of the multiple
516 cycle description to the type signature of the single cycle description that
517 the rest of the system expects (assuming that the rest of the system is
518 described in the \quote{normal} per-cycle manner). For example, an infinitely
519 recursive expression typically has the return type \lam{[a]}, while the rest
520 of the system would expect just \lam{a} (since the recursive expression
521 generates just a single element each cycle).
522
523 Naively, this matching could be done using a (built-in) function with a
524 signature like \lam{[a] -> a}, which also serves as an indicator to the
525 compiler that some expanding over time is required. However, this poses a
526 problem for simulation: how will our Haskell implementation of this magical
527 built-in function know which element of the input list to return. This
528 obviously depends on the current cycle number, but there is no way for this
529 function to know the current cycle without breaking all kinds of safety and
530 purity properties. Making this function have some state input and output could
531 help, though this state is not present in the actual hardware (or perhaps
532 there is some state, if there are value passed from one recursion step to the
533 next, but how can the type of that state be determined by the typechecker?).
534
535 It seems that this is the most pressing problem for multicycle descriptions:
536 How to interface with the rest of the system, without sacrificing safety and
537 simulation capabilities?
538
539 \section{Higher order values in state}
540 Another interesting idea is putting a higher-order value inside a function's
541 state value. Since we can use higher-order values anywhere, why not in the
542 state?
543
544 \startbuffer[HigherAccum]
545 -- The accumulator function that takes a word and returns a new accumulator
546 -- and the result so far. This is the function we want to put inside the
547 -- state.
548 type Acc = Word -> (Acc, Word)
549 acc = \a -> (\b -> acc ( a + b ), a )
550
551 main :: Word -> State Acc -> (State Acc, Word)
552 main a s = (State s', out)
553   where (s', out) = s a
554 \stopbuffer
555 \placeexample[][ex:HigherAccum]{An accumulator using a higher-order state.}
556   {\typebufferhs{HigherAccum}}
557
558 As a (contrived) example, consider the accumulator in
559 \in{example}[ex:HigherAccum]. This code uses a function as its state,
560 which implicitly contains the value accumulated so far. This is a
561 fairly trivial example, that is more easy to write with a simple
562 \hs{Word} state value, but for more complex descriptions this style
563 might pay off. Note that in a way we are using the \emph{continuation
564 passing style} of writing functions, where we pass a sort of
565 \emph{continuation} from one cycle to the next.
566
567 Our normalization process completely removes higher-order values inside a
568 function by moving applications and higher-order values around so that every
569 higher-order value will eventually be full applied. However, if we would put a
570 higher-order value inside our state, the path from the higher-order value
571 definition to its application runs through the state, which is external to the
572 function. A higher-order value defined in one cycle is not applied until a
573 later cycle. Our normalization process only works within the function, so it
574 cannot remove this use of a higher-order value.
575
576 However, we cannot leave a higher-order value in our state value, since it is
577 impossible to generate a register containing a higher-order value, we simply
578 cannot translate a function type to a hardware type. To solve this, we must
579 replace the higher-order value inside our state with some other value
580 representing these higher-order values.
581
582 On obvious approach here is to use an algebraic datatype where each
583 constructor represents one possible higher-order value that can end up in the
584 state and each constructor has an argument for each free variable of the
585 higher-order value replaced. This allows us to completely reconstruct the
586 higher-order value at the spot where it is applied, and thus the higher-order
587 value disappears.
588
589 This approach is commonly known as the \quote{Reynolds approach to
590 defuntionalization}, first described by J.C. Reynolds \cite[reynolds98]\ and
591 seems to apply well to this situation. One note here is that Reynolds'
592 approach puts all the higher-order values in a single datatype. For a typed
593 language, we will at least have to have a single datatype for each function
594 type, since we cannot mix them. It would be even better to split these
595 datatypes a bit further, so that such a datatype will never hold a constructor
596 that is never used for a particular state variable. This separation is
597 probably a non-trivial problem, though.
598
599 \section{Don't care values}
600   A powerful value in \VHDL\ is the \emph{don't care} value, given as
601   \type{'-'}. This value tells the compiler that you do not really care about
602   which value is assigned to a signal, allowing the compiler to make some
603   optimizations. Since choice in hardware is often implemented using
604   a collection of logic gates instead of multiplexers only, synthesizers can
605   often reduce the amount of hardware needed by smartly choosing values for
606   these don't care cases.
607
608   There is not really anything comparable with don't care values in normal
609   programming languages. The closest thing is an undefined or uninitialized
610   value, though those are usually associated with error conditions.
611
612   It would be useful if Cλash also has some way to specify don't care values.
613   When looking at the Haskell typing system, there are really two ways to do
614   this:
615
616   \startitemize
617     \item Add a special don't care value to every datatype. This includes the
618     obvious \hs{Bit} type, but will also need to include every user defined
619     type. An exception can be made for vectors and product types, since those
620     can simply use the don't care values of the types they contain.
621
622     This would also require some kind of \quote{Don't careable} type class
623     that allows each type to specify what its don't care value is. The
624     compiler must then recognize this constant and replace it with don't care
625     values in the final \VHDL\ code.
626
627     This is of course a very intrusive solution. Every type must become member
628     of this type class, and there is now some member in every type that is a
629     special don't care value. Guaranteeing the obvious don't care semantics
630     also becomes harder, since every pattern match or case expressions must now
631     also take care of the don't care value (this might actually be an
632     advantage, since it forces designers to specify how to handle don't care
633     for different operations).
634
635     \item Use the special \hs{undefined}, or \emph{bottom} value present in
636     Haskell. This is a type that is member of all types automatically, without
637     any explicit declarations.
638
639     Any expression that requires evaluation of an undefined value
640     automatically becomes undefined itself (or rather, there is some exception
641     mechanism). Since Haskell is lazy, this means that whenever it tries to
642     evaluate undefined, it is apparently required for determining the output
643     of the system. This property is useful, since typically a don't care
644     output is used when some output is not valid and should not be read. If
645     it is in fact not read, it should never be evaluated and simulation should
646     be fine.
647
648     In practice, this works less ideal. In particular, pattern matching is not
649     always smart enough to deal with undefined. Consider the following
650     definition of an \hs{and} operator:
651
652     \starthaskell
653     and :: Bit -> Bit -> Bit
654     and Low _ = Low
655     and _ Low = Low
656     and High High = High
657     \stophaskell
658
659     When using the \hs{and} operation on an undefined (don't care) and a Low
660     value should always return a Low value. Its value does not depend on the
661     value chosen for the don't care value. However, though when applying the
662     above and function to \hs{Low} and \hs{undefined} results in exactly that
663     behviour, the result is \hs{undefined} when the arguments are swapped.
664     This is because the first pattern forces the first argument to be
665     evaluated. If it is \hs{undefined}, evaluation is halted and an exception
666     is show, which is not what is intended.
667   \stopitemize
668
669   These options should be explored further to see if they provide feasible
670   methods for describing don't care conditions. Possibly there are completely
671   other methods which work better.
672
673 % vim: set sw=2 sts=2 expandtab: