Modulszerkezet
Az Idris modulok:
- függvények, típusok, típusosztályok definícióit tartalmazzák
- fontos a függvények sorrendje
Ha egy függvényt előbb kezdünk használni, minthogy definiálnánk, akkor a fordító hibát jelez.
A modulokban a függvények, típusok és típusosztályok elé megadhatunk egy láthatóságot az alábbiak közül:
- private
- abstract
- public
Az alapértelmezett láthatóság a private, ekkor az adott entitás nem lesz látható kívülről. Abstract esetén csak a név lesz kívülről látható. Függvényeknél ez azt jelenti, hogy az implementáció nem látszik majd. Adattípusoknál azt, hogy a típus neve látható lesz, de a konstruktorok nem. Osztályoknál az osztálynév lesz látható, a benne lévő függvények neve viszont nem. Public láthatóság értelem szerűen annyit jelent, hogy minden látható lesz kívülről.
Példa modul:
module easy
import mymodule
private
getZero : Nat
getZero = Z
public
id' : a -> a -> a
id' x = a
abstract
listif : Bool -> (List Nat) -> (List Nat) -> (List Nat)
listif first second bool = if bool then first else second
public
main : IO ()
main = do return ()
Az Idris programok belépési pontja a main függvény.
Névterek
Minden Idris modul egy saját névtérrel rendelkezik, így előfordulhat, hogy több modul is tartalmaz ugyanolyan nevű függvényt. Jól mutatja ezt a listák, illetve a vektorok Nil konstruktora (ez is egy függvény). Az, hogy egy adott esetben melyik modul függvényére hivatkozunk, a típus alapján kell, hogy eldőljön. Lehetőség van egy modulon belül is létrehozni névtereket:
module mymodule
namespace namesp1
-- valami.t1.test
test : Int -> Int
test x = 42
namespace namesp2
test : String -> String
test x = „appletree”
Függvények
Az Idris programok legfontosabb elemei a függvények:
- kötelező megadni a típusukat
- definíciójuk mintaillesztéssel történik
- where klózban tartalmazhatnak lokális definíciókat
A példa az előbbieket szemlélteti:
stringLengthSum : (List String) -> Nat
stringLengthSum xs = foldl add zero lengthList
where add : Nat -> Nat -> Nat
add x y = x + y
zero : Nat
zero = 0
lengthList : (List Nat)
lengthList = map (the (String -> Nat) length) xs
A legelső sor a típust adja meg. A where olyan definíciókat tartalmaz, melyek csak a függvénytörzsben vannak érvényben. A the függvény "típuskényszerítésre" használható, azaz megmondja a fordítónak, hogy mi a Stringek hosszát megadó length függvényt szeretnénk használni.
Implicit paraméterek
Egyes függvények típusában függő típusok is vannak. Ebben az esetben a típus azért függő, mert valamilyen értéktől függ. Ez az érték implicit paraméterként jelenik meg. Függvény típusa implicit paraméterek kiírása nélkül:
index : Fin n -> Vect n a -> a
Ha kiírjuk az implicit paramétereket:
index : {a : Type} -> {n : Nat} -> Fin n -> Vect n a -> a
Példa ugyanebben az esetben függvényhívásra:
index {a=Int} {n=2} 0 (2 :: 3 :: Nil)
Valójában bármelyik argumentumnak adható név:
index : (i : Fin n) -> (xs : Vect n a) -> a
Mutual
Időnként előfordul, hogy egymást hívó függvényeket szeretnénk megadni. Ekkor használhatjuk a mutual blokkot.
mutual
even : Nat -> Bool
even Z = True
even (S k) = odd k
odd : Nat -> Bool
odd Z = False
odd (S k) = even k
Először a deklaráció, aztán a függvénytest kerül hozzáadásra.