9 nil = (t,N) = \f. f true N
14 head = L get-second get-first
15 tail = L get-second get-second
17 would be nice if nil tail = nil
18 nil tail = (t, N) get-second get-second = N get-second
19 so N get-second should be (t,N)
23 a fixed point g_ of g : g_ = (g g_)
25 N = (\n. K (t,n)) N is of the form N = g N
26 So if we just set N = Y g, we'll have what we want. N = (Y g) = g (Y g) = g N
28 i.e. N = Y g = Y (\n. K (t,n))
29 and nil = (t, N) = (t, Y (\n. K (t, n)))
31 nil get-second get-second ~~>
32 Y (\n. K (t, n)) get-second ~~>
33 (\n. K (t, n)) (Y (\n. K (t,n))) get-second ~~>
34 K (t, Y (\n. K (t,n))) get-second ~~>
42 L (\h\t.K deal_with_h_and_t) if-nil
44 We've already seen enumerations: true | false, red | green | blue
45 What if you want one or more of the elements to have associated data? e.g. red | green | blue <how-blue>
47 could handle like this:
48 the-value if-red if-green (\n. handler-if-blue-to-degree-n)
50 then red = \r \g \b-handler. r
51 green = \r \g \b-handler. g
52 make-blue = \degree. \r \g \b-handler. b-handler degree
54 A list is basically: empty | non-empty <head,tail>
56 empty = \non-empty-handler \if-empty. if-empty = false
57 cons = \h \t. \non-empty-handler \if-empty. non-empty-handler h t
59 so [a] = cons a empty = \non-empty-handler \_. non-empty-handler a empty
64 [a; tl] isnil == (\f. f a tl) (\h \t.false) a b ~~> false a b
66 nil isnil == (\f. M) (\h \t. false) a b ~~> M[f:=isnil] a b == a
68 so M could be \a \b. a, i.e. true
69 so nil = \f. true == K true == K K = \_ K
77 nil tail = K true tail = true = \x\y.x = \f.f? such that f? = Kx. there is no such.
78 nil head = K true head = true. could mislead.