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 и реализована.
Примеры
[править | править код]Натуральные числа и их сложение
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 (англ.) — диссертация автора языка
 | Это заготовка статьи о компьютерных языках. Помогите Википедии, дополнив её. |
 | Для улучшения этой статьи по информационным технологиям желательно:
|
