[[!toc levels=2]]
-# System F and recursive types
-
-In the simply-typed lambda calculus, we write types like <code>σ
--> τ</code>. This looks like logical implication. We'll take
-that resemblance seriously when we discuss the Curry-Howard
-correspondence. In the meantime, note that types respect modus
-ponens:
-
-<pre>
-Expression Type Implication
------------------------------------
-fn α -> β α ⊃ β
-arg α α
------- ------ --------
-(fn arg) β β
-</pre>
-
-The implication in the right-hand column is modus ponens, of course.
+# System F: the polymorphic lambda calculus
+
+The simply-typed lambda calculus is beautifully simple, but it can't
+even express the predecessor function, let alone full recursion. And
+we'll see shortly that there is good reason to be unsatisfied with the
+simply-typed lambda calculus as a way of expressing natural language
+meaning. So we will need to get more sophisticated about types. The
+next step in that journey will be to consider System F.
System F was discovered by Girard (the same guy who invented Linear
Logic), but it was independently proposed around the same time by