[[!toc levels=2]]
-# System F and recursive types
+# 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.
In the simply-typed lambda calculus, we write types like <code>σ
-> τ</code>. This looks like logical implication. We'll take