+In fact, unlike in the simply-typed lambda calculus,
+it is even possible to give a type for ω in System F.
+
+<code>ω = λx:(∀α.α->α). x [∀α.α->α] x</code>
+
+In order to see how this works, we'll apply ω to the identity
+function.
+
+<code>ω id ≡ (λx:(∀α.α->α). x [∀α.α->α] x) (Λα.λx:α.x)</code>
+
+Since the type of the identity function is `∀α.α->α`, it's the
+right type to serve as the argument to ω. The definition of
+ω instantiates the identity function by binding the type
+variable `α` to the universal type `∀α.α->α`. Instantiating the
+identity function in this way results in an identity function whose
+type is (in some sense, only accidentally) the same as the original
+fully polymorphic identity function.
+
+So in System F, unlike in the simply-typed lambda calculus, it *is*
+possible for a function to apply to itself!
+
+Does this mean that we can implement recursion in System F? Not at
+all. In fact, despite its differences with the simply-typed lambda
+calculus, one important property that System F shares with the
+simply-typed lambda calculus is that they are both strongly
+normalizing: *every* expression in either system reduces to a normal
+form in a finite number of steps.
+
+Not only does a fixed-point combinator remain out of reach, we can't
+even construct an infinite loop. This means that although we found a
+type for ω, there is no general type for Ω ≡ ω
+ω. In fact, it turns out that no Turing complete system can be
+strongly normalizing, from which it follows that System F is not
+Turing complete.
+
+
+## Polymorphism in natural language
+
+Is the simply-typed lambda calclus enough for analyzing natural
+language, or do we need polymorphic types? Or something even more expressive?
+
+The classic case study motivating polymorphism in natural language
+comes from coordination. (The locus classicus is Partee and Rooth
+1983.)
+
+ Type of the argument of "and":
+ Ann left and Bill left. t
+ Ann left and slept. e->t
+ Ann and Bill left. (e->t)-t (i.e, generalize quantifiers)
+ Ann read and reviewed the book. e->e->t
+
+In English (likewise, many other languages), *and* can coordinate
+clauses, verb phrases, determiner phrases, transitive verbs, and many
+other phrase types. In a garden-variety simply-typed grammar, each
+kind of conjunct has a different semantic type, and so we would need
+an independent rule for each one. Yet there is a strong intuition
+that the contribution of *and* remains constant across all of these
+uses.
+
+Can we capture this using polymorphic types?
+
+ Ann, Bill e
+ left, slept e -> t
+ read, reviewed e -> e -> t
+
+With these basic types, we want to say something like this:
+
+ and:t->t->t = λl:t. λr:t. l r false
+ gen_and = Λα.Λβ.λf:(β->t).λl:α->β.λr:α->β.λx:α. f (l x) (r x)
+
+The idea is that the basic *and* (the one defined in the first line)
+conjoins expressions of type `t`. But when *and* conjoins functional
+types (the definition in the second line), it builds a function that
+distributes its argument across the two conjuncts and then applies the
+appropriate lower-order instance of *and*.
+
+ and (Ann left) (Bill left)
+ gen_and [e] [t] and left slept
+ gen_and [e] [e->t] (gen_and [e] [t] and) read reviewed
+
+Following the terminology of Partee and Rooth, this strategy of
+defining the coordination of expressions with complex types in terms
+of the coordination of expressions with less complex types is known as
+Generalized Coordination, which is why we call the polymorphic part of
+the definition `gen_and`.
+
+In the first line, the basic *and* is ready to conjoin two truth
+values. In the second line, the polymorphic definition of `gen_and`
+makes explicit exactly how the meaning of *and* when it coordinates
+verb phrases depends on the meaning of the basic truth connective.
+Likewise, when *and* coordinates transitive verbs of type `e->e->t`,
+the generalized *and* depends on the `e->t` version constructed for
+dealing with coordinated verb phrases.
+
+On the one hand, this definition accurately expresses the way in which
+the meaning of the conjunction of more complex types relates to the
+meaning of the conjunction of simpler types. On the other hand, it's
+awkward to have to explicitly supply an expression each time that
+builds up the meaning of the *and* that coordinates the expressions of
+the simpler types. We'd like to have that automatically handled by
+the polymorphic definition; but that would require writing code that
+behaved differently depending on the types of its type arguments,
+which goes beyond the expressive power of System F.
+
+And in fact, discussions of generalized coordination in the
+linguistics literature are almost always left as a meta-level
+generalizations over a basic simply-typed grammar. For instance, in
+Hendriks' 1992:74 dissertation, generalized coordination is
+implemented as a method for generating a suitable set of translation
+rules, which are in turn expressed in a simply-typed grammar.
+
+There is some work using System F to express generalizations about
+natural language: Ponvert, Elias. 2005. Polymorphism in English Logical
+Grammar. In *Lambda Calculus Type Theory and Natural Language*: 47--60.
+
+Not incidentally, we're not aware of any programming language that
+makes generalized coordination available, despite is naturalness and
+ubiquity in natural language. That is, coordination in programming
+languages is always at the sentential level. You might be able to
+evaluate `(delete file1) and (delete file2)`, but never `delete (file1
+and file2)`.
+
+We'll return to thinking about generalized coordination as we get
+deeper into types. There will be an analysis in term of continuations
+that will be particularly satisfying.
+
+
+#Types in OCaml