Agda

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

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

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

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

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

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

Примеры

Натуральные числа и их сложение

data Nat : Set where
  zero : Nat
  suc  : Nat -> Nat

_+_ : Nat -> Nat -> Nat
zero  + m = m
suc n + m = suc (n + m)

Пример зависимого типа: список, в типе которого хранится натуральное число — его длина

data Vec (A : Set) : Nat -> Set where
  []   : Vec A zero
  _::_ : {n : Nat} -> A -> Vec A n -> Vec A (suc n)

Безопасная функция вычисления головы списка, не позволяющая выполнять эту операцию над пустым списком (нулевой длины):

head : {A : Set}{n : Nat} -> Vec A (suc n) -> A
head (x :: xs) = x

Ссылки

• официальный сайт Agda (англ.)
• Dependently Typed Programming in Agda (англ.) — подробное введение в язык
• A Brief Overview of Agda Архивная копия от 12 марта 2013 на Wayback Machine (англ.) — краткий обзор языка
• Ulf Norell. Towards a practical programming language based on dependent type theory. PhD thesis (англ.) — диссертация автора языка