-\chapter{Prototype}
- Choice of Haskell
- Core - description of the language (appendix?)
- Stages (-> Core, Normalization, -> VHDL)
- Implementation issues
-
- Haskell language coverage / constraints
- Recursion
- Builtin types
- Custom types (Sum types, product types)
- Function types / higher order expressions
+\chapter[chap:prototype]{Prototype}
+ An important step in this research is the creation of a prototype compiler.
+ Having this prototype allows us to apply the ideas from the previous chapter
+ to actual hardware descriptions and evaluate their usefulness. Having a
+ prototype also helps to find new techniques and test possible
+ interpretations.
+ Obviously the prototype was not created after all research
+ ideas were formed, but its implementation has been interleaved with the
+ research itself. Also, the prototype described here is the final version, it
+ has gone through a number of design iterations which we will not completely
+ describe here.
+
+ \section[sec:prototype:input]{Input language}
+ When implementing this prototype, the first question to ask is: What
+ (functional) language will we use to describe our hardware? (Note that
+ this does not concern the \emph{implementation language} of the compiler,
+ just the language \emph{translated by} the compiler).
+
+ Initially, we have two choices:
+
+ \startitemize
+ \item Create a new functional language from scratch. This has the
+ advantage of having a language that contains exactly those elements that
+ are convenient for describing hardware and can contain special
+ constructs that allows our hardware descriptions to be more powerful or
+ concise.
+ \item Use an existing language and create a new backend for it. This has
+ the advantage that existing tools can be reused, which will speed up
+ development.
+ \stopitemize
+
+ \todo{Sidenote: No EDSL}
+
+ Considering that we required a prototype which should be working quickly,
+ and that implementing parsers, semantic checkers and especially
+ typcheckers is not exactly the core of this research (but it is lots and
+ lots of work!), using an existing language is the obvious choice. This
+ also has the advantage that a large set of language features is available
+ to experiment with and it is easy to find which features apply well and
+ which don't. A possible second prototype could use a custom language with
+ just the useful features (and possibly extra features that are specific to
+ the domain of hardware description as well).
+
+ The second choice is which of the many existing languages to use. As
+ mentioned before, the chosen language is Haskell. This choice has not been the
+ result of a thorough comparison of languages, for the simple reason that
+ the requirements on the language were completely unclear at the start of
+ this research. The fact that Haskell is a language with a broad spectrum
+ of features, that it is commonly used in research projects and that the
+ 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
+ output our hardware in some format that can be later processed and
+ programmed by other tools.
+
+ Looking at other tools in the industry, the Electronic Design Interchange
+ Format (\small{EDIF}) is commonly used for storing intermediate
+ \emph{netlists} (lists of components and connections between these
+ components) and is commonly the target for \small{VHDL} and Verilog
+ compilers.
+
+ However, \small{EDIF} is not completely tool-independent. It specifies a
+ meta-format, but the hardware components that can be used vary between
+ various tool and hardware vendors, as well as the interpretation of the
+ \small{EDIF} standard. \todo{Is this still true? Reference:
+ http://delivery.acm.org/10.1145/80000/74534/p803-li.pdf?key1=74534\&key2=8370537521\&coll=GUIDE\&dl=GUIDE\&CFID=61207158\&CFTOKEN=61908473}
+
+ This means that when working with \small{EDIF}, our prototype would become
+ technology dependent (\eg only work with \small{FPGA}s of a specific
+ vendor, or even only with specific chips). This limits the applicability
+ of our prototype. Also, the tools we'd like to use for verifying,
+ simulating and draw pretty pictures of our output (like Precision, or
+ QuestaSim) are designed for \small{VHDL} or Verilog input.
+
+ For these reasons, we will not use \small{EDIF}, but \small{VHDL} as our
+ output language. We choose \VHDL over Verilog simply because we are
+ familiar with \small{VHDL} already. The differences between \small{VHDL}
+ and Verilog are on the higher level, while we will be using \small{VHDL}
+ mainly to write low level, netlist-like descriptions anyway.
+
+ An added advantage of using VHDL is that we can profit from existing
+ optimizations in VHDL synthesizers. A lot of optimizations are done on the
+ VHDL level by existing tools. These tools have years of experience in this
+ field, so it would not be reasonable to assume we could achieve a similar
+ amount of optimization in our prototype (nor should it be a goal,
+ considering this is just a prototype).
+
+ Note that we will be using \small{VHDL} as our output language, but will
+ not use its full expressive power. Our output will be limited to using
+ simple, structural descriptions, without any behavioural descriptions
+ (which might not be supported by all tools). This ensures that any tool
+ that works with \VHDL will understand our output (most tools don't support
+ synthesis of more complex \VHDL). This also leaves open the option to
+ switch to \small{EDIF} in the future, with minimal changes to the
+ prototype.
+
+ \section{Prototype design}
+ As suggested above, we will use the Glasgow Haskell Compiler (\small{GHC}) to
+ implement our prototype compiler. To understand the design of the
+ compiler, we will first dive into the \small{GHC} compiler a bit. It's
+ compilation consists of the following steps (slightly simplified):
+
+ \startuseMPgraphic{ghc-pipeline}
+ % Create objects
+ save inp, front, desugar, simpl, back, out;
+ newEmptyBox.inp(0,0);
+ newBox.front(btex Fronted etex);
+ newBox.desugar(btex Desugarer etex);
+ newBox.simpl(btex Simplifier etex);
+ newBox.back(btex Backend etex);
+ newEmptyBox.out(0,0);
+
+ % Space the boxes evenly
+ inp.c - front.c = front.c - desugar.c = desugar.c - simpl.c
+ = simpl.c - back.c = back.c - out.c = (0, 1.5cm);
+ out.c = origin;
+
+ % Draw lines between the boxes. We make these lines "deferred" and give
+ % them a name, so we can use ObjLabel to draw a label beside them.
+ ncline.inp(inp)(front) "name(haskell)";
+ ncline.front(front)(desugar) "name(ast)";
+ ncline.desugar(desugar)(simpl) "name(core)";
+ ncline.simpl(simpl)(back) "name(simplcore)";
+ ncline.back(back)(out) "name(native)";
+ ObjLabel.inp(btex Haskell source etex) "labpathname(haskell)", "labdir(rt)";
+ ObjLabel.front(btex Haskell AST etex) "labpathname(ast)", "labdir(rt)";
+ ObjLabel.desugar(btex Core etex) "labpathname(core)", "labdir(rt)";
+ ObjLabel.simpl(btex Simplified core etex) "labpathname(simplcore)", "labdir(rt)";
+ ObjLabel.back(btex Native code etex) "labpathname(native)", "labdir(rt)";
+
+ % Draw the objects (and deferred labels)
+ drawObj (inp, front, desugar, simpl, back, out);
+ \stopuseMPgraphic
+ \placefigure[right]{GHC compiler pipeline}{\useMPgraphic{ghc-pipeline}}
+
+ \startdesc{Frontend}
+ This step takes the Haskell source files and parses them into an
+ abstract syntax tree (\small{AST}). This \small{AST} can express the
+ complete Haskell language and is thus a very complex one (in contrast
+ with the Core \small{AST}, later on). All identifiers in this
+ \small{AST} are resolved by the renamer and all types are checked by the
+ typechecker.
+ \stopdesc
+ \startdesc{Desugaring}
+ This steps takes the full \small{AST} and translates it to the
+ \emph{Core} language. Core is a very small functional language with lazy
+ semantics, that can still express everything Haskell can express. Its
+ simpleness makes Core very suitable for further simplification and
+ translation. Core is the language we will be working with as well.
+ \stopdesc
+ \startdesc{Simplification}
+ Through a number of simplification steps (such as inlining, common
+ subexpression elimination, etc.) the Core program is simplified to make
+ it faster or easier to process further.
+ \stopdesc
+ \startdesc{Backend}
+ This step takes the simplified Core program and generates an actual
+ runnable program for it. This is a big and complicated step we will not
+ discuss it any further, since it is not required for our prototype.
+ \stopdesc
+
+ In this process, there a number of places where we can start our work.
+ Assuming that we don't want to deal with (or modify) parsing, typechecking
+ and other frontend business and that native code isn't really a useful
+ format anymore, we are left with the choice between the full Haskell
+ \small{AST}, or the smaller (simplified) core representation.
+
+ The advantage of taking the full \small{AST} is that the exact structure
+ of the source program is preserved. We can see exactly what the hardware
+ descriiption looks like and which syntax constructs were used. However,
+ the full \small{AST} is a very complicated datastructure. If we are to
+ handle everything it offers, we will quickly get a big compiler.
+
+ Using the core representation gives us a much more compact datastructure
+ (a core expression only uses 9 constructors). Note that this does not mean
+ that the core representation itself is smaller, on the contrary. Since the
+ core language has less constructs, a lot of things will take a larger
+ expression to express.
+
+ However, the fact that the core language is so much smaller, means it is a
+ lot easier to analyze and translate it into something else. For the same
+ reason, \small{GHC} runs its simplifications and optimizations on the core
+ representation as well.
+
+ However, we will use the normal core representation, not the simplified
+ core. Reasons for this are detailed below. \todo{Ref}
+
+ The final prototype roughly consists of three steps:
+
+ \startuseMPgraphic{clash-pipeline}
+ % Create objects
+ save inp, front, norm, vhdl, out;
+ newEmptyBox.inp(0,0);
+ newBox.front(btex \small{GHC} frontend + desugarer etex);
+ newBox.norm(btex Normalization etex);
+ newBox.vhdl(btex \small{VHDL} generation etex);
+ newEmptyBox.out(0,0);
+
+ % Space the boxes evenly
+ inp.c - front.c = front.c - norm.c = norm.c - vhdl.c
+ = vhdl.c - out.c = (0, 1.5cm);
+ out.c = origin;
+
+ % Draw lines between the boxes. We make these lines "deferred" and give
+ % them a name, so we can use ObjLabel to draw a label beside them.
+ ncline.inp(inp)(front) "name(haskell)";
+ ncline.front(front)(norm) "name(core)";
+ ncline.norm(norm)(vhdl) "name(normal)";
+ ncline.vhdl(vhdl)(out) "name(vhdl)";
+ ObjLabel.inp(btex Haskell source etex) "labpathname(haskell)", "labdir(rt)";
+ ObjLabel.front(btex Core etex) "labpathname(core)", "labdir(rt)";
+ ObjLabel.norm(btex Normalized core etex) "labpathname(normal)", "labdir(rt)";
+ ObjLabel.vhdl(btex \small{VHDL} description etex) "labpathname(vhdl)", "labdir(rt)";
+
+ % Draw the objects (and deferred labels)
+ drawObj (inp, front, norm, vhdl, out);
+ \stopuseMPgraphic
+ \placefigure[right]{Cλash compiler pipeline}{\useMPgraphic{clash-pipeline}}
+
+ \startdesc{Frontend}
+ This is exactly the frontend and desugarer from the \small{GHC}
+ pipeline, that translates Haskell sources to a core representation.
+ \stopdesc
+ \startdesc{Normalization}
+ This is a step that transforms the core representation into a normal
+ form. This normal form is still expressed in the core language, but has
+ to adhere to an extra set of constraints. This normal form is less
+ expressive than the full core language (e.g., it can have limited higher
+ order expressions, has a specific structure, etc.), but is also very
+ close to directly describing hardware.
+ \stopdesc
+ \startdesc{\small{VHDL} generation}
+ The last step takes the normal formed core representation and generates
+ \small{VHDL} for it. Since the normal form has a specific, hardware-like
+ structure, this final step is very straightforward.
+ \stopdesc
+
+ The most interesting step in this process is the normalization step. That
+ is where more complicated functional constructs, which have no direct
+ hardware interpretation, are removed and translated into hardware
+ constructs. This step is described in a lot of detail at
+ \in{chapter}[chap:normalization].
+
+ \section{The Core language}
+ \defreftxt{core}{the Core language}
+ Most of the prototype deals with handling the program in the Core
+ language. In this section we will show what this language looks like and
+ how it works.
+
+ The Core language is a functional language that describes
+ \emph{expressions}. Every identifier used in Core is called a
+ \emph{binder}, since it is bound to a value somewhere. On the highest
+ level, a Core program is a collection of functions, each of which bind a
+ binder (the function name) to an expression (the function value, which has
+ a function type).
+
+ The Core language itself does not prescribe any program structure, only
+ expression structure. In the \small{GHC} compiler, the Haskell module
+ structure is used for the resulting Core code as well. Since this is not
+ so relevant for understanding the Core language or the Normalization
+ process, we'll only look at the Core expression language here.
+
+ Each Core expression consists of one of these possible expressions.
+
+ \startdesc{Variable reference}
+ \defref{variable reference}
+ \startlambda
+ x :: T
+ \stoplambda
+ This is a reference to a binder. It's written down as the
+ name of the binder that is being referred to along with its type. The
+ binder name should of course be bound in a containing scope (including
+ top level scope, so a reference to a top level function is also a
+ variable reference). Additionally, constructors from algebraic datatypes
+ also become variable references.
+
+ The value of this expression is the value bound to the given binder.
+
+ Each binder also carries around its type (explicitly shown above), but
+ this is usually not shown in the Core expressions. Only when the type is
+ relevant (when a new binder is introduced, for example) will it be
+ shown. In other cases, the binder is either not relevant, or easily
+ derived from the context of the expression. \todo{Ref sidenote on type
+ annotations}
+ \stopdesc
+
+ \startdesc{Literal}
+ \defref{literal}
+ \startlambda
+ 10
+ \stoplambda
+ This is a literal. Only primitive types are supported, like
+ chars, strings, ints and doubles. The types of these literals are the
+ \quote{primitive} versions, like \lam{Char\#} and \lam{Word\#}, not the
+ normal Haskell versions (but there are builtin conversion functions).
+ \stopdesc
+
+ \startdesc{Application}
+ \defref{application}
+ \startlambda
+ func arg
+ \stoplambda
+ This is function application. Each application consists of two
+ 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.
+
+ The value of an application is the value of the function part, with the
+ first argument binder bound to the argument part.
+ \stopdesc
+
+ \startdesc{Lambda abstraction}
+ \defref{lambda abstraction}
+ \startlambda
+ λbndr.body
+ \stoplambda
+ This is the basic lambda abstraction, as it occurs in labmda calculus.
+ It consists of a binder part and a body part. A lambda abstraction
+ creates a function, that can be applied to an argument. The binder is
+ usually a value binder, but it can also be a \emph{type binder} (or
+ \emph{type variable}). The latter case introduces a new polymorphic
+ variable, which can be used in types later on. See
+ \in{section}[sec:prototype:coretypes] for details.
+
+ Note that the body of a lambda abstraction extends all the way to the
+ end of the expression, or the closing bracket surrounding the lambda. In
+ other words, the lambda abstraction \quote{operator} has the lowest
+ priority of all.
+
+ The value of an application is the value of the body part, with the
+ binder bound to the value the entire lambda abstraction is applied to.
+ \stopdesc
+
+ \startdesc{Non-recursive let expression}
+ \defref{let expression}
+ \startlambda
+ let bndr = value in body
+ \stoplambda
+ A let expression allows you to bind a binder to some value, while
+ evaluating to some other value (where that binder is in scope). This
+ allows for sharing of subexpressions (you can use a binder twice) and
+ explicit \quote{naming} of arbitrary expressions. Note that the binder
+ is not in scope in the value bound to it, so it's not possible to make
+ recursive definitions with the normal form of the let expression (see
+ the recursive form below).
+
+ Even though this let expression is an extension on the basic lambda
+ calculus, it is easily translated to a lambda abstraction. The let
+ expression above would then become:
+
+ \startlambda
+ (λbndr.body) value
+ \stoplambda
+
+ This notion might be useful for verifying certain properties on
+ transformations, since a lot of verification work has been done on
+ lambda calculus already.
+
+ The value of a let expression is the value of the body part, with the
+ binder bound to the value.
+ \stopdesc
+
+ \startdesc{Recursive let expression}
+ \startlambda
+ letrec
+ bndr1 = value1
+ \vdots
+ bndrn = valuen
+ in
+ body
+ \stoplambda
+ This is the recursive version of the let expression. In \small{GHC}'s
+ Core implementation, non-recursive and recursive lets are not so
+ distinct as we present them here, but this provides a clearer overview.
+
+ The main difference with the normal let expression is that each of the
+ binders is in scope in each of the values, in addition to the body. This
+ allows for self-recursive or mutually recursive definitions.
+
+ It should also be possible to express a recursive let using normal
+ lambda calculus, if we use the \emph{least fixed-point operator},
+ \lam{Y}. This falls beyond the scope of this report, since it is not
+ needed for this research.
+ \stopdesc
+
+ \startdesc{Case expression}
+ \defref{case expression}
+ \startlambda
+ case scrutinee of bndr
+ DEFAULT -> defaultbody
+ C0 bndr0,0 ... bndr0,m -> body0
+ \vdots
+ Cn bndrn,0 ... bndrn,m -> bodyn
+ \stoplambda
+
+ \todo{Define WHNF}
+
+ A case expression is the only way in Core to choose between values. All
+ \hs{if} expressions and pattern matchings from the original Haskell
+ PRogram have been translated to case expressions by the desugarer.
+
+ 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}. It then chooses a body depending on
+ the constructor of its scrutinee. If none of the constructors match, the
+ \lam{DEFAULT} alternative is chosen. A case expression must always be
+ exhaustive, \ie it must cover all possible constructors that the
+ scrutinee can have (if all of them are covered explicitly, the
+ \lam{DEFAULT} alternative can be left out).
+
+ Since we can only match the top level constructor, there can be no overlap
+ in the alternatives and thus order of alternatives is not relevant (though
+ the \lam{DEFAULT} alternative must appear first for implementation
+ efficiency).
+
+ Any arguments to the constructor in the scrutinee are bound to each of the
+ binders after the constructor and are in scope only in the corresponding
+ body.
+
+ To support strictness, the scrutinee is always evaluated into
+ \small{WHNF}, even when there is only a \lam{DEFAULT} alternative. This
+ allows aplication of the strict function \lam{f} to the argument \lam{a}
+ to be written like:
+
+ \startlambda
+ f (case a of arg DEFAULT -> arg)
+ \stoplambda
+
+ According to the \GHC documentation, this is the only use for the extra
+ binder to which the scrutinee is bound. When not using strictness
+ annotations (which is rather pointless in hardware descriptions),
+ \small{GHC} seems to never generate any code making use of this binder.
+ In fact, \GHC has never been observed to generate code using this
+ binder, even when strictness was involved. Nonetheless, the prototype
+ handles this binder as expected.
+
+ Note that these case statements are less powerful than the full Haskell
+ case statements. In particular, they do not support complex patterns like
+ in Haskell. Only the constructor of an expression can be matched,
+ complex patterns are implemented using multiple nested case expressions.
+
+ Case statements are also used for unpacking of algebraic datatypes, even
+ when there is only a single constructor. For examples, to add the elements
+ of a tuple, the following Core is generated:
+
+ \startlambda
+ sum = λtuple.case tuple of
+ (,) a b -> a + b
+ \stoplambda
+
+ Here, there is only a single alternative (but no \lam{DEFAULT}
+ alternative, since the single alternative is already exhaustive). When
+ it's body is evaluated, the arguments to the tuple constructor \lam{(,)}
+ (\eg, the elements of the tuple) are bound to \lam{a} and \lam{b}.
+ \stopdesc
+
+ \startdesc{Cast expression}
+ \defref{cast expression}
+ \startlambda
+ body ▶ targettype
+ \stoplambda
+ A cast expression allows you to change the type of an expression to an
+ equivalent type. Note that this is not meant to do any actual work, like
+ conversion of data from one format to another, or force a complete type
+ change. Instead, it is meant to change between different representations
+ of the same type, \eg switch between types that are provably equal (but
+ look different).
+
+ In our hardware descriptions, we typically see casts to change between a
+ Haskell newtype and its contained type, since those are effectively
+ different types (so a cast is needed) with the same representation (but
+ no work is done by the cast).
+
+ More complex are types that are proven to be equal by the typechecker,
+ but look different at first glance. To ensure that, once the typechecker
+ has proven equality, this information sticks around, explicit casts are
+ added. In our notation we only write the target type, but in reality a
+ cast expressions carries around a \emph{coercion}, which can be seen as a
+ proof of equality. \todo{Example}
+
+ The value of a cast is the value of its body, unchanged. The type of this
+ value is equal to the target type, not the type of its body.
+
+ \todo{Move and update this paragraph}
+ Note that this syntax is also used sometimes to indicate that a particular
+ expression has a particular type, even when no cast expression is
+ involved. This is then purely informational, since the only elements that
+ are explicitely typed in the Core language are the binder references and
+ cast expressions, the types of all other elements are determined at
+ runtime.
+ \stopdesc
+
+ \startdesc{Note}
+ The Core language in \small{GHC} allows adding \emph{notes}, which serve
+ as hints to the inliner or add custom (string) annotations to a core
+ expression. These shouldn't be generated normally, so these are not
+ handled in any way in the prototype.
+ \stopdesc
+
+ \startdesc{Type}
+ \defref{type expression}
+ \startlambda
+ @type
+ \stoplambda
+ It is possibly to use a Core type as a Core expression. For the actual
+ types supported by Core, see \in{section}[sec:prototype:coretypes]. This
+ \quote{lifting} of a type into the value domain is done to allow for
+ type abstractions and applications to be handled as normal lambda
+ abstractions and applications above. This means that a type expression
+ in Core can only ever occur in the argument position of an application,
+ and only if the type of the function that is applied to expects a type
+ as the first argument. This happens for all polymorphic functions, for
+ example, the \lam{fst} function:
+
+ \startlambda
+ fst :: \forall a. \forall b. (a, b) -> a
+ fst = λtup.case tup of (,) a b -> a
+
+ fstint :: (Int, Int) -> Int
+ fstint = λa.λb.fst @Int @Int a b
+ \stoplambda
+
+ The type of \lam{fst} has two universally quantified type variables. When
+ \lam{fst} is applied in \lam{fstint}, it is first applied to two types.
+ (which are substitued for \lam{a} and \lam{b} in the type of \lam{fst}, so
+ the type of \lam{fst} actual type of arguments and result can be found:
+ \lam{fst @Int @Int :: (Int, Int) -> Int}).
+ \stopdesc
+
+ \subsection[sec:prototype:coretypes]{Core type system}
+ Whereas the expression syntax of Core is very simple, its type system is
+ a bit more complicated. It turns out it is harder to \quote{desugar}
+ Haskell's complex type system into something more simple. Most of the
+ type system is thus very similar to that of Haskell.
+
+ We will slightly limit our view on Core's type system, since the more
+ complicated parts of it are only meant to support Haskell's (or rather,
+ \GHC's) type extensions, such as existential types, \small{GADT}s, type
+ families and other non-standard Haskell stuff which we don't (plan to)
+ support.
+
+ 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).
+
+ Any type in core is one of the following:
+
+ \startdesc{A type variable}
+ \startlambda
+ t
+ \stoplambda
+
+ This is a reference to a type defined elsewhere. This can either be a
+ polymorphic type (like the latter two \lam{t}'s in \lam{id :: \forall t.
+ t -> t}), or a type constructor (like \lam{Bool} in \lam{not :: Bool ->
+ Bool}). Like in Haskell, polymorphic type variables always
+ start with a lowercase letter, while type constructors always start
+ with an uppercase letter.
+
+ \todo{How to define (new) type constructors?}
+
+ A special case of a type constructor is the \emph{function type
+ constructor}, \lam{->}. This is a type constructor taking two arguments
+ (using application below). The function type constructor is commonly
+ written inline, so we write \lam{a -> b} when we really mean \lam{-> a
+ b}, the function type constructor applied to \lam{a} and \lam{b}.
+
+ Polymorphic type variables can only be defined by a lambda
+ abstraction, see the forall type below.
+ \stopdesc
+
+ \startdesc{A type application}
+ \startlambda
+ Maybe Int
+ \stoplambda
+
+ This applies a some type to another type. This is particularly used to
+ apply type variables (type constructors) to their arguments.
+
+ As mentioned above, applications of some type constructors have
+ special notation. In particular, these are applications of the
+ \emph{function type constructor} and \emph{tuple type constructors}:
+ \startlambda
+ foo :: a -> b
+ foo' :: -> a b
+ bar :: (a, b, c)
+ bar' :: (,,) a b c
+ \stoplambda
+ \stopdesc
+
+ \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.
+ \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:
+
+ \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.
+
+ \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.
+
+
+ \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
+ call (unless you add an explicit, synchronous reset port).
+
+ External init state is natural for simulation.
+
+ External init state works for hardware generation as well.
+
+ Implementation issues: state splitting, linking input to output state,
+ checking usage constraints on state variables.
+
+ \todo{Implementation issues: Separate compilation, simplified core.}
+
+% vim: set sw=2 sts=2 expandtab:
projects / matthijs / master-project / report.git / blobdiff