Agda

Agda
Agda
Класс языка	функциональный, доказыватель теорем
Появился в	2007 (1.0 в 1999)
Автор	Ульф Норелл
Разработчик	Чалмерский технологический институт
Расширение файлов	.agda или .lagda
Выпуск	2.6.2.2 (2 апреля 2022)
Система типов	статическая, строгая, зависимая
Испытал влияние	Haskell, Coq, Epigram
Повлиял на	Idris
Лицензия	BSD
Сайт	wiki.portal.chalmers.se/…
ОС	Windows и Unix-подобная операционная система

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

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

Agda поддерживает индуктивные типы данных, сопоставление с образцом (гибко использующее наличие зависимых типов), систему параметризованных модулей, проверку завершаемости программ^[англ.], миксфиксный синтаксис для операторов. Поддержка неявных аргументов приводит к существенному упрощению программирования с зависимыми типами. Для программ на Agda характерно широкое использование Юникода.

В стандартную реализацию Agda входит расширение редактора Emacs, позволяющее осуществлять пошаговое построение программ. Система проверки типов языка дает программисту полезную информацию о ещё не написанных частях программы.

Конкретный синтаксис языка Agda весьма близок к синтаксису Haskell, на котором система Agda и реализована.