Доказательное, часть I

Дошло тут до меня о великий царь, что, хотя в Haskell и нет зависимых типов, но его способности к доказательству на самом деле очень и очень велики.

Если говорить, например, об алгоритмах сортировки, то, обычно, приходит в голову две очевидных вещи:
1) Результат должен быть отсортирован, и
2) Результат должен иметь ту же длину, что и исходная последовательность.

Так вот, я раньше думал, что пункт (2) можно отследить типами, а вот пункт (1) — ни фига. Но оказывается...

Прежде, чем писать о пункте (1), я, всё-таки, займусь пунктом (2). Он, конечно, почти очевиден — во всяком случае, очевидно, что это МОЖНО сделать, — но, глядя, как он делается, мы можем лучше понять более сложный пункт (1).

Итак. Само собой, чтобы доказывать на Haskell выполнение пункта (2), нам нужно завести числа на уровне типов. Да, сейчас есть всякие promoted literals и всё такое прочее... но мы будем работать по простому. По сути, единственное расширение, которое нам понадобится по делу — это GADT-ы:

> {-# LANGUAGE GADTs #-}

Ну, для начала мы таки введём наши числа:

> module Num where

> data Zero = Zero
> data Succ n = Succ n

Один момент: почему тип Succ определён именно как data, а не newtype? Дело в том, что паттерн-матчинг для GADT-ов сделан не самым лучшим образом, и, зачастую, сыплет warning-ами на совершенно правильный и законный код. В частности, мы поймаем их, если используем здесь newtype. Этот баг известен; сначала его исправление назначили на версию 7.8.1, потом сдвинули на 7.10.1, потом — на 7.12.1, где он сейчас и висит.

Мы будем доказывать банальный QuickSort. И довольно простой, и довольно эффективный. Но, коли так, нам нужно будет соединять две последовательности в одну. А, значит, их длины — за которыми мы будем следить — складываются. Стало быть, нам нужно сложение чисел.

Операции над типами сейчас модно делать с помощью type families. Но мы, опять-таки, поработаем по старинке, чтобы не уйти в дебри undecidable instance-ов.

А по старинке — это те же GADT-ы:

> data Plus m k n where
>     ZPlus :: Plus Zero n n
>     SPlus :: Plus m k n -> Plus (Succ m) k (Succ n)

Здесь значение типа Plus m k n — это свидетельство того, что m+k=n. Ясен пень, что такое свидетельство можно подделать — например, явно указав в качестве него undefined — но всё-таки более-менее полагаться на него можно. Опять-таки, полноценных доказательств тут не будет, в Haskell каждый тип населён — но работать они помогают.

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

> sPlus :: Plus a b c -> Plus a (Succ b) (Succ c)
> sPlus ZPlus = ZPlus
> sPlus (SPlus p) = SPlus (sPlus p)

А второе, что нам потребуется — довольно технический факт: если f — произвольный тип (подходящего кайнда), то f (0 + n) — это то же самое, что f n. Практически тривиально:

> uzPlus :: Plus Zero k n -> f k a -> f n a
> uzPlus ZPlus fna = fna

Здесь я добавил ещё один аргумент a — по чисто техническим причинам; так будет удобнее впоследствии. Можно было и обойтись.

На этом с числами всё. Займёмся теперь последовательностями.

> {-# LANGUAGE GADTs #-}
> module Seq where
> import Num

Так как мы будем отслеживать длины последовательностей, нам нужно внести длину в, собственно, тип. Числа у нас уже есть, так что всё остальное просто:

> data Seq n a where
>     ZSeq :: Seq Zero a
>     SSeq :: a -> Seq n a -> Seq (Succ n) a

Чтобы иметь возможность посмотреть содержимое такой последовательности, сконвертируем её в обычный список:

> toList :: Seq n a -> [a]
> toList ZSeq = []
> toList (SSeq a as) = a : toList as

Обратный процесс — преобразование списка в такую последовательность — чуть более сложен. В списке не содержится его длина — так что на выходе должна быть последовательность произвольной длины, что означает дополнительный тип:

> data ESeq a where ESeq :: Seq n a -> ESeq a

> fromList :: [a] -> ESeq a
> fromList [] = ESeq ZSeq
> fromList (a : as) = case fromList as of ESeq as' -> ESeq (SSeq a as')

Добрались до, собственно, сортировки.

> {-# LANGUAGE GADTs #-}
> module QS where
> import Num
> import Seq

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

> data TwoSeq n a where TwoSeq :: Seq m a -> Seq k a -> Plus m k n -> TwoSeq n a

Сама функция пишется проще простого: делим хвост списка, после чего добавляем первый его элемент куда нужно. Чтобы решить, куда именно — сравниваем этот самый первый элемент с выбранным зарание pivot-ом. Я специально не стану обобщать и делать деление списка по произвольному предикату, чтобы было более похоже на то, что будет происходит в следующем посте, про пункт (1).

> split :: Ord a => a -> Seq n a -> TwoSeq n a
> split _ ZSeq = TwoSeq ZSeq ZSeq ZPlus
> split a (SSeq a' as) =
>     case split a as of
>       TwoSeq sl sg p ->
>           if a' < a
>             then TwoSeq (SSeq a' sl) sg (SPlus p)
>             else TwoSeq sl (SSeq a' sg) (sPlus p)

Кроме того, такие последовательности придётся склеивать обратно. Для этого нам понадобится аналогичная функция:

> append :: Seq m a -> Seq k a -> Plus m k n -> Seq n a
> append ZSeq as2 p = uzPlus p as2
> append (SSeq a as1) as2 p = appendSucc a as1 as2 p

> appendSucc :: a -> Seq m a -> Seq k a -> Plus (Succ m) k n -> Seq n a
> appendSucc a as1 as2 (SPlus p) = SSeq a (append as1 as2 p)

Зачем понадобилась дополнительная функция appendSucc? Как и выше — чтобы избежать ошибочных warning-ов ghc по поводу "неполного паттерн-матчинга". Увы, ghc в этом месте довольно глуп, и не понимает, что, на самом деле, все остальные варианты паттерн-матчинга невозможны. Причём если их добавить, то он выдаст ошибку типизации (что правильно).

Заметим, кроме того, что в одном месте нам понадобилось использовать функцию uzPlus. По сути, вот из-за чего: мы знаем, что длина получающейся последовательности равна m+k и что n=m+k; но из этого не можем — автоматически — сделать вывод, что длина получающейся последовательности равна n. Приходится кое-где скастовать явно.

Ну и, наконец, вот она, сортировка.

> sort :: Ord a => Seq n a -> Seq n a
> sort ZSeq = ZSeq
> sort (SSeq a as) =
>     case split a as of TwoSeq sl sg p -> append (sort sl) (SSeq a (sort sg)) (sPlus p)

То, что и хотелось — длина списка на выходе гарантированно совпадает с длиной списка на входе. Алгоритм работает тривиально, пустой список выдаётся как есть, остальное делится на два подсписка, они сортируются отдельно, после чего соединяются (с pivot-ом посередине).

Здесь я должен признаться в одном упущении. Когда я писал этот алгоритм в первый раз, я забыл рекурсивно отсортировать подсписки. Получилось что-то в таком роде:

sort (SSeq a as) = case split a as of TwoSeq sl sg p -> append sl (SSeq a sg) (sPlus p)

Соответственно, результат получился хоть и нужной длины, но слегка не такой, как хотелось бы. Вот этим мы в следующем посте и займёмся.

Напоследок — функция для проверки всего этого добра:

> sortList :: Ord a => [a] -> [a]
> sortList as = case fromList as of ESeq as' -> toList (sort as')

Проверяем:

*QS> sortList [5,1,3,2,4] :: [Integer]
[1,2,3,4,5]

Доказательное, часть II

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

Как можно отслеживать подобное при компиляции? Мы знаем, что на этапе компиляции мы можем следить только за типами; все значения одного типа на этом этапе неотличимы. Никаких зависимых типов тут нет. Так как же?

Первое, что приходит в голову — это каким-то образом поднять значения на уровень типов. Например, если значения — это числа, то можно представить их в виде Пеано (что мы, кстати, и делали). Или можно закодировать в типах их двоичное представление.

Сделать это всё, конечно, можно. А вот сделать это полиморфным образом — чтобы не требовать от типа ничего, кроме упорядоченности — уже нельзя. Никак. Да и вообще, это весьма сомнительный трюк. Как же тогда быть?

На помощь приходят уникальные типы. Да-да, в Хаскеле есть уникальные типы — то есть, такие типы, что в программе возможно только одно значение этого типа (ну, до тех пор, пока мы не начали использовать unsafeCoerce и тому подобные вещи). Да, все значения одного типа неотличимы — но если у типа только одно значение, то они к тому же и в рантайме будут гарантированно равны. Итак, как получить уникальный тип в Хаскеле?

> {-# LANGUAGE GADTs #-}
> module Tag(Tag(untag), Tagged(Tagged), tag) where

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

> newtype Tag t a = Tag {untag :: a}

Что же делает его уникальным? То, что конструктор Tag мы не экспортируем. Только сам тип и функцию untag. Поэтому, если мы каким-то образом обеспечим возможность создать значение данного типа, но только одно — то наша задача выполнена. Все значения такого типа, созданные вне данного модуля, будут равны.

Чтобы это сделать, мы воспользуемся всё теми же GADT-ами. Именно, мы спрячем этот самый "тэг" под экзистеншиал:

> data Tagged a where Tagged :: Tag t a -> Tagged a

Теперь мы не будем создавать сам Tag t a, мы будем создавать Tagged a:

> tag :: a -> Tagged a
> tag a = Tagged (Tag a)

Таким образом, мы можем создать кучу значений типа Tagged a — но, распаковав их с помощью паттерн-матчинга, мы получим значения типов Tag t a с разными t. То есть, мы можем создать кучу "тэгированных" значений, несущих внутри себя одно и то же a — но сами по себе они будут разных типов. Мы даже не сможем сравнить их на равенство: равенство действует только в пределах одного типа.

И как же это поможет нам со сравнениями? А вот как. Мы не можем сделать тип 3 < 5 — так как 3 и 5 это значения, а не типы. Но если есть уникальный тип, содержаший значение 3 с тэгом t, и уникальный тип, содержащий значение 5 с тэгом s, мы вполне можем соорудить тип t < s.

Однако, можно также образовать и тип s < t. Как мы гарантируем, что это не происходит? Точно так же, как и в случае тэгов: экспортируя не конструктор, а функцию, проверяющую неравенство.

> {-# LANGUAGE GADTs, TypeOperators #-}
> module Ord(
>   (:=), refl, symm, eTrans,
>   (:<), (:>), mirrorLG, mirrorGL, lTrans, gTrans,
>   Comparison(..), comparison
>   ) where
> import Tag

Но для начала, прежде чем заняться неравенствами, мы займёмся равенствами.

> data t := s = Equal

Напомню, что мы сравниваем тэги, а не сами значения.

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

> refl :: t := t
> refl = Equal

> symm :: t := s -> s := t
> symm Equal = Equal

> eTrans :: t := s -> s := r -> t := r
> eTrans Equal Equal = Equal

Переходим к неравенствам. Достаточно было бы, конечно, ввести одно из них, но я введу оба, и "больше", и "меньше". С симметричными вещами проще работать.

> data t :< s = Less

> data t :> s = Greater

Заметьте, что конструкторы Less и Greater мы не экспортируем, чтобы не допустить прямого создания этих типов вне данного модуля.

Разумеется, эти отношения эквивалентны с точностью до перестановки аргументов:

> mirrorLG :: t :< s -> s :> t
> mirrorLG Less = Greater

> mirrorGL :: t :> s -> s :< t
> mirrorGL Greater = Less

Оба они транзитивны:

> lTrans :: t :< s -> s :< r -> t :< r
> lTrans Less Less = Less

> gTrans :: t :> s -> s :> r -> t :> r
> gTrans Greater Greater = Greater

Остаётся показать, как именно мы будем создавать их. Когда мы сравниваем два значения, может получиться три варианта ответа: первое больше второго, первое равно второму, первое меньше второго. Соответственно, мы введём тип для такого ответа:

> data Comparison t s = CL (t :< s) | CE (t := s) | CG (t :> s)

И, наконец, напишем функцию, которая это сравнение производит.

> comparison :: Ord a => Tag t a -> Tag s a -> Comparison t s
> comparison ta sa =
>   case compare (untag ta) (untag sa) of
>    LT -> CL Less
>    EQ -> CE Equal
>    GT -> CG Greater

Отмечу одно обстоятельство. Мы используем здесь класс Ord, инстанс которого может быть написан неправильно. Например, сравнение может быть нетранзитивным. В этом случае, используя функцию lTrans, мы можем, в принципе, выразить в типах неверное сравнение. Это никак не обойти: транзитивность сравнений нам действительно будет нужна. Но, с другой стороны, если сравнение реализовано неправильно, то и QuickSort будет работать неправильно.

Итак, вся машинерия готова. Теперь со всем этим мы попробуем взлететь.

> {-# LANGUAGE GADTs, TypeOperators #-}
> module QuickSort where
> import Num
> import Ord
> import Seq
> import Tag

Вспомним ещё раз, как делается QuickSort. Для начала мы делим наш список на два, в одном — маленькие элементы, в другом — большие. При этом на сей раз за такими ограничениями мы должны следить. Значит, простой Seq нам не подойдёт, нужен другой тип, который, во-первых, имеет эти самые ограничения сверху и снизу, а, во-вторых, содержит значения вместе с тэгами, без которых мы не можем отслеживать порядок.

> data BoundedSeq l u n a where
>   ZBSeq :: BoundedSeq l u Zero a
>   SBSeq :: Tag t a -> l t -> u t -> BoundedSeq l u n a -> BoundedSeq l u (Succ n) a

То есть, мы храним не только значения с тэгами, но и свидетельства того, что эти значения удовлетворяют наложенным ограничениям.

Правда, изначально никаких ограничений нет. Поэтому нам понадобится "пустое" ограничение:

> data Whatever a = Whatever

Ну и, чтобы старый Seq переделать в новый BoundedSeq, нам понадобится простенькая функция:

> fromSeq :: Seq n a -> BoundedSeq Whatever Whatever n a
> fromSeq ZSeq = ZBSeq
> fromSeq (SSeq a as) = case tag a of Tagged ta -> SBSeq ta Whatever Whatever (fromSeq as)

Далее, в списке могут случиться повторяющиеся элементы. То есть, одно из ограничений — сверху или снизу — должно быть нестрогим.

> data t :<= s = L (t :< s) | E (t := s)

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

> data TwoSeq l u n t a where
>   TwoSeq
>     :: BoundedSeq l ((:>) t) m a
>     -> BoundedSeq ((:<=) t) u k a
>     -> Plus m k n
>     -> TwoSeq l u n t a

К сожалению, инфиксные операторы на уровне типов не позволяют делать секции, иначе можно было бы писать не ((:>) t), а просто (t :>).

Функция, разделяющая список на два, выглядит почти так же, как и в предыдущем случае:

> split :: Ord a => Tag t a -> BoundedSeq l u n a -> TwoSeq l u n t a
> split _ ZBSeq = TwoSeq ZBSeq ZBSeq ZPlus
> split ta (SBSeq ta' lt ut as) =
>   case split ta as of
>    TwoSeq sl sg p ->
>      case comparison ta ta' of
>       CL l -> TwoSeq sl (SBSeq ta' (L l) ut sg) (sPlus p)
>       CE e -> TwoSeq sl (SBSeq ta' (E e) ut sg) (sPlus p)
>       CG g -> TwoSeq (SBSeq ta' lt g sl) sg (SPlus p)

Единственное, о чём нужно позаботиться — это о том, чтобы аккуратно свести случаи "меньше" и "равно".

Теперь второй этап. Мы хотим получить на выходе отсортированную последовательность. Значит, нам потребуется для этого отдельный тип.

> data SortedSeq l u n a where
>   ZSSeq :: SortedSeq l u Zero a
>   SSSeq :: Tag t a -> l t -> u t -> SortedSeq ((:<=) t) u n a -> SortedSeq l u (Succ n) a

Ну и, для преобразования отсортированной последовательности в обычную, простенькая функция:

> toSeq :: SortedSeq l u n a -> Seq n a
> toSeq ZSSeq = ZSeq
> toSeq (SSSeq ta _ _ as) = SSeq (untag ta) (toSeq as)

Теперь — о функции слияния. Тут есть один занятный момент.

Мы склеиваем две последовательности. Отсортированных. Но у первой из них верхняя граница — это выбранный pivot, а не та граница, которая была у исходной, неотсортированной последовательности. Значит, нам нужно как-то скастовать одну последовательность к другой, ослабив ограничение. Для этого нам послужит такой класс:

> class Lower p where lower :: p t -> t :> s -> p s
> instance Lower Whatever where lower Whatever _ = Whatever
> instance Lower ((:>) r) where lower = gTrans

То есть, мы можем либо ослабить ограничение до пустого (Whatever), либо до какой-то большей, но всё-таки существующей, границы.

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

И вот какая функция получается. По чисто техническим причинам мне удобнее склеивать не две последовательности сами по себе, а две последовательности и pivot между ними.

> append3
>   :: Lower u => SortedSeq l ((:>) t) m a
>   -> Tag t a
>   -> l t
>   -> u t
>   -> SortedSeq ((:<=) t) u k a
>   -> Plus m (Succ k) n
>   -> SortedSeq l u n a
> append3 ZSSeq ta lt ut as2 p = uzPlus p (SSSeq ta lt ut as2)
> append3 (SSSeq ta' lt' ut' as1) ta _ ut as2 p = append3Succ ta' lt' ut' as1 ta ut as2 p

> append3Succ
>   :: Lower u => Tag t' a -> l t' -> t :> t'
>   -> SortedSeq ((:<=) t') ((:>) t) m a
>   -> Tag t a -> u t
>   -> SortedSeq ((:<=) t) u k a
>   -> Plus (Succ m) (Succ k) n
>   -> SortedSeq l u n a
> append3Succ ta' lt' tt' as1 ta ut as2 (SPlus p) =
>   SSSeq ta' lt' (lower ut tt') (append3 as1 ta (L (mirrorGL tt')) ut as2 p)

Причина появления дополнительной функции append3Succ — прежняя, иначе ghc будет ошибочно жаловаться на неполный паттерн-матчинг.

Наконец, собираем всё вместе.

> sort :: (Lower u, Ord a) => BoundedSeq l u n a -> SortedSeq l u n a
> sort ZBSeq = ZSSeq
> sort (SBSeq ta lt ut as) =
>   case split ta as of TwoSeq sl sg p -> append3 (sort sl) ta lt ut (sort sg) (sPlus p)

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

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

> sortSeq :: Ord a => Seq n a -> SortedSeq Whatever Whatever n a
> sortSeq as = sort (fromSeq as)

Чтобы протестировать её, введём дополнительную функцию, сортирующую уже обычный, хаскельный список:

> sortList :: Ord a => [a] -> [a]
> sortList as = case fromList as of ESeq as' -> toList (toSeq (sortSeq as'))

Тестируем:

*QuickSort> sortList [5,1,3,2,4,1] :: [Integer]
[1,1,2,3,4,5]