lists.mdwn

   1 (list?)
   2 nil
   3 cons
   4 nil?, (pair?)
   5 head
   6 tail
   7
   8 Chris's lists:
   9         nil = (t,N)  = \f. f true N
  10         [a] = (f,(a,nil))
  11         [b,a] = (f,(b,[a]))
  12
  13 isnil = get-first
  14 head = L get-second get-first
  15 tail = L get-second get-second
  16
  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)
  20         e.g. N = K (t,N)
  21                    = (\n. K (t,n)) N
  22         How to do that?
  23         a fixed point g_ of g : g_ = (g g_)
  24         (Y g) = g (Y 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
  27
  28         i.e. N = Y g = Y (\n. K (t,n))
  29         and nil = (t, N) = (t, Y (\n. K (t, n)))
  30
  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 ~~>
  35                 (t, Y (\n. K (t,n)))
  36
  37
  38 Lists 2:
  39         nil = false
  40         [a] = (a,nil)
  41
  42 L (\h\t.K deal_with_h_and_t) if-nil
  43
  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>
  46
  47 could handle like this:
  48         the-value if-red if-green (\n. handler-if-blue-to-degree-n)
  49
  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
  53
  54 A list is basically: empty | non-empty <head,tail>
  55
  56                 empty = \non-empty-handler \if-empty. if-empty = false
  57                 cons = \h \t. \non-empty-handler \if-empty. non-empty-handler h t
  58
  59                 so [a] = cons a empty = \non-empty-handler \_. non-empty-handler a empty
  60
  61
  62
  63 Lists 3:
  64 [a; tl] isnil == (\f. f a tl) (\h \t.false) a b ~~> false a b
  65
  66 nil isnil == (\f. M) (\h \t. false) a b ~~> M[f:=isnil] a b == a
  67
  68         so M could be \a \b. a, i.e. true
  69         so nil = \f. true == K true == K K = \_ K
  70
  71         nil = K true
  72         [a] = (a,nil)
  73         [b,a] = (b,[a])
  74
  75 isnil = (\x\y.false)
  76
  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.
  79
  80