idris é uma linguagem de programação funcional avançada que possui tipos dependentes. Isso significa que os tipos de dados no código estão relacionados entre si e podem ser definidos com base em outros tipos de dados. Isso fornece uma maior segurança e precisão no código, pois os erros são detectados antes da execução. Além disso, a linguagem é fortemente tipada, o que significa que os tipos de dados precisam ser especificados explicitamente no código. Isso também ajuda a detectar erros e torna o código mais fácil de entender. 