Подтвердить что ты не робот

Как узнать agda

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

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

Ответ 1

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

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

Coq'Art - слегка устаревший, но начинающий дружелюбный
Сертифицированное программирование с зависимыми типами

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

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

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

Ответ 2

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