Jav*_*ran 23 haskell zipper 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的一个实例？如果答案是肯定的,我的方法有问题吗？
pig*_*ker 33
在微积分中,莱布尼茨的符号比牛顿的符号更少引起混淆,因为它明确了我们所区分的变量.事物的上下文是通过差异化给出的,因此我们必须注意所处的情境.在这里,工作中有两个"子结构"的概念:子树和元素.它们各自具有不同(但相关)的"上下文"概念,因此具有"拉链",其中拉链是一对物品及其上下文.
您的BTZ类型显示为子树拉链的概念.然而,拉链comonadic结构适用于拉链元素:extract意思是"在这里给元素"; duplicate意思是"用其上下文装饰每个元素".所以你需要元素上下文.令人困惑的是,对于这些二叉树,元素拉链和子树拉链是同构的,但这是一个非常特殊的原因(即它们形成一个共同的comonad).
通常,元素和子树拉链不同,例如,对于列表.如果我们从为列表构建element-zipper comonad开始,当我们回到树时,我们不太可能迷路.让我试着为其他人和你自己填写更多的一般情况.
该子列表 -contexts对于[a]通过刚给出的[a],是我们从子表到整个名单的出路路过的元素列表.[3,4]in 的子列表上下文[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],[])}
]
我们已经看到了如何从一个元素或一个可用元素中走出来.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是元素拉链.
树木怎么样？
让我重构你的二叉树类型来展示一些结构.从字面上看,让我们拉出标记叶子或叉子的元素作为一个共同因素.让我们也分离functor(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 comonad构建.由于每个子树都有一个根元素,因此每个元素都可以用它的根所在的树来装饰.
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中,总有一个元素,您可以进一步了解树结构,但不能进一步向上看.
在元素拉链comonad中,总有一个元素,你可以看到上下两个元素.
代数
d/dt (TF t) = d/dt (1 + t*t) = 0 + (1*t + t*1)
所以我们可以定义
type DTF t = Either ((), t) (t, ())
说"子结构blob"中的子树位于左侧或右侧.我们可以检查"插入"是否有效.
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.那是因为唯一的元素是那些标记节点的元素.将节点拆分为元素及其上下文与将其拆分为其标签及其子结构blob相同.也就是说,我们得到了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实例.像之前一样...
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)
)
]}}
通过测试一小部分数据的comonad定律,让我们检查一下:
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)