+ \startdesc{The forall type}
+ \startlambda
+ id :: \forall a. a -> a
+ \stoplambda
+ The forall type introduces polymorphism. It is the only way to
+ introduce new type variables, which are completely unconstrained (Any
+ possible type can be assigned to it). Constraints can be added later
+ using predicate types, see below.
+
+ A forall type is always (and only) introduced by a type lambda
+ expression. For example, the Core translation of the
+ id function is:
+ \startlambda
+ id = λa.λx.x
+ \stoplambda
+
+ Here, the type of the binder \lam{x} is \lam{a}, referring to the
+ binder in the topmost lambda.
+
+ When using a value with a forall type, the actual type
+ used must be applied first. For example haskell expression \hs{id
+ True} (the function \hs{id} appleid to the dataconstructor \hs{True})
+ translates to the following Core:
+
+ \startlambda
+ id @Bool True
+ \stoplambda
+
+ Here, id is first applied to the type to work with. Note that the type
+ then changes from \lam{id :: \forall a. a -> a} to \lam{id @Bool ::
+ Bool -> Bool}. Note that the type variable \lam{a} has been
+ substituted with the actual type.
+
+ In Haskell, forall types are usually not explicitly specified (The use
+ of a lowercase type variable implicitly introduces a forall type for
+ that variable). In fact, in standard Haskell there is no way to
+ explicitly specify forall types. Through a language extension, the
+ \hs{forall} keyword is available, but still optional for normal forall
+ types (it is needed for \emph{existentially quantified types}, which
+ Cλash does not support).
+ \stopdesc
+
+ \startdesc{Predicate type}
+ \startlambda
+ show :: \forall a. Show s ⇒ s → String
+ \stoplambda
+
+ \todo{Sidenote: type classes?}
+
+ A predicate type introduces a constraint on a type variable introduced
+ by a forall type (or type lambda). In the example above, the type
+ variable \lam{a} can only contain types that are an \emph{instance} of
+ the \emph{type class} \lam{Show}. \refdef{type class}
+
+ There are other sorts of predicate types, used for the type families
+ extension, which we will not discuss here.
+
+ A predicate type is introduced by a lambda abstraction. Unlike with
+ the forall type, this is a value lambda abstraction, that must be
+ applied to a value. We call this value a \emph{dictionary}.
+
+ Without going into the implementation details, a dictionary can be
+ seen as a lookup table all the methods for a given (single) type class
+ instance. This means that all the dictionaries for the same type class
+ look the same (\eg contain methods with the same names). However,
+ dictionaries for different instances of the same class contain
+ different methods, of course.
+
+ A dictionary is introduced by \small{GHC} whenever it encounters an
+ 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
+ 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
+ \stoplambda
+ \stopdesc
+
+ Using this set of types, all types in basic Haskell can be represented.
+
+ \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}.
+
+ % Use \type instead of \hs here, since the latter breaks inside
+ % section headings.
+ \subsection{Type renaming (\type{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)