Typeteori

I matematikk, informatikk og logikk er **typeteori** studien av visse formelle systemer som relaterer termer til typer.
Typeteori ble opprinnelig utviklet for reparere Russels og Whiteheads logiske system *Principia Mathematica*, som
Kurt Gödel i 1902 oppdaget var inkonsistent, men typeteori er i dag et studium i seg selv.
Det forskes på bruk av typeteori som et alternativ til mengdelære som fundamentet for matematikk, og det
er en nær sammenheng mellom datatyper, slik man finner dem i programmeringsspråk, og typene i typeteori.
Videre er det en tett sammenheng med logikk, tydeliggjort av Curry-Howard-korrespondansen.

## Lambdakalkylen med endelige typer
Lambdakalylen med endelig typer (eng: "simply typed lambda calculus"), \lambda^\to, ble utviklet
av Alonzo Church i 1940, i et forsøk på temme den utypete lambdakalkylen, som er logisk sett inkonsistent.

### Syntaks
Den syntaktiske kategorien for typer defineres som følger, hvor B er en mengde med "basistyper",
:\tau ::= \tau \to \tau \mid T \quad \mathrm{hvor} \quad T \in B.
Et eksempel på basistyper som man kan finne i programmeringsspråk er
:B = \{ \mathrm{nat},\; \mathrm{bool} \},
hvor nat står for naturlige tall, og
bool for bolske verdier. 
Da vil f.eks. typen  \mathrm{nat} \to \mathrm{bool} representere
en funksjon som tar et naturlig tall og returnerer en boolsk verdi. En funksjon som tar flere
argumenter, f.eks. pluss funksjonen, vil ha typen  \mathrm{nat} \to \mathrm{nat} \to \mathrm{nat}.

Termene i \lambda^\to er definert som 
:e ::= x \mid e\,e \mid \lambda x : \tau. e.
Her represetnerer \lambda x : \tau . e en funksjon
som tar et argument x av typen \tau,
og som returnerer e. Jukstaposisjon av to termer, e_1 \, e_2
representerer funksjonskall (vanlig notasjon innen matematikk er e_1(e_2)), og x er referanse til en variable.

### Typesjekking
Relasjonen \Gamma \vdash e\,:\,\tau definerer hvorvidt et uttykk e har typen \tau under
antagelsene \Gamma = x_1 : \tau_1, \ldots, x_n : \tau_n (hvor x_i : \tau_i representerer antagelsen at variabelen x har typen \tau).
\Gamma kalles en *kontekst*.
Relasjonen defineres som følger:

For å være formell, må det spesifiseres hva \Gamma er og hva \Gamma, x:\tau og \Gamma(x) = \tau skal bety.
Det er flere måter å gjøre dette på. Det konseptuelt enkleset er å si at \Gamma er en endelig, partiell funksjon fra mengden av variabler til typer,
og å definere \Gamma, x : \tau som funksjonen slik at (\Gamma, x : \tau)(x) = \tau, og ellers (\Gamma, x : \tau)(y) = \Gamma(y),
gitt at  x \not= y.

### Semantikk
Standardsemantikken for lambda kalkylen er \beta-reduksjon, som kan defineres som  (\lambda x : \tau . e_1)\, e_2 \to_\beta e_1[e_2 / x], hvor
e_1[e_2 / x] er funksjonen som substituerer alle frie forekomster av x i e_1 med e_2, og samtidig
passer på at ingen av de fri variablene i e_2 blir bundet av binderne i e_1.
Siden et uttrykk på formen (\lambda x : \tau . e_1) e_2 kan \beta-reduseres, kalles uttrykk på den formen en "redex" (eng "reducable expression", norsk: reduserbart uttrykk).

Denne relasjonen kan så løftes til en relasjon som gjør en enkel \beta-reduksjon hvor som helst i en term. Relasjonen defineres som følger:

Gjentatt reduksjon representeres med relasjonen e \to^* e', som tilsvarer den refleksive og transitive tillukkningen av e \to e', og som defineres som :

Hvis en term e ikke kan reduseres, altså, det finnes ingen e' slik at  e \to e', så kalles e en verdi. 
Det er bevist at for alle termer e, kontekster \Gamma og typer \tau slik at  \Gamma \vdash e : \tau,
så vil e \to e' slik at e' er en verdi. Dette er ikke tilfellet for utypet lambdakalkyle, hvor f.eks. termen (\lambda x. x \, x) (\lambda x. x \, x)
ikke reduserer til noen verdi.

### Lambdakalkyle à la Curry
Presentasjonen av \lambda^\to i avsnittene over, er presentert à la Church, siden termene er annotert med typer. Et alternativ er å beholde de utypede termene fra den 
utypede lambdakalkylen. Dette kalles à la Curry, og definisjonen av termer er da:
: e ::= x \mid \lambda x . e \mid e \, e  
og typerelasjonen er

Hvorvidt et typesystem er presentert à la Curry eller Church vil få følger for hvilke egenskaper systemet får. F.eks. kan et uttrykk e i \lambda^\to à la Church kun
ha en type, mens i à la Curry kan et term ha mange forskjellige typer. For mer uttrykksfulle typesystemer, så kan typesjekking bli uavgjørbart i Curry form, mens de oftere er avgjørbare i Church form. 
Noen typesystemer har kun mening i en av formuleringene.

### Normalform
I motsetning til utypet lambdakalkyle, så har alle vell-typede termer i \lambda^\to en unik normalform (opp til alpha-ekvivalens).

## System F
**System F** generaliserer \lambda-kalkyle med endelige typer, ved å legge til *kvantifisering* over typer. 
Typesystemet går også under navnene *Andreordens <math>\lambda</math>-kalkulus* og *polymorfisk <math>\lambda</math>-kalkulus*.
System F ble oppdaget av både logikeren Jean-Yves Girard og informatikeren John C. Reynolds uanvhengig av hverandre.

### Motivasjon
Hvis man ser på den utypede funksjonen \lambda x . x, altså identitetsfunksjone, så kan man se at den har typen \tau \to \tau for 
alle \tau i \lambda^\to à 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 \lambda^\to 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
\alpha kan forekomme fritt i \tau. Konkret notasjon for kvantoren er \forall \alpha . \tau. Her er noen eksempler på 
funksjonstyper hvor allkvantoren kommer til nytte:

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

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

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

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

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

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

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

## Barendregts lambda-kube

Matematikeren Henk Barendregt utviklet lambda-kuben, \lambda-kuben, for å utforske forskjellige utvidelser av typesystemer.
Han tar utgangspunkt i \lambda^\to, og ser på tre utvidelser, som vises som akser i kuben:

# Typeoperatorer — typer som er avhenger av typer, z-aksen
# Polymorphisme — termer som avhenger av typer, y-aksen
# *Dependent* typer — typer som avhenger av termer, x-aksen

Disse utvidelsene gir opphav til åtte forskjellige typesystemer, avhengig av hvilke utvidelser man tar med. Lambda-kuben gir et 
rammeverk som definerer alle åtte systemene samtidig, men det er også mulig å definere hvert system for seg selv.
Hvis man ikke tar med noen av utvidelsene så får man \lambda^\to som beskrevet over, 
og tar man med alle, får man noe som tilsvarer Calculus of Constructions.

### Definisjon av lambda kuben
Det er ikke lenger praktisk å ha to seperate syntaktiske kategorier for termer og typer, og i \lambda-kuben definerer man derfor pseudo-termer som
: \mathcal{T} ::= x \mid C \mid \mathcal{T}_1\, \mathcal{T}_2 \mid \lambda x : \mathcal{T}_1 . \mathcal{T}_2 \mid \Pi x : \mathcal{T}_1 . \mathcal{T}_2
hvor C er en mengde konstanter, som minst inneholder * (les: type) og \Box (les: 'kind').

#### Felles regler
Alle systemene har noen regler til felles.

#### Parametriske regler
Følgende regel er parametrisk i  s_1, s_2 \in \{ *, \Box \}. 

:\Gamma \vdash A : s_1 \quad \Gamma, x : A \vdash B : s_2 \over \Gamma \vdash \Pi x:A.B : s_2 

Man kan bestemme hvilket typesystem man ønsker ved å bestemme hvilke instanser av (s_1, s_2) man som er godtatt. Tabellen under lister opp alle mulighetene.

## Egenskaper ved typesystemer

To klassiske egenskaper som typesystemer kan ha er:
* Preservering (eng: *subject reduction* el. *preservation*): hvis \vdash e : \tau og e \to e', så \vdash e' : \tau. Altså, reduksjon bevarer typen.
* Progresjon (eng: *progress*): hvis \vdash e : \tau, så er enten e en verdi, eller så eksisterer en e' slik at e \to e'. Altså, vel-typede termer henger ikke.

## Litteratur
* S. Abramsky / D. M. Gabbay / T. S. E. Maibaum / H. P. Barendregt (1993). "Handbook of Logic in Computer Science, volume II, chapter Lambda Calculi with Types"
* Jean-Yves Girard (1989). *Proofs and Types*, Cambridge University Press. ISBN 0 521 37181 3. Tilgjengelig online: http://www.paultaylor.eu/stable/Proofs+Types.html