Agda is too mainstream!

Материалов о языке Idris на русском практически нет, попробую это исправить кратким обзором. Также постараюсь сделать текст понятным для начинающих, не-функциональных и незнакомых с зависимыми типами программистов, и потому тем, кто знаком с подобными языками, может быть проще отмотать в конец или сразу прочесть официальную документацию. Писать серьёзное введение в язык и теорию не берусь, но надеюсь показать, о чём это вообще.

Итак, Idris — чистый функциональный язык программирования общего назначения с зависимыми типами.