## Booleans ##
-We'll start with the `if ... then
-... else...` construction we saw last week:
+We'll start with the `if ... then ... else ...` construction we saw last week:
if M then N else L
~~> ((\x x) L)
~~> L
-So have seen our first major encoding in the Lambda Calculus:
+So we have seen our first major encoding in the Lambda Calculus:
"true" is represented by **K**, and "false" is represented by **K I**.
We'll be building up a lot of representations in the weeks to come,
and they will all maintain the discipline that if a expression is
Our proposal was to define the triple `(a, b, c)` as:
- \f. f a b c
+ \h. h a b c
To extract the first element of this, you'd write:
- (\f. f a b c) fst_of_three
+ (\h. h a b c) fst_of_three
where `fst_of_three` is the function `\x y z. x`:
- (\f. f a b c) (\x y z. x) ~~>
+ (\h. h a b c) (\x y z. x) ~~>
(\x y z. x) a b c ~~>
(\y z. a) b c ~~>
(\z. a) c ~~>
Here are the corresponding definitions in Scheme (Racket):
(define make-triple (lambda (a) (lambda (b) (lambda (c)
- (lambda (f) (((f a) b) c))))))
+ (lambda (h) (((h a) b) c))))))
(define fst_of_three (lambda (x) (lambda (y) (lambda (z) x))))
(define snd_of_three (lambda (x) (lambda (y) (lambda (z) y))))
If you really want to, you can disguise what's going on like this:
- (define lifted-fst_of_three (lambda (p) (p fst_of_three)))
+ (define lifted-fst_of_three (lambda (trip) (trip fst_of_three)))
Then you could say:
- (lifted-fst_of_three p)
+ (lifted-fst_of_three t)
instead of:
- (p fst_of_three)
+ (t fst_of_three)
Of course, the last is still what's happening under the hood.
(Remark: `(lifted-f (((make-triple 10) 20) 30))` stands to `((((make-triple 10) 20) 30) f)` as
`((((make-triple 10) 20) 30) f)` stands to `(((f 10) 20) 30)`.)
+
+### Curried and Uncurried functions in the Lambda Calculus ###
+
+As we've explained before, an *uncurried* function is one that takes multiple arguments in a single bundle, as a tuple, like this:
+
+ f (x, y, z)
+
+Whereas a *curried* function is one that takes multiple arguments in sequence, like this:
+
+ g x y z
+
+That is, `g` is a function expecting one argument (here `x`), that evaluates to a second function, that itself expects another argument (here `y`), and so on. (So `g` is a *higher-order function*: the result of applying it to argument `x` returns another function.) In discussing Kapulet and Scheme and OCaml and Haskell, we sometimes worked with uncurried functions, and other times with curried ones. Now that you've seen how to build and work with tuples in the Lambda Calculus, you can write uncurried functions there too. That is, you can write functions `f` that will expect arguments of the form `\h. h x y z`. But in the end, `f` is going to have to apply that argument to some auxiliary handler function `g` anyway, where `g` takes *its* arguments in curried form. So if you can, in the Lambda Calculus it's easiest to just work with curried functions like `g` in the first place, rather than uncurried, tuple-expecting arguments like `f`.
+
+In some cases you can't do this, because you'll be partaking of some general pattern that only makes room for a single argument --- like the "starting value" `z` in the `fold_right` function discussed below; yet you're performing some task that really requires you to stuff a couple of values into that position. Tuples are ideal for that purpose. But in for run-of-the-mill functions you're defining in the Lambda Calculus, if multiple arguments need to be passed to a function, and it's up to you whether to pass them in curried or uncurried/tuple style, you should default to the curried style (as in, `g x y z`). That's the more idiomatic, native style for passing arguments in the Lambda Calculus.
+
+
## Lists ##
There are multiple ways to encode lists, and also multiple ways to encode numbers. We are going to start with what we think are the most natural and elegant encodings. Historically these were the first encodings of numbers but not of lists.
\f z. f a (f b (f c z))
-Here we work with curried functions, because that's how the Lambda Calculus does things. You wouldn't want to build up a tuple using the mechanisms described above, and then supply `f` as an argument to that tuple, and so on. That would be a lot of red tape for no benefit. In the Lambda Calculus, it's simpler to just work with curried functions as our natural idiom.
+Here we assume `f` to be a curried function, taking its arguments in the form `f c z` rather that `f (c, z)` (that is, `f (\h. h c z)`), because as we explained at the end of the section on Tuples, the curried form is the idiomatic and native style for passing multiple arguments in the Lambda Calculus.
So if `[a, b, c]` should be the displayed higher-order function above, what should `[c]` be? Evidently:
In our Lambda Calculus encoding, `fold_right (f, z) xs` gets translated to `xs f z`. That is, the list itself is the operator, just as we saw triples being. So we just need to know how to represent `lambda (x, zs). g x & zs`, on the one hand, and `[]` on the other, into the Lambda Calculus, and then we can also express `map`. Well, in the Lambda Calculus we're working with curried functions, and there's no infix syntax, so we'll replace the first by `lambda x zs. cons (g x) zs`. But we just defined `cons`, and the lambda is straightforward. And we also just defined `[]`. So we already have all the pieces to do this. Namely:
- map (g, z) xs
+ map g xs
in Kapulet syntax, turns into this in our lambda evaluator:
<code>3 ≡ \f z. f (f (f z)) ; or \f z. f<sup>3</sup> z</code>
<code>...</code>
-The encoding for `0` can also be written as `\f z. z`, which we've also proposed as the encoding for `[]` and for `false`. Don't read too much into this.
+The encoding for `0` is equivalent to `\f z. z`, which we've also proposed as the encoding for `[]` and for `false`. Don't read too much into this.
Given the above, can you figure out how to define the `succ` function? We already worked through the definition of `cons`, and this is just a simplification of that, so you should be able to do it. We'll make it a homework.