\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
+zero, its type must have the form ρ --> σ --> σ 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 (σ --> τ) --> σ -->
+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 result 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
+definition of zero. Finally, by examinining the definition of two, we
see that expressions of type τ must be suitable to serve as
-arguments to functions of type σ --> τ. The most general
+arguments to functions of type σ --> τ, since the result of
+applying `s` to `z` serves as the argument of `s`. The most general
way for that to be true is if τ ≡ σ. So at this
-point, we have the overall type of (σ --> σ) --> σ -->
-σ.
-
+point, we have the overall type of (σ --> σ) --> σ
+--> σ.
+<!-- Make sure there is talk about unification and computation of the
+principle type-->
## Predecessor and lists are not representable in simply typed lambda-calculus ##