Newer
Older
<p>Suppose you have a function</p>
<pre>add :: Int -> Int -> Int<br />add a b = a + b</pre>
<p>Now suppose we have a second function</p>
<pre>add5 :: Int -> Int<br />add5 x = add 5 x</pre>
<p>So now <span class="tt">add5</span> is a function that takes its argument, adds it to 5, and returns the result.</p>
<p>In Haskell, we can simplify the definition of <span class="tt">add5</span> slightly by eliminating its argument, viz.:</p>
<pre>add5 = add 5</pre>
<p>This process is called "currying" (after Haskell Curry, who popularized the technique - yes, this is the same Haskell that the language is named after). <span class="tt">add5</span> is now declared like a constant, but it is still a function with one argument.</p>
<p>Now instead of seeing <span class="tt">add</span> as a function that takes two arguments, we can see it is a function which takes one argument, and returns another function with the value 5 embedded inside it. This second function also takes one argument. When you call this second function with some argument, it adds the argument with the value that's embedded inside it (in this case, 5) and returns its result. So <span class="tt">add x y</span> can also be written <span class="tt">(add x) y</span>.</p>
<p>We can also write add5 like this:</p>
<pre>add5 = \x -> add 5 x</pre>
<p>An expression like <span class="tt">\x -> y</span> is a λ-expression. (The Greek letter lambda (λ) can't be typed on most keyboards, but <span class="tt">\</span> looks a bit similar, so Haskell uses that instead.) It's an anonymous function that takes one argument, calling it <span class="tt">x</span>, and returns <span class="tt">y</span>. In lambda calculus notation, <span class="tt">\x -> y</span> is λx.y.</p>
<p>Suppose <span class="tt">y</span> is <span class="tt">5 + x</span>. If we want to call our λ-expression <span class="tt">\x -> 5 + x</span> (in lambda calculus, λx.5 + x) with some value <span class="tt">z</span>, we write <span class="tt">(\x -> 5 + x) z</span>. (If this confuses you, notice that <span class="tt">add 5</span> is just the same as <span class="tt">\x -> 5 + x</span>. I.e., it is a function that takes an argument and adds 5 to it. So <span class="tt">(\x -> 5 + x) z</span> is really just the same as <span class="tt">(add 5) z</span>, which as we established above is the same as <span class="tt">add 5 z</span>).</p>
<p>To evaluate <span class="tt">(\x -> 5 + x) z</span>, what we do is what is called a β-reduction (β being the Greek letter beta, if you didn't know). This basically involves replacing all occurences of the variable name <span class="tt">x</span> in the right hand side of the λ-expression with z. So <span class="tt">(\x -> 5 + x) z</span> becomes <span class="tt">5 + z</span>. This is what is expressed on your notes as something like (λx.y) z => y[z/x] (I might have got the z and x the wrong way round here, since I don't have my notes handy right now). y[z/x], which some texts write y[x := z], just means y with all appearances of x replaced with z.</p>
<p>There are two more conversions you can do: α-conversion and η-conversion. η-conversion (η is called eta) is the name given to the process by which we derived the second definition of add5 from the first (and in reverse, yields the third from the second). Basically, an expression like <span class="tt">\x -> f x</span> can be replaced with just <span class="tt">f</span>, because this "application" function is just the same as the function that it applies. (Because for any <span class="tt">z</span>, <span class="tt">(\x -> f x) z == f z</span>.) However, to take an example from "The Haskell School of Expression" (again from memory), a function like <span class="tt">foo x y = f y x y</span> can't be replaced by <span class="tt">foo x = f y x</span>, because then what is <span class="tt">y</span> on the right? This is what the notes mean when they say that λx.f x can be replaced with f only if x doesn't appear free in f. (The meaning of "free" here will be explained in the next paragraph.)</p>
<p>α-conversion (α is called alpha) is really just a technicality of the textual nature of the lambda calculus, and it says that two expressions which differ only in the names of their variables are the same. For example, suppose we have a function <span class="tt">\x -> (\x -> x)</span>. How then do we reduce <span class="tt">(\x -> (\x -> x)) z</span>? We can't reduce it to <span class="tt">\x -> z</span>, because the inner lambda declares <span class="tt">x</span> in the expression to the right of the arrow to be the function's argument (we say that this <span class="tt">x</span> is a bound variable, or is bound by this lambda - a free variable is simply one that isn't bound by a lambda). We have to rename this inner <span class="tt">x</span> to make it not clash. So we replace <span class="tt">x</span> in the inner lambda expression with some other name - say, <span class="tt">y</span>. Then <span class="tt">\x -> x</span> becomes <span class="tt">\y -> y</span>. Now <span class="tt">(\x -> (\y -> y)) z</span> obviously can only reduce to <span class="tt">(\y -> y)</span>[<span class="tt">z</span>/<span class="tt">x</span>], and since <span class="tt">x</span> doesn't appear in <span class="tt">\y -> y</span>, this reduces to just <span class="tt">\y -> y</span>.</p>
<p>So to summarise:</p>
<ul>
<li>λx.y means a function taking an argument x and returning y.</li>
<li>λx.y is written in Haskell as <span class="tt">\x -> y</span>.</li>
<li>In λx.f x, where x and f are variables, x is bound and f is free.</li>
<li>A function taking multiple arguments is the same as a function taking one argument and returning a function taking another argument. So if <span class="tt">foo bar baz = quux</span>, then
<pre>foo bar baz
= (foo bar) baz
= (\x -> (\y -> quux)) bar baz
= ((\x -> (\y -> quux)) bar) baz</pre>in
which all of <span class="tt">foo</span>, <span class="tt">foo bar</span>, <span class="tt">\x -> (\y -> quux)</span>, and <span class="tt">(\x -> (\y -> quux)) bar</span> are functions. Note that there is some syntactic sugar
in Haskell:<pre>\x -> (\y -> quux)
= \x -> \y -> quux
= \x y -> quux</pre></li>
<li>α-conversion: renaming bound variables, usually to avoid a clash.</li>
<li>β-reduction: evaluating function applications.</li>
<li>η-conversion: currying.</li>
</ul>