Idris é uma linguagem de programação funcional de tipo estático com inferência de tipo e tipos dependentes. Baseia-se na família de linguagens ML e toma emprestado características de Haskell e outras linguagens.
Idris é uma linguagem de uso geral, com foco na segurança de tipo, verificação de programas e desempenho. Tem um sistema de tipo forte e estático com tipos dependentes. Isto permite que os tipos sejam utilizados para expressar invariantes e assegurar que os programas satisfazem determinadas propriedades.
O sistema de tipo é também utilizado para gerar documentação, facilitar a refactoring e melhorar o desempenho.
Idris é de código aberto e está disponível sob a licença do MIT.