Redigerer Typeteori (avsnitt)

=== Definisjon ===
Typene fra <math>\lambda^2</math> utvides med to nye former:
:<math> \tau ::= T \mid \alpha \mid \tau \to \tau \mid \forall \alpha . \tau </math>
hvor <math>\alpha</math> kalles en type-variabel, og <math>\forall \alpha . \tau</math> representerer polymorfi.

Termene utvides med to nye konstruktører:
:<math> e ::= x \mid e\,e \mid \lambda x : \tau . e \mid \Lambda \alpha . e \mid e\,\tau</math>
hvor <math>\Lambda \alpha. e</math> sier at termen <math>e</math> skal fungere for alle typer satt inn i <math>e</math>,
og <math>e\,\tau</math>, som forventer at <math>e</math> er av typen <math>\forall \alpha . \tau'</math>, betyr at uttrykket
<math>e</math> skal spesialiseres til typen <math>\tau</math>.

Typereglene for System F er som for <math>\lambda^\to</math>, men med to ekstra regler:
<math> \Gamma \vdash e : \tau \quad \alpha \not\in \mathrm{FV}(\Gamma) \over \Gamma \vdash \Lambda \alpha . e : \forall \alpha. \tau </math>
og
<math> \Gamma \vdash e : \forall \alpha . \tau_1 \over \Gamma \vdash e\,\tau_2 : \tau_1[\tau_2 / \alpha] </math>. Notasjonen <math>\mathrm{FV(\Gamma)}</math>
betyr her mengden av frie type-variabler som forekommer i <math>\Gamma</math>.