Для тех кто из-за карантина уже научил кота плясать, построил 3хэтажный карточный домик с террасой и сделал всякие другие нужные и полезные вещи вот тут вот в открытом доступе лежит книга type driven development with Idris.
Почему стоит почитать:
1. Это, наверное, первый "мейнстримовый"(неакадимический) язык с зависимыми типами
2. Idris -- реально странный! Там типы как first class citizen(можно передавать в функцию, возвращать и т.д.). Все функции тотальные и нет исключений.
3. А еще(имхо, самое важное) автор уверяет, что книжка-то не про идрис, а про программирование через типы. Т.е. про то как подружиться с компилятором на столько, что бы он помогал писать код, а не просто орал в конце "rejected!!1". Собственно ради этого люди и идут в функциональщину