# System F and recursive types
In the simply-typed lambda calculus, we write types like <code>σ
--> τ</code>. This looks like logical implication. Let's take
-that resemblance seriously. Then note that types respect modus
-ponens: given two expressions <code>fn:(σ -> τ)</code> and
-<code>arg:σ</code>, the application of `fn` to `arg` has type
-<code>(fn arg):τ</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:
-Here and below, writing <code>x:α</code> means that a term `x`
-is an expression with type <code>α</code>.
+<pre>
+Expression Type Implication
+----------------------------------
+fn α -> β α ⊃ β
+arg α α
+------ ------ --------
+fn arg β β
+</pre>
-This is a special case of a general pattern that falls under the
-umbrella of the Curry-Howard correspondence. We'll discuss
-Curry-Howard in some detail later.
+The implication in the right-hand column is modus ponens, of course.
-System F is due (independently) to Girard and Reynolds.
-It enhances the simply-typed lambda calculus with quantification over
-types. In System F, you can say things like
+System F is usually attributed to Girard, but was independently
+proposed around the same time by Reynolds. It enhances the
+simply-typed lambda calculus with quantification over types. In
+System F, you can say things like
-<code>Γ α (\x.x):(α -> α)</code>
+<code>Λ α (\x.x):(α -> α)</code>
This says that the identity function maps arguments of type α to
-results of type α, for any choice of α. So the Γ is
+results of type α, for any choice of α. So the Λ is
a universal quantifier over types.
-