# 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.