Partially update state annotations section in the prototype chapter.
authorMatthijs Kooijman <matthijs@stdin.nl>
Fri, 4 Dec 2009 19:05:42 +0000 (20:05 +0100)
committerMatthijs Kooijman <matthijs@stdin.nl>
Fri, 4 Dec 2009 19:06:09 +0000 (20:06 +0100)
This is an unfinished commit, to store intermediate progress.

Chapters/Normalization.tex
Chapters/Prototype.tex

index cf905c3..bf0d388 100644 (file)
         transformations will probably need updating to handle them in all
         cases.
 
         transformations will probably need updating to handle them in all
         cases.
 
-      \subsection{Normalization of stateful descriptions}
+      \subsection[sec:normalization:stateproblems]{Normalization of stateful descriptions}
         Currently, the intended normal form definition\refdef{intended
         normal form definition} offers enough freedom to describe all
         valid stateful descriptions, but is not limiting enough. It is
         Currently, the intended normal form definition\refdef{intended
         normal form definition} offers enough freedom to describe all
         valid stateful descriptions, but is not limiting enough. It is
index b9e8aa7..794aa34 100644 (file)
     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.
     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.
-      \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: 
+    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
 
 
       \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}
 
       \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
+          
+          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
           
           
-      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).
+          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
     \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