С чего начать с программирования зависимого типа?

Существует учебник Идриса, учебник по Агде и многие другие статьи в стиле учебника и вводный материал с бесконечными ссылками на вещи, которые еще предстоит изучить. Я как бы ползаю среди всех этих, и большую часть времени я застрял с математическими обозначениями и новой терминологией, появляющейся внезапно без объяснения причин. Возможно, моя математика сосет: -)

Есть ли какой-либо дисциплинированный способ подхода к программированию зависимого типа? Например, когда вы хотите изучить Haskell, вы начинаете с "Учить себя Haskell", когда вы хотите изучить Scala, вы начинаете с книги Odersky, для Ruby вы читаете этот странный учебник с мутированными ошибками в нем. Но я не могу начать с Агды или Идриса своими книгами. Они намного выше моей головы. Я попробовал Coq и застрял в стиле "все-о-тере". Агда требует огромного математического фона и Идриса, ну, оставь это сейчас!

Я очень хорошо понимаю системы статического типа, я хорошо разбираюсь в Scala, и при необходимости я могу использовать Haskell. Я понимаю Функциональную Парадигму и использую ее изо дня в день, я понимаю Алгебраические Типы Данных и GADT (довольно гладко на самом деле), и мне недавно удалось понять Lambda Cube. Однако мне не хватает математики и логики.

Ответы

Ответ 1

Я очень рекомендую Основы программного обеспечения. Эта книга очень хороша, когда вы представляете вас в Coq один шаг за раз. Да, есть много доказательств теоремы, но эта часть вкуса зависимых типов. Это отличное чувство, когда линия между "программированием" и "проверкой" начинает размываться.

Мне не хватает математической и логической частей.

Я думаю, что Software Foundations делает довольно хорошую работу, чтобы довести вас до скорости для логики, которую вам нужно знать. Тем не менее, уже комфортно с концепцией импликации.

Ответ 2

(Примечание: это самореклама)

Я пишу учебное пособие Agda, и моя главная цель - пусть люди играют с Агда без теоретического фона.

Этот учебник может решить большинство ваших проблем:

• пытается объяснить программирование Agda без внешних ссылок
• требуется только математическая математика средней школы
• пытается преподавать методы программирования.

Он находится в разработке, но первая половина готова.