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. We'll take
5 that resemblance seriously when we discuss the Curry-Howard
6 correspondence. In the meantime, note that types respect modus
10 Expression Type Implication
11 ----------------------------------
12 fn α -> β α ⊃ β
14 ------ ------ --------
18 The implication in the right-hand column is modus ponens, of course.
20 System F is usually attributed to Girard, but was independently
21 proposed around the same time by Reynolds. It enhances the
22 simply-typed lambda calculus with quantification over types. In
23 System F, you can say things like
25 <code>Λ α (\x.x):(α -> α)</code>
27 This says that the identity function maps arguments of type α to
28 results of type α, for any choice of α. So the Λ is
29 a universal quantifier over types.