Здравствуйте, Marty, Вы писали:

M>А что это?

На сайте ПОМИ РАН можно посмотреть лекции на тему «Программирование с зависимыми типами на языке Idris»: http://compsciclub.ru/courses/idrisprogramming/2017-spring/?tab=classes