Dnes byla vydána verze 0.6.0 jazyka Idris 2. Přináší drobná rozšíření standardní knihovny, režimu REPL a odstraňuje bugy. Na rozdíl od jiných jazyků se závislostními typy (např. Agda, Coq a Lean) je Idris určen v první řadě pro psaní aplikací, nikoliv formalizaci matematických důkazů. Je čistě funkcionální a syntakticky vychází z Haskellu.
V jazycích se závislostním typovým systémem jsou typy tzv. „first-class citizens“, ovšem při plném zachování statické typové kontroly v době překladu. Je také možné používat typové parametry, jejichž hodnota není známa v době překladu, například instanci typu Vector n a (pole prvků typu a velikosti n) lze vytvořit až za běhu, přičemž n může přijít například ze vstupu od uživatele. Plně jsou také podporovány zobecněné algebraické datové typy a typový systém je kvantitavní, což znamená, že každý typ má pevně danou multiplicitu, takže lze například spravovat paměť pomocí lineárních typů a vyhnout se tak GC (podobně jako v jazyce Mercury).
Jazyk nabízí několik tzv. backendů, zdrojový kód lze překládat do různých verzí Scheme (Chez, Racket, Gambit), C (s počítáním referencí), JS apod. Poskytuje také jednoduchý způsob volání funkcí v dynamických knihovnách (FFI). Nefunkcionální kód lze provádět v monádě IO. Pro vyzkoušení je možné využít online hřiště.
