Настроение:	good
Музыка:	Tying Tiffany -- Spin Around
Entry tags:	dependently typed programming, type theory

Булева слепота
Юзер ketmar поднимает важную тему. В самом деле, сколько можно это терпеть? Как известно, булев тип -- это тип, который имеет ровно два значения. Если вы используете его, чтобы проверить выполняется ли некоторое условие (предикат), то вы оказываетесь в весьма глупом положении, потому что эти значения сами по себе никак не связаны с условием, которые вы хотите проверить. Это явление известно как булева слепота.

Механизм зависимых типов позволяет излечиться от булевой слепоты.



Пусть имеются два типа A и B и вы хотите определить функцию f : A -> B. Пусть значения типа A могут обладать некоторым свойством P, которое может выполняется или нет. В обычном языке вам приходится написать функцию p : A -> Bool, проверяющую условие P и две функции g h : A -> B, которые вызываются в зависимости от условия. Т.е. f a = if (p a) then (g a) else (h a). Поскольку функции g и h никак не связаны с условием P вам остается только скрестить пальцы и молиться, что p реализована правильно.

В языке с зависимыми типами, вы можете явно записать само условие P. Задать условие P значит описать множество его доказательств. Тогда, если a имеет тип A, то P a -- это какое-то доказательство того, что для а выполняется P. Если P разрешимо, то это можно явно записать p : (a : A) -> P a + (P a -> Zero), где + -- это прямая сумма, а Zero -- пустой тип. Аргументом для соответствующих ветвей определяемой функции f будет не только само a, но и доказательство P a либо его отрицание: G : {a : A} -> P a -> B, H : {a : A} -> (P -> Zero) -> B, а функция f определяется так:

f a with p a
f a | inl x = G x
f a | inr y = H y

Обе ветви точно знают какую именно ситуацию они обрабатывают, что позволяет избежать большого числа ошибок.

Интересно, что зависимые типы позволяют рафинировать даже тип с одним значением. В классической ситуации, для есть только один предикат над A, который выполняется для всех a из A -- это тривиальный предикат. В конструктивном случае их, вообще говоря, до фига. В частности, если A -- индуктивный тип, то все P для которых можно определить функцию p : (a : A) -> P a содержат, например, все возможные способы определить индукцию над A.

Поясним на примере деления. Деление, как известно, нельзя определить с помощью структурной рекурсии над парой натуральных чисел. В тотальных языках это важно, потому что компилятору всегда должно быть очевидно, что каждая определяемая функция завершается. Что же делать. Определяем вспомогательный индуктивный тип, например, так:

data DivView : Nat -> Nat -> Set where
dz : {k : Nat}(x : Fin (ns k)) -> DivView (ns k) [ x ]
ds : {k : Nat}{n : Nat} -> DivView (ns k) n -> DivView (ns k) ((ns k) + n)

Здесь Fin -- это тип конечных множеств, [_] : {n : Nat} -> Fin n -> Nat -- функция, которая нумерует элементы конечного множества, ns -- функция следования. Тип DivView можно рассматривать как дерево рекурсивных вызовов процедуры деления. Для любой пары натуральных чисел k, n можно построить функцию unfold: (k n : Nat) -> DivView (ns k) n, которая строит это дерево. Это половина дела. Вторая половина -- свернуть это дерево, чтобы получить функции целой части и остатка. Они уже будут примитивно рекурсивны относительно типа DivView:

div : {k n : Nat} -> DivView k n -> Nat
div (dz x) = 0
div (ds x) = ns (div x)

mod : {k n : Nat} -> DivView k n -> Nat
mod (dz x) = [ x ]
mod (ds x) = mod x

Несложно доказать корректность построенной процедуры:

div-correct : {k n : Nat}(x : DivView k n) -> n == (div x) * k + mod x
div-correct (dz x) = refl
div-correct (ds {k} {n} x) = trans (cong (_+_ (ns k)) (div-correct x)) (sym (+-assoc (ns k) (div x * ns k) (mod x)))
where
open CommutativeSemiring commutativeSemiring using (+-assoc)

Мы не только объяснили компьютеру что такое деление, но обучили его новым принципам индукции над натуральными числами и новым способам зависимого сопоставления с образцом (dependent pattern matching). Подробнее об этом можно почитать в статье ``Взгляд Слева''. Декомпозиция в виде развертывание / свертывание связана с двойственностью между коалгебрами и алгебрами, про нее можно прочитать в статье ``Программирование с помощью бананов, линз, оберток и колючей проволоки''. А применительно к определению тотальных функций в статье про соответствующий метод.




Незатейливый теоретико-типовой юморок: