Redigerer Typeteori (avsnitt)

=== Motivasjon ===
Hvis man ser på den utypede funksjonen <math>\lambda x . x</math>, altså identitetsfunksjone, så kan man se at den har typen <math>\tau \to \tau</math> for 
alle <math>\tau</math> i <math>\lambda^\to</math> à la Curry. Men hvis funksjonen forekommer som en del-term og den bindes til en variabel, så vil den variabelen
kun ha èn type i den gitte derivasjonen. Det betyr at i <math>\lambda^\to</math> må man gjenta definisjoner for forskjellige typer, selv om det er «unødvendig».

I System F løses dette ved å innføre variabler for typer og en kvantor som gjør det mulig å uttrykke ''for alle typer <math>\alpha</math>, så er <math>\tau</math> en type'', hvor
<math>\alpha</math> kan forekomme fritt i <math>\tau</math>. Konkret notasjon for kvantoren er <math>\forall \alpha . \tau</math>. Her er noen eksempler på 
funksjonstyper hvor allkvantoren kommer til nytte:

* <math> identity : \forall \alpha. \; \alpha \to \alpha </math>. Identitetsfunksjonen.
* <math> cons : \forall \alpha. \; \alpha \to \mathrm{List}\;\alpha \to \mathrm{List}\;\alpha</math>. Funksjonen som legger til et element foran i en liste.
* <math> map : \forall \alpha. \forall \beta. \; \mathrm{List}\,\alpha \to (\alpha \to \beta) \to \mathrm{List}\,\beta</math> (Hvor <math>List</math> er antatt en primitiv type for lister med elementer av en gitt type.) 
* <math> \forall \alpha . \alpha \to (\alpha \to \alpha) \to \alpha</math>. Typen for Church-enkodingen av naturlige tall.