X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=topics%2F_week5_system_F.mdwn;h=f0134f925bc25e93e523cff4c69f16d503d01e18;hp=684f42be4087594c9c97768e7f7ef66bcca0bc5b;hb=a4d2693effe839524592f4427465ff8d97625302;hpb=e786697f406f29139f4116d13687b37e42594f81;ds=sidebyside
diff --git a/topics/_week5_system_F.mdwn b/topics/_week5_system_F.mdwn
index 684f42be..f0134f92 100644
--- a/topics/_week5_system_F.mdwn
+++ b/topics/_week5_system_F.mdwn
@@ -1,27 +1,30 @@
# System F and recursive types
In the simply-typed 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):τ.
+-> τ. 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 x:α means that a term `x`
-is an expression with type α.
+
+Expression Type Implication
+----------------------------------
+fn α -> β α ⊃ β
+arg α α
+------ ------ --------
+fn arg β β
+
-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
-Γ α (\x.x):(α -> α)
+Λ α (\x.x):(α -> α)
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.
-