Idris on puhas funktsionaalne keel ja me ei saa, näiteks, teha lihtsat funktsiooni, 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 jaoks 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 selliseks 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.
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.
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 y. Lõpuks teeme arvutuse ccc. Pane tähele, et arvutus bbb saab kasutada muutujat x ja arvutus ccc 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 |
Ehk konkreetselt, näiteks järgnev programm, kus küsitakse kasutajalt nimi ja tervitatakse teda nimeliselt. Pane tähele, et kuna putStrLn tüüp on String -> IO () siis muutuja x väärtus on ().
| 1tervitus : IO () 2tervitus = do x <- putStr "Kirjuta oma nimi: " 3 y <- getLine 4 putStrLn ("Tere, "++y++"!") |
| Main> :exec tervitus Kirjuta oma nimi: Kalmer Tere, Kalmer! |
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 19 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 funktsioonide tüübis tähistab seda, et tegemist on lineaarsete funktsioonidega ja seetõttu saame neid funktsioone kasutada ka siis kui argumendist koopia tegemine on keelatud.
| 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) |
t2ring : IO (), mis trükib juhuarvu vahemikust 1 kuni 6.
prindiArvud : List Int32 -> IO () ning protseduur trükiNimekiri : Stream String -> List String -> IO ().
loeArv : IO Int32, mis kordab küsimist kuni sisend on korrektne mittenegatiivne täisarv.
summa2 : IO (), mis küsib kaks arvu ja trükib summa. Laiendage lahenduseni summaN, mis summeerib n sisestatud arvu.