Agda

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 (англ.) — диссертация автора языка

Это заготовка статьи о компьютерных языках. Помогите Википедии, дополнив её.

В статье есть список источников, но не хватает сносок.

Без сносок сложно определить, из какого источника взято каждое отдельное утверждение. Вы можете улучшить статью, проставив сноски на источники, подтверждающие информацию. Сведения без сносок могут быть удалены.(10 ноября 2012)