Uusi tüüpe saab Idrises luua kahel viisil: võtmesõnaga data ja definitsiooniga, mille tulemus on tüüpi Type. Esmalt vaatame definitsioone.
Idris on n.n. sõltuvate tüüpidega programmeerimiskeel — me vaatame hiljem täpsemalt, mida see tähendab. Sõltuvate tüüpidega programmeerimiskeelte puhul on tavaline, et tüübid spetsifitseeritakse samasuguste avaldistega kui definitsioonid. Ehk siis tüübid võivad sisaldada lambdasid, funktsioonikutseid, tingimuslauseid jne.
Näiteks saame defineerida tüübisünonüümid, kus avaldised Pikkus ja Laius väärtustuvad täisarvutüübiks Int. Selline kood on hea koodi dokumenteerimiseks või kui me hiljem soovime definitsioone muuta.
| 1Pikkus : Type 2Pikkus = Int 3 4Laius : Type 5Laius = Int |
Sellised tüübisünonüümid ei sobi aga kasutusjuhtudeks, kus tahame eristada väärtust tüübiga Pikkus väärtusest tüübiga Laius. Näiteks, kui meil on h: Pikkus ja w: Laius ning funktsioon rk_pindala: Pikkus -> Laius -> Pindala siis saame seda välja kutsuda kui rk_pindala w h.
Saame teha ka funktsiooni, mis tagastab tüübi. Funktsioon Punkt : Nat -> Type võtab parameetriks naturaalarvu ja seab sellele vastavusse ujukomaarvude enniku, milles on parameetri jagu komponente. Vaata järgnevat koodi.
| 1Punkt : Nat -> Type 2Punkt 0 = () 3Punkt 1 = Double 4Punkt (S n) = (Double, Punkt n) 5 6vec3d : Punkt 3 7vec3d = (1.0,0.0,1.0) |
Sarnaselt saame teha ka funktsioone, mis võtavad parameetriteks ning tagastavad tüüpe. Näiteks funktsiooni Ennik : List Type -> Type, mis võtab parameetriks tüüpide listi ja seab sellele vastavusse enniku, mille komponendid on vastava parameetri listi elemendid. Vaata järgnevat koodi. Pane tähele, et nii Punkt 3 kui ka Ennik [Double,Double,Double] väärtustuvad tüübiks (Double,Double,Double).
| 1Ennik : List Type -> Type 2Ennik [] = () 3Ennik [t] = t 4Ennik (t::ts) = (t,Ennik ts) 5 6test1 : Ennik [String, Double, Char] 7test1 = ("tere", 1.5, 'x') 8 9test2 : Ennik [Double, Double, Double] 10test2 = vec3d |
Teine võimalus uute tüüpide loomiseks on data võtmesõnaga, kus loetletakse üles kõik väärtuste (vajadusel parametriseeritud) variandid. Selliselt defineeritud tüübis on variandid lõikumatud ja injektiivsed. Vaatame erinevaid võimalusi näidete põhjal. Esmalt vaatame, kuidas on Idrises defineeritud tõeväärtuste tüüp Bool.
| 1data Bool = True | False |
Sellest koodireast loeme välja järgnevat: defineeritakse uus andmetüüp Bool: Type, defineeritakse konstruktor True: Bool,defineeritakse konstruktor False: Bool.
Lähtudes lõikumatusest, teame et tõesus True ja väärus False on erinevad.
Ning kuna loetleti üles kõik variandid, siis tähendab, et kõik tõeväärtused on kas True või False.
Seetõttu on põhjendatud, miks saame kasutada mustrisobitust.
| 1not : Bool -> Bool 2not True = False 3not False = True |
Tõeväärtustest Bool veel lihtsama struktuuriga andmetüüp on ühiktüüp, mis on standardteegis defineeritud järgnevalt. Pane tähele, et Idrise kompilaator asendab () vastavalt vajadusele kas Unit-ga või MkUnit-ga. Väärtusele tüübiga () on võimalik teha mustrisobitust, aga see ei anna praktikas infot juurde.
| 1data Unit = MkUnit 2test_Unit : () -- sama mis Unit 3test_Unit = MkUnit -- sama mis () 4f1, f2 : Unit -> Unit 5f1 () = () 6f2 _ = () |
Jätkates ühe konstruktoriga andmetüüpidega, vaatame paari tüübipere definitsiooni standardteegis. Tüübipere tähendab siinkohal seda, et Pair iseseisvalt ei ole tüüp vaid vajab tüübiks saamiseks kaht argumenti. Tüübil on üks konstruktor MkPair : a -> b -> Pair a b. Siin Idrise kompilaator asendab (,) vastavalt vajadusele kas Pair-ga või MkPair-ga. Seega MkPair-i tüübiks võib kirjutada ka a -> b -> (a, b).
| 1data Pair a b = MkPair a b 2test_pair : (Int, Char) -- sama mis Pair Int Char 3test_pair = MkPair 4 'x' -- sama mis (4, 'x') 4add_pair : (Int, Int) -> Int 5add_pair (x, y) = x + y |
Tähtis andmestruktuur on ka Either a b, mille väärtus sisaldab kas a väärtust või b väärtust.
Konstruktor Left : a -> Either a b võtab argumendiks Either-i esimese parameetri tüübiga väärtuse ja Right : b -> Either a b võtab argumendiks Either-i teise parameetri tüübiga väärtuse.
| 1data Either a b = Left a | Right b |
Teeme kõrvalpõike algebrasse. Paaride tüüp on mingis mõttes tüüpide (otse)korrutis, kuna paaride väärtuste arv on komponent-tüüpide väärtuste arvude korrutis ehk |Pair A B| = |A| * |B|, kus |·| on funktsioon, mis seab tüübile vastavusse tema väärtuste arvu. Lisaks, ühiktüüp on selle korrutise ühikelement. Algebrast tuntud struktuuri ringi saamiseks oleks vaja teada ka, mis on tüüpide summa. Selleks ongi tüübipere Either, mis vastab väärtuste hulkade lõikumatu ühendi operatsioonile. Kehtib |Either A B| = |A| + |B|.
Naturaalarvud on standardteegis defineeritud kahe konstruktori Z ja S kaudu. Kusjuures konstruktoril S on argument tüübiga Nat. Seega naturaalarvud on defineeritud induktiivselt: Z on naturaalarv ja iga naturaalarvu n : Nat kohta teame, et S n on naturaalarv.
| 1data Nat = Z | S Nat |
Kuigi konstruktoril S on funktsioonitüüp Nat -> Nat siis tegemist pole suvalise funktsiooniga vaid injektiivse konstruktoriga. Injektiivne tähendab siin kontekstis seda, et rakenduse informatsioon ei lähe kaduma. See tähendab muuhulgas, et S (S Z) erineb väärtusest S Z.
Tüüpide algebraga (Pair, Unit ja Either) ning funktsioonitüübiga saame luua väga palju kasulikke andmetüüpe ilma ise data võtmesõna kasutamata. Näiteks tõeväärtuste asemel võtta Either () (). Probleem tekib aga rekursiivsete andmetüüpidega. Näiteks naturaalarve võiks saada defineerida kui MyNat = Either () MyNat. See aga kahjuks Idrises ei tööta.
Listide definitsioon on väga sarnane naturaalarvudele — lisatud on parameeter tüübile ja teisele konstruktorile. Listid List a on standardteegis defineeritud kahe konstruktori Nil ja (::) kaudu. Kusjuures konstruktoril (::) on argumendid tüübiga a ja List a.
| 1data List a = Nil | (::) a (List a) |
Idrise kompilaator asendab [] konstruktoriga Nil ja konstantide listi
[x1, … , xn]
konstruktsiooniga x1 :: … :: xn :: Nil .
Nüüd vaatme väga kasulikku tüübiperet Maybe : Type -> Type. Esimene võimalus Maybe a tüüpi väärtuse loomiseks on konstruktoriga Nothing. Teine võimalus on konstruktoriga Just, millele tuleb argumendiks anda a tüüpi väärtus.
| 1data Maybe a = Nothing | Just a |
Tüüp Maybe lisab väärtsute hulgale ühe väärtuse, mida kasutatakse tihtipeale nurjumise tähistamiseks. Näiteks paaride listist otsimise funktsioon lookup kasutab tulemuses väärtust Nothing tähistamaks, et listis otsitavat paari ei leidu.
| 1lookup : Int -> List (Int,b) -> Maybe b 2lookup x [] = Nothing 3lookup x ((y,z)::ys) = if x==y then Just z else lookup x ys |
Funktsiooni lookup saame kasutada järgnevalt:
lookup 4 [(3,'x'),(4,'y')] == Just 'y'
lookup 2 [(3,'x'),(4,'y')] == Nothing
Algebraliste andmestruktuuride loomise süntaks on väga võimas ja paindlik. Samas, on selle abil tüütu kirjutada andmestruktuure, kus on üks konstruktor ja sellel palju argumente. Sellise erijuhu jaoks on loodud n.n. kirjete süntaks.
Näiteks saame teha andmestruktuuri kahemõõtmelise ruumi punktidele
| 1record Punkt where 2 constructor MkPunkt 3 x : Double 4 y : Double 5 6record Ring where 7 constructor MkRing 8 kesk : Punkt 9 raadius : Double 10 11test_punkt : Punkt 12test_punkt = MkPunkt 5.0 4.0 13 14test_ring : Ring 15test_ring = MkRing { kesk = test_punkt, raadius = 6.0} |
Selline süntaks loob tüübid Punkt: Type ja Ring: Type ning andmekonstruktorid MkPunkt: Double -> Double -> Punkt ja MkRing: Punkt -> Double -> Ring. Pane tähele, et konstruktori argumendid tulevad väljadest.
Kirjete loomiseks on kaks võimalust: tavaline konstruktori süntaks (kasutatud test_punkt puhul) ja kirje loomise süntaks (kasutatud test_ring puhul). Kirje loomise süntaks algab konstruktori nimega, millele järgnevad väljade väärtuste kirjeldused loogeliste sulgude vahel. Väljade väärtused võib defineerida suvalises järjekorras.
Argumendi väärtuse edastamine nime kaudu pole tegelikult seotud kirjete süntaksiga. Saame ka ise teha funktsiooni, mille argumentidel on nimed, ning kutsusda see funktsioon välja andes parameetritele nimeliselt väärtused.
| 1loo_ring : (x: Double) -> (y: Double) -> (r: Double) -> Ring 2loo_ring x y r = MkRing (MkPunkt x y) r 3 4test_ring2 : Ring 5test_ring2 = loo_ring {x=10, r=4, y=10} |
Kirjete puhul on eriline aga see, et saab kasutada kirje uuendamise süntaksit. See võimaldab luua uue kirje vana kirje baasilt, kus mõned väljad on muudetud. See töötab nagu järgnevas väites. Esmalt loogelistes sulgudes muudatused ja selle järel (nagu funktsioonirakendus) kirje. Uuendus ‘’:=’-ga kirjutab vana väärtuse üle. Uuendus ‘’$=’-ga rakendab vanale väärtusele funktsiooni. Pane tähele, et uuendatav väli võib minna läib mitme kirje kihi.
| Main> test_ring MkRing (MkPunkt 5.0 4.0) 6.0 Main> {raadius := 1} test_ring MkRing (MkPunkt 5.0 4.0) 1.0 Main> {kesk.x := 1} test_ring MkRing (MkPunkt 1.0 4.0) 6.0 Main> {kesk.x $= (+1)} test_ring MkRing (MkPunkt 6.0 4.0) 6.0 Main> {kesk.y $= (*2)} test_ring MkRing (MkPunkt 5.0 8.0) 6.0 |
Lisaks konstruktori mustrisobitusele defineeritakse kirjete puhul ka selektorid. Punktide puhul siis (.x): Punkt -> Double ja (.y): Punkt -> Double ning ringide tüübi jaoks (.kesk): Ring -> Punkt ja (.raadius): Ring -> Double.
Punktiga algavad funktsioonid on erilised, kuna neid saab rakendada Java meetoditele sarnaselt argumendist paremal.
| Main> test_punkt MkPunkt 5.0 4.0 Main> test_punkt.x 5.0 Main> test_ring.kesk.y 4.0 |