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=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 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):τ`. - -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 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 +-> τ. 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: + +
```+Expression    Type     Implication
+----------------------------------
+fn            α -> β   α ⊃ β
+arg           α        α
+------        ------    --------
+fn arg        β        β
+```
+ +The implication in the right-hand 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 +simply-typed 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. -