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