λ-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.
Ka Char-d on enumeratsioonid. 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∈Int, 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).