FUNKTSIONAALPROGRAMMEERIMISE ÕPIK
Kalmer Apinis, Varmo Vene
[Mustand, 21. 8. 2025]
Käesolev materjal on minimalistlik sissejuhatus funktsionaalsesse programmeerimisse nii teoorias kui praktikas.
Sihtgrupiks on algajad informaatika üliõpilased, kellelt ma ei eelda põhjalikke teadmisi programmeerimisest.
Siin raamatus kasutatakse keelt Idris 2 (idris-lang.org) versiooni 0.7.0. Idris keele kompilaatori paigaldamiseks soovitan otsida võmalikult värsket infot ametlikult lehelt (näiteks https://github.com/idris-lang/Idris2/blob/main/INSTALL.md) või järgida ülikooli kursuste võimalikult värskeid õpetusi.
Programmide kirjutamiseks soovitame kasutada VS Codium redaktorit koos Idris keele pluginaga. Sarnaseid pluginaid leidub muuhulgas ka Emacs ja Vim redaktorite jaoks.
Idrise (ehk täpsemalt Idris 2) programm sisaldab definitsioone; igal defineeritaval nimel on tüüp. Näiteks, loome faili Test.idr:
| 1module Test 2 3a : Double 4a = 40.0 5 6b : Double 7b = 30.0 8 9c : Double 10c = sqrt (a*a + b*b) |
Kõik Idrise kood asub moodulites. Idrise testimiseks ei pea moodulit deklareerima — sellisel juhul on mooduli nimeks Main.
Tavaliselt peaks mooduli nimi ühtima faili nimega ehk kui meil on fail Test.idr, siis peaks me see fail algama näiteks reaga module Test. Suuremates programmides võivad moodulid paikneda hierarhiliselt pakettide sees. Näiteks tõeväärtustega arvutamise funktsioonid on kataloogis Data failis Bool.idr ning see fail algab reaga module Data.Bool. Etteruttavalt, nende abifunktsioonide kasutamiseks tuleks need meie moodulisse importida käsuga import Data.Bool.
Kooloniga tähistakse mingi nime või väärtuse tüüpi. Kui kirjuame a : Double, siis seda loeme kui "a tüüp on Double". Uue nime defineerimisel tähendab võrdusmärk defineerimist, ehk kui kirjutame a = 40.0 siis seda loeme kui "a väärtus on definitsiooni järgi 40.0". See tähendab, et a väärtuseks on ujukomaarv 40.0 väärtus. Täpsemalt räägime väärtustamisest peatükis ??.
Sarnaselt a-le defineeritakse ujukomaarv b väärtusega 30.
Kuid c on küll ujukomaarv aga definitsiooniks on sqrt (a*a+b*b) ehk ruutjuur a ja b ruutude summast.
Sellise faili saab lugeda Idris-e REPL-sse (inglise keelest read-eval-print-loop).
| % idris2 Test.idr ____ __ _ ___ / _/___/ /____(_)____ |__ \ / // __ / ___/ / ___/ __/ / Version 0.7.0 _/ // /_/ / / / (__ ) / __/ https://www.idris-lang.org /___/\__,_/_/ /_/____/ /____/ Type :? for help Welcome to Idris 2. Enjoy yourself! 1/1: Building Test (Test.idr) Test> |
Esmalt kutsume käsurealt välja idris2 REPL-i andes argumendiks loodud faili Test.idr. Idris laeb definitsioonid sisse ja teostab tüübikontrolli. Lõpuks jääb Idris kasutaja edasisi käske ootama. Saame näiteks anda Idrisele ülesandeks väärtustada ujukomaarv c. Tulemuseks peaks tulema 50.0 nagu näha järgnevas väljatrükis.
| Test> c 50.0 Test> :q |
Peale c arvutamist ja väljatrükki tahame Idrise sulgeda — anname käskluse :q .
Praktilises programmeerimiskeeltes (alustades Algolist, 1958) hakati tüüpe kasutama vajamineva mälu arvestamiseks ja mäluaadresside arvutamise jaoks. Massiivi indekseerimise jaoks oli tarvis teada, kui palju mälu võtab üks element.
Tüübiteoorias (Bertrand Russell, 1908) kasutati tüüpe, juba 50 aastat varem, loogika süsteemi ja loogika valemite kooskõlalisuse tagamiseks ja Russell’i paradoksi vältimiseks. Mingi valem on selles loogikas lubatud vaid siis kui sellel on tüüp — mis tähendab, et selle kooskõlalisus on kontrollitud.
Idrise (ja funktsionaalprogrammeerimise tüübid üldiselt) tulevad rohkem tüübiteooriast. Idris 2 keel ongi ühe väga võimsa tüübiteooria implementatsioon — sellega saab nii programmeerida kui ka mingil määral tõestada. Esmalt vaatame aga selles keeles programmeerimist.
Lihtsustatult võib mõelda, et tüübid vastavad mingile väärtuste hulgale. Näiteks, on Idrises tõeväärtuste tüüp Bool, mis tähendab, et kui miski on tüüpi Bool, siis see on kas tõene ehk True või väär ehk False. Rohkem variante ei ole. S.t. mingi Bool tüüpi avaldise väärtustamine võib võtta väga palju samme aga tulemus on lõpuks ikka kas True või False. Näiteks: False : Bool.
Lisaks tõeväärtustele on Idrises rida erinevaid täisarvutüüpe, millest kõige rohkem kasutatavad on Int ja Integer. Suures pildis on Int tüüpi väärtused 64-biti sisse mahtuvad (pluss või miinus-)märgiga täisarvud ja Integer tüüpi väärtused on suvalise pikkusega (piiratud arvuti mälu mahuga) (pluss või miinus-)märgiga täisarvud. Näiteks: -10 : Int ja 90000000000000000000 : Integer.
Tüüp Double väärtused on 64bitised (IEEE 754 standard) ujukomaarvud. Tüüp Char väärtused on Unicode sümbolid ja tüüp String väärtused on sõned. Näiteks: 5.5 : Double, 'x' : Char ja "tekst" : String .
Mõned tüübid on parametriseeritud tüüpidega; näiteks List Bool, Maybe Int. Selliseid juhte vaatame hiljem detailselt aga esialgu võite meelde jätta, et ilma parameetrita List on tüübipere ja koos parameetriga List Int on tüüp mille väärtusteks on listid ehk järjendid Int tüüpi elementidest. Näiteks: [True, False] : List Bool.
Idris on puhas funktsionaalne programmeerimiskeel, mis tähendab, et selles on muutumatud (i.k. immutable) definitsioonid ja parameetrid. Pole muutujaid, millele saaksime omistada uue väärtuse. Me küll ütleme parameetrite kohta "muutuja" aga vaid selles mõttes, et funktsiooni erinevatel väljakutsetel võivad parameetri väärtused olla erinevad. Või näiteks ütleme mõne standard-teegi definitsiooni kohta "muutuja", kuna kompilaatori järgmises versioonis võib definitsioon olla natukene muutunud.
On mitu võimalust, et kontrollida kas mingi nimi või avaldis on mingit konkreetset tüüpi. Esiteks võib Idriselt avaldise või nime tüüpi küsida käsuga ":t <avaldis>".
| Test> :t a Test.a : Double Test> :t sqrt (a*a + b*b) sqrt ((a * a) + (b * b)) : Double |
Näeme, et mooduli Test nimi a on Double tüüpi ja avaldis sqrt (a*a + b*b) tüüp on samuti Double.
Mõnel juhul on pole see viis ideaalne. Näiteks, kui tahame teada kas on arv 1 sobib Double tüüpi nime väärtuseks. Idris vastab, et 1 tüüp on Integer. Mis sellest siis arvata? Parem on seda kontrolli teha kutsudes välja the Double 1. Avaldis 1 sobib tüübiga Double, seetõttu tagastatakse Double tüüpi väärtus 1. Seevastu, avaldis 1.5 ei sobi tüübiga Int ja tuleb tüübiviga. (Selle tüübivea põhjust ja detaile võite uurida peale liideste peatüki lugemist.)
| Test> :t a Test.a : Double Test> :t 1 1 : Integer Test> the Double 1 1.0 Test> the Int 1.5 Error: Can't find an implementation for FromDouble Int. (Interactive):1:9--1:12 1 | the Int 1.5 ^^^ |
Seost f mingite hulkade X ja Y vahel nimetatakse matemaatikas funktsiooniks, kui iga hulga X element on seoses ühe hulga Y elemendiga. Sellisel juhul kirjutatakse matemaatikas f ∈ X→ Y. Funktsiooni f lähtehulka X nimetatakse ka määramispiirkonnaks ehk domeeniks ja sihthulka Y nimetatakse kodomeeniks.
Näiteks funktsioon f∈ ℝ→ ℝ, mis on defineeritud võrdusega f(x) = x2 seab iga reaalarvu x∈ ℝ vastavusse tema ruuduga x2∈ ℝ. Paneme tähele, et negatiivsed reaalarvud ei ole saavutatavad — pole reaalarvu y mille korral f(y) oleks −1. Seega, saaksime kodomeeniks valida ka mittenegatiivsed reaalarvud, ehk f∈ ℝ→ ℝ≥0.
Sarnaselt matemaatilisele hulga notatsioonile kasutatakse funktsionaalprogrammeerimises funktsiooni tüübiks konstruktsiooni "α -> β", kus α on argumendi tüüp ja β funktsiooni tagastustüüp. Näiteks on Idrises tüüp Int -> Bool. Nii argument kui ka tagastustüüp võivad ise olla funktsioonid — sellist funktsiooni nimetatakse kõrgemat järku funktsiooniks. Näieks (Int -> Bool) -> (Int -> Bool).
Funktsioon tüübiga (Int -> Bool) -> (Int -> Bool) on sisuliselt kahe argumendiga funktsioon, kuna ta vajab üht argumenti tüübiga Int -> Bool ja lisaks teist argumenti tüübiga Int, et tagastada tõeväärtust.
Sulgude vähendamise eesmärgil on funktsioonitüübi nool paremassotsiatiivne ehk sulgude puudumisel pannakse sulud vaikimisi paremale. S.t., et parempoolsed sulud võib panemata jätta. Näiteks tüüp (Int -> Bool) -> (Int -> Bool) on sama mis (Int -> Bool) -> Int -> Bool. Valik paremassotsiatiivuses kasuks tuleneb sellest, et mitme argumendiga funktsioonid on tavalisemad kui funktsioonid mille parameeter on ise funktsioon.
Matemaatikas on funktsioonid täielikud. Näiteks, kuna funktsioon f(x) = 1/x ei oma sobilikku mõtet x=0 puhul, jäetakse null lihtsalt määramispiirkonnast välja, ehk kirjutatakse f ∈ ℝ∖{0} → ℝ.
Erinevus tavalise matemaatika ja tüübiteooria vahel on see, et tüüpidel on rangemad piirangud võrreldes hulkadega (selleks et välistada Russelli paradoksi). Seetõttu tüübid ja väärtused defineeritakse koos, mitte ei kombineerita olemasolevaid väärtusi uuteks tüüpideks — nii nagu hulkade puhul oleme harjunud tegema.
Ujukomaarv 0 (ehk 0.0) pole tüübiteoorias sama objekt kui täisarv 0. Seetõttu peab funktsiooni defineerimisel olema selge, mis tüüpi objekti mõeldakse — näiteks, kas funktsiooni defineerimisel kasutatud 0 peaks olema täisarv, ujukomaarv või hoopis midagi muud. Seetõttu on uute tüüpide defineerimine tülikam kui matemaatikas tavaliselt — tüütum on defineerida tüüp reaalarvude jaoks, mis ei sisalda nulli. Paljud praktilised funktsionaalsed programmeerimskeeled lubavad seetõttu mittetäielikke funktsioone.
Funktsiooni f : X -> Y mittetäielikus võib tähendada kahte juhtu või nende kombinatsiooni. Esiteks, võib olla süntaktiliselt selge, et funktsioon pole defineeritud mingil väärtusel x : X. Sellisel juhul f(x) väärtustamine jääb kinni (ing. k. stuck), ja enamasti praktikas väljastatakse mingi veateade. Teine võimalus on, et funktsioon on defineeritud rekursiooni abil kuid pole selge, et sellise rekursiooni väärtustamine termineerub. Mõlemal juhul pole garanteeritud, et funktsioon seab iga argumenditüübi väärtusele vastavusse mingi konkreetse tulemustüübi väärtusega.
Tüübisüsteem, mis lubab ilma piiranguteta kasutada mittetäielikke funktsioone, ei saa seega garanteerida, et avaldis e : T väärtustub mingiks T-tüüpi väärtuseks. Kõik garantiid kehtivad vaid eeldusel, et e väärtustamine termineerub ega jää kinni.
Osadel funktsionaalsetel programmeerimiskeeltel (näiteks Haskell ja OCaml) on funktsiooni parim tüüp automaatselt tuletatav ja seda ei pea koodi ise sisse kirjutama. Idris 2 on läinud teist teed — funktsiooni tüübi kirjutamist nõutakse. Seetõttu saavad tüübid olla teiste keeltega võrreldes keerulisemad ja täpsemad.
Matemaatikas on tavaline, et funktsioonikutse on süntaksiga f(x1,x2,…,xn) ehk süntaktiliselt kõigepealt funktsiooni nimi ja siis argumendid sulgudes ja komadega eraldatult. Näiteks max(5,10).
Idrises (ja paljudes teistes funktsionaalsetes keeltes) seevastu kirjutatakse funktsioon ja tema argumendid üksteise järele. Kui funktsiooni argumendiks on mingi keerukam avaldis, võib olla vajalik selle paigutamine sulgudesse. Vt. järgnevat tabelit.
Üldiselt funktsioon f(x1,x2,…,xn) kirjutatakse Idrises
f(x1)(x2)…(xn), kus
xi ümbert võib lihtsamal juhul sulud ära jätta.
Tehniliselt, avaldisi parsitakse nii, et funktsioonirakendus seob kõige tugevamini võrreldes teiste operaatoritega. Kui olete kirjutanud avaldise a b + c d siis Idris loeb seda kui funktsioonirakenduste a b ja c d summat. Kui soovite a-le rakendada b ja c summat ning d-d, peate kirjutama hoopis a (b + c) d.
Idrise süntaks erineb tavalisest matemaatilisest kirjaviisist kuna tahetakse soodustada kõrgemat järku funktsioonidega arvutamist. Keele kasutamine peaks olema mugav ka siis kui funktsioonid saavad argumendiks ja/või tagastavad funktsioone.
Mitme argumendiga funktsioonid on Idrises ja paljudes teistes funktsionaalsetes keeltes lahendatud nii, ühe argumendiga funktsioon tagastab funktsiooni, mis võtab järgmise argumendi. See on nii näiteks funktsiooni g : Bool -> Int -> Bool puhul. Saame anda funktsioonile tema esimese argumendi ja saada tagasi funktsiooni, mis ootab järgmist argumenti. Näiteks g True : Int -> Bool.
Lisaks on ka tavaline juhtum, kui funktsioon võtab argumendiks mingi muu funktsiooni. Näiteks h : (Int -> Bool) -> String saame välja kutsuda h (g True) ning tulemus on tüüpi String.
Mitme argumendi rakendamist parsitakse tehniliselt vasakassotsiatiivselt ehk max 5 10 parsitakse kui (max 5) 10. See tähendab, et sisuliselt rakendatakse funktsioonile argumente ükshaaval.
Funktsioonirakenduse vasakasotsiatiivsus ja funktsioonitüübi paremassotsiatiivsus töötavad koos nii, et mitmeargumentiliste funktsioonide puhul lisasulge vaja ei ole.
| ehk |
|
Funktsioone defineeritakse võrdusmärgiga kasutades formaalsed parameetrid. Näiteks järgnev kahe argumendiga funktsioon pyth, mis arvutab ujukomaarvudega täisnurkse kolmnurga hüpotenuusi pikkust kaatetite pikkuse järgi.
Idrise kompilaator teostab definitsioonidel tüübikontrolli. Paremaks pooleks olev avaldis peab vastama tüübile, arvestades parameetreid. Kasutada võib parameetreid, koodis varem (ehk ülevalpool) defineeritud nimesid ja defineeritavat nime ennast (rekursioon). Näiteks pyth puhul peab kontrollima, kas sqrt (x*x + y*y) on tüüpi Double kui lokaalselt eeldada, et x : Double ja y : Double. Tüüpimine sõltub siin sellest, kuidas on defineeritud sqrt, + ja *.
Peale definitsiooni tüübikontrolli saab vastavat nime avaldistes kasutada. Näiteks, 2*(pyth (2+1) 4). Tingimus on, et tegelik argument vastaks funktsiooni argumendi tüübile. Kuna pyth võtab kaks Double tüüpi argumenti, peame kontrollima, et 2+1 : Double ja 4 : Double. Eeldusel, et ujukomaarve saab liita ja korrutada, saame et näite tüüp on tõepoolest Double.
Funktsiooni tähendus tuleb tema definitsioonist. Kui mõnes avaldises on vaja väärtustada funktsioonikutset, siis asendatakse funktsioonikutse definitsiooni parema poolega, kus formaalsed parameetrid on asendatud vastavate tegelike argumentidega, ja väärtustatakse tulemust edasi.
|
Seni oleme näinud, kuidas defineerida tavalisi funktsioone, kus funktsiooni nimi on vasakul ja tema argumendid paremal. Seda kutsutakse prefix rakenduseks, kuna funktsioon on enne argumente. Näiteks min 3 1.
Aritmeetikas on aga tavaks ka infixsed operatsioonid, kus funktsioon on argumentide vahel. Näiteks liitmine 1+2 ja korrutamine 2*3.
Infix operaatorid Idrises on definitsioonid mis koosnevad ainult järgnevatest sümbolitest: :+-*\/=.?|&><!@$%~^# . Sellisel juhul saab neid programmides kasutada infixselt ehk argumnentide vahel. Näiteks: 5+2, 2*pi*r*r.
Infix operaatori kasutamiseks prefix-vormis tuleb panna see operaaror sulgudesse. Näiteks: 3 + 4 on sama mis (+) 3 4.
Infix operaatoril on prioriteetide (i.k. precedence) tasemed, mis näitavad operatsioonide vaikejärjekorda. Mida kõrgem on tase, seda tugevamalt operaator vaikimisi (ehk sulgude puudumisel) seob. Näiteks: 3*4+5 == (3*4)+5, kuna * on tasemel 9 ja + tasemel 8.
Infix operaator võib olla parem- või vasakassotsiatiivne. Näiteks tõeväärtuste konjuntksioon && on paremassotsiatiivne, ehk operaatori mitmekordsel rakendamisel pannakse sulud paremale. S.t. a && b && c on sama mis a&&(b&&c).
Paremassotsiatiivsuse on konjunktsiooni puhul tähtis, kuna seetõttu kontrollitakse a && b && c arvutades kõigepealt a tõeväärtust — ja kui see on väär tagastatakse väär ilma b-d ja c-d väärtustamata. Lahutamine on Idrises vasakassotsiatiivne, ehk sulgude puudumisel seob tugevamalt vasakpoolseim lahutusoperaator. Näiteks 4-3-2 on sama mis (4-3)-2 ehk selle väärtus on -1 .
Infix operaatori prioriteete ja assotsiatiivsust seatakse nn. fixity deklaratsioonidega. Paremassotsiatiivseks seab võtmesõna infixr, vasakassotsiatiivsust võtmesõna infixl ning mitteassotsiatiivseks võtmesõna infix. Võtmesõnale järgneb prioriteet ja komadega eraldatud võtmesõnade nimekiri. Näiteks:
| 1 infixl 8 +, - 2 infixl 9 *, / 3 infixr 5 && |
Prefix operaatoreid saab rakendada infix-selt tagurpidi-ülakomade ( `) vahel. Näiteks: 5 `div` 2 või siis 5 `max` 2.
Idrise süntaksis asuvad definitsioonid loogilistes blokkides, kusjuures samas blokis olevad definitsioonid peavad algama samalt veerult.
Mooduli Test deklaratsioonid alata suvaliselt, näiteks viiendalt, veerult.
| 1module Test 2 a : Double 3 a = 40.0 4 b : Double 5 b = 30.0 6 c : Double 7 c = sqrt (a*a + b*b) |
Mõnikord on funktsiooni definitsiooni selguse mõttes mõistlik struktureerida nii, et kasutada abifunktsioone ja vaheväärtuseid. Selleks on kaks peamist võimalust. Esimene võimalus on n.n. let-in konstruktsioon, mis võimaldab anda lokaalseid definitsioone avaldise sees — enne kui avaldise sisuga jätkatakse. Vaata järgnevat koodi.
| 1koonuse_ruumala : Double -> Double -> Double 2koonuse_ruumala r h = 3 let ringi_pindala : Double -> Double 4 ringi_pindala r = pi * r * r 5 in 6 ringi_pindala r * h / 3 |
Vaatame koonuse ruumala arvutamise funktsiooni koonuse_ruumala. Funktsiooni keha algab let võtmesõnaga, mis tähendab, et järgneb abimuutujate/funktsioonide blokk. Näites kasutame abifunktsiooni ringi_pindala. Peale abifunktsioone tuleb võtmesõna in ning jätkub koonuse_ruumala funktsiooni definitsioon, mis kasutab defineeritud abifunktsiooni.
Taanetega grupeerimise üldine loogika on see, et taande vähenemist loetakse eelneva(te) blokkide lõpetamiseks, ja taande suurenemist loetakse uue bloki alustamiseks Sama bloki jätkamiseks peab see algama samalt veerult.
Tuleme tagasi koonuse ruumala näite juurde. Abifunktsiooni ringi_pindala tüübideklaratsioonid ja definitsioonid peavad olema sama taandega; kusjuures see taane peab olema suurem kui välise definitsiooni koonuse_ruumala taane. Lisaks on tähtis, et koonuse_ruumala parema poolega seotud read oleks koonuse_ruumala definitsiooni taandest suurema taandega.
Teine võimalus abifunktsioonide defineerimiseks on where-konstruktsiooniga. See võimaldab abifunktsioonid paigutada peale definitsiooni andmist.
| 1koonuse_ruumala' : Double -> Double -> Double 2koonuse_ruumala' r h = ringi_pindala r * h / 3 where 3 ringi_pindala : Double -> Double 4 ringi_pindala r = pi * r * r |
Funktsiooni koonuse_ruumala' parem pool algab avaldisega ringi_pindala r * h / 3 mis, kasutades abifunktsiooni ringi_pindala, arvutab koonuse ruumala. Seejärel tuleb võtmesõna where, millele järgneb blokk defineeritavate abifunktsioonidega.
Valik, kas kasutada let-in või where konstruktsioponi, on suuresti maitse küsimus. Siiski on neil üks erinevus — lihtsalt väärtuse defineerimisel ei pea let-iga spetsifitseerima tüüpi vaid saab kohe anda definitsiooni. Vaata järgnevat koodi näitena, kuidas kasutada nii let-in kui ka where konstruktsiooni korraga.
| 1koonuse_ruumala'' : Double -> Double -> Double 2koonuse_ruumala'' r h = 3 let sp = ringi_pindala r in 4 sp * h / 3 5 where 6 ringi_pindala : Double -> Double 7 ringi_pindala r = pi * r * r |
Ka siin peavad abifunktsiooni ringi_pindala tüübideklaratsioonid ja definitsioonid olema sama taandega; kusjuures see taane peab olema suurem kui välise definitsiooni koonuse_ruumala taane. Lisaks on tähtis, et koonuse_ruumala parema poolega seotud read oleks koonuse_ruumala definitsiooni taandest suurema taandega. Kõik muud taanded on dekoratiivsed ja programmeerija vaba valik.
Järgneb natuke pikem näide, mis arvutab sõnes leiduvate sõnade keskmist pikkust. See näide kasutab funktsiooni words, mille kasutamiseks peame importima Data.String mooduli. Funktsiooni sisu ja sellest arusaamine pole sel hetkel oluline. Vaatame abimuutujate ja abifunktsioonide taandeid. Siin peavad nii let-i abimuutujad ja where-i abifunktsioonid olema oma blokis sama taandega; kusjuures see taane peab olema suurem kui välise definitsiooni average taane. Lisaks on tähtis, et average parema poolega seotud read oleks average definitsiooni taandest suurema taandega.
| 1average : String -> Double 2average str = let numWords = wordCount str 3 totalLength = sum (allLengths (words str)) in 4 cast totalLength / cast numWords 5 where 6 wordCount : String -> Nat 7 wordCount str = length (words str) 8 allLengths : List String -> List Nat 9 allLengths strs = map length strs |
Suures pildis on puhas λ-arvutus üks minimaalne ja täielik arvutusmudel. Sellistest formaalsetest arvutusmudelitest on λ-arvutus kõige lähedasem tavamõttes programmeerimisele. Lisaks oli see esimene selline mudel. Vaatame nüüd täpsemalt.
Formaalne arvutusmudel on matemaatiline süsteem, kus saab kirjeldab mingit hulka algoritme ja näidata, kuidas selles mudelis antud algoritm antud sisendite puhul väljundini jõuab. Näiteks on lõplikud olekumasinad formaalne arvutusmudel, millega saab arvutada sõne vastavust regulaaravaldisele. Veel üks tuntud formaalne arvutusmudel on Turingi masin, mida kasutatakse arvutatavuse teooria teoreetilistes tõestustes.
Praktikas võib väita, et suvaline konkreetne arvuti on arvutusmudel, aga praktilised arvutid pole minimaalsed ega teoreetilises mõttes täielikud. Lihtsa algoritmi töö üle arutlemine konkreetsel arvutil on väga palju keerukam, kuna arvuti keerukus lisandub algoritmi keerukusele.
Mitteformaalselt võib arvutusmudeliks nimetada ka suvalist progamemerimiskeelt, kui selle keele programmide väärtustamine on piisavalt täpselt defineeritud. Formaalses arutluses on parem kui keel oleks väike ja selge kuid samas lubaks algoritmide kirjeldamist võimalikult lühidalt. Java ja Pythoni kompilaatorites kasutatakse arvutusmudelina vastavat baitkoodi ja virtuaalmasinat.
Puhas λ-arvutus on arvutusmudel, mis koosneb väga vähestest osadest ja väga vähestest reeglitest. Siiski on see täielik — kõik efektiivselt arvutatavad funktsioonid on arvutatavad puhtas λ-arvutuses (Church-Turingi teesi järgi).
Vaatame esmalt üldisemat mudelit — konstantidega λ-arvutust, mis on saadud mingi hulga konstantide lisamisega puhtale λ-arvutusele.
Konstantide idee seisneb selles, et me soovime praktikas kasutada protsessori poolt pakutavaid väärtuseid ja nende operatsioone. Näiteks 64-bitiseid täisarve ja ujukomaarve.
Hiljem näeme, et puhta λ-arvutusega on võimalik implementeerida kõik vajalikud andmestruktuurid ja konstantide kasutamiseks teoreetiline vajadus puudub. Praktikas on muidugi protsessori aritmeetika väga palju kiirem kui selle implementatsioon puhtas λ-arvutuses.
Avaldisi λ-arvutuses kutsutakse termideks. Termide hulk Λ on defineeritud induktiivses vormis järgneva nelja reegliga.
Kirjanduses kasutatakse ka järgnevat (samaväärset) süntaktilist definitsiooni λ-termide jaoks.
|
λ-termidest mõelge kui programmikoodist. Varsti näeme, kuidas λ-arvutus arvutab termile t vastava väärtuse v — seda kirjutame kui t ↠ v. Hetkel võtke lihtsalt teatavaks, et väärtuse arvutamine käib samm-haaval ja väärtus ise on term, kus ühtegi sammu teha ei saa. Ehk siis λ-termid kodeerivad nii ülesande püstitust, vahepealseid seisundeid kui ka lõpptulemust.
Enamasti kasutame muutujateks ladina tähti näiteks a, b, c või x, y ja z. Kui muutuja on mõeldud tähistama funktsiooni siis kasutame aga näiteks f, g või h. Vajadusel kasutame ka pikemaid muutujanimesid, näiteks parem või vasak.
Näiteks on λ-termid muutujad x ja f. Sellisel juhul mõelge muutujatest x või f nagu globaalsetest muutujatest — s.t. nende muutujate tähendus peab tulema välisest kontekstist ja üldiselt ei saa me midagi muud nende kohta arvata. λ-arvutuses kutsutakse globaalseid muutujaid vabadeks muutujateks.
Abstraktsioon on funktsioon. Kui e on term, siis (λx. e) on (ilma nimeta) funktsiooni definitsioon, mille formaalne parameeter on x ja mille keha on term e. Abstraktsiooni (λx. e) keha e sees olevaid parameetri x esinemisi nimetatakse seotud muutujakas — selle väärtus ei tulene välisest kontekstist vaid hoopis funktsiooni argumendi väärtusest. Detaile vaatame hiljem aga üldjoontes, kui sellele funktsioonile λx. e anda argument, siis funktsiooni tulemus arvutatakse funktsiooni keha e järgi, võttes kehas vaba muutuja x asemel tegeliku argumendi.
Kõige lihtsam funktsioon λ-arvutuses on identsusfunktsioon ehk term λx. x, kus funktsiooni kehaks on sama muutuja x mis on funktsiooni formaalseks parameetriks. Kui funktsiooni keha x eraldiseisvalt vaadata, siis on tegemist vaba muutujaga. Abstraktsioon seob aga keha sees olevad vabad muutujad enda parameetriga. Ehk termis λx. e on muutuja x seotud. Intuitiivselt näeme, et tegemist ongi identsusfunktsiooniga, kuna ta igal juhul tagastab oma argumendi muutmata kujul. Pane tähele, et ka λy. y on identsusfunktsioon.
Aplikatsioon on funktsioonirakendus. Kui term f väärtustub funktsiooniks siis iga termi t puhul term (f t) väärtustub selle funktsiooni tulemuseks, kui funktsiooni argumendiks võtta termi t väärtus.
Näiteks on λ-termid (f x) ja ((λx. x) y). Esimesel juhul on funktsiooniks vaba muutuja f ja argumendiks vaba muutuja x. Teisel juhul on funktsiooniks identsusfunktsioon (λx. x) ja argumendiks vaba muutuja y. Erinevalt y-st pole x termis ((λx. x) y) vaba muutuja ja arvutuse tulemus ei sõltu sellest, mis on globaalse muutuja x väärtus.
Üldiselt võime konstantideks võtta suvalise hulga väärtuseid ja operatsioone nendel väärtustel — tingimusel, et need konstandid on eristatavad abstraktsioonist, aplikatsioonist ja muutujatest.
Näiteks, kui võtame C := ℕ ∪ { add } siis on term (λx. ((add 10) x)) võiks näiteks esitada funktsiooni, mis liidab oma argumendile juurde kümme.
Enne võimalike konstantide valimist, vaatame kuidas vähendada sulgude arvu.
Termid moodustavad puustruktuuri ja puustruktuuri esitamiseks tekstis on tavaks kasutada sulge. Kui tahame struktuuri üles kirjutada nii selgelt kui võimalik, oleks mõistlik kasutada minimaalsel arvul sulge. Selleks kasutame kirjanduses tavaks saanud reegleid, mida tuleks lugeda nii, et kui me kirjutame nii nagu vasakul, siis me mõtleme sama termi nagu paremal. Ehk mõlema kirjapildi abil mõtleme sama asja.
|
Kirjanduses on tavaks, et aplikatsioon on vasakassotsiatiivne, ehk rohkem kui kahe järjestikuse aplikatsiooni puhul on sulud vaikimisi vasakul. Seega vaikimisi eeldame, et funktsioonile rakendatakse mitu argumenti, mitte et see sisaldab mitut funktsiooni.
Veel on tavaks, et abstraktsioon seob nii pikalt paremale kui võimalik. Sulgude puudumisel on kõik peale punkti seotud abstraktsiooniga.
Kolmas reegel lubab üksteise sees asuvaid abstraktsioone kirjutada ühe λ-sümboliga.
Näited λ-termidest:
Esiteks võtame konstantideks tõeväärtused true ∈ C, false ∈ C ning tingimusfunktsiooni cond ∈ C. Aga lisaks peame ka näitama, kuidas nendega arvutus toimub.
Konstantide arvutusreeglid antakse λ-arvutuses δ-reeglitega, mis on lihtsustusseos termide vahel. Kui kirjutada e1 →δ e2, siis see tähendab, et term e1 lihtsustub termiks e2 vastavalt konstantide reeglitele.
Kui tingimusavaldisele on rakendatud kolm argumenti millest esimene on tõeväärtus true , siis on tulemus teine argument. Aga kui tingimusavaldisele on rakendatud kolm argumenti millest esimene on tõeväärtus false , siis on tulemus kolmas argument.
Ehk kõigi termide e1 ka e2 jaoks kehtib
|
Näiteks on term cond true false true . See term redutseerub termiks false ühe δ-reduktsiooni sammuga. Term cond true (cond false false true) true redutseerub ühe sammuga termiks cond false false true ning järgmise sammuga termiks true .
Mitme sammuga redutseerumist kirjutatakse ka järgnevalt.
|
Joonisime alla redutseeritava termi e. reedeksi — kõik mis pole allajoonitud jääb samaks. Viimases näites redutseerisime tervet termi korraga.
On tavaks, et λ-arvutuses lubatakse reduktsiooni käib sügavamal termis — lihtsustus võib toimuda samahästi väljaspool kui ka seespool. Ehk, kui t1 → t2 siis iga u∈Λ ja x∈ V korral. See kehtib nii δ- kui ka muude reduktsioonide kohta.
|
See tähendab, et võib redutseerida ka teises järjekorras. Näiteks cond -i teine argument enne.
|
Enamasti tahame, et tulemus ei sõltuks lihtsustussammude järjekorrast. Peame olema reduktsiooni defineerimisel ettevaatlikud!
Edasi võtame konstantide hulka protsessori poolt toetatud (näiteks 64bit) täisarvud Int ⊂ C. Lisaks aritmeetika baastehted liitmine add ∈ C, lahutamine sub ∈ C, korrutamine mul ∈ C ja võrdlemine nulliga iszero ∈ C .
Reduktsioon vastab protsessori käitumisele. Vaata järgnevaid näiteid.
Seni oleme vaadanud baasandmetüüpe: tõeväärtused ja täisarvud. Kuidas aga teha abstraktseid andmetüüpe — näiteks paare?
Lisame konstandid pair ∈ C, fst ∈ C ja snd ∈ C paaride jaoks. Näiteks on termideks pair x y, fst x ja snd (pair x y).
Ehk kõigi termide e1 ka e2 jaoks kehtib
|
Vaata järgnevaid näiteid.
Nüüd lisame konstandid listide jaoks. Listid on rekursiivne abstraktne andmestruktuur. Lisame konstandid nil ∈ C, cons ∈ C ning null∈ C, hd∈ C ja tl∈ C. Näiteks on termideks nil, cons x nil, nil ja hd (cons x nil).
Kõigi termide e1 ka e2 jaoks kehtib
|
Vaata järgnevaid näiteid.
Eelnevad näited käsitlesid positiivseid juhte, kus argumendid olid just parajad, et tuleks mõistlik tulemus. Mis juhtub aga muul juhul? Vastus: muul juhul lihtsustada ei saa ja term jääb selliseks nagu ta on. Vaata järgnevaid näiteid, mis on δ-normaalkujul ehk rohkem samme teha ei saa.
Võrreldes praktiliste programmeerimiskeeltega kaob λ-arvutuses ülevaatlikus, kuna termid tulevad tihti väga pikad. Pole mooduleid ega globaalseid definitsioone, kus saaks hoida valmis algoritme ja funktsioone.
Üks võimalus globaalsete definitsioonide kasutamiseks ilma konstruktsioonide lisamiseta λ termide definitsiooni on kasutada makrodefinistioone. See tähendab seda, et definitsioonid asendatakse termi enne redutseerimise sammudega alustamist.
Näiteks võime defineerida kuulsad S, K ja I kombinaatorid järgnevate makrodega
|
Kombinaator tähendab siin kinnist (ehk vabade muutujateta) termi mis on normaalkujul (ehk mida ei saa iseseisvalt lihtsustada). Nende kombinaatorite tähtsusest räägime natuke hiljem.
On tavaks, et makrodefinitsioonid on kombinaatorid. Sellisel juhul on termi asendatuna alati sama tähendusega ja ei lisa väärtustamisele lihtsustamissamme.
Vaadake, kuidas makrosid on kasutatud termide kirjutamisel.
|
Vaadates viimaseid näiteid näeme, et pikemad λ-termid näevad arusaamatud välja. Selliste termide puhul polegi enamasti mõtet hakata neid intuitsiooni kaudu analüüsima. Lahendus on hoopis püüda neid terme masinlikult lihtsamateks redutseerida. Ehk rakendada reduktsiooni reegleid ja loota, et tulemus on midagi arusaadavat.
Nägime, kuidas δ-reduktsioon lihtsustas termi, milles olid konstantidele rakendatud konstandid ja muud termid. Kuidas aga lihtsustata termi, kus abstraktsioonile (λ x. e1) on rakendatud argument e2. Sellist juhtu nimetataksegi β-reduktsiooniks.
Intuitiivselt on termi (λ x. e1) e2 reduktsioon üsnagi lihtne — selle väärtus on funktsiooni keha väärtus, kui funktsiooni kehas võtta vaba muutuja x asemel termi e2. Näiteks
Siin võib juhtuda aga üks probleem, mida nimetatakse vaba muutuja vangistamiseks. Vaatame termi (λ x y. (λ x y. sub x y) y x) 3 6 kahte erinevat reduktsioonijada. Esiteks redutseerime termi võimalikult väljast.
|
Nüüd aga redutseerime kõigepealt seestpoolt.
|
Tulemus on ühel juhul 3 ja teisel juhul 0. Mis läks valesti? Vastus: vigane on esimene reduktsioon, kus abstraktsiooni kehas λ y. sub x y pidime asendama vabad x-d termiga y. Intuitiivne vastus λ y. sub y y on aga vale, sest kui enne said vähendatav ja lahutaja olla erinevad, siis peale vigast lihtsustust peavad need olema võrdsed — ehk vahe on alati null. Teistpidi vaadates, y, mis oli funktsioonirakenduse reedeksis vaba muutuja, on peale asendamist nüüd seotud sisemise abstraktsiooniga.
Peame ettevaatlikult ja põhjalikult defineerima vangistamisest hoiduva asendamise. Selleks peame esmalt formaalselt defineerima, mis on termi vabad muutujad.
Termi t vabade muutujate hulga arvutab järgnev funktsioon FV ∈ Λ → 2V, mis on defineeritud süntaktiliselt iga termi liigi jaoks.
|
Ehk, kui term on muutuja x∈ V, siis see muutuja ongi vaba. Konstant c∈C ei sisalda vabu muutujaid. Abstraktsiooni λ x. e vabad muutujad on keha e vabad muutujad, kuid peame eemaldama funktsiooni parameetri x, kuna see on seotud just selle lambdaga. Lõpetuseks, aplikatsiooni t u vabad muutujad on lihtsalt t ja u vabade muutujate ühend.
Näited:
|
Vabade muutujate leidmiseks saab kasutada funktsiooni FV, aga paberil/tahvlil arvutades on see liiga tülikas. Enamasti piisab, kui käia üle termi ja iga muutuja juures leida, kus või kas ta on seotud. Vaata järgnevat näidet.
Esimesed kaks muutujat x ja y pole vabad, kuna saime leida abstraktsiooni parameetri, kus nad on seotud. Viimase y juures aga sellist lambdat ei leidu — seega see on muutuja y vaba esinemine.
Nüüd saame defineerida vangistamisest hoiduva substitutsiooni operatsiooni. Kirjutame t[x→ u], mis asendab termis t vabad muutujad x∈ V termidega u selliselt, et u vabad muutujad ei saa vangistatud. Substitutsioon on defineeritud süntaktiliselt iga termi t liigi jaoks.
|
Kui term on muutuja y, siis substitutsioon y[x→ u] tagastab u, kui x on sama muutuja mis y. Kui x≠ y, siis jätame termi muutmata ehk tagastame y. Substitutsioon jätab konstandid samaks ja aplikatsiooni puhul teostatakse substitutsioon nii funktsiooni kui ka argumendi peal. Kõige keerulisem juht on abstraktsioon substitutsioon (λ y. t)[x→ u]. Kui x=y, siis lambda termis vabu x-e ei leidu ja saame tagastada termi muutmata kujul. Kui asendatavas termis u pole y vaba, siis saame otse teha substitutsiooni abstraktsiooni kehas t. Muul juhul peame tegema substitutsiooni, et vältida u-s vaba muutuja y vangistamist. Selleks leiame n.n. värske muutuja z — muutuja, mis ei esine termides u ega t. Seejärel teisendame termi (λ y. t) termiks (λ z. t[y→z]).
Seega on β-reduktsiooni reegel iga t,u∈Λ jaoks järgmine. Aga tuleb meeles pidada, et saame redutseerida ka termis seespool.
| (λ x. t) u →βt[x→u] |
Nüüd redutseerime meie motiveerivat näidet uuesti seestpoolt.
|
Sama tulemus mis kõigepealt väljast redutseerides. Veendusime, et vähemalt sellel juhul ei sõltu tulemus lihtsustussammude järjekorrast.
Hiljem näeme, et teoorias pole konstante ega δ-reduktsiooni vaja — konstandid saab defineerida makrodena nii, et mitmesammuline β-reduktsioon täidab ka δ-reduktsiooni ülesannet. See on nii, kuna arvutusteooria standardid programmi töö efektiivsusele on madalad — efektiivselt arvutatavus ei tähenda kiirust vaid ainult seda et lahenduseni on võimalik konstruktiivselt jõuda.
Programmeerimiskeeltes oleme harjunud kasutama sisukaid muutujanimesid kuigi teame, et nime valik ei mõjuta tegelikult programmi tööd. Heade nimede panemine väldib arusaamatusi programmeerimise protsessi käigus — see aitab ühel programmeerijal kiiremini mõista teise programmeerija programme. Aga meie ei tegele siin praktilise programmeerimisega vaid uurime arvutusmudelit.
Arusaama, et nime valik ei mõjuta tegelikult programmi tööd, nimetatakse α-ekvivalentsuseks (või α-kongruentsuseks). Intuitiivselt, kaks termi, mis võivad erineda ainult seotud muutujate nimede poolest, peaks arvutusprotsessis käituma identselt. Kirjanduses kasutatakse ka sõnastust, et α-ekvivalentsed termid on identsed seotud muutujate ümbernimetamise täpsuseni.
Näited α-ekvivalentsetest termidest.
Formaalselt on termid t, u∈Λ α-ekvivalentsed, ehk t =αu, siis ja ainult siis kui α([], [], t, u) = true. Abifunktsioon α∈ list V → list V → Λ → Λ → B, kus B on tõeväärtuste hulk, on defineeritud järgnevalt.
|
Näiteks soovime veenduda, et (λ x y. x) =α(λ y x. y). Arvutame järgnevalt.
|
Enamasti pole nii detailne arvutuskäik vajalik, et tuvastada, kas termid on α-ekvivalentsed. Paberil/tahvlil arutledes piirdume intuitiivse käsitlusega.
Formaalsels lähenemises on aga tarvis tähele panna, et vaba muutuja asendamine teise muutujaga ei tee termi suuremaks (lemma 1). Seda tähelepanekut kasutame hiljem väidete induktsiooniga tõestamisel, kui substitutsioon teostab vangistamise vältimiseks α-teisenduse.
Tõestus. Tõestus induktsiooniga üle termi t struktuuri. Induktsiooni hüpoteesiks, et t-st struktuurselt väiksemate termide puhul lemma kehtib.
Tõestustes kasutame teoreemi 2, mis ütleb, et α-ekvivalentsus on refleksiivne.
Tõestus. Tõestus induktsiooniga üle lambda keha t. Ekvivalentsuse kontroll läbib termide paari rekursiivselt. Muutuja ja konstandi juhud on triviaalsed. Aplikatsiooni t= f u puhul järeldub väite korrektsus induktsiooni hüpoteesist, et f =α f ja u =α u. Abstraktsiooni t=(λ x. u) puhul peame kontrollima, kas värske muutuja z puhul kehtib, et u[x→ z] =α u[x→ z]. Teoreemi 1 järgi on u[x→ z] suurus sama kui u suurus ehk see on rangelt väiksem kui t suurus. Seega saame rakendada indutksiooni hüpoteesi. Olemegi näidanud, et u[x→ z] =α u[x→ z].
Termi väärtustamiseks piisab δ- ja β-reduktsiooni reeglitest. λ-arvutusel on aga ka kasutusjuht, kus tahame teada termide võrdsust. Sel juhul ei redutseeri me üht termi vaid kahte termi ja vaatame siis, kas mõlema normaalkujud on α-ekvivalentsed. Näiteks on termide võrdsust vaja teada sõltuvate tüüpidega keeltes, kus ka tüübid kodeeritakse sisuliselt λ-termidega. Siin aga tekib probleem.
Vaatame näiteks terme add ja (λ x y. add x y). Mõlemad on βδ-normaalkujul — ühtegi reduktsiooni teha ei saa. Samas, pole need termid α-ekvivalentsed. Kas need polegi võrdsed?
Loogikas on mõiste ekstensionaalsus, mis tähendab seda, et objektid on võrdsed kui need on väliselt eristamatud. Termid add ja (λ x y. add x y) on väliselt eristamatud, kuna argumente lisades on väärtused samad.
Ekstensionaalsuse vaste λ-arvutuses on η-reduktsioon, mis iga t∈Λ puhul, kus x∉FV(t), lihtsustab abstraktsiooni järgnevalt. Jällegi, pidage meeles, et see võib toimuda ka sügavamal termi sees.
|
Ehk, siis kui term on kujul (λ x. t x), kus alamterm t ei sisalda x-i vabalt, saame ümbritseva lambda ja aplikatsiooni ära jätta.
Termide add ja (λ x y. add x y) normaalkuju kasutades βηδ-reduktsioone on mõlemal juhul add . Seega on termid võrdsed — või täpsemalt öeldud βηδ-võrdsed.
|
Teoreetilises λ-arvutuses on kaks põhimõttelist erinevat strateegiat: väljast-enne ja seest-enne. Kuna tehniliselt võib nii välimisi kui sisemisi olla mitu, siis on tavaks võtta alati vasakpoolseim. Nii saame kaks standardset reduktsioonijärjekorda.
Näiteks vaatame termi (λ x y. add y y) (mul 2 3) (sub 5 2). Leiame kõik reeksid.
| ( |
| ) |
Tulemusest on näha meie võimalused. Esmalt redutseerime normaaljärjekorras ehk väljast sisse.
|
Nüüd redutseerime aga sama termi aplikatiivjärjekorras ehk seest välja.
|
Mõlemal juhul läks normaalkuju leidmiseks viis sammu ja tulemuseks on arv kuus. Vaatame erinevusi.
Normaaljärjekorras ei pidanud me arvutama mul 2 3, kuna abstraktsiooni kehas polnud parameetrit x kasutatud. See-eest pidime sub 5 2 kaks korda arvutama, kuna abstraktsiooni kehas on y kasutatud kaks korda.
Aplikatiivjärjekorras arvutasime nii mul 2 3 kui ka sub 5 2 välja olenemata sellest, mida funktsioon teeb. Samas ei pea me midagi topelt arvutama.
Kõigil termidel ei olegi normaalkuju. Vaatame näiteks kirjandusest tuntud makrodefinitsiooni ω = λ x. x x ning termi ω ω. Termil ω ω = (λ x. x x) (λ x. x x) on üks reedeks — kogu term (λ x. x x) (λ x. x x). Nii pole vahet, mis järjekorda reduktsiooniks eelistada — tulemus on ikka sama term.
|
Aga on ka terme, kus normaaljärjekord viib normaalkujuni aga aplikatiivjärjekord ei vii. Üks näide sellisest termist on (λ x. 1) (ω ω), mis normaaljärjekorras saavutab normaalkuju ühe sammuga (λ x. 1) (ω ω) →β 1. Aplikatiivjärjekorras tuleb aga enne funktsiooni asendamist leida argumendi normaalkuju — seda aga ei leidu.
|
Järgnevalt vaatame reduktsiooni tähtsamaid omadusi, alustades Church-Rosseri teoreemist.
Kui termi t jaoks leidub u ja v, nii et t↠βη u ja t↠βη v, siis leidub ka term k nii, et u↠βη k ja v↠βη k.
Church-Rosseri teoreemi põhiline mõte on selles, et reduktsioon ei saa halval juhul minna tupikusse nii, et algselt võimalik olnud lahendus jääb kättesaamatuks. Ebasoodne järjekorra valik võib teha redutseerimisel tööd juurde aga mitte lõpmatult palju tööd.
Kasutades Church-Rosseri teoreemi, saame näidata normaalkujude unikaalsust.
Kui termi t βη-normaalkuju eksisteerib, on see unikaalne.
Oletame, et termil t leidub βη-normaalkuju u ja βη-normaalkuju v. See tähendab, et t↠βη u ja t↠βη v. Church-Rosseri teoreemi järgi teame, et leidub k, nii et , et u↠βη k ja v↠βη k. Teame, et u ja v on βη-normaalkujul, ehk rohkem βη-reduktsioone teha ei saa. Seega u↠βη k saab olla vaid null-sammuline reduktsioon, ehk u=k. Ning ka v=k on ainuke võimalus, et v↠βη k. Seega on mõlemad normaalkujud võrdsed.
Pole selge, kuidas leida termile vastavat normaalkuju kõige paremini või kiiremini. Kõige kiirema järjekorra leidmiseks on vaja keerukat algoritmi – kui selline üldse leidub. Aga tuleb välja, et kui termil normaalkuju leidub, siis normaaljärjekord leiab selle väärtuse lõpliku arvu sammude järel.
Kui termil leidub β-normaalkuju, siis see on saavutatav normaaljärjekorras redutseerides.
Esiteks paneme tähele, et termis ((λ x. u) v), kus u,v∈Λ, võime saada redutseerida alamtermis u→β u′ ja saada tulemuseks β-reedeks ((λ x. u′) v) või redutseerida alamtermis v→β v′ ja saada tulemuseks β-reedeks ((λ x. u) v′). Näeme, et mõlemal juhul on tulemus uuesti β-reedeks. Seega, väärtuse saamiseks ei saa me jätta välist termi redutseerimata. Nüüd olgu termi t0 normaalkuju v, ehk t0↠β v. TODO
λ-arvutuse abstraktsioonile vastavat konstruktsiooni ehk anonüümset funktsiooni saab Idrises luua süntaksiga
\ x, y, z => e, kus x, y ja z on formaalsed parameetrid ja e on avaldis. Lähtekoodis tuleb λ sümboli asemel kirjutada langjoon ’\’, mis tähistab ’λ’ sümbolit. Näiteks saame REPL-is kirjutada järgnevalt.
| Main> (\ x => x+10) 1 11 Main> (\ x, y => 2*x+y) 3 10 16 |
λ-abstraktsiooni saab kasutada ka funktsioonide defineerimiseks. Koodi tähenduse mõttes pole vahet, kas defineerida add10 ühe parameetriga või ilma parameetrita aga λ-abil.
| 1add10: Int -> Int 2add10 = \ x => x+10 3-- add10 x = x+10 |
Avaldise add10 1 väärtust see ei mõjuta – tulemus on 11. Muidugi lambdade kasutamise mõte ongi see, et me ei peaks defineerima uusi nimesid väga lihtsate funktsioonide jaoks.
| Main> add10 1 11 |
Anonüümseid funktsioone kasutatakse, kui mingit lihtsat funktsiooni on vaja anda mõnele teisele funktsioonile argumendiks. Funtksiooni map ja liste vaatame järgnevates peatükkides. Aga intuitiivselt on näha, et lambdaga antud funktsioon on rakendatud igale argumendile.
| Main> map (\ x => x+10) [1,2,4] [11, 12, 14] |
Idrises saab väärtustest luua paare ja muid ennikuid (i.k. n-tuple). Ennikute komponendid pannakse sulgudesse ja eraldatakse komadega.
Näiteks (1,'a'), (1,'a',0) ja ((1.1,8,'x'), False).
Tehniliselt on ennikud implementeeritud paaride abil, kus ('x',1,2.5) on sama mis ('x',(1,2.5)). See tähendab, et sulud võib teatavatel juhtudel ära
Idris järgib Haskelli traditsiooni, et ennikute tüüp kasutab sama süntaksit nagu väärtused. Ehk, enniku tüüp on komponentide tüüpide ennik. Näiteks kolmikute puhul (1,'a',False) : (Int,Char,Bool) ehk (1,('a',False)) : (Int,(Char,Bool)).
Info saab ennikutest kätte mustrisobitusega. Pannes enniku tüübi funktsiooni argumendiks saame definitsioonis kirjutada argumendi nime asemel tüübile vastava mustri. Vaata järgnevat koodi.
| 1f : (Int,Char,String) -> Int 2f (x,c,ys) = x + 1 |
Nägime kuidas saab kasutada kahest suuremaid ennikuid. Võib küsida, mis on ennik kus n on null või üks. Praktilisel kaalutlustel on üksik (e) mingist väärtusest e lihtsalt see väärtus e ise. Ehk, sulgude panemine ei muuda väärtust ega tüüpi. Edasi vaatame juhtu n=0.
Kõige triviaalsem väärtus Idrises tühi ennik (). Selle tüüp on samuti () ehk () : (). Kasutatakse juhtudel, kui pole vaja informatsiooni edastada. Paljudes keeltes kasutatakse selle asemel tüüpi "void".
Tühja ennikut kutsutakse ühikväärtuseks ja selle tüüpi ühiktüübiks. Selline nimetus tuleb faktist, et tüüpidest saab lihtsustatult mõelda kui väärtuste hulkadest. Esiteks, ühiktüüp on nagu üheelemendiline hulk — selles on vaid ühikväärtus. Lisaks saame tüüpe (sarnaselt hulkadele) teoorias defineerida otsekorrutise ja lõikumatu ühendi kaudu. Selliste operatioonide puhul käitub ühiktüüp nagu selle algebralise struktuuri (ringi) ühikelement, kui vaadata hulkade suurust.
Nägime, et ennikute puhul teame elementide arvu ja et iga komponent võib olla ise tüüpi. Mis andmestruktuuri kasutada aga siis, kui meil on varieeruv arv sama tüüpi elemente? Vastus: näiteks liste.
Idrises on naturaalarvude tüüp Nat, kus on defineeritud konstrukor Z : Nat, mis kodeerib arvu null, ja konstruktor S, mis suurendab arvu ühe võrra. Seega on arvud Z, S Z, S (S Z), S (S (S Z)) jne. Selle kohta öeldakse ka, et tegemist on unaarse definitsiooniga (erinevalt näiteks binaarsest arvudest), kus arv on loogilises mõttes tema S-de arv.
Seega, kuigi Idrises võime kirjutada naturaalarve nagu ikka kümnendkujul, siis kompilaator teisendab need ikkagi Z-i ja S-i kasutavaks. Võime väita nii 5 : Nat kui ka S (S (S (S (S Z)))) : Nat. Sisemiselt on arvud mälus esitatu unaarsel kujul, kuigi Idris trükib neid tihti välja kümnendkujul.
| Main> S (S (S (S (S Z)))) 5 |
Selline naturaalarvude definitsioon on tõestamiseks väga mõnus, nagu me näeme mõnes hilisemas peatükis, aga arvutamiseks ebaoptimaalne. Näiteks unaarsete arvude liitmisel on lineaarne tööaeg ja mälu-kasutus. Binaarsetel arvudel on mõlemad logaritmilised. Seega efektiivsust nõudvates kohtades kasutada tüüpe Int ja Integer aga tõestamise juures on vahel mõistlik kasutada tüüpi Nat.
Järjend ehk list on andmetüüp, milles saame hoida suvalise arvu mingit konkreetset tüüpi elemente. Näiteks täisarude listid on [1,2,3], [3] ja []. Tõeväärtuste listid on [True, False, False], [False] ja [].
Pane tähele, et tühi list [] on täisarvude, tõeväärtuste ja kõigi teiste elemenditüüpide puhul sama.
Üldiselt on järjendi tüübiks List a, kus a on elementide tüüp.
Näiteks, täisarvude list on tüübiga List Int ja sümbolite list on tüübiga List Char. Listi elemendid võivad ise olla listid — ujukoma-arvude listide list on näiteks tüübiga List (List Float).
Idrise listid on arvuti mälus esitatud puudena.
Pane tähele, et listi elemendid on alati vahetipu vasakud lapsed. Vahetippude paremad lapsed on alati listid. Veel pane tähele, et puuduvad viidad listi algusest-lõppu ja lõpust algusse.
Sellisel listi esitusel on nii head kui ka halvad omadused. Halvaks omaduseks on näiteks see, et listi viimase elemendi leidmiseks tuleb kogu list läbida. Heaks omaduseks aga see, et listi [0,1,2,3] tegemiseks piisab luua mälupesa puu juure jaoks ning sinna salvestada viidad arvule 0 ja olemasoleva listi [1,2,3] puu juurele.
Seni oleme vaadanud konstantseid liste — neid saab esitada nurksulgude vahel ja komadega eraldatult. Järgnevalt vaatame, kuidas luua ja kasutada liste üldiselt.
Järjendi loomiseks Idrise koodis on kaks konstruktorit, mis vastavad (list-tüüpi) puu tippudele. Tühja listi konstruktor [] : List a ja mittetühja listi konstruktor (::) : a -> List a -> List a. Mittetühja listi konstruktori esimest argumenti kutsutakse listi peaks (i.k. head) ja teist argumenti sabaks (i.k. tail).
Näiteks konstantne list [1,2,3] on Idrises konstrukorite abil kirjutatav kui list 1 :: (2 :: (3 :: [])). Selle listi pea on arv 1 ja saba 2 :: (3 :: []) ehk [2,3].
Kui meil on näiteks täisarvude listide list xs : List (List Int), siis tühja listi lisamiseks selle algusse kirjutame [] :: xs.
Funktsionaalsetes keeltes on konventsioon, et listi tüüpi muutujate nimed lõpevad s-ga. Näiteks xs, zs. See tuleneb mitmuse tunnusest inglise keeles. Listide-listide puhul kasutatakse mõnikord kahte s-i. Näiteks yss.
Listi andmete töötlemiseks kasutatakse rekursiivseid funktsioone ja mustrisobitust. Näiteks listi pikkust saab leida järgneva (standardteegis leiduva) funktsiooni length abil.
| 1length : List a -> Nat 2length [] = 0 3length (x::xs) = 1 + length xs |
Funktsioon length võtab argumendiks suvalise elemenditüübiga listi ja tagastab naturaalarvu. Kuna listidel on kaks konstruktorit, peame mustrisobitusel arvestama mõlema juhuga. Kui argumendiks on tühi list, siis selle tühja listi pikkus on null. Kui argument on mittetühi list, kus x on listi peas olev element ja xs on saba, siis kogu listi pikkuse saame kui liidame saba pikkusele ühe.
Listide loomiseks saame kirjutada ise rekursiivseid funktsioone aga saame kasutada ka standardteegi funktsioone. Üht komplekti kasulikke standardteegi funktsioone nimetatakse enumeratsioonideks.
Enumeratsioonidel on eriline süntaks. Kui m ja n on täisarvud (muutujad või konstandid), siis saame kirjutada [m..n] tähistamaks listi mis algab m-ga ja lõppeb n-ga. Näiteks [3..6] = [3,4,5,6] ja [6..3] = [6,5,4,3].
Lisaks saame kirjutada [m,n..k], et genereerida elemendid m-st k-ni sammuga n-m. Näiteks [6,4..1] arvutab listi [6,4,2]. Paneme tähele, et k ei ole ilmtingimata arvutatavasse listi. Genereerimise lõpetamise tingimus, et arvud ei lähe üle piiri k.
Enumeratsioonid töötavad ka näiteks Char sümbolitel, kuna need on loomulikul teel teisendatavad naturaalarvudeks. Kehtib ['a'..'e'] = ['a','b','c','d','e'] ning ['a','c'..'m'] = ['a','c','e','g','i','k','m'].
Lisaks võime kirjutada [m..], tähistamaks lõpmatut striimi mis algab m-ga, ning [m,n..], tähistamaks lõpmatut striimi mis algab m-ga ning sammuga n-m.
Peamine erinevus listide ja striimide vahel on see, et striimidel pole tühja striimi konstruktorit — kõik striimid on lõpmatud. Striime vaatame peatükis 12.
Matemaatikas kasutatakse hulgakomprehensiooni, näiteks paaris arvude hulka saame defineerida kui {n | ∃ k∈ℤ, n=2k}. Ehk siis paarisarvud on kõik n-d, kus leidub täisarv k nii et kehtib n=2k. Selline kirjaviis sisaldab piisavalt infot, et kontrollida sisaldumist hulgas. Lisaks saame selle abil genereerida paarisarve — võtame suvalise täisarvu k ja korrutame selle kahega.
Matemaatikas kasutatakse hulgakomprehensiooni tihti lõpmatute hulkade puhul. Programmidese me aga tegelikult ei soovi lõpmatuid hulki või liste välja arvutada. Vastupidi, Idrises kasutame listikomprehensiooni võrdlemisi lühikeste listide genereerimiseks.
Üldjuhul on süntaks
[ e | q1, q2, …, qn ] kus e on avaldis ja qi võib olla generaator, let avaldis või valvur. Järgnevalt vaatame neid kolme juhtu.
Generaator on kujul x ← l, kus x on muutuja ja l list. Muutuja x väärtuseks proovitakse järjest läbi kõik listi l väärtused.
Let avaldis on kujul let x = e, kus x on muutuja ja e avaldis. Muutuja x väärtuseks võtetakse e väärtus. Sisuliselt saavutaksime sama efekti kasutades x ← [e].
Valvur on Bool tüüpi avaldis mis töötab filtrina. Kui avaldis väärtustub tõeseks, jätkatakse listi genereerimist olemasolevate muutujatega. Kui avaldis väärtustub vääraks, läheb arvutusprotsess tagasi ja proovitakse järgmisi väärtusi.
Avaldise e väärtus genereerib listi elemendid. Avaldis võib kasutada paremal defineeritud muutujaid ja qi-d võivad kasutada vasakul defineeritud muutujaid.
Näited
[ x*x | x <- [1..10]] = [1,4,9,16,25,36,49,64,81,100]
[ x*x | x <- [1..10], mod x 3 == 0] = [9,36,81]
[ m | x <- [1..10], let m = x*x,m < 50] = [1,4,9,16,25,36,49]
[(a,b)|a<-[1..2],b<-[1..3]] = [(1,1),(1,2),(1,3),(2,1),(2,2),(2,3)]
Esimene näide genereerib arvude üks kuni kümme kõik ruudud. Teine näide genereerib vaid sellised ruudud, mis jaguvad kolmega. Kolmas näide genereerib arvude üks kuni kümme ruudud, kus tulemus on väiksem kui 50. Viimane näide genereerib arvude paarid, kus vasakpoolne komponent on üks või kaks ja parempoolne komponent ühest kolmeni. Viimane näide näitab ka ära, et parempoolsed generaatorid vahetuvad kiiremini kui vasakpoolsed — enne tuleb (1,2) ja alles hiljem (2,1).
Kõrgemat järku funktsioonid on funktsioonid, mis võtavad funktsioone argumentideks (näiteks tüübiga (A -> B) -> C) ja/või tagastavad funktsioone (näiteks tüübiga A -> (B -> C)). FP läbiv idee ongi, et funktsioonid on tavalised väärtused.
Seega on funktsionaalprogrammeerimises kõrgemat järku funktsioonide kasutamine tavaline nähtus. Näiteks, kõik kahe ja enam parameetriga funktsioonid Idrises rangelt võttes kõrgemat järku funktsioonid.
Kõrgemat järku funktsioonide kasutamisega kaasneb asjaolu, et funktsiooni parameetrite arv võib erineda funktsiooniväljakutse argumentide arvust. Programmi valiidsuse peab tagama tüübikontroll.
Kui argumente antakse liiga vähe, on tulemuseks funktsioon, mis ootab ülejäänud argumente. Näiteks (+) on kahe argumendiga funktsioon seega (+) 5 on ühe argumendiga funktsioon, mis võtab teise liidetava.
Kui argumente antakse rohkem kui parameetreid, lähevad ülejäänud argumendid funktsiooni poolt tagastatava funktsiooni argumendiks.
Näiteks võtame standardteegi funktsiooni const : a -> b -> a — kahe parameetriga funktsioon, mis on defineeritud kui const x y = x. Seega const ((+) 2) ((*) 2) 5 kutsub funktsiooni const välja kolme argumendiga kuigi parameetreid on kaks. Viimane argument 5 antakse edasi funktsioonile (+) 2 ja tulemus on 7.
Vaatame harjutamiseks mõningaid listidega seotud kõrgemat järku funktsioone. Idrise standardteegis on need funktsioonid natuke üldisemate tüüpidega — neid uurime täpsemalt liideste peatükis ???.
Funktsioon map võtab esimeseks parameetriks funktsiooni ja teiseks parameetriks listi ning rakendab funktsiooni kõigile listi elementidele ja tagagastab saadud tulemused listina.
Üks viis map-i defineerida on järgmine.
| 1map : (a -> b) -> List a -> List b 2map f [] = [] 3map f (x::xs) = f x :: map f xs |
Teine sobilik definitsioon oleks map f xs = [ f x | x <- xs ]. Aga meelde tuleks jätta hoopis järgmine võrdus pseudokoodis:
| map f [x1, x2, …, xn] = [f x1, f x2, …, f xn] |
Teine võimalik interpretatsioon map funktsioonile on, et map teisendab funktsiooni f : a -> b listide funktsiooniks map f : List a -> List b. Sellest interpretatsioonist saab map-i jaoks hiljem tuletada ka üldisema tüübi, mis tõstab teisendava funktsiooni iga sobiva konteineri teisenduse funktsiooniks.
Näiteks tahame ujukomaarvude listi konverteerida pöördarvude listiks. See vastab täpselt map-i mustrile. Seega saame defineerida järgmise funktsiooni.
| 1inverses : List Double -> List Double 2inverses = map (\ x => 1 / x) |
Kutsudes välja inverses [1,2,4,8], saame tulemuseks [1.0,0.5,0.25,0.125]. Samas paneme tähele, et definitsioonil pole ühtegi formaalset parameetrit ja map-le on antud kahest parameetrist vaid esimene.
Teine väga kasulik kõrgemat järku listifunktsioon on foldr, mis võtab parameetriteks listi töötlemise funktsiooni f, väärtuse b ja listi.
Funktsioon tagastab tühja listi puhul b ja kasutab mittetühja listi puhul funktsiooni f listi pea ja saba rekursiivsel väljakutsel.
Idrises saab funktsiooni defineerida järgnevalt.
| 1foldr : (a -> b -> b) -> b -> List a -> b 2foldr f b [] = b 3foldr f b (x::xs) = f x (foldr f b xs) |
Meelde võiks jätta järgmise võrduse, mis näitab, kuidas foldr listi elemente funktsiooniga (⊕) järjest vasakult-paremale töötleb. Täht r funktsiooni foldr lõpus tähistabki seda, et operatsiooni kasutatakse parem-assotsiatiivselt.
foldr (⊕) b [x1, x2, …, xn] = x1 ⊕ (x2 ⊕ (… ⊕ (xn ⊕ b))) |
Funktsiooni map saab defineerida läbi foldr-i järgnevalt.
| 1map : (a -> b) -> List a -> List b 2map f xs = foldr g [] xs 3 where g : a -> List b -> List b 4 g x ys = f x :: ys |
Nii saame tuletada foldr-i võrdusest map-i võrduse.
|
Funktsioon foldr on eriline rekursiooni operaator, mille tüübi ja implementatsiooni saab automaatselt (listi) andmetüübi deklaratsiooni järgi genereerida. Sisuliselt foldr asendab listi tühja listi konstruktori teise argumendiga ja mittetühja list konstruktori esimese argumendiga.
Ehk foldr f b (x1 :: x2 :: … :: xn :: []) redutseerub samaks väärtuseks kui x1 `f` x2 `f` … `f` xn `f` b.
Teoreetiliselt saab listi rekursiooni operaatoriga defineerida kõik rekursiivsed listifunktsioonid ilma eksplitsiitselt rekursiooni kasutamata. Mõninal juhul on foldr-ga defineeritud funktsioon väga selge. Näiteks listi pikkuse arvutamine.
| 1length : List a -> Nat 2length = foldr (+) 0 |
Funktsioonil foldr on teoreetiliselt väga head omadused, mis on seotud lõpmatute struktuuridega ja laisa väärtustamisega — uurime seda edasi peatükis ???. Kuna Idris on agar keel ja me töötleme kogu listi läbi, siis oleks parem kui fold-funktsioon oleks sabarekursiivne. Seega tuleks kaaluda hoopis funktsiooni foldl kasutamist.
Väga kasulik kõrgemat järku listifunktsioon on foldl, mis võtab parameetriteks listi töötlemise funktsiooni f, väärtuse b ja listi.
Funktsioon tagastab baasjuhul b. Mittetühja listi puhul kasutatakse rekursiooni, kus teiseks argumendiks võetakse funktsioon f rakendatud listi peale ja väärtusele b.
Idrises saab seda funktsiooni defineerida järgnevalt.
| 1foldl : (b -> a -> b) -> b -> List a -> b 2foldl f b [] = b 3foldl f b (x::xs) = foldl f (f x b) xs |
Meelde võiks jätta järgmise võrduse, mis näitab, kuidas foldl listi elemente funktsiooniga (⊕) järjest paremalt-vasakule töötleb. Täht l funktsiooni foldl lõpus tähistabki seda, et operatsiooni kasutatakse vasak-assotsiatiivselt.
foldl (⊕) b [x1, x2, …, xn] = ((((b ⊕ x1) ⊕ x2) ⊕ …) ⊕ xn) |
Suur erinevus foldr-i ja foldl-i vahel on see, et kuigi list läbitakse päripidises järjekorras siis lõpptulemus tuleb justkui tagurpidises järjekorras. Seetõttu saab foldl-iga väga lihtsalt implementeerida listi ümberpööramist. Vaata järgmist definitsiooni.
| 1reverse : List a -> List a 2reverse xs = foldl g [] xs 3 where g : List a -> a -> List a 4 g x y = y :: x |
Saame näidata foldl-i võrduse abil, kuidas reverse tõepoolest listi ümber pöörab.
|
Pöidlareegel on, et laiskades keeltes (nagu Haskell) peaks eelistama foldr funktsiooni, kuna see töötab ka lõpmatutel listidel. Agarates keeltes (nagu näiteks Scala või Idris) peaks võimalusel eelistama foldl-i.
Veel üks väga kasulik kõrgemat järku listifunktsioon on filter, mis võtab parameetriteks predikaadi f : a -> Bool ja listi xs : List a.
Funktsioon tagastab samas järjekorras listi xs elemendid, kus p tagastab true.
Idrises saab seda funktsiooni defineerida järgnevalt.
| 1filter : (a -> Bool) -> List a -> List a 2filter _ [] = [] 3filter p (x::xs) = if p x then x :: filter p xs else filter p xs |
Näiteks saame kasutada filter-it et jätta listis [1,20,3,40,5,60] alles kõik kümnest väiksemad arvud või kõik kümnest suuremad arvud. Funktsiooniks kasutame näiteks sektsioone < 10 ja > 10, kus binaarse operaatori puudu olevast vasakust poolest saab funktsiooni argument.
| Main> filter (< 10) [1,20,3,40,5,60] [1, 3, 5] Main> filter (> 10) [1,20,3,40,5,60] [20, 40, 60] |
Alternatiivne võimalus filter funktsiooni defineerimiseks oleks listikomprehensiooniga: filter p xs = [ x | x <- xs, p x ].
Uusi tüüpe saab Idrises luua kahel viisil: võtmesõnaga data ja definitsiooniga, mille tulemus on tüüpi Type. Esmalt vaatame definitsioone.
Idris on n.n. sõltuvate tüüpidega programmeerimiskeel — me vaatame hiljem täpsemalt, mida see tähendab. Sõltuvate tüüpidega programmeerimiskeelte puhul on tavaline, et tüübid spetsifitseeritakse samasuguste avaldistega kui definitsioonid. Ehk siis tüübid võivad sisaldada lambdasid, funktsioonikutseid, tingimuslauseid jne.
Näiteks saame defineerida tüübisünonüümid, kus avaldised Pikkus ja Laius väärtustuvad täisarvutüübiks Int. Selline kood on hea koodi dokumenteerimiseks või kui me hiljem soovime definitsioone muuta.
| 1Pikkus : Type 2Pikkus = Int 3 4Laius : Type 5Laius = Int |
Sellised tüübisünonüümid ei sobi aga kasutusjuhtudeks, kus tahame eristada väärtust tüübiga Pikkus väärtusest tüübiga Laius. Näiteks, kui meil on h: Pikkus ja w: Laius ning funktsioon rk_pindala: Pikkus -> Laius -> Pindala siis saame seda välja kutsuda kui rk_pindala w h.
Saame teha ka funktsiooni, mis tagastab tüübi. Funktsioon Punkt : Nat -> Type võtab parameetriks naturaalarvu ja seab sellele vastavusse ujukomaarvude enniku, milles on parameetri jagu komponente. Vaata järgnevat koodi.
| 1Punkt : Nat -> Type 2Punkt 0 = () 3Punkt 1 = Double 4Punkt (S n) = (Double, Punkt n) 5 6vec3d : Punkt 3 7vec3d = (1.0,0.0,1.0) |
Sarnaselt saame teha ka funktsioone, mis võtavad parameetriteks ning tagastavad tüüpe. Näiteks funktsiooni Ennik : List Type -> Type, mis võtab parameetriks tüüpide listi ja seab sellele vastavusse enniku, mille komponendid on vastava parameetri listi elemendid. Vaata järgnevat koodi. Pane tähele, et nii Punkt 3 kui ka Ennik [Double,Double,Double] väärtustuvad tüübiks (Double,Double,Double).
| 1Ennik : List Type -> Type 2Ennik [] = () 3Ennik [t] = t 4Ennik (t::ts) = (t,Ennik ts) 5 6test1 : Ennik [String, Double, Char] 7test1 = ("tere", 1.5, 'x') 8 9test2 : Ennik [Double, Double, Double] 10test2 = vec3d |
Teine võimalus uute tüüpide loomiseks on data võtmesõnaga, kus loetletakse üles lõikumatud ja injektiivsed väärtuste kõik (vajadusel parametriseeritud) variandid. Vaatame erinevaid võimalusi näidete põhjal. Esmalt vaatame, kuidas on Idrises defineeritud tõeväärtuste tüüp Bool.
| 1data Bool = True | False |
Sellest koodireast loeme välja järgnevat: defineeritakse uus andmetüüp Bool: Type, defineeritakse konstruktor True: Bool,defineeritakse konstruktor False: Bool.
Lähtudes lõikumatusest, teame et tõesus True ja väärus False on erinevad.
Ning kuna loetleti üles kõik variandid, siis tähendab, et kõik tõeväärtused on kas True või False.
Seetõttu on põhjendatud, miks saame kasutada mustrisobitust.
| 1not : Bool -> Bool 2not True = False 3not False = True |
Tõeväärtustest Bool veel lihtsama struktuuriga andmetüüp on ühiktüüp, mis on standardteegis defineeritud järgnevalt. Pane tähele, et Idrise kompilaator asendab () vastavalt vajadusele kas Unit-ga või MkUnit-ga. Väärtusele tüübiga () on võimalik teha mustrisobitust, aga see ei anna praktikas infot juurde.
| 1data Unit = MkUnit 2test_unit : () -- sama mis Unit 3test_unit = MkUnit -- sama mis () 4f1, f2 : Unit -> Unit 5f1 () = () 6f2 _ = () |
Jätkates ühe konstruktoriga andmetüüpidega, vaatame paari tüübipere definitsiooni standardteegis. Tüübipere tähendab siinkohal seda, et Pair iseseisvalt ei ole tüüp vaid vajab tüübiks saamiseks kaht argumenti. Tüübil on üks konstruktor MkPair : a -> b -> Pair a b. Siin Idrise kompilaator asendab (,) vastavalt vajadusele kas Pair-ga või MkPair-ga. Seega MkPair-i tüübiks võib kirjutada ka a -> b -> (a, b).
| 1data Pair a b = MkPair a b 2test_pair : (Int, Char) -- sama mis Pair Int Char 3test_pair = MkPair 4 'x' -- sama mis (4, 'x') 4add_pair : (Int, Int) -> Int 5add_pair (x, y) = x + y |
Teeme kõrvalpõike algebrasse. Paaride tüüp on mingis mõttes tüüpide (otse)korrutis, kuna paaride väärtuste arv on komponent-tüüpide väärtuste arvude korrutis ehk |Pair A B| = |A| * |B|, kus |·| on funktsioon, mis seab tüübile vastavusse tema väärtuste arvu. Lisaks, ühiktüüp on selle korrutise ühikelement. Algebrast tuntud struktuuri ringi saamiseks oleks vaja teada ka, mis on tüüpide summa. Selleks on tüübipere Either : Type -> Type -> Type, mis vastab väärtuste hulkade lõikumatu ühendi operatsioonile. Kehtib |Either A B| = |A| + |B|
Konstruktor Left : a -> Either a b võtab argumendiks Either-i esimese parameetri tüübiga väärtuse ja Right : b -> Either a b võtab argumendiks Either-i teise parameetri tüübiga väärtuse.
| 1data Either a b = Left a | Right b |
Naturaalarvud on standardteegis defineeritud kahe konstruktori Z ja S kaudu. Kusjuures konstruktoril S on argument tüübiga Nat. Seega naturaalarvud on defineeritud induktiivselt: Z on naturaalarv ja iga naturaalarvu n : Nat kohta teame, et S n on naturaalarv.
| 1data Nat = Z | S Nat |
Kuigi konstruktoril S on funktsioonitüüp Nat -> Nat siis tegemist pole suvalise funktsiooniga vaid injektiivse konstruktoriga. Injektiivne tähendab siin kontekstis seda, et rakenduse informatsioon ei lähe kaduma. See tähendab muuhulgas, et S (S Z) erineb väärtusest S Z.
Tüüpide algebraga (Pair, Unit ja Either) ning funktsioonitüübiga saame luua väga palju kasulikke andmetüüpe ilma ise data võtmesõna kasutamata. Näiteks tõeväärtuste asemel võtta Either () (). Probleem tekib aga rekursiivsete andmetüüpidega. Näiteks naturaalarve võiks saada defineerida kui MyNat = Either () MyNat. See aga kahjuks praktikas ei tööta, kuna Idris on agar keel ja soovib MyNat lõplikult väärtustada.
Listide definitsioon on väga sarnane naturaalarvudele — lisatud on parameeter tüübile ja teisele konstruktorile. Listid List a on standardteegis defineeritud kahe konstruktori Nil ja (::) kaudu. Kusjuures konstruktoril (::) on argumendid tüübiga a ja List a.
| 1data List a = Nil | (::) a (List a) |
Idrise kompilaator asendab [] konstruktoriga Nil ja konstantide listi
[x1, … , xn]
konstruktsiooniga x1 :: … :: xn :: Nil .
Nüüd vaatme väga kasulikku tüübiperet Maybe : Type -> Type. Esimene võimalus Maybe a tüüpi väärtuse loomiseks on konstruktoriga Nothing. Teine võimalus on konstruktoriga Just, millele tuleb argumendiks anda a tüüpi väärtus.
| 1data Maybe a = Nothing | Just a |
Tüüp Maybe lisab väärtsute hulgale ühe väärtuse, mida kasutatakse tihtipeale nurjumise tähistamiseks. Näiteks paaride listist otsimise funktsioon lookup kasutab tulemuses väärtust Nothing tähistamaks, et listis otsitavat paari ei leidu.
| 1lookup : Int -> List (Int,b) -> Maybe b 2lookup x [] = Nothing 3lookup x ((y,z)::ys) = if x==y then Just z else lookup x ys |
Funktsiooni lookup saame kasutada järgnevalt:
lookup 4 [(3,'x'),(4,'y')] == Just 'y'
lookup 2 [(3,'x'),(4,'y')] == Nothing
Eelnevalt nägime, kuidas arvutada konstantidega λ-arvutuses, kus konstantideks võtsime tõeväärtused, täisarvud, paarid ja listid. Nüüd vaatame, kuidas defineerida tõeväärtused, naturaalarvud, paarid ja listid kasutades puhast λ-arvutust. See tähendab, et teoreetilises lähenemises võime konstante ja δ-reduktsioone ignoreerida.
Definitsioonideks valime kombinaatorid: ilma vabade muutujateta termid, mis on normaalkujul. Nii käituvad meie definitsioonid sarnaselt konstantidele — ei tekita juurde vabu muutujaid ega redutseeru selliselt, et me neid ära ei tunne. Tegelikult on võimalik kõik abstraktsioonid kirjeldada S, K ja I kombinaatoritega.
|
Tõeväärtuste spetsifikatsiooniks võtame tõeväärtuste funktsioonide δ-reduktsioonid, leiame konstantidele vastavad λ-termid ja näitame, et δ-reduktsiooni asemel saame teha β-reduktsioone ja saada sama tulemuse.
Tõeväärtuste operatsioonid on spetsifitseeritud järgnevalt.
|
Sobivate definitsioonide leidmiseks kasutame järgnevat strateegiat: väärtuseks võtame vastava väärtuse mustrisobituse operatsiooni. Tõeväärtuse true mustrisobitus ehk tingimuslause võtab kaks parameetrit, e1 ja e2, ning tagastab e1. Seega võtame true := λ x y. x. Sarnase argumentatsiooniga võtame false := λ x y. y. Muud operatsioonid saame programmeerida kasutades teadmist, et tõeväärtused on nendele vastavad tingimuslaused.
|
Saame näidata, et δ-reduktsioonile vastab mitmesammuline β-reduktsioon.
|
|
|
|
Paaride operatsioonid on spetsifitseeritud järgnevalt.
|
Definitsioonide leidmise strateegia on sama mis tõeväärtuste puhul — leiame mustrisobitusele vastava termi. Idrises saab paaride mustrisobitust teostada avaldisega match MkPair e_1 e_2 with MkPair x y => p. Seega λ-arvutuses võime võtta näiteks pair = λ e1 e2 p. p e1 e2. Ehk siis paari komponendid antakse ainukesele harule edasi eraldi parameetritena. Siis fst ja snd saame impmeneteerida kasutades mustrisobitus järgnevalt.
|
Nüüd saame näidata definitsioonide vastavust spetsifikatsioonile.
|
|
Natutaalarvude kohta nõuame, et succ , pred , iszero , add ja mul arvutaks vastavalt järgmise arvu, eelmise arvu, arvu võrdumise nulliga, liitmise ja korrutamise.
Esmalt püüame ehitada nii, et nulli esitab identsusfunktsioon λ x. x ja nullist suuremad arve paarid, mille esimene komponent on false ja teine on ühe võrra väiksem number. Nii on arvude struktuur sarnane Idrise struktuurile aga lisatud on false komponendid. Sellist konstruktsiooni nimetatakse standardnumbriteks.
|
Saame näidata, et succ , pred ja iszero töötavad korrektselt. Näeme, et pred töötab vaid nullist suuremate arvude korral.
|
|
|
|
|
Kui makrode defineerimisel oleks rekursioon lubatud, saaks standardnumbrite liitmise defineerida kui add := λ x y. cond (iszero x) y (add (pred x)(succ y)). Hiljem, peatükis ???, näeme ühte võimalust, kuidas rekursiooniga hakkama saada. Enne aga vaatame ühte alternatiivset lähenemist — Churchi numbreid.
Numbrite defineerimiseks kasutame funktsiooni termide astendamise notatsiooni. Termide E, E∈ Λ jaoks En E′ rakendab funktsiooni E n-korda, alustades argumendist E′. Ehk E0 E′ = E′, E1 E′ = E E′, E2 E′ = E (E E′) , E3 E′ = E (E (E E′)) jne. Nüüd saame defineerida Churchi numbrid.
|
Churchi numbrite intuitsioon on, et arv n tähistab mingi valitud operatsiooni n-kordset tegemist — arv vastab sellele, mitu iteratsiooni tuleb teha. Arvule ühe lisamine tähendab ühe iteratsiooni lisamist. Nulliga võrdumist saab kontrollida nii, et algseisuks võetakse true ja tsüklis muudetakse see false -ks; nulli iteratsiooni puhul jääb seisundiks true ja rohkemate iteratsioonide puhul on tulemus false . Vaata formaalseid β-reduktsioone.
|
|
|
Liitmise, korrutamise ja isegi astendamise saame defineerida järgnevalt. Pane tähele, et astendamise definitsiooni saaks kirjutada veel lühemalt: exp = λ m n. n m.
|
Vaatame, kuidas term add m n β-redutseerub naturaalarvude m ja n summaks. Intuitiivselt, kõigepealt tehakse n iteratsiooni ja seejärel veel m iteratsiooni. Korrutamise korrektsuse verifitseerimiseks peame veenduma, et (λ x. fn x )m x on tõesti sama kui fmn x. Ehk, intuitiivselt m korda tehakse n iteratsiooni.
|
|
Churchi numbrite puhul on keeruliseks ülesandeks hoopis ühe lahutamine. Intuitiivselt, kui meil on arv n ja me saame teha n iteratsiooni aga soovime teha n−1 iteratsiooni. Selle probleemile on kaks standardset lahendust. Esiteks vaatame lahendust, kus meil intuitiivselt on iteratsioonis lisamuutuja — tõeväärtus, mis ütleb, kas me oleme juba ühe maha lahutanud. Vajame abifunktsiooni, mis käituks järgnevalt.
|
Sellist spetsifikatsiooni rahuldab järgmine definitsioon.
|
|
|
Reduktsiooni (prefn f)n (false,x) ↠ (false,fn x) tõestame induktsiooniga üle naturaalarvu n. Vaatame baasjuhtu n=0 ja induktsiooni sammu n=n′+1.
|
|
Siis saame defineerida eelmise arvu leidmise operaatori pred .
|
|
|
Seega oleme andnud ühe naturaalarvude implementatsiooni kasutades paari ja tõeväärtust. Teine variant on implementeerida viivitus naturaalarvude paariga, mille mõlemad komponendid on alguses nullid. Iga iteratsioon kopeerib paari teise komponendi esimeseks ja suurendab teiset komponenti ühe võrra — nii on paari esimene komponent alati peale esimest iteratsiooni ühe võrra väiksem. Peale iteratsioone tagastatakse paari esimene komponent.
|
Esmalt tõestamie induktsiooniga, et f-i n-kordsel rakendamisel paarile pair m m+1 on tulemuseks (pair m+n m+n+1). Induktsiooni baas kehtib triviaalselt kuna f0 (pair m m+1) = pair m m+1. Induktsiooni sammu kehtivust tõestab järgnev reduktsioon.
|
Nüüd saame hõlpsasti näidata, et pred 0 redutseerub väärtuseks 0 ja pred n+1 redutseerub väärtuseks n.
|
|
Listide kohta on jägnevad δ-reduktsioonireegild.
|
Sarnaselt naturaalarvudele, on siin võimalik kaks lähenemist. Esiteks võime lähtuda listi mingist fold-funktsioonist ja implementeerida null, hd ja tl kasutades seda fold-i. Teine võimalus oleks kasutada paare ja tõeväärtueseid — teades ette, et fold-i puudumisel on paljude funktsioonide implementeerimiseks vaja rekursioon.
Vaatame esmalt põgusalt listide implementatsiooni, mis on tuletatud listide foldr funktsioonist.
|
Nüüd saame implementeerida konstandid null ja hd.
|
|
|
|
Listi saba leidmine kasutades fold funktsioone on võimalik aga parajalt tülikas. Definitsioonid tulevad pikad ja korrektsuse näitamine võtab palju samme. Seetõttu piirdume siin Idrise koodiga, mis arvutavad listi saba kasutade foldr või foldl.
| 1tl1 : List a -> List a 2tl1 l = snd (foldl f (True,[]) l) where 3 f : (Bool, List a) -> a -> (Bool, List a) 4 f (True ,r) x = (False, r) 5 f (False,r) x = (False, r++[x]) 6 7tl2 : List a -> List a 8tl2 l = snd (foldr f (pred (length l), []) l) where 9 f : a -> (Nat, List a) -> (Nat, List a) 10 f x (0, r) = (0, r) 11 f x (S n, r) = (n, x::r) |
Teine võimalus listifunktsioone defineerida on läbi paaride ja tõeväärtuste.
|
Nüüd saame näidata, et meie definitsioonid vastavad spetsifikatsioonile kasutades β-reduktsiooni.
|
|
|
|
Sellised definitsioonid ei võimalda meil aga defineerida rekursiivset foldr funktsiooni. Järgmisena vaatamegi, kuidas toetada rekursiivset käitumist.
Termi M nimetatakse püsipunktikombinaatoriks kui kehtib
| ∀ F. M F =βF (M F). |
Tuntuim püsipunktikombinaator on Haskell Curry “paradoksaalne” kombinaator
| Y := λf. (λx. f (x x)) (λx. f (x x)). |
Saame näidata, et Y on püsipunktikombinaator.
|
Pane tähele, et tõestuse viimase sammuna tuleb β-ekspansioon, mitte β-reduktsioon. Seetõttu on mõnevõrra raskendatud Y e-ks ekspandeerutava termi äratundmine suurema termi sees — kui meil oleks mingi konkreetne term e. Seetõttu võib olla kasulik kasutada hoopis “tugevat” püsipunkti kombinaatorit Θ.
| Θ := (λ x y. y (x x y)) (λ x y. y (x x y)) |
Kombinaatori Θ kohta saame tõestada tugevama väite, et Θ e →β e (Θ e).
|
Püsipunktikombinaatoreid saab kasutada rekursiivsete funktsioonide defineerimiseks. Võtame näiteks standardnumbrite (naturaalarvude) liitmise. Rekursiivse väljakutse jaoks lisame definitsiooni esimese parameetri ja rakendame funktsiooni püsipunktikombinaatorile.
| add := Y (λf x y. cond (iszero x) y (f (pred x)(succ y))) |
Tõestame näiteks ka liitmise korrektsust, s.t, et add m n redutseerub avaldiseks m+n. Tõestuseks kasutame induktsiooni ja alustame baasjuhust m=0, kus kasutame add-i definitsiooni järel püsipunktikombinaatori võrdust Y f =β f (Y f), teadmist iszero 0 ↠β true ja cond true e1 e2 ↠β e1.
|
Jätkame induktsiooni sammu m=m′+1 tõestusega, kus kasutame add-i definitsiooni järel püsipunktikombinaatori võrdust Y f =β f (Y f), teadmist iszero m+1 ↠β false , teadmist pred m+1 ↠β m, teadmist succ n ↠β n+1, teadmist cond false e1 e2 ↠β e2 ning induktsiooni hüpoteesi ∀ k, add m k ↠β m+k.
|
Sarnaselt liitmisoperatsioonile add saame kõik rekursiivsed definitsioonid kirjutada mitterekursiivselt, kasutades mõnda püsipunktioperaatorit. Üldine muster on, et funktsioonile tuleb lisada esimene parameeter ja sellega asendada kõik rekursiivsed väljakutsed. Nii saame funktsiooni, mis töötab soovitud viisil kuni rekursiivse väljakutseni. Kuidas aga anda funktsioonile see esimene argument? Seda teeb püsipunktioperaator. Ehk kui soovime defineerida funktsiooni, mis käitub nagu võrdus f = λx y z. … (f a b c) … siis piisab meil see defineerida mitterekursiivse makrona f := Y (λf’ x y z. … (f’ a b c) …).
Olukorda, kus sama sümbol tähistab mitut erinevat tüüpi väärtusi nimetatakse programmeerimiskeeltes polümorfismiks. Näiteks 5 võib tähistada täisarvu Int kui ka ujukomaarvu Double.
Polümorfisme on mitut erinevat sorti. Näiteks võib polümorfismiks nimetada alamtüüpimist, parameetrilist polümorfismi ja ad-hoc polümorfismi. Järgnevalt arutleme erinevate polümorfismi sortide üle ja vaatame, mis on funktsionaalprogrammeerimises relevantne.
Programmeerimiskeeles Java on List<String> tüübi Collection<String> alamtüüp. Seega iga sõnede list on ka sõnede kollektsioon ja sama sõnede list on ühes kontekstis list ja teises kollektsioon.
Funktsionaalprogrammeerimises on alamtüüpimine enamasti seotud kirjete tüübiga, kus tüübiks ei ole kirje nimi vaid kirje signatuur. Idrises kirjete alamtüüpimist ei ole — kirje tüübid on vaja eraldi defineerida ning anda definitsioonile nimi. Seega vaatame keelt OCaml, kus tüüp {x: int, y: int} on tüübi {x: int, y: int, z: int} alamtüüp ehk {x: int, y: int} <: {x: int, y: int, z: int}. Funktsioonile, mis võtab parameetriks kahe väljaga kirje, võib argumendiks anda ka rohkemate väljadega kirje.
Vajadus alamtüüpimise järele sõltub programmeerimiskeeles kasutavatest mustritest. Mõningatel juhtudel võib sama efekti, näiteks et 5 on nii Int kui Double, saavutada nii alamtüüpimise kui ka näiteks ad-hoc polümorfismi kasutades.
Parameetriline polümorfism võimaldab sama koodi rakendada sõltumata andmete konkreetsest tüübist. Üks lihtsaim parameetrilise polümorfismi näide on identsusfunktsioon id : a -> a, mis tagastab sisendi olenemata tüübist.
Paramteetrilist polümorfismi tunneb Idrises ära selle järgi, et tüübis on kasutatud tüübimuutujaid. Näiteks map : (a -> b) -> List a -> List b on polümorfne funktsioon. Kui öeldakse polümorfne funktsioon, siis mõeldaksegi enamasti parameetrilist polümorfismi.
Funktsioonile map saab rakendada suvalist tüüpi funktsiooni ning tulemuseks on vastav listide teisendusfunktsioon.
Idrises on sisuliselt kaks võimalust luua tüübiparameetrit. Esiteks juba nähtud implitsiitne võimalus, kus kasutatakse mingit uut muutujanime. Näiteks funktsiooni filter : (a -> Bool) -> List a -> List a puhul kasutame implitsiitset parameetrit a eeldusel, et selles kontekstis pole a-l mingit definitsiooni.
Implitsiitse tüübiparameetri skoop on kogu defintsioon ehk, näiteks, filter-i tüübis (a -> Bool) -> List a -> List a kõik a-d on sama väärtusega ja seda a-d saab kasutada ka definitsioonis.
Näiteks, saame filter defineerida hoopis järgnevalt. Pane tähele, et let-is kasutatakse ka sama a-d.
| 1filter : (a -> Bool) -> List a -> List a 2filter p [] = [] 3filter p (x::xs) = 4 let rs : List a 5 rs = filter p xs in 6 if p a then x :: rs else rs |
Teine võimalus on eksplitsiitselt defineerida funktsioonile parameeter tüübiga Type ja anda väärtusele nimi. Seejärel saab defineetirud nime tüübis kasutada ning definitsioonis saab esimesele parameetrile anda uuesti nime. Näiteks saame listi pikkust arvutada järgnevalt defineeritud funktsiooniga length.
| 1length : (a: Type) -> List a -> Nat 2length t [] = 0 3length t (x::xs) = 1 + length t xs |
Sellist length definitsiooni kasutades peame esimeseks argumendiks andma list elementide tüübi ja teiseks argumendiks vastava listi. Vaata järgnevaid näiteid.
| Main> length Int [1,2,3] 3 Main> length Bool [True, False] 2 |
Selline eksplitsiitne tüübiparameetrite edastus on kohmakas, kuna tuleb infot korrata. Tegelikult, Idris suudab tihti vajaliku info ise tuletada — saame tüübiargumendi asendada alakriipsuga, näiteks length _ [True, False]. Seetõttu on Idrises võimalus märkida parameetrid implitsiitseks — nende väärtus tuleb tuletada teistest argumentidest. Implitsiitsed parameetrid tähistatakse loogeliste sulgudega. Vaata järgmist length' defintisiooni ja pane tähele, et definitsioonis ja väljakutsel me esimest argumenti ei maini.
| 1length' : {a: Type} -> List a -> Nat 2length' [] = 0 3length' (x::xs) = 1 + length' xs |
Implitiitseteks märgitud parameetreid saab definitsioonides ja mujal kasutada ka ekspltsiitselt — kasutades nimega parameetrite funktsioonikutse süntaksit. Näiteks, length' \{a=Int\} [1,2,3]. Nimedega paramteriseeritud funktsioontüübi puhul võime argumendid anda võrdustega, loogeliste sulgude vahel, komaga eraldatult. Argumentide järjekord pole oluline. Funktsiooni length' puhul anname a väärtuseks tüübi Int.
Parameetriline polümorfism on väga võimas tööriist. Polümorfismi, ehk mingi sümboli kasutamine erinevate tüüpide kontekstis, saab implementeerida lisaparameetrite (s.h. kasutades tüübiparameetreid) abil. Sellise lähenemise nõrgaks küljeks on koodi tekkivad parameetrid, mida ei saa alati implitsiitselt tuletada — kood muutub halvemini loetavaks. Loetavuse hoidmiseks on lisatud keelde Idris ka ad-hoc polümorfism.
Parameetriline polümorfism oli see, kui sama funktsioon töötab eri tüüpi andmetel olenemata tüübist. Ad-hoc polümorfism, seevastu, töötab erinevatel tüüpidel erinevate funktsioonidega. Näiteks, kui tahame sama funktsiooniga kontrollida täisarvude võrdust equal 4 5, sümbolite võrdsust equal 'x' 'x' ja sõnede võrdsust equal "abc" "123". Selline võrduse sümboli equal defineerimine ei ole parameetrilise polümorfismi kaudu otse võimalik. Kindlasti ei saa me teha equal funktsiooni tüübiga a -> a -> Bool, kuna näiteks Integer -> Integer funktsioonide võrdlemine ei ole praktiliselt võimalik — peaksime kontrollima funktsioonide tagastusväärtusi kõikide argumentide puhul.
Idrises saame defineerida liidese Equal a ning selle instantsid Equal Int, Equal Char jne.
| 1interface Equal a where 2 equal : a -> a -> Bool 3 4Equal Int where 5 equal a b = ?eq_Int -- Int'ide võrdsus 6Equal Char where 7 equal a b = ?eq_Char -- Char'ide võrdsus |
Kuigi liideses on kirjas equal : a -> a -> Bool, siis funktsiooni equal tüüp on tegelikult hoopis Equal a => a -> a -> Bool. Ehk, funktsiooni rakendamiseks kahele a-tüüpi argumendile peab leiduma instants Equal a. Kuna meil on defineritud Equal Int ja Equal Int siis saame saame kasutada equal-funktsiooni täisarvudel ja sümbolitel. Kuna me pole instantsi funktsioonidele, siis tuleb tüübiviga, kui proovime täisarvude funktsioone võrrelda — vaata järgmist koodi.
| Main> equal 4 5 False Main> equal (\x => min x 1000) (\ x => x) Error: Can't find an implementation for Equal (Integer -> Integer). (Interactive):1:1--1:33 1 | equal (\x => min x 1000) (\ x => x) ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ |
Idrise standardteegis on defineeritud tüübiklass Eq. Ehk samas liideses on defineeritu nii võrdumise kui mittevõrdumise kontroll. Minimaalne definitsioon peab sisaldama kas (==) või (/=) — puuduoleva funktsiooni definitsiooniks võetakse vaikedefinitsioon.
| 1interface Eq a where 2 (==), (/=) : a -> a -> Bool 3 x /= y = not (x == y) 4 x == y = not (x /= y) |
Kõikidel polümorfsetel funktsioonidel, mis kasutavad võrdust peab tüübi kontekstis olema kitsendus Eq. Näiteks polümorfne paaride listist otsimise funktsioon lookup võib olla defineeritud järgnevalt. Tüübi a elemente saab võrrelda tänu sellele, et kontekstis on kitsendus Eq a.
| 1lookup : Eq a => a -> List (a, b) -> Maybe b 2lookup _ [] = Nothing 3lookup x ((y,z)::ys) = if x==y then Just z else lookup x ys |
Konteksti ei ole mõtet lisada kitsendust konkreetsetele tüüpidele.
| 1eq_test : Eq Int => Int -> Int -- töötab ka: Int -> Int 2eq_test x = if x = 100 then 0 else x |
Liidestel võivad omakorda olla kontekstid — nii tekivad liideste hierarhiad. Näiteks Ord ty liidesel on kitsendus Eq ty. Ehk kõik täielikult järjestatud tüübid on ka võrduskontrolliga. Seetõttu võime kirjutada funktsioonile kitsenduse Ord a ja seejärel kasutada ka võrduskontrolli. Vaatame koodi Idrise standardteegist; minmaalseks implementatsiooniks piisab defineerida compare.
| 1interface Eq ty => Ord ty where 2 compare : ty -> ty -> Ordering 3 (<) : ty -> ty -> Bool 4 (>) : ty -> ty -> Bool 5 (<=) : ty -> ty -> Bool 6 (>=) : ty -> ty -> Bool 7 max : ty -> ty -> ty 8 min : ty -> ty -> ty 9 -- lisaks vaikedefinitsioonid |
Liidese instantsidele saab anda ka nime. Näiteks võime tahta defineerida naturaalarvudele tavalisest vastupidise täieliku järjestuse nimega revord.
| 1 compare Z (S n) = GT 2 compare (S n) Z = LT 3 compare Z Z = EQ 4 compare (S x) (S y) = compare @{revord} x y |
Nüüd saame kasutada sorteerimsfunktsiooni sort : Ord a => List a -> List a (moodulist Data.List), kasutades nii tavalist järjestust ja ka vastupidist järjestust.
| Main> :import Data.List Imported module Data.List Main> sort [1,3,6,4,2] [1, 2, 3, 4, 6] Main> sort @{revord} [1,3,6,4,2] [6, 4, 3, 2, 1] |
Liidestel võib olla ka rohkem parameetreid kui üks aga sellisel juhul ei pruugi kompilaatoril olla võimalik instantse automaatselt leida. Sellisel juhul võib olla abi sellest, kui märkida ära liidese määravad parameetrid. Süntaktiliselt tuleb peale liidese parameetreid kirjutada püstkriips ja anda komadega eraldatult määravad parameetrid. Näiteks, kui tahame defineerida täisarvude listide korrutamist täisarvuga, peame andma liidesele kolm parameetrit, mis vastavad korrutatavate tüüpidele ja tulemuse tüübile.
| 1interface Korda a b c | a, b where 2 mul: a -> b -> c 3 4Korda (List Integer) Integer (List Integer) where 5 mul xs y = map (*y) xs 6Korda Integer (List Integer) (List Integer) where 7 mul y xs = map (*y) xs |
Kui määravaid parameetreid Korda liideses mitte märkida, võib kompilaator jääda hätta liidese leidmisega. Näiteks avaldise mul [1,2,3] 5 tüüpimisel tuleb veateade "Error: Can't find an implementation for Korda (List Integer) Integer ?c"
Üldiselt on mõistlik vältida ülekattega instantse ja anda võimalikult üldised defintisioonid. Näiteks võiks Korda instantsid anda Integer asemel kõikidele tüüpidele, mis rahuldavad Num kitsendust. Liides Num defineerib nimelt liitmise (+) ja korrutamise (*).
| 1Num a => Korda (List a) a (List a) where 2 mul xs y = map (*y) xs 3 4Num a => Korda a (List a) (List a) where 5 mul y xs = map (*y) xs 6 7test_mul : List Double 8test_mul = 5.0 `mul` [1.0,2.0,1.2] |
Liideste ja instantside kohta saab infot standardteegi dokumentatsioonist ning Idrise REPL-ist. Näiteks, kui tahame teada, mis liides defineerib jagamise (/) siis piisab meil anda REPL-i käsk :doc (/). Saame teada, et jagamine on defineeritud kasutades Fractional tüübiklassi. Kirjutades :doc Fractional saame teada, et jagamine on Fractional-i meetod koos pöördväärtuse funktsiooni recip-ga ning et Num on Fractional-i kitsendus. Lisaks näeme, et vaikimisi on Fractional instants vaid ujukomatüübil Double.
| Main> :doc (/) Prelude.(/) : Fractional ty => ty -> ty -> ty Totality: total Visibility: public export Fixity Declaration: infixl operator, level 9 Main> :doc Fractional interface Prelude.Fractional : Type -> Type Parameters: ty Constraints: Num ty Constructor: MkFractional Methods: (/) : ty -> ty -> ty Fixity Declaration: infixl operator, level 9 recip : ty -> ty Implementation: Fractional Double |
Alampeatükis 6.5 vaatasime enumeratsioone. Nüüd näeme, et enumeratsioonid on lihtsalt erisüntaks liidesele Range. Näeme, et vaikimisi on defineeritud instantsid Range Nat, Range Nat ning (Integral a, Ord a, Neg a) => Range a.
| Main> :doc Range interface Prelude.Range : Type -> Type Parameters: a Constructor: MkRange Methods: rangeFromTo : a -> a -> List a -- [x..y] rangeFromThenTo : a -> a -> a -> List a -- [x,y..z] rangeFrom : a -> Stream a -- [x..] rangeFromThen : a -> a -> Stream a -- [x,y..] Implementations: Range Nat (Integral a, (Ord a, Neg a)) => Range a Range Char |
Alampeatükis 7.1 vaatasime listifunktsiooni map, mis on liidese Functor meetod. Functor on defineeritud näiteks tüübiperede Maybe ja List jaoks.
Funktsioonide foldl ja foldr vaatasime peatükkides 7.3 ja 7.2. Need on standardteegis liidese Foldable meetodid ning defineeritud näiteks tüübiperede Maybe ja List jaoks.
Lisaks on väga kasulik liides Show, milles on ainukeseks meetodiks on show, tüübiga Show a => a -> String. Funktsioon show saab kasutada enamike baastüübi väärtuste peal välja arvatud funktsioonid.
Väga kasulik on kahe argumendiga liides Cast a b, mille ainukeseks meetodiks on cast: Cast a b => a -> b. Funktsioon cast saab kasutada näiteks arvutüüpide vahel teisendamiseks. Samas tuleb siin olla ettevaatlik, kuna cast teisendused võivad olla kadudega. Näiteks the Nat (cast "5") on 5 aga the Nat (cast "-5") on 0.
Kasulikud liidesed on veel Applicative ja tema alamliides Monad. Nii Applicative ja Monad on tüübiperede liidesed, s.t. nende argumendid on tüübiga Type -> Type ehk argumentideks sobivad näiteks List ja Maybe. Mainitud liides Monad m modelleerib järjestikuseid arvutusi — kuid selleni jõuame varsti.
Monaadi Monad m intuitsioon üldiselt on, et m a tüüpi väärtused on "masinad, mille tulemus on a tüüpi väärtus." Monaadidel on olenevalt konkreetsest tüübiperest m baas-"masinad".
Näiteks valime IO, ehk sisendit ja väljundit tegeva masina. Selle baas-"masinateks" on näiteks funktsioonid: sisendist lugemine, väljundisse kirjutamine ja juhusliku väärtuse arvutamine. Standardteegis on juhuarvude genereerimine defineeritud paketis contrib moodulis System.Random, ehk selle laadimiseks tuleb REPL-i käivitamiseks anda lipp -p contrib. Liides Random instantsid on standardteegis vaid tüüpidele Int32 ja Double.
|
Intuitiivselt, funktsioon putStrLn võtab argumendiks sõne s ja tagastab masina, mis trükib konsooli sõne s ning tagastab väärtuse (). Funktsioon getLine on masin, mis ootab käsurealt sõne sisestamist ning tagagastab siis selle sõne. Funktsioon randomRIO võtab arvude paari ja tagastab masina, mis tagastab juhusliku arvu paaris olevate arvude vahemikus.
Aga mis kasu on meil masinast nagu putString "Tere, maailm!"? Kasu tuleneb sellest, et Idris oskab neid masinaid käivitada. Näiteks REPL-is saame anda käsu :exec, mille järel IO a tüüpi masin. Pane tähele, et masina käivitamisel selle tagastusväärtust välja ei trükita — juhuarv vahemikus nullist kümneni arvutatakse küll välja aga siis loobutakse sellest.
| Main> :exec randomRIO (0.0,10.0) Main> :exec putStrLn "Tere, maailm!" Tere, maailm! |
Monaadide liidesel on kaks peamist üldist meetodit: funktsioon pure ja operaator (>>=) ehk inglise keeles bind.
|
Funktsioon pure ütleb, et iga väärtuse x kohta leidub triviaalne masin pure x, mille ainuke tegevus on tagastada väärtus x.
Funktsioon (>>=) võtab argumendiks a-tüüpi väärtuse tagastava masina ning funktsiooni, mis iga a-tüüpi väärtuse kohta tagastab masina tüüpi m b. Funktsioonikutse s >>= f on masinate järjestikrakendus — kõigepealt käivitatakse masin s: m a ja saadakse tulemus x: a ja siis käivitatakse masin f x: m b ja saadakse tulemus y: b ning lõpus tagastatakse väärtus y.
Vaatame avaldist randomRIO (0.0,10.0) >>= (\\ x => putStrLn (show x)), mis koostab masina tüübiga IO (). Käivitades leitakse kõigepealt juhuslik ujukomaarv nulli ja kümne vahel ja siis trükitakse see välja.
| Main> :exec randomRIO (0.0,10.0) >>= (\ x => putStrLn (show x)) 0.03542536370122251 Main> :exec randomRIO (0.0,10.0) >>= (\ x => putStrLn (show x)) 5.870265901782135 |
Ühiktüüpi tagastava protseduuri komponeerimiseks saab kasutada operaatorit (>>), mis on defineeritud kui x >> y = x >>= (\ () => y). Intuitiivselt, masin x >> y käivitab masina x ning selle lõppedes käivitatakse masin y ning tagastatakse y-i tagastusväärtus. Vaata järgmist näidet.
| Main> :exec putStr "Tere" >> putStrLn ", maailm!" Tere, maailm! |
Kasutades tingimuslauset või mustrisobitust, saab implementeerida hargnemist; kasutades rekursiooni, saab implementeerida tsükleid. Vaata näiteks järgnevat üheargumendilist protseduuri trykiKuni, mis trükib erinevatele ridadeld numbrid argumendist kuni üheni.
| 1trykiKuni : Int -> IO () 2trykiKuni 0 = pure () 3trykiKuni n = trykiKuni (n-1) >> putStrLn (show n) |
| Main> :exec trykiKuni 3 1 2 3 |
Idris on puhas funktsionaalne keel ja me ei saa, näiteks, teha lihtsat funtksiooni, mis tagastab meile juhusliku täisarvu. Kuna aegajalt meil siiski on tarvis mittepuhtaid programme teha, on välja mõeldud monaadid, mille abil on võimalik mittepuhtaid programme puhtalt modelleerida.
Nagu nägime eelmises peatükis, on Idrises mõne tüübikonstruktori m jaok monaadi liides Monad m, kus on defineeritud funktsioon pure : a -> m a ja operaator (>>=) : m a -> (a -> m b) -> m b.
Meie intuitsiooni järgi on monaadilised väärtused tüübiga m a masinad, mis arvutavad välja mingi a tüüpi väärtuse.
Ehk siis tegelikud mittepuhtad efektid toimuvad alles masina käivitamisel.
Üheks tüübikonstruktoriks on IO, kus väärtus IO a on masin mis toodab a tüüpi väärtuse.
Standardteegis on defineeritud putStrLn : String -> IO (), mis trükib sõne konsooli, ja getLine : IO String, mis lubab kasutajal sisestada rea teksti.
Seetõttu saame mainitud funktsioone kasutades ehitada sisendit ja väljundit kasutava masina. Just nagu tavalise Python-i funktsiooni.
Samas, monaadi liidese funktsioone pure ja (>>=) kasutades ei tule kood eriti loetav. Seetõttu loodi monaadilise koodi selgemaks kirjapanekuks do-notatsioon.
Vaatame, näiteks, järgnevat pseudokoodi, kus teeme arvutuse aaa ning salvestame selle tulemust muutujasse x, seejärel teeme arvutuse bbb ning salvestame selle tulemust muutujasse x. Lõpuks teeme arvutuse ccc. Pane tähele, et arvutus bbb saab kasutada muutujat x ja arvutus bbb saab kasutada nii muutujat x kui ka muutujat y.
| 1 aaa >>= (\ x => 2 bbb >>= (\ y => 3 ccc 4 )) |
Do-notatsioonis on eelnevalt kirjeldatud kood järgnev. Esmalt tuleb kirjutada võtmesõna do, millele järgneb samas veerus algavad käsud. Näeme, kuidas esmalt pannakse muutujasse x masina aaa tulemus. Siis pannakse muutujasse y masina bbb tulemus. Seejärel käivitatakse ccc, mille tagastusväärtusest saab kogu masina tagastusväärtus.
| 1 do x <- aaa 2 y <- bbb 3 ccc |
Do-süntaks algab do-võtmesõnaga, millele järgnevad järjest töödeldavad laused. Selliseid lauseid on kolme sorti.
<- p”. Kui p on tüüpi IO a siis järgnevates lausetes saab kasutada muutujat x : a.
let algavad definitsiooniplokid. Defineeritud nimesid saab järgnevates lausetes kasutada.
IO a. Kui tegemist on viimase lausega, siis on selle lause tagastusväärtus ka kogu masina tagastusväärtus. Vastasel korral on avaldise effekt sama mis lause “_ <- e” puhul — selle masina tagastusväärtust ignoreeritakse ja arvesse läheb vaid masina käivitamise kõrvalmõju.
Tegelikult töötab do-süntaks ka muude monaadidega, kuigi me neid siinkohal lähedalt ei vaata. Aga ka näiteks listid on monaadid ja nende puhul on do-süntaks väga sarnane listikomprehensioonile.
| 1paarid : List (Int, Char) 2paarid = do x <- [1..3] 3 y <- ['a'..'d'] 4 pure (x,y) |
| Main> paarid [(1, 'a'), (1, 'b'), (1, 'c'), (1, 'd'), (2, 'a'), (2, 'b'), (2, 'c'), (2, 'd'), (3, 'a'), (3, 'b'), (3, 'c'), (3, 'd')] |
Idris 2 sisend-väljund süsteem on tegelikult ehitatud lineaarsetele tüüpidele ning monaadiline liides lihtsalt kasutab lineaarsete tüüpidega implementeeritud API-t.
Seetõttu on tegelikult Idrise sisend-väljund funktsioonid eelnevalt mainitust teistsuguse tüübiga.
Näiteks putStrLn : HasIO io => String -> io ().
Lineaarseid tüüpe vaatame peatükis 18 ja seniks võib lihtsalt eeldada, et ainuke HasIO instants ongi tavaline IO.
Järgneb väike ülevaade sisend-väljund protseduuridest Idrise standardteegis. Esmalt konsooli kirjutamise ja konsoolist lugemise protseduurid.
| 1putStr : HasIO io => String -> io () 2putStrLn : HasIO io => String -> io () 3putChar : HasIO io => Char -> io () 4putCharLn : HasIO io => Char -> io () 5getLine : HasIO io => io String 6getChar : HasIO io => io Char |
Kui andmetüübil on Show liides, siis saab seda printida ilma väärtust eksplitsiitselt sõneks tegemata.
| 1print : HasIO io => Show a => a -> io () 2printLn : HasIO io => Show a => a -> io () |
Üks lihtsaim viis mitmelõimelise programmi loomiseks on kasutada funktsioone fork ja threadWait.
Siinkohal peab etteruttavalt mainima, et arv 1 nende funktsiooninde tüübis tähistab seda, et tegemist on lineaarsete funktsioonidega ja seetõttu on meil keelatud lõime identifikaatorist koopia tegemine.
| 1fork : (1 prog : IO ()) -> IO ThreadID 2threadWait : (1 threadID : ThreadID) -> IO () |
Nagu juba eelmises peatükis mainitud, on contrib paketis moodul System.Random, kus leiame liidesed ja funktsioonid juhuarvude loomiseks.
Liides Random võimaldab juhuarve luua, kuid standardteegis on liidese instantsid vaid ujukomaarvude Double ja 32-bitiste täisarvude Int32 jaoks.
| 1interface Random a where 2 randomIO : HasIO io => io a 3 randomRIO : HasIO io => (a, a) -> io a 4 5Random Int32 where ... 6Random Double where ... |
Failidega opereerimiseks on standardteegis moodul System.File, kus muuhulgas on järgnevad protseduurid. Pange tähele, kuidas funktsiooide tüübid juba dokumenteerivad ära, mida nendest definitsioonidest oodata võiks.
| 1copyFile: HasIO io => (src: String) -> (dest: String) -> 2 io (Either (FileError, Int) ()) 3writeFile: HasIO io => (filePath: String) -> (contents: String) -> 4 io (Either FileError ()) 5appendFile: HasIO io => (filePath: String) -> (contents: String) -> 6 io (Either FileError ()) 7readFilePage: HasIO io => (offset: Nat) -> (until: Fuel) -> (fname: String) -> 8 io (Either FileError (Bool, List String)) |
Moodulis System.Clock on aja, kellade ja kuupäevadega seotud definitsioonid. Defineeritud on abstraktne andmestruktuur OSClock, mis vastab mingile kellaajale vastavas operatsioonisüsteemis ja millest omakorda saab teha Idrise kellaaja tüübiga Clock type. Viimasest saab vastavate funktsioonidega välja lugeda aja sekundites ja nanosekundites.
| 1clockTimeUtc : IO OSClock 2clockTimeProcess : IO OSClock 3clockTimeThread : IO OSClock 4fromOSClock : {type : ClockType} -> OSClock -> IO (Clock type) |
Selles peatükis võrdleme normaaljärjekorras- ja aplikatiivjärjekorras redutseerimist. Kumba eelistada ja mis on eelised ja puudused. Meenutuseks: normaaljärjekord redutseerib alati välimise vasakpoolse alamtermi ja aplikatiivjärjekord redutseerib alati sisemise vasakpoolse alamtermi.
Normaaljärjekorras redutseerimise eeliseks on, et ei redutseerita argumente mida ei kasutata. Näiteks term (λx. 0) (fact 100) väärtustub nulliks ühe sammuga, kuigi fact 100 väärtustamiseks võib minna väga palju samme. Seega võime funktsiooni argumendina kasutada ka terme, millel endal pole normaalkuju.
Vaatame makrodefinitsiooni from := Y (λf n. consn (f (add 1 n))), mis seab igale täisarvule vastavusse lõpmatu listi alates sellest arvust. Vaata termi from 1 reduktsiooni ja pane tähele, et sellel puudub normaalkuju.
|
Aplikatiivjärjekorras redutseerimisel ei saa sellist definitsiooni kasutada, kuna sellist alamtermi sisaldav termi redutseerimine ei termineeru kunagi. Normaaljärjekorras redutseerimisel saame aga võtta selle lõpmatu listi peas oleva väärtuse. See tähendab, et argumenti from 1 väärtustatakse vaid niikaua, kuni selle peasse tekib cons — siis läheb redutseerimisele välimine δ-reedeks.
|
Lisaks, saame defineerida funktsiooni, mis võtab lõpmatu listi algusest etteantud arvu elemente. Vaata järgnevalt defineeritud funktsiooni take. Sellise funktsiooni kasutamine töötab samuti vaid eeldusel, et argumenti ei redutseeritaks oluliselt rohkem kui seda vaja läheb.
Vaata järgnevat normaaljärjekorras reduktsiooni. Paneme tähele, et reduktsioonijada on üsna pikk (tegelikult 34 sammu) isegi kui võtame lõpmatust listist vaid kaks elementi. Lisaks on näha, et mingid reduktsioonid korduvad: sub 2 1 redutseetitakse esimese take rakenduse juures väärtuseks 1 aga hiljem tuleb see uuesti teha sub (sub 2 1) 1 juures. Samamoodi tuleb arvutada tl(from 1) ja siis hiljem jälle otsast peale tl(tl(from 1)).
|
Reduktsioonisamme tuleks vähem (kokku 24), kui alamterm from 1 redutseerida esmalt termiks cons1 (cons2 (from 3)). Aga ka see pole kaugeltgi optimaalne.
Reduktsioonisammude arvu vähendamiseks on mitu erinevat strateegiat. Üks viis oleks analüüsida kasutatud funktsioone, et teada saada, kas mõnda argumenti, mida kasutatakse funktsiooni kehas mitmes kohas ja on igal juhul vaja välja arvutada. Meie näites on selline argument take-i esimene argument n. Sellisel juhul on mõistlik argument väärtustada enne funktsioonikutset. Mida aga teha take-i teise argumendiga xs? Seda on kasutatud vaid cond-i teises harus — kuid seal kaks korda. Seega ei tohi me püüda seda enne funktsioonikutset väärtustada, kuna väärtustamine ei pruugi termineeruda samas kui selle väärtust tegelikut vaja ei lähe.
Vahemärkusena, kindlasti vajamineva argumendi väljaarvutamine enne funktsioonikutset võib olla ka praktiliselt otstarbekas. Laisk keel Haskell ei väärtusta üldjuhul foldl funktsiooni argumente enne funktsioonikutset. Sellel on aga jõudluses tagajärjed. Seetõttu on Haskelli standardteegis funktioon foldl', mis väärtustab teise argumendi enne funktsioonikutset. Vaata järgnevaid näiteid, kus vastavad fold-i kasutades liidetakse listi [10,20,30] elemendid.
|
Näeme, et tulemus ei muutu ja tehtud sammude arv on sama. Seetõttu võib olla üllatav, et agar funktsioon foldl' on palju kiirem. Vaata Haskelli REPL-is testimist, kus kümne miljoni arvu liitmisel tuleb kümnekordne vahe jõudluses.
| *Main> time $ print $ foldl (+) 0 [0..10000000] 50000005000000 2.895953s *Main> time $ print $ foldl' (+) 0 [0..10000000] 50000005000000 0.268244s |
Haskelli kompilaator GHC sisaldab palju optimeeringuid ja tehnikaid, et lõpmatuid vahestruktuure sisaldav kood võimalikult kiiresti jookseks.Haskellis on kasutatud n.n. graafireduktsiooni, mis tähendab, ühe monoliitse termi asemel on meil definitsioonid ja term, mille sees võivad olla viidad. Kui viida kaudu üht alamtermi väärtustad, siis sama viita kasutav term lõikab sellelt automaatselt kasu. Öeldakse ka, et need alamtermid on jagatud. Tekstuaalsel kujul on tavaks sellist graafi kirjeldada where-dega, mis tuleb mängu siis kui sama parameetrit kasutatakse mitmes kohas ja argument ei ole juba normaalkujul. Näiteks võib see välja näha järgnevalt. Erinevalt Idrisest ei pea Haskellis tüüpe kirjutama. Mittetühja listi konstruktoriks on üks koolon.
Laisk väärtustamine laiemas mõttes ongi funktsiooni argumentide väärtustamie edasilükkamine (näiteks kasutades normaaljärjekorda) kasutades jagamist. Väärtustamine kitsamas mõttes on üks konkreetne viis kuidas normaalkujuni jõuda ilma termi reduktsioonisammudga teisendamata — seda vaatame peatükiks ??.
Kokkuvõtteks, normaaljärjekorras väärtustamine võib leida normaalkuju ka siis kui aplikatiivjärjekorras seda leida ei õnnestu. Sellisel juhul ei pea programmeerija muretsema lõpmatutest definitsioonidest hoidumisest. Samas ei pruugi normaaljärjekorras väärtustamine olla kiirem aplikatiivjärjekorras väärtustamisest. Praktikas kasutatakse reduktsiooni kiiruse tõstmiseks funktsiooni argumentide kasutuse analüüsi ja jagamist/graafireduktsiooni.
Laisa väärtusamise miinuseks on väiksem jõudlus, suurem mälukasutus ja tööaja hindamise suurem keerukus. Seetõttu on populaarsed ka agarad funktsionaalsed keeled nagu Swift, Lisp, OCaml, Erlang jne. Ka kompileeritud Idrise programmid väärtustatakse aplikatiivjärjekorras. Lisaks on peaaegu kõik multi-paradigma keeli, kus saab FP stiilis programmeerida, agarad.
Samas on ka vaikimisi agarates keeltes võimalik kasutada laiskust ja lõpmatuid struktuure. Näiteks Idrises on tüübikonstruktorid Lazy ja Inf ning funktsioonid Delay ja Force. Esmalt vaatame andmetüüpi Stream, mis on standardteegis defineeritud järgnevalt.
| 1data Stream a = (::) a (Inf (Stream A)) |
Defineeritud on vaid üks konstruktor (::) : a -> Inf (Stream a) -> Stream a, kuna tühja striimi olemas ei ole.
Konstruktori esimene argument on striimi pea ja teine argument on saba, mis on pandud Inf kontruktsiooni sisse. Enamasti saab Idris ise hakkama tüüpide A ja Inf A vahel teisendamisega. Harva on ise vaja panna mõni Delay või Force.
| Main> the (Inf Int) (5+5) Delay (5 + 5) Main> Force (the (Inf Int) (5+5)) 10 |
Ehk, kui tahame listi ühest seitsmeni, saame kirjutada [1..7] ja selle väärtustamine annab [1, 2, 3, 4, 5, 6, 7]. Kui tahame striimi ühest lõpmatuseni, kirjutame [1..]. Pane tähele, et seda ei arvutata välja kaugemale kui üheni. Aga kui võtame esimesed seitse elementi sellest lõpmatust listist, siis saame jälle sama tulemuse nagu [1..7].
| Main> [1..7] [1, 2, 3, 4, 5, 6, 7] Main> [1..] 1 :: Delay (countFrom 2 (\arg => prim__add_Integer 1 arg)) Main> take 7 [1..] [1, 2, 3, 4, 5, 6, 7] |
Lõpmatute andmestruktuuride kasutamise motivatsiooniks on võimaldada eraldada vahestruktuuri loomist tarbimisest. Näiteks kirjeldas vanakreeka matemaatik Eratosthenes viisi kuidas leida algarvude tabelit, viisil, kus lõpmatust arvude jadast 2, 3, 4, 5, 6 jne. filtreeritakse välja kõigepealt kahest suuremad kahekordsed, siis kolmest suuremad kolmekordsed, siis neljast suuremad neljakordsed jne. Alles jäävad algarvud. Järgnev kood implementeerib Eratosthenese algoritmi Idrises. Seejärel saab kuus esimest algarvu välja arvutada avaldisega take 6 primes mis tagastab listi [2, 3, 5, 7, 11, 13]
| 1filter : (a -> Bool) -> Stream a -> Stream a 2filter p (x :: xs) = 3 if p x then 4 x :: filter p xs 5 else 6 filter p xs 7 8iterate : (a -> a) -> a -> Stream a 9iterate f x = x :: iterate f (f x) 10 11sieve : Stream Int -> Stream Int 12sieve (p::xs) = filter (\x => x `mod` p /= 0) xs 13 14primes : Stream Int 15primes = map head (iterate sieve [2..]) |
See kood on Idrises natuke kohmakas (ja aeglane). Laisusele optimeetirud keeles Haskell saame kasutada standardteegi funktioone filter ja iterate ning ei pea kirjutama sieve tüüpi. Haskelli versioon Eratosthenese algoritmist on järgnev.
This document was translated from LATEX by HEVEA.