X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?a=blobdiff_plain;f=topics%2F_week5_system_F.mdwn;h=3f533abdd64d883a50f7eacbf89321b33bddd784;hb=25203ef5960e2eedad25ffaac5db3d86ba5b31b1;hp=684f42be4087594c9c97768e7f7ef66bcca0bc5b;hpb=e786697f406f29139f4116d13687b37e42594f81;p=lambda.git
diff --git a/topics/_week5_system_F.mdwn b/topics/_week5_system_F.mdwn
index 684f42be..3f533abd 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.
-