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



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

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

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

18 числа вышло обновление версии языка (текущая версия - 2.5.1), вот некоторые изменения:
Некоторые изменения:

• представлена официальная пользовательская документация;
• с помощью прагмы HASKELL можно добавлять к модулю произвольный код на Haskell;
• многочисленные изменения в области метапрограммирования и рефлексии;
• исправлены некоторые ошибки в бекэндах:
  • теперь нет необходимости указывать {-# COMPILED_DATA #-} для встроенных типов Bool, Int, Float и других;
  • клозы функций с разной арностью компилируются корректно;
  • поддержка co-patterns в бекэндах GHC/UHC;
• поддержка Utrecht Haskell Compiler (UHC) в качестве бекэнда.

 Оригинал новости