#Typing numerals#
-The Church numerals are well behaved with respect to types. They can
-all be given the type (σ --> σ) --> σ --> σ.
+The Church numerals are well behaved with respect to types.
+To see this, consider the first three Church numerals (starting with zero):
+
+ \s z . z
+ \s z . s z
+ \s z . s (s z)
+
+Given the internal structure of the term we are using to represent
+zero, its type must have the form ρ --> σ --> $sigma; for
+some ρ and σ. This type is consistent with term for one,
+but the structure of the definition of one is more restrictive:
+because the first argument `s` must apply to the second argument `z`,
+the type of the first argument must describe a function from
+expressions of type σ to some other type. So we can refine ρ
+by replacing it with the more specific type σ --> τ. At
+this point, the overall type is (σ --> τ) --> σ -->
+σ. Note that this refined type remains compatible with the
+definition of zero. Finally, by examinine the definition of two, we
+see that expressions of type τ must be suitable to serve as
+arguments to functions of type σ --> τ. The most general
+way for that to be true is if τ ≡ σ. So at this
+point, we have the overall type of (σ --> σ) --> σ -->
+σ.
+
+
## Predecessor and lists are not representable in simply typed lambda-calculus ##