- \transexample{Case removal}{from}{to}
-
- \subsection{Removing polymorphism}
- Reference type-specialization (== argument propagation)
-
- Reference polymporphic binding inlining (== non-representable binding
- inlining).
-
- \subsection{Defunctionalization}
- These transformations remove most higher order expressions from our
- program, making it completely first-order (the only exception here is for
- arguments to builtin functions, since we can't specialize builtin
- function. TODO: Talk more about this somewhere).
-
- Reference higher-order-specialization (== argument propagation)
+ \transexample{caserem}{Case removal}{from}{to}
+
+ \subsection{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, but these are really meant to
+ address three different kinds of unrepresentable values:
+ Polymorphic values, higher order values and literals. Each of these
+ 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
+ \refdef{beta-reduction}
+ then be removed by β-reduction.
+
+ 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.
+
+ \todo{Finish this section}
+
+ There is one case where higher order values cannot be completely
+ removed: Builtin functions are still allowed to have higher
+ order arguments (Since we have no function body that we could
+ properly specialize). These are limited to (partial applications
+ of) top level functions, however, which is handled by the
+ top-level function extraction (see
+ \in{section}[sec:normalization:funextract]). However, the code
+ that generates \VHDL for builtin functions knows how to handle
+ these, so this is not a problem.
+
+ \subsubsection{Literals}
+ \todo{Fill this section}