Как выучить agda
пытаюсь выучить agda. Однако у меня возникла проблема. Все руководства, которые я нашел на вики-сайте agda, слишком сложны для меня и охватывают различные аспекты программирования. После параллельного чтения 3 руководств по agda я смог написать простые доказательства, но у меня все еще недостаточно знаний, чтобы использовать их для проверки правильности алгоритма реального слова.
Вы можете порекомендовать мне какие-нибудь уроки по этой теме? Что-то похожее на Learn Yourself a Haskell, но для Agda.
1 ответ
Когда я начал изучать Агду около года назад, я думал, что перепробовал все доступные учебники, и каждый научил меня чему-то новому.
Вы, вероятно, должны попробовать Coq, потому что у него большая база пользователей и для него доступны две хорошие книги:
- Coq'Art - Немного устаревший, но удобный для начинающих
- Сертифицированное программирование с зависимыми типами
Основы программного обеспечения также очень приятно.
Приятно то, что теории, на которых основаны Agda и Coq, несколько похожи, поэтому многие примеры можно перевести с одного на другое. Программирование в Теории типов Мартина-Лёфа - это действительно хорошее и читаемое введение в теорию зависимых типов, оно может кое-что прояснить для вас.
Было бы полезно узнать, что вы подразумеваете под «алгоритмами реального мира». Многие примеры развития описаны в работах , в которых упоминается Агда .