Assume Ω has type τ, and `\x.xx` has type σ. Then
because `\x.xx` takes an argument of type σ and returns
-something of type τ, `\x.xx` must also have type `σ -->
-τ`. By repeating this reasoning, `\x.xx` must also have type
-`(σ --> τ) --> τ`; and so on. Since variables have
+something of type τ, `\x.xx` must also have type σ -->
+τ. By repeating this reasoning, `\x.xx` must also have type
+(σ --> τ) --> τ; and so on. Since variables have
finite types, there is no way to choose a type for the variable `x`
that can satisfy all of the requirements imposed on it.
Version 1 type numerals are not a good choice for the simply-typed
lambda calculus. The reason is that each different numberal has a
different type! For instance, if zero has type σ, then `false`
-has type τ --> τ --> &tau, for some τ. Since one is
-represented by the function `\x.x false 0`, one must have type `(τ
---> τ --> &tau) --> &sigma --> σ`. But this is a different
+has type τ --> τ --> τ, for some τ. Since one is
+represented by the function `\x.x false 0`, one must have type (τ
+--> τ --> τ) --> σ --> σ. But this is a different
type than zero! Because each number has a different type, it becomes
impossible to write arithmetic operations that can combine zero with
one. We would need as many different addition operations as we had
pairs of numbers that we wanted to add.
Fortunately, the Church numberals are well behaved with respect to
-types. They can all be given the type `(σ --> σ) -->
-σ --> σ`.
+types. They can all be given the type (σ --> σ) -->
+σ --> σ.