Peatükk 15 Tüübituletus

Eelmises peatükis nägime, kuidas kontrollida kas mingi Churchi stiilis lambda term on korrektne lihtsalt tüübitud λ-arvutuses. Kuidas aga peaks me selliseid terme saama, näiteks, kui meil on sisendiks Curry stiilis tüüpimata λ-arvutuse term?

Esmalt (lõigus 15.1) vaatame intuitiivset lähenemist, mida on mugav kasutada paberil/tahvlil ülesannete lahendamiseks. Seeljärel (lõigus 15.2) vaatame formaalselt, kuidas tuletada Curry stiilis lambda termile tüüp.

15.1 Intuitiivne tüübituletus lihtsalt tüübitud λ-arvutuses

Tüübituletuse jaoks paneme tähele, et tuletusreeglid on termi struktuuri arvestades paarikaupa üksteist välistavad. Ei saa juhtuda olukorda, kus sama termi puhul saaks rakendada mitut tüüpimisreeglit.

Seega, kui meil on Curry stiilis lambda term e, siis tüübireegli valik ei sõltu kontekstist ega tüübist vaid ainult termi struktuurist — kas see on muutuja, konstant, abstraktsioon või mingite termide rakendus. Seega saame tüüpimisreeglitest puu ehitada jättes lüngad ehk augud tüüpide kohtadele.

Tähtis on aga augud märgendada, et meeles pidada, kuidas aukude väärtusi kopeerima peab. Muutuja ja konstandi reeglites märgendada mõlemad augud vastavalt sama sildiga. Abstraktsiooni reeglis tuleb viis lünka märgendada kahe sildiga: parameetri tüüp ühe sildiga ja tulemustüüp teise sildiga. Aplikatsiooni puhul tuleb neli lünka märgendada kahe sildiga — eristuvad argumendi tüüp ja funktsiooni tulemustüüp.

Näiteks, kui proovime tuletada termi λf. add (f 5) tüüpi, koostame esmalt tüüpimispuu. Puu genereerimine käib alt-ülesse, vaadates järjest, milline reegel rakendub. Näites on termi väliselt abstraktsioon (λf . …) ja selle sees rakendus (add (f 5)) jne. Märgendamiseks valime järjest uusi sümboleid. Tulemus peaks olema järgnev.

Seejärel hakkame täitma lünki ülalt-alla ja kontrollima, kas tüübireeglid ka päriselt kehtivad. Näites kontrollime ja täidame esialgu konstandi lehed. Kuna add on tüüpi Int→Int→Int siis lünka γ tuleb Int ja lünka βtuleb Int→Int. Kuna viis on täisarvuline konstant, siis auk δ tuleb kirjutada Int. Tulemuseks on järgnev puu.

Seejärel näeme, et puudu on ainult auk α tüüp, mille me saame muutuja reeglist. Ehk siis lüngd α täidame tüübiga Int→Int. Seejärel tuleb üle kontrollida kaks aplikatsiooni ja üks abstraktsioonireegel. Kuna kõik on korras, saamegi tulemuseks järgneva puu.

Selle näite puhul tüüpimine õnnestus. Suutsime Curry stiilis λ-termi λf. add (f 5) jaoks intuitiivselt tuletada Churchi stiilis λ-termi λf: Int→Int. add (f 5). Lisaks saime, et selle termi tüüp meile lihtsalt tüübitud konstantidega λ-arvutuses on (Int→Int)→Int→Int.

Mis aga juhtub, kui termile ei vasta konkreetne tüüp? Üks põhjus, miks λ-termile ei vasta konkreetne tüüp, on see, et funktsioonile rakendadakse argument, mis (otse või kaudselt) sinna ei sobi. Näiteks vaatame Curry stiilis termi add ((λx . x) true). Esmalt koostame lünkadega tüüpimispuu.

Märkame konstandi reegli põhjal, et δ peab olema Bool. Seejärel näeme muutuja reegli põhjal, et ka lünk β peab olema tüüpi Bool. Tulemuseks on järgnev puu.

Nüüd tuvastame aga vastuolu. Kuna add peaks olema Int→Int→Int tüüpi konstant ehk funktsioon mis võtab esimeseks argumendiks täisarvu. Tuletamise käigus oleme aga olukorras, kus esimene argument peab olema tõeväärtus ehk tüüpi Bool.

Teine näide termist, millel ei ole lihtsalt tüübitud λ-arvutuses konkreetset tüüpi on identsusfunktsioon λx. x? Vaata järgnevat aukudega tüübipuud.

Siin on tüübid ala-spetsifitseeritud. Muutuja reegli kohaselt tuleb auk α ja auk β täita sama tüübiga aga meile pole keegi öelnud, millist tüüpi sinna valida. Kuna tegemist on vaid intuitiivse lähenemisega, siis võime ka siin intuitsiooni kasutada ja midagi sobivat sinna leida. Aga peame meeles pidama, et selline tuletuskäik ei andnud meile seda unikaalset ainuõiget lahendust. Seega on parem kokku leppida, et loeme sellised tüübituletused ebaõnnestunuks.

Võime otsustada ala-spetsifitseerutud terme mitte vigaseks lugeda põhjendusega, et mingis kontekstis (näiteks termis (λx. x) true) on nendel tüüp olemas. Samas teame, et eneselerakendusega termil λx. x x ei tohiks olla lihtsalt tüübitud λ-arvutuses tüüpi. Tekib küsimus, kuidas tuvastada, kas term on mingis kontekstis tüübitav või mitte. Vaatame termi λx. x x tüübipuud.

Kuna näeme muutuja reegli abil, et aukudes γ ja α peavad alati olema sama tüüp. Seega saame näiteks γ märgendid asendada α-dega. Tulemus on järgnev.

Nüüd näeme teise muutuja reegli põhjal, et augus α peab olema samaaegselt funktsiooni argument ja see sama funktsioon. Säärane olukord on aga võimatu. Ei saa olla konkreetseid tüüpe α ja β, et α ≡ α→β ega α ≡ β→α.

Seega nägime, kuidas eneselerakendusega termis tekkis vastuolu. Ei leidu tüüpe mis rahuldaks tüübikontrolli tingimusi. Seega, sellisel termil ei saa olla tüüpi lihtsalt tüübitud λ-arvutuse termi ühesgi kontekstis. Rääkimata, et sellel oleks tüüp eraldiseisvalt.

15.2 Formaalne tüübituletus lihtsalt tüübitud λ-arvutuses

Üldjuhul võib tüüpide struktuur olla keerulisem, kui lihtsalt tüübidut λ-arvutuses. Näiteks teist-järku λ-arvutuse (ehk λ2) puhul võib tüüp τ olla kujul ∀ α. τ′, kus α on tüübimuutuja ja τ′ mingi tüüp. Näiteks, (∀ α. α→α) → Int on λ2 tüüp. Siis on Curry-stiilis termide tüübituletus ja tüübikontroll lahendamatud ülesanded.

Lihtsamate süsteemide jaoks on tüübituletus võimalik. Näiteks, Hindley-Milner’i tüübisüsteemi (ehk HM) puhul, kus üldsuskvantor on tüübi kõige välimisem osa. Näited HM tüüpidest on identsusfunktsiooni tüüp ∀ α. α → α ning map-i tüüp ∀ α.∀ β. (α→β)→List α→List β.

Paljude praktiliste FP keelte (näiteks Haskell, OCaml, ML, F# jne.) tüübisüsteemide algpunktiks ongi Hindley-Milner’i tüübisüsteemi.

Järgnevalt vaatamegi tüübituletus λ^→ a’la Curry jaoks, ehk lihtsa juhu jaoks, kus tüübid on konstandid, või funktsioonid tüüpide vahel. Algoritm koosneb kolmest sammust.

Esimese sammuna, annoteerime iga alamavaldise ja muutuja sidumise unikaalse tüübimuutujaga. Tüübimuutujad täidavad siin sama rolli, nagu intuitiivse tüübituletuse juures lüngad. Näiteks termi λf. add (f 0) annoteerimise tulemusel saame termi (λf  ^α1. (add  ^α2 (f  ^α3 0^α4)^α5)^α6)^α7.

Annoteerimise tulemusena saame midagi sarnast väidetele aukudega Churchi stiilist termide jaoks, kus kooloni ja lünkade asemel tähistame tüüpe annotatsioonidega. Praegu, aga, ei ole meil tarvis tüüpe ainult abstraktsioonide parameetrite juures vaid lisaks ka kõikide applikatsioonide ja abstraktsioonide tulemuste juures.

Järgmisena defineerime tüüpimisreeglid uuesti annotatsioonide süntaksi jaoks. Pane tähele, et annotatsioonide põhjal ei suuda me alati kohe lõplikult otsustada, kas tüübikontrollis tekkis viga. Annotatsioonideks võib olla tüübimuutuja, mille väärtust me veel ei tea. Seetõttu kogume kokku kõik kitsendused, mis me tüübikontrolli juures tegema pidime.

Teise sammuna, genereerime puu äsja antud tuletusreeglite järgi. Lisaks puule on tulemuseks on termile vastav kitsenduste hulk.

Tuletatud kitsendused on järgnevad.

Kuna kõik kitsendused kogutakse üheks hulgaks, polegi tegelikult mõtet kitsendustega puu loomisel tegeleda. Piisab, kui kirjutame välja kõikide kitsenduste hulga. Näites on kitsendusteks hulk {α2=Int→Int→Int, α1=α3, α4=Int, α3 = α4→α5, α2 = α5→α6, α7 = α1→α6 }.

Kolmanda sammuna on vaja lahendada genereeritud kitsenduste süsteem ja väljastada kogu termile vastav tüüp. Kitsenduste lahendamiseks rakendame kõige üldisema unifitseeria leidmise algoritmi, mis lihtsustusreeglite korduva rakendumise kaudu. Reeglid on järgnevad:

1. Asenda kitsenduste hulgas üks võrdus kujul τ₁→τ₂ = τ₃→τ₄ kahe võrdusega τ₁=τ₃ ja τ₂=τ₄.
2. Olgu võrdus kujul α = τ või τ=α. Kui α∈FV(τ) siis raporteeri viga, vastasel korral asenda kõigis võrdustes α asemel τ.
3. Eemalda tautoloogiad, ehk reeglid, kus võrduse mõlemad pooled on identsed.
4. Kui leidub võrdus τ₁ = τ₂, kus peatüübikonstruktorid on erinevad (näit. Bool=α₁→α₂), siis raprorteeri viga.

Reeglite rakendamisel tuleb jälgida, et ei kaotaks ära kogu termi tüüpi tähistav tüübimuutuja. Näites oli selleks α7.

Näites on algne kitsenduste hulk {α2=Int→Int→Int, α1=α3, α4=Int, α3 = α4→α5, α2 = α5→α6, α7 = α1→α6 }. Esmalt saame asendada kõik α₂ esinemised tüübiga Int→Int→Int, kõik α₃ esinemised muutujaga α1 ning kõik α₄ esinemised tüübiga Int. Peale tautoloogiate eemaldamise saame kitsenduste hulgaks

ehk siis

Asendame α₁ asemele Int→α5 ja eemaldame tautoloogia. Tulemus on

Asendame α₅ asemele Int, α6 asemel Int→Int ning eemaldame tautoloogia. Tulemusena saame kogu termi λf. add (f 0) tähistava annotatsiooni α7 jaoks tüübi α7 = (Int→Int)→Int→Int.