Use η/β-expansion instead of η/β-abstraction.
[matthijs/master-project/report.git] / Chapters / Prototype.tex
index bad0d0647646f97ac552c97b4b6feb0d68d90ba9..101594bf2a9b4aaacbd210c1242fd968ed0f2fa7 100644 (file)
@@ -73,7 +73,7 @@
     Haskell an obvious choice.
 
   \section[sec:prototype:output]{Output format}
-    The second important question is: What will be our output format?
+    The second important question is: what will be our output format?
     This output format should at least allow for programming the
     hardware design into a field-programmable gate array (\small{FPGA}).
     The choice of output format is thus limited by what hardware
       func arg
       \stoplambda
       This is function application. Each application consists of two
-      parts: The function part and the argument part. Applications are used
+      parts: the function part and the argument part. Applications are used
       for normal function \quote{calls}, but also for applying type
       abstractions and data constructors.
 
       
       A case expression evaluates its scrutinee, which should have an
       algebraic datatype, into weak head normal form (\small{WHNF}) and
-      (optionally) binds it to \lam{bndr}. Every alternative lists a
-      single constructor (\lam{C0 ... Cn}). Based on the actual
-      constructor of the scrutinee, the corresponding alternative is
-      chosen. The binders in the chosen alternative (\lam{bndr0,0 ....
-      bndr0,m} are bound to the actual arguments to the constructor in
-      the scrutinee.
+      (optionally) binds it to \lam{bndr}. If bndr is wild, \refdef{wild
+      binders} it is left out.  Every alternative lists a single constructor
+      (\lam{C0 ... Cn}). Based on the actual constructor of the scrutinee, the
+      corresponding alternative is chosen. The binders in the chosen
+      alternative (\lam{bndr0,0 ....  bndr0,m} are bound to the actual
+      arguments to the constructor in the scrutinee.
 
       This is best illustrated with an example. Assume
       there is an algebraic datatype declared as follows\footnote{This
       families and other non-standard Haskell stuff which we do not (plan to)
       support.
 
+      \placeintermezzo{}{
+        \startframedtext[width=8cm,background=box,frame=no]
+        \startalignment[center]
+          {\tfa The \hs{id} function}
+        \stopalignment
+        \blank[medium]
+          A function that is probably present in every functional language, is
+          the \emph{identity} function. This is the function that takes a
+          single argument and simply returns it unmodified. In Haskell this
+          function is called \hs{id} and can take an argument of any type
+          (\ie, it is polymorphic).
+
+          The \hs{id} function will be used in the examples every now and
+          then.
+        \stopframedtext
+      }
       In Core, every expression is typed. The translation to Core happens
       after the typechecker, so types in Core are always correct as well
       (though you could of course construct invalidly typed expressions
       Word} and \hs{Word} types by pattern matching and by using the explicit
       the \hs{State constructor}.
 
-      This explicit conversion makes the \VHDL\ generation easier: Whenever we
+      This explicit conversion makes the \VHDL\ generation easier: whenever we
       remove (unpack) the \hs{State} type, this means we are accessing the
       current state (\eg, accessing the register output). Whenever we are a
       adding (packing) the \hs{State} type, we are producing a new value for
       function.
 
       Fortunately, the \lam{accs'} variable (and any other substate) has a
-      property that we can easily check: It has a \lam{State} type
+      property that we can easily check: it has a \lam{State} type
       annotation. This means that whenever \VHDL\ is generated for a tuple
       (or other algebraic type), we can simply leave out all elements that
       have a \lam{State} type. This will leave just the parts of the state
       \stoplambda
               
       When we would really leave out the crossed out parts, we get a slightly
-      weird program: There is a variable \lam{s} which has no value, and there
+      weird program: there is a variable \lam{s} which has no value, and there
       is a variable \lam{s'} that is never used. Together, these two will form
       the state process of the function. \lam{s} contains the "current" state,
       \lam{s'} is assigned the "next" state. So, at the end of each clock