Főbb vezérlési szerkezetek
Az Idris vezérlési szerkezetei eltérnek az imperatív nyelvek vezérlési szerkezeteitől. A programok megírása során nem szekvenciák, elágazások és ciklusok, hanem inkább függvényalkalmazás, kompozíció, mintaillesztés, őrfeltételek és rekurzió segítségével építkezünk. Az alábbiakban láthatjuk a legfontosabb szintaktikai elemeket, vezérlési szerkezeteket, amelyek a programírást segítik.
If ... then ... else kifejezés:
case e1 of True -> e2
False -> e3
Az if szerkezetben e1-nek Bool-nak kell lennie, míg e2-nek és e3-nak azonos típusúnak kell lennie.
Case-kifejezések
Az esetszétválasztás szintaxisa a következő:
if predicate then expr01 else expr02
A predikátum Bool típusú, a két kifejezés azonos típusú. A konstrukció valójában a nyelv szintaxisbővítési lehetőségét használja ki.
Let-kifejezések
A let segítségével köztes értékeket számolhatunk ki, és köthetünk "változókhoz", vagy mintaillesztéseket végezhetünk el. A kötött "változók" scope-ja csak a let-kifejezés belseje.
mirrorlist : List a -> List a
mirrorlist xs = let xs’ = reverse xs in
xs ++ xs
Do-blokkok
A do-szintaxis segítségével monádokat használhatunk egy egyszerűsített jelöléssel. Az ilyen szintaxissal megírt program hasonlít egy imperatív kódra (mintha egy szekvencia lenne).
main : IO ()
main = do putStr "Please, give me a file name!"
filename <- getLine
filecontent <- readFile filename
putStr filecontent
Átírási lépések:
- x <- v; e ehelyett: v »= (\x => e)
- v; e ehelyett: v »= (\_ => e)
- let x = v; e ehelyett let x = v in e
With-szintaxis
A with-szintaxis tulajdonképpen az őrfeltételek egyfajta általánosítása. Segítségével függő mintaillesztéseket végezhetünk. Az alábbi példa a with használatát mutatja be. A parity függvényt és a hozzá hasonló függvényeket nézeteknek nevezzük. A nézet segítségével mintát illesztünk a natToBin argumentumára, a lehetséges alakokat a függőleges vonalak után adjuk meg, mintha azok őrfeltételek lennének (even és odd). A függőleges vonalaktól balra is minták szerepelnek (függő minták, hisz a k parításától függnek). A minták egyes elemeit (j) felhasználjuk a visszatérési érték meghatározásánál az egyenlőségjelektől jobbra.
data Parity : Nat -> Type where
even : Parity (n + n)
odd : Parity (S (n + n))
-- view
parity : (n:Nat) -> Parity n
natToBin : Nat -> List Bool
natToBin Z = Nil
natToBin k with (parity k)
natToBin (j + j) | even = False :: (natToBin j)
natToBin (S (j + j)) | odd = True :: (natToBin j)