Введение в 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 и создадим в нём модуль

module Bool where

(в отличии от Haskell указание модуля обязательно)

Определение булевого типа на Agda будет выглядеть так:

data 𝔹 : Set where --𝔹 пишется с помощью \bB
    true : Bool
    false : Bool

В определении типа булеан у нас указано 𝔹 : 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.

Сигнатура будет следующая:

--→ пишется через \to
if_then_else_ : {A : Set} → 𝔹 → A → A → A

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

вместе с реализацией:

if_then_else_ : {A : Set} → 𝔹 → A → A → A
if true then a else b = a
if false then a else b = b

Так же можем определить операцию коньюнкции

infixr 30 _∧_ --\and

_∧_ : 𝔹 → 𝔹 → 𝔹
true ∧ b = b
_ ∧ _ = false

и дизьюнкции

infixr 20 _∨_ --\or

_∨_ : 𝔹 → 𝔹 → 𝔹
false ∨ b = b
_ ∨ _ = true

и отрицания

infix 40 ¬_ --\neg

¬_ : 𝔹 → 𝔹
¬ true = false
¬ false = true

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

infix 4 _≡_

data _≡_ {A : Set} : A → A → Set where
  refl : { a : A } → a ≡ a

Фактически это означает, что для любого типа A и любого терма a этого типа справедливо, что a ≡ a и таким образом refl является доказательством по определению.

Теперь можно сформулировать законы Де Морогана

DeMorgan-law₁ : (a b : 𝔹) → ¬ (a ∧ b) ≡ ¬ a ∨ ¬ b

DeMorgan-law₂ : (a b : 𝔹) → ¬ (a ∨ b) ≡ ¬ a ∧ ¬ b

На самом деле булеан достаточно простой тип и доказать множество вещей можно просто разбором случаев:

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

¬ (true ∧ b) ≡ ¬ true ∨ ¬ b => ¬ (b) ≡ false ∨ ¬ b => ¬ b ≡ ¬ b

но важно заметить, что доказательства достаточно сильно зависят от определений, например, если мы определим коньюнкцию иначе:

_∧_ : 𝔹 → 𝔹 → 𝔹
true ∧ true = true
_ ∧ _ = false

то наши доказательства работать уже не будет, т.к. компилятор не найдёт подходящих паттернов в нашем определении.

true ∧ b != b of type 𝔹

тут так же важно понимать, что “не равно” в данном случае не означает, что левая и правая части выражения различаются, это означает лишь то, что у компилятора нет оснований считать, что левая и правая часть одинаковы, мы можем предоставить компилятору доказательство, что это одно и то же, и тогда он с радостью скомпилирует наш код.