Существует учебник Идриса, учебник по Агде и многие другие статьи в стиле учебника и вводный материал с бесконечными ссылками на вещи, которые еще предстоит изучить. Я как бы ползаю среди всех этих, и большую часть времени я застрял с математическими обозначениями и новой терминологией, появляющейся внезапно без объяснения причин. Возможно, моя математика сосет: -)
Есть ли какой-либо дисциплинированный способ подхода к программированию зависимого типа? Например, когда вы хотите изучить Haskell, вы начинаете с "Учить себя Haskell", когда вы хотите изучить Scala, вы начинаете с книги Odersky, для Ruby вы читаете этот странный учебник с мутированными ошибками в нем. Но я не могу начать с Агды или Идриса своими книгами. Они намного выше моей головы. Я попробовал Coq и застрял в стиле "все-о-тере". Агда требует огромного математического фона и Идриса, ну, оставь это сейчас!
Я очень хорошо понимаю системы статического типа, я хорошо разбираюсь в Scala, и при необходимости я могу использовать Haskell. Я понимаю Функциональную Парадигму и использую ее изо дня в день, я понимаю Алгебраические Типы Данных и GADT (довольно гладко на самом деле), и мне недавно удалось понять Lambda Cube. Однако мне не хватает математики и логики.
