----------------
We saw that the predecessor function couldn't be expressed in the
-simply-typed lambda calculus. It can be expressed in System F, however.
+simply-typed lambda calculus. It can be expressed in System F,
+however. Here is one way, coded in
+[[Benjamin Pierce's type-checker and evaluator for
+System F|http://www.cis.upenn.edu/~bcpierce/tapl/index.html]] (the
+part you want is called "fullpoly"):
+
+ N = All X . (X->X)->X->X;
+ Pair = All X . (N -> N -> X) -> X;
+ let zero = lambda X . lambda s:X->X . lambda z:X. z in
+ let snd = lambda x:N . lambda y:N . y in
+ let pair = lambda x:N . lambda y:N . lambda X . lambda z:N->N->X . z x y in
+ let suc = lambda n:N . lambda X . lambda s:X->X . lambda z:X . s (n [X] s z) in
+ let shift = lambda p:Pair . p [Pair] (lambda a:N . lambda b:N . pair (suc a) a) in
+ let pre = lambda n:N . n [Pair] shift (pair zero zero) [N] snd in
+
+ pre (suc (suc (suc zero)));
+
+We've truncated the names of "suc(c)" and "pre(d)", since those are
+reserved words in Pierce's system. Note that in this code, there is
+no typographic distinction between ordinary lambda and type-level
+lambda, though the difference is encoded in whether the variables are
+lower case (for ordinary lambda) or upper case (for type-level
+lambda).
+
+The key to the extra flexibility provided by System F is that we can
+instantiate the `pair` function to return a number, as in the
+definition of `pre`, or we can instantiate it to return an ordered
+pair, as in the definition of the `shift` function. Because we don't
+have to choose a single type for all uses of the pair-building
+function, we aren't forced into a infinite regress of types.
[See Benjamin C. Pierce. 2002. *Types and Programming Languages*, MIT
Press, pp. 350--353, for `tail` for lists in System F.]
+Typing ω
+--------------
+
+In fact, it is even possible to give a type for &omeage; in System F.
+
+ omega = lambda x:(All X. X->X) . x [All X . X->X] x in
+ omega;
+
+Each time the internal application is performed, the type of the head
+is chosen anew. And each time, we choose the same type as before, the
+type of a function that takes an argument of any type and returns a
+result of the same type...
+
Types in OCaml
--------------