X-Git-Url: https://git.stderr.nl/gitweb?p=matthijs%2Fmaster-project%2Freport.git;a=blobdiff_plain;f=Chapters%2FFuture.tex;h=38d618ff89906090885a9f359ee97e36dfbfc193;hp=daeee3fd10844b351fde9109a96656bd73bd79b5;hb=19c17205efa182b80916caa31afeadad9d2dd5b5;hpb=100a8917713c1300a2002299cea94b04ac66848a

diff --git a/Chapters/Future.tex b/Chapters/Future.tex
index daeee3f..38d618f 100644
--- a/Chapters/Future.tex
+++ b/Chapters/Future.tex
@@ -47,13 +47,40 @@ will be desugared into:
 (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.
+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 is highlights an important aspect of using a functional language for our
 descriptions: We can use the language itself to provide abstractions of common
@@ -126,7 +153,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.
 
@@ -356,7 +383,7 @@ Note that in the above example the \hs{suba} and \hs{subb} functions are
 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 statement that
+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
@@ -391,8 +418,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
@@ -573,7 +600,7 @@ lightly.
     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 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).
@@ -616,4 +643,12 @@ lightly.
   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: