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}
η-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:
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
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