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"), ${\displaystyle \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 ${\displaystyle B}$ er en mengde med "basistyper",

${\displaystyle \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

${\displaystyle B=\{\mathrm {nat} ,\;\mathrm {bool} \}}$,

hvor nat står for naturlige tall, og bool for bolske verdier. Da vil f.eks. typen ${\displaystyle \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 ${\displaystyle \mathrm {nat} \to \mathrm {nat} \to \mathrm {nat} }$.

Termene i ${\displaystyle \lambda ^{\to }}$ er definert som

${\displaystyle e::=x\mid e\,e\mid \lambda x:\tau .e}$.

Her represetnerer ${\displaystyle \lambda x:\tau .e}$ en funksjon som tar et argument ${\displaystyle x}$ av typen ${\displaystyle \tau }$, og som returnerer ${\displaystyle e}$. Jukstaposisjon av to termer, ${\displaystyle e_{1}\,e_{2}}$ representerer funksjonskall (vanlig notasjon innen matematikk er ${\displaystyle e_{1}(e_{2})}$), og ${\displaystyle x}$ er referanse til en variable.

Typesjekking

Relasjonen ${\displaystyle \Gamma \vdash e\,:\,\tau }$ definerer hvorvidt et uttykk ${\displaystyle e}$ har typen ${\displaystyle \tau }$ under antagelsene ${\displaystyle \Gamma =x_{1}:\tau _{1},\ldots ,x_{n}:\tau _{n}}$ (hvor ${\displaystyle x_{i}:\tau _{i}}$ representerer antagelsen at variabelen ${\displaystyle x}$ har typen ${\displaystyle \tau }$). ${\displaystyle \Gamma }$ kalles en kontekst. Relasjonen defineres som følger:

${\displaystyle {x{\mathbin {:}}\sigma \in \Gamma \over \Gamma \vdash x{\mathbin {:}}\sigma }}$ (var)

${\displaystyle {\Gamma ,x{\mathbin {:}}\sigma \vdash e{\mathbin {:}}\tau \over \Gamma \vdash (\lambda x{\mathbin {:}}\sigma .~e){\mathbin {:}}(\sigma \to \tau )}}$ (lam)

${\displaystyle {\Gamma \vdash e_{1}{\mathbin {:}}\sigma \to \tau \quad \Gamma \vdash e_{2}{\mathbin {:}}\sigma \over \Gamma \vdash e_{1}~e_{2}{\mathbin {:}}\tau }}$ (app)

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

Semantikk

Standardsemantikken for lambda kalkylen er ${\displaystyle \beta }$-reduksjon, som kan defineres som ${\displaystyle (\lambda x:\tau .e_{1})\,e_{2}\to _{\beta }e_{1}[e_{2}/x]}$, hvor ${\displaystyle e_{1}[e_{2}/x]}$ er funksjonen som substituerer alle frie forekomster av ${\displaystyle x}$ i ${\displaystyle e_{1}}$ med ${\displaystyle e_{2}}$, og samtidig passer på at ingen av de fri variablene i ${\displaystyle e_{2}}$ blir bundet av binderne i ${\displaystyle e_{1}}$. Siden et uttrykk på formen ${\displaystyle (\lambda x:\tau .e_{1})e_{2}}$ kan ${\displaystyle \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 ${\displaystyle \beta }$-reduksjon hvor som helst i en term. Relasjonen defineres som følger:

${\displaystyle {e\to _{\beta }e' \over e\to e'}}$

${\displaystyle {e\to e' \over \lambda x:\tau .e\to \lambda x:\tau .e'}}$

${\displaystyle {e\to e' \over e\,e_{2}\to e'\,e_{2}}}$

${\displaystyle {e\to e' \over e_{1}\,e\to e_{1}\,e'}}$

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

${\displaystyle {\mathrm {} \over e\to ^{*}e}}$

${\displaystyle {e_{1}\to e_{2}\quad e_{2}\to ^{*}e_{3} \over e_{1}\to ^{*}e_{3}}}$

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

Lambdakalkyle à la Curry

Presentasjonen av ${\displaystyle \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:

${\displaystyle e::=x\mid \lambda x.e\mid e\,e}$

og typerelasjonen er

${\displaystyle {\Gamma (x)=\tau \over \Gamma \vdash x:\tau }}$ (var)

${\displaystyle {\Gamma \vdash e_{1}:\tau _{2}\to \tau _{2}\quad \Gamma \vdash e_{2}:\tau _{2} \over \Gamma \vdash e_{1}\,e_{2}:\tau _{2}}}$ (app)

${\displaystyle {\Gamma ,x:\tau _{2}\vdash e:\tau _{2} \over \Gamma \vdash \lambda x.e:\tau _{1}\to \tau _{2}}}$ (lam)

Hvorvidt et typesystem er presentert à la Curry eller Church vil få følger for hvilke egenskaper systemet får. F.eks. kan et uttrykk ${\displaystyle e}$ i ${\displaystyle \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 ${\displaystyle \lambda ^{\to }}$ en unik normalform (opp til alpha-ekvivalens).

System F

System F generaliserer ${\displaystyle \lambda }$-kalkyle med endelige typer, ved å legge til kvantifisering over typer. Typesystemet går også under navnene Andreordens ${\displaystyle \lambda }$-kalkulus og polymorfisk ${\displaystyle \lambda }$-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 ${\displaystyle \lambda x.x}$, altså identitetsfunksjone, så kan man se at den har typen ${\displaystyle \tau \to \tau }$ for alle ${\displaystyle \tau }$ i ${\displaystyle \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 ${\displaystyle \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 ${\displaystyle \alpha }$, så er ${\displaystyle \tau }$ en type, hvor ${\displaystyle \alpha }$ kan forekomme fritt i ${\displaystyle \tau }$. Konkret notasjon for kvantoren er ${\displaystyle \forall \alpha .\tau }$. Her er noen eksempler på funksjonstyper hvor allkvantoren kommer til nytte:

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

Definisjon

Typene fra ${\displaystyle \lambda ^{2}}$ utvides med to nye former:

${\displaystyle \tau ::=T\mid \alpha \mid \tau \to \tau \mid \forall \alpha .\tau }$

hvor ${\displaystyle \alpha }$ kalles en type-variabel, og ${\displaystyle \forall \alpha .\tau }$ representerer polymorfi.

Termene utvides med to nye konstruktører:

${\displaystyle e::=x\mid e\,e\mid \lambda x:\tau .e\mid \Lambda \alpha .e\mid e\,\tau }$

hvor ${\displaystyle \Lambda \alpha .e}$ sier at termen ${\displaystyle e}$ skal fungere for alle typer satt inn i ${\displaystyle e}$, og ${\displaystyle e\,\tau }$, som forventer at ${\displaystyle e}$ er av typen ${\displaystyle \forall \alpha .\tau '}$, betyr at uttrykket ${\displaystyle e}$ skal spesialiseres til typen ${\displaystyle \tau }$.

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

Eksempler

Vi kan observere at vi nå kan definere en genrell identitetsfunksjon, ${\displaystyle \Lambda \alpha .\,\lambda x:\alpha .x}$ som har typen ${\displaystyle \forall \alpha .\alpha \to \alpha }$. Hvis vi kaller funksjonen ${\displaystyle id}$ ser vi at uttrykket ${\displaystyle id\,\mathrm {nat} }$ har typen ${\displaystyle \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 ${\displaystyle n}$ representeres av en iterator som itererer ${\displaystyle n}$ ganger. I utypet ${\displaystyle \lambda }$-kalkyle kan man definere 0 som ${\displaystyle \lambda x.\lambda f.x}$, altså funksjonen som tar et element ${\displaystyle x}$ og en funksjon ${\displaystyle f}$, og sender ${\displaystyle x}$ gjennom funksjonen ${\displaystyle f}$ null ganger. Videre defineres 1 som ${\displaystyle \lambda x.\lambda x.f\,x}$, altså funksjonen som sender ${\displaystyle x}$ gjennom ${\displaystyle f}$ en gang, og 2 defineres som ${\displaystyle \lambda x.\lambda f.f\,(f\,x))}$, funksjonen som sender ${\displaystyle x}$ gjennom ${\displaystyle f}$ to ganger. Generelt defineres tallet ${\displaystyle n}$ som funksjonen ${\displaystyle \lambda x.\lambda f.f^{n}\,x}$.

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

Barendregts lambda-kube

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

1. Typeoperatorer — typer som er avhenger av typer, z-aksen
2. Polymorphisme — termer som avhenger av typer, y-aksen
3. 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 ${\displaystyle \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 ${\displaystyle \lambda }$-kuben definerer man derfor pseudo-termer som

${\displaystyle {\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 ${\displaystyle C}$ er en mengde konstanter, som minst inneholder ${\displaystyle *}$ (les: type) og ${\displaystyle \Box }$ (les: 'kind').

Felles regler

Alle systemene har noen regler til felles.

${\displaystyle {\mathrm {} \over \cdot \vdash *:\Box }}$ (ax) En type er en kind.

${\displaystyle {\Gamma \vdash N:A \over \Gamma ,x:B\vdash N:A}}$ (wk) Man kan legge til variabler.

${\displaystyle {\mathrm {} \over \Gamma ,x:A\vdash x:A}}$ (var)

${\displaystyle {\Gamma \vdash N:\Pi x:A.B\quad \Gamma \vdash M:A \over \Gamma \vdash N\,M:B[M/x]}}$ (app)

${\displaystyle {\Gamma ,x:A\vdash N:B \over \Gamma \vdash \lambda x:A.N:\Pi x:A.B}}$ (abs)

${\displaystyle {\Gamma \vdash N:A\quad A=_{\beta }A' \over \Gamma \vdash N:A'}}$ (conv)

Parametriske regler

Følgende regel er parametrisk i ${\displaystyle s_{1},s_{2}\in \{*,\Box \}}$.

${\displaystyle \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 ${\displaystyle (s_{1},s_{2})}$ man som er godtatt. Tabellen under lister opp alle mulighetene.

	Dependent typer	Polymorfi	Typeoperatorer	Forkortelse	Navn
${\displaystyle (*,*)}$				${\displaystyle \lambda ^{\to }}$	Simply typed lambda calculus
${\displaystyle (*,*)}$			${\displaystyle (\Box ,\Box )}$	${\displaystyle \lambda {\underline {\omega }}}$
${\displaystyle (*,*)}$		${\displaystyle (\Box ,*)}$		${\displaystyle \lambda 2}$	System F
${\displaystyle (*,*)}$		${\displaystyle (\Box ,*)}$	${\displaystyle (\Box ,\Box )}$	${\displaystyle \lambda \omega }$	System F${\displaystyle \omega }$
${\displaystyle (*,*)}$	${\displaystyle (*,\Box )}$			${\displaystyle \lambda P}$	LF (Logical Framework)
${\displaystyle (*,*)}$	${\displaystyle (*,\Box )}$		${\displaystyle (\Box ,\Box )}$	${\displaystyle \lambda P{\underline {\omega }}}$
${\displaystyle (*,*)}$	${\displaystyle (*,\Box )}$	${\displaystyle (\Box ,*)}$		${\displaystyle \lambda P2}$
${\displaystyle (*,*)}$	${\displaystyle (*,\Box )}$	${\displaystyle (\Box ,*)}$	${\displaystyle (\Box ,\Box )}$	Coc, ${\displaystyle \lambda C}$, ${\displaystyle \lambda P\omega }$	Calculus of Construction

Egenskaper ved typesystemer

To klassiske egenskaper som typesystemer kan ha er:

• Preservering (eng: subject reduction el. preservation): hvis ${\displaystyle \vdash e:\tau }$ og ${\displaystyle e\to e'}$, så ${\displaystyle \vdash e':\tau }$. Altså, reduksjon bevarer typen.
• Progresjon (eng: progress): hvis ${\displaystyle \vdash e:\tau }$, så er enten ${\displaystyle e}$ en verdi, eller så eksisterer en ${\displaystyle e'}$ slik at ${\displaystyle 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