X-Git-Url: https://git.stderr.nl/gitweb?p=matthijs%2Fmaster-project%2Freport.git;a=blobdiff_plain;f=Chapters%2FFuture.tex;h=9c60dfe8e3b8f656ef0bd8a74e67fa6a98b4e80b;hp=f61044dceb7f1f0091a083a0173ce750c4412f0b;hb=b2047c9f1622d62aecc6708dd19c38b14810f275;hpb=1b9665a243799137f9b3f2b04e13489ba6f66e5e

diff --git a/Chapters/Future.tex b/Chapters/Future.tex
index f61044d..9c60dfe 100644
--- a/Chapters/Future.tex
+++ b/Chapters/Future.tex
@@ -1,6 +1,6 @@
 \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.
 
@@ -29,7 +29,7 @@ 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
 using the monadic \emph{bind} operator, written in Haskell as \hs{>>}. For
@@ -44,9 +44,10 @@ do
 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
@@ -58,7 +59,7 @@ 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{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:
@@ -117,7 +118,7 @@ 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 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
@@ -133,8 +134,8 @@ 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
@@ -152,8 +153,10 @@ 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
@@ -161,7 +164,7 @@ 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.
 
@@ -177,7 +180,7 @@ 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 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
@@ -194,6 +197,7 @@ There seem to be two obvious ways of handling this problem:
 
   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
@@ -216,12 +220,12 @@ 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
+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:
 
@@ -239,7 +243,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
@@ -254,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.
@@ -263,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:
 
@@ -387,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
@@ -611,3 +615,13 @@ 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.
+
+\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: