rename topics/_week5_system_F.mdwn to topics/week5_system_F.mdwn
[lambda.git] / topics / week2_encodings.mdwn
1 # Encoding Booleans, Tuples, Lists, and Numbers #
2
3 The Lambda Calculus can represent any computable function?
4
5 We need to do some work to show how to represent some of the functions
6 we've become acquainted with.
7
8 <a id=booleans></a>
9 ## Booleans ##
10
11 We'll start with the `if ... then ... else ...` construction we saw last week:
12
13     if M then N else L
14
15 For a boolean-valued expression `M`, the displayed expression should evaluate to whatever `N` does
16 if `M` evaluates to `'true`, and to whatever `L` does if `M` evaluates to `'false`.
17 In order to encode or simulate such an `if` clause in the Lambda Calculus, we
18 need to settle on a way to represent `'true` and `'false`.
19
20 We could simply add the constants `'true` and `'false` to the
21 language, since it does make sense to extend the Lambda Calculus by adding constants.
22 However, that would also require complicating the
23 interpretation of the language; at the very least, we would need more
24 than just beta-reduction as our engine of computation.  In the spirit
25 of computational minimalism, let's see how far we can get with the
26 "pure" lambda calculus, without any special constants.
27
28 Let's get rid of the parts of the `if` statement that are
29 just syntactic window-dressing.  That is, let's get rid of the
30 `if`, the `then`, and the `else`:
31
32     M  N  L
33
34 Recall that our convention is that values associate left to right, so
35 this series of terms would be evaluated as:
36
37     ((M N) L)
38
39 If this expression is supposed to have the meaning of `if M then N
40 else L`, then we need to find a value for `'true` such that when it is
41 substituted in place of `M`, the expression evaluates to `N`.  The
42 function we're looking for should take two arguments: first `N`, then `L`,
43 and it should throw away `L` and return `N`.
44
45 We've already seen such a function.  We called it **K**: `(\x y. x)`.
46 Let's test:
47
48     ((K N) L) == (((\x y. x) N) L) ~~> ((\y. N) L) ~~> N
49
50 Sucess! In the same spirit, `'false` could be **K I**, which reduces to `(\y x. x)` (also written as `(\y. (\x x))`):
51
52     (((K I) N) L) == ((((\x y. x) (\x x)) N) L)
53                      ~~> (((\y. (\x x)) N) L)
54                      ~~> ((\x x) L)
55                      ~~> L
56
57 So we have seen our first major encoding in the Lambda Calculus:
58 "true" is represented by **K**, and "false" is represented by **K I**.
59 We'll be building up a lot of representations in the weeks to come,
60 and they will all maintain the discipline that if a expression is
61 meant to be interpreted as a truth value (i.e. as a Boolean), it will
62 be equivalent to (convertible with) **K** or **K I**.
63
64 In class, we explained how "and" could be thought of as the function, here written
65 in Kapulet syntax:
66
67     lambda p q. if p then q else false
68
69 or:
70
71     lambda p q. if p then q else p
72
73 Given that we know how to express `if ... then ...` in terms of our encoded Booleans,
74 we can represent this easily in the Lambda Calculus as either:
75
76     \p q. p q (\y x. x)
77
78 or:
79
80     \p q. p q p
81
82 Typically there will be more than one way to encode a given function into the Lambda Calculus, even holding fixed
83 all your other decisions about how to encode other functions. In this case, we can use either representation
84 because we're assuming that the `p` only gets bound to arguments that are either `\x y. x` or `\y x. x`. We don't make any
85 promises about what will happen if our encodings are abused, that is, supplied with arguments they weren't designed to accept.
86 If `p` is bound to `\x y. x`, then the result of both of the above displayed expressions will be whatever `q` is bound to.
87 If on the other hand, `p` is bound to `\y x. x`, then the two displayed expressions will return the same result, namely that function.
88
89 Despite this, the two displayed expressions are two different lambda terms, and
90 are not convertible. It's only within the frame of our assumptions about the
91 restricted arguments we're thinking of supplying them that they behave exactly
92 alike.
93
94 You can try out these expressions in the [[lambda evaluator|code/lambda evaluator]]:
95
96     let true = \x y. x in
97     let false = \y x. x in
98     let and = \p q. p q p in
99     and true false
100
101 will reduce or "normalize" to `\y x. x`, or false, just as you'd predict. The `let true =` stuff isn't officially part of the Lambda Calculus language. It's just a convenient shorthand that lets you use the lambda evaluator more easily. Behind the scenes, the displayed expression above gets translated to:
102
103     (\true.
104       (\false.
105         (\and. and true false)))
106         (\x y. x) ; this gets bound to variable "true"
107         (\y x. x) ; this gets bound to variable "false"
108         (\p q. p q p) ; this gets bound to variable "and"
109
110 We expect you'll agree that the first is easier to write and to read.
111
112 In Scheme (Racket), all of these notions can be defined like this:
113
114     (define true  (lambda (x) (lambda (y) x)))
115     (define false (lambda (y) (lambda (x) x)))
116     (define lambda-and (lambda (p) (lambda (q) ((p q) p))))
117
118 and then used like this:
119
120     ((lambda-and true) false)
121
122 which will evaluate to a function, that happens to be the same function `false` is bound to. Most Scheme interpreters like Racket will helpfully display the function with the name, if any, that was first defined to be bound to it. So we'll see the result as:
123
124     #<procedure:false>
125
126 The funny calling pattern, where we write `((lambda-and true) false)` instead of just `(lambda-and true false)`, is because that's how you have to write curried functions in Scheme. Similarly for why we have `(lambda (x) (lambda (y) x))` instead of just `(lambda (x y) x)`.
127
128 It's possible to do the next few weeks of assignment without using a Scheme interpreter, however
129 we do recommend you [get Scheme installed on your
130 computer](/how_to_get_the_programming_languages_running_on_your_computer), and
131 [get started learning Scheme](/learning_scheme). It will help you understand the ideas better to experiment with it.
132
133 There's also a (slow, bare-bones, but perfectly adequate) version of Scheme available for online use at <http://tryscheme.sourceforge.net/>. (Unfortunately, though, that Scheme implementation will only display the result of `((lambda-and true) false)` as `#<procedure lambda>`. You won't be able to see if it's the function assigned to `true` or the function assigned to `false`. You'd have to feed that result some more arguments to see how it behaved.)
134
135 You should also be experimenting with this site's [[lambda evaluator|code/lambda evaluator]].
136
137
138 <a id=tuples></a>
139 ## Tuples ##
140
141 In class, we also showed you how to encode a tuple in the Lambda Calculus. We did it with an ordered triple, but the strategy generalizes in a straightforward way. (Some authors just use this strategy to define *pairs*, then define triples as pairs whose second member is another pair, and so on. Yech. If you keep a firm grip on your wits, that can also be made to work, but it's extremely likely that people who code in that way are going to lose their grip at some point and get themselves in a corner where they'll regret having made that decision about how to encode triples. And they will be forced to add further complexities at later points, that they're probably not anticipating now. The strategy presented here is as elegant as it first looks, and will help you program more hygienically even when your attention lapses.)
142
143 Our proposal was to define the triple `(a, b, c)` as:
144
145     \h. h a b c
146
147 To extract the first element of this, you'd write:
148
149     (\h. h a b c) fst_of_three
150
151 where `fst_of_three` is the function `\x y z. x`:
152
153     (\h. h a b c) (\x y z. x) ~~>
154     (\x y z. x) a b c ~~>
155     (\y z. a) b c ~~>
156     (\z. a) c ~~>
157     a
158
159 Here are the corresponding definitions in Scheme (Racket):
160
161     (define make-triple (lambda (a) (lambda (b) (lambda (c)
162                           (lambda (h) (((h a) b) c))))))
163
164     (define fst_of_three (lambda (x) (lambda (y) (lambda (z) x))))
165     (define snd_of_three (lambda (x) (lambda (y) (lambda (z) y))))
166     (define trd_of_three (lambda (x) (lambda (y) (lambda (z) z))))
167
168 Then:
169
170     (define p (((make-triple 10) 20) 30))
171     (p fst_of_three)  ; will evaluate to 10
172     (p snd_of_three)  ; will evaluate to 20
173
174 If you're puzzled by having the triple to the left and the function that "uses" or "consumes" or operates on it to the right, think about why it's being done this way: the triple is a package that will be used in coordination with some function for operating on its elements. We don't know in advance what that function will be. And it's not obvious how to make the triple be some structure that the function can "look inside" and extract the elements from. We're still trying to *figure out* how to define such structures! But what we can do is make *the triple take the function as an argument*, and return *the result of* operating on its elements with that function. In other words, the triple is a higher-order function: a function that expects another function as an argument.
175
176 (Consider the similarities between this definition of a triple and a generalized quantifier. This is in fact our first taste of "continuations" in the course, which are a systematic pattern for inverting the naive order of who-is-the-argument? and who-is-the-operator?)
177
178 If you really want to, you can disguise what's going on like this:
179
180     (define lifted-fst_of_three (lambda (trip) (trip fst_of_three)))
181
182 Then you could say:
183
184     (lifted-fst_of_three t)
185
186 instead of:
187
188     (t fst_of_three)
189
190 Of course, the last is still what's happening under the hood.
191
192 (Remark: `(lifted-f (((make-triple 10) 20) 30))` stands to `((((make-triple 10) 20) 30) f)` as
193 `((((make-triple 10) 20) 30) f)` stands to `(((f 10) 20) 30)`.)
194
195
196 ### Curried and Uncurried functions in the Lambda Calculus ###
197
198 As we've explained before, an *uncurried* function is one that takes multiple arguments in a single bundle, as a tuple, like this:
199
200     f (x, y, z)
201
202 Whereas a *curried* function is one that takes multiple arguments in sequence, like this:
203
204     g x y z
205
206 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`.
207
208 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.
209
210
211 <a id=lists></a>
212 ## Lists ##
213
214 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.
215
216 In seminar we discussed two further functions for working with lists or sequences. Reverting to Kapulet syntax, these functions work like this:
217
218     fold_right (f, z) [10, 20, 30]
219
220 That will evaluate to whatever this does:
221
222     f (10, f (20, f (30, z)))
223
224 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.
225
226 The other function works like this:
227
228     fold_left (f, z) [10, 20, 30]
229
230 That will evaluate to whatever this does:
231
232     f (f (f (z, 10), 20), 30)
233
234 <a id=flipped-cons></a>
235 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:
236
237     let
238       flipped_cons match lambda (xs, x). x & xs  # also expressible as `uncurried_flip (&)`
239     in fold_left (flipped_cons, []) [10, 20, 30]
240
241 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.
242
243 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:
244
245     fold_right ((lambda (_, z). 1 + z), 0) xs
246
247 And we could define `map g xs` as:
248
249     fold_right ((lambda (x, zs). g x & zs), []) xs
250
251 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.
252
253 We also saw in seminar how to define `fold_right`. We could do this in Kapulet like this:
254
255     letrec
256       fold_right (f, z) xs = case xs of
257                                [] then z;
258                                y & ys then f (y, fold_right (f, z) ys)
259                              end
260     in fold_right
261
262 (In some presentations you may see this expecting `f` to be a curried function `lambda y z. ...` rather than the uncurried `lambda (y, z). ...` that I'm expecting here. We will be shifting to the curried form ourselves momentarily.)
263
264 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.
265
266 What should the encoding look like? We don't know *what* function and *what* starting value someone might want to fold over our list!
267
268 Wait, does that remind you of anything?
269
270 Good. I knew it would.
271
272 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:
273
274     \f z. SOMETHING
275
276 Now, what should the `SOMETHING` be? Well, when we supply an `f` and a `z` we should get back the right-fold of those over `[a, b, c]`, so the answer should evidently be:
277
278     \f z. f a (f b (f c z))
279
280 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.
281
282 So if `[a, b, c]` should be the displayed higher-order function above, what should `[c]` be? Evidently:
283
284     \f z. f c z
285
286 Now what should the empty list `[]` be? Think about it...
287
288 Did you arrive at an answer?
289
290 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.
291
292 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:
293
294     let cons = \d ds. \f z. f d (ds f z)
295     in ...
296
297 Let's walk through this. We supply this function with our `c` and `[]` as arguments. So its `d` gets bound to our `c`, and its `ds` 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 end up as `z`. If we just simply *substituted* `z` for `SOMETHING`, then our `cons` function would *always* end up giving us back a singleton list of the form `\f z. f X z` for some `X`. That is the form we want in the present case, computing `cons c []`, but not in the general case. What we'd like instead is to *do something to* the second argument we fed to `cons`, here `[]` or `\f z. z`, and have *it* reduce to `z`, with the hope that the same operation would 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 an `f` and a `z` handy, since we're inside something of the form `\f z. f c SOMETHING`. The `f` and `z` will be supplied by the consumer or user of the sequence `[c]` that we're building. So let's just give *those* `f` and `z` to `\f z. z` as *its* arguments, and we end up with simply `z`. In other words, where `ds` is the second argument we fed to `cons`, we make `SOMETHING` in `\f z. f c SOMETHING` be `ds f z`. That is why we make `cons` be:
298
299     \d ds. \f z. f d (ds f z)
300
301 Let's step through it formally. Given our definitions:
302
303     cons c []
304
305 is:
306
307     (\d ds. \f z. f d (ds f z)) c (\f z. z) ~~>
308     (\ds. \f z. f c (ds f z)) (\f z. z) ~~>
309     \f z. f c ((\f z. z) f z) ~~>
310     \f z. f c ((\z. z) z) ~~>
311     \f z. f c z
312
313 which is just the representation of `[c]` we were after.
314
315 Will this work when more complex values are supplied as the second argument to `cons`? Let's see:
316
317     cons b [c]
318
319 is:
320
321     (\d ds. \f z. f d (ds f z)) b (\f z. f c z) ~~>
322     (\ds. \f z. f b (ds f z)) (\f z. f c z) ~~>
323     \f z. f b ((\f z. f c z) f z) ~~>
324     \f z. f b ((\z. f c z) z) ~~>
325     \f z. f b (f c z)
326
327 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 arguments over the list elements in the appropriate order.
328
329 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.
330
331 Now we saw above how to define `map` in terms of `fold_right`. In Kapulet syntax, `map g xs` was:
332
333     fold_right ((lambda (x, zs). g x & zs), []) xs
334
335 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:
336
337     map g xs
338
339 in Kapulet syntax, turns into this in our lambda evaluator:
340
341     let empty = \f z. z in
342     let cons = \d ds. \f z. f d (ds f z) in
343     xs (\x zs. cons (g x) zs) empty
344
345 Try out this:
346
347     let empty = \f z. z in
348     let cons = \d ds. \f z. f d (ds f z) in
349     let map = \g xs. xs (\x zs. cons (g x) zs) empty in
350     let abc = \f z. f a (f b (f c z)) in
351     map g abc
352
353 That will evaluate to:
354
355     \f z. f (g a) (f (g b) (f (g c) z))
356
357 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 arguments over `[g a, g b, g c]`, which is `map g [a, b, c]`.
358
359
360 <a id=numbers></a>
361 ## Numbers ##
362
363 Armed with the encoding we developed for lists above, Church's method for encoding numbers in the Lambda Calculus is very natural. But this is not the order that these ideas were historically developed.
364
365 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.
366
367 The idea here is that a number is something like a list, only without any slot for an interesting, possibly varying head element at each level. Whereas in a list like:
368
369     [a, b, c]
370
371 we have:
372
373     head=a, sublist=(head=b, sublist=(head=c, sublist=[]))
374
375 with the number `3` we instead only have:
376
377     head=(), subnumber=(head=(), subnumber=(head=(), subnumber=zero))
378
379 where `()` is the zero-length tuple, the one and only member of its type. That is, the head here is a type of thing that cannot interestingly vary. Or we could just eliminate the head, and have:
380
381     subnumber=(subnumber=(subnumber=zero))
382
383 probably more familiar to you as:
384
385     succ (succ (succ zero))
386
387 In other words, where a list is inductively built up out of some interesting new datum and its "sublist" or tail, a number is inductively built up out of no interesting new datum and its "subnumber" or predecessor. In this light, a number can be seen as a kind of stunted or undernourished list.
388
389 Now, we had a strategy for encoding the list `[a, b, c]` as:
390
391     \f z. f a (f b (f c z))
392
393 So perhaps we can apply the same kind of idea to the number `3`, and encode it as:
394
395     \f z. f   (f   (f   z))
396
397 In fact, there's a way of looking at this that makes it look incredibly natural. You may have encountered the idea of a composition of two functions `f` and `g`, written as <code>f &cir; g</code>, or in Kapulet as `f comp g`. This is defined to be:
398
399     \x. f (g x)
400
401 For example, the operation that maps a number `n` to <code>n<sup>2</sup>+1</code> is the composition of the successor function and the squaring function (first we square, then we take the successor).
402
403 The composition of a function `f` with itself, namely:
404
405     \x. f (f x)
406
407 is sometimes abbreviated as <code>f<sup>2</sup></code>. Similarly, <code>f &cir; f &cir; f</code> or `\x. f (f (f x))` is sometimes abbreviated as <code>f<sup>3</sup></code>. <code>f<sup>1</sup></code> is understood to be just `f` itself, and <code>f<sup>0</sup></code> is understood to be the identity function.
408
409 So in proposing to encode the number `3` as:
410
411     \f z. f   (f   (f   z))
412
413 we are proposing to encode it as:
414
415 <code>\f z. f<sup>3</sup> z</code>
416
417 (The <code>f<sup><em>n</em></sup></code> isn't some bit of new Lambda Calculus syntax. It's just our metalanguage abbreviation for the same expressions we had before. It does help focus our attention on what we're essentially doing here.)
418
419 And indeed this is the Church encoding of the numbers:
420
421 <code>0 &equiv; \f z. z &nbsp;&nbsp;;  <~~> \f z. I z, or \f z. f<sup>0</sup> z</code>  
422 <code>1 &equiv; \f z. f z &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;;  or \f z. f<sup>1</sup> z</code>  
423 <code>2 &equiv; \f z. f (f z) &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;;  or \f z. f<sup>2</sup> z</code>  
424 <code>3 &equiv; \f z. f (f (f z)) &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;;  or \f z. f<sup>3</sup> z</code>  
425 <code>...</code>
426
427 The encoding for `0` is what we also proposed as the encoding for `[]` and for `false`. Don't read too much into this.
428
429 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.
430
431 We saw that using the `cons` operation (Kapulet's `&`) and `[]` as arguments to `fold_right` over a list give us back that very same list. In the Lambda Calculus, that comes to the following:
432
433     [a, b, c] cons []
434
435 with the appropriate lambda terms substituted throughout, just reduces to the same lambda term we used to encode `[a, b, c]`.
436
437 In the same spirit, what do you expect this will reduce to:
438
439     3 succ 0
440
441 Since `3` is `\f z. f (f (f z))`, it should reduce to whatever:
442
443     succ (succ (succ 0))
444
445 does. And if we define `succ` properly, we should expect that to give us the same lambda term that we used to encode `3` in the first place.
446
447
448 We'll look at other encodings of lists and numbers later.