From: Jim Date: Sat, 7 Feb 2015 21:27:22 +0000 (-0500) Subject: push encodings (unfinished) X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=commitdiff_plain;h=f7ccd3396509d8fee56332f67ce0a98ccd568337 push encodings (unfinished) --- diff --git a/content.mdwn b/content.mdwn index ff03e690..f500b2b4 100644 --- a/content.mdwn +++ b/content.mdwn @@ -25,7 +25,7 @@ Week 2: * [[Introduction to the Lambda Calculus|topics/week2 lambda intro]] * [[Advanced notes on the Lambda Calculus|topics/week2 lambda advanced]] -* Encoding Booleans, Tuples, Lists, and Numbers (in progress) +* [[Encoding Booleans, Tuples, Lists, and Numbers|topics/week2 encodings]] (in progress); * Homework for week 2 (in progress) diff --git a/index.mdwn b/index.mdwn index 756cb216..4524ef30 100644 --- a/index.mdwn +++ b/index.mdwn @@ -93,7 +93,7 @@ The [[differences between our made-up language and Scheme, OCaml, and Haskell|ro > Topics: [[Intro to the Lambda Calculus|topics/week2 lambda intro]]; [[Advanced notes|topics/week2 lambda advanced]]; -Encoding Booleans, Tuples, Lists, and Numbers (in progress); +[[Encoding Booleans, Tuples, Lists, and Numbers|topics/week2 encodings]] (in progress); Homework (in progress) > Also, if you're reading the Hankin book, try reading Chapters 1-3. You will most likely need to come back again and read it multiple times; but this would be a good time to make the first attempt. diff --git a/topics/_lambda_encodings.mdwn b/topics/week2_encodings.mdwn similarity index 51% rename from topics/_lambda_encodings.mdwn rename to topics/week2_encodings.mdwn index 90fea0cc..46f15299 100644 --- a/topics/_lambda_encodings.mdwn +++ b/topics/week2_encodings.mdwn @@ -194,9 +194,150 @@ Of course, the last is still what's happening under the hood. ## Lists ## -Coming... +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. + +In seminar we discussed two further functions for working with lists or sequences. Reverting to Kapulet syntax, these functions work like this: + + fold_right (f, z) [10, 20, 30] + +That will evaluate to whatever this does: + + f (10, f (20, f (30, z))) + +For example, if we let `f` be `(+)` and `z` be `0`, then it will be `10 + (20 + (30 + 0))` or `60`. Another example, if we let `f` be `(&)` and `z` be `[]`, then `fold_right ((+), []) [10, 20, 30]` will be `10 & (20 & (30 & []))` or `[10, 20, 30]`, the same sequence we began with. + +The other function works like this: + + fold_left (f, z) [10, 20, 30] + +That will evaluate to whatever this does: + + f (f (f (z, 10), 20), 30) + +With a commutative operator like `(+)`, it makes no difference whether you say `fold_right ((+), z) xs` or `fold_left ((+), z) xs`. But with other operators it will make a difference. We can't say `fold_left ((&), []) [10, 20, 30]`, since that would start by trying to evaluate `[] & 10`, which would crash. But we could do this: + + let + flipped_cons match lambda (xs, x). x & xs # also expressible as `uncurried_flip (&)` + in fold_left (flipped_cons, []) [10, 20, 30] + +and that would evaluate to `flipped_cons (flipped_cons (flipped_cons ([], 10), 20), 30)`, in other words, to `30 & (20 & (10 & []))`, or `[30, 20, 10]`. So this reverses the sequence we began with. + +In class we considered how to express other list operations in terms of these. For example, we saw that we could define `length xs` as: + + fold_right ((lambda (_, z). 1 + z), 0) xs + +And we could define `map g xs` as: + + fold_right ((lambda (x, zs). g x & zs), []) xs + +Here is [a nice website](http://stevekrouse.github.io/hs.js) we found that lets you evaluate these things step by step. Just click on the subexpressions to evaluate them. + +We also saw in seminar how to define `fold_right`. We could do this in Kapulet like this: + + letrec + fold_right (f, z) xs = case xs of + [] then zs; + y & ys then f (y, fold_right (f, z) ys) + in fold_right + +(In some presentations you may see this with `f` as a curried function of the form `lambda x z. ...` rather than the uncurried form `lambda (x, z). ...` I have here.) + +We suggested in class that these functions were very powerful, and could be deployed to do most everything you might want to do with a list. Given how our strategy for encoding booleans turned out, this ought to suggest to you the idea that *folding is what we fundamentally do* with lists, just as *conditional branching is what we fundamentally do* with booleans. So we can try to encode lists in terms of lambda expressions that will let us perform folds on them. We could try to do this with either right-folds or left-folds. Either is viable. Some things are more natural if you use right-folds, though, so let's do that. + +But what should the encoding look like? We don't know *what* function and *what* starting value someone might want to fold over our list! + +Wait, does that remind you of anything? + +Good. I knew it would. + +Indeed, we'll make our encoded lists consist of higher-order *functions* that take the `f` and the starting value `z` to be folded *as arguments*. So the list `[a, b, c]` should look something like this: + + \f z. SOMETHING + +but what should the `SOMETHING` be? Well, when we supply an `f` and a `z` we should get the right-fold of those over `[a, b, c]` back, so the answer should evidently be: + + \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. + +So if `[a, b, c]` should be the displayed higher-order function above, what should `[c]` be? Evidently: + + \f z. f c z + +Now what should the empty list `[]` be? Think about it... + +Did you arrive at an answer? + +I hope it was this one: `\f z. z`. Because when we fold a function `f` and a starting value `z` over the empty list, we just get back whatever the starting value `z` was. + +We saw before what a `make-triple` function would look like. What about a `make-list` function, or as we've been calling it, "cons" (`&` in Kapulet)? Well, we've already seen what the representation of `[]` and `[c]` are. In that simplest case, the `cons` function should take us from the encoding of `[]`, namely `\f z. z` to the encoding of `[c]`, namely `\f z. f c z`, as a result. Here is how we can define this: + + let cons = \c cs. \f z. f c (cs f z) + in ... + +Let's walk through this. We supply this function with our `c` and `[]` as arguments. So its `c` gets bound to our `c`, and its `cs` gets bound to our `[]`, namely `\f z z`. Then our result is a higher order function of the form `\f z. f c SOMETHING`. That looks good, what we're after is just this, except the `SOMETHING` should be `z`. If we just simply said `z` here, then our `cons` function would always be giving us back a singleton list of the form `\f z. f x z` for some `x`. That's what we want in this case, but not in the general case. What we'd like is to use the second argument we fed to `cons`, here `[]` or `\f z. z`, and have it reduce to `z`, with the hope that the same strategy wuld make more complex second arguments reduce to other appropriate values. Well, `\f z. z` expects an `f` and a `z` as arguments, and hey we happen to have been given an `f` and a `z`, supplied by the consumer or user of the sequence `[c]` that we're building. So let's just give them to `\f z. z` as its arguments, and it gives us `z`. In other words, we make `SOMETHING` be `cs f z`. + +Formally: + + cons c [] + +is: + + (\c cs. \f z. f c (cs f z)) c (\f z. z) ~~> + (\cs. \f z. f c (cs f z)) (\f z. z) ~~> + \f z. f c ((\f z. z) f z) ~~> + \f z. f c ((\z. z) z) ~~> + \f z. f c z + +which is just the representation of `[c]` we were after. + +Will this work when more complex values are supplied as the second argument to `cons`? Let's see: + + cons b [c] + +is: + + (\c cs. \f z. f c (cs f z)) b (\f z. f c z) ~~> + (\cs. \f z. f b (cs f z)) (\f z. f c z) ~~> + \f z. f b ((\f z. f c z) f z) ~~> + \f z. f b ((\z. f c z) z) ~~> + \f z. f b (f c z) + +which looks right. Persuade yourself that the `cons` we've defined here, together with the representation `\f z. z` for the empty list, always give us the correct encoding for complex lists, in terms of a function that takes an `f` and a `z` as arguments, and then returns the result of right-folding those values over the list elements in the appropriate order. + +You may notice that the encoding we're proposing for `[]` is the same encoding we proposed above for `false`. There's nothing deep to this. If we had adopted other conventions, we could easily have made it instead be `true` and `[]` that had the same encoding. + +Now we saw above how to define `map` in terms of `fold_right`. In Kapulet syntax, `map g xs` was: + + fold_right ((lambda (x, zs). g x & zs), []) xs + +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 + +in Kapulet syntax, turns into this in our lambda evaluator: + + let empty = \f z. z in + let cons = \c cs. \f z. f c (cs f z) in + xs (\x zs. cons (g x) zs) empty + +Try out this: + + let empty = \f z. z in + let cons = \c cs. \f z. f c (cs f z) in + let map = \g xs. xs (\x zs. cons (g x) zs) empty in + let abc = \f z. f a (f b (f c z)) in + map g abc + +That will evaluate to: + + \f z. f (g a) (f (g b) (f (g c) z)) + +which looks like what we want, a higher-order function that will take an `f` and a `z` as arguments and then return the right fold of those values over `[g a, g b, g c]`, which is `map g [a, b, c]`. ## Numbers ## -Coming... +It's noteworthy that when he was developing the lambda calculus, Church had not predicted it would be possible to encode the numbers. It came as a welcome surprise. + +*More coming...*