Строго типизированный функциональный язык программирования с зависимыми типами и синтаксисом Haskell. Интересен тем, что типы помогают генерировать дальнейший код для описания содержимого функции.

Книги:

• Little Typer

Видео:

• https://youtube.com/watch?v=VxINoKFm-S4
• Brady - Idris 2 - Type-driven Development of Idris
• Лекции по Idris от Брагилевского в ВШЭ