--- /dev/null
+#Version 4 lists: Efficiently extracting tails#
+
+Version 3 lists and Church numerals are lovely, because they have their recursive capacity built into their very bones. However, one disadvantage
+to them is that it's relatively inefficient to extract a list's tail, or get a
+number's predecessor. To get the tail of the list `[a;b;c;d;e]`, one will
+basically be performing some operation that builds up the tail afresh: at
+different stages, one will have built up `[e]`, then `[d;e]`, then `[c;d;e]`, and
+finally `[b;c;d;e]`. With short lists, this is no problem, but with longer lists
+it takes longer and longer. And it may waste more of your computer's memory
+than you'd like. Similarly for obtaining a number's predecessor.
+
+The v1 lists and numbers on the other hand, had the tail and the predecessor
+right there as an element, easy for the taking. The problem was just that the
+v1 lists and numbers didn't have recursive capacity built into them, in the
+way the v3 implementations do.
+
+A clever approach would marry these two strategies.
+
+Version 3 makes the list `[a;b;c;d;e]` look like this:
+
+ \f z. f a (f b (f c (f d (f e z))))
+
+or in other words:
+
+ \f z. f a <the result of folding f and z over the tail>
+
+Instead we could make it look like this:
+
+ \f z. f a <the tail itself> <the result of folding f and z over the tail>
+
+That is, now `f` is a function expecting *three* arguments: the head of the
+current list, the tail of the current list, and the result of continuing to
+fold `f` over the tail, with a given base value `z`.
+
+Call this a **version 4** list. The empty list can be the same as in v3:
+
+<pre><code>empty ≡ \f z. z</code></pre>
+
+The list constructor would be:
+
+<pre><code>make_list ≡ \h t. \f z. f h t (t f z)</code></pre>
+
+It differs from the version 3 `make_list` only in adding the extra argument
+`t` to the new, outer application of `f`.
+
+Similarly, `five` as a v3 or Church numeral looks like this:
+
+ \s z. s (s (s (s (s z))))
+
+or in other words:
+
+ \s z. s <the result of applying s to z (pred 5)-many times>
+
+Instead we could make it look like this:
+
+ \s z. s <pred 5> <the result of applying s to z (pred 5)-many times>
+
+That is, now `s` is a function expecting *two* arguments: the predecessor of the
+current number, and the result of continuing to apply `s` to the base value `z`
+predecessor-many times.
+
+Jim had the pleasure of "inventing" these implementations himself. However,
+unsurprisingly, he wasn't the first to do so. See for example [Oleg's report
+on P-numerals](http://okmij.org/ftp/Computation/lambda-calc.html#p-numerals).
+
+