Agda: типы, зависящие от значений

Agda — функциональный язык программирования и одновременно proof assistant: в нём типы могут зависеть от значений, а программа может нести доказательство своих свойств. Это делает Agda удобной для формализации математики, проверки структур данных и изучения теории типов. Практической «промышленной» разработки на ней мало, зато как инструмент мышления она даёт то, чего не дают обычные языки: компилятор не пропустит случай, который вы не доказали.

Зачем типы, зависящие от значений

В обычном языке тип списка не говорит, сколько в нём элементов. В Agda можно описать вектор — список фиксированной длины, — и тогда функция, которая берёт первый элемент, потребует доказательства, что длина не ноль. Ошибиться в индексе становится невозможно: неверный вызов просто не пройдёт проверку типов.

Основа языка — теория типов Мартина-Лёфа. Утверждение «A верно» записывается как наличие значения типа A, а доказательство — это программа. Такая переписка между логикой и вычислениями называется соответствием Карри — Ховарда и определяет весь стиль работы.

Установка

В Debian и Ubuntu есть готовые пакеты, включая стандартную библиотеку и режим для Emacs. Если нужна свежая версия, используйте cabal или stack — но тогда приготовьтесь собирать зависимости.

sudo apt install agda agda-stdlib elpa-agda2-mode
agda --version
agda-mode setup

После установки настройте стандартную библиотеку. Agda ищет файлы .agda-lib по путям из ~/.agda/libraries, а список подключаемых библиотек по умолчанию берёт из ~/.agda/defaults:

mkdir -p ~/.agda
echo '/usr/share/agda-stdlib/standard-library.agda-lib' >> ~/.agda/libraries
echo 'standard-library' >> ~/.agda/defaults

Путь зависит от дистрибутива и способа установки: найдите файл *.agda-lib в каталоге библиотеки и подставьте его. Проверка простая: импорт Data.Nat должен проходить без ошибок.

Убедиться, что режим Emacs подхватился, можно по строке состояния при открытии файла с расширением .agda: там появится Agda. Если этого не произошло, выполните установку режима ещё раз и перезапустите редактор.

Первая программа

Создайте файл Hello.agda. Модуль должен совпадать с именем файла, иначе компилятор выдаст ошибку. Минимальный пример с натуральными числами и сложением выглядит так:

module Hello where

open import Data.Nat using (ℕ; zero; suc; _+_)
open import Data.Nat.Show using (show)
open import IO

main : Main
main = run (putStrLn (show (2 + 3)))

Проверка запускается из командной строки. Флаг --compile создаёт исполняемый файл через выбранный бэкенд, по умолчанию — GHC.

agda Hello.agda
agda --compile Hello.agda
./Hello

Векторы и доказательства

Определим вектор: конструктор [] даёт пустой вектор, а _∷_ добавляет элемент и увеличивает длину на единицу. Тип длины — индекс, поэтому разные длины — разные типы.

data Vec (A : Set) : ℕ → Set where
  []  : Vec A zero
  _∷_ : ∀ {n} → A → Vec A n → Vec A (suc n)

head : ∀ {A n} → Vec A (suc n) → A
head (x ∷ xs) = x

Обратите внимание: в сигнатуре head стоит suc n, а не произвольное n. Компилятор видит, что пустой вектор не подходит, и не требует отдельной ветки для []. Это и есть практическая польза зависимых типов: невозможные случаи исчезают из кода.

Функция append складывает длины. Доказательство завершаемости здесь не нужно — структурная рекурсия по первому вектору видна проверяющему тотальности.

_++_ : ∀ {A m n} → Vec A m → Vec A n → Vec A (m + n)
[]       ++ ys = ys
(x ∷ xs) ++ ys = x ∷ (xs ++ ys)

Работа в редакторе

Agda рассчитана на интерактивную разработку. В Emacs режим agda2-mode даёт «дыры» в программе: вы пишете ?, загружаете файл, и редактор показывает цель и доступные переменные. Затем цель уточняется по частям, а компилятор проверяет каждый шаг.

• C-c C-l — загрузить и проверить файл.
• C-c C-, — показать цель и контекст.
• C-c C-. — показать тип выражения под курсором.
• C-c C-r — уточнить цель, создав заготовку.
• C-c C-c — разобрать случай по переменной.

Для VS Code есть расширения с поддержкой языка, но именно Emacs остаётся наиболее полной средой. Начинающим стоит пройти встроенный учебник: он учит не синтаксису, а процессу — как вести цель к готовому доказательству.

Полезные флаги и типичные ошибки

Флаг --safe запрещает небезопасные конструкции, --without-K меняет правила для равенства, --cubical включает кубическую теорию типов. Включайте их осознанно: смена теории ломает часть библиотек.

Самая частая ошибка новичка — незакрытая мета-переменная: программа «проверилась», но в ней осталась дыра ?. Вторая — нарушение завершаемости: рекурсивный вызов идёт не по структурно меньшему аргументу. Третья — путаница вселенных: Set сам имеет тип Set₁, и попытка сделать Set : Set обречена.

agda --safe Hello.agda
agda --without-K Hello.agda
agda --cubical Hello.agda

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

Модули и импорты

Каждый файл — модуль, имя которого должно совпадать с путём. Директива open import подключает другой модуль, а using и renaming сужают пространство имён. Если импорт не находится, проверьте список библиотек и путь к проекту: Agda не ищет модули «наугад», она следует только явно заданным каталогам.

open import Data.Vec using (Vec; _∷_; [])
open import Relation.Binary.PropositionalEquality using (_≡_; refl)

Практический смысл

Agda полезна не только математикам. Она помогает проектировать API, где инварианты выражены в типах, проверять протоколы и структуры данных, а также объяснять идеи зависимых типов на живых примерах. Код на Agda можно извлечь в Haskell и использовать как библиотеку, хотя для большинства задач проще ограничиться прототипом и доказательством ключевых свойств.

Ещё один сценарий — обучение. Разбирая доказательство по шагам в интерактивном режиме, проще понять, как устроены индукция, равенство и завершаемость. Для команды это хороший способ договориться о точных формулировках инвариантов до написания кода. Начать можно с одного модуля и двух функций — этого достаточно, чтобы оценить подход.

Итог

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