\chapter[chap:future]{Future work}
\section{Improved notation for hierarchical state}
-The hierarchic state model requires quite some boilerplate code for unpacking
+The hierarchical state model requires quite some boilerplate code for unpacking
and distributing the input state and collecting and repacking the output
state.
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 seemed promising, whas he \hs{do}
+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
will be desugared into:
\starthaskell
-(somefunc a b) >> (otherfunc b c)
+(somefunc a) >> (otherfunc b)
\stophaskell
+\todo{Properly introduce >>=}
There is also the \hs{>>=} operator, which allows for passing variables from
one expression to the next. If we could use this notation to compose a
stateful computation from a number of other stateful functions, this could
descriptions: We can use the language itself to provide abstractions of common
patterns, making our code smaller.
-\subsection{Outside the Monad}
+\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:
f1 >> f2 = f1 >>= \_ -> f2
(>>=) :: Stateful s1 r1 -> (r1 -> Stateful s2 r2) -> Stateful (s1, s2) r2
-f1 >>= f2 = \\(s1, s2) -> let (s1', r1) = f1 s1
+f1 >>= f2 = \(s1, s2) -> let (s1', r1) = f1 s1
(s2', r2) = f2 r1 s2
in ((s1', s2'), r2)
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 completel equivalent to the original: \hs{foo :: Word ->
+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
type FooState = ( AState, (BState, ()) )
foo :: Word -> Stateful FooState Word
foo in = do
- outa <- funca in sa
- outb <- funcb outa sb
+ outa <- funca in
+ outb <- funcb outa
return outb
\stopbuffer
\placeexample[here][ex:DoState]{Simple function composing two stateful
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 the above issues, misusing Haskell's do notation is probably not
+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
\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 involves quite some registers
+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.
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 registers. However, when a variable crosses multiple stage boundaries,
+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
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
\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 implicit list-recursive
+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.
+hardware descriptions if we could support (full) recursion.
For this, there are two main problems to solve:
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/)
+\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 which guarantee it will work.
+recursion that guarantee it will work.
-TODO: Loop unrolling
+\todo{Reference Christian for loop unrolling?}
\stopitemize
\section{Multiple clock domains and asynchronicity}
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 supported. There is
+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.
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 events.
+could get its own clock events.
As an example, we would have something like the following:
func inp _ = inp * 2 + 3
\stophaskell
-TODO: Picture
+\todo{Picture}
In this example, we see that every function takes an input of type
\hs{Event}. The function \hs{main} that takes the output of
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
+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 that shows a system with two clock domains.
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.
+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
particular state variable. This separation is probably a non-trivial problem,
though.
-TODO: Reference "Definitional interpreters for higher-order programming
+\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
+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
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 statement 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: