Típusszerkezet
Az Idris típusszerkezete hasonló a Haskell-éhez, viszont annál erősebb, hiszen úgynevezett "függő típusokat" is megenged. Függő típus alatt olyan típust értünk, amely függ valamely értéktől. Ez azt jelenti, hogy a program viselkedését tulajdonképpen megadhatjuk (bizonyos mértékig) a típusok segítségével. Ezáltal nehezebb rossz programot írni, könnyebbé válik a helyességbizonyítás, tisztább, érthetőbb kód hozható létre. A függő típusosság (más eszközökkel együtt) lehetőséget ad arra is, hogy az Idrist mint helyességbizonyító rendszert használjuk.
Egy fontos megjegyzés az Idris statikusan, szigorúan típusos rendszeréhez, hogy itt sincs altípusosság, ugyanúgy, ahogy Haskellben.
Elemi típusok
Az Idris az alábbi primitív típusokat tartalmazza:
- Int (architektúrától függően 32 vagy 64 bites)
- Integer (tetszőlegesen nagy természetes szám)
- Char (karakter)
- String (karakterlánc)
- Ptr ("idegen" pointer, külső nyelvek típusaihoz)
Algebrai adattípusok
Az algebrai adattípusok alapvető fontosságúak, programjainkban ezekkel reprezentálhatjuk modellünk egyes részleteit. Nevüket arról kapták, hogy két művelettel képezhetőek:
- Összeadás (a "|" jel, több konstruktor bevezetése)
- Szorzás (többparaméteres konstruktor bevezetése)
Az algebrai adattípusoknak az alábbi fajtáiról beszélhetük:
Felsorolási ahol a konstruktoroknak nincs paramétere
data Colour = Red | Green | Blue
Parametrikus ahol a típuskonstruktor egy vagy több típusparamétert vár, tehát tulajdonképpen egy olyan függvény, amely egy vagy több típusból hoz létre egy újat
data Elem a = Celem a
Rekurzív ahol valamelyik típuskonstruktor típusában szerepel maga az algebrai adattípus
data List a = Nil | Cons a (List a)
Rekord
record Person : Type where
MkPerson : (name : String) -> (age : Int) -> Person
Mint láthatjuk, a rekordok valójában algebrai adattípusok. A record kulcsszó használatával a fordító automatikusan elkészíti az elérőfüggvényeket az egyes mezőkhöz, illetve használható az úgynevezett rekord-szintaxis, amelynél egy myrec Myrecord típusú entitás field1 mezőjére az alábbi módon hivatkozhatunk frissítéskor: record { field1=newvalue } myrec
Függő típusok
A függő típusok vagy indexelt típusok a típusban értéket (indexet) tartalmaznak, ettől függnek. A leggyakrabban emlegetett példa függő típusra a vektor, amely tulajdonképpen olyan listaként képzelhető el, melynek típusa tartalmazza annak hosszát:
data Vect : Nat -> Type -> Type where
Nil : Vect Z a
(::) : a -> Vect k a -> Vect (S k) a
Az ilyen vektorok tipikus művelete az összefűzés, amely egy n és egy m hosszú vektorból egy n+m hosszút csinál:
(++) : Vect n a -> Vect m a -> Vect (n + m) a
(++) Nil ys = ys
(++) (x :: xs) ys = x :: (xs ++ ys)
A függő típusok közé tartoznak a függő párok is, ahol a pár második eleme az elsőtől függ.
vec : (n : Nat ** Vect n Int)
vec = (2 ** [3, 4])
Az ilyen párokat használhatjuk arra, hogy egy szűrőfüggvény visszatérési értékében megadjuk, hány elemű lett a valamely predikátum szerint megszűrt vektor:
filter : (a -> Bool) -> Vect n a -> (p ** Vect p a)
Léteznek függő rekordok is, ahol az egyes mezők között áll fenn függőség. Az ilyen rekordok csak úgy frissíthetők, hogy a függőség megmaradjon (jóltípusozottság), különben a típusellenőrző hibát jelez.
Típusosztályok
A típusosztályokat legjobban talán az objektumelvű nyelvek interfész fogalmához hasonlíthatjuk. Egy típusosztály definiálandó függvényeket tartalmaz, azon típusoknak, amelyeknek van példánya a típusosztályra, meg kell valósítaniuk ezeket a függvényeket. Egy egyszerű példa a Show, amely arról gondoskodik, hogy egy típus egy példánya a képernyőn ábrázolható legyen (mint szöveg):
class Show a where
show : a -> String
data Elem = AnElem
instance Show Elem where
show AnElem = "Element"
A típusosztályok segítségével szimulálható az objektumelvű nyelvekből ismert altípusosság, amely egyébként nincs jelen az Idrisben.
Monádok
Az Idris standard library is támogatja a monadikus programozást (a Haskellhez hasonlóan). A Monad valójában egy típusosztály, azon típusokat, melyeknek van rá példányuk, nevezzük monádoknak. A monádok segítségével egységbe zárhatunk és a felhasználó elől elrejthetünk valamilyen számítási logikát, például a potenciálisan sikertelen számítást vagy input/output kezelését (IO). Utóbbi egyébként az Idrisben már beépítetten benne van ugyanúgy, mint a Haskell esetében. Egy eltérés etéren a két nyelv között, hogy az Idris interpreter nincsen benne egy implicit IO monádban, így ha az értelmezőből szeretnénk IO műveleteket végezni, a :x EXPRESSION speciális parancsot kell használnunk.