Зависимые типы имеют реальное практическое применение. И бояться их не надо, они могут встречаться в самых неожиданных местах. Посмотрите внимательно в вашем коде, я думаю скорее всего найдете пару-тройку применений зависимых типов. И это — не обязательно сложные математические доказательства.
Более мощная система типов повышает выразительную мощь языка, что позволяет лаконичнее описывать решение практической задачи.
Задача
Имеем структуру представляющую битовую последовательность. Структура эта по сути треугольник. Ниже приведены примеры.
^ /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-треугольники могут иметь разный размер, что — не хорошо. Таким образом типы функций теперь выражают меньше чем хотелось бы.
Не сочтите за докапывание на пустом месте, статья очень понравилась и написана неплохим языком, однако
ВідповістиВидалити“Также с типов видно что в случае сворачивания получаемый треугольник имеет глубину на единицу меньшую чем входной.”
очень бросилось в глаза. На мой вкус, следует переписать как
“Также *из* типов видно*,* что”.
Еще раз приношу извинения за комментарий не по существу.
Спасибо. Приятно, что статья воспринялась вами именно как статья :)
Видалити