Как сделать бинарное дерево на молнии экземпляром Comonad?
Я хочу сделать бинарную молнию дерева экземпляром Comonad, но я не могу понять, как реализовать duplicate должным образом.
Вот моя попытка:
{-# LANGUAGE DeriveFunctor #-}
import Data.Function
import Control.Arrow
import Control.Comonad
data BinTree a
= Leaf a
| Branch a (BinTree a) (BinTree a)
deriving (Functor, Show, Eq)
data Dir = L | R
deriving (Show, Eq)
-- an incomplete binary tree, aka data context
data Partial a = Missing Dir (BinTree a) a
deriving (Show, Eq, Functor)
-- BTZ for BinTree Zipper
newtype BTZ a = BTZ { getBTZ :: ([Partial a], BinTree a) }
deriving (Show, Eq)
instance Functor BTZ where
fmap f (BTZ (cs,t)) = BTZ (map (fmap f) cs, fmap f t)
-- | replace every node label with the zipper focusing on that node
dup :: BinTree a -> BinTree (BTZ a)
dup (Leaf v) = Leaf (BTZ ([], Leaf v))
dup t@(Branch v tl tr) = Branch (BTZ ([],t)) tlZ trZ
where
tlZ = fmap (BTZ . first (++ [Missing L tr v]) . getBTZ) (dup tl)
trZ = fmap (BTZ . first (++ [Missing R tl v]) . getBTZ) (dup tr)
-- | extract root label
rootVal :: BinTree a -> a
rootVal (Leaf v) = v
rootVal (Branch v _ _) = v
-- | move zipper focus around
goUp, goLeft, goRight :: BTZ a -> BTZ a
goUp (BTZ ([], _)) = error "already at root"
goUp (BTZ (Missing wt t2 v:xs, t1)) = case wt of
L -> BTZ (xs, Branch v t1 t2)
R -> BTZ (xs, Branch v t2 t1)
goLeft z = let (cs,t) = getBTZ z in
case t of
Leaf _ -> error "already at leaf"
Branch v t1 t2 -> BTZ (Missing L t2 v:cs, t1)
goRight z = let (cs,t) = getBTZ z in
case t of
Leaf _ -> error "already at leaf"
Branch v t1 t2 -> BTZ (Missing R t1 v:cs, t2)
instance Comonad BTZ where
extract (BTZ (_,t)) =
case t of
Leaf v -> v
Branch v _ _ -> v
duplicate z@(BTZ (cs, bt)) = case bt of
Leaf _ -> BTZ (csZ, Leaf z) -- extract . duplicate = id
Branch v tl tr ->
-- for each subtree, use "dup" to build zippers,
-- and attach the current focusing root(bt) and rest of the data context to it
let tlZ = fmap (BTZ . first (++Missing L tr v :cs) . getBTZ) (dup tl)
trZ = fmap (BTZ . first (++Missing R tl v :cs) . getBTZ) (dup tr)
in BTZ (csZ, Branch z tlZ trZ)
where
-- go up and duplicate, we'll have a "BTZ (BTZ a)"
-- from which we can grab "[Partial (BTZ a)]" out
-- TODO: not sure if it works
upZippers = take (length cs-1) . tail $ iterate goUp z
csZ = fmap (head . fst . getBTZ . duplicate) upZippers
main :: IO ()
main = do
let tr :: BTZ Int
tr = rootVal $ dup (Branch 1 (Leaf 2) (Branch 3 (Leaf 4) (Leaf 5)))
equalOnTr :: Eq a => (BTZ Int -> a) -> (BTZ Int -> a) -> Bool
equalOnTr = (==) `on` ($ tr)
print $ (extract . duplicate) `equalOnTr` id
print $ (fmap extract . duplicate) `equalOnTr` id
print $ (duplicate . duplicate) `equalOnTr` (fmap duplicate . duplicate)
Некоторое объяснение:
BinTree aявляется типом данных двоичного дерева, и каждый узел дерева содержит метку.Partial aэто двоичное дерево с левым или правым поддеревом. СтекPartial aв моем коде играет роль контекст данных.BTZвыступает заBinTreeмолния, которую я хочу сделать экземплярComonad, он состоит из контекста данных и фокусирующего поддерева.
Чтобы сделать это примером Comonadмой план заключается в реализации extract а также duplicateи убедитесь, что свойства comonad выполнены, взяв несколько случайных двоичных деревьев.
extract это просто, просто убрав фокусирующее поддерево.
функция dup служит вспомогательной функцией, которая заменяет каждую метку узла на молнию дерева, фокусирующуюся на этом узле.
За duplicate zметка узла должна быть z сам так, что extract . duplicate == id держит. Для нелистовых узлов я использую dup иметь дело со своими поддеревьями, как будто у них нет родителей, и текущее внимание z и остальная часть контекста данных добавляется к этим молниям впоследствии.
Пока первые два свойства comonad выполнены (extract . duplicate = id а также fmap extract . duplicate), но я понятия не имею, что делать с контекстом данных. То, что я сейчас делаю, это забираю z и продолжать идти вверх. По пути мы возьмем вершину каждого стека контекста данных, чтобы построить новый стек контекста данных, который звучит правильно, а также имеет правильный тип ([Partial (BTZ a)], Но мой подход не может удовлетворить третий закон.
Учитывая приведенное выше определение типа данных для двоичного дерева, можно ли сделать его экземпляром Comonad? Если ответ да, то что-то не так с моим подходом?
1 ответ
В дифференциальном исчислении нотация Лейбница вызывает меньше путаницы, чем ньютоновская, потому что она явно относится к переменной, относительно которой мы дифференцируем. Контексты в вещах задаются дифференцированием, поэтому мы должны позаботиться о том, что происходит в контексте. Здесь есть два понятия "субструктура" в работе: поддеревья и элементы. У каждого из них есть различные (но связанные) понятия "контекст" и, следовательно, "молния", где молния - это пара вещей и их контекст.
Ваш BTZ Тип представлен как понятие молнии для поддеревьев. Тем не менее, comonadic строительство молнии работает на молнии для элементов: extract означает "дать элемент здесь"; duplicate означает "украшать каждый элемент его контекстом". Итак, вам нужны контексты элементов. Забавно, что для этих бинарных деревьев молнии элементов и поддеревья молний изоморфны, но это происходит по очень конкретной причине (а именно, что они образуют свободную комонаду).
Как правило, молнии элементов и поддеревьев различаются, например, для списков. Если мы начнем с создания comonad element-zipper для списков, мы с меньшей вероятностью потеряемся, когда вернемся к деревьям. Позвольте мне также попытаться заполнить немного больше общей картины, как для других, так и для себя.
Контексты подсписков
Подсписок -contexts для [a] просто даны [a] Будучи списком элементов, мы проходим по пути от подсписка ко всему списку. Контекст подсписка для [3,4] в [1,2,3,4] является [2,1], Контексты подузлов для рекурсивных данных - это всегда списки, представляющие то, что вы видите на пути от узла к корню. Тип каждого шага задается частной производной формулы для одного узла данных относительно рекурсивной переменной. Так вот
[a] = t where -- t is the recursive variable standing for [a]
t = 1 + a*t -- lists of a are either [] or an (a : t) pair
∂/∂t (1 + a*t) = a -- that's one step on a path from node to root
sublist contexts are [a] -- a list of such steps
Таким образом, список-молния является парой
data LinLZ a = LinLZ
{ subListCtxt :: [a]
, subList :: [a]
}
Мы можем написать функцию, которая вставляет подсписок обратно в его контекст, возвращая обратно путь
plugLinLZ :: LinLZ a -> [a]
plugLinLZ (LinLZ { subListCtxt = [], subList = ys}) = ys
plugLinLZ (LinLZ { subListCtxt = x : xs, subList = ys})
= plugLinLZ (LinLZ { subListCtxt = xs, subList = x : ys})
Но мы не можем сделать LinLZ Comonad потому что (например) из
LinLZ { subListCtxt = [], subList = [] }
мы не можем extract элемент (a от LinLZ a), только подсписок.
Контексты элемента списка
Контекст элемента списка - это пара списков: элементы перед элементом в фокусе и элементы после него. Контекст элемента в рекурсивной структуре всегда является парой: сначала задайте контекст подузла для подузла, в котором хранится элемент, а затем укажите контекст для элемента в его узле. Мы получаем контекст "элемент в своем узле", дифференцируя формулу для узла относительно переменной, которая обозначает элементы.
[a] = t where -- t is the recursive variable standing for [a]
t = 1 + a*t -- lists of a are either [] or an (a : t) pair
∂/∂a (1 + a*t) = t = [a] -- the context for the head element is the tail list
Таким образом, контекст элемента задается парой
type DL a =
( [a] -- the sublist context for the node where the element is
, [a] -- the tail of the node where the element is
)
и элемент застежка-молния задается путем сопряжения такого контекста с элементом "в дыре".
data ZL a = ZL
{ this :: a
, between :: DL a
} deriving (Show, Eq, Functor)
Вы можете превратить такую застежку-молнию обратно в список (выходя из элемента), сначала восстановив подсписок, в котором находится элемент, предоставив нам застежку-молнию подсписка, а затем вставив подсписок в его контекст подсписка.
outZL :: ZL a -> [a]
outZL (ZL { this = x, between = (zs, xs) })
= plugLinLZ (LinLZ { subListCtxt = zs, subList = x : xs })
Помещение каждого элемента в контекст
Учитывая список, мы можем связать каждый элемент с его контекстом. Мы получаем список способов, которыми мы можем "войти" в один из элементов. Мы начинаем так,
into :: [a] -> [ZL a]
into xs = moreInto (LinLZ { subListCtxt = [], subList = xs })
но настоящая работа выполняется вспомогательной функцией, которая работает со списком в контексте.
moreInto :: LinLZ a -> [ZL a]
moreInto (LinLZ { subListCtxt = _, subList = [] }) = []
moreInto (LinLZ { subListCtxt = zs, subList = x : xs })
= ZL { this = x, between = (zs, xs) }
: moreInto (LinLZ { subListCtxt = x : zs, subList = xs })
Обратите внимание, что вывод повторяет форму тока subList, Кроме того, молния в x место имеет this = x, Также генерирующая молния для украшения xs имеет subList = xs и правильный контекст, запись, что мы прошли мимо x, Тестирование,
into [1,2,3,4] =
[ ZL {this = 1, between = ([],[2,3,4])}
, ZL {this = 2, between = ([1],[3,4])}
, ZL {this = 3, between = ([2,1],[4])}
, ZL {this = 4, between = ([3,2,1],[])}
]
Комонадная структура для молний элементов списка
Мы видели, как выйти из элемента или в один из доступных элементов. Комонадная структура говорит нам, как перемещаться между элементами, оставаясь там, где мы находимся, или переходя к одному из других.
instance Comonad ZL where
extract дает нам элемент, который мы посещаем.
extract = this
к duplicate молнию, заменяем текущий элемент x со всей текущей молнией zl (чья this = x)...
duplicate zl@(ZL { this = x, between = (zs, ys) }) = ZL
{ this = zl
... и мы прорабатываем контекст, показывая, как перефокусироваться на каждом элементе. Наши существующие moreInto давайте двигаться внутрь, но мы также должны двигаться outward...
, between =
( outward (LinLZ { subListCtxt = zs, subList = x : ys })
, moreInto (LinLZ { subListCtxt = x : zs, subList = ys })
)
}
... который включает в себя путешествие назад по контексту, перемещение элементов в подсписок, следующим образом
where
outward (LinLZ { subListCtxt = [], subList = _ }) = []
outward (LinLZ { subListCtxt = z : zs, subList = ys })
= ZL { this = z, between = (zs, ys) }
: outward (LinLZ { subListCtxt = zs, subList = z : ys })
Итак, мы получаем
duplicate ZL {this = 2, between = ([1],[3,4])}
= ZL
{ this = ZL {this = 2, between = ([1],[3,4])}
, between =
( [ ZL {this = 1, between = ([],[2,3,4])} ]
, [ ZL {this = 3, between = ([2,1],[4])}
, ZL {this = 4, between = ([3,2,1],[])}
]
)
}
где this "пребывание в 2 "и мы between "переход к 1 "и" движется к 3 или переезд в 4 ".
Итак, comonadic структура показывает нам, как мы можем перемещаться между различными элементами, расположенными внутри списка. Структура подсписка играет ключевую роль в поиске узлов, где находятся элементы, но структура молнии duplicate d является молнией элемента.
Так что насчет деревьев?
Отступление: помеченные деревья уже являются комонадами
Позвольте мне провести рефакторинг вашего типа бинарных деревьев, чтобы выявить некоторую структуру. Буквально, давайте вытянем элемент, который маркирует лист или вилку как общий фактор. Давайте также выделим функтор (TF), которая объясняет эту структуру поддеревьев листьев или вилок.
data TF t = Leaf | Fork (t, t) deriving (Show, Eq, Functor)
data BT a = a :& TF (BT a) deriving (Show, Eq, Functor)
То есть каждый узел дерева имеет метку, будь то лист или ветвь.
Везде, где у нас есть структура, в которой каждый узел имеет метку и блоб субструктур, у нас есть комонада: cofree comonad. Позвольте мне немного изменить рефакторинг TF...
data CoFree f a = a :& f (CoFree f a) deriving (Functor)
... так что у нас есть общее f где мы имели TF до. Мы можем восстановить наши конкретные деревья.
data TF t = Leaf | Fork (t, t) deriving (Show, Eq, Functor)
type BT = CoFree TF
deriving instance Show a => Show (BT a)
deriving instance Eq a => Eq (BT a)
И теперь, раз и навсегда, мы можем дать бесплатную конструкцию комонады. Поскольку каждое поддерево имеет корневой элемент, каждый элемент может быть украшен деревом, корнем которого он является.
instance Functor f => Comonad (CoFree f) where
extract (a :& _) = a -- extract root element
duplicate t@(a :& ft) = t :& fmap duplicate ft -- replace root element by whole tree
Давайте иметь пример
aTree =
0 :& Fork
( 1 :& Fork
( 2 :& Leaf
, 3 :& Leaf
)
, 4 :& Leaf
)
duplicate aTree =
(0 :& Fork (1 :& Fork (2 :& Leaf,3 :& Leaf),4 :& Leaf)) :& Fork
( (1 :& Fork (2 :& Leaf,3 :& Leaf)) :& Fork
( (2 :& Leaf) :& Leaf
, (3 :& Leaf) :& Leaf
)
, (4 :& Leaf) :& Leaf
)
Увидеть? Каждый элемент был связан с его поддеревом!
Списки не дают начало свободной комонаде, потому что не каждый узел имеет элемент: в частности, [] не имеет элемента. В cofree comonad всегда есть элемент, где вы находитесь, и вы можете видеть дальше в древовидную структуру, но не дальше.
В элементе zipper comonad всегда есть элемент, где вы находитесь, и вы можете видеть как вверх, так и вниз.
Контексты поддеревьев и элементов в бинарных деревьях
Алгебраически
d/dt (TF t) = d/dt (1 + t*t) = 0 + (1*t + t*1)
поэтому мы можем определить
type DTF t = Either ((), t) (t, ())
говоря, что поддерево внутри "сгустка субструктур" находится либо слева, либо справа. Мы можем проверить, что "подключение" работает.
plugF :: t -> DTF t -> TF t
plugF t (Left ((), r)) = Fork (t, r)
plugF t (Right (l, ())) = Fork (l, t)
Если мы создаем t и в паре с меткой узла, мы получаем один шаг контекста поддерева
type BTStep a = (a, DTF (BT a))
который изоморфен Partial в вопросе.
plugBTinBT :: BT a -> BTStep a -> BT a
plugBTinBT t (a, d) = a :& plugF t d
Итак, поддерево -контекст для одного BT a внутри другого дается [BTStep a],
Но как насчет элемента контекста? Итак, каждый элемент помечает некоторое поддерево, поэтому мы должны записать как контекст этого поддерева, так и остальную часть дерева, помеченного этим элементом.
data DBT a = DBT
{ below :: TF (BT a) -- the rest of the element's node
, above :: [BTStep a] -- the subtree context of the element's node
} deriving (Show, Eq)
Досадно, я должен свернуть свой собственный Functor пример.
instance Functor DBT where
fmap f (DBT { above = a, below = b }) = DBT
{ below = fmap (fmap f) b
, above = fmap (f *** (either
(Left . (id *** fmap f))
(Right . (fmap f *** id)))) a
}
Теперь я могу сказать, что такое молния элемента.
data BTZ a = BTZ
{ here :: a
, ctxt :: DBT a
} deriving (Show, Eq, Functor)
Если вы думаете "что нового?", Вы правы. У нас есть контекст поддерева, above вместе с поддеревом, данным here а также below, И это потому, что единственными элементами являются те, которые помечают узлы. Разделение узла на элемент и его контекст - это то же самое, что разделение узла на его метку и блоб субструктур. То есть мы получим это совпадение для cofree comonads, но не в целом.
Однако это совпадение только отвлекает! Как мы видели со списками, нам не нужно, чтобы элементы-молнии были такими же, как subnode-zippers, чтобы элементы-молнии были комонадой.
Следуя тому же шаблону, что и списки выше, мы можем украсить каждый элемент его контекстом. Работа выполняется вспомогательной функцией, которая накапливает контекст поддерева, который мы сейчас посещаем.
down :: BT a -> BT (BTZ a)
down t = downIn t []
downIn :: BT a -> [BTStep a] -> BT (BTZ a)
downIn (a :& ft) ads =
BTZ { here = a, ctxt = DBT { below = ft, above = ads } }
:& furtherIn a ft ads
Обратите внимание, что a заменяется на молнию, ориентированную на a, Поддеревья обрабатываются другим помощником.
furtherIn :: a -> TF (BT a) -> [BTStep a] -> TF (BT (BTZ a))
furtherIn a Leaf ads = Leaf
furtherIn a (Fork (l, r)) ads = Fork
( downIn l ((a, Left ((), r)) : ads)
, downIn r ((a, Right (l, ())) : ads)
)
Видеть, что furtherIn сохраняет древовидную структуру, но соответствующим образом расширяет контекст поддерева, когда он посещает поддерево.
Давайте перепроверим.
down aTree =
BTZ { here = 0, ctxt = DBT {
below = Fork (1 :& Fork (2 :& Leaf,3 :& Leaf),4 :& Leaf),
above = []}} :& Fork
( BTZ { here = 1, ctxt = DBT {
below = Fork (2 :& Leaf,3 :& Leaf),
above = [(0,Left ((),4 :& Leaf))]}} :& Fork
( BTZ { here = 2, ctxt = DBT {
below = Leaf,
above = [(1,Left ((),3 :& Leaf)),(0,Left ((),4 :& Leaf))]}} :& Leaf
, BTZ { here = 3, ctxt = DBT {
below = Leaf,
above = [(1,Right (2 :& Leaf,())),(0,Left ((),4 :& Leaf))]}} :& Leaf
)
, BTZ { here = 4, ctxt = DBT {
below = Leaf,
above = [(0,Right (1 :& Fork (2 :& Leaf,3 :& Leaf),()))]}} :& Leaf)
Увидеть? Каждый элемент украшен своим контекстом, а не только деревом под ним.
Бинарные молнии из дерева образуют Comonad
Теперь, когда мы можем украшать элементы их контекстами, давайте создадим Comonad пример. Как прежде...
instance Comonad BTZ where
extract = here
... extract говорит нам об элементе в фокусе, и мы можем использовать наше существующее оборудование, чтобы идти дальше в дерево, но нам нужно создать новый комплект, чтобы исследовать способы, которыми мы можем двигаться наружу.
duplicate z@(BTZ { here = a, ctxt = DBT { below = ft, above = ads }}) = BTZ
{ here = z
, ctxt = DBT
{ below = furtherIn a ft ads -- move somewhere below a
, above = go_a (a :& ft) ads -- go above a
}
} where
Чтобы выйти наружу, как со списками, мы должны вернуться по пути к корню. Как и в случае со списками, каждый шаг на пути - это место, которое мы можем посетить.
go_a t [] = []
go_a t (ad : ads) = go_ad t ad ads : go_a (plugBTinBT t ad) ads
go_ad t (a, d) ads =
( BTZ { here = a, ctxt = DBT { below = plugF t d, above = ads } } -- visit here
, go_d t a d ads -- try other subtree
)
В отличие от списков, на этом пути есть альтернативные ветви для изучения. Везде, где путь хранит невидимое поддерево, мы должны украшать его элементы их контекстами.
go_d t a (Left ((), r)) ads = Left ((), downIn r ((a, Right (t, ())) : ads))
go_d t a (Right (l, ())) ads = Right (downIn l ((a, Left ((), t)) : ads), ())
Итак, теперь мы объяснили, как перефокусироваться с любой позиции элемента на любую другую.
Посмотрим. Здесь мы были в гостях 1:
duplicate (BTZ {here = 1, ctxt = DBT {
below = Fork (2 :& Leaf,3 :& Leaf),
above = [(0,Left ((),4 :& Leaf))]}}) =
BTZ {here = BTZ {here = 1, ctxt = DBT {
below = Fork (2 :& Leaf,3 :& Leaf),
above = [(0,Left ((),4 :& Leaf))]}}, ctxt = DBT {
below = Fork (BTZ {here = 2, ctxt = DBT {
below = Leaf,
above = [(1,Left ((),3 :& Leaf)),(0,Left ((),4 :& Leaf))]}} :& Leaf
,BTZ {here = 3, ctxt = DBT {
below = Leaf,
above = [(1,Right (2 :& Leaf,())),(0,Left ((),4 :& Leaf))]}} :& Leaf
),
above = [(BTZ {here = 0, ctxt = DBT {
below = Fork (1 :& Fork (2 :& Leaf,3 :& Leaf),4 :& Leaf),
above = []}}
,Left ((),BTZ {here = 4, ctxt = DBT {
below = Leaf,
above = [(0,Right (1 :& Fork (2 :& Leaf,3 :& Leaf),()))]}} :& Leaf)
)
]}}
Чтобы проверить законы комонад на небольшой выборке данных, давайте проверим:
fmap (\ z -> extract (duplicate z) == z) (down aTree)
= True :& Fork (True :& Fork (True :& Leaf,True :& Leaf),True :& Leaf)
fmap (\ z -> fmap extract (duplicate z) == z) (down aTree)
= True :& Fork (True :& Fork (True :& Leaf,True :& Leaf),True :& Leaf)
fmap (\ z -> fmap duplicate (duplicate z) == duplicate (duplicate z)) (down aTree)
= True :& Fork (True :& Fork (True :& Leaf,True :& Leaf),True :& Leaf)