Augud
Avaldisse saab kirjutada n.n. auke, süntaksiga ?nimi. Näiteks:
näide : ?auk1 -> Maybe ?auk2 näide x = ?auk3
Selline kood on valiidne: seda saab kompileerida ja lugeda REPL-sse, kus saab küsida käsuga :m, millised augud vajavad veel implementeerimist:
Main> :m 3 holes: Main.auk1 : Type Main.auk2 : Type Main.auk3 : Maybe ?auk2
Lisaks, küsides augu tüüpi, saame teada ka veel selle augu implementeerimisel olemasolevaid kohalikke muutujaid. Näiteks, auk3 täitmiseks saame kasutada muutujat x, millel tüüp on vaja veel implementeerida.
Main> :t auk3
x : ?auk1 [no locals in scope]
------------------------------
auk3 : Maybe ?auk2
VSCode pluginas näeb augu tüüpi, kui selle peal kursoriga hõljuda.
Miks "no locals in scope"?
Pane tähele, et aukude skoobid on erinevad -- muutujad, mis on ühe augu jaoks nähtavad, võivad teise augu jaoks olla teise nimega või hoopis nähtamatu.
näide2 : (x:Int) -> (y: ?aukA) -> (z:Int) -> Int näide2 a b c = ?aukB
aukA jaoks on skoobis x : Int.
Main> :t aukA
x : Int
------------------------------
aukA : Type
aukB jaoks on skoobis a, b ja c nii, et b tüübi jaoks on nähtav a (mitte x).
Main> :t aukB
a : Int
b : ?aukA [locals in scope: a]
c : Int
------------------------------
aukB : Int
VSCode + Idris Language Plugin (või Emacs + idris2_mode)
Tänu IDE ja REPL-i koostööle võimaldab Idris interaktiivset programmeerimist. Implementeerimisel kasutatakse auke, et saada tagasisidet, mis tüüpi väärtus sinna peab minema ning mis muutujad on skoobis.
Osa implementeerimisest tehakse automatiseeritult; näiteks mustrisobitus ja tüübi järgi avaldise genereerimine.
Parameetri Mustrisobitus
Tahame näiteks implementeerida tõeväärtuse negatsiooni:
not : Bool -> Bool not b = ?r1
Minnes kursoriga parameetri b juurde ja vajutades seal ctrl+alt+c (Emacsis: C-c C-c) saame
not : Bool -> Bool not False = ?r1_1 not True = ?r1_2
Ehk siis hargnemine tõeväärtuse põhjal tehakse automaatselt. Edasi tuleb implementeeida augud.
Niimoodi vähendame kirjutamise vaeva ja ei pea vaatama, mis konstruktorid vastaval parameetril on.
Tõestuse otsing
Mõnede üldiste funktsioonide puhul spetsifitseerib funktsiooni tüüp juba ka selle definitsiooni. Tüübile vastava avaldise saab automaatselt leida vajutades augu juures ctrl+alt+p (Emacsis: C-c C-a).
Lihtsamal juhul:
id : a -> a id x = ?r2
Mõnel juhul on mõistlik enne teha (automaatne) mustrisobitus:
f : (a,b) -> (b,a) f p = ?r3 map : (a->b) -> Vect n a -> Vect n b map f xs = ?r4
Selline automaatika on eriti tõhus tõestuste puhul -- seal on peamine küsimus selles, kas implementatsioon üleüldse leidub.