Однопроходная линзы для корня сбалансированного бинарного дерева

Question

У меня есть сбалансированное бинарное дерево, которое включает в себя глубину этого дерева в своем роде:

data Nat = Zero | Succ Nat 
data Tree (n :: Nat) a where 
    Leaf :: Tree Zero a 
    Branch :: a -> (Tree n a, Tree n a) -> Tree (Succ n) a 

я хотел бы способ запуска произвольных функций f :: Tree n a -> Tree n a на поддереве глубины n в корне любых Tree m a, m ≥ n.

я был в состоянии осуществить это один из способов, используя класс типа для извлечения и замены корневой поддерево:

mapRoot :: X m n => (Tree n a -> Tree n a) -> Tree m a -> Tree m a 
mapRoot f t = putRoot (f (getRoot t)) t 

class X m n where 
    getRoot :: Tree m a -> Tree n a 
    putRoot :: Tree n a -> Tree m a -> Tree m a 

instance X m Zero where 
    getRoot t = Leaf 
    putRoot Leaf t = t 

instance X m n => X (Succ m) (Succ n) where 
    getRoot (Branch a (l,r)) = (Branch a (getRoot l, getRoot r)) 
    putRoot (Branch a (l,r)) (Branch _ (l',r')) = Branch a (putRoot l l', putRoot r r') 

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

Это почти возможно с помощью ленивых вычислений (обвязок узла):

mapRoot' :: Y m n => (Tree n a -> Tree n a) -> Tree m a -> Tree m a 
mapRoot' f t = t' where 
    (r, t') = swapRoot t r' 
    r' = f r 

class Y m n where 
    swapRoot :: (Tree m a, Tree n a) -> (Tree n a, Tree m a) 

instance Y m Zero where 
    swapRoot t leaf = (leaf, t) 

instance Y m n => Y (Succ m) (Succ n) where 
    swapRoot (Branch a (l,r)) (Branch a' (l',r')) = (Branch a (lx,rx), Branch a' (lx',rx')) where 
    (lx,lx') = swapRoot l l' 
    (rx,rx') = swapRoot r r' 

Но если вы на самом деле пытаетесь запустить mapRoot' вы обнаружите, что он не останавливается; это потому, что swapRoot не является ленивым в своем втором аргументе (чего не может быть, потому что Tree n a - это GADT).

Однако, учитывая getRoot и putRoot, у меня в объектив для корневого поддерева, что приводит меня подозревать, что есть другие, в том числе тот, который может быть использован для реализации mapRoot в один проход.

Что такое такой объектив?

Answer 1

Ваш подход «привязать узел» звучит - вам нужны все параметры в нужном месте, поэтому функция может быть достаточно ленивой.

data (:<=) (n :: Nat) (m :: Nat) where 
    LTEQ_0 :: 'Zero :<= n 
    LTEQ_Succ :: !(n :<= m) -> 'Succ n :<= 'Succ m 

mapRoot :: n :<= m -> (Tree n a -> Tree n a) -> Tree m a -> Tree m a 
mapRoot p0 f0 t0 = restore (f0 root) where 
    (root, restore) = go p0 t0 

    go :: n :<= m -> Tree m a -> (Tree n a, Tree n a -> Tree m a) 
    go LTEQ_0 t = (Leaf, const t) 
    go (LTEQ_Succ p) (Branch a (l,r)) = 
    case (go p l, go p r) of 
     ((l', fl), (r', fr)) -> 
     (Branch a (l', r') 
     , \(Branch a1 (l1, r1)) -> Branch a1 (fl l1, fr r1) 
     ) 

go Обратите внимание, что возвращает пары - корень дерева, а функция принимает обработанный корень и возвращает результат. Это делает его явным (для programmar и runtime!), Что результат Tree n a не зависит от ввода Tree n a.

Кроме того, я заменил ваш класс GADT только для краткости.