From e786697f406f29139f4116d13687b37e42594f81 Mon Sep 17 00:00:00 2001 From: Chris Date: Sun, 22 Feb 2015 17:32:47 -0500 Subject: [PATCH] Added system F --- topics/_week5_system_F.mdwn | 27 +++++++++++++++++++++++++++ 1 file changed, 27 insertions(+) create mode 100644 topics/_week5_system_F.mdwn diff --git a/topics/_week5_system_F.mdwn b/topics/_week5_system_F.mdwn new file mode 100644 index 00000000..684f42be --- /dev/null +++ b/topics/_week5_system_F.mdwn @@ -0,0 +1,27 @@ +# 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 + +Γ α (\x.x):(α -> α) + +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