субота, 24 серпня 2013 р.

Dependent types at work

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

Более мощная система типов повышает выразительную мощь языка, что позволяет лаконичнее описывать решение практической задачи.

Задача

Имеем структуру представляющую битовую последовательность. Структура эта по сути треугольник. Ниже приведены примеры.

    ^
   /0\
  *---*

      ^
     /0\
    *---*
   /0\1/1\ 
  *---*---*

          ^
         /0\ 
        *---*
       /1\1/0\
      *---*---*
     /0\1/0\1/1\
    *---*---*---*
   /0\1/1\1/0\1/0\
  *---*---*---*---*

То есть высота этого треугольника — степень числа 2, а количество ячеек — степень числа 4.

Так же имеются заданные правила (16 штук), с помощью которых можно переписывать треугольники состоящие из четырех ячеек. Эти правила имеют вид:

      ^            ^
     /0\          /1\
    *---*  ===>  *---*
   /0\1/1\      /1\0/1\
  *---*---*    *---*---*

Среди этих правил есть два терминальные:

      ^            ^
     /0\          /0\
    *---*  ===>  *---*
   /0\0/0\      /0\0/0\
  *---*---*    *---*---*
      ^            ^
     /1\          /1\
    *---*  ===>  *---*
   /1\1/1\      /1\1/1\
  *---*---*    *---*---*

Так же имеется два дополнительных правила:

      ^
     /0\          ^
    *---*  ===>  /0\
   /0\0/0\      *---*
  *---*---*
      ^
     /1\          ^
    *---*  ===>  /1\
   /1\1/1\      *---*
  *---*---*

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

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

А задачей является написать алгоритм, который примет на вход битовую строку правильной длинны (записанный в строку треугольник) и вернет единственный бит, полученный с помощью выше описанных правил.

Решение

Базовыми типами у нас будут вектор статической длинны 4, и бит (0 или 1).

data Bit : Set where
  B0 B1 : Bit

Triangle : Set  Set
Triangle A = Vec A 4

Треугольники различного размера в этом случае будут иметь также разные типы, но при этом у нас будет гарантия времени компиляции, что все четыре sub-треугольника имеют одинаковую глубину (размер), так как они имеют один и тот же тип.

t0 : Bit
t0 = B0

t1 : Triangle Bit
t1 = B0  B1  B0  B1  []

t2 : Triangle (Triangle Bit)
t2 = t1  t1  t1  t1  []

Тогда базовые операции задаваемые условием задачи будут выглядеть следующим образом:

triangle⇒triangle : Triangle Bit  Triangle Bit
triangle⇒triangle = ... {- 16 rules here -}

triangle⇒bit : Triangle Bit  Maybe Bit
triangle⇒bit (B0  B0  B0  B0  []) = just B0
triangle⇒bit (B1  B1  B1  B1  []) = just B1
triangle⇒bit _ = nothing

Операции для работы с треугольниками произвольной длинны выглядят тоже достаточно просто. Присмотревшись к типам, можно видеть, что переписывать и сворачивать можно только треугольники с глубиной больше или равно 1, т.е. с количеством элементов больше или равно 4, так как MultiTriangle (suc n) = Triangle (MultiTriangle n). Также из типов видно, что в случае сворачивания получаемый треугольник имеет глубину на единицу меньшую чем входной.

compose :  {} {A : Set}    (A  A)  (A  A)
compose 0 _ = id
compose (suc n) f = f  compose n f

MultiTriangle :  n  Set
MultiTriangle n = compose n Triangle Bit

replace :  {n}  MultiTriangle (suc n)  MultiTriangle (suc n)
replace {0} = triangle⇒triangle
replace {suc n} = map (replace {n})

reduce :  {n}  MultiTriangle (suc n)  Maybe (MultiTriangle n)
reduce {0} = triangle⇒bit
reduce {suc n}  = helper  map (reduce {n})
    where helper :  {n} {A : Set}  Vec (Maybe A) n  Maybe (Vec A n)
          helper = ...

Кроме важных гарантий времени компиляции (в частности равенство sub-треугольников), в данной задачи зависимые типы разрешают матчить по глубине треугольника. Представьте только себе как бы выглядело решение без этой возможности. Скорее всего появилась бы куча runtime проверок, а код бы уже не выражал достаточно полно и красиво предметную область.

К сожалению Агда не очень пригодна для практических задач, а с другими языками с зависимыми типами я еще не знаком в достаточной мере. Поэтому окончательная реализация выполнена на Хаскеле.

UPDATE: Добавил реализацию без зависимых типов, получилось в полтора раза меньше кода ツ Но! Исчезли некоторые гарантии времени компиляции. Например можно заметить сообщение с ошибкой времени исполнения в функции run. Все потому, что функция rewrite теперь не всегда гарантировано завершается без ошибки, поскольку разные sub-треугольники могут иметь разный размер, что — не хорошо. Таким образом типы функций теперь выражают меньше чем хотелось бы.

2 коментарі:

  1. Не сочтите за докапывание на пустом месте, статья очень понравилась и написана неплохим языком, однако
    “Также с типов видно что в случае сворачивания получаемый треугольник имеет глубину на единицу меньшую чем входной.”
    очень бросилось в глаза. На мой вкус, следует переписать как
    “Также *из* типов видно*,* что”.
    Еще раз приношу извинения за комментарий не по существу.

    ВідповістиВидалити
    Відповіді
    1. Спасибо. Приятно, что статья воспринялась вами именно как статья :)

      Видалити