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

[migmit]

Дошло тут до меня о великий царь, что, хотя в 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]

Comments

[vinslivins.livejournal.com]

3. результат должен быть перестановкой исходного значения

[migmit.livejournal.com]

Я думал об этом, но тут слишком много вариантов, я пока не знаю, как лучше делать. Может, третью часть напишу. Когда-нибудь.

[sassa-nf.livejournal.com]

а не придётся ли тогда где-то как-то определять равенство?

[migmit.livejournal.com]

Как в части II — вполне можно.

[sassa-nf.livejournal.com]

ммм... мне кажется, это не совсем то.

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

  data insert_into_==_ {A : Set} (x : A) : List A -> List A -> Set where
    iihead : (xs : List A) -> insert x into xs == (x :: xs)
    iimid  : (xs : List A) -> (hs : List A) -> (h : A) -> insert x into xs == hs -> insert x into (h :: xs) == (h :: hs)

и

  data Permutation {A : Set} : List A -> List A -> Set where
    pnil : Permutation nil nil
    p::  : forall {xs zs ys} -> (x : A) -> (y : A) -> insert y into zs == ys -> x == y -> Permutation xs zs -> Permutation (x :: xs) ys

Кажется, в Permutation можно и обойтись без x == y, а вот insert x into xs == ys всё-таки требует зависимого типа от x:A, чтобы insert 0 into xs == ys и insert 1 into xs == ys были отличимы на уровне компилирования - т.е. придётся моделировать и типы элементов списка, не только Nat.

Хотя, может, на самом деле можно как-то и обойтись.

[migmit.livejournal.com]

Ну дык надо инсёртить не само значение, а значение с тэгом.

[sassa-nf.livejournal.com]

любопытно посмотреть.

[migmit.livejournal.com]

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