Fix spelling as suggested by aspell.
[matthijs/master-project/report.git] / Chapters / Future.tex
index f61044d..523fc0a 100644 (file)
@@ -1,6 +1,46 @@
 \chapter[chap:future]{Future work}
+\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 have 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{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.
+
 \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.
 
@@ -29,9 +69,9 @@ 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 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
+details. It allows one to write a list of expressions, which are composed
 using the monadic \emph{bind} operator, written in Haskell as \hs{>>}. For
 example, the snippet:
 
@@ -44,21 +84,49 @@ do
 will be desugared into:
 
 \starthaskell
-(somefunc a b) >> (otherfunc b c)
+(somefunc a) >> (otherfunc b)
 \stophaskell
 
-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.
+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 behavior in the binding operators.
+
+The \hs{>>=} operator allows extracting the actual result of a function
+and passing it to another function. The following snippet should
+illustrate this:
 
-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.
+\starthaskell
+do
+  x <- somefunc a
+  otherfunc x
+\stophaskell
 
-\subsection{Outside the Monad}
+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 has 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:
@@ -77,29 +145,30 @@ 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).
+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
+\hs{Monad} type class. This does conflict with the existing methods of the
+\hs{Monad} type class, 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.
+Prelude with hardware-translatable 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.
+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} implicitly, but can be called explicitly by a hardware
+description. \in{Example}[ex:StateMonad] shows these definitions.
 
-\starthaskell
+\startbuffer[StateMonad]
 (>>) :: Stateful s1 r1 -> Stateful s2 r2 -> Stateful (s1, s2) r2
 f1 >> f2 = f1 >>= \_ -> f2
 
@@ -110,14 +179,16 @@ f1 >>= f2 = \(s1, s2) -> let (s1', r1) = f1 s1
                
 return :: r -> Stateful () r
 return r = \s -> (s, r)
-\stophaskell
+\stopbuffer
+\placeexample[here][ex:StateMonad]{Binding operators to compose stateful computations}
+  {\typebufferhs{StateMonad}}
 
-As you can see, this closely resembles the boilerplate of unpacking state,
+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
+definitions, we could have written \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
@@ -125,7 +196,7 @@ Note that the \hs{FooState} type has changed (so indirectly the type of
 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
+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.
 
@@ -133,11 +204,11 @@ happening.
   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
+\placeexample[][ex:DoState]{Simple function composing two stateful
                                 functions, using do notation.}
                                {\typebufferhs{DoState}}
 
@@ -146,23 +217,32 @@ 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
+A less obvious 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 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
 feasible.
 
+\subsection{Arrows}
+Another abstraction mechanism offered by Haskell are arrows. Arrows are
+a generalization 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 involves quite some registers
-into an otherwise regular combinatoric system, we might look for some way to
+be easy to specify a pipelined system. Since it introduces quite some registers
+into an otherwise regular combinational 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:
@@ -175,11 +255,11 @@ 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
+This problem is slightly more complex than the problem we have 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
+Since we cannot 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.
@@ -189,13 +269,14 @@ 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
+  stages should be passed on explicitly, 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
+  the maximum number 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
@@ -204,7 +285,7 @@ There seem to be two obvious ways of handling this problem:
 
   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.
+  of the 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.
@@ -216,18 +297,18 @@ 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 implicit list-recursive
-builtin functions.
+therefore not possible, instead we rely on a number of implicitly list-recursive
+built-in 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:
 
 \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 that improvements in the \small{GHC} type-checker 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.
 
@@ -239,7 +320,7 @@ 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{Reference Christian for loop unrolling?}
 \stopitemize
@@ -251,23 +332,21 @@ 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.
+Cλash, currently). Since every function in Cλash describes the behavior on
+each cycle boundary, we really cannot fit in asynchronous behavior 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.
 
-A possible way to express more complex timing behaviour would be to make
+A possible way to express more complex timing behavior 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:
-
-\starthaskell
+\startbuffer[AsyncDesc]
 data Event = ClockUp | Reset | ...
 
 type MainState = State Word
@@ -287,33 +366,39 @@ main inp event (State acc) = (State acc', acc')
       -- On any other event, leave state and output unchanged
       _ -> acc
 
--- func is some combinatoric expression
+-- func is some combinational expression
 func :: Word -> Event -> Word
 func inp _ = inp * 2 + 3
-\stophaskell
+\stopbuffer
+
+\placeexample[][ex:AsyncDesc]{Hardware description using asynchronous events.}
+  {\typebufferhs{AsyncDesc}}
 
 \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
-\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.
+\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 combinational
+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 do not use it, either because they are completely combinational (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 that shows a system with two clock domains.
-There is no real integration between the clock domains (there is one input and
-one output for each clock domain), but it does show how multiple clocks can be
-distinguished.
+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.
 
-\starthaskell
+\startbuffer[MulticlockDesc]
 data Event = ClockUpA | ClockUpB | ...
 
 type MainState = State (SubAState, SubBState)
@@ -345,21 +430,25 @@ suba = ...
 type SubBState = State ...
 subb :: Word -> SubAState -> (SubAState, Word)
 subb = ...
-\stophaskell
+\stopbuffer
 
-Note that in the above example 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.
+\placeexample[][ex:MulticlockDesc]{Hardware description with multiple clock domains through events.}
+  {\typebufferhs{MulticlockDesc}}
 
-As you can see, there is some code duplication in the case statement that
+Note that in \in{example}[ex:MulticlockDesc] the \hs{suba} and \hs{subb}
+functions are \emph{always} called, to get at their combinational
+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.
+function that only updates its state on a specific (clock) event. Such a
+function is shown in \in{example}[ex:SelectClock].
 
-\starthaskell
+\startbuffer[SelectClock]
 select_clock :: Event
                 -> (input -> State s -> (State s, output))
                 -> (input -> State s -> Event -> (State s, output))
@@ -373,26 +462,28 @@ 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
-\stophaskell
+\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,
+Going along this route for more complex timing behavior seems promising,
+especially since it seems possible to express very advanced timing behaviors,
 while still allowing simple functions without any extra overhead when complex
-behaviour is not needed.
+behavior 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.
+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
+description. In other words, every function describes behavior 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
@@ -401,21 +492,21 @@ 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
+  instead of just one, where n is the length of the list.
+  \item A large combinational expressions that would introduce a very long
+  combinational 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.
+  is too complex and contains too many trade-offs, 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
+  simply become a single clock cycle. When expanding bounded but unknown
   recursion, we probably need to add an extra data valid output bit or
   something similar.
 \stopitemize
@@ -429,30 +520,28 @@ 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
+Naively, this matching could be done using a (built-in) 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
+problem for simulation: how will our Haskell implementation of this magical
+built-in 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?).
+next, but how can the type of that state be determined by the type-checker?).
 
-It seems that this is the most pressing problem for multicycle descriptions:
+It seems that this is the most pressing problem for multi-cycle 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
+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?
 
-As a (contrived) example, consider the following accumulator:
-
-\starthaskell
+\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.
@@ -462,87 +551,56 @@ 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
-\stophaskell
-
-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
+\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 implicitly 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
+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.
+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.
+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
+cannot 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
+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
+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.
+defunctionalization}, first described by J.C. Reynolds \cite[reynolds98]\ 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 cannot mix them. It would be even better to split these
+data-types 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.
 
 \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
+  A powerful value in \VHDL\ is the \emph{don't care} value, given as
+  \type{'-'}. This value tells the compiler that you do not 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
+  optimizations. Since 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.
@@ -561,15 +619,15 @@ lightly.
     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
+    This would also require some kind of \quote{Don't 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.
+    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
+    of this type class, 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 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).
@@ -592,7 +650,7 @@ lightly.
     definition of an \hs{and} operator:
 
     \starthaskell
-    or :: Bit -> Bit -> Bit
+    and :: Bit -> Bit -> Bit
     and Low _ = Low
     and _ Low = Low
     and High High = High
@@ -602,7 +660,7 @@ lightly.
     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.
+    behavior, 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.
@@ -611,3 +669,5 @@ lightly.
   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.
+
+% vim: set sw=2 sts=2 expandtab: