index 684f42b..f0134f9 100644 (file)
@@ -1,27 +1,30 @@
# System F and recursive types

In the simply-typed lambda calculus, we write types like <code>&sigma;
# 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>.
+-> &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:

-Here and below, writing <code>x:&alpha;</code> means that a term `x`
-is an expression with type <code>&alpha;</code>.
+<pre>
+Expression    Type     Implication
+----------------------------------
+fn            &alpha; -> &beta;   &alpha; &sup; &beta;
+arg           &alpha;        &alpha;
+------        ------    --------
+fn arg        &beta;        &beta;
+</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>&Gamma; &alpha; (\x.x):(&alpha; -> &alpha;)</code>
+<code>&Lambda; &alpha; (\x.x):(&alpha; -> &alpha;)</code>

This says that the identity function maps arguments of type &alpha; to

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

a universal quantifier over types.

-