Is leastness important?
-##The simply-typed lambda calculus##
-
-The uptyped lambda calculus is pure computation. It is much more
-common, however, for practical programming languages to be typed.
-Likewise, systems used to investigate philosophical or linguistic
-issues are almost always typed. Types will help us reason about our
-computations. They will also facilitate a connection between logic
-and computation.
-
-Soon we will consider polymorphic type systems. First, however, we
-will consider the simply-typed lambda calculus. There's good news and
-bad news: the good news is that the simply-type lambda calculus is
-strongly normalizing: every term has a normal form. We shall see that
-self-application is outlawed, so Ω can't even be written, let
-alone undergo reduction. The bad news is that fixed-point combinators
-are also forbidden, so recursion is neither simple nor direct.
-
-#Types#
-
-We will have at least one ground type, `o`. From a linguistic point
-of view, think of the ground types as the bar-level 0 categories, that
-is, the lexical types, such as Noun, Verb, Preposition (glossing over
-the internal complexity of those categories in modern theories).
-
-In addition, there will be a recursively-defined class of complex
-types `T`, the smallest set such that
-
-* ground types, including `o`, are in `T`
-
-* for any types σ and τ in `T`, the type σ -->
- τ is in `T`.
-
-For instance, here are some types in `T`:
-
- o
- o --> o
- o --> o --> o
- (o --> o) --> o
- (o --> o) --> o --> o
-
-and so on.
-
-#Typed lambda terms#
-
-Given a set of types `T`, we define the set of typed lambda terms <code>Λ_T</code>,
-which is the smallest set such that
-
-* each type `t` has an infinite set of distinct variables, {x^t}_1,
- {x^t}_2, {x^t}_3, ...
-
-* If a term `M` has type σ --> τ, and a term `N` has type
- σ, then the application `(M N)` has type τ.
-
-* If a variable `a` has type σ, and term `M` has type τ,
- then the abstract <code>λ a M</code> has type σ --> τ.
-
-The definitions of types and of typed terms should be highly familiar
-to semanticists, except that instead of writing σ --> τ,
-linguists (following Montague, who followed Church) write <σ,
-τ>. We will use the arrow notation, since it is more iconic.
-
-Some examples (assume that `x` has type `o`):
-
- x o
- \x.x o --> o
- ((\x.x) x) o
-
-Excercise: write down terms that have the following types:
-
- o --> o --> o
- (o --> o) --> o --> o
- (o --> o --> o) --> o
-
-#Associativity of types versus terms#
-
-As we have seen many times, in the lambda calculus, function
-application is left associative, so that `f x y z == (((f x) y) z)`.
-Types, *THEREFORE*, are right associative: if `f`, `x`, `y`, and `z`
-have types `a`, `b`, `c`, and `d`, respectively, then `f` has type `a
---> b --> c --> d == (a --> (b --> (c --> d)))`.
-
-It is a serious faux pas to associate to the left for types. You may
-as well use your salad fork to stir your tea.
-
-#The simply-typed lambda calculus is strongly normalizing#
-
-If `M` is a term with type τ in Λ_T, then `M` has a
-normal form. The proof is not particularly complex, but we will not
-present it here; see Berendregt or Hankin.
-
-Since Ω does not have a normal form, it follows that Ω
-cannot have a type in Λ_T. We can easily see why:
-
- Ω = (\x.xx)(\x.xx)
-
-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
-finite types, there is no way to choose a type for the variable `x`
-that can satisfy all of the requirements imposed on it.
-
-In general, there is no way for a function to have a type that can
-take itself for an argument. It follows that there is no way to
-define the identity function in such a way that it can take itself as
-an argument. Instead, there must be many different identity
-functions, one for each type.
-
-#Typing numerals#
-
-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 τ --> τ --> τ, 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 (σ --> σ) -->
-σ --> σ.
-