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`
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`
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
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