Az Idris programozási nyelv

Helyesség

Programok helyessége

A nyelv koncepciója szerint a függvények típusának kell arról gondoskodnia, hogy a program helyes legyen. Egyrészt a függő típusok használatával nagyjából már kifejezhetjük azt, mit kell egy függvénynek csinálnia, másrészt pedig kijelentéseket, állításokat helyezhetünk a típusba, amelyeknek teljesülnie kell. Az ilyen kijelentéseket mindig bizonyítanunk kell (például az interaktív helyességbizonyító segítségével). A bizonyítások maguk is függvények.

Tételbizonyítás

Az Idris interpreter tartalmaz egy interaktív bizonyítót is, mellyel különböző tételeket láthatunk be. Ezeket aztán felhasználhatjuk programjaink típushelyességének bizonyítására, például előállhat az a helyzet, hogy a típusellenőrző nem képes belátni egy fügvény típushelyességét, és nekünk kell "kisegítenünk" manuális bizonyításokkal.
Ha egy programról tudjuk, hogy az típushelyes, de nem fordul le, helyettesítsük a fordító által hibásnak ítélt részt "ideiglenes definícióval" (= helyett ?=). Ilyenkor az Idris elhelyez egy lyukat (amelyet majd "fel kell töltenünk" saját bizonyítással), és átugorja a problémát. A lyukaknál adódó bizonyítandó állítás belátásához taktikákat használhatunk, melyek előre definiáltak. Pár példa:

Ha azt szeretnénk, hogy az Idris lásson be valamit anélkül, hogy pontos bizonyítást tudnánk adni, vagyis tulajdonképpen fogadja el, hogy az adott állítást egyszerűen el kell hinnie, használhatjuk a believe_me függvényt. Ez nagyon veszélyes is lehet, mindenképpen csak az átgondolt használata javasolt.