Dependent types. Don't need proofs

У многих зависимые типы ассоциируются с теоремами и доказательствами. Это и не странно, поскольку, наверное, первое, на что обращает внимание пытливый ум, это изоморфизм Карри-Ховарда. Но доказывать теоремы и проверять доказательства — это далеко не все, что можно делать с помощью зависимых типов.

А что, если бы не было изоморфизма Карри-Ховарда? Никаких теорем, никаких доказательств, никаких HoTT и так далее. Но что бы тогда осталось? Вы не поверите! Осталась бы суть... а именно зависимые типы.

Давайте рассмотрим пару функций на Агда (объектами типа Set в Агде являются простые типы, такие как Int, String, etc.):

Provider : String → Set
Provider "Nat" = ℕ
Provider "String" = String

provide : (s : String) → Provider s
provide "Nat" = 42
provide "String" = "Hello world!"

Так просто — и уже зависимые типы.

Что можно сказать об этом коде? Во-первых он имеет смысл только когда аргумент известен на этапе компиляции (конечно и в рантайме от него может быть польза, но пусть исследование этого будет домашним заданием). Во-вторых тип результата полностью зависит от значения аргумента, а не просто параметризован им, как например в случае этой функции. Как это влияет на использование данных функций?

len : String → ℕ
len = ...

test₁ = len (provide "String")
test₂ = len (provide "Nat") -- Type error: ℕ != String

Первый тест компилируется, тогда как второй нет. Это и понятно, но самое интересное, что для определения типа нужно полностью выполнить функцию provide. То есть окончательный тип результата, с которым можно хоть что-то полезное делать, появляется только после выполнения самой функции. Если еще раз пристально всмотреться в этот код можно увидеть следующее:

def provide(s):
    if (s == "int"):
        return 42
    elif (s == "str"):
        return "Hello world!"

test1 = len(provide("str"))
test2 = len(provide("int")) # TypeError: object of type 'int' has no len()

И это не шутка :) даже несмотря на смайл :-D

Единственная принципиальная разница — это то, когда именно выполняется provide: на Агда — во время компиляции программы, а на Питоне, соответственно — во время ее выполнения. Но и там и там проверка типов при вызове функции len осуществляется уже после выполнения функции provide.

Ну и наконец практическая польза. Из-за своей тесной связи с теорией предикатов (тут нужно вспомнить, что Агда все таки разрабатывалась с сильной оглядкой на изоморфизм Карри-Ховарда), она не допускает противоречивостей, все функции тотальны, а все рекурсии останавливаются. По-этому все случаи нужно обрабатывать и описывать (даже те, которые никогда не выполнятся). Рассмотрим пример (взято из брутального введения).

sub : (n m : ℕ) → m ≤ n → ℕ
sub n .zero z≤n  = n
sub (suc n) (suc m) (s≤s p) = sub n m p

Тут у нас "правильное" вычитание, которое работает НЕ для всех аргументов. А вот представим теперь, что нам нужно воспользоваться этой функцией во время компиляции, то есть оба аргумента известны на этапе компиляции. Зачем нам тогда доказательства?

Зачем вообще нужны доказательства?

Доказательства (теоремы, и соответственно типы) нужны для того, чтоб охарактеризовать некий объект и описать его свойства в то время, когда он сам неизвестен.

Например "правильное" вычитание знает что его аргументы — натуральные числа, а также, что вычитаемое меньше уменьшаемого и это — все, что знает данная функция.

Возвращаемся. Так что делать, если аргумент известен на этапе компиляции? Во-первых не нужно никакое дополнительно описание (доказательство), у нас есть объект — лучшего описания не придумаешь. Во-вторых может просто НЕ быть возможности построить нужное доказательство. В таком случае нам нужна ошибка этапа компиляции. И пример:

Sub : ℕ → ℕ → Set
Sub n zero = ℕ
Sub zero (suc m) = ⊤
Sub (suc n) (suc m) = Sub n m

sub : (n m : ℕ) → Sub n m
sub n zero = n
sub zero (suc m) = _
sub (suc n) (suc m) = sub n m

x₁ : ℕ
x₁ = sub 3 3 -- Ok

x₂ : ℕ
x₂ = sub 2 3 -- Type error: ⊤ != ℕ

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

Выводы

Данный подход является очень мощным, несмотря на свою простоту, поскольку дает возможность проверять, а не доказывать. Такой себе Пролог. Также этот подход широко используется в Decidable TypeRep, так как все вычисления происходят во время компиляции. Например, сначала строится Haskell style TypeRep (т.е. undecidable, НЕ типозависимый), так как это проще, а далее из этого TypeRep строится Decidable TypeRep. И в процессе построения просто проверяется можно ли это сделать. Действительно удобно и мощно.