app2 would get the 2 in subscript, which might be confusing.
expression shows an example:
\startlambda
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
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
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
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
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
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
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
\stoplambda
This example also shows that the resulting normal form might not be as