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

[migmit]

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

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

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

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

На помощь приходят уникальные типы. Да-да, в Хаскеле есть уникальные типы — то есть, такие типы, что в программе возможно только одно значение этого типа (ну, до тех пор, пока мы не начали использовать 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]

Comments

[thedeemon.livejournal.com]

Прикольно!
Я так понимаю, у Олега такой подход назван Lightweight Dependent Typing, у него там куча старинных примеров на окамле.

[migmit.livejournal.com]

Дико силен и дико некультурен. Он, кажется, никогда ничего не читал. Думает, что Вьетнам в Америке. Даже книг по специальности не любит. Иногда, послюнив палец, листает и с отвращением откладывает. "Еще читать, - думает он, - сам сделаю". И действительно, делает.

(c)И. Грекова, "За проходной"

Надо, наверное, всё-таки прочитать, что там у Олега по этому поводу...

[akuklev.livejournal.com]

Класс. Я раньше такое видел ровно в одном месте (см. пред. оратора) и не думал, что оно и на такие задачи масштабируется.

[migmit.livejournal.com]

Меня тут подзуживают написать третью часть — про то, что результат является перестановкой исходной последовательности.