index 86f1c75..f0134f9 100644 (file)
@@ -1,22 +1,26 @@
# System F and recursive types

In the simply-typed lambda calculus, we write types like <code>&sigma;
--> &tau;</code>.  This looks like logical implication.  Let's take
-that resemblance seriously.  Then note that types respect modus
-ponens: given two expressions <code>fn:(&sigma; -> &tau;)</code> and
-<code>arg:&sigma;</code>, the application of `fn` to `arg` has type
-<code>(fn arg):&tau;</code>.
-
-Here and below, writing <code>x:&alpha;</code> means that a term `x`
-is an expression with type <code>&alpha;</code>.
-
-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.
-
-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
+-> &tau;</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            &alpha; -> &beta;   &alpha; &sup; &beta;
+arg           &alpha;        &alpha;
+------        ------    --------
+fn arg        &beta;        &beta;
+</pre>
+
+The implication in the right-hand column is modus ponens, of course.
+
+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>&Lambda; &alpha; (\x.x):(&alpha; -> &alpha;)</code>

@@ -24,4 +28,3 @@ This says that the identity function maps arguments of type &alpha; to
results of type &alpha;, for any choice of &alpha;.  So the &Lambda; is
a universal quantifier over types.

-