From: Matthijs Kooijman Date: Tue, 1 Dec 2009 19:40:46 +0000 (+0100) Subject: Restructure and expand parts of the normalization chapter. X-Git-Tag: final-thesis~126 X-Git-Url: https://git.stderr.nl/gitweb?p=matthijs%2Fmaster-project%2Freport.git;a=commitdiff_plain;h=787eb0c9be548cf6e012647e2ef12eee2a734682 Restructure and expand parts of the normalization chapter. --- diff --git a/Chapters/HardwareDescription.tex b/Chapters/HardwareDescription.tex index 20c43e3..2f72a8b 100644 --- a/Chapters/HardwareDescription.tex +++ b/Chapters/HardwareDescription.tex @@ -342,6 +342,7 @@ and3 a b c = and (and a b) c types) and just one field (which are technically not a product). \stopdesc \startdesc{Enumerated types} + \defref{enumerated types} An enumerated type is an algebraic datatype with multiple constructors, but none of them have fields. This is essentially a way to get an enum-like type containing alternatives. diff --git a/Chapters/Normalization.tex b/Chapters/Normalization.tex index c42aa3a..0f6d0eb 100644 --- a/Chapters/Normalization.tex +++ b/Chapters/Normalization.tex @@ -316,7 +316,7 @@ - \subsection{Intended normal form definition} + \subsection[sec:normalization:intendednormalform]{Intended normal form definition} Now we have some intuition for the normal form, we can describe how we want the normal form to look like in a slightly more formal manner. The following EBNF-like description completely captures the intended structure (and @@ -331,11 +331,11 @@ \italic{normal} = \italic{lambda} \italic{lambda} = λvar.\italic{lambda} (representable(var)) | \italic{toplet} - \italic{toplet} = letrec [\italic{binding}...] in var (representable(varvar)) + \italic{toplet} = letrec [\italic{binding}...] in var (representable(var)) \italic{binding} = var = \italic{rhs} (representable(rhs)) -- State packing and unpacking by coercion | var0 = var1 ▶ State ty (lvar(var1)) - | var0 = var1 ▶ ty (var0 :: State ty) (lvar(var1)) + | var0 = var1 ▶ ty (var1 :: State ty) (lvar(var1)) \italic{rhs} = userapp | builtinapp -- Extractor case @@ -364,7 +364,7 @@ no longer true, btw} When looking at such a program from a hardware perspective, the top level - lambda's define the input ports. The variable referenc in the body of + lambda's define the input ports. The variable reference in the body of the recursive let expression is the output port. Most function applications bound by the let expression define a component instantiation, where the input and output ports are mapped to local @@ -843,8 +843,7 @@ \stopbuffer \transexample{beta-type}{β-reduction for type abstractions}{from}{to} - - + \subsubsection{Empty let removal} This transformation is simple: It removes recursive lets that have no bindings (which usually occurs when unused let binding removal removes the last @@ -861,7 +860,7 @@ \todo{Example} - \subsubsection{Simple let binding removal} + \subsubsection[sec:normalization:simplelet]{Simple let binding removal} This transformation inlines simple let bindings, that bind some binder to some other binder instead of a more complex expression (\ie a = b). @@ -993,7 +992,7 @@ of the other value definitions in let bindings and making the final return value a simple variable reference. - \subsubsection{η-abstraction} + \subsubsection[sec:normalization:eta]{η-abstraction} This transformation makes sure that all arguments of a function-typed expression are named, by introducing lambda expressions. When combined with β-reduction and non-representable binding inlining, all function-typed @@ -1020,7 +1019,7 @@ \transexample{eta}{η-abstraction}{from}{to} - \subsubsection{Application propagation} + \subsubsection[sec:normalization:appprop]{Application propagation} This transformation is meant to propagate application expressions downwards into expressions as far as possible. This allows partial applications inside expressions to become fully applied and exposes new transformation @@ -1358,7 +1357,7 @@ categories instead. \stopitemize - \subsubsection{Argument simplification} + \subsubsection[sec:normalization:argsimpl]{Argument simplification} This transform deals with arguments to functions that are of a runtime representable type. It ensures that they will all become references to global variables, or local signals in the resulting @@ -1629,51 +1628,278 @@ \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 - \todo{Finish this section} + 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. - 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. + 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:approp]). 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 + app2 :: (Word -> Word) -> Word -> Word + app2 = λf.λa.f (f a) + + main = λa.app (λx. x + x) a + \stoplambda + + This example shows a function \lam{app2} 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{app2} 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 + app2' :: Word -> Word + app2' = λ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{app2'} function is a bit complex, but the entire original body of + the original \lam{app2} function is wrapped in a lambda abstraction + and applied to the argument we've specialized for (\lam{λx. x + x}) + and the other arguments. This complex expression can fortunately be + effectively reduced by repeatedly applying β-reduction: + + \startlambda + app2' :: Word -> Word + app2' = λ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{Literals} - \todo{Fill this section} + There are a limited number of literals available in Haskell and Core. + \refdef{enumerated types} When using (enumerating) algebraic + datatypes, 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} typeclass, which offers a \hs{fromInteger} method + that converts any \hs{Integer} to the Cλash datatypes. + + 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 builtin + 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 builtin 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{Non-representable binding inlining} - \todo{Move this section into a new section (together with - specialization?)} This transform inlines let bindings that are bound to a non-representable value. Since we can never generate a signal assignment for these bindings (we cannot declare a signal assignment with a non-representable type, for obvious reasons), we have no choice but to inline the binding to remove it. - If the binding is non-representable because it is a lambda abstraction, it is - likely that it will inlined into an application and β-reduction will remove - the lambda abstraction and turn it into a representable expression at the - inline site. The same holds for partial applications, which can be turned into - full applications by inlining. - - Other cases of non-representable bindings we see in practice are primitive - Haskell types. In most cases, these will not result in a valid normalized - output, but then the input would have been invalid to start with. There is one - exception to this: When a builtin function is applied to a non-representable - expression, things might work out in some cases. For example, when you write a - literal \hs{SizedInt} in Haskell, like \hs{1 :: SizedInt D8}, this results in - the following core: \lam{fromInteger (smallInteger 10)}, where for example - \lam{10 :: GHC.Prim.Int\#} and \lam{smallInteger 10 :: Integer} have - non-representable types. \todo{Expand on this. This/these paragraph(s) - should probably become a separate discussion somewhere else} - - \todo{Can this duplicate work? -- For polymorphism probably, for - higher order expressions only if they are inlined before they - are themselves normalized.} + As we have seen in the previous sections, inlining these bindings + solves (part of) the polymorphism, higher order values and + unrepresentable literals in an expression. \starttrans letrec @@ -1714,68 +1940,204 @@ \transexample{nonrepinline}{Nonrepresentable binding inlining}{from}{to} - \subsubsection{Argument propagation} - \todo{Rename this section to specialization} - - This transform deals with arguments to user-defined functions that are - not representable at runtime. This means these arguments cannot be - preserved in the final form and most be {\em propagated}. + \subsubsection{Function specialization} + This transform removes arguments to user-defined functions that are + not representable at runtime. This is done by creating a + \emph{specialized} version of the function that only works for one + particular value of that argument (in other words, the argument can be + removed). - Propagation means to create a specialized version of the called - function, with the propagated argument already filled in. As a simple - example, in the following program: + Specialization means to create a specialized version of the called + function, with one argument already filled in. As a simple example, in + the following program (this is not actual Core, since it directly uses + a literal with the unrepresentable type \lam{GHC.Prim.Int\#}). \startlambda f = λa.λb.a + b inc = λa.f a 1 \stoplambda - We could {\em propagate} the constant argument 1, with the following - result: + We could specialize the function \lam{f} against the literal argument + 1, with the following result: \startlambda f' = λa.a + 1 inc = λa.f' a \stoplambda - Special care must be taken when the to-be-propagated expression has any - free variables. If this is the case, the original argument should not be - removed completely, but replaced by all the free variables of the - expression. In this way, the original expression can still be evaluated - inside the new function. Also, this brings us closer to our goal: All - these free variables will be simple variable references. + In some way, this transformation is similar to β-reduction, but it + operates across function boundaries. It is also similar to + non-representable let binding inlining above, since it sort of + \quote{inlines} an expression into a called function. - To prevent us from propagating the same argument over and over, a simple - local variable reference is not propagated (since is has exactly one - free variable, itself, we would only replace that argument with itself). + Special care must be taken when the argument has any free variables. + If this is the case, the original argument should not be removed + completely, but replaced by all the free variables of the expression. + In this way, the original expression can still be evaluated inside the + new function. - This shows that any free local variables that are not runtime representable - cannot be brought into normal form by this transform. We rely on an - inlining transformation to replace such a variable with an expression we - can propagate again. + To prevent us from propagating the same argument over and over, a + simple local variable reference is not propagated (since is has + exactly one free variable, itself, we would only replace that argument + with itself). + + This shows that any free local variables that are not runtime + representable cannot be brought into normal form by this transform. We + rely on an inlining or β-reduction transformation to replace such a + variable with an expression we can propagate again. \starttrans x = E ~ - x Y0 ... Yi ... Yn \lam{Yi} is not of a runtime representable type + x Y0 ... Yi ... Yn \lam{Yi} is not representable --------------------------------------------- \lam{Yi} is not a local variable reference x' y0 ... yi-1 f0 ... fm Yi+1 ... Yn \lam{f0 ... fm} are all free local vars of \lam{Yi} - ~ - x' = λy0 ... λyi-1. λf0 ... λfm. λyi+1 ... λyn . + ~ \lam{T0 ... Tn} are the types of \lam{Y0 ... Yn} + x' = λ(y0 :: T0) ... λ(yi-1 :: Ty-1). λf0 ... λfm. λ(yi+1 :: Ty+1) ... λ(yn :: Tn). E y0 ... yi-1 Yi yi+1 ... yn \stoptrans - \todo{Describe what the formal specification means} - \todo{Note that we don't change the sepcialised function body, only - wrap it} - \todo{This does not take care of updating the types of y0 ... - yn. The code uses the types of Y0 ... Yn for this, regardless of - whether the type arguments were properly propagated...} + This is a bit of a complex transformation. It transforms an + application of the function \lam{x}, where one of the arguments + (\lam{Y_i}) is not representable. A new + function \lam{x'} is created that wraps the body of the old function. + The body of the new function becomes a number of nested lambda + abstractions, one for each of the original arguments that are left + unchanged. + + The ith argument is replaced with the free variables of + \lam{Y_i}. Note that we reuse the same binders as those used in + \lam{Y_i}, since we can then just use \lam{Y_i} inside the new + function body and have all of the variables it uses be in scope. + + The argument that we are specializing for, \lam{Y_i}, is put inside + the new function body. The old function body is applied to it. Since + we use this new function only in place of an application with that + particular argument \lam{Y_i}, behaviour should not change. + + Note that the types of the arguments of our new function are taken + from the types of the \emph{actual} arguments (\lam{T0 ... Tn}). This + means that any polymorphism in the arguments is removed, even when the + corresponding explicit type lambda is not removed + yet.\refdef{type lambda} - \todo{Example} + \todo{Examples. Perhaps reference the previous sections} + + + \section{Unsolved problems} + The above system of transformations has been implemented in the prototype + and seems to work well to compile simple and more complex examples of + hardware descriptions. \todo{Ref christiaan?} However, this normalization + system has not seen enough review and work to be complete and work for + every Core expression that is supplied to it. A number of problems + have already been identified and are discussed in this section. + \subsection[sec:normalization:duplicatework]{Work duplication} + A possible problem of β-reduction is that it could duplicate work. + When the expression applied is not a simple variable reference, but + requires calculation and the binder the lambda abstraction binds to + is used more than once, more hardware might be generated than strictly + needed. + As an example, consider the expression: + + \startlambda + (λx. x + x) (a * b) + \stoplambda + + When applying β-reduction to this expression, we get: + + \startlambda + (a * b) + (a * b) + \stoplambda + + which of course calculates \lam{(a * b)} twice. + + A possible solution to this would be to use the following alternative + transformation, which is of course no longer normal β-reduction. The + followin transformation has not been tested in the prototype, but is + given here for future reference: + + \starttrans + (λx.E) M + ----------------- + letrec x = M in E + \stoptrans + + This doesn't seem like much of an improvement, but it does get rid of + the lambda expression (and the associated higher order value), while + at the same time introducing a new let binding. Since the result of + every application or case expression must be bound by a let expression + in the intended normal form anyway, this is probably not a problem. If + the argument happens to be a variable reference, then simple let + binding removal (\in{section}[sec:normalization:simplelet]) will + remove it, making the result identical to that of the original + β-reduction transformation. + + When also applying argument simplification to the above example, we + get the following expression: + + \startlambda + let y = (a * b) + z = (a * b) + in y + z + \stoplambda + + Looking at this, we could imagine an alternative approach: Create a + transformation that removes let bindings that bind identical values. + In the above expression, the \lam{y} and \lam{z} variables could be + merged together, resulting in the more efficient expression: + + \startlambda + let y = (a * b) in y + y + \stoplambda + + \subsection{Non-determinism} + As an example, again consider the following expression: + + \startlambda + (λx. x + x) (a * b) + \stoplambda + + We can apply both β-reduction (\in{section}[sec:normalization:beta]) + as well as argument simplification + (\in{section}[sec:normalization:argsimpl]) to this expression. + + When applying argument simplification first and then β-reduction, we + get the following expression: + + \startlambda + let y = (a * b) in y + y + \stoplambda + + When applying β-reduction first and then argument simplification, we + get the following expression: + + \startlambda + let y = (a * b) + z = (a * b) + in y + z + \stoplambda + As you can see, this is a different expression. This means that the + order of expressions, does in fact change the resulting normal form, + which is something that we would like to avoid. In this particular + case one of the alternatives is even clearly more efficient, so we + would of course like the more efficient form to be the normal form. + + For this particular problem, the solutions for duplication of work + seem from the previous section seem to fix the determinism of our + transformation system as well. However, it is likely that there are + other occurences of this problem. + + \subsection{Casts} + We do not fully understand the use of cast expressions in Core, so + there are probably expressions involving cast expressions that cannot + be brought into intended normal form by this transformation system. + + The uses of casts in the core system should be investigated more and + transformations will probably need updating to handle them in all + cases. \section[sec:normalization:properties]{Provable properties} When looking at the system of transformations outlined above, there are a diff --git a/Outline b/Outline index 35ccc7d..7a18303 100644 --- a/Outline +++ b/Outline @@ -59,3 +59,5 @@ TODO: simplification -> Normalisation? TODO: Use saturated (application) instead of complete (application)? TODO: core => Core TODO: \defref{beta-reduction} -> \defref{β-reduction} +TODO: Make interaction links not bold +TODO: Say something about implementation differences with transformation specs