Byla vydána verze 0.5.0 jazyka Idris 2. Z větších změn lze zmínit přidání inkrementálního překladu a zrychlení typové kontroly omezením redukcí v době překladu.
Idris je funkcionální jazyk s velmi silným typovým systémem včetně závislostních typů. Syntaxí se podobá Haskellu, implementace je ale bližší Agdě. Idris 2 je kompletním přepisem původní experimentální implementace.
