`Λ_T`

,
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 `λ a M`

has type σ -> τ.
The definitions of types and of typed terms should be highly familiar
to semanticists, except that instead of writing σ -> τ,
linguists 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 `x`, `y`, and `z`
have types `a`, `b`, and `c`, respectively, then `f` has type
`a -> b -> c -> d == (a -> (b -> (c -> d)))`, where `d` is the
type of the complete term.
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. Some of those types can be functions,
and some of those functions can be (type-restricted) identity
functions; but a simply-types identity function can never apply to itself.
#Typing numerals#
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 ρ -> σ -> σ 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 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 examinining the definition of two, we
see that expressions of type τ must be suitable to serve as
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 (σ -> σ) -> σ
-> σ.
## Predecessor and lists are not representable in simply typed lambda-calculus ##
As Oleg Kiselyov points out, [[predecessor and lists can't be
represented in the simply-typed lambda
calculus|http://okmij.org/ftp/Computation/lambda-calc.html#predecessor]].
This is not because there is any difficulty typing what the functions
involved do "from the outside": for instance, the predecessor function
is a function from numbers to numbers, or τ -> τ, where τ
is our type for Church numbers (i.e., (σ -> σ) -> σ
-> σ). (Though this type will only be correct if we decide that
the predecessor of zero should be a number, perhaps zero.)
Rather, the problem is that the definition of the function requires
subterms that can't be simply-typed. We'll illustrate with our
implementation of the predecessor, sightly modified in inessential
ways to suit present purposes:
let zero = \s z. z in
let snd = \a b. b in
let pair = \a b. \v. v a b in
let succ = \n s z. s (n s z) in
let collect = \p. p (\a b. pair (succ a) a)
let pred = \n. n collect (pair zero zero) snd in
Let's see how far we can get typing these terms. `zero` is the Church
encoding of zero. Using `N` as the type for Church numbers (i.e.,
`N == (σ -> σ) -> σ -> σ`

for some
σ, `zero` has type `N`. `snd` takes two numbers, and returns
the second, so `snd` has type `N -> N -> N`. Then the type of `pair`
is `N -> N -> (type(snd)) -> N`, that is, `N -> N -> (N -> N -> N) ->
N`. Likewise, `succ` has type `N -> N`, and `collect` has type `pair
-> pair`, where `pair` is the type of an ordered pair of numbers,
namely, `pair ≡ (N -> N -> N) -> N`

. So far so good.
The problem is the way in which `pred` puts these parts together. In
particular, `pred` applies its argument, the number `n`, to the
`collect` function. Since `n` is a number, its type is `(σ ->
σ) -> σ -> σ`. This means that the type of
`collect` has to match `σ -> σ`. But we concluded above
that the type of `collect` also had to be `pair -> pair`. Putting
these constraints together, it appears that `σ` must be the type
of a pair of numbers. But we already decided that the type of a pair
of numbers is `(N -> N -> N) -> N`. Here's the difficulty: `N` is
shorthand for a type involving `σ`. If `σ` turns out to
depend on `N`, and `N` depends in turn on `σ`, then `σ` is a proper
subtype of itself, which is not allowed in the simply-typed lambda
calculus.
The way we got here is that the pred function relies on the right-fold
structure of the Church numbers to recursively walk down the spine of
its argument. In order to do that, the argument number had to take
the operation in question as its first argument. And the operation
required in order to build up the predecessor must be the sort of
operation that manipulates numbers, and the infinite regress is
established.
Now, of course, this is only one of myriad possible implementations of
the predecessor function in the lambda calculus. Could one of them
possibly be simply-typeable? It turns out that this can't be done.
See the works cited by Oleg for details.