Siin raamatus kasutatakse peamiselt keelt Idris 2 (idris-lang.org), täpsemalt selle keele versiooni 0.8.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 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.
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.8.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 (mis ise ei ole tüüp) 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.
Idrises 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 eelnevate 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 konstruktsiooni, 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 |