From b082bc6529323e004c1c8466b507de34525c33bf Mon Sep 17 00:00:00 2001 From: Chris Date: Mon, 23 Feb 2015 14:14:28 -0500 Subject: [PATCH] edits --- topics/_week5_system_F.mdwn | 37 ++++++++++++++++++++----------------- 1 file changed, 20 insertions(+), 17 deletions(-) diff --git a/topics/_week5_system_F.mdwn b/topics/_week5_system_F.mdwn index 86f1c75b..72488153 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. - -- 2.11.0