1 # System F and recursive types
3 In the simply-typed lambda calculus, we write types like <code>σ
4 -> τ</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:(σ -> τ)</code> and
7 <code>arg:σ</code>, the application of `fn` to `arg` has type
8 <code>(fn arg):τ</code>.
10 Here and below, writing <code>x:α</code> means that a term `x`
11 is an expression with type <code>α</code>.
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.
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
21 <code>Λ α (\x.x):(α -> α)</code>
23 This says that the identity function maps arguments of type α to
24 results of type α, for any choice of α. So the Λ is
25 a universal quantifier over types.