+[[!toc]]
+
Building Lists
==============
To build a data-structure, you begin by deciding what the data-structure needs to do. When we built booleans, what they needed to do was select between two choices. When we built ordered pairs, what we needed was a way to wrap two elements into the pair, and ways to operate on the wrapped elements, especially a way to extract a specified one of them.
-Now we're going to try to build lists. First, let's explain what is the difference bwteen a list and a pair.
+Now we're going to try to build lists. First, let's explain what is the difference between a list and a pair.
-A list can two elements, but it can also have more elements, or fewer. A list can even have zero elements: this is called the empty list. Sometimes this is written `nil`. In Scheme it's also written `'()` and `(list)`, and in OCaml it's written `[]`. Those languages are nice and have list structures pre-built into them. But we're going to build lists ourselves, from scratch.
+A list can have two elements, but it can also have more elements, or fewer. A list can even have zero elements: this is called the empty list. Sometimes this is written `nil`. In Scheme it's also written `'()` and `(list)`, and in OCaml it's written `[]`. Those languages are nice and have list structures pre-built into them. But we're going to build lists ourselves, from scratch.
OK, so a list doesn't have to have two elements, but still, what's the difference between a two-element list and a pair? And the difference between a three-element list and a triple?
We regard two pairs as being of the same type when their corresponding members are of the same type.
+Some programming languages permit type-heterogenous lists. Some imperative languages further permit a kind of *mutable* list. We'll consider such things later. For now, we regard these as frills. What we're discussing here is just the prototypical, meat-and-potatoes list.
+
Another difference between lists and pairs:
* The length of a list is not essential to its type. A two-element list can be of the same type as a three-element list (whose members are of the right type).
Adding *m* to *n* is a matter of applying the successor function to *n* *m* times. And we know how to apply an arbitrary function s to *n* *m* times: we just give that function s, and the base-value *n*, to *m* as arguments. Because that's what the function we're using to implement *m* *does*. Hence **add** can be defined to be, simply:
- \m \n. m succ n
+ \m n. m succ n
Isn't that nice?
+Alternatively, one could do:
+
+ \m n. \s z. m s (n s z)
+
How would we tell whether a number was 0? Well, look again at the implementations of the first few numbers:
<pre><code>zero ≡ \s z. s<sup>0</sup> z ≡ \s z. z
Multiplication is even more elegant. Consider that applying an arbitrary function s to a base value z *m × n* times is a matter of applying s to z *n* times, and then doing that again, and again, and so on...for *m* repetitions. In other words, it's a matter of applying the function (\z. n s z) to z *m* times. In other words, *m × n* can be represented as:
- \s z. m (\z. n s z) z
- ~~> \s z. m n s z
-
-which eta-reduces to:
-
- m n
-
-Isn't that nice?
-
-However, at this point the elegance gives out. The predecessor function is substantially more difficult to construct on this implementation. As with all of these operations, there are several ways to do it, but they all take at least a bit of ingenuity. If you're only first learning programming right now, it would be unreasonable to expect you to be able to figure out how to do it.
-
-However, if on the other hand you do have some experience programming, consider how you might construct a predecessor function for numbers implemented in this way. Using only the resources we've so far discussed. (So you have no general facility for performing recursion, for instance.)
-
-
-
-
-
-
-(list?)
-nil
-cons
-nil?, (pair?)
-head
-tail
-
-Chris's lists:
- nil = (t,N) = \f. f true N
- [a] = (f,(a,nil))
- [b,a] = (f,(b,[a]))
-
-isnil = get-first
-head = L get-second get-first
-tail = L get-second get-second
-
-
-
-Lists 2:
- nil = false
- [a] = (a,nil)
+ \s z. m (\z. n s z) z
-L (\h\t.K deal_with_h_and_t) if-nil
+which can be eta-reduced to:
-We've already seen enumerations: true | false, red | green | blue
-What if you want one or more of the elements to have associated data? e.g. red | green | blue <how-blue>
+ \s. m (n s)
-could handle like this:
- the-value if-red if-green (\n. handler-if-blue-to-degree-n)
+and we might abbreviate that as:
- then red = \r \g \b-handler. r
- green = \r \g \b-handler. g
- make-blue = \degree. \r \g \b-handler. b-handler degree
+<pre><code>m ∘ n</code></pre>
-A list is basically: empty | non-empty <head,tail>
- empty = \non-empty-handler \if-empty. if-empty = false
- cons = \h \t. \non-empty-handler \if-empty. non-empty-handler h t
-
- so [a] = cons a empty = \non-empty-handler \_. non-empty-handler a empty
-
-
-
-Lists 3:
-[a; tl] isnil == (\f. f a tl) (\h \t.false) a b ~~> false a b
-
-nil isnil == (\f. M) (\h \t. false) a b ~~> M[f:=isnil] a b == a
-
- so M could be \a \b. a, i.e. true
- so nil = \f. true == K true == K K = \_ K
-
- nil = K true
- [a] = (a,nil)
- [b,a] = (b,[a])
-
-isnil = (\x\y.false)
-
-nil tail = K true tail = true = \x\y.x = \f.f? such that f? = Kx. there is no such.
-nil head = K true head = true. could mislead.
-
-
-
-Church figured out how to encode integers and arithmetic operations
-using lambda terms. Here are the basics:
-
-0 = \f\x.fx
-1 = \f\x.f(fx)
-2 = \f\x.f(f(fx))
-3 = \f\x.f(f(f(fx)))
-...
-
-Adding two integers involves applying a special function + such that
-(+ 1) 2 = 3. Here is a term that works for +:
-
-+ = \m\n\f\x.m(f((n f) x))
-
-So (+ 0) 0 =
-(((\m\n\f\x.m(f((n f) x))) ;+
- \f\x.fx) ;0
- \f\x.fx) ;0
-
-~~>_beta targeting m for beta conversion
-
-((\n\f\x.[\f\x.fx](f((n f) x)))
- \f\x.fx)
+Isn't that nice?
-\f\x.[\f\x.fx](f(([\f\x.fx] f) x))
+And if we *apply* `m` to `n` instead of composing it, we get a implementation of exponentiation.
-\f\x.[\f\x.fx](f(fx))
+However, at this point the elegance gives out. The predecessor function is substantially more difficult to construct on this implementation. As with all of these operations, there are several ways to do it, but they all take at least a bit of ingenuity. If you're only first learning programming right now, it would be unreasonable to expect you to be able to figure out how to do it.
-\f\x.\x.[f(fx)]x
+However, if on the other hand you do have some experience programming, consider how you might construct a predecessor function for numbers implemented in this way. Using only the resources we've so far discussed. (So you have no general facility for performing recursion, for instance.)
-\f\x.f(fx)
+Lists, version 3
+----------------
+It's possible to follow the same design for implementing lists, too. To see this, let's first step back and consider some of the more complex things you might do with a list. We don't need to think specifically inside the confines of the lambda calculus right now. These are general reflections.
+Assume you have a list of five integers, which I'll write using the OCaml notation: `[1; 2; 3; 4; 5]`.
+Now one thing you might want to do with the list is to double every member. Another thing you might want to do is to increment every number. More generally, given an arbitrary function `f`, you might want to get the list which is `[f 1; f 2; f 3; f 4; f 5]`. Computer scientists call this **mapping** the function `f` over the list `[1; 2; 3; 4; 5]`.
+Another thing you might want to do with the list is to retrieve every member which is even. Or every member which is prime. Or, given an arbitrary function f, you might want to **filter** the original list to a shorter list containing only those elements `x` for which `f x` evaluates to true.
+These are very basic, frequently-used operations on lists.
+Another operation on lists is a bit harder to get a mental hold of, but is even more fundamental than the two just mentioned. An example of this operation would be if you were to **sum up** the members of the list. What would you do? We'll you'd start with the first element of the list. Actually, for generality, let's say you start with a *seed value*. In this case the seed value can be 0. Then you take the first element of the list and add it to the seed value. Now you have 1. You take the second element of the list, and add it to the result so far. Now you have 3. You take the third element of the list, and add it to the result so far. And so on.
+This general form of operation is known as **folding** an operation---in this case, the addition operation---over the list. Addition is symmetric, so it doesn't matter whether you start at the left side of the list or the right. But we can't in general rely on the operations to be symmetric. So there are two notions. This is the **left-fold** of an operation f over our list `[1; 2; 3; 4; 5]` given a seed value z:
-let t = <<fun y _ -> y>>
-let f = <<fun _ n -> n>>
-let b = <<fun f g x -> f (g x)>>
-let k = << $t$ >>
-let get1 = << $t$ >>
-let get2 = << $f$ >>
-let id = <<fun x -> x>>
-let w = <<fun f -> f f>>
-let w' = <<fun f n -> f f n>>
-let pair = <<fun x y theta -> theta x y>>
+ f (f (f (f (f z 1) 2) 3) 4) 5
-let zero = <<fun s z -> z>>
-let succ = <<fun n s z -> s (n s z)>>
-let one = << $succ$ $zero$ >>
-let two = << $succ$ $one$ >>
-let three = << $succ$ $two$ >>
-let four = << $succ$ $three$ >>
-let five = << $succ$ $four$ >>
-let six = << $succ$ $five$ >>
-let seven = << $succ$ $six$ >>
-let eight = << $succ$ $seven$ >>
-let nine = << $succ$ $eight$ >>
+and this is the **right-fold**:
-(*
-let pred = <<fun n -> n (fun u v -> v (u $succ$)) ($k$ $zero$) $id$ >>
-*)
-let pred = <<fun n s z -> n (fun u v -> v (u s)) ($k$ z) $id$ >>
-(* ifzero n withp whenz *)
-let ifzero = <<fun n -> n (fun u v -> v (u $succ$)) ($k$ $zero$) (fun n' withp
-whenz -> withp n') >>
+ f 1 (f 2 (f 3 (f 4 (f 5 z))))
+
+Church's proposal for implementing the numbers identified the essential behavior of a number *m* to be applying an arbitary function s to a base value z *m* times. In a similar spirit, we can identify the essential behavior of a list to be folding an arbitrary operation f over the elements of the list and a seed value z. In other words, we could represent the list `[1; 2; 3; 4; 5]` as a function that accepted arbitrary `f` and `z` as arguments, and returned one of the folds above.
-let pred' =
- let iszero = << fun n -> n (fun _ -> $f$) $t$ >> in
- << fun n -> n ( fun f z' -> $iszero$ (f $one$) z' ($succ$ (f z')) ) ($k$ $zero$) $zero$ >>
+You could do this using either sort of fold, but choosing the right fold gives us an implementation closest to Church's encoding of the numbers. Then we'd define `[1; 2; 3; 4; 5]` to be:
-(*
- so n = zero ==> (k zero) zero
- n = one ==> f=(k zero) z'=zero ==> z' i.e. zero
- n = two ==> g(g (k zero)) zero
- f = g(k zero) z'=zero
- f = fun z'->z' z'=zero ==> succ (f z') = succ(zero)
- n = three ==> g(g(g (k zero))) zero
- f = g(g(k zero)) z'=zero
- f = fun z' -> succ(i z') z'=zero
- ==> succ (f z') ==> succ(succ(z'))
-*)
+ \f z. f 1 (f 2 (f 3 (f 4 (f 5 z))))
-let pred'' =
- let shift = (* <n,_> -> <n+1,n> *)
- <<fun d -> d (fun d1 _ -> $pair$ ($succ$ d1) d1) >> in
- <<fun n -> n $shift$ ($pair$ $zero$ $zero$) $get2$ >>
+Compare Church's definition of the number five:
+ \s z. s (s (s (s (s z))))
+This has real elegance, and it makes it easy to implement a number of primitive list operatioons. For example, checking whether a list implemented in this way is empty is easy. So too is extracting the head of a list known to be non-empty. However, other operations require some ingenuity. Extracting the tail of a list is about as difficult as retrieving the predecessor of a Church number. (This should not be surprising, given how similar in design these implementations are.)
-let add = <<fun m n -> n $succ$ m>>
-(* let add = <<fun m n -> fun s z -> m s (n s z) >> *)
-let mul = << fun m n -> n (fun z' -> $add$ m z') $zero$ >>
-
-
-(* we create a pairs-list of the numbers up to m, and take the
- * head of the nth tail. the tails are in the form (k tail), with
- * the tail of mzero being instead (id). We unwrap the content by:
- * (k tail) tail_of_mzero
- * or
- * (id) tail_of_mzero
- * we let tail_of_mzero be the mzero itself, so the nth predecessor of
- * zero will still be zero.
- *)
-
-let sub =
- let mzero = << $pair$ $zero$ $id$ >> in
- let msucc = << fun d -> d (fun d1 _ -> $pair$ ($succ$ d1) ($k$ d)) >> in
- let mtail = << fun d -> d $get2$ d >> in (* or could use d $get2$ $mzero$ *)
- <<fun m n -> n $mtail$ (m $msucc$ $mzero$) $get1$ >>
-
-let min' = <<fun m n -> $sub$ m ($sub$ m n) >>
-let max' = <<fun m n -> $add$ n ($sub$ m n) >>
-let lt' =
- let mzero = << $pair$ $zero$ $id$ >> in
- let msucc = << fun d -> d (fun d1 _ -> $pair$ ($succ$ d1) ($k$ d)) >> in
- let mtail = << fun d -> d $get2$ d >> in (* or could use d $get2$ $mzero$ *)
- <<fun n m -> n $mtail$ (m $msucc$ $mzero$) $get1$ (fun _ -> $t$) $f$ >>
-
-let leq' =
- let mzero = << $pair$ $zero$ $id$ >> in
- let msucc = << fun d -> d (fun d1 _ -> $pair$ ($succ$ d1) ($k$ d)) >> in
- let mtail = << fun d -> d $get2$ d >> in (* or could use d $get2$ $mzero$ *)
- <<fun m n -> n $mtail$ (m $msucc$ $mzero$) $get1$ (fun _ -> $f$) $t$ >>
-
-let eq' =
- (* like leq, but now we make mzero have a self-referential tail *)
- let mzero = << $pair$ $zero$ ($k$ ($pair$ $one$ $id$)) >> in
- let msucc = << fun d -> d (fun d1 _ -> $pair$ ($succ$ d1) ($k$ d)) >> in
- let mtail = << fun d -> d $get2$ d >> in (* or could use d $get2$ $mzero$ *)
- <<fun m n -> n $mtail$ (m $msucc$ $mzero$) $get1$ (fun _ -> $f$) $t$ >>
-
-(*
-let divmod' = << fun n d -> n
- (fun f' -> f' (fun d' m' ->
- $lt'$ ($succ$ m') d ($pair$ d' ($succ$ m')) ($pair$ ($succ$ d') $zero$)
- ))
- ($pair$ $zero$ $zero$) >>
-let div' = <<fun n d -> $divmod'$ n d $get1$ >>
-let mod' = <<fun n d -> $divmod'$ n d $get2$ >>
-*)
-
-let divmod' =
- let triple = << fun d1 d2 d3 -> fun sel -> sel d1 d2 d3 >> in
- let mzero = << $triple$ $succ$ ($k$ $zero$) $id$ >> in
- let msucc = << fun d -> $triple$ $id$ $succ$ ($k$ d) >> in
- let mtail = (* open in dhead *)
- << fun d -> d (fun dz mz df mf drest ->
- fun sel -> (drest dhead) (sel (df dz) (mf mz))) >> in
- << fun n divisor ->
- ( fun dhead -> n $mtail$ (fun sel -> dhead (sel $zero$ $zero$)) )
- (divisor $msucc$ $mzero$ (fun _ _ d3 -> d3 _))
- (fun dz mz _ _ _ -> $pair$ dz mz) >>
-
-let div' = <<fun n d -> $divmod'$ n d $get1$ >>
-let mod' = <<fun n d -> $divmod'$ n d $get2$ >>
-
-(*
- ISZERO = lambda n. n (lambda x. false) true,
-
- LE = lambda x. lambda y. ISZERO (MONUS x y),
- { ? x <= y ? }
-
- MONUS = lambda a. lambda b. b PRED a,
- {NB. assumes a >= b >= 0}
-
- DIVMOD = lambda x. lambda y.
- let rec dm = lambda q. lambda x.
- if LE y x then {y <= x}
- dm (SUCC q) (MONUS x y)
- else pair q x
- in dm ZERO x,
-*)
-
-(* f n =def. phi n_prev f_prev *)
-let bernays = <<fun phi z n -> n (fun d -> $pair$ (d (fun n_prev f_prev -> $succ$ n_prev)) (d phi)) ($pair$ $zero$ z) (fun n f -> f)>>
-
-
-(*
-let pred_b = << $bernays$ $k$ $zero$ >>
-let fact_b = << $bernays$ (fun x p -> $mul$ ($succ$ x) p) $one$ >>
-
-(* if m is zero, returns z; else returns withp (pred m) *)
-let ifzero = <<fun z withp m -> $bernays$ (fun x p -> withp x) z m>>
-let ifzero = <<fun z withp m -> m ($k$ (withp ($pred$ m))) z>>
-*)
-
-let y = <<fun f -> (fun u -> f (u u)) (fun u -> f (u u))>>
-(* strict y-combinator from The Little Schemer, Crockford's http://www.crockford.com/javascript/little.html *)
-let y' = <<fun f -> (fun u -> f (fun n -> u u n)) (fun u -> f (fun n -> u u n))>>
-(*
-let y'' = <<fun f -> (fun u n -> f (u u n)) (fun u n -> f (u u n))>>
-*)
-
-let turing = <<(fun u f -> f (u u f)) (fun u f -> f (u u f))>>
-let turing' = <<(fun u f -> f (fun n -> u u f n)) (fun u f -> f (fun n -> u u f n))>>
-
-
-let fact_w = << $w$ (fun f n -> $ifzero$ n (fun p -> $mul$ n (f f
-p)) $one$)>>
-let fact_w' = <<(fun f n -> f f n) (fun f n -> $ifzero$ n (fun p ->
- $mul$ n (f f p)) $one$)>>
-let fact_w'' = let u = <<(fun f n -> $ifzero$ n (fun p -> $mul$ n (f f
-p)) $one$)>> in <<fun n -> $u$ $u$ n>>
-
-let fact_y = << $y$ (fun f n -> $ifzero$ n (fun p -> $mul$ n (f p)) $one$)>>
-let fact_y' = << $y'$ (fun f n -> $ifzero$ n (fun p -> $mul$ n (f p)) $one$)>>
-
-let fact_turing = << $turing$ (fun f n -> $ifzero$ n (fun p -> $mul$ n (f p)) $one$)>>
-let fact_turing' = << $turing'$ (fun f n -> $ifzero$ n (fun p -> $mul$ n (f p)) $one$)>>
-
-
-
-let zero_ = <<fun s z -> z>>;;
-let succ_ = <<fun m s z -> s m (m s z)>>;;
-let one_ = << $succ_$ $zero_$ >>;;
-let two_ = << $succ_$ $one_$ >>;;
-let three_ = << $succ_$ $two_$ >>;;
-let four_ = << $succ_$ $three_$ >>;;
-let five_ = << $succ_$ $four_$ >>;;
-let six_ = << $succ_$ $five_$ >>;;
-let seven_ = << $succ_$ $six_$ >>;;
-let eight_ = << $succ_$ $seven_$ >>;;
-let nine_ = << $succ_$ $eight_$ >>;;
-
-let pred_ = <<fun n -> n (fun n' _ -> n') $zero_$ >>
-let add_ = <<fun m n -> n (fun _ f' -> $succ_$ f') m>>
-let mul_ = <<fun m n -> n (fun _ f' -> $add_$ m f') $zero_$ >>
-(* let pow_ = *)
-
-let sub_ = <<fun m n -> n (fun _ f' -> $pred_$ f') m>>
-let min_ = <<fun m n -> $sub_$ m ($sub_$ m n)>> (* m-max(m-n,0) = m+min(n-m,0) = min(n,m) *)
-let max_ = <<fun m n -> $add_$ n ($sub_$ m n)>> (* n+max(m-n,0) = max(m,n) *)
-
-let eq_ = <<fun m -> m (fun _ fm' n -> n (fun n' _ -> fm' n') $f$) (fun n -> n (fun _ _ -> $f$) $t$)>>
-let lt_ = <<fun m n -> ($sub_$ n m) (fun _ _ -> $t$) $f$ >>
-let leq_ = << fun m n -> ($sub_$ m n) (fun _ _ -> $f$) $t$ >>
-
-let divmod_ = << fun n d -> n
- (fun _ f' -> f' (fun d' m' ->
- $lt_$ ($succ_$ m') d ($pair$ d' ($succ_$ m')) ($pair$ ($succ_$ d') $zero_$)
- ))
- ($pair$ $zero_$ $zero_$) >>
-let div_ = <<fun n d -> $divmod_$ n d $get1$ >>
-let mod_ = <<fun n d -> $divmod_$ n d $get2$ >>