+ \subsection[sec:normalization:nonrep]{Removing unrepresentable values}
+ The transformations in this section are aimed at making all the
+ values used in our expression representable. There are two main
+ transformations that are applied to \emph{all} unrepresentable let
+ bindings and function arguments. These are meant to address three
+ different kinds of unrepresentable values: Polymorphic values, higher
+ order values and literals. The transformation are described generically:
+ They apply to all non-representable values. However, non-representable
+ values that don't fall into one of these three categories will be moved
+ around by these transformations but are unlikely to completely
+ disappear. They usually mean the program was not valid in the first
+ place, because unsupported types were used (for example, a program using
+ strings).
+
+ Each of these three categories will be detailed below, followed by the
+ actual transformations.
+
+ \subsubsection{Removing Polymorphism}
+ As noted in \in{section}[sec:prototype:polymporphism],
+ polymorphism is made explicit in Core through type and
+ dictionary arguments. To remove the polymorphism from a
+ function, we can simply specialize the polymorphic function for
+ the particular type applied to it. The same goes for dictionary
+ arguments. To remove polymorphism from let bound values, we
+ simply inline the let bindings that have a polymorphic type,
+ which should (eventually) make sure that the polymorphic
+ expression is applied to a type and/or dictionary, which can
+ then be removed by β-reduction (\in{section}[sec:normalization:beta]).
+
+ Since both type and dictionary arguments are not representable,
+ \refdef{representable}
+ the non-representable argument specialization and
+ non-representable let binding inlining transformations below
+ take care of exactly this.
+
+ There is one case where polymorphism cannot be completely
+ removed: Builtin functions are still allowed to be polymorphic
+ (Since we have no function body that we could properly
+ specialize). However, the code that generates \VHDL for builtin
+ functions knows how to handle this, so this is not a problem.
+
+ \subsubsection{Defunctionalization}
+ These transformations remove higher order expressions from our
+ program, making all values first-order.
+
+ Higher order values are always introduced by lambda abstractions, none
+ of the other Core expression elements can introduce a function type.
+ However, other expressions can \emph{have} a function type, when they
+ have a lambda expression in their body.
+
+ For example, the following expression is a higher order expression
+ that is not a lambda expression itself:
+
+ \refdef{id function}
+ \startlambda
+ case x of
+ High -> id
+ Low -> λx.x
+ \stoplambda
+
+ The reference to the \lam{id} function shows that we can introduce a
+ higher order expression in our program without using a lambda
+ expression directly. However, inside the definition of the \lam{id}
+ function, we can be sure that a lambda expression is present.
+
+ Looking closely at the definition of our normal form in
+ \in{section}[sec:normalization:intendednormalform], we can see that
+ there are three possibilities for higher order values to appear in our
+ intended normal form:
+
+ \startitemize[KR]
+ \item[item:toplambda] Lambda abstractions can appear at the highest level of a
+ top level function. These lambda abstractions introduce the
+ arguments (input ports / current state) of the function.
+ \item[item:builtinarg] (Partial applications of) top level functions can appear as an
+ argument to a builtin function.
+ \item[item:completeapp] (Partial applications of) top level functions can appear in
+ function position of an application. Since a partial application
+ cannot appear anywhere else (except as builtin function arguments),
+ all partial applications are applied, meaning that all applications
+ will become complete applications. However, since application of
+ arguments happens one by one, in the expression:
+ \startlambda
+ f 1 2
+ \stoplambda
+ the subexpression \lam{f 1} has a function type. But this is
+ allowed, since it is inside a complete application.
+ \stopitemize
+
+ We will take a typical function with some higher order values as an
+ example. The following function takes two arguments: a \lam{Bit} and a
+ list of numbers. Depending on the first argument, each number in the
+ list is doubled, or the list is returned unmodified. For the sake of
+ the example, no polymorphism is shown. In reality, at least map would
+ be polymorphic.
+
+ \startlambda
+ λy.let double = λx. x + x in
+ case y of
+ Low -> map double
+ High -> λz. z
+ \stoplambda
+
+ This example shows a number of higher order values that we cannot
+ translate to \VHDL directly. The \lam{double} binder bound in the let
+ expression has a function type, as well as both of the alternatives of
+ the case expression. The first alternative is a partial application of
+ the \lam{map} builtin function, whereas the second alternative is a
+ lambda abstraction.
+
+ To reduce all higher order values to one of the above items, a number
+ of transformations we've already seen are used. The η-abstraction
+ transformation from \in{section}[sec:normalization:eta] ensures all
+ function arguments are introduced by lambda abstraction on the highest
+ level of a function. These lambda arguments are allowed because of
+ \in{item}[item:toplambda] above. After η-abstraction, our example
+ becomes a bit bigger:
+
+ \startlambda
+ λy.λq.(let double = λx. x + x in
+ case y of
+ Low -> map double
+ High -> λz. z
+ ) q
+ \stoplambda
+
+ η-abstraction also introduces extra applications (the application of
+ the let expression to \lam{q} in the above example). These
+ applications can then propagated down by the application propagation
+ transformation (\in{section}[sec:normalization:appprop]). In our
+ example, the \lam{q} and \lam{r} variable will be propagated into the
+ let expression and then into the case expression:
+
+ \startlambda
+ λy.λq.let double = λx. x + x in
+ case y of
+ Low -> map double q
+ High -> (λz. z) q
+ \stoplambda
+
+ This propagation makes higher order values become applied (in
+ particular both of the alternatives of the case now have a
+ representable type). Completely applied top level functions (like the
+ first alternative) are now no longer invalid (they fall under
+ \in{item}[item:completeapp] above). (Completely) applied lambda
+ abstractions can be removed by β-abstraction. For our example,
+ applying β-abstraction results in the following:
+
+ \startlambda
+ λy.λq.let double = λx. x + x in
+ case y of
+ Low -> map double q
+ High -> q
+ \stoplambda
+
+ As you can see in our example, all of this moves applications towards
+ the higher order values, but misses higher order functions bound by
+ let expressions. The applications cannot be moved towards these values
+ (since they can be used in multiple places), so the values will have
+ to be moved towards the applications. This is achieved by inlining all
+ higher order values bound by let applications, by the
+ non-representable binding inlining transformation below. When applying
+ it to our example, we get the following:
+
+ \startlambda
+ λy.λq.case y of
+ Low -> map (λx. x + x) q
+ High -> q
+ \stoplambda
+
+ We've nearly eliminated all unsupported higher order values from this
+ expressions. The one that's remaining is the first argument to the
+ \lam{map} function. Having higher order arguments to a builtin
+ function like \lam{map} is allowed in the intended normal form, but
+ only if the argument is a (partial application) of a top level
+ function. This is easily done by introducing a new top level function
+ and put the lambda abstraction inside. This is done by the function
+ extraction transformation from
+ \in{section}[sec:normalization:funextract].
+
+ \startlambda
+ λy.λq.case y of
+ Low -> map func q
+ High -> q
+ \stoplambda
+
+ This also introduces a new function, that we have called \lam{func}:
+
+ \startlambda
+ func = λx. x + x
+ \stoplambda
+
+ Note that this does not actually remove the lambda, but now it is a
+ lambda at the highest level of a function, which is allowed in the
+ intended normal form.
+
+ There is one case that has not been discussed yet. What if the
+ \lam{map} function in the example above was not a builtin function
+ but a user-defined function? Then extracting the lambda expression
+ into a new function would not be enough, since user-defined functions
+ can never have higher order arguments. For example, the following
+ expression shows an example:
+
+ \startlambda
+ twice :: (Word -> Word) -> Word -> Word
+ twice = λf.λa.f (f a)
+
+ main = λa.app (λx. x + x) a
+ \stoplambda
+
+ This example shows a function \lam{twice} that takes a function as a
+ first argument and applies that function twice to the second argument.
+ Again, we've made the function monomorphic for clarity, even though
+ this function would be a lot more useful if it was polymorphic. The
+ function \lam{main} uses \lam{twice} to apply a lambda epression twice.
+
+ When faced with a user defined function, a body is available for that
+ function. This means we could create a specialized version of the
+ function that only works for this particular higher order argument
+ (\ie, we can just remove the argument and call the specialized
+ function without the argument). This transformation is detailed below.
+ Applying this transformation to the example gives:
+
+ \startlambda
+ twice' :: Word -> Word
+ twice' = λb.(λf.λa.f (f a)) (λx. x + x) b
+
+ main = λa.app' a
+ \stoplambda