Fix a lot of things following from Jan's comments.

[matthijs/master-project/report.git] / Chapters / Future.tex

\chapter[chap:future]{Future work}
\section{Improved notation for hierarchical state}
The hierarchical state model requires quite some boilerplate code for unpacking
and distributing the input state and collecting and repacking the output
state.

\in{Example}[ex:NestedState] shows a simple composition of two stateful
functions, \hs{funca} and \hs{funcb}. The state annotation using the
\hs{State} newtype has been left out, for clarity and because the proposed
approach below cannot handle that (yet).

\startbuffer[NestedState]
  type FooState = ( AState, BState )
  foo :: Word -> FooState -> (FooState, Word)
  foo in s = (s', outb)
    where
      (sa, sb) = s
      (sa', outa) = funca in sa
      (sb', outb) = funcb outa sb
      s' = (sa', sb')
\stopbuffer
\placeexample[here][ex:NestedState]{Simple function composing two stateful
                                    functions.}{\typebufferhs{NestedState}}

Since state handling always follows strict rules, there is really no other way
in which this state handling can be done (you can of course move some things
around from the where clause to the pattern or vice versa, but it would still
be effectively the same thing). This means it makes extra sense to hide this
boilerplate away. This would incur no flexibility cost at all, since there are
no other ways that would work.

One particular notation in Haskell that seems promising, is the \hs{do}
notation. This is meant to simplify Monad notation by hiding away some
details. It allows one to write a list of expressions, which are composited
using the monadic \emph{bind} operator, written in Haskell as \hs{>>}. For
example, the snippet:

\starthaskell
do
  somefunc a
  otherfunc b
\stophaskell

will be desugared into:

\starthaskell
(somefunc a) >> (otherfunc b)
\stophaskell

The main reason to have the monadic notation, is to be able to wrap
results of functions in a datatype (the \emph{monad}) that can contain
extra information, and hide extra behaviour in the binding operators.

The \hs{>>=} operator allows extracting the actual result of a function
and passing it to another function. Let's try to illustrate this from an
example. The following snippet:

\starthaskell
do
  x <- somefunc a
  otherfunc x
\stophaskell

will be desugared into:

\starthaskell
(somefunc a) >>= (\x -> otherfunc x)
\stophaskell

The \hs{\x -> ...} notation creates a lambda abstraction in Haskell,
that binds the \hs{x} variable. Here, the \hs{>>=} operator is supposed
to extract whatever result somefunc has and pass it to the lambda
expression created. This will probably not make the monadic notation
completely clear to a reader without prior experience with Haskell, but
it should serve to understand the following discussion.

The monadic notation could perhaps be used to compose a number of
stateful functions into another stateful computation. Perhaps this could
move all the boilerplate code into the \hs{>>} and \hs{>>=} operators.
Because the boilerplate is still there (it's not magically disappeared,
just moved into these functions), the compiler should still be able to compile
these descriptions without any special magic (though perhaps it should
always inline the binding operators to reveal the flow of values).

This highlights an important aspect of using a functional language for our
descriptions: We can use the language itself to provide abstractions of common
patterns, making our code smaller and easier to read.

\subsection{Breaking out of the Monad}
However, simply using the monad notation is not as easy as it sounds. The main
problem is that the Monad type class poses a number of limitations on the
bind operator \hs{>>}. Most importantly, it has the following type signature:

\starthaskell
(>>) :: (Monad m) => m a -> m b -> m b
\stophaskell

This means that any expression in our composition must use the same Monad
instance as its type, only the "return" value can be different between
expressions. 

Ideally, we would like the \hs{>>} operator to have a type like the following
\starthaskell
type Stateful s r = s -> (s, r)
(>>) :: Stateful s1 r1 -> Stateful s2 r2 -> Stateful (s1, s2) r2
\stophaskell

What we see here, is that when we compose two stateful functions (that
have already been applied to their inputs, leaving just the state
argument to be applied to), the result is again a stateful function
whose state is composed of the two \emph{substates}. The return value is
simply the return value of the second function, discarding the first (to
preserve that result, the \hs{>>=} operator can be used).

There is a trick we can apply to change the signature of the \hs{>>} operator.
\small{GHC} does not require the bind operators to be part of the \hs{Monad}
type class, as long as it can use them to translate the do notation. This
means we can define our own \hs{>>} and \hs{>>=} operators, outside of the
\hs{Monad} typeclass. This does conflict with the existing methods of the
\hs{Monad} typeclass, so we should prevent \small{GHC} from loading those (and
all of the Prelude) by passing \type{-XNoImplicitPrelude} to \type{ghc}. This
is slightly inconvenient, but since we hardly using anything from the prelude,
this is not a big problem. We might even be able to replace some of the
Prelude with hardware-translateable versions by doing this.

The binding operators can now be defined exactly as they are needed. For
completeness, the \hs{return} function is also defined. It is not called
by \small{GHC} implicitely, but can be called explicitely by a hardware
description. \in{Example}[ex:StateMonad] shows these definitions.

\startbuffer[StateMonad]
(>>) :: Stateful s1 r1 -> Stateful s2 r2 -> Stateful (s1, s2) r2
f1 >> f2 = f1 >>= \_ -> f2

(>>=) :: Stateful s1 r1 -> (r1 -> Stateful s2 r2) -> Stateful (s1, s2) r2
f1 >>= f2 = \(s1, s2) -> let (s1', r1) = f1 s1
                             (s2', r2) = f2 r1 s2
                         in ((s1', s2'), r2)
               
return :: r -> Stateful () r
return r = \s -> (s, r)
\stopbuffer
\placeexample[here][ex:StateMonad]{Binding operators to compose stateful computations}
  {\typebufferhs{StateMonad}}

These definitions closely resemble the boilerplate of unpacking state,
passing it to two functions and repacking the new state. With these
definitions, we could have writting \in{example}[ex:NestedState] a lot
shorter, see \in{example}[ex:DoState]. In this example the type signature of
foo is the same (though it is now written using the \hs{Stateful} type
synonym, it is still completely equivalent to the original: \hs{foo :: Word ->
FooState -> (FooState, Word)}.

Note that the \hs{FooState} type has changed (so indirectly the type of
\hs{foo} as well). Since the state composition by the \hs{>>} works on two
stateful functions at a time, the final state consists of nested two-tuples.
The final \hs{()} in the state originates from the fact that the \hs{return}
function has no real state, but is part of the composition. We could have left
out the return expression (and the \hs{outb <-} part) to make \hs{foo}'s return
value equal to \hs{funcb}'s, but this approach makes it clearer what is
happening.

\startbuffer[DoState]
  type FooState = ( AState, (BState, ()) )
  foo :: Word -> Stateful FooState Word
  foo in = do
      outa <- funca in
      outb <- funcb outa
      return outb
\stopbuffer
\placeexample[][ex:DoState]{Simple function composing two stateful
                                functions, using do notation.}
                               {\typebufferhs{DoState}}

An important implication of this approach is that the order of writing
function applications affects the state type. Fortunately, this problem can be
localized by consistently using type synonyms for state types, which should
prevent changes in other function's source when a function changes.

A less obvous implications of this approach is that the scope of variables
produced by each of these expressions (using the \hs{<-} syntax) is limited to
the expressions that come after it. This prevents values from flowing between
two functions (components) in two directions. For most Monad instances, this
is a requirement, but here it could have been different.

\todo{Add examples or reference for state synonyms}

\subsection{Alternative syntax}
Because of these typing issues, misusing Haskell's do notation is probably not
the best solution here. However, it does show that using fairly simple
abstractions, we could hide a lot of the boilerplate code. Extending
\small{GHC} with some new syntax sugar similar to the do notation might be a
feasible.

\subsection{Arrows}
Another abstraction mechanism offered by Haskell are arrows. Arrows are
a generalisation of monads \cite[hughes98], for which \GHC also supports
some syntax sugar \cite[paterson01]. Their use for hiding away state
boilerplate is not directly evident, but since arrows are a complex
concept further investigation is appropriate.

\section[sec:future:pipelining]{Improved notation or abstraction for pipelining}
Since pipelining is a very common optimization for hardware systems, it should
be easy to specify a pipelined system. Since it introduces quite some registers
into an otherwise regular combinatoric system, we might look for some way to
abstract away some of the boilerplate for pipelining.

Something similar to the state boilerplate removal above might be appropriate:
Abstract away some of the boilerplate code using combinators, then hide away
the combinators in special syntax. The combinators will be slightly different,
since there is a (typing) distinction between a pipeline stage and a pipeline
consisting of multiple stages. Also, it seems necessary to treat either the
first or the last pipeline stage differently, to prevent an off-by-one error
in the amount of registers (which is similar to the extra \hs{()} state type
in \in{example}[ex:DoState], which is harmless there, but would be a problem
if it introduced an extra, useless, pipeline stage).

This problem is slightly more complex than the problem we've seen before. One
significant difference is that each variable that crosses a stage boundary
needs a register. However, when a variable crosses multiple stage boundaries,
it must be stored for a longer period and should receive multiple registers.
Since we can't find out from the combinator code where the result of the
combined values is used (at least not without using Template Haskell to
inspect the \small{AST}), there seems to be no easy way to find how much
registers are needed.

There seem to be two obvious ways of handling this problem:

\startitemize
  \item Limit the scoping of each variable produced by a stage to the next
  stage only. This means that any variables that are to be used in subsequent
  stages should be passed on explicitely, which should allocate the required
  number of registers.

  This produces cumbersome code, where there is still a lot of explicitness
  (though this could be hidden in syntax sugar).
  \todo{The next sentence is unclear}
  \item Scope each variable over every subsequent pipeline stage and allocate
  the maximum amount of registers that \emph{could} be needed. This means we
  will allocate registers that are never used, but those could be optimized
  away later. This does mean we need some way to introduce a variable number
  of variables (depending on the total number of stages), assign the output of
  a different register to each (\eg., a different part of the state) and scope
  a different one of them over each the subsequent stages.

  This also means that when adding a stage to an existing pipeline will change
  the state type of each of the subsequent pipeline stages, and the state type
  ofthe added stage depends on the number of subsequent stages.

  Properly describing this will probably also require quite explicit syntax,
  meaning this is not feasible without some special syntax.
\stopitemize

Some other interesting issues include pipeline stages which are already
stateful, mixing pipelined with normal computation, etc.

\section{Recursion}
The main problems of recursion have been described in
\in{section}[sec:recursion]. In the current implementation, recursion is
therefore not possible, instead we rely on a number of implicitly list-recursive
builtin functions.

Since recursion is a very important and central concept in functional
programming, it would very much improve the flexibility and elegance of our
hardware descriptions if we could support (full) recursion.

For this, there are two main problems to solve:

\startitemize
\item For list recursion, how to make a description type check? It is quite
possible that improvements in the \small{GHC} typechecker will make this
possible, though it will still stay a challenge. Further advances in
dependent typing support for Haskell will probably help here as well.

\todo{Reference Christiaan and other type-level work
(http://personal.cis.strath.ac.uk/conor/pub/she/)}
\item For all recursion, there is the obvious challenge of deciding when
recursion is finished. For list recursion, this might be easier (Since the
base case of the recursion influences the type signatures). For general
recursion, this requires a complete set of simplification and evaluation
transformations to prevent infinite expansion. The main challenge here is how
to make this set complete, or at least define the constraints on possible
recursion that guarantee it will work.

\todo{Reference Christian for loop unrolling?}
\stopitemize

\section{Multiple clock domains and asynchronicity}
Cλash currently only supports synchronous systems with a single clock domain.
In a lot of real-world systems, both of these limitations pose problems.

There might be asynchronous events to which a system wants to respond. The
most obvious asynchronous event is of course a reset signal. Though a reset
signal can be synchronous, that is less flexible (and a hassle to describe in
Cλash, currently). Since every function in Cλash describes the behaviour on
each cycle boundary, we really can't fit in asynchronous behaviour easily.

Due to the same reason, multiple clock domains cannot be easily supported. There is
currently no way for the compiler to know in which clock domain a function
should operate and since the clock signal is never explicit, there is also no
way to express circuits that synchronize various clock domains.

A possible way to express more complex timing behaviour would be to make
functions more generic event handlers, where the system generates a stream of
events (Like \quote{clock up}, \quote{clock down}, \quote{input A changed},
\quote{reset}, etc.). When working with multiple clock domains, each domain
could get its own clock events.

\startbuffer[AsyncDesc]
data Event = ClockUp | Reset | ...

type MainState = State Word

-- Initial state
initstate :: MainState
initstate = State 0

main :: Word -> Event -> MainState -> (MainState, Word)
main inp event (State acc) = (State acc', acc')
  where
    acc' = case event of
      -- On a reset signal, reset the accumulator and output
      Reset -> initstate
      -- On a normal clock cycle, accumulate the result of func
      ClockUp -> acc + (func inp event)
      -- On any other event, leave state and output unchanged
      _ -> acc

-- func is some combinatoric expression
func :: Word -> Event -> Word
func inp _ = inp * 2 + 3
\stopbuffer

\placeexample[][ex:AsyncDesc]{Hardware description using asynchronous events.}
  {\typebufferhs{AsyncDesc}}

\todo{Picture}

\in{Example}[ex:AsyncDesc] shows a simple example of this event-based
approach. In this example we see that every function takes an input of
type \hs{Event}. The function \hs{main} that takes the output of
\hs{func} and accumulates it on every clock cycle. On a reset signal,
the accumulator is reset. The function \hs{func} is just a combinatoric
function, with no synchronous elements.  We can see this because there
is no state and the event input is completely ignored. If the compiler
is smart enough, we could even leave the event input out for functions
that don't use it, either because they are completely combinatoric (like
in this example), or because they rely on the the caller to select the
clock signal.

This structure is similar to the event handling structure used to perform I/O
in languages like Amanda. \todo{ref} There is a top level case expression that
decides what to do depending on the current input event.

A slightly more complex example is show in
\in{example}[ex:MulticlockDesc]. It shows a system with two clock
domains. There is no real integration between the clock domains in this
example (there is one input and one output for each clock domain), but
it does show how multiple clocks can be distinguished.

\startbuffer[MulticlockDesc]
data Event = ClockUpA | ClockUpB | ...

type MainState = State (SubAState, SubBState)

-- Initial state
initstate :: MainState
initstate = State (initsubastate, initsubbstate)

main :: Word -> Word -> Event -> MainState -> (MainState, Word, Word)
main inpa inpb event (State (sa, sb)) = (State (sa', sb'), outa, outb)
  where
    -- Only update the substates if the corresponding clock has an up
    -- transition.
    sa' = case event of
      ClockUpA -> sa''
      _ -> sa
    sb' = case event of
      ClockUpB -> sb''
      _ -> sb
    -- Always call suba and subb, so we can always have a value for our output
    -- ports.
    (sa'', outa) = suba inpa sa
    (sb'', outb) = subb inpb sb

type SubAState = State ...
suba :: Word -> SubAState -> (SubAState, Word)
suba = ...

type SubBState = State ...
subb :: Word -> SubAState -> (SubAState, Word)
subb = ...
\stopbuffer

\placeexample[][ex:MulticlockDesc]{Hardware description with multiple clock domains through events.}
  {\typebufferhs{MulticlockDesc}}

Note that in \in{example}[ex:MulticlockDesc] the \hs{suba} and \hs{subb}
functions are \emph{always} called, to get at their combinatoric
outputs. The new state is calculated as well, but only saved when the
right clock has an up transition.

As you can see, there is some code duplication in the case expression that
selects the right clock. One of the advantages of an explicit approach like
this, is that some of this duplication can be extracted away into helper
functions. For example, we could imagine a \hs{select_clock} function, which
takes a stateful function that is not aware of events, and changes it into a
function that only updates its state on a specific (clock) event. Such a
function is shown in \in{example}[ex:SelectClock].

\startbuffer[SelectClock]
select_clock :: Event
                -> (input -> State s -> (State s, output))
                -> (input -> State s -> Event -> (State s, output))
select_clock clock func inp state event = (state', out)
  where
    state' = if clock == event then state'' else state
    (state'', out) = func inp state

main :: Word -> Word -> Event -> MainState -> (MainState, Word, Word)
main inpa inpb event (State (sa, sb)) = (State (sa', sb'), outa, outb)
  where
    (sa'', outa) = (select_clock ClockUpA suba) inpa sa event
    (sb'', outb) = (select_clock ClockUpB subb) inpb sb event
\stopbuffer
\placeexample[][ex:SelectClock]{A function to filter clock events.}
  {\typebufferhs{SelectClock}}

As you can see, this can greatly reduce the length of the main function, while
increasing the readability. As you might also have noted, the select\_clock
function takes any stateful function from the current Cλash prototype and
turns it into an event-aware function!

Going along this route for more complex timing behaviour seems promising,
espicially since it seems possible to express very advanced timing behaviours,
while still allowing simple functions without any extra overhead when complex
behaviour is not needed.

The main cost of this approach will probably be extra complexity in the
compiler: The paths (state) data can take become very non-trivial, and it
is probably hard to properly analyze these paths and produce the
intended \VHDL description.

\section{Multiple cycle descriptions}
In the current Cλash prototype, every description is a single-cycle
description. In other words, every function describes behaviour for each
separate cycle and any recursion (or folds, maps, etc.) is expanded in space.

Sometimes, you might want to have a complex description that could possibly
take multiple cycles. Some examples include:

\startitemize
  \item Some kind of map or fold over a list that could be expanded in time
  instead of space. This would result in a function that describes n cycles
  instead of just one, where n is the lenght of the list.
  \item A large combinatoric expressions that would introduce a very long
  combinatoric path and thus limit clock frequency. Such an expression could
  be broken up into multiple stages, which effectively results in a pipelined
  system (see also \in{section}[sec:future:pipelining]) with a known delay.
  There should probably be some way for the developer to specify the cycle
  division of the expression, since automatically deciding on such a division
  is too complex and contains too many tradeoffs, at least initially.
  \item Unbounded recursion. It is not possible to expand unbounded (or even
  recursion with a depth that is not known at compile time) in space, since
  there is no way to tell how much hardware to create (it might even be
  infinite).

  When expanding infinite recursion over time, each step of the recursion can
  simply become a single clockcycle. When expanding bounded but unknown
  recursion, we probably need to add an extra data valid output bit or
  something similar.
\stopitemize

Apart from translating each of these multiple cycle descriptions into a per-cycle
description, we also need to somehow match the type signature of the multiple
cycle description to the type signature of the single cycle description that
the rest of the system expects (assuming that the rest of the system is
described in the \quote{normal} per-cycle manner). For example, an infinitely
recursive expression typically has the return type \lam{[a]}, while the rest
of the system would expect just \lam{a} (since the recursive expression
generates just a single element each cycle).

Naively, this matching could be done using a (builtin) function with a
signature like \lam{[a] -> a}, which also serves as an indicator to the
compiler that some expanding over time is required. However, this poses a
problem for simulation: How will our Haskell implementation of this magical
builtin function know which element of the input list to return. This
obviously depends on the current cycle number, but there is no way for this
function to know the current cycle without breaking all kinds of safety and
purity properties. Making this function have some state input and output could
help, though this state is not present in the actual hardware (or perhaps
there is some state, if there are value passed from one recursion step to the
next, but how can the type of that state be determined by the typechecker?).

It seems that this is the most pressing problem for multicycle descriptions:
How to interface with the rest of the system, without sacrificing safety and
simulation capabilities?

\section{Higher order values in state}
Another interesting idea is putting a higher order value inside a function's
state value. Since we can use higher order values anywhere, why not in the
state?

\startbuffer[HigherAccum]
-- The accumulator function that takes a word and returns a new accumulator
-- and the result so far. This is the function we want to put inside the
-- state.
type Acc = Word -> (Acc, Word)
acc = \a -> (\b -> acc ( a + b ), a )

main :: Word -> State Acc -> (State Acc, Word)
main a s = (State s', out)
  where (s', out) = s a
\stopbuffer
\placeexample[][ex:HigherAccum]{An accumulator using a higher order state.}
  {\typebufferhs{HigherAccum}}

As a (contrived) example, consider the accumulator in
\in{example}[ex:HigherAccum]. This code uses a function as its state,
which implicitely contains the value accumulated so far. This is a
fairly trivial example, that is more easy to write with a simple
\hs{Word} state value, but for more complex descriptions this style
might pay off. Note that in a way we are using the \emph{continuation
passing style} of writing functions, where we pass a sort of
\emph{continuation} from one cycle to the next.

Our normalization process completely removes higher order values inside a
function by moving applications and higher order values around so that every
higher order value will eventually be full applied. However, if we would put a
higher order value inside our state, the path from the higher order value
definition to its application runs through the state, which is external to the
function. A higher order value defined in one cycle is not applied until a
later cycle. Our normalization process only works within the function, so it
cannot remove this use of a higher order value.

However, we cannot leave a higher order value in our state value, since it is
impossible to generate a register containing a higher order value, we simply
can't translate a function type to a hardware type. To solve this, we must
replace the higher order value inside our state with some other value
representing these higher order values.

On obvious approach here is to use an algebraic datatype where each
constructor represents one possible higher order value that can end up in the
state and each constructor has an argument for each free variable of the
higher order value replaced. This allows us to completely reconstruct the
higher order value at the spot where it is applied, and thus the higher order
value disappears.

This approach is commonly known as the \quote{Reynolds approach to
defuntionalization}, first described by J.C. Reynolds and seems to apply well
to this situation. One note here is that Reynolds' approach puts all the
higher order values in a single datatype. For a typed language, we will at
least have to have a single datatype for each function type, since we can't
mix them. It would be even better to split these datatypes a bit further, so
that such a datatype will never hold a constructor that is never used for a
particular state variable. This separation is probably a non-trivial problem,
though.

\todo{Reference "Definitional interpreters for higher-order programming
languages":
http://portal.acm.org/citation.cfm?id=805852\&dl=GUIDE\&coll=GUIDE\&CFID=58835435\&CFTOKEN=81856623}

\section{New language}
During the development of the prototype, it has become clear that Haskell is
not the perfect language for this work. There are two main problems:
\startitemize
\item Haskell is not expressive enough. Haskell is still quite new in the area
of dependent typing, something we use extensively. Also, Haskell has some
special syntax to write monadic composition and arrow composition, which is
well suited to normal Haskell programs. However, for our hardware
descriptions, we could use some similar, but other, syntactic sugar (as we
have seen above).
\item Haskell is too expressive. There are some things that Haskell can
express, but we can never properly translate. There are certain types (both
primitive types and certain type constructions like recursive types) we can
never translate, as well as certain forms of recursion.
\stopitemize

It might be good to reevaluate the choice of language for Cλash, perhaps there
are other languages which are better suited to describe hardware, now that
we've learned a lot about it.

Perhaps Haskell (or some other language) can be extended by using a
preprocessor. There has been some (point of proof) work on a the Strathclyde
Haskell Enhancement (\small{SHE}) preprocessor for type-level programming,
perhaps we can extend that, or create something similar for hardware-specific
notation.

It is not unlikely that the most flexible way
forward would be to define a completely new language with exactly the needed
features. This is of course an enormous effort, which should not be taken
lightly.

\section{Don't care values}
  A powerful value in \VHDL is the \emph{don't care} value, given as
  \type{'-'}. This value tells the compiler that you don't really care about
  which value is assigned to a signal, allowing the compiler to make some
  optimizations. Since hardware choice in hardware is often implemented using
  a collection of logic gates instead of multiplexers only, synthesizers can
  often reduce the amount of hardware needed by smartly choosing values for
  these don't care cases.

  There is not really anything comparable with don't care values in normal
  programming languages. The closest thing is an undefined or uninitialized
  value, though those are usually associated with error conditions.

  It would be useful if Cλash also has some way to specify don't care values.
  When looking at the Haskell typing system, there are really two ways to do
  this:

  \startitemize
    \item Add a special don't care value to every datatype. This includes the
    obvious \hs{Bit} type, but will also need to include every user defined
    type. An exception can be made for vectors and product types, since those
    can simply use the don't care values of the types they contain.

    This would also require some kind of \quote{Dont careable} type class
    that allows each type to specify what its don't care value is. The
    compiler must then recognize this constant and replace it with don't care
    values in the final \VHDL code.

    This is of course a very intrusive solution. Every type must become member
    of this typeclass, and there is now some member in every type that is a
    special don't care value. Guaranteeing the obvious don't care semantics
    also becomes harder, since every pattern match or case expressions must now
    also take care of the don't care value (this might actually be an
    advantage, since it forces designers to specify how to handle don't care
    for different operations).

    \item Use the special \hs{undefined}, or \emph{bottom} value present in
    Haskell. This is a type that is member of all types automatically, without
    any explicit declarations.

    Any expression that requires evaluation of an undefined value
    automatically becomes undefined itself (or rather, there is some exception
    mechanism). Since Haskell is lazy, this means that whenever it tries to
    evaluate undefined, it is apparently required for determining the output
    of the system. This property is useful, since typically a don't care
    output is used when some output is not valid and should not be read. If
    it is in fact not read, it should never be evaluated and simulation should
    be fine.

    In practice, this works less ideal. In particular, pattern matching is not
    always smart enough to deal with undefined. Consider the following
    definition of an \hs{and} operator:

    \starthaskell
    or :: Bit -> Bit -> Bit
    and Low _ = Low
    and _ Low = Low
    and High High = High
    \stophaskell

    When using the \hs{and} operation on an undefined (don't care) and a Low
    value should always return a Low value. Its value does not depend on the
    value chosen for the don't care value. However, though when applying the
    above and function to \hs{Low} and \hs{undefined} results in exactly that
    behviour, the result is \hs{undefined} when the arguments are swapped.
    This is because the first pattern forces the first argument to be
    evaluated. If it is \hs{undefined}, evaluation is halted and an exception
    is show, which is not what is intended.
  \stopitemize

  These options should be explored further to see if they provide feasible
  methods for describing don't care conditions. Possibly there are completely
  other methods which work better.

\section{Correctness proofs of the normalization system}
As stated in \in{section}[sec:normalization:properties], there are a
number of properties we would like to see verified about the
normalization system.  In particular, the \emph{termination} and
\emph{completeness} of the system would be a good candidate for future
research. Specifying formal semantics for the Core language in
order to verify the \emph{soundness} of the system would be an even more
challenging task.
% vim: set sw=2 sts=2 expandtab: