Add initial sketch for conclusions.
[matthijs/master-project/report.git] / Chapters / Future.tex
index 38904bea13edb937ff83be17dac29f56b928ae77..9c60dfe8e3b8f656ef0bd8a74e67fa6a98b4e80b 100644 (file)
 \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. There is really only one way in which this state handling can be done,
-so it would make sense to hide this boilerplate. This would incur no
-flexibility cost at all, since there are no other ways that would work.
+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:
 
-Options: Misuse the do notation in Haskell, create some abstraction in
-Haskell or add new syntax.
+\starthaskell
+do
+  somefunc a
+  otherfunc b
+\stophaskell
+
+will be desugared into:
+
+\starthaskell
+(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
+move all the boilerplate code into the \hs{>>} operator. Perhaps the compiler
+should be taught to always inline the \hs{>>} operator, but after that there
+should be no further changes required to the compiler.
+
+This is 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.
+
+\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 (whose inputs
+have already been applied, leaving just the state argument to be applied), 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 one, 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.
+
+We can now define the following binding operators. For completeness, we also
+supply the return function, which is not called by \small{GHC} implicitely,
+but can be called explicitely by a hardware description.
+
+\starthaskell
+(>>) :: 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)
+\stophaskell
+
+As you can see, this closely resembles 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 statement (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[here][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.
 
 \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.
 
-Example of naive pipelined code
+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:
 
-Using monadic do does not fit the typing
+\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
 
-Using custom combinators would work
+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
-\at{section}[sec:recursion]. In the current implementation, recursion is
-therefore not possible, instead we rely on a number of implicit list-recursive
+\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.
+hardware descriptions if we could support (full) recursion.
 
 For this, there are two main problems to solve:
 
@@ -39,17 +235,17 @@ 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/)
+\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}
@@ -62,7 +258,7 @@ 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 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.
@@ -71,7 +267,7 @@ 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 events.
+could get its own clock events.
 
 As an example, we would have something like the following:
 
@@ -100,7 +296,7 @@ func :: Word -> Event -> Word
 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
@@ -113,7 +309,7 @@ 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
+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.
@@ -195,8 +391,8 @@ 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.
+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
@@ -213,7 +409,7 @@ take multiple cycles. Some examples include:
   \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 \at{section}[sec:future:pipelining]) with a known delay.
+  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.
@@ -311,9 +507,9 @@ 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
+\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
@@ -345,3 +541,87 @@ 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 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: