Bővíthető szintaxis
Az Idris többféleképpen is segíti a beágyazott, domain specifikus nyelvek implementálását (EDSL), például a bővíthető szintaxissal. Szabályok megadásával új szintaktikai elemek definiálhatók. Egy nagyon jó példa a szintaxisbővítésre az if...then...else... vezérlési szerkezet, amely nincs a nyelvbe előre beégetve. Definíciója:
syntax "if" [test] "then" [t] "else" [e] = boolCase test t e;
Az idézőjeles szavak az új kulcsszavakat adják meg, míg a szögletes zárójelben az egyenlőség jobb oldalán felhasználható kifejezések vannak. Az egyenlőség jobb oldala egy függvény, amely leírja a szintaktikus bővítmény szemantikáját.
Dsl-jelölés
A dsl-jelölés a beágyazott nyelvek leírását segíti. Megadható egy szintaxis-túlterhelés, mely egy megfeleltetést ad az Idris nyelvi elemei és a dsl elemek reprezentációja között. Példa:
dsl dsl_name
lambda = Lam
variable = Var
index_first = stop
index_next = pop
A stop és a pop a Bruijn index felépítéséhez kellenek.
Egyéb
Az Idris az előzőek mellett az alábbiakat is tartalmazza:
- Foreign function interface - interfész külső, például C függvények meghívásához
- Idris-Javascript fordító - Idris kódból készít Javascriptet
- Type providers - az F#-hoz hasonló "típus kiszolgálók"
- Literális programozás