如何使一个二叉树拉链一个Comonad的实例？ [英] How to make a binary tree zipper an instance of Comonad?

问题描述

我想创建一个二叉树拉链作为comonad的一个实例，但我无法弄清楚如何正确实现 duplicate 。

以下是我的尝试：

  { - ＃LANGUAGE DeriveFunctor＃ - } 
 import Data 。功能
导入Control.Arrow 
导入Control.Comonad 
 
数据BinTree a 
 = Leaf a 
 |分支a（BinTree a）（BinTree a）
派生（Functor，Show，Eq）
 
 data Dir = L | R 
导出（Show，Eq）
 
  - 一个不完整的二叉树，aka数据上下文
数据部分a =缺少的目录（BinTree a）a 
导出（ Show，Eq，Functor）
 
  -  BTT for BinTree Zipper 
 newtype BTZ a = BTZ {getBTZ ::（[Partial a]，BinTree a）} 
 deriving（Show ，公式）
 
实例Functor BTZ其中
 fmap f（BTZ（cs，t））= BTZ（map（fmap f）cs，fmap ft）
 
 -  |用拉链聚焦在该节点上替换每个节点标签
 dup :: BinTree a  - > BinTree（BTZ a）
 dup（Leaf v）= Leaf（BTZ（[]，Leaf v））
 dup t @（Branch v tl tr）=分支（BTZ（[]，t）） tlZ trZ 
其中
 tlZ = fmap（BTZ。first（++ [Missing L tr v]）。getBTZ）（dup tl）
 trZ = fmap（BTZ。first（++ [ Missing R tl v]）。getBTZ）（dup tr）
 
  -  |提取根标签
 rootVal :: BinTree a  - > a 
 rootVal（Leaf v）= v 
 rootVal（Branch v _ _）= v 
 
  -  |在
附近移动拉链焦点goUp，goLeft，goRight :: BTZ a  - > BTZ a 
 
 goUp（BTZ（[]，_））=错误已在根目录
 goUp（BTZ（缺失wt t2 v：xs，t1））= b $ b 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 _  - >错误已经在叶子上
 Branch v t1 t2  - > BTZ（Missing L t2 v：cs，t1）
 
 goRight z = let（cs，t）= getBTZ z in 
 case t of 
 Leaf _  - >错误已经在叶子上
 Branch v t1 t2  - > BTZ（缺失R t1 v：cs，t2）
 
实例Comonad BTZ其中
提取（BTZ（_，t））= 
案例t 
 Leaf v - > v 
分支v _ _  - > v 
 
重复z @（BTZ（cs，bt））= b 
 Leaf _  - > BTZ（csZ，Leaf z） - 提取物。 duplicate = id 
 Branch v tl tr  - > 
  - 对于每个子树，使用dup构建拉链，
  - 并将当前聚焦根（bt）和其余数据上下文附加到它
 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）
在BTZ（csZ，Branch z tlZ trZ）
其中
  - 上升并重复，我们将有一个BTZ（BTZ a）
  - 我们可以从中抓住[Partial（BTZ a）]out 
  -  TODO：不知道它是否有效
 upZippers = take（长度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 是二叉树数据类型，每个树节点包含。
  
• 部分a 是一个具有左或右子树的二叉树。在我的代码中，一堆部分a
  起着数据上下文的作用。 代表 BinTree 拉链，我想制作一个 Comonad 的实例，它由数据上下文和聚焦子树组成。

使它成为 Comonad的一个实例，我的计划是实现解压缩和重复，并通过采取一些随机验证comonad属性是否成立二进制树。

摘录很简单，只需将聚焦子树取出即可。

函数 dup 作为辅助函数，用每个节点标签
替换为集中在该节点上的树形拉链。

对于重复的z ，节点标签本身必须是 z ，那提取。重复== id 成立。对于非叶节点，我使用 dup 来处理它们的子树，就好像它们没有父节点一样，当前焦点 z


到目前为止，前两个comonad属性都满足了（ extract）。重复= id 和 fmap提取。duplicate ），但我不知道如何处理数据上下文。我目前正在做的是拉动 z 并继续上涨。一路走来，我们将每个数据上下文堆栈的顶部构建为新的数据上下文堆栈，这听起来正确并且是正确的类型（ [Partial（BTZ a）]


给定二叉树拉链的数据类型定义，
有可能使它成为一个comonad的实例？
如果答案是肯定的，我的方法有什么问题吗？


解决方案

演算中，莱布尼兹的符号比牛顿的描述引起的混淆更少，因为它明确地说明了我们区分的变量，事物的上下文是通过区分给出的，所以我们必须注意被上下文化的东西。 在工作中：子树和元素。它们每个都有不同的（但相关的）上下文和拉链的概念，拉链是一对事物及其上下文。

您的 BTZ 类型表示为子树的拉链的概念。但是，zipper comonadic构造在元素的拉链上工作： extract 意思是给元素在这里; duplicate 意思是用它的上下文装饰每个元素。所以你需要元素上下文。令人困惑的是，对于这些二叉树，元素拉链和子树拉链是同构的，但这是一个非常特殊的原因（即它们形成一个cofree comonad）。

通常，元素和子树拉链的不同，例如列表。如果我们开始为列表构建元素 - 拉链的comonad，那么当我们回到树上时，我们不太可能迷路。让我尝试为其他人以及你自己填充一些总体情况。

子列表上下文

c>，它是我们从子列表出发到整个列表的路径中传递的元素的列表。 [1,2,3,4] 中的 [3,4] 的子列表上下文为 [2,1] 。递归数据的子节点上下文始终是列表，表示您在从节点到根的路径中看到的内容。每一步的类型由相对于递归变量的一个数据节点的公式的偏导数给出。所以这里

  [a] = t其中 -  t是代表[a] 
t = 1的递归变量+ a * t  -  a的列表可以是[]或（a：t）对
∂/∂t（1 + a * t）= a  - 这是从节点到根的路径上的一个步骤
子列表上下文是[a]  - 这样的步骤列表
  

拉链是一对

 数据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}）
  

但是我们不能让<$ c因为（例如）来自

 LinLZ  a  Comonad  >  LinLZ {subListCtxt = []，subList = []} 
  

我们可以从 LinLZ a（ a ）提取 an 元素

列表元素上下文

列表元素上下文是一对列表：元素在焦点之前的元素，以及元素之后的元素。递归结构中的元素上下文始终是一对：首先为存储元素的子节点指定子节点上下文，然后为其节点中的元素指定上下文。我们通过将节点的公式与表示元素的变量相区别来获得节点中的元素。

 t = 1 + a * t的递归变量 -  a的列表是[]或（a：t）对
 /∂a（1 + a * t）= t = [a]  -  head元素的上下文是尾部列表
  

所以元素上下文是由一对元素给出的

 类型DL a = 
 （[a]  - 元素为
的节点的子列表上下文，[a]  - 元素为
的节点的尾部）
  

并且元素拉链是通过将这样的上下文与元素在洞中配对而给出的。

 数据ZL a = ZL 
 {this :: a 
，介于:: DL a 
}派生（Show，Eq，Functor） 
  

你可以将这样一个拉链变成一个列表（去通过首先重构元素所在的子列表，给我们一个子列表拉链，然后将子列表插入到它的子列表上下文中。

  outZL :: ZL a  - > [b] 
 outZL（ZL {this = x，between =（zs，xs）}）
 = plugLinLZ（LinLZ {subListCtxt = zs，subList = x：xs}）
  





将每个元素放到上下文中

给定一个列表，每个元素都有其上下文。我们列出了我们可以进入其中一个要素的方式。我们就这样开始，

  into :: [a]  - > [ZL a] 
到xs = moreInto（LinLZ {subListCtxt = []，subList = xs}）
  

$ p
pre $ moreInto：b

但实际的工作是通过辅助函数完成的， ：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 。测试，

 到[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其中
  

摘录给了我们元素我们正在访问。

  extract = this 
  

为了 duplicate 一个拉链，我们用当前元素 x 替换为整个当前的拉链 zl （其中 this = x ）...

  duplicate zl @（ZL {this = x，between =（zs，ys）}）= ZL 
 {this = zl 
  

...我们通过上下文工作，展示如何重新聚焦每个元素。我们现有的 moreInto 可让我们向内移动，但我们还必须将向外移动 ...

 ，介于= 
（向外（LinLZ {subListCtxt = zs，subList = x：ys}）
，moreInto（LinLZ {subListCtxt = x：zs，subList = ys}）
）
} 
  

..其中涉及沿着上下文返回，将元素移动到子列表中，如下所示：

 其中
向外（LinLZ {subListCtxt = []，subList = _}）= [] 
（LinLZ {subListCtxt = z：zs，subList = ys}）
 = ZL {this = z，between =（zs，ys ）} 
：向外（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 ，介于=（[]，[2,3,4]）} ] = {[2,1]，[4]）} 
，[ZL {this = 3，between = ]）} 
] 
）
} 
  

<$>其中 是住在 2 ，我们< 移动至 1 和移至 3 或移至 4 。

所以，这个结构向我们展示了如何在列表中的不同元素之间移动。子列表结构在查找元素所在的节点中起着关键作用，但是拉链结构 duplicate d是一个元素拉链。

那么树呢？

Digression：已标记的树木已经是comonads

让我重构你的二叉树的类型以带出一些结构。从字面上看，让我们把标注叶子或叉子的元素作为一个公共因素拉出来。让我们也分离出解释这个叶或叉子树结构的函子（ TF ）。

  data TF t = Leaf | Fork（t，t）派生（Show，Eq，Functor）
数据BT a = a：& TF（BT a）派生（Show，Eq，Functor）
  

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

无论我们有哪种结构，每个节点都有一个标签和一个子结构，我们有一个comonad： em> cofree comonad 。让我重构一下，抽象出 TF ...

 数据CoFree fa = a：& f（CoFree fa）派生（Functor）
  

...所以我们有一个普通的 f 之前我们有 TF 。我们可以恢复我们的特定树木。

  data TF t = Leaf | Fork（t，t）派生（Show，Eq，Functor）
类型BT = CoFree TF 
派生实例Show a =>显示（BT a）
导出实例Eq a =>公式（BT a）
  

现在，我们可以一次性完成cofree comonad的构建。由于每个子树都有一个根元素，所以每个元素都可以用其根目录树来修饰。

 实例Functor f => ; Comonad（CoFree f）其中
提取（a：& _）= a  - 提取根元素
重复t @（a：& ft）= t：& fmap duplicate ft  - 用整棵树替换根元素
  

让我们举个例子吧

  aTree = 
 0：&分叉
（1：& Fork 
（2：& Leaf 
，3：&Leaf 
）
，4：&Leaf 
 ）
 
重复aTree = 
（0：& Fork（1：&Fork（2：& Leaf，3：&Leaf），4：&Leaf））： &安培;分叉
（（1：&Fork（2：& Leaf，3：& Leaf））：& Fork 
（（2：& Leaf）：& Leaf 
 ，（3：& Leaf）：& Leaf 
）
，（4：& Leaf）：& Leaf 
）
  

请参阅？每个元素都与它的子树配对！

列表不引起cofree comonad，因为不是每个节点都有一个元素：具体地说， [] 没有元素。在cofree comonad中，总是存在一个元素，你可以进一步看到树结构，，但不能继续向上。

在一个元素拉链comonad中，总是存在一个元素，你可以同时看到它。

子树和二元树中的元素上下文

代数
$ b $ $ p $ d / dt（TF t）= d / dt（1 + t * t）= 0+（1 * t + t * 1）


$ b $因此我们可以定义

 类型DTF t =（（），t）（t，（））
  

表示子结构块内的子树不是在左边就是在右边。我们可以检查插入工作。

  plugF :: t  - > DTF t  - > TF t 
 plugF t（Left（（），r））=叉（t，r）
 plugF t（右（l，（）））=叉（l，t）
  

如果我们实例化 t 并与节点标签配对， （a，DTF（BT a））

 类型BTStep a = code> 

与问题中的 Partial 同构。

  plugBTinBT :: BT a  - > BTS步骤a  - > BT a 
 plugBTinBT t（a，d）= a：&因此，对于一个<$ c $的子树  - 上下文c> BT a 在另一个里面是由 [BTStep a] 。
 
 
 
给出关于元素的上下文呢？那么，每个元素都会标记一个子树，所以我们应该记录该子树的上下文和该元素标记的树的其余部分。 
 
 
  data DBT a = DBT 
 {below :: TF（BT a） - 元素节点的其余部分
，高于:: [BTStep a]  - 元素节点的子树上下文
 
 
 
 
 
 $ b 
令人烦恼的是，我不得不将自己的 Functor  instance。
  instance Functor DBT其中
 fmap f（DBT {above = a，below = b}）= DBT 
 {below = fmap（fmap f）b 
，above = fmap（f ***（
（Left。（id *** fmap f））
（Right。（fmap f *** id））））a 
} 
  
现在我可以说一个元素拉链。 
 
 
  data BTZ a = BTZ 
 {here :: a 
，ctxt :: DBT a 
}派生（Show，Eq，Functor）
  
如果你是呃想着什么是新的？，你是对的。我们有一个子树上下文，大于，连同由给出的子树和在。那是因为唯一的元素是标签节点。 
将一个节点分割成一个元素及其上下文与将其分割成其标签及其子结构的块相同。也就是说，我们得到了cofree comonads的这个巧合，但并不普遍。 
 
 
然而，这个巧合只是一种分心！正如我们在列表中看到的那样，我们不需要元素拉链就像子节点拉链一样使元素拉链成为一个comonad。
 
 
 
遵循与上面列出，我们可以用它的上下文来装饰每个元素。这项工作是由一个辅助函数完成的，该辅助函数累积了我们目前正在访问的子树上下文。
  down :: BT a  - > BT（BTZ a）
 down t = downIn t [] 
 
 downIn :: BT a  - > [BTS步骤a]  - > BT（BTZ a）
 downIn（a：& ft）ads = 
 BTZ {here = a，ctxt = DBT {below = ft，above = ads}} 
：&进一步在英尺广告
  
请注意 a 是取而代之的是一个侧重于 a 的拉链。子树由另一个助手处理。
  furtherIn :: a  - > TF（BT a） - > [BTS步骤a]  - > TF（BT（BTZ a））
 further in a leaf ads = Leaf 
 further in a（Fork（l，r））ads = Fork 
（downIn l（（a，Left（（） （（a，Right（l，（）））：ads）
）
  
看到 furtherIn 保留树结构，但在访问子树时适当增大子树上下文。
 
 
 
让我们仔细检查。
  down aTree = 
 BTZ {here = 0，ctxt = DBT {
低于= Fork（1：& Fork（2：& Leaf，3：&Leaf），4：&Leaf），
 above = []}} ：放大器; Fork 
（BTZ {here = 1，ctxt = DBT {
低于= 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 {
低于= Leaf，
高于= [（1，Right（2：& Leaf，（））），（0，Left（（），4：& Leaf））]}}：& amp ; Leaf 
）
 BTZ {here = 4，ctxt = DBT {
 below = Leaf，
 above = [（0，Right（1：&Fork & Leaf，3：& Leaf），（）））]}}：& Leaf）
  
看到了吗？每个元素都用整个上下文进行装饰，而不仅仅是它下面的树。
 
 
 
二叉树拉链组成一个Comonad 
 
 
 <现在我们可以用它们的上下文来装饰元素，让我们来构建 Comonad 实例。和以前一样...... 
 
 $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ > 
 ... 提取告诉我们关注的元素，我们可以利用我们的现有的机器进一步进入树，但我们需要建立新的工具包，探索我们可以向外移动的方式。 
 
 
  duplicate z @（BTZ {here = a，ctxt = DBT {below = ft，above = ads}}）= BTZ 
 {here = z 
，ctxt = DBT 
 {below = furtherIn英尺广告 - 移到某个地方，低于
，高于= go_a（a：& ft）广告 - 高于
} 
}，其中
  
要像列表一样向外走，我们必须沿着朝向根的路径前进。与列表一样，路径上的每一步都是我们可以访问的地方。
  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 td，above = ads}}  -  visit here 
，go_d tad ads  - 尝试其他子树
）
  
与列表不同，沿着该路径有其他分支可供探索。无论路径存储了一个未访问的子树，我们都必须用它们的上下文来修饰元素。
  go_d ta（Left（（），r））ads = Left（（），downIn r（（a，Right（t，（）））：ads））
 go_d ta l，（）））ads = Right（downIn l（（a，Left（（），t））：ads），（））
  
所以现在我们已经解释了如何从任何元素位置重新聚焦到其他元素。
 
 
 
让我们来看看。这里我们访问 1 ： 
 
 
  duplicate（BTZ {here = 1 ，ctxt = DBT {
低于= Fork（2：& Leaf，3：& Leaf），
以上= [（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 {这里= 3，ctxt = DBT {
低于= Leaf，
高于= [（1，Right（2：& Leaf，（））），（0，Left（（），4： ; Leaf））]}}：& Leaf 
），
 above = [（BTZ {here = 0，ctxt = DBT {
 below = Fork（1：&Fork ：& Leaf，3：&am磷;叶），4：& （），BTZ {here = 4，ctxt = DBT {
 below = Leaf，
 above = [（0）），
 above = []}} 
， ，右（1：&Fork（2：& Leaf，3：& Leaf），（）））]}}：& Leaf）
）
]}} 
  
通过测试少量样本数据的共同定律，让我们检查：
 
 
  fmap（\ z  - > extract（duplicate z）== z）（down a Tree）
 = 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 a Tree）
 = True：& Fork（True：&Fork（True：& Leaf，True：&Leaf），True：&Leaf）
  
 
I want to make a binary tree zipper an instance of comonad, but I can't figure out how to implement duplicate properly.


Here is my attempt:
{-# 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)
Some explanation:


BinTree a is the binary tree data type and each tree node contains a label.
Partial a is a binary tree with either left or right subtree. A stack of Partial a
in my code plays the role of data context.
BTZ stands for the BinTree zipper, which I want to make an instance of Comonad, it consists of a data context and the focusing subtree.


To make it an instance of Comonad, my plan is to implement extract and duplicate, and verify if the comonad properties hold by taking some random binary trees.

The extract is straightforward, just taking the focusing subtree out.

Function dup serves as an auxiliary function that replaces each node label
with the tree zipper focusing on that node.

For duplicate z, the node label needs to be z itself so that extract . duplicate == id holds. For non-leaf nodes, I use dup to deal with their subtrees as if they have no parents, and the current focus of z and the rest of the data context gets appended to these zippers afterwards.

So far the first two comonad properties are satisfied (extract . duplicate = id and fmap extract . duplicate), but I have no idea what to do with the data context. What I currently do is taking the zipper z and keep going up. Along the way we take the top of each data context stack to build the new data context stack, which sounds right to be and also is of the correct type ([Partial (BTZ a)]. But my approach cannot satisfy the third law.

Given the data type definition of binary tree zipper above,
is it possible to make it an instance of Comonad?
If the answer is yes, is there something wrong with my approach?
解决方案
In the differential calculus, Leibniz's notation causes less confusion than Newton's because it is explicit about the variable with respect to which we differentiate. Contexts in things are given by differentiation, so we must take care what is being contextualized. Here, there are two notions of "substructure" at work: subtrees and elements. They each have different (but related) notions of "context" and hence of "zipper", where a zipper is the pair of a thing and its context.

Your BTZ type is presented as the notion of zipper for subtrees. However, the zipper comonadic construction works on zippers for elements: extract means "give element here"; duplicate means "decorate each element with its context". So you need element contexts. Confusingly, for these binary trees, element zippers and subtree zippers are isomorphic, but that is for a very particular reason (namely that they form a cofree comonad).

Generally, element- and subtree-zippers differ, e.g., for lists. If we start by building the element-zipper comonad for lists, we are less likely to get lost when we come back to trees. Let me try also to fill in a bit more of the general picture, for others as well as yourself.

Sublist contexts

The sublist-contexts for [a] are just given by [a], being the list of elements we pass by on the way out from the sublist to the whole list. The sublist context for [3,4] in [1,2,3,4] is [2,1]. Subnode contexts for recursive data are always lists representing what you see on the path from the node to the root. The type of each step is given by the partial derivative of the formula for one node of data with respect to the recursive variable. So here
[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
So a sublist-zipper is a pair
data LinLZ a = LinLZ
  {  subListCtxt  :: [a]
  ,  subList      :: [a]
  }
We can write the function which plugs a sublist back into its context, reversing back up the path
plugLinLZ :: LinLZ a -> [a]
plugLinLZ (LinLZ { subListCtxt = [],      subList = ys})  = ys
plugLinLZ (LinLZ { subListCtxt = x : xs,  subList = ys})
  = plugLinLZ (LinLZ { subListCtxt = xs,  subList = x : ys})
But we can't make LinLZ a Comonad, because (for example) from
LinLZ { subListCtxt = [], subList = [] }
we can't extract an element (an a from LinLZ a), only a sublist.

List Element Contexts

A list element context is a pair of lists: the elements before the element in focus, and the elements after it. An element context in a recursive structure is always a pair: first give the subnode-context for the subnode where the element is stored, then give the context for the element in its node. We get the element-in-its-node context by differentiating the formula for a node with respect to the variable which stands for elements.
[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
So an element context is given by a pair
type DL a =
  (  [a]     -- the sublist context for the node where the element is
  ,  [a]     -- the tail of the node where the element is
  )
and an element zipper is given by pairing such a context with the element "in the hole".
data ZL a = ZL
  {  this :: a
  ,  between :: DL a
  }  deriving (Show, Eq, Functor)
You can turn such a zipper back into a list (going "out" from an element) by first reconstituting the sublist where the element sits, giving us a sublist zipper, then plugging the sublist into its sublist-context.
outZL :: ZL a -> [a]
outZL (ZL { this = x, between = (zs, xs) })
  = plugLinLZ (LinLZ { subListCtxt = zs, subList = x : xs })


Putting each element into context

Given a list, we can pair each element up with its context. We get the list of ways we can "go into" one of the elements. We start like this,
into :: [a] -> [ZL a]
into xs = moreInto (LinLZ { subListCtxt = [], subList = xs })
but the real work is done by the helper function which works on a list-in-context.
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 })
Notice that the output echoes the shape of the current subList. Also, the zipper in x's place has
this = x. Also, the generating zipper for decorating xs has subList = xs and the correct context,
recording that we have moved past x. Testing,
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 structure for list element zippers

We've seen how to go out from an element, or into one of the available elements. The comonadic structure tells us how to move between elements, either staying where we are, or moving to one of the others.
instance Comonad ZL where
The extract gives us the element we're visiting.
  extract = this
To duplicate a zipper, we replace the current element x with the whole current zipper zl (whose this = x)...
  duplicate zl@(ZL { this = x, between = (zs, ys) }) = ZL
    {  this = zl
...and we work our way through the context, showing how to refocus at each element. Our existing moreInto lets us move inward, but we must also move outward...
    ,  between =
         (  outward (LinLZ { subListCtxt = zs, subList = x : ys })
         ,  moreInto (LinLZ { subListCtxt = x : zs, subList = ys })
         )
    }
...which involves travelling back along the context, moving elements into the sublist, as follows
    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 })
So we get
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],[])}
        ]
     )
  }
where this is "staying at 2" and we are between "moving to 1" and "moving to 3 or moving to 4".

So, the comonadic structure shows us how we can move between different elements located inside a list. The sublist structure plays a key role in finding the nodes where the elements are, but the zipper structure duplicated is an element zipper.

So what about trees?

Digression: labelled trees are comonads already

Let me refactor your type of binary trees to bring out some structure. Literally, let us pull the element which labels a leaf or a fork out as a common factor. Let us also isolate the functor (TF) which explains this leaf-or-fork subtree structure.
data TF t = Leaf | Fork (t, t) deriving (Show, Eq, Functor)
data BT a = a :& TF (BT a) deriving (Show, Eq, Functor)
That is, every tree node has a label, whether it is a leaf or a fork.

Wherever we have the structure that every node has a label and a blob of substructures, we have a comonad: the cofree comonad. Let me refactor a little more, abstracting out TF...
data CoFree f a = a :& f (CoFree f a) deriving (Functor)
...so we have a general f where we had TF before. We can recover our specific trees.
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)
And now, once for all, we can give the cofree comonad construction. As every subtree has a root element, every element can be decorated with the tree whose root it is.
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
Let's have an example
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
  )
See? Each element has been paired with its subtree!

Lists do not give rise to a cofree comonad, because not every node has an element: specifically, [] has no element. In a cofree comonad, there is always an element where you are, and you can see further down into the tree structure, but not further up.

In an element zipper comonad, there is always an element where you are, and you can see both up and down.

Subtree and element contexts in binary trees

Algebraically
d/dt (TF t) = d/dt (1 + t*t) = 0 + (1*t + t*1)
so we may define
type DTF t = Either ((), t) (t, ())
saying that a subtree inside the "blob of substructures" is either on the left or the right. We can check that "plugging in" works.
plugF :: t -> DTF t -> TF t
plugF  t  (Left   ((), r))  = Fork (t, r)
plugF  t  (Right  (l, ()))  = Fork (l, t)
If we instantiate t and pair up with the node label, we get one step of subtree context
type BTStep a = (a, DTF (BT a))
which is isomorphic to Partial in the question.
plugBTinBT :: BT a -> BTStep a -> BT a
plugBTinBT t (a, d) = a :& plugF t d
So, a subtree-context for one BT a inside another is given by [BTStep a].

But what about an element context? Well, every element labels some subtree, so we should record both that subtree's context and the rest of the tree labelled by the 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)
Annoyingly, I have to roll my own Functor instance.
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  
    }
Now I can say what an element zipper is.
data BTZ a = BTZ
  {  here  :: a
  ,  ctxt  :: DBT a
  }  deriving (Show, Eq, Functor)
If you're thinking "what's new?", you're right. We have a subtree context, above, together with a subtree given by here and below. And that's because the only elements are those which label nodes.
Splitting a node up into an element and its context is the same as splitting it into its label and its blob of substructures. That is, we get this coincidence for cofree comonads, but not in general.

However, this coincidence is only a distraction! As we saw with lists, we don't need element-zippers to be the same as subnode-zippers to make element-zippers a comonad.

Following the same pattern as lists above, we can decorate every element with its context. The work is done by a helper function which accumulates the subtree context we are currently visiting.
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
Note that a is replaced by a zipper focused on a. The subtrees are handled by another helper.
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)
  )
See that furtherIn preserves the tree structure, but grows the subtree context suitably when it visits a subtree.

Let's double check.
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)
See? Each element is decorated with its whole context, not just the tree below it.

Binary tree zippers form a Comonad

Now that we can decorate elements with their contexts, let us build the Comonad instance. As before...
instance Comonad BTZ where
  extract = here
...extract tells us the element in focus, and we can make use of our existing machinery to go further into the tree, but we need to build new kit to explore the ways we can move outwards.
  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
To go outwards, as with lists, we must move back along the path towards the root. As with lists, each step on the path is a place we can visit.
    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
      )
Unlike with lists, there are alternative branches along that path to explore. Wherever the path stores an unvisited subtree, we must decorate its elements with their contexts.
    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), ())
So now we've explained how to refocus from any element position to any other.

Let's see. Here we were visiting 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)
                )
               ]}}
By way of testing the comonad laws on a small sample of data, let us check:
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)


                        
这篇关于如何使一个二叉树拉链一个Comonad的实例？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！