The Church numerals are well behaved with respect to types. They can
all be given the type (σ --> σ) --> σ --> σ.
+## Predecessor and lists are not representable in simply typed lambda-calculus ##
+As Oleg Kiselyov points out, [[predecessor and lists can't be
+represented in the simply-typed lambda
+calculus|http://okmij.org/ftp/Computation/lambda-calc.html#predecessor]].
+The reason is that ...
+Need to digest the following, which is quoted from Oleg's page:
-## Predecessor and lists are not representable in simply typed lambda-calculus ##
The predecessor of a Church-encoded numeral, or, generally, the encoding of a list with the car and cdr operations are both impossible in the simply typed lambda-calculus. Henk Barendregt's ``The impact of the lambda-calculus in logic and computer science'' (The Bulletin of Symbolic Logic, v3, N2, June 1997) has the following phrase, on p. 186:
Lists can also be represented in System F. As a matter of fact, we do not need the full System F (where the type reconstruction is not decidable). We merely need the extension of the Hindley-Milner system with higher-ranked types, which requires a modicum of type annotations and yet is able to infer the types of all other terms. This extension is supported in Haskell and OCaml. With such an extension, we can represent a list by its fold, as shown in the code below. It is less known that this representation is faithful: we can implement all list operations, including tail, drop, and even zip.
-See also [[Oleg Kiselyov on the predecessor function in the lambda
-calculus|http://okmij.org/ftp/Computation/lambda-calc.html#predecessor]].