Idris: зависимые типы на практике

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

Что дают зависимые типы

В обычном языке head возвращает значение или бросает исключение. В Idris тип формулируют так, что пустой список станет ошибкой компиляции. Vect n a содержит длину на уровне типа, а Fin n — число, заведомо меньшее n. Вместе они превращают проверки в доказательства, которые нельзя забыть.

Выгода не в математике ради математики, а в переносе части тестов в компилятор. Парсер CSV, возвращающий строку ровно из n колонок; протокол, где нельзя отправить данные до рукопожатия; доступ к буферу без проверки индекса — всё это описывается типами. Цена — сложные сигнатуры и время на доказательства.

Установка

Проще всего поставить Idris 2 через pack: скрипт приносит компилятор в домашний каталог и не трогает системные пакеты. Понадобятся Chez Scheme, Git и компилятор C. Пакеты и LSP ставятся отдельно.

bash -c "$(curl -fsSL https://raw.githubusercontent.com/stefan-hoeck/idris2-pack/main/install.bash)"
pack update
pack install-app idris2-lsp
idris2 --version

После установки проверьте, что pack виден в новом shell. Если вы предпочитаете системный пакет, в некоторых дистрибутивах есть готовые пакеты idris2, но версия может отставать. Для редактора поставьте плагин, который умеет запускать idris2-lsp: без него подсказки типов и интерактивные дыры становятся неудобными.

Векторы фиксированной длины

Начнём с функции, которая берёт первый элемент и не падает на пустом векторе. Компилятор видит, что образец x :: _ покрывает вектор длины хотя бы один.

import Data.Vect

safeHead : Vect (S n) a -> a
safeHead (x :: _) = x

safeTail : Vect (S n) a -> Vect n a
safeTail (_ :: xs) = xs

Сигнатура Vect (S n) a означает «вектор, длина которого равна следующему за n», то есть минимум один. Вызвать safeHead [] нельзя: типы не сойдутся. Функция safeTail возвращает вектор длины n. Обе функции тотальны: конструкторы вектора покрывают все случаи.

Длина может быть результатом вычисления. replicate принимает n и значение, а возвращает Vect n a. Складывать можно только векторы одинаковой длины, а конкатенация возвращает сумму длин. За каждой операцией стоит индуктивное определение.

Fin и безопасная индексация

Fin n — тип чисел от нуля до n-1. Он строится конструкторами FZ (ноль) и FS (следующий). Индекс нельзя создать из воздуха: значение типа Fin 3 равно 0, 1 или 2.

import Data.Fin
import Data.Vect

safeIndex : (i : Fin n) -> Vect n a -> a
safeIndex FZ (x :: _) = x
safeIndex (FS k) (_ :: xs) = safeIndex k xs

third : Vect 3 String -> String
third v = safeIndex 2 v

Литерал 2 приводится к Fin 3 автоматически. Если написать safeIndex 3 v, программа не соберётся: тройка не помещается в Fin 3. В императивном коде это было бы исключением в рантайме или чтение чужой памяти, а здесь ошибка видна до запуска.

Тип Fin удобен для разбора бинарных форматов и таблиц переходов. Состояние описывают как индекс, а таблицу переходов — как вектор той же длины. Добавили состояние — компилятор потребует обновить таблицу.

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

Простые равенства доказываются конструктивно. Чтобы убедить компилятор в n + 0 = n, достаточно индукции: база — Refl, шаг — cong S к индукционному предположению.

%default total

plusZero : (n : Nat) -> n + 0 = n
plusZero Z = Refl
plusZero (S k) = cong S (plusZero k)

%default total требует, чтобы функции завершались и покрывали все случаи. Это дисциплина, которая ловит забытые ветки. Иногда компилятор не может доказать завершение — тогда помогает assert_total, но это осознанное обещание, а не способ заткнуть ошибку. Ещё один инструмент — rewrite: он заменяет часть типа по доказанному равенству.

Для конфигурации удобен тип-индекс: data Setting : String -> Type, где Setting "port" хранит число, а Setting "host" — строку. Разбор возвращает Maybe (Setting key), и вызывающий код не перепутает поля. Это заменяет десяток проверок вроде «а точно ли здесь число».

Проект и сборка

Проект описывается файлом ipkg. В нём перечислены модули, зависимости и главный файл. Сборка через pack подтягивает зависимости и кладёт исполняемый файл в build/exec.

package configcheck
version = 0.1.0
authors = "Team"
main = Main
depends = base
modules = Config, Main

pack build configcheck.ipkg
./build/exec/configcheck

Для быстрой проверки одного файла хватает idris2 Main.idr -o app. Команда pack repl открывает REPL с зависимостями проекта, а pack run test.ipkg запускает тестовый модуль. Держите доказательства рядом с кодом: если тип изменился, компилятор укажет все места, где доказательство перестало работать.

FFI и бэкенды

Idris 2 по умолчанию компилирует через Chez Scheme, но есть бэкенды Racket, Node.js и C. Для вызова C используется директива %foreign; возвращаемое значение оборачивают в PrimIO, чтобы сохранить чистоту.

%foreign "C:puts,libc"
puts : String -> PrimIO Int

main : IO ()
main = do
  _ <- primIO (puts "hello from Idris")
  pure ()

Для C-бэкенда сборка выглядит как idris2 --cg refc -o app Main.idr. Проверяйте, какой бэкенд поддерживает нужные библиотеки: экосистема Idris 2 меньше, чем у Python или Go, и не каждая задача имеет готовую обёртку. FFI стоит изолировать в отдельном модуле, чтобы основная логика оставалась чистой и проверяемой.

Когда не стоит

Idris 2 не заменит Python для скриптов и не подходит команде без готовности разбираться с доказательствами:

• компиляция медленнее;
• вакансий мало;
• библиотек немного.

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

Итог

Idris 2 превращает часть проверок в типы: Vect не даёт выйти за длину, Fin гарантирует допустимый индекс, а тотальные функции исключают необработанные ветки. Начните с установки через pack, напишите безопасные safeHead и safeIndex, затем добавьте доказательство вроде plusZero. Проект собирается через ipkg и pack, а FFI позволяет обращаться к C. Главное — не гнаться за тотальностью всего кода, а выбрать участки, где цена ошибки выше цены доказательства.