+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 (σ -> σ) -> σ
+-> σ.
+
+<!-- Make sure there is talk about unification and computation of the
+principle type-->
+
+## 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.,
+<code>N ≡ (σ -> σ) -> σ -> σ</code> 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, <code>pair ≡ (N -> N -> N) -> N</code>. 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 <code>(σ
+-> σ) -> σ -> σ</code>. This means that the type of
+`collect` has to match <code>σ -> σ</code>. But we
+concluded above that the type of `collect` also had to be `pair ->
+pair`. Putting these constraints together, it appears that
+<code>σ</code> 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
+<code>σ</code>. If <code>σ</code> turns out to depend on
+`N`, and `N` depends in turn on <code>σ</code>, then
+<code>σ</code> 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 built-in
+right-fold structure of the Church numbers to recursively walk down
+the spine of its argument. In order to do that, the argument had to
+apply to the `collect` operation. And since `collect` had to be the
+sort of operation that manipulates numbers, 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.
+
+Because lists are (in effect) a generalization of the Church numbers,
+computing the tail of a list is likewise beyond the reach of the
+simply-typed lambda calculus.
+
+This result is surprising. It illustrates how recursion is built into
+the structure of the Church numbers (and lists). Most importantly for
+the discussion of the simply-typed lambda calculus, it demonstrates
+that even fairly basic recursive computations are beyond the reach of
+a simply-typed system.
+
+
+## Montague grammar is a simply-typed
+
+Systems based on the simply-typed lambda calculus are the bread and
+butter of current linguistic semantic analysis. One of the most
+influential modern semantic formalisms---Montague's PTQ
+fragment---involved a simply-typed version of the Predicate Calculus
+with lambda abstraction. More specifically, Montague called the
+semantic part of the PTQ fragment `Intensional Logic'. Montague's IL
+had three base types: `e`, for individuals, `t`, for truth values, and
+`s` for evaluation indicies (world-time pairs). The set of types was
+defined recursively:
+
+ e, t, s are types
+ if a and b are types, <a,b> is a type
+ if a is a type, <s,a> is a type
+
+So `<e,<e,t>>` and `<s,<<s,e>,t>>` are types, but `<e,s>` is not a
+type. As mentioned, this paper is the source for the convention in
+linguistics that a type of the form `<a, b>` corresponds to a
+functional type that we will write `a -> b`.
+
+Montague gave rules for the types of various logical formulas. Of
+particular interest here, he gave the following typing rules for
+functional application and for lambda abstracts:
+
+* If *α* is an expression of type *a*, and *β* is an
+expression of type b, then *α(β)* has type *b*.
+* If *α* is an expression of type *a*, and *u* is a variable of
+type *b*, then *λuα* has type <code><b, a></code>.
+
+In future discussions about monads, we will investigate Montague's
+treatment of intensionality in some detail. In the meantime,
+Montague's PTQ fragment is responsible for making the simply-typed
+lambda calculus the baseline semantic analysis for linguistics.