Существует учебник Idris, учебник Agda и многие другие документы в стиле учебника и вводные материалы с бесконечными ссылками на вещи, которые еще предстоит изучить. Я как бы ползаю посреди всего этого и большую часть времени застреваю в математических обозначениях и новой терминологии, появляющейся внезапно без объяснения причин. Может у меня математика хромает :-)
Есть ли какой-нибудь дисциплинированный подход к программированию зависимых типов? Например, когда вы хотите изучить Haskell, вы начинаете с «Научите себя Haskell», когда вы хотите изучить Scala, вы начинаете с книги Одерски, для Ruby вы читаете этот странный учебник с мутировавшими ошибками в нем. Но я не могу начать Агду или Идрис с их книгами. Они намного выше моей головы. Я попробовал Coq и застрял в его универсальном стиле проверки работоспособности. Агда требует огромной математической подготовки, а Идрис, ну, давайте пока оставим это!
Я очень хорошо разбираюсь в системах статического типа, неплохо разбираюсь в Scala и при необходимости могу использовать Haskell. Я понимаю функциональную парадигму и использую ее изо дня в день, я понимаю алгебраические типы данных и GADT (на самом деле довольно гладко), и недавно мне удалось понять лямбда-куб. Но мне не хватает математики и логики.
