Added system F

diff --git a/topics/_week5_system_F.mdwn b/topics/_week5_system_F.mdwn
new file mode 100644 (file)
index 0000000..684f42b
--- /dev/null
+++ b/topics/_week5_system_F.mdwn
@@ -0,0 +1,27 @@
+# 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
+
+<code>&Gamma; &alpha; (\x.x):(&alpha; -> &alpha;)</code>
+
+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
+a universal quantifier over types.
+
+