Введение в Agda
Это текстовая версия видео-лекции с нашего канала.
Что такое Agda?
Agda — чистый функциональный язык программирования с зависимыми типами. Теоретической основой для Agda служит интуиционистская теория типов Мартин-Лёфа, которая расширена набором конструкций, полезных для практического программирования.
Почему Agda?
Функциональный язык с зависимыми типами
Agda является одним из самых продвинутых функциональных языков программирования и не смотря на то, что на данный момент языки подобные Agda используются скорее в исследовательских и образовательных целях я думаю будет полезно разобраться как работать с зависимыми типами т.к. я убеждён, что в будущем они станут такой же обыденностью как и функциональный подход к работе с коллекциями. Уже сейчас всё больше практически ориентированных языков программирования позволяют использовать зависимые типы, есть Idris, в каком-то виде они реализованы в Haskell, а с помощью специальных библиотек их можно использовать и в Scala.
Является системой автоматического доказательства
На Agda можно формализовать очень много конструкций из математики и доказать множество теорем.
Вместе с Coq является языком формализации HoTT
Гомотопическая теория типов достаточно перспективная, интересная и активно развивающаяся область математики в которой как мне кажется есть чем заняться обычным программистам. С помощью гомотопической теории типов строятся унивалентные основания математики – универсальный формальный язык являющийся конструктивными основаниями для современных разделов математики и обеспечивающий возможность автоматической проверки правильности доказательств на компьютере.
Установка
Если у вас уже стоит Stack, то установить Agda можно командой
stack install Agda
Иначе установите сначала Stack
Настройка
Для написания программ рекомендуется использовать либо Emacs, либо Atom. Я остановлюсь на последнем. Для удобной работы нужно поставить плагины agda-mode и language-agda, сделать это можно командами
apm install language-agda
apm install agda-mode
Hello, World!
Обычно когда рассказывают про какой-то язык программирования в качестве первого примера приводят программу выводящую в консоль Hello, World!, но Agda не совсем обычный язык программирования и IO там используют редко, поэтому поговорим мы о нём как-нибудь в другой раз. Вместо этого мы определим тип булеан и реализуем несколько операций над ним.
Agda не загружает автоматически стандартную библиотеку. Поэтому мы можем начать с нуля и не бояться коллизий.
Для начала создадим файл Bool.agda и создадим в нём модуль
(в отличии от Haskell указание модуля обязательно)
Определение булевого типа на Agda будет выглядеть так:
В определении типа булеан у нас указано 𝔹 : Set
, что в точности означает 𝔹 имеет тип Set.
Т.к. Agda является языком с зависимыми типами она не различает термы и типы, поэтому у каждого типа есть тип. Большинство базовых типов имеют тип Set т.е. множество.
Для того, чтобы избежать парадокса Рассела, который возникает если разрешить множествам содержать в себе множества, тип Set имеет тип не Set, а Set₁, который в свою очередь имеет тип Set₂ и т.д. Бесконечная иерархия типов позволяет избежать ситуации в которой в типе содержится он сам.
Теперь можем определить условный оператор if
. Agda поддерживает так называемую миксфиксную запись, например, можно определить if_then_else_
, который далее можно вызвать и как if a then b else c
и if_then_else_ a b c
.
Сигнатура будет следующая:
в фигурных скобках указываются так называемые неявные параметры, т.е. параметры, которые при вызове не нужно будет явно указывать, компилятор Agda сам поймёт, что нужно подставить.
вместе с реализацией:
Так же можем определить операцию коньюнкции
и дизьюнкции
и отрицания
Думаю теперь пришло время что-нибудь наконец доказать, например, законы Де Моргана. Для этого нам нужно будет ввести тип равенства:
Фактически это означает, что для любого типа A
и любого терма a
этого типа справедливо, что a ≡ a
и таким образом refl
является доказательством по определению.
Теперь можно сформулировать законы Де Морогана
На самом деле булеан достаточно простой тип и доказать множество вещей можно просто разбором случаев:
DeMorgan-law₁ : (a b : 𝔹) → ¬ (a ∧ b) ≡ ¬ a ∨ ¬ b
DeMorgan-law₁ false b = refl
DeMorgan-law₁ true b = refl
DeMorgan-law₂ : (a b : 𝔹) → ¬ (a ∨ b) ≡ ¬ a ∧ ¬ b
DeMorgan-law₂ true b = refl
DeMorgan-law₂ false b = refl
В данной ситуации, перебора значений первого аргумента будет достаточно. Если зафиксировать в качестве первого аргумент значение true, то левая и правая часть равенства будут равны просто по определению, такая же ситуация будет и если зафиксировать false
но важно заметить, что доказательства достаточно сильно зависят от определений, например, если мы определим коньюнкцию иначе:
то наши доказательства работать уже не будет, т.к. компилятор не найдёт подходящих паттернов в нашем определении.
тут так же важно понимать, что “не равно” в данном случае не означает, что левая и правая части выражения различаются, это означает лишь то, что у компилятора нет оснований считать, что левая и правая часть одинаковы, мы можем предоставить компилятору доказательство, что это одно и то же, и тогда он с радостью скомпилирует наш код.