haskell - 用于平衡二叉树根的单通透镜

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

我想要一种在任何 根部深度 n 的子树上运行任意函数 f::Tree n a -> Tree n a 的方法树 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 返回一对 - 根树，以及一个获取处理后的根并返回结果的函数。这使得(对程序和运行时!)结果 Tree n a 不依赖于输入 Tree n a 。

此外，为了简洁起见，我已将您的类(class)替换为 GADT。