author Matthijs Kooijman Tue, 1 Dec 2009 19:53:35 +0000 (20:53 +0100) committer Matthijs Kooijman Tue, 1 Dec 2009 19:53:35 +0000 (20:53 +0100)
app2 would get the 2 in subscript, which might be confusing.

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