- \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.
+ \todo{Overview of polymorphism with more examples (or move examples
+ here)}.
+
+ \section[sec:prototype:statetype]{State annotations in Haskell}
+ 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
+
+ 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, 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}}