not WIP
[lambda.git] / topics / _week5_system_F.mdwn
1 # System F and recursive types
2
3 In the simply-typed lambda calculus, we write types like <code>&sigma;
4 -> &tau;</code>.  This looks like logical implication.  Let's take
5 that resemblance seriously.  Then note that types respect modus
6 ponens: given two expressions <code>fn:(&sigma; -> &tau;)</code> and
7 <code>arg:&sigma;</code>, the application of `fn` to `arg` has type
8 <code>(fn arg):&tau;</code>.  
9
10 Here and below, writing <code>x:&alpha;</code> means that a term `x`
11 is an expression with type <code>&alpha;</code>.
12
13 This is a special case of a general pattern that falls under the
14 umbrella of the Curry-Howard correspondence.  We'll discuss
15 Curry-Howard in some detail later.
16
17 System F is due (independently) to Girard and Reynolds.
18 It enhances the simply-typed lambda calculus with quantification over
19 types.  In System F, you can say things like
20
21 <code>&Gamma; &alpha; (\x.x):(&alpha; -> &alpha;)</code>
22
23 This says that the identity function maps arguments of type &alpha; to
24 results of type &alpha;, for any choice of &alpha;.  So the &Gamma; is
25 a universal quantifier over types.
26
27