Järgnevalt hakkame uurima üht klassikalist viisi, kuidas spetsifitseerida (konstantidega) λ-termide omadusi. Esmalt vaatame näidet matemaatikast, kus tüüpidega spetsifitseerimine on tavaline.
Kui meil on näiteks polünoom f(x) := x2 +2x − 8, siis me saame öelda et f on funktsioon reaalarvude hulgast reaalarvude hulka ehk f ∈ ℝ → ℝ. See tähendab omadust, et kui funktsioonile f rakendada ükskõik milline reaalarv, siis tulemus on samuti reaalarv. Samas, kui meil on funktsioon g(x) := 10/(x−3) − 13 siis selle funktsiooni tüüp on näiteks g ∈ ℝ∖{3} → ℝ. Ehk siis funktsioon g ei ole defineeritud argumendil 3.
Nüüd tuleb välja tüüpide hea omadus, et me võime ilma funktsioonide definitsioone analüüsimata öelda, et saame g väljundi panna f-i sisendiks, näiteks arvutada f(g(2)). Kui me aga tahame panna g väljundi uuesti g sisendiks, siis me peame analüüsima, kas see sisend on kolm või mitte. Ehk siis, me ei saa arvutada g(g(2)).
Seega pange tähele, et sellised tüübid spetsifitseerivad funktsioone väga piiratult — ainuke omadus, mida tüüp sellisel juhul spetsifitseerib on nõutud sisendi hulk ja väljundite hulk. Samas piisab sellisest spetsifikatsioonist, et välistada nulliga jagamist.
Nüüd vaatamegi, kuidas sarnased tüüpe lisada konstantidega λ-arvutusele, kus tüübisüsteemi esimene eesmärk on välistada redutseerimise kinnijäämise.
Näiteks selline kahtlane term mul 0 true, kus püütakse nulliga korrutada tõeväärtust true. Ühest küljest pole võimalust seda edasi redutseerida aga samas pole tegu ka mõistliku väärtusega.
Tahame saada olukorda, et kui mingi term on tüüpi Int siis selle termi redutseerimise tulemus on täisarvu esitav konstant. Selleks defineerime tüübisüsteemi.
Tüübisüsteem koosneb kolmest komponendist: tüüpide hulk, programmide hulk ja tüüpimisreeglid. Järgnevalt defineerime ühe tüübisüsteemi, mida kutsutakse lihtsalt tüübitud λ-arvutuseks (ehk STLC) ning tähtistatakse λ→.
Klassikaliselt defineeritakse lihtsalt tüübitud lambda arvutuse tüübid järgneva grammatika abil.
|
Ehk siis tüüp võib olla mingi baastüüp, näiteks täisarvutüüp Int või tõeväärtustüüp Bool. Teine alternatiiv on, et tüüp on funktsioon ühest tüübist teise. Näiteks funktsioon Int → Bool või (Bool → Int) → Bool.
Üldiselt eeldame, et igal konstandil on maksimaalselt üks konkreetne tüüp. Näiteks kui võtame 5 : Int siis on välistatud 5 : Bool ja 5 : Nat. Vajadusel on võimalik lisada eraldi konstandid vastavalt tüübile ehk 5Int : Int ja 5Nat : Nat.
Pane tähele, et lihtsalt tüübitud λ-arvutuses pole polümorfseid tüübimuutujaid. Seega pole siin võimalik esitada näiteks cons tüüpi, mis peaks olema iga tüübi α kohta α → List α → List α. Aga listid ja paarid saame hiljem lisada lihtsalt tüübitud λ-arvutuse lisana.
Ka siin kasutatakse sulgude konvetsiooni nagu Idrises, et funktsioonitüübi operaator on paremassotsiatiivne ehk sulud asuvad vaikimisi paremal. Näiteks Bool → Int → Bool on sama tüüp mis Bool → (Int → Bool).
Tüübisüsteemi defineerimiseks peame järgmisena defineerima lihtsalt tüübitud λ-arvutuse programmide hulga. Siin on kaks peamist stiili: Church’i stiil ja Curry stiil.
Church’i stiilis kirjutatakse funktsiooni parameetrite tüübid ilmutatult ehk abstraktsioon on kujul λx : τ. e. Muutujad, konstandid ning applikatsioon kirjutatakse samamoodi kui tüüpimata λ-arvutuses. Lisaks kasutame samu süntaktilisi konventsioone kui puhtas λ-arvutuses. Soovime intuitiivselt, et termil (λx: Int. x) oleks tüüp Int → Int.
Curry stiilis on termid on samad mis tüüpimata λ-arvutuses. Termidel võib olla palju erinevaid tüüpe. Intuitiivselt in korrektne väide nii (λx. x) : Int → Int kui ka (λx. x) : Bool → Bool.
Esmalt kasutame Church’i stiili ehk defineerime lihtsalt tüübitud λ-arvutuse termid järgnevalt.
|
Substitutsioon ja reduktsioon on defineertud analoogselt puhta λ-avutusega ignoreerides tüübiannotatsioone. Näiteks (λx : Int. add 1 x) 6 →β add 1 6 →δ 7.
Selleks, et anda reeglid tüüpide ja termide seostamiseks peame kõigepealt võtma kasutusele abistruktuuri vabade muutujate tüüpide salvestamiseks. Sellist abistruktuuri nimetatakse (tüübi-)kontekstiks ja tähtistatakse tihti tähega Γ. Kontekstiks Γ = {x1:τ1, …, xn:τn} on sisuliselt paaride hulk, kus muutuja xi jaoks on salvestatud tüüp τi.
Korrektses tüüpimisrelatsioonis seab kontekst iga termi vaba muutuja vastausse mingi tüübiga. Kontekst võib kirjeldada ka muutujate tüüpe, mida termis vabalt ei esine. Kindlasti ei tohi kontekstis sama muutuja olla seotud mitme erineva tüübiga. Näiteks termi λx: Int. add x y jaoks sobib konteks Γ1 = {y : Int} ja ka Γ2 = {x: Bool, y : Int} aga mitte Γ3 = {y: Bool, y : Int} Seega konteksti uue seose lisamisel eemaldame vana seose. Näiteks Γ2, x:Int = {x:Int, y:Int}.
Kontekst, term ja tüüp moodustavad koos tüüpimisväite kujul Γ ⊢ e : τ, mida loetakse kui “kontekstis Γ on termi e tüüp τ”.
See, millised väited kehtivad, defineeritakse n.n. tuletusreeglite kaudu. Tuletusreeglid on üldjuhul järgneva kujuga.
Tuletusreeglil on üks järeldus a ja suvaline arv eeldusi b, c, …, z. Viitamiseks on tuletusreeglitel nimi. Kui reeglil ei ole eeldusi, siis nimetatakse seda reeglit aksioomiks.
Lihtsalt tüübitud λ-arvutusel on neli tuletusreeglit, mille järeldused vastavad konstantidega λ-arvutuse termide definitsiooni eri juhtudele. Vaatame järjest kõiki nelja reeglit, alustades muutuja reeglist.
Muutuja reegel (var) on aksioom: muutuja x tüüp on τ kui tema kontekstis on muutuja x seotud just tüübiga τ. Vahemärkusena: mõnes allikas on pole muutuja reegel aksioom — reegli järeldus on sel juhul Γ ⊢ x : τ ning eelduseks tingimus x:τ ∈ Γ.
Konstandi reegel (con): konstant c tüüp on τ kui ta on τ-tüüpi konstant. Sisuliselt on tegemist tautoloogiaga ehk väide Γ ⊢ c : τ kehtib parajasti siis kui me oleme konstandi c sellise tüübiga defineerinud.
Abstraktsiooni reegel (abs): termi λ x : σ. e tüüp on σ → τ kontekstis Γ juhul kui lambda keha e on tüüpi τ kontekstis Γ, x:σ.
Funktsioonirakenduse reegel (app): termi e1 e2 tüüp on τ kontekstis Γ juhul kui argumendi e2 tüüp on σ kontekstis Γ ja funktsiooni e1 tüüp on σ → τ kontekstis Γ.
Tüüpimisväite tõestamiseks peame looma tüüpimispuu eelnevalt vaadatud tuletusreeglitega.
Nüüd saame defineerida tüüpimisväite, mida enne kasutasime intuitiivses mõttes. Programm (ehk kinnine term) e on tüüpi τ ehk e:τ, kui tal on see tüüp tühjas kontekstis ∅ ⊢ e : τ.
Näiteks vaatame, kas termi λ x:Int. mul y (add 5 x) tüüp on Int→Int eeldusel, et y:Int. Vastuse saamiseks tõestame väite Γ ⊢ λ x:Int. mul y (add 5 x) : Int→Int. Tõestuseks konstrueerime järgneva puu, kus Γ = { y:Int } ja Γ1 = { y:Int, x:Int}. Paneme tähele, et siin kasutasime konstante {add, 5}⊆ C ja baastüüpi Int∈τ .
Esitatud lihtsalt tüübitud λ-arvutus defineerib konstantidega λ-arvutuse alamkeele: leidub terme, mis on valiidsed konstantidega λ-arvutuses aga pole valiidne lihtsalt tüübitud λ-arvutuses. Näiteks ei leidu tüüpipuhtal λ-termil (λx. y) (λx. x x) pole
Paaride konstantide ({pair, snd, fst}⊆ C) toetamiseks lisame tüüpide grammatikasse tüüpide korrutise ehk paaritüübi variandi τ1 * τ2. Tulemusena on meil nüüd võimalikud tüübid näiteks Int * Bool ja Int → ((Bool→Int) * (Bool * Bool)).
|
Tüübireeglitele lisame järgnevad kolm reeglit.
Pane tähele, et näiteks termil fst iseseisvalt pole tüüpi ehk lihtsalt tüübitud λ-arvutuses ei saa olla term lihtsalt fst . Põhjus on selles, et fst -le tahame rakendada erinevate tüüpide paare (näiteks nii täisarvude paar Int * Int kui ka tõeväärtuste paar Bool * Bool) aga lihtne tüübisüsteem ei sisalda tüüpi, mis mõlemad juhud kataks. Idrises on palju võimsam tüübimuutujatega tüübisüsteem ning seal saame leida üldise tüübi — fst : (a,b) -> a.
Tüübisüsteemi λ→ laienduses on aga tüüp termil fst e kui e on tüüpi τ1 * τ2. Samuti nõuame, et snd -l oleks argument ning pair -il isegi kaks argumenti. Seega saame reeglitest valmistada puu tõestamaks väidet ⊢ fst (pair 1 true) : Int.
Järgmisena lisame tüüpide grammatikasse kahe tüübi summa ehk tüübi kus saab valida kahe tüübi vahel. Näiteks saame kasutada tüüpi Int + Bool, mis tähendab, et seda tüüpi väärtus sisaldab kas täisarvu või hoopis tõeväärtust. Sellise struktuuri konstantideks on {either, inl, inr}⊆ C.
|
Tüübireeglitele lisame järgnevad kolm reeglit. Konstandid inl ja inr konstrueerivad vastavalt summa tüübi väärtused. Konstant either võtab kolma argumenti, millest esimene on tüüpide summa. Teine argument on funktsioon summa vasakust poolest tüüpi τ3 ning kolmas argument on funktsioon summa paremast poolest tüüpi τ3.
Kasutades tüüpide summat ja korrutis saame konstrueerida suure hulga mitterekursiivseid tüüpe. Selliseid summa ja korrutise abil defineeritud tüüpe nimetatakse algebraliteks andmestruktuurideks. Ehk siis, oleme loonud tüüpide alebra, millega saab esitada kõiki piiratud suurusega tüüpide kompositsioone.
Sellisel tüüpide algebral on ühikelement mis on neutraalne korrutamise suhtes. Lisame tüübisüsteemi ühiktüübi Unit ainsa väärtusega (). Paneme tähele, et konstant () ei sisalda mingit informatsiooni.
Aga miks valisime tüüpide operaatoriteks ’+’ ja ’*’? Vastuse saame, kui analüüsime tüüpide väärtuste arvu. Olgu tüübi τ väärtuste arv |τ|. Näiteks |Unit|=1 ja |Bool| = 2. Saame järgnevad võrdused.
|
Pane tähele, et summa ja korrutise abil ei ole võimalik defineerida rekursiivseid tüüpe. Kui rekursiivsed tüübidefinitsioonid oleks lubatud, saaksime täisarvude tüübiks Nat = Unit + Nat ja listide tüübiks List τ = Unit + (τ * List τ).
Lihtsalt tüübitud λ-arvutusele ei ole kombeks lisada üldist tüüpide rekursiooni, kuna tüübisüsteem on liiga piiratud ja ei toeta kõigi vajalike operatsioonide reeglipärast käsitlemist. Üldine tüüpide rekursioon on näiteks palju võimsama tüübisüsteemiga OCaml keeles. Meie lisame järgmises alampeatükis ühe spetsiifilise rekursiivse tüübipere — listid.
Järgmise lihtsalt tüübitud λ-arvutuse lisana, lisame tüüpide hulka listid. Näiteks saame kasutada tüüpe List Int → List Bool ja List (Int→Int).
|
Probleem tekib aga "funktsiooniga" hd, mis ei ole täielik funktsioon. Seega ei saa me olla kindlad, et kui meil on list l tüübiga List Int siis hd l ei pruugi redutseeruda täisarvuks.
Kui tahame tüübisüsteemiga välistada tühja listi pea võtmise, siis peaksime tüüpide tasandil eristama tühja listi ja mittetühja listi. See pole lihtsalt tüübitud λ-arvutuses üldjuhul võimalik.
Alternatiivina saame võtta konstandiks listide foldr-funktsiooni. Sellega saab kasutaja mittetühja listi puhul arvutada midagi listi pead ja saba kasutades — tingimusel et kood arvestab ka tühja listi juhuga. Defineerime järgnevad reeglid.
Öeldakse, et korrektselt tüübitud programmid ei lähe valesti. See tähendab, et programm kas juba on normaalkujul või saab ta teha reduktsiooni. S.t. välistatud on ebaloogilised sammud, kus tüübi järgi oleks oodatud üks tulemus aga reduktsioon jääb kinni vigasesse seisundisse.
Korrektne tüüpimine koosneb kahest komponendist: progress ja säilitamine. Progress tähendab, et korrektselt tüübitud term ei ole tupikus — ta on kas väärtus või saab teha ühe väärtustusreeglitele vastava sammu. Säilitamine tähendab, et kui korrektselt tüübitud term teeb ühe sammu, siis on ka resultaat korrektselt tüübitud.
Tüüpide säilimise ehk subjekt-reduktsiooni saab kirja panna nii: kui Γ ⊢ e : τ ja e redutseerub termiks e′ siis peab kehtima ka Γ ⊢ e′ : τ. Ehk siis reduktsiooni puhul tüüp säilub. Lihtsalt tüübitud λ-arvutuses säilitab reduktsioon tüübi.
Progressi omadus on järgnev: kui Γ ⊢ e : τ siis kas e juba on väärtus või leidub term e′ nii et e→ e′. Näiteks iga termi e : Bool jaoks teame, et see term juba on väärtus true või false või leidub term e′ nii et e→ e′. Pane tähele, et see, et term oleks õiget tüüpi väärtus, tuleneb tüüpide unikaalusest ja säilimsest.
Tüübikorrektsus on süntaktiline konstruktsioon, mis ei tegele termi sisuga. Seetõttu leidub terme, mis sisuliselt on korrektsed — käituvad vastavalt spetsifikatsioonile, aga pole tüübikorrektsed. Mõned mõistlikud programmid hüljatakse.
Paneme aga tähele, et “ei lähe valesti” ei pruugi tähendada, et läheb õigesti. Puudu jääb tingimus, et reduktsioon tõepoolest termineerub. Seda kutsutakse kirjanduses ka tugevaks normaliseerimiseks
Lihtsalt tüübitud puhas λ-arvutuse hea omadus ongi see, et selle reduktsioon termineerub ehk iga (β-)reduktsiooni jada on lõplik. Termineeruvus on tagatud ka mitmete lisade puhul: tõeväärtused, täisarvud, paarid, tüüpide summad, listid jne. Küll aga pole termineeruvus garanteeritud, kui lisada keelde püsipunktikombinaatorid.
Üks hea tüübisüsteemi omadus on tüüpide unikaalsus: kui kehtivad väited Γ ⊢ e : τ1 ja Γ ⊢ e : τ2 siis τ1 = τ2. See kehtib lihtsalt tüübitud λ-arvutuses aga ei kehti paljudes keerulisemates tüübisüsteemides.
Lihtne näide tüüpide unikaalsuse mittekehtivusest on see kui tüübisüsteemis saab kirjutada termi (λ x. x) ja sellele anda tüübiks nii Bool → Bool kui ka Int → Int. Lihtsalt tüübitud λ-arvutuse puhul on unikaalsus tagatud ka läbi selle, et abstraktsiooni parameetrite tüübid on termis ilmutatult kirjas.
Seega saame järeldada, et termide võrdsuse küsimus on λ→ süsteemis lahenduv ning püsipunktikombinaatorid ei ole defineeritavad.