Redigerer Typeteori (avsnitt)

=== Eksempler ===
Vi kan observere at vi nå kan definere en genrell identitetsfunksjon, <math> \Lambda \alpha.\, \lambda x : \alpha . x</math> som har typen <math> \forall \alpha . \alpha \to \alpha</math>.
Hvis vi kaller funksjonen <math>id</math> ser vi at uttrykket <math>id\, \mathrm{nat}</math> har typen <math>\mathrm{nat} \to \mathrm{nat}</math>.

Det er også mulig å representere naturlige tall ved å benytte Churchs enkoding i System F. Ideen bak Churchs enkoding er at et tall <math>n</math> representeres av
en ''iterator'' som itererer <math>n</math> ganger. I utypet <math>\lambda</math>-kalkyle kan man definere 0 som <math>\lambda x. \lambda f. x</math>, altså
funksjonen som tar et element <math>x</math> og en funksjon <math>f</math>, og sender <math>x</math> gjennom funksjonen <math>f</math> null ganger.
Videre defineres 1 som <math>\lambda x. \lambda x. f \, x</math>, altså funksjonen som sender <math>x</math> gjennom <math>f</math> en gang, og
2 defineres som <math>\lambda x. \lambda f. f\,(f\,x))</math>, funksjonen som sender <math>x</math> gjennom <math>f</math> to ganger. Generelt
defineres tallet <math>n</math> som funksjonen <math>\lambda x . \lambda f. f^n\, x</math>.

* La <math>nat</math> være en forkortelse for typen <math>\forall \alpha . \alpha \to (\alpha \to \alpha) \to \alpha</math>.
* La <math>0</math> være definert som <math>\forall \alpha. \lambda x : \alpha . \lambda f : \alpha \to \alpha . x</math>. Observer at <math>\vdash 0 : nat</math>.
* La <math>S</math> være definert som <math>\lambda n : nat. \forall \alpha . \lambda x : \alpha. \lambda f : \alpha \to \alpha. n \alpha\, x\, (f\, x)</math>. Navnet <math>S</math> er første bokstav i suksessor, og representerer ''pluss en'' funksjonen. Observer at <math>\vdash S : nat \to nat</math>.