+Typing ω
+--------------
+
+In fact, it is even possible to give a type for ω in System F.
+
+<code>ω = lambda x:(All X. X->X) . x [All X . X->X] x</code>
+
+In order to see how this works, we'll apply ω to the identity
+function.
+
+<code>ω [All X . X -> X] id ==</code>
+
+ (lambda x:(All X . X->X) . x [All X . X->X] x) (lambda X . lambda x:X . x)
+
+Since the type of the identity function is `(All X . X->X)`, it's the
+right type to serve as the argument to ω. The definition of
+ω instantiates the identity function by binding the type
+variable `X` to the universal type `All X . X->X`. Instantiating the
+identity function in this way results in an identity function whose
+type is 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 (in this case, the identity 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 Ω ≡ ω
+ω. (It turns out that no Turing complete system can be strongly
+normalizing, from which it follows that System F is not Turing complete.)
+