WikiSort.ru - Программирование

ПОИСК ПО САЙТУ | о проекте
Agda
Класс языка функциональный, доказыватель теорем[en]
Появился в 2007
Автор Ульф Норелл
Расширение файлов .agda или .lagda
Выпуск
Система типов статическая, строгая, зависимая
Испытал влияние Haskell, Coq, Epigram (англ.)
Лицензия BSD
ОС кроссплатформенность
Сайт wiki.portal.chalmers.se/…

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

Примечания

Ссылки

Данная страница на сайте WikiSort.ru содержит текст со страницы сайта "Википедия".

Если Вы хотите её отредактировать, то можете сделать это на странице редактирования в Википедии.

Если сделанные Вами правки не будут кем-нибудь удалены, то через несколько дней они появятся на сайте WikiSort.ru .




Текст в блоке "Читать" взят с сайта "Википедия" и доступен по лицензии Creative Commons Attribution-ShareAlike; в отдельных случаях могут действовать дополнительные условия.

Другой контент может иметь иную лицензию. Перед использованием материалов сайта WikiSort.ru внимательно изучите правила лицензирования конкретных элементов наполнения сайта.

2019-2024
WikiSort.ru - проект по пересортировке и дополнению контента Википедии