Агда (язык программирования)

приглашенный
Парадигма	Функциональный
Разработано	Ульф Норелл; Катарина Коканд (1.0)
Разработчик	Ульф Норелл; Катарина Коканд (1.0)
Впервые появился	2007 г .; 17 лет назад ( 1.0 в 1999 ; 25 лет назад )
Стабильная версия	2.6.3 / 30 января 2023 г .; 16 месяцев назад
Дисциплина набора текста	сильный , статический , зависимый , номинальный , явный , предполагаемый
Язык реализации	Хаскелл
ТЫ	Кросс-платформенный
Лицензия	BSD-подобный
Расширения имен файлов	.agda, .lagda, .lagda.md, .lagda.rst, .lagda.tex
Веб-сайт	неделя .портал .Чалмерс .se / приглашать
Под влиянием
	Кок , Эпиграмма , Haskell
Под влиянием
	Идрис

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

Agda также является помощником по доказательству, основанным на парадигме предложений как типов , но в отличие от Coq не имеет отдельного языка тактики , а доказательства написаны в стиле функционального программирования. В языке имеются обычные программные конструкции, такие как типы данных , сопоставление с образцом , записи , выражения let и модули, а также Haskell синтаксис, подобный . Система имеет Emacs , Atom и VS Code. интерфейсы ^[4]^[5]^[6] но также может быть запущен в пакетном режиме из командной строки.

Агда основана на единой теории зависимых типов (UTT) Чжаохуэй Луо. ^[7] теория типов, подобная теории типов Мартина-Лёфа .

Агда названа в честь шведской песни «Hönan Agda», написанной Корнелисом Врисвейком . ^[8] речь идет о курице по имени Агда. Это отсылка к имени человека, доказывающего теоремы Coq , который был назван в честь Тьерри Коканда .

Особенности [ править ]

Индуктивные типы [ править ]

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

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

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

По сути, это означает, что существует два способа создания значения типа $\mathbb {N}$ , представляющий натуральное число. Для начала 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. ^[9] Таким образом, значение 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 : $\mathbb {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. ^[10]

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

Проверка завершения [ править ]

Agda — тотальный язык , т. е. каждая программа в нем должна завершиться и сопоставить все возможные шаблоны. Без этой функции логика языка становится противоречивой, и становится возможным доказывать произвольные утверждения. Для проверки завершения Agda использует подход проверки завершения Fetus. ^[12]

Стандартная библиотека [ править ]

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

Юникод [ править ]

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

Бэкэнды [ править ]

Существует два бэкэнда компилятора: MAlonzo для Haskell и один для JavaScript .

См. также [ править ]

Список помощников по проверке

Ссылки [ править ]

^ Файл лицензии Agda
^ Ульф Норелл. К практическому языку программирования, основанному на теории зависимых типов. Кандидатская диссертация. Технологический университет Чалмерса, 2007 г. [1]
^ «Агда: интерактивный редактор корректуры» . Архивировано из оригинала 8 октября 2011 г. Проверено 20 октября 2014 г.
^ Коканд, Катарина; Синек, Дэн; Такэяма, Макото. Интерфейс Emacs для типизированной поддержки построения доказательств и программ (PDF) . Европейские совместные конференции по теории и практике программного обеспечения, 2005 г. Архивировано из оригинала (PDF) 22 июля 2011 г.
^ «agda-режим на Atom» . Проверено 7 апреля 2017 г.
^ «agda-mode — Visual Studio Marketplace» . marketplace.visualstudio.com . Проверено 6 июня 2023 г.
^ Ло, Чжаохуэй. Вычисления и рассуждения: теория типов для информатики . Oxford University Press, Inc., 1994.
^ «[Агда] происхождение слова «Агда»? (список рассылки Агда)» . Проверено 24 октября 2020 г.
^ «Нат из стандартной библиотеки Агда» . Гитхаб . Проверено 20 июля 2014 г.
^ Ван дер Уолт, Пол и Воутер Свирстра. «Инженерное доказательство путем отражения в Агде». В «Реализации и применении функциональных языков» , стр. 157-173. Springer Berlin Heidelberg, 2013. [2]
^ Кокке, Пепейн и Воутер Свирстра. «Машина в Агде».
^ Абель, Андреас. «foetus – средство проверки завершения для простых функциональных программ». Отчет лаборатории программирования 474 (1998). [3]

Дальнейшее чтение [ править ]

Бове, Ана; Дюбьер, Питер; Норелл, Ульф (н. д.). «Краткий обзор Agda — функционального языка с зависимыми типами» (PDF) .
Норелл, Ульф; Чепмен, Джеймс (nd). «Зависимо типизированное программирование в Agda» (PDF) .

Внешние ссылки [ править ]

Официальный сайт
Знакомство с Agda — плейлистом YouTube из пяти частей, созданным Дэниелом Пиблсом.
Брутальное [мета] введение в зависимые типы в Agda
Учебное пособие по Agda: «Изучите программирование в Agda без теоретической подготовки»
Летняя школа HoTTEST 2022 , 66 лекций по теории гомотопических типов, включая ряд вводных лекций и упражнений по Agda

[1] Файл лицензии Agda

[2] Ульф Норелл. К практическому языку программирования, основанному на теории зависимых типов. Кандидатская диссертация. Технологический университет Чалмерса, 2007 г. [1]

[3] «Агда: интерактивный редактор корректуры» . Архивировано из оригинала 8 октября 2011 г. Проверено 20 октября 2014 г.

[emacs-mode-4] Коканд, Катарина; Синек, Дэн; Такэяма, Макото. Интерфейс Emacs для типизированной поддержки построения доказательств и программ (PDF) . Европейские совместные конференции по теории и практике программного обеспечения, 2005 г. Архивировано из оригинала (PDF) 22 июля 2011 г.

[5] «agda-режим на Atom» . Проверено 7 апреля 2017 г.

[6] «agda-mode — Visual Studio Marketplace» . marketplace.visualstudio.com . Проверено 6 июня 2023 г.

[7] Ло, Чжаохуэй. Вычисления и рассуждения: теория типов для информатики . Oxford University Press, Inc., 1994.

[8] «[Агда] происхождение слова «Агда»? (список рассылки Агда)» . Проверено 24 октября 2020 г.

[9] «Нат из стандартной библиотеки Агда» . Гитхаб . Проверено 20 июля 2014 г.

[10] Ван дер Уолт, Пол и Воутер Свирстра. «Инженерное доказательство путем отражения в Агде». В «Реализации и применении функциональных языков» , стр. 157-173. Springer Berlin Heidelberg, 2013. [2]

[11] Кокке, Пепейн и Воутер Свирстра. «Машина в Агде».

[12] Абель, Андреас. «foetus – средство проверки завершения для простых функциональных программ». Отчет лаборатории программирования 474 (1998). [3]

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]

[11]

[12]

v т и Технологический университет Чалмерса
Academics	Johanneberg Science Park Lindholmen University College School of Entrepreneurship
Organizations	Ballong Corps Engineering Trainee Appointment Committee Naval Architecture Students' Society Students' Union
Projects	Agda DVD Player EcoProIT FEniCS Project Humanoid Project IT++ Lazy ML
Joint ventures	Bioscience Business School Center for Intellectual Property Studies IT University Lindholmen Science Park Viktoria Institute
Related	William Chalmers Cortège