Pull to refresh

Zipper — производная от типа

Reading time5 min
Views3K
Zipper — способ представления типа данных, позволяющий проходить по структуре и изменять отдельные элементы, несмотря на функциональную чистоту. Например, если по списку мы можем только пробежаться вперёд, делая что-либо с элементами, то с зиппером мы сможем «находиться» в определённом элементе, перемещаться вперёд-назад и менять текущий элемент.
Интересно то, что зиппер для некоторого типа можно получить буквально взяв его производную.

Попробуем сначала придумать зиппер для списка без математики.
Нам нужна возможность пройти по списку вперёд и назад, а также иметь отдельно взятое текущее значение, чтобы его менять.
[0,1,2,3,4,5,6,7,8,9]
       |
[0,1,2]3[4,5,6,7,8,9]
Отсюда видно, что зиппер можно представить как текущий элемент, список последующих значений и список предыдущих. Тогда для перехода к элементу 4 мы просто добавим 3-ку к списку предыдущих, а у списка последующих эту 4-ку «оторвём», а для перехода к элементу 2 всё наоборот. Так как добавлять и отрезать у списка проще с головы, то список предыдущих элементов удобнее развернуть (так что в данном случае 2-ка будет находиться спереди списка). Замена текущего элемента тривиальна.
[1,2]3[4,5,6,7,8,9]
     |->
[1,2,3]4[5,6,7,8,9]
       |
[1,2,3]7[5,6,7,8,9]
Чтобы получить зиппер для списка, в качестве начального элемента можно взять его голову, а в качестве последующих элементов — хвост. Ну а чтобы получить соответствущий список для зиппера, список предыдущих элементов (не забыв его развернуть обратно, конечно) надо соединить с текущим элементом и списком последующих.

Чтобы брать производную, для начала нужно как-то представить тип в пригодном для её взятия виде.
Пусть тип 0 — тип, не имеющий ни одного значения, 1 — тип с ровно одним значением и т.д.
Тип A + B может быть представлен либо значением типа A, либо значением типа B. Т.о. количество всех возможных значений типа A + B будет суммой всех возможных значений A и B. В Хаскеле это соответствует типу Either a b.
Тип A × B представляется значениями обоих типов одновременно, т.е. это кортеж.

Список может быть либо пустым (простое значение — соответствует 1), либо содержит голову (элемент соответствующего типа) и хвост (остаток списка). Запишем это с помощью вышеописанной нотации:
List A = 1 + A × (List A)
Зиппер для списка содержит текущий элемент, список спереди и список позади:
ZipperList A = A × (List A) × (List A)
Перепишем тип списка в виде обычной функции, чтобы было привычнее брать производную:
f(x) = 1 + x*f(x)
zipper = x*f'(x) -- x - текущий элемент
Только в данном случае x — это не число, а тип [элементов списка], но это никак не влияет на дальнейшие преобразования.
Далее следует механическое взятие производной, известное всем ещё со школы:
f'(x) = 0 + 1*f(x) + x*f'(x)
f'(x) = f(x) + x*f'(x)
переименуем f' в g
g(x) = f(x) + x*g(x)
если пару раз раскрыть g(x) в правой части
g(x) = f(x) + x*f(x) + x*x*f(x) + x*x*x*g(x)
то можно увидеть, что f(x) можно вынести за скобки
g(x) = f(x) * (1 + x*g(x))
введём дополнительную функцию h(x)
h(x) = 1 + x*h(x)
заметим, что h(x)*f(x) = g(x)
h(x)*f(x) = f(x) + x*f(x)*h(x) = f(x) + x*f(x) + x*x*f(x)*h(x) = g(x)
g(x) = f(x)*h(x)
А теперь посмотрите на f(x) ;)
f(x) = 1 + x*f(x)
h(x) = 1 + x*h(x)
Таким образом, окончательно zipper имеет вид
zipper = x*f'(x) = x*f(x)*h(x)
Zipper = A × (List A) × (List A)
Т.е. ровно то, что и было у нас!

Чтобы убедиться, попробуем найти зиппер для дерева и разберёмся с тем, что получится. Дерево может быть либо пустым, либо иметь текущий элемент и левую/правую ветки:
Tree A = 1 + A × (Tree A) × (Tree A)
f(x) = 1 + x*f(x)^2
f'(x) = 0 + 1*f(x)^2 + x*2*f(x)*f'(x)
f'(x) = f(x)^2 + f'(x)*(2*x*f(x))
-- f' -> g, f(x)^2 -> T, 2*x*f(x) -> S
g(x) = T + S*g(x) = T + S*T + S*S*g(x) = T + S*T + S*S*T + ... = T * (1 + S*g(x))
История повторяется, только выражения стали посложнее. Аналогично можно вынести T и в итоге получим:
h(x) = 1 + S*h(x) = List S(x)
g(x) = T(x) * (List S(x))

Zipper = A × (Tree A) × (Tree A) × [A × (Tree A) + A × (Tree A)]
Остаётся разобраться, что это всё означает.
Первое A, очевидно, значение в текущем узле. Последующие два (Tree A) — левое и правое поддеревья относительно этого узла. Зная их, мы сможем продвинуться вниз по дереву — вправо или влево.
Если пойдём направо, то текущие значения поддеревьев мы возьмём из правого поддерева, а чтобы не потерять левое, мы его запишем в список. Но кроме этого надо также указать в списке, какой именно путь мы выбрали (вправо или влево), поэтому там сумма из одинаковых кортежов. Если там лежит значение левого слагаемого, то мы продвинулись влево, если правого — то вправо. Таким образом, вся информация для перемещения имеется.
Как нам вернуться обратно вверх? Чтобы сделать один шаг наверх, надо знать элемент в том узле и знать недостающее поддерево (одно у нас и так имеется — наше текущее положение и есть известное поддерево узла выше). Шагов вверх может быть много, поэтому необходимо хранить весь список.
Если в голове списке лежит значение Left (5 × rtree), то в текущий узел мы попали, шагнув влево, из узла со значением 5, у которого правое поддерево есть rtree; а если в списке лежит Right (7 × ltree), то мы шагнули вправо из узла с левым поддеревом rtree.

Возможно, кодом будет понять проще, приведу его «как есть», проверить его можно в интерпретаторе.
data Tree a = Empty | Node a (Tree a) (Tree a) deriving (Read, Show)

data TreeZipper a = TreeZipper a (Tree a) (Tree a) [Either (a, Tree a) (a, Tree a)] deriving (Read, Show)

zipperFromTree Empty = error "Zipper can't point empty trees"
zipperFromTree (Node val left right) = TreeZipper val left right []

zipperToTree (TreeZipper val left right []) = Node val left right
zipperToTree zipper = zipperToTree $ moveBack zipper

moveRight (TreeZipper _ _ Empty _) = error "No way!"
moveRight (TreeZipper val left (Node nval nleft nright) trace) =
    TreeZipper nval nleft nright ((Right (val, left)):trace)

moveLeft (TreeZipper _ Empty _ _) = error "No way!"
moveLeft (TreeZipper val (Node nval nleft nright) right trace) =
    TreeZipper nval nleft nright ((Left (val, right)):trace)

moveBack (TreeZipper val left right []) = error "No way!"
moveBack (TreeZipper val left right ((Right (rval, rleft)):trace)) =
    TreeZipper rval rleft (Node val left right) trace
moveBack (TreeZipper val left right ((Left (lval, lright)):trace)) =
    TreeZipper lval (Node val left right) lright trace

getNodeValue (TreeZipper val _ _ _) = val
setNodeValue (TreeZipper _ left right trace) = TreeZipper val left right trace

-- Теперь можно взять дерево, пройтись вправо, затем влево, и поменять элемент на 10
ghci> zipperFromTree tree
TreeZipper 1 (Node 2 Empty Empty) (Node 3 (Node 4 Empty Empty) Empty) []
ghci> moveRight it
TreeZipper 3 (Node 4 Empty Empty) Empty [Right (1,Node 2 Empty Empty)]
ghci> moveLeft it
TreeZipper 4 Empty Empty [Left (3,Empty),Right (1,Node 2 Empty Empty)]
ghci> setNodeValue 10 it
TreeZipper 10 Empty Empty [Left (3,Empty),Right (1,Node 2 Empty Empty)]
ghci> zipperToTree it
Node 1 (Node 2 Empty Empty) (Node 3 (Node 10 Empty Empty) Empty)


По мотивам The Derivative of a Regular Type is its Type of One-Hole Contexts
Tags:
Hubs:
+22
Comments11

Articles