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 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. -