XGitUrl: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=topics%2F_week5_system_F.mdwn;h=f0134f925bc25e93e523cff4c69f16d503d01e18;hp=86f1c75bb9eb48708797946ea766dd58fa96d6b5;hb=a4d2693effe839524592f4427465ff8d97625302;hpb=d03fe382641cc8bc266184561d3c484deeb12ca1
diff git a/topics/_week5_system_F.mdwn b/topics/_week5_system_F.mdwn
index 86f1c75b..f0134f92 100644
 a/topics/_week5_system_F.mdwn
+++ b/topics/_week5_system_F.mdwn
@@ 1,22 +1,26 @@
# System F and recursive types
In the simplytyped lambda calculus, we write types like σ
> τ
. This looks like logical implication. Let's take
that resemblance seriously. Then note that types respect modus
ponens: given two expressions fn:(σ > τ)
and
arg:σ
, the application of `fn` to `arg` has type
(fn arg):τ
.

Here and below, writing x:α
means that a term `x`
is an expression with type α
.

This is a special case of a general pattern that falls under the
umbrella of the CurryHoward correspondence. We'll discuss
CurryHoward in some detail later.

System F is due (independently) to Girard and Reynolds.
It enhances the simplytyped lambda calculus with quantification over
types. In System F, you can say things like
+> τ. This looks like logical implication. We'll take
+that resemblance seriously when we discuss the CurryHoward
+correspondence. In the meantime, note that types respect modus
+ponens:
+
++Expression Type Implication
+
+fn α > β α ⊃ β
+arg α α
+  
+fn arg β β
+
+
+The implication in the righthand 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
+simplytyped lambda calculus with quantification over types. In
+System F, you can say things like
Λ α (\x.x):(α > α)
@@ 24,4 +28,3 @@ This says that the identity function maps arguments of type α to
results of type α, for any choice of α. So the Λ is
a universal quantifier over types.
