(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
would be nice if nil tail = nil
nil tail = (t, N) get-second get-second = N get-second
so N get-second should be (t,N)
e.g. N = K (t,N)
= (\n. K (t,n)) N
How to do that?
a fixed point g_ of g : g_ = (g g_)
(Y g) = g (Y g)
N = (\n. K (t,n)) N is of the form N = g N
So if we just set N = Y g, we'll have what we want. N = (Y g) = g (Y g) = g N
i.e. N = Y g = Y (\n. K (t,n))
and nil = (t, N) = (t, Y (\n. K (t, n)))
nil get-second get-second ~~>
Y (\n. K (t, n)) get-second ~~>
(\n. K (t, n)) (Y (\n. K (t,n))) get-second ~~>
K (t, Y (\n. K (t,n))) get-second ~~>
(t, Y (\n. K (t,n)))
Lists 2:
nil = false
[a] = (a,nil)
L (\h\t.K deal_with_h_and_t) if-nil
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
could handle like this:
the-value if-red if-green (\n. handler-if-blue-to-degree-n)
then red = \r \g \b-handler. r
green = \r \g \b-handler. g
make-blue = \degree. \r \g \b-handler. b-handler degree
A list is basically: empty | non-empty
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.