# System F and recursive types
In the simply-typed lambda calculus, we write types like σ
-> τ. This looks like logical implication. We'll take
that resemblance seriously when we discuss the Curry-Howard
correspondence. In the meantime, note that types respect modus
ponens:
Expression Type Implication
----------------------------------
fn α -> β α ⊃ β
arg α α
------ ------ --------
fn arg β β
The implication in the right-hand column is modus ponens, of course.
System F is usually attributed to Girard, but was independently
proposed around the same time by 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.