Как выучить агду

Question

Я пытаюсь выучить агду.Однако у меня возникла проблема.Все учебники, которые я нашел в agda wiki, слишком сложны для меня и охватывают различные аспекты программирования.После параллельного чтения 3 учебных пособий по agda я смог написать простые доказательства, но у меня все еще не хватает знаний, чтобы использовать их для правильности алгоритма реального слова.

Можете ли вы порекомендовать мне какие-либо учебные пособия по этой теме?Нечто похожее на Learn Yourself a Haskell, но для Agda.

Answer 1

Когда я начал изучать Агду около года назад, я думал, что перепробовал все доступные учебники, и каждый научил меня чему-то новому.

Вам, вероятно, стоит попробовать Coq, потому что у него большая база пользователей и для него доступны две хорошие книги:

1. Coq'Art -Немного устаревший, но удобный для начинающих
2. Сертифицированное программирование с зависимыми типами

Основы программного обеспечения тоже очень приятно.

Приятно то, что теории, на которых основаны Agda и Coq, несколько похожи, поэтому многие примеры можно перевести с одного на другой. Программирование в теории типов Мартина-Лёфа - это действительно хорошее и читаемое введение в теорию зависимых типов, оно может кое-что прояснить для вас.

Это поможет понять, что вы подразумеваете под"алгоритмы реального мира".Многие примеры развития описаны в статьях, в которых упоминается Agda .

.

Answer 2

Конор МакБрайд прочитал большую серию лекций в прошлом году о программировании с зависимым типом с использованием AgdaЭто хорошее место, если вы хотите отдохнуть от кратких уроков по этой теме.Я считаю, что есть и сопутствующие упражнения.