Agda

Перейти к навигацииПерейти к поиску
Agda
Изображение логотипа
Класс языкафункциональный, доказыватель теорем
Появился в2007; 17 лет назад (2007) (1.0 в 1999; 25 лет назад (1999))
АвторУльф Норелл
Расширение файлов.agda или .lagda
Выпуск2.6.2.2 (2 апреля 2022; 2 года назад (2022-04-02))
Система типовстатическая, строгая, зависимая
Испытал влияние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

Ссылки