Agda (язык программирования) - Agda (programming language)

Агда
Стилизованный цыпленок в черных линиях и точках слева от имени «Agda» без засечек, первая буква наклонена вправо.
Парадигма Функциональный
Разработано Ульф Норелл; Катарина Кокванд (1.0)
Разработчик Ульф Норелл; Катарина Кокванд (1.0)
Впервые появился 2007 ; 14 лет назад (1,0 в 1999 г . ; 22 года назад ) ( 2007 ) ( 1999 )
Стабильный выпуск
2.6.2 / 19 июня 2021 г . ; 2 месяца назад ( 2021-06-19 )
Печатная дисциплина сильный , статический , зависимый , номинальный , явный , предполагаемый
Язык реализации Haskell
Операционные системы Кроссплатформенность
Лицензия BSD-подобный
Расширения имени файла .agda, .lagda, .lagda.md, .lagda.rst,.lagda.tex
Веб-сайт wiki .portal .chalmers .se / agda
Под влиянием
Coq , эпиграмма , Haskell
Под влиянием
Идрис

Agda - это функциональный язык программирования с зависимой типизацией, первоначально разработанный Ульфом Нореллом из Технологического университета Чалмерса, реализация которого описана в его докторской диссертации. Первоначальная система Agda была разработана в Чалмерсе Катариной Кокванд в 1999 году. Текущая версия, первоначально известная как Agda 2, представляет собой полностью переработанную версию, которую следует рассматривать как новый язык, имеющий общее имя и традиции.

Agda также является помощником по проверке, основанным на парадигме предложений как типов , но, в отличие от Coq , не имеет отдельного языка тактик , а доказательства написаны в стиле функционального программирования. В языке есть обычные программные конструкции, такие как типы данных , сопоставление с образцом , записи , let-выражения и модули, а также синтаксис, подобный Haskell . Система имеет интерфейсы Emacs и Atom, но также может запускаться в пакетном режиме из командной строки.

Agda основана на единой теории зависимых типов (UTT) Чжаохуэй Луо, теории типов , подобной теории типов Мартина-Лёфа .

Агда названа в честь шведской песни «Hönan Agda», написанной Корнелисом Фрисвейком , о курице по имени Агда. Это намекает на название Coq .

Функции

Индуктивные типы

Основной способ определения типов данных в Agda - это индуктивные типы данных, которые похожи на алгебраические типы данных в языках программирования с независимой типизацией.

Вот определение чисел Пеано в Агде: 

 data ℕ : Set where
   zero : ℕ
   suc : ℕ → ℕ

По сути, это означает, что есть два способа создать значение типа ℕ, представляющее натуральное число. Для начала, zeroэто натуральное число, и если nэто натуральное число, то suc n, стоя на преемнику из n, является натуральным числом тоже.

Вот определение отношения «меньше или равно» между двумя натуральными числами: 

 data _≤_ : ℕ → ℕ → Set where
   z≤n : {n : ℕ} → zero ≤ n
   s≤s : {n m : ℕ} → n ≤ m → suc n ≤ suc m

Первый конструктор z≤nсоответствует аксиоме, согласно которой ноль меньше любого натурального числа или равен ему. Второй конструктор s≤sсоответствует правилу вывода, позволяющему превратить доказательство n ≤ mв доказательство suc n ≤ suc m. Таким образом, значение s≤s {zero} {suc zero} (z≤n {suc zero})является доказательством того, что единица (преемник нуля) меньше или равна двум (преемник единицы). Параметры, указанные в фигурных скобках, могут быть опущены, если они предполагаются.

Зависимо типизированное сопоставление с образцом

В теории основных типов принципы индукции и рекурсии используются для доказательства теорем об индуктивных типах . В Agda вместо этого используется сопоставление шаблонов с зависимым типом. Например, сложение натуральных чисел можно определить так: 

 add zero n = n
 add (suc m) n = suc (add m n)

Такой способ написания рекурсивных функций / индуктивных доказательств более естественен, чем применение принципов простой индукции. В Agda сопоставление с образцом с зависимым типом является примитивом языка; в базовом языке отсутствуют принципы индукции / рекурсии, на которые переводится сопоставление с образцом.

Метапеременные

Одной из отличительных особенностей Agda по сравнению с другими подобными системами, такими как Coq , является сильная зависимость от метапеременных при построении программ. Например, в Agda можно написать такие функции: 

 add : ℕ → ℕ → ℕ
 add x y = ?

?вот метапеременная. При взаимодействии с системой в режиме emacs он покажет ожидаемый тип пользователя и позволит ему уточнить метапеременную, то есть заменить ее более подробным кодом. Эта функция позволяет создавать инкрементные программы аналогично тактическим помощникам по доказательствам, таким как Coq.

Доказательство автоматизации

Программирование в чистой теории типов требует множества утомительных и повторяющихся доказательств. Хотя в Agda нет отдельного языка тактик, можно запрограммировать полезные тактики внутри самой Agda. Обычно это работает путем написания функции Agda, которая, возможно, возвращает доказательство некоторого интересующего свойства. Затем тактика создается путем запуска этой функции во время проверки типов, например, с использованием следующих вспомогательных определений: 

  data Maybe (A : Set) : Set where
    Just : A → Maybe A
    Nothing : Maybe A

  data isJust {A : Set} : Maybe A → Set where
    auto : ∀ {x} → isJust (Just x)

  Tactic : ∀ {A : Set} (x : Maybe A) → isJust x → A
  Tactic Nothing ()
  Tactic (Just x) auto = x

Учитывая функцию, check-even : (n : ℕ) → Maybe (Even n)которая вводит число и, при необходимости, возвращает доказательство его четности, тактика может быть построена следующим образом: 

  check-even-tactic : {n : ℕ} → isJust (check-even n) → Even n
  check-even-tactic {n} = Tactic (check-even n)

  lemma0 : Even zero
  lemma0 = check-even-tactic auto

  lemma2 : Even (suc (suc zero))
  lemma2 = check-even-tactic auto

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

Кроме того, для написания более сложных тактик Agda поддерживает автоматизацию через отражение . Механизм отражения позволяет заключать фрагменты программы в кавычки или извлекать их из абстрактного синтаксического дерева. Способ использования отражения аналогичен тому, как работает Template Haskell.

Другой механизм автоматизации проверки - это действие поиска доказательства в режиме emacs. Он перечисляет возможные условия подтверждения (ограниченный 5 секундами), и, если один из терминов соответствует спецификации, он будет помещен в мета-переменную, в которой вызывается действие. Это действие принимает подсказки, например, какие теоремы и из каких модулей можно использовать, может ли действие использовать сопоставление с образцом и т. Д.

Проверка прекращения

Agda - это тотальный язык , то есть каждая программа в нем должна завершаться, и все возможные шаблоны должны быть сопоставлены. Без этой функции логика языка становится непоследовательной, и становится возможным доказывать произвольные утверждения. Для проверки прерывания Agda использует метод проверки прерывания плодов.

Стандартная библиотека

Agda имеет обширную стандартную библиотеку де-факто, которая включает множество полезных определений и теорем об основных структурах данных, таких как натуральные числа, списки и векторы. Библиотека находится в стадии бета-тестирования и находится в стадии активной разработки.

Юникод

Одна из наиболее заметных особенностей Agda - это сильная зависимость от Unicode в исходном коде программы. Стандартный режим emacs использует ярлыки для ввода, например, \Sigmaдля Σ.

Бэкэнды

Есть два бэкэнда компилятора, MAlonzo для Haskell и один для JavaScript .

Смотрите также

использованная литература

внешние ссылки