X-Git-Url: https://git.stderr.nl/gitweb?p=matthijs%2Fmaster-project%2Freport.git;a=blobdiff_plain;f=Chapters%2FNormalization.tex;h=db743fc9a049d716c931747ca7cb09180723980a;hp=0f6d0eb23ecdff6c32920ee5b4ea20b6ee67ec68;hb=b1a9ce14b51423bf676df768278fd6b6d6579ca1;hpb=787eb0c9be548cf6e012647e2ef12eee2a734682 diff --git a/Chapters/Normalization.tex b/Chapters/Normalization.tex index 0f6d0eb..db743fc 100644 --- a/Chapters/Normalization.tex +++ b/Chapters/Normalization.tex @@ -958,12 +958,12 @@ \startbuffer[from] (+) :: Word -> Word -> Word - (+) = GHC.Num.(+) @Word $dNum + (+) = GHC.Num.(+) @Word \$dNum ~ (+) a b \stopbuffer \startbuffer[to] - GHC.Num.(+) @ Alu.Word $dNum a b + GHC.Num.(+) @ Alu.Word \$dNum a b \stopbuffer \transexample{toplevelinline}{Top level binding inlining}{from}{to} @@ -1610,8 +1610,7 @@ 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. + then be removed by β-reduction (\in{section}[sec:normalization:beta]). Since both type and dictionary arguments are not representable, \refdef{representable} @@ -1713,7 +1712,7 @@ η-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 + 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: @@ -1788,17 +1787,17 @@ expression shows an example: \startlambda - app2 :: (Word -> Word) -> Word -> Word - app2 = λf.λa.f (f a) + 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{app2} that takes a function as a + 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{app2} to apply a lambda epression twice. + 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 @@ -1808,23 +1807,23 @@ Applying this transformation to the example gives: \startlambda - app2' :: Word -> Word - app2' = λb.(λf.λa.f (f a)) (λx. x + x) b + 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{app2'} function is a bit complex, but the entire original body of - the original \lam{app2} function is wrapped in a lambda abstraction + \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'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) + twice' :: Word -> Word + twice' = λb.(b + b) + (b + b) \stoplambda This example also shows that the resulting normal form might not be as