Partially update state annotations section in the prototype chapter.
[matthijs/master-project/report.git] / Chapters / Prototype.tex
index ac4cc93e29023e8d319b54537cfa2a0f45eb968f..794aa347b1ffc065688dc60f9f122dde642b0bee 100644 (file)
@@ -51,8 +51,6 @@
     primary compiler, \GHC, provides a high level API to its internals, made
     Haskell an obvious choice.
 
-    \note{There should be evaluation of the choice of Haskell and \VHDL}
-
   \section[sec:prototype:output]{Output format}
     The second important question is: What will be our output format? Since
     our prototype won't be able to program FPGA's directly, we'll have to have
         instance declaration. This dictionary, as well as the binder
         introduced by a lambda that introduces a dictionary, have the
         predicate type as their type. These binders are usually named starting
-        with a \lam{$}. Usually the name of the type concerned is not
+        with a \lam{\$}. Usually the name of the type concerned is not
         reflected in the name of the dictionary, but the name of the type
         class is. The Haskell expression \hs{show True} thus becomes:
 
         \startlambda
-        show @Bool $dShow True
+        show @Bool \$dShow True
         \stoplambda
       \stopdesc
 
       here)}.
         
   \section[sec:prototype:statetype]{State annotations in Haskell}
-      \fxnote{This entire section on state annotations should be reviewed}
-
-      Ideal: Type synonyms, since there is no additional code overhead for
-      packing and unpacking. Downside: there is no explicit conversion in Core
-      either, so type synonyms tend to get lost in expressions (they can be
-      preserved in binders, but this makes implementation harder, since that
-      statefulness of a value must be manually tracked).
-
-      Less ideal: Newtype. Requires explicit packing and unpacking of function
-      arguments. If you don't unpack substates, there is no overhead for
-      (un)packing substates. This will result in many nested State constructors
-      in a nested state type. \eg: 
+    As noted in \in{section}[sec:description:stateann], Cλash needs some
+    way to let the programmer explicitly specify which of a function's
+    arguments and which part of a function's result represent the
+    function's state.
+
+    Using the Haskell type systems, there are a few ways we can tackle this.
+
+    \subsection{Type synonyms}
+      Haskell provides type synonyms as a way to declare a new type that is
+      equal to an existing type (or rather, a new name for an existing type).
+      This allows both the original type and the synonym to be used
+      interchangedly in a Haskell program. This means no explicit conversion
+      is needed either. For example, a simple accumulator would become:
+
+      \starthaskell
+      type State s = s
+      acc :: Word -> State Word -> (State Word, Word)
+      acc i s = let sum = s + i in (sum, sum)
+      \stophaskell
+
+      This looks nice in Haskell, but turns out to be hard to implement. There
+      are no explicit conversion in Haskell, but not in Core either. This
+      means the type of a value might be show as \hs{AccState} in some places,
+      but \hs{Word} in others (and this can even change due to
+      transformations). Since every binder has an explicit type associated
+      with it, the type of every function type will be properly preserved and
+      could be used to track down the statefulness of each value by the
+      compiler. However, this makes the implementation a lot more complicated
+      than it currently is using \hs{newtypes}.
+    \subsection{Type renaming (\hs{newtype})}
+      Haskell also supports type renamings as a way to declare a new type that
+      has the same (runtime) representation as an existing type (but is in
+      fact a different type to the typechecker). With type renaming, an
+      explicit conversion between values of the two types is needed. The
+      accumulator would then become:
+
+      \starthaskell
+      newtype State s = State s
+      acc :: Word -> State Word -> (State Word, Word)
+      acc i (State s) = let sum = s + i in (State sum, sum)
+      \stophaskell
+
+      The \hs{newtype} line declares a new type \hs{State} that has one type
+      argument, \hs{s}. This type contains one \quote{constructor} \hs{State}
+      with a single argument of type \hs{s}. It is customary to name the
+      constructor the same as the type, which is allowed (since types can
+      never cause name collisions with values). The difference with the type
+      synonym example is in the explicit conversion between the \hs{State
+      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
+      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
+      the state (\eg, providing the register input).
+
+      When dealing with nested states (a stateful function that calls stateful
+      functions, which might call stateful functions, etc.) the state type
+      could quickly grow complex because of all the \hs{State} type constructors
+      needed. For example, consider the following state type (this is just the
+      state type, not the entire function type):
 
       \starttyping
       State (State Bit, State (State Word, Bit), Word)
       \stoptyping
 
-      Alternative: Provide different newtypes for input and output state. This
-      makes the code even more explicit, and typechecking can find even more
-      errors. However, this requires defining two type synomyms for each
-      stateful function instead of just one. \eg:
-
-      \starttyping
-      type AccumStateIn = StateIn Bit
-      type AccumStateOut = StateOut Bit
-      \stoptyping
-
-      This also increases the possibility of having different input and output
-      states. Checking for identical input and output state types is also
-      harder, since each element in the state must be unpacked and compared
-      separately.
-
-      Alternative: Provide a type for the entire result type of a stateful
-      function, not just the state part. \eg:
-
-      \starttyping
-      newtype Result state result = Result (state, result)
-      \stoptyping
-      
-      This makes it easy to say "Any stateful function must return a
-      \type{Result} type, without having to sort out result from state. However,
-      this either requires a second type for input state (similar to
-      \type{StateIn} / \type{StateOut} above), or requires the compiler to
-      select the right argument for input state by looking at types (which works
-      for complex states, but when that state has the same type as an argument,
-      things get ambiguous) or by selecting a fixed (\eg, the last) argument,
-      which might be limiting.
+      We cannot leave all these \hs{State} type constructors out, since that
+      would change the type (unlike when using type synonyms). However, when
+      using type synonyms to hide away substates, \todo{see below} this
+      disadvantage should be limited.
+
+      \subsubsection{Different input and output types}
+        An alternative could be to use different types for input and output
+        state (\ie current and updated state). The accumulator example would
+        then become something like:
+
+        \starthaskell
+        newtype StateIn s = StateIn s
+        newtype StateOut s = StateOut s
+        acc :: Word -> StateIn Word -> (StateIn Word, Word)
+        acc i (StateIn s) = let sum = s + i in (StateIn sum, sum)
+        \stophaskell
+        
+        This could make the implementation easier and the hardware
+        descriptions less errorprone (you can no longer \quote{forget} to
+        unpack and repack a state variable and just return it directly, which
+        can be a problem in the current prototype). However, it also means we
+        need twice as many type synonyms to hide away substates, making this
+        approach a bit cumbersome. It also makes it harder to copmare input
+        and output state types, possible reducing the type safety of the
+        descriptions.
+
+    \subsection{Type synonyms for substates}
+      As noted above, when using nested (hierarchical) states, the state types
+      of the \quote{upper} functions (those that call other functions, which
+      call other functions, etc.) quickly becomes complicated. Also, when the
+      state type of one of the \quote{lower} functions changes, the state
+      types of all the upper functions changes as well. If the state type for
+      each function is explicitly and completely specified, this means that a
+      lot of code needs updating whenever a state type changes.
+
+      To prevent this, it is recommended (but not enforced) to use a type
+      synonym for the state type of every function. Every function calling
+      other functions will then use the state type synonym of the called
+      functions in its own type, requiring no code changes when the state type
+      of a called function changes. This approach is used in
+      \in{example}[ex:AvgState] below. The \hs{AccState} and \hs{AvgState}
+      are examples of such state type synonyms.
+
+    \subsection{Chosen approach}
+      To keep implementation simple, the current prototype uses the type
+      renaming approach, with a single type for both input and output states.
+      \todo{}
 
       \subsubsection{Example}
-      As an example of the used approach, a simple averaging circuit, that lets
-      the accumulation of the inputs be done by a subcomponent.
-
-      \starttyping
-        newtype State s = State s
-
-        type AccumState = State Bit
-        accum :: Word -> AccumState -> (AccumState, Word)
-        accum i (State s) = (State (s + i), s + i)
-
-        type AvgState = (AccumState, Word)
-        avg :: Word -> AvgState -> (AvgState, Word)
-        avg i (State s) = (State s', o)
-          where
-            (accums, count) = s
-            -- Pass our input through the accumulator, which outputs a sum
-            (accums', sum) = accum i accums
-            -- Increment the count (which will be our new state)
-            count' = count + 1
-            -- Compute the average
-            o = sum / count'
-            s' = (accums', count')
-      \stoptyping
-
-      And the normalized, core-like versions:
-
-      \starttyping
-        accum i spacked = res
-          where
-            s = case spacked of (State s) -> s
-            s' = s + i
-            spacked' = State s'
-            o = s + i
-            res = (spacked', o)
-
-        avg i spacked = res
-          where
-            s = case spacked of (State s) -> s
-            accums = case s of (accums, \_) -> accums
-            count = case s of (\_, count) -> count
-            accumres = accum i accums
-            accums' = case accumres of (accums', \_) -> accums'
-            sum = case accumres of (\_, sum) -> sum
-            count' = count + 1
-            o = sum / count'
-            s' = (accums', count')
-            spacked' = State s'
-            res = (spacked', o)
-      \stoptyping
-
-
-
-      As noted above, any component of a function's state that is a substate,
-      \eg passed on as the state of another function, should have no influence
-      on the hardware generated for the calling function. Any state-specific
-      \small{VHDL} for this component can be generated entirely within the called
-      function. So,we can completely leave out substates from any function.
-      
-      From this observation, we might think to remove the substates from a
-      function's states alltogether, and leave only the state components which
-      are actual states of the current function. While doing this would not
-      remove any information needed to generate \small{VHDL} from the function, it would
-      cause the function definition to become invalid (since we won't have any
-      substate to pass to the functions anymore). We could solve the syntactic
-      problems by passing \type{undefined} for state variables, but that would
-      still break the code on the semantic level (\ie, the function would no
-      longer be semantically equivalent to the original input).
-
-      To keep the function definition correct until the very end of the process,
-      we will not deal with (sub)states until we get to the \small{VHDL} generation.
-      Here, we are translating from Core to \small{VHDL}, and we can simply not generate
-      \small{VHDL} for substates, effectively removing the substate components
-      alltogether.
-
-      There are a few important points when ignore substates.
-
-      First, we have to have some definition of "substate". Since any state
-      argument or return value that represents state must be of the \type{State}
-      type, we can simply look at its type. However, we must be careful to
-      ignore only {\em substates}, and not a function's own state.
-
-      In the example above, this means we should remove \type{accums'} from
-      \type{s'}, but not throw away \type{s'} entirely. We should, however,
-      remove \type{s'} from the output port of the function, since the state
-      will be handled by a \small{VHDL} procedure within the function.
-
-      When looking at substates, these can appear in two places: As part of an
-      argument and as part of a return value. As noted above, these substates
-      can only be used in very specific ways.
-
-      \desc{State variables can appear as an argument.} When generating \small{VHDL}, we
-      completely ignore the argument and generate no input port for it.
-
-      \desc{State variables can be extracted from other state variables.} When
-      extracting a state variable from another state variable, this always means
-      we're extracting a substate, which we can ignore. So, we simply generate no
-      \small{VHDL} for any extraction operation that has a state variable as a result.
-
-      \desc{State variables can be passed to functions.} When passing a
-      state variable to a function, this always means we're passing a substate
-      to a subcomponent. The entire argument can simply be ingored in the
-      resulting port map.
-
-      \desc{State variables can be returned from functions.} When returning a
-      state variable from a function (probably as a part of an algebraic
-      datatype), this always mean we're returning a substate from a
-      subcomponent. The entire state variable should be ignored in the resulting
-      port map. The type binder of the binder that the function call is bound
-      to should not include the state type either.
-
-      \startdesc{State variables can be inserted into other variables.} When inserting
-      a state variable into another variable (usually by constructing that new
-      variable using its constructor), we can identify two cases: 
-
-      \startitemize
-        \item The state is inserted into another state variable. In this case,
-        the inserted state is a substate, and can be safely left out of the
-        constructed variable.
-        \item The state is inserted into a non-state variable. This happens when
-        building up the return value of a function, where you put state and
-        retsult variables together in an algebraic type (usually a tuple). In
-        this case, we should leave the state variable out as well, since we
-        don't want it to be included as an output port.
-      \stopitemize
-
-      So, in both cases, we can simply leave out the state variable from the
-      resulting value. In the latter case, however, we should generate a state
-      proc instead, which assigns the state variable to the input state variable
-      at each clock tick.
-      \stopdesc
-      
-      \desc{State variables can appear as (part of) a function result.} When
-      generating \small{VHDL}, we can completely ignore any part of a function result
-      that has a state type. If the entire result is a state type, this will
-      mean the entity will not have an output port. Otherwise, the state
-      elements will be removed from the type of the output port.
-
-
-      Now, we know how to handle each use of a state variable separately. If we
-      look at the whole, we can conclude the following:
-
-      \startitemize
-        \item A state unpack operation should not generate any \small{VHDL}. The binder
-        to which the unpacked state is bound should still be declared, this signal
-        will become the register and will hold the current state.
-        \item A state pack operation should not generate any \small{VHDL}. The binder th
-        which the packed state is bound should not be declared. The binder that is
-        packed is the signal that will hold the new state.
-        \item Any values of a State type should not be translated to \small{VHDL}. In
-        particular, State elements should be removed from tuples (and other
-        datatypes) and arguments with a state type should not generate ports.
-        \item To make the state actually work, a simple \small{VHDL} proc should be
-        generated. This proc updates the state at every clockcycle, by assigning
-        the new state to the current state. This will be recognized by synthesis
-        tools as a register specification.
-      \stopitemize
-
-
-      When applying these rules to the example program (in normal form), we will
-      get the following result. All the parts that don't generate any value are
-      crossed out, leaving some very boring assignments here and there.
+        As an example of the used approach, there is a simple averaging circuit in
+        \in{example}[ex:AvgState]. This circuit lets the accumulation of the
+        inputs be done by a subcomponent, \hs{acc}, but keeps a count of value
+        accumulated in its own state.
+        
+        
+        \startbuffer[AvgState]
+          -- The state type annotation
+          newtype State s = State s
+
+          -- The accumulator state type
+          type AccState = State Bit
+          -- The accumulator
+          acc :: Word -> AccState -> (AccState, Word)
+          acc i (State s) = let sum = s + i in (State sum, sum)
+
+          -- The averaging circuit state type
+          type AvgState = (AccState, Word)
+          -- The averaging circuit
+          avg :: Word -> AvgState -> (AvgState, Word)
+          avg i (State s) = (State s', o)
+            where
+              (accs, count) = s
+              -- Pass our input through the accumulator, which outputs a sum
+              (accs', sum) = acc i accs
+              -- Increment the count (which will be our new state)
+              count' = count + 1
+              -- Compute the average
+              o = sum / count'
+              s' = (accs', count')
+        \stopbuffer
+
+        \placeexample[here][ex:AvgState]{Simple stateful averaging circuit.}
+          %\startcombination[2*1]
+            {\typebufferhs{AvgState}}%{Haskell description using function applications.}
+          %  {\boxedgraphic{AvgState}}{The architecture described by the Haskell description.}
+          %\stopcombination
+        \todo{Picture}
+
+        And the normalized, core-like versions:
+
+        \startbuffer[AvgStateNormal]
+          acc = λi.λspacked.
+            let
+              -- Remove the State newtype
+              s = spacked ▶ Word
+              s' = s + i
+              o = s + i
+              -- Add the State newtype again
+              spacked' = s' ▶ State Word
+              res = (spacked', o)
+            in
+              res
+
+          avg = λi.λspacked.
+            let
+              s = spacked ▶ (AccState, Word)
+              accs = case s of (accs, _) -> accs
+              count = case s of (_, count) -> count
+              accres = acc i accs
+              accs' = case accres of (accs', _) -> accs'
+              sum = case accres of (_, sum) -> sum
+              count' = count + 1
+              o = sum / count'
+              s' = (accs', count')
+              spacked' = s' ▶ State (AccState, Word)
+              res = (spacked', o)
+            in
+              res
+        \stopbuffer
+
+        \placeexample[here][ex:AvgStateNormal]{Normalized version of \in{example}[ex:AvgState]}
+            {\typebufferlam{AvgStateNormal}}
       
-    
-  \starthaskell
-    avg i --spacked-- = res
-      where
-        s = --case spacked of (State s) -> s--
-        --accums = case s of (accums, \_) -> accums--
-        count = case s of (--\_,-- count) -> count
-        accumres = accum i --accums--
-        --accums' = case accumres of (accums', \_) -> accums'--
-        sum = case accumres of (--\_,-- sum) -> sum
-        count' = count + 1
-        o = sum / count'
-        s' = (--accums',-- count')
-        --spacked' = State s'--
-        res = (--spacked',-- o)
-  \stophaskell
+      \subsection{What can you do with state?}
+        Now that we've seen how state variables are typically used, the
+        question rises of what can be done with these state variables exactly?
+        What limitations are there on their use to guarantee that proper \VHDL
+        can be generated?
+
+        We will try to formulate a number of rules about what operations are
+        allowed with state variables. These rules apply to the normalized Core
+        representation, but will in practice apply to the original Haskell
+        hardware description as well. Ideally, these rules would become part
+        of the intended normal form definition \refdef{intended normal form
+        definition}, but this is not the case right now. This can cause some
+        problems, which are detailed in
+        \in{section}[sec:normalization:stateproblems].
+
+        In these rules we use the terms state variable to refer to any
+        variable that has a \lam{State} type. A state-containing variable is
+        any variable whose type contains a \lam{State} type, but is not one
+        itself (like \lam{(AccState, Word)} in the example, which is a tuple
+        type, but contains \lam{AccState}, which is again equal to \lam{State
+        Word}).
+
+        We also use a distinction between input and output (state) variables,
+        which will be defined in the rules themselves.
+
+        \startdesc{State variables can appear as an argument.}
+          \startlam
+            λspacked. ...
+          \stoplam
+
+          Any lambda that binds a variable with a state type, creates a new
+          input state variable.
+        \stopdesc
+
+        \startdesc{Input state variables can be unpacked.}
+          \startlam
+            s = spacked ▶ (AccState, Word)
+          \stoplam
+
+          An input state variable may be unpacked using a cast operation. This
+          removes the \lam{State} type renaming and the result has no longer a
+          \lam{State} type.
+
+          If the result of this unpacking does not have a state type and does
+          not contain state variables, there are no limitations on its use.
+          Otherwise if it does not have a state type but does contain
+          substates, we refer to it as a \emph{state-containing input
+          variable} and the limitations below apply. If it has a state type
+          itself, we refer to it as an \emph{input substate variable} and the
+          below limitations apply as well.
+
+          It may seem strange to consider a variable that still has a state
+          type directly after unpacking, but consider the case where a
+          function does not have any state of its own, but does call a single
+          stateful function. This means it must have a state argument that
+          contains just a substate. The function signature of such a function
+          could look like:
+
+          \starthaskell
+            type FooState = State AccState
+          \stophaskell
+
+          Which is of course equivalent to \lam{State (State Word)}.
+        \stopdesc
+  
+        \startdesc{Variables can be extracted from state-containing input variables.}
+          \startlam
+            accs = case s of (accs, _) -> accs
+          \stoplam
+
+          A state-containing input variable is typically a tuple containing
+          multiple elements (like the current function's state, substates or
+          more tuples containing substates). All of these can be extracted
+          from an input variable using an extractor case (or possibly
+          multiple, when the input variable is nested).
+
+          If the result has no state type and does not contain any state
+          variables either, there are no further limitations on its use. If
+          the result has no state type but does contain state variables we
+          refer to it as a \emph{state-containing input variable} and this
+          limitation keeps applying. If the variable has a state type itself,
+          we refer to it as an \emph{input substate variable} and below
+          limitations apply.
+
+        \startdesc{Input substate variables can be passed to functions.} 
+          \startlam
+            accres = acc i accs
+            accs' = case accres of (accs', _) -> accs'
+          \stoplam
           
-      When we would really leave out the crossed out parts, we get a slightly
-      weird program: There is a variable \type{s} which has no value, and there
-      is a variable \type{s'} that is never used. Together, these two will form
-      the state proc of the function. \type{s} contains the "current" state,
-      \type{s'} is assigned the "next" state. So, at the end of each clock
-      cycle, \type{s'} should be assigned to \type{s}.
-
-      Note that the definition of \type{s'} is not removed, even though one
-      might think it as having a state type. Since the state type has a single
-      argument constructor \type{State}, some type that should be the resulting
-      state should always be explicitly packed with the State constructor,
-      allowing us to remove the packed version, but still generate \small{VHDL} for the
-      unpacked version (of course with any substates removed).
+          An input substate variable can (only) be passed to a function.
+          Additionally, every input substate variable must be used in exactly
+          \emph{one} application, no more and no less.
+
+          The function result should contain exactly one state variable, which
+          can be extracted using (multiple) case statements. The extracted
+          state variable is referred to the \emph{output substate}
+
+          The type of this output substate must be identical to the type of
+          the input substate passed to the function.
+        \stopdesc
+
+        \startdesc{Variables can be inserted into state-containing output variables.}
+          \startlam
+            s' = (accs', count')
+          \stoplam
+          
+          A function's output state is usually a tuple containing its own
+          updated state variables and all output substates. This result is
+          built up using any single-constructor algebraic datatype.
+
+          The result of these expressions is referred to as a
+          \emph{state-containing output variable}, which are subject to these
+          limitations.
+        \stopdesc
+
+        \startdesc{State containing output variables can be packed}
+          As soon as all a functions own update state and output substate
+          variables have been joined together, the va...
+          todo{}
+              spacked' = s' ▶ State (AccState, Word)
+
+        \desc{State variables can appear as (part of) a function result.} When
+        generating \small{VHDL}, we can completely ignore any part of a
+        function result that has a state type. If the entire result is a state
+        type, this will mean the entity will not have an output port.
+        Otherwise, the state elements will be removed from the type of the
+        output port.
+
+      \subsection{Translating to \VHDL}
+        \in{Example}[ex:AvgStateNormal] shows the normalized Core version of the
+        same description (note that _ is a wild binder). \refdef{wild binder}
+        The normal form is used to translated to \VHDL.
+
+        As noted above, the basic approach when generating \VHDL for stateful
+        functions is to generate a single register for every stateful function.
+        We look around the normal form to find the let binding that removes the
+        \lam{State} newtype (using a cast). We also find the let binding that
+        adds a \lam{State} type. These are connected to the output and the input
+        of the generated let binding respectively. This means that there can
+        only be one let binding that adds and one that removes the \lam{State}
+        type. It is easy to violate this constraint. This problem is detailed in
+        \in{section}[sec:normalization:stateproblems].
+
+        This approach seems simple enough, but will this also work for more
+        complex stateful functions involving substates?  Observe that any
+        component of a function's state that is a substate, \ie passed on as
+        the state of another function, should have no influence on the
+        hardware generated for the calling function. Any state-specific
+        \small{VHDL} for this component can be generated entirely within the
+        called function.  So, we can completely ignore substates when
+        generating \VHDL for a function.
+        
+        From this observation, we might think to remove the substates from a
+        function's states alltogether, and leave only the state components
+        which are actual states of the current function. While doing this
+        would not remove any information needed to generate \small{VHDL} from
+        the function, it would cause the function definition to become invalid
+        (since we won't have any substate to pass to the functions anymore).
+        We could solve the syntactic problems by passing \type{undefined} for
+        state variables, but that would still break the code on the semantic
+        level (\ie, the function would no longer be semantically equivalent to
+        the original input).
+
+        To keep the function definition correct until the very end of the
+        process, we will not deal with (sub)states until we get to the
+        \small{VHDL} generation.  Then, we are translating from Core to
+        \small{VHDL}, and we can simply ignore substates, effectively removing
+        the substate components alltogether.
+
+        There are a few important points when ignoring substates.
+
+        First, we have to have some definition of "substate". Since any state
+        argument or return value that represents state must be of the
+        \type{State} type, we can look at the type of a value. However, we
+        must be careful to ignore only \emph{substates}, and not a function's
+        own state.
+
+        In \in{example}[ex:AvgStateNorm] above, we should generate a register
+        connected with its output connected to \lam{s} and its input connected
+        to \lam{s'}. However, \lam{s'} is build up from both \lam{accs'} and
+        \lam{count'}, while only \lam{count'} should end up in the register.
+        \lam{accs'} is a substate for the \lam{acc} function, for which a
+        register will be created when generating \VHDL for the \lam{acc}
+        function.
+
+        Fortunately, the \lam{accs'} variable (and any other substate) has a
+        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
+        that do not have a \lam{State} type themselves, like \lam{count'},
+        which is exactly a function's own state. This approach also means that
+        the state part of the result is automatically excluded when generating
+        the output port, which is also required.
+
+
+
+
+
+
+
+
+
+
+        Now, we know how to handle each use of a state variable separately. If we
+        look at the whole, we can conclude the following:
+
+        \startitemize
+          \item A state unpack operation should not generate any \small{VHDL}.
+          The binder to which the unpacked state is bound should still be
+          declared, this signal will become the register and will hold the
+          current state.
+          \item A state pack operation should not generate any \small{VHDL}.
+          The binder to which the packed state is bound should not be
+          declared. The binder that is packed is the signal that will hold the
+          new state.
+          \item Any values of a State type should not be translated to
+          \small{VHDL}. In particular, State elements should be removed from
+          tuples (and other datatypes) and arguments with a state type should
+          not generate ports.
+          \item To make the state actually work, a simple \small{VHDL} proc
+          should be generated. This proc updates the state at every
+          clockcycle, by assigning the new state to the current state. This
+          will be recognized by synthesis tools as a register specification.
+        \stopitemize
+
+        When applying these rules to the example program (in normal form), we will
+        get the following result. All the parts that don't generate any value are
+        crossed out, leaving some very boring assignments here and there.
+        
       
-      As you can see, the definition of \type{s'} is still present, since it
-      does not have a state type (The State constructor. The \type{accums'} substate has been removed,
-      leaving us just with the state of \type{avg} itself.
+        \starthaskell
+          avg i --spacked-- = res
+            where
+              s = --case spacked of (State s) -> s--
+              --accums = case s of (accums, \_) -> accums--
+              count = case s of (--\_,-- count) -> count
+              accumres = accum i --accums--
+              --accums' = case accumres of (accums', \_) -> accums'--
+              sum = case accumres of (--\_,-- sum) -> sum
+              count' = count + 1
+              o = sum / count'
+              s' = (--accums',-- count')
+              --spacked' = State s'--
+              res = (--spacked',-- o)
+        \stophaskell
+                
+        When we would really leave out the crossed out parts, we get a slightly
+        weird program: There is a variable \type{s} which has no value, and there
+        is a variable \type{s'} that is never used. Together, these two will form
+        the state proc of the function. \type{s} contains the "current" state,
+        \type{s'} is assigned the "next" state. So, at the end of each clock
+        cycle, \type{s'} should be assigned to \type{s}.
+
+        Note that the definition of \type{s'} is not removed, even though one
+        might think it as having a state type. Since the state type has a single
+        argument constructor \type{State}, some type that should be the resulting
+        state should always be explicitly packed with the State constructor,
+        allowing us to remove the packed version, but still generate \small{VHDL} for the
+        unpacked version (of course with any substates removed).
+        
+        As you can see, the definition of \type{s'} is still present, since it
+        does not have a state type (The State constructor. The \type{accums'} substate has been removed,
+        leaving us just with the state of \type{avg} itself.
     \subsection{Initial state}
       How to specify the initial state? Cannot be done inside a hardware
       function, since the initial state is its own state argument for the first