如何使二叉树拉链成为 Comonad 的实例？

Question

我想让二叉树拉链成为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 的实例？ 如果答案是肯定的，那么我的方法有问题吗？

Answer 1

在微积分中，莱布尼茨的符号比牛顿的符号引起的混乱更少，因为它明确了我们区分的变量。事物中的语境是由微分给出的，所以我们必须注意被语境化的东西。在这里，有两个“子结构”概念在起作用：子树和元素。它们每个都有不同（但相关）的“上下文”概念，因此也有“拉链”的概念，其中拉链是事物及其上下文的对。

您的BTZ 类型被表示为子树 的拉链概念。然而，对于 elements，zipper comonadic 构造适用于 zippers：extract 表示“在此处提供元素”； duplicate 的意思是“用它的上下文装饰每个元素”。所以你需要元素上下文。令人困惑的是，对于这些二叉树，元素 zippers 和子树 zippers 是同构的，但这是出于一个非常特殊的原因（即它们形成了一个 cofree 共单子）。

通常，元素拉链和子树拉链不同，例如，对于列表。如果我们从为列表构建 element-zipper comonad 开始，当我们回到树时，我们不太可能迷路。让我也尝试为他人和您自己填写更多的总体情况。

子列表上下文

[a] 的 子列表-上下文由 [a] 给出，是我们在从子列表到整个列表的途中经过的元素列表。 [1,2,3,4] 中 [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

所以 sublist-zipper 是一对

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 一个元素（来自LinLZ a 的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
  )

并且通过将这样的上下文与“in the hole”元素配对来给出一个元素拉链。

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],[])}
  ]

列表元素拉链的单子结构

我们已经看到了如何从一个元素出来，或者进入一个可用的元素。 comonadic 结构告诉我们如何在元素之间移动，要么留在原地，要么移动到其他元素之一。

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 结构向我们展示了如何在列表内的不同 元素 之间移动。子列表结构在查找元素所在的节点中起着关键作用，但拉链结构duplicated 是一个元素拉链。

那么树呢？

题外话：标记的树已经是共生体了

让我重构您的二叉树类型以显示一些结构。从字面上看，让我们将标记叶子或叉子的元素作为一个共同因素拉出来。让我们也分离出解释这种叶子或叉子树结构的函子 (TF)。

data TF t = Leaf | Fork (t, t) deriving (Show, Eq, Functor)
data BT a = a :& TF (BT a) deriving (Show, Eq, Functor)

也就是说，每个树节点都有一个标签，无论是叶子还是叉子。

只要我们有每个节点都有一个标签和一团子结构的结构，我们就有一个comonad：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)

现在，我们可以一劳永逸地进行 cofree 共体结构了。由于每个子树都有一个根元素，因此每个元素都可以用它所在的树来装饰。

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，因为不是每个节点都有一个元素：具体来说，[] 没有元素。在 cofree 共单子中，您所在的位置总有一个元素，您可以进一步看到树结构，但不能进一步向上。

在一个元素拉链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] 给出。

但是 element 上下文呢？好吧，每个元素都标记了某个子树，因此我们应该记录该子树的上下文以及该元素标记的树的其余部分。

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的这种巧合，但不是一般的。

然而，这种巧合只是一种干扰！正如我们在列表中看到的那样，我们不需要 element-zippers 与 subnode-zippers 相同来使 element-zippers 成为一个comonad。

按照与上面列表相同的模式，我们可以用它的上下文来装饰每个元素。这项工作由一个辅助函数完成，该函数累积我们当前正在访问的子树上下文。

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
      )

与列表不同，沿着这条路径可以探索其他分支。无论路径存储未访问的子树，我们都必须用 它们的 上下文来装饰 its 元素。

    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)