Like most modern functional programming languages, Idris supports a notion of inductively-defined data type and parametric polymorphism.
La fel ca majoritatea limbajelor de programare funcționale moderne, Idris susține o noțiune de tip de date definit inductiv și polimorfism parametric.