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

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

Зависимый тип — тип, параметризованный значением, например Vector n a — список ровно из n элементов типа a, где n — число на уровне типа.

Что значит «зависеть от значения»

В обычных системах типы зависят от типов: List a параметризован типом a. Зависимые типы идут дальше — тип может зависеть от значения. Канонический пример: Vector n a, список фиксированной длины n. Тут n — не тип, а конкретное число, поднятое на уровень типа. Это стирает границу между значениями и типами: число живёт в обоих мирах.

Зачем? Чтобы выражать инварианты, недоступные обычным типам. Конкатенация получает честный тип Vector n a -> Vector m a -> Vector (n + m) a: компилятор знает и проверяет, что длина результата — сумма длин. А head требует Vector (Succ n) a — непустой по построению, так что «head пустого вектора» невыразимо.

-- Idris/Agda-нотация
append : Vector n a -> Vector m a -> Vector (n + m) a
head   : Vector (S n) a -> a        -- требует длину минимум 1
replicate : (n : Nat) -> a -> Vector n a   -- тип зависит от значения n

Пи-типы и Сигма-типы

Зависимость обобщает знакомые конструкции. Пи-тип (x : A) -> B x — зависимая функция: тип результата зависит от значения аргумента (обобщение стрелки и forall). Сигма-тип (x : A) ** B x — зависимая пара: тип второй компоненты зависит от первой (обобщение произведения и «существует»). По Карри — Говарду Пи — это «для всех» (квантор всеобщности), Сигма — «существует». Так логика первого порядка тоже становится типами.

Демонстрация: вектор длины n с проверкой инварианта

Полноценные зависимые типы Python не выразит, но мы можем смоделировать проверку инварианта длины — то, что зависимая система делает статически, мы сделаем как защищённый конструктор.

class Vector:
    def __init__(self, n, items):
        if len(items) != n:
            raise TypeError("инвариант нарушен: длина " + str(len(items)) + " != n=" + str(n))
        self.n = n
        self.items = list(items)

def append(v1, v2):
    # тип результата: Vector (n + m) -- складываем длины
    return Vector(v1.n + v2.n, v1.items + v2.items)

def head(v):
    if v.n == 0:                       # в зависимой системе это невыразимо вовсе
        raise TypeError("head требует Vector (S n): длина >= 1")
    return v.items[0]

a = Vector(2, [10, 20])
b = Vector(3, [1, 2, 3])
c = append(a, b)
print("append длины 2 и 3 -> n =", c.n, "items =", c.items)
print("head a =", head(a))
try:
    head(Vector(0, []))
except TypeError as e:
    print("ошибка:", e)

Вывод:

append длины 2 и 3 -> n = 5 items = [10, 20, 1, 2, 3]
head a = 10
ошибка: head требует Vector (S n): длина >= 1

Разница: у нас проверка в рантайме, а в Idris/Agda тип Vector (n+m) проверяется статически — несоответствие длины не скомпилируется. Инвариант становится теоремой.

Что позволяют доказывать

С зависимыми типами спецификация и доказательство сливаются с программой. Можно потребовать в типе, что сортировка возвращает отсортированную перестановку входа; что индекс не выходит за границы; что протокол соблюдает порядок операций. Тип Sorted (sort xs) обитаем только корректной сортировкой. Платформы: Agda и Idris (языки программирования с зависимыми типами), Coq и Lean (преимущественно пруверы), F* (верификация системного кода).

Как работает под капотом

Раз типы содержат значения, проверка типов должна вычислять: чтобы сверить Vector (2 + 3) с Vector 5, чекер редуцирует 2 + 3 до 5. Поэтому в зависимых системах проверка типов запускает вычисление, а равенство типов становится равенством с точностью до редукции (definitional equality). Отсюда же требование завершаемости: незавершающееся вычисление в типе зациклит проверку и разрушит логику.

Частые ошибки

Путать List a и Vector n a. Первый параметризован типом, второй — ещё и значением длины.
Думать, что зависимые типы бесплатны. Доказательства инвариантов пишет человек; это мощно, но трудозатратно.
Игнорировать завершаемость. В зависимой системе общая рекурсия запрещена/ограничена, иначе проверка типов и логика ломаются.

Итоги

Зависимый тип параметризован значением (Vector n a), стирая границу значение/тип.
Пи-тип — зависимая функция («для всех»), Сигма-тип — зависимая пара («существует»).
Инварианты (длина, сортированность, границы) становятся проверяемыми теоремами.
Проверка типов вычисляет; равенство — с точностью до редукции; нужна завершаемость.