Kivételkezelés
Az Idris nyelvben nem található az imperatív nyelvekhez hasonló try...catch szerkezet a kivételkezelésre, viszont megemlítendő a Maybe típus, amely a kivételes esetek kezelésére való. Segítségével valamely parciális f függvényt totálissá tehetünk úgy, hogy azon helyeken, ahol f eddig értelmezve volt, és x értékkel tért vissza, Just x visszatérést adunk, ahol pedig f nem volt értelmezve, ott az eredmény Nothing lesz. A Maybe típus definíciója:
data Maybe a = Just a | Nothing