Agda

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

Примеры

Натуральные числа и их сложение \textttdata Nat : Set where\\ \texttt  zero : Nat\\ \texttt  suc  : Nat -\textgreater Nat \texttt\_+\_ : Nat -\textgreater Nat -\textgreater Nat\\ \textttzero  + m = m\\ \textttsuc n + m = suc (n + m) Пример зависимого типа: список, в типе которого хранится натуральное число — его длина \textttdata Vec (A : Set) : Nat -\textgreater Set where\\ \texttt  []   : Vec A zero\\ \texttt  \_::\_ : \{n : Nat\} -\textgreater A -\textgreater Vec A n -\textgreater Vec A (suc n) Безопасная функция вычисления головы списка, не позволяющая выполнять эту операцию над пустым списком (нулевой длины): \texttthead : \{A : Set\}\{n : Nat\} -\textgreater Vec A (suc n) -\textgreater A\\ \texttthead (x :: xs) = x