migmit | Путезависимое

Что-то работается сегодня не очень. Напишу, пожалуй, что-нибудь сине-зелёное.

> {-# LANGUAGE Rank2Types #-}
> module PathDependent where

Вот, есть такой классический тип Set. Множество, стало быть. Как известно, оно требует, чтобы элементы, лежащие в нём, принадлежали классу Ord. Ну, внутри у него сбалансированное дерево, которое без упорядоченности не может.

Так вот, как известно, ограничения вида Ord a => ... — это просто ещё один аргумент в функцию. Только неявный. И этот аргумент может, при некоторых условиях, оказаться в разных случаях разным (хотя это и противоречит идеологии классов). Ну, вот может.

То есть, фактически, интерфейс, предоставляемый типом Set примерно такой (я привожу интерфейс не полностью, а на "реализацию" рекомендую не смотреть вообще, она здесь только для примера):

> data Set a = Set
> empty :: Set a
> empty = Set
> insert :: (a -> a -> Ordering) -> a -> Set a -> Set a
> insert _ _ ~Set = Set
> check :: (a -> a -> Ordering) -> a -> Set a -> Bool
> check _ _ ~Set = False

Ну и, естественно, здесь мы уже вообще не контролируем, что первый аргумент (типа (a -> a -> Ordering)) будет одним и тем же. А если он будет меняться — наше множество непременно поплывёт. Может, например, оказаться, что один и тот же элемент окажется в нём несколько раз. Или, что ещё хуже, что функция check не найдёт в множестве элемент, который там точно есть. И так далее.

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

> data GSet a = GSet (a -> a -> Ordering) (Set a)

Так, действительно, можно обезопасить указанный интерфейс. Функцию сравнения придётся перенести в другое место, но это не страшно:

> emptyG :: (a -> a -> Ordering) -> GSet a
> emptyG comparator = GSet comparator empty
> insertG :: a -> GSet a -> GSet a
> insertG a (GSet comparator s) = GSet comparator (insert comparator a s)
> checkG :: a -> GSet a -> Bool
> checkG a (GSet comparator s) = check comparator a s

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

> union :: (a -> a -> Ordering) -> Set a -> Set a -> Set a
> union _ ~Set ~Set = Set

unionG :: GSet a -> GSet a -> GSet a
unionG (GSet comparator1 s1) (GSet comparator2 s2) = GSet ??? (union ??? s1 s2)

И что ставить вместо ???? Один из компараторов? Который? А второй что — потерять? А то, что операция получится некоммутативной — ничего? Или поставить один в одном месте, другой — в другом?

Единственный разумный выход — это преобразовать одно из множеств в список и добавить его элементы во второе по одному. Но это — медленная операция. По крайней мере, медленная в сравнении с объединением упорядоченных деревьев.

На этом месте продвинутые читатели подумали "Ха! Зависимые типы!" И да, если бы в Хаскеле были зависимые типы, то мы написали бы что-то в таком духе:

newtype SetDT a (comparator :: a -> a -> Ordering) = SetDT (Set a)

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

emptyDT :: (comparator :: a -> a -> Ordering) -> SetDT a comparator
emptyDT _ = SetDT empty

insertDT :: a -> SetDT a comparator -> SetDT a comparator
insertDT a ~(SetDT s) = SetDT (insert comparator a s)

checkDT :: a -> SetDT a comparator -> Bool
checkDT a ~(SetDT s) = check comparator a s

unionDT :: SetDT a comparator -> SetDT a comparator -> SetDT a comparator
unionDT (SetDT s1) (SetDT s2) = SetDT (union comparator s1 s2)

Собственно говоря, полноценные зависимые типы не обязательны, достаточно того, что в Scala называется path-dependent types. Это более слабая, но и более простая фишка. Суть в том, что тип зависит не от значения, а от указателя на значение. В результате требуемые зависимыми типами доказательства исчезают — зачем доказывать, что два значения совпадают, когда они хранятся в одной переменной.

Так что, Scala может сделать безопасный интерфейс, а мы не можем? Не бывать такому!

Добавим новый тип, который будет своего рода "флагом" для нашего значения:

> newtype Comparator r a = Comparator (a -> a -> Ordering)
> newtype SetPD r a = SetPD (Set a)

Тип r здесь как бы ни при чём, он нигде не используется. Но он поможет нам удостовериться, что компараторы одинаковые.

Интерфейс получается практически идентичный тому, который был приведён в начале поста:

> emptyPD :: SetPD r a
> emptyPD = SetPD empty

> insertPD :: Comparator r a -> a -> SetPD r a -> SetPD r a
> insertPD (Comparator cmp) a (SetPD s) = SetPD (insert cmp a s)

> checkPD :: Comparator r a -> a -> SetPD r a -> Bool
> checkPD (Comparator cmp) a (SetPD s) = check cmp a s

> unionPD :: Comparator r a -> SetPD r a -> SetPD r a -> SetPD r a
> unionPD (Comparator cmp) (SetPD s1) (SetPD s2) = SetPD (union cmp s1 s2)

Ну что ж, это всё хорошо, но мы не решили проблему, а сдвинули её. Теперь нам нужно как-то гарантировать, что все используемые нами значения типа Comparator r a совпадают. Точнее даже, что мы используем только одно значение этого типа. И в этом нам поможет полиморфизм, вместе с такой функцией:

> withComparator :: (a -> a -> Ordering) -> (forall r. Comparator r a -> b) -> b
> withComparator cmp h = h $ Comparator cmp

Фокус в том, что мы не будем экспортировать конструкторы для типов Comparator и SetPD. Мы экспортируем только интерфейс SetPD и функцию withComparator. А значит, эта функция окажется единственным способом создать компаратор. При этом она не даст нам создать компараторы одного типа — точнее, полиморфизм не позволит нам утверждать, что компараторы относятся к одному типу, а это ничем не хуже. Ну, разумеется, если кто-то решит поработать функцией unsafeCoerce, то он сам себе злобный буратино.

Проверяем, как оно работает. Первый тест:

> test1 =
>     withComparator compare $ \c ->
>     checkPD c 1 $ insertPD c 2 $ insertPD c 1 $ emptyPD

Этот тест проходит совершенно нормально, он вполне законный. Попробуем использовать два разных компаратора:

> test2 =
>     withComparator compare $ \c1 ->
>     withComparator (flip compare) $ \c2 ->
>     checkPD c1 1 $ insertPD c2 2 $ emptyPD

Получим ошибку компиляции:

C:\Users\m.mitrofanov\Dropbox\PathDependent.lhs:58:22:
    Couldn't match type `r1' with `r'
      `r1' is a rigid type variable bound by
           a type expected by the context: Comparator r1 Integer -> Bool
           at PathDependent.lhs:57:7
      `r' is a rigid type variable bound by
          a type expected by the context: Comparator r Integer -> Bool
          at PathDependent.lhs:56:7
    Expected type: SetPD r Integer
      Actual type: SetPD r1 Integer
    In the second argument of `($)', namely `insertPD c2 2 $ emptyPD'
    In the expression: checkPD c1 1 $ insertPD c2 2 $ emptyPD
    In the second argument of `($)', namely
      `\ c2 -> checkPD c1 1 $ insertPD c2 2 $ emptyPD'
Failed, modules loaded: none.

Полиморфизм вообще не позволит нам вытащить ни множества, ни сам компаратор, из аргумента функции withComparator:

> test3 =
>     withComparator compare $ \c ->
>     insertPD c 2 $ insertPD c 1 $ emptyPD

Получаем, опять-таки, ошибку:

C:\Users\m.mitrofanov\Dropbox\PathDependent.lhs:52:7:
    Couldn't match expected type `b' with actual type `SetPD r Integer'
      `b' is a rigid type variable bound by
          the inferred type of test3 :: b
          at PathDependent.lhs:50:3
    In the expression: insertPD c 2 $ insertPD c 1 $ emptyPD
    In the second argument of `($)', namely
      `\ c -> insertPD c 2 $ insertPD c 1 $ emptyPD'
    In the expression:
      withComparator compare
      $ \ c -> insertPD c 2 $ insertPD c 1 $ emptyPD
Failed, modules loaded: none.

Интерфейс полностью безопасен. При этом нам никто не мешает аргумент функции withComparator разбивать на подфункции, которые знать не знают ничего ни про какие {-# LANGUAGE Rank2Types #-}. Главное, чтобы они сохраняли полиморфность по r.

Вот.

Иномировой агент

Путезависимое

Путезависимое

no subject