+ 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 β-expansion. For our example,
+ applying β-expansion 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 have nearly eliminated all unsupported higher-order values from this
+ expressions. The one that is remaining is the first argument to the
+ \lam{map} function. Having higher-order arguments to a built-in
+ 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 built-in 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 have 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 expression 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
+
+ The \lam{main} function is now in normal form, since the only
+ higher-order value there is the top level lambda expression. The new
+ \lam{twice'} function is a bit complex, but the entire original body
+ of the original \lam{twice} function is wrapped in a lambda
+ abstraction and applied to the argument we have specialized for
+ (\lam{λx. x + x}) and the other arguments. This complex expression can
+ fortunately be effectively reduced by repeatedly applying β-reduction:
+
+ \startlambda
+ twice' :: Word -> Word
+ twice' = λb.(b + b) + (b + b)
+ \stoplambda
+
+ This example also shows that the resulting normal form might not be as
+ efficient as we might hope it to be (it is calculating \lam{(b + b)}
+ twice). This is discussed in more detail in
+ \in{section}[sec:normalization:duplicatework].
+
+ \subsubsection[sec:normalization:literals]{Literals}
+ There are a limited number of literals available in Haskell and Core.
+ \refdef{enumerated types} When using (enumerating) algebraic
+ data-types, a literal is just a reference to the corresponding data
+ constructor, which has a representable type (the algebraic datatype)
+ and can be translated directly. This also holds for literals of the
+ \hs{Bool} Haskell type, which is just an enumerated type.
+
+ There is, however, a second type of literal that does not have a
+ representable type: integer literals. Cλash supports using integer
+ literals for all three integer types supported (\hs{SizedWord},
+ \hs{SizedInt} and \hs{RangedWord}). This is implemented using
+ Haskell's \hs{Num} type class, which offers a \hs{fromInteger} method
+ that converts any \hs{Integer} to the Cλash data-types.
+
+ When \GHC\ sees integer literals, it will automatically insert calls to
+ the \hs{fromInteger} method in the resulting Core expression. For
+ example, the following expression in Haskell creates a 32 bit unsigned
+ word with the value 1. The explicit type signature is needed, since
+ there is no context for \GHC\ to determine the type from otherwise.
+
+ \starthaskell
+ 1 :: SizedWord D32
+ \stophaskell
+
+ This Haskell code results in the following Core expression:
+
+ \startlambda
+ fromInteger @(SizedWord D32) \$dNum (smallInteger 10)
+ \stoplambda
+
+ The literal 10 will have the type \lam{GHC.Prim.Int\#}, which is
+ converted into an \lam{Integer} by \lam{smallInteger}. Finally, the
+ \lam{fromInteger} function will finally convert this into a
+ \lam{SizedWord D32}.
+
+ Both the \lam{GHC.Prim.Int\#} and \lam{Integer} types are not
+ representable, and cannot be translated directly. Fortunately, there
+ is no need to translate them, since \lam{fromInteger} is a built-in
+ function that knows how to handle these values. However, this does
+ require that the \lam{fromInteger} function is directly applied to
+ these non-representable literal values, otherwise errors will occur.
+ For example, the following expression is not in the intended normal
+ form, since one of the let bindings has an unrepresentable type
+ (\lam{Integer}):
+
+ \startlambda
+ let l = smallInteger 10 in fromInteger @(SizedWord D32) \$dNum l
+ \stoplambda
+
+ By inlining these let-bindings, we can ensure that unrepresentable
+ literals bound by a let binding end up in an application of the
+ appropriate built-in function, where they are allowed. Since it is
+ possible that the application of that function is in a different
+ function than the definition of the literal value, we will always need
+ to specialize away any unrepresentable literals that are used as
+ function arguments. The following two transformations do exactly this.
+
+ \subsubsection[sec:normalization:nonrepinline]{Non-representable binding inlining}