拉链Comonads，一般
鉴于任何容器types，我们可以形成（以元素为中心的）拉链，并知道这个结构是一个Comonad。 这是最近探讨在另一个堆栈溢出问题的以下types的精彩细节：
data Bin a = Branch (Bin a) a (Bin a) | Leaf a deriving Functor 用下面的拉链
data Dir = L | R data Step a = Step a Dir (Bin a) deriving Functor data Zip a = Zip [Step a] (Bin a) deriving Functor instance Comonad Zip where ...
Zip是一个Comonad虽然它的实例有点多毛。 也就是说， Zip可以从Tree完全机械地派生出来，并且（我相信）以这种方式派生的任何types都自动成为Comonad ，所以我觉得应该是这样的，我们可以一般地自动构造这些types和它们的连接器。
一种实现拉链构造普遍性的方法是使用以下类别和types族
data Zipper ta = Zipper { diff :: D ta, here :: a } deriving instance Diff t => Functor (Zipper t) class (Functor t, Functor (D t)) => Diff t where data D t :: * -> * inTo :: ta -> t (Zipper ta) outOf :: Zipper ta -> ta
（或多或less）在Haskell Cafe线程和Conal Elliott的博客中显示。 这个类可以被实例化为各种核心代数types，从而为讨论ADT的派生提供了一个通用的框架。
所以，最终，我的问题是我们是否可以写作
instance Diff t => Comonad (Zipper t) where ...
这可以用来包含上述特定的Comonad实例：
instance Diff Bin where data D Bin a = DBin { context :: [Step a], descend :: Maybe (Bin a, Bin a) } ...
不幸的是，我没有写过这样的例子。 inTo / outOf签名是否足够？ 还有什么需要限制的types？ 这个例子甚至可能吗？
就像Chitty-Chitty-Bang-Bang中的child l引诱孩子们被糖果和玩具囚禁一样，大学生物理学的招聘者喜欢用肥皂泡和飞镖来欺骗，但是当门叮叮当当的closures时，这是“正确的，孩子，学习的时间关于偏分化！“ 我也是。 不要说我没有提醒你
这是另一个警告：下面的代码需要{-# LANGUAGE KitchenSink #-} ，或者更确切地说
{-# LANGUAGE TypeFamilies, FlexibleContexts, TupleSections, GADTs, DataKinds, TypeOperators, FlexibleInstances, RankNTypes, ScopedTypeVariables, StandaloneDeriving, UndecidableInstances #-}
没有特别的顺序。
可区分的仿函数可以提供相同的拉链
什么是可区分的仿函数呢？
class (Functor f, Functor (DF f)) => Diff1 f where type DF f :: * -> * upF :: ZF fx -> fx downF :: fx -> f (ZF fx) aroundF :: ZF fx -> ZF f (ZF fx) data ZF fx = (:<-:) {cxF :: DF fx, elF :: x}
这是一个派生函数，也是一个函子。 导数表示元素的单孔上下文。 拉链式ZF fx表示一对单孔上下文和孔中的元素。
Diff1的操作描述了我们可以在拉链上进行的导航types（没有任何“向左”和“向右”的概念，请参阅我的“ 小丑和小丑”的论文）。 我们可以“向上”，通过将元件插入孔中来重新组装结构。 我们可以“向下”，find各种方式访问给定结构中的元素：我们用它的上下文来装饰每个元素。 我们可以“走过去”，拿着现有的拉链和装饰每个元素的背景，所以我们find所有的方法来重新调整（以及如何保持我们当前的重点）。
现在， aroundF的types可能会提醒你的一些
class Functor c => Comonad c where extract :: cx -> x duplicate :: cx -> c (cx)
你是对的提醒！ 我们有一跳，一跳，
instance Diff1 f => Functor (ZF f) where fmap f (df :<-: x) = fmap f df :<-: fx instance Diff1 f => Comonad (ZF f) where extract = elF duplicate = aroundF
我们坚持这一点
extract . duplicate == id fmap extract . duplicate == id duplicate . duplicate == fmap duplicate . duplicate
我们也需要这个
fmap extract (downF xs) == xs -- downF decorates the element in position fmap upF (downF xs) = fmap (const xs) xs -- downF gives the correct context
多项式函数是可微的
不变的函数是可微的。
data KF ax = KF a instance Functor (KF a) where fmap f (KF a) = KF a instance Diff1 (KF a) where type DF (KF a) = KF Void upF (KF w :<-: _) = absurd w downF (KF a) = KF a aroundF (KF w :<-: _) = absurd w
没有地方放置一个元素，所以不可能形成一个上下文。 没有地方downF ，我们很容易find所有的方法去downF 。
身份函数是可微的。
data IF x = IF x instance Functor IF where fmap f (IF x) = IF (fx) instance Diff1 IF where type DF IF = KF () upF (KF () :<-: x) = IF x downF (IF x) = IF (KF () :<-: x) aroundF z@(KF () :<-: x) = KF () :<-: z
在一个普通的情况下有一个元素， downFfind它， upF它，并且aroundF只能保持放置。
总和保留可微性。
data (f :+: g) x = LF (fx) | RF (gx) instance (Functor f, Functor g) => Functor (f :+: g) where fmap h (LF f) = LF (fmap hf) fmap h (RF g) = RF (fmap hg) instance (Diff1 f, Diff1 g) => Diff1 (f :+: g) where type DF (f :+: g) = DF f :+: DF g upF (LF f' :<-: x) = LF (upF (f' :<-: x)) upF (RF g' :<-: x) = RF (upF (g' :<-: x))
其他的零零碎碎的东西有点less。 为了downF ，我们必须在被标记的组件内部downF ，然后修改生成的拉链以在上下文中显示标签。
downF (LF f) = LF (fmap (\ (f' :<-: x) -> LF f' :<-: x) (downF f)) downF (RF g) = RF (fmap (\ (g' :<-: x) -> RF g' :<-: x) (downF g))
为了aroundF ，我们将标签剥离，找出未aroundF标签的东西，然后在所有拉链中恢复标签。 焦点元素x被其整个拉链z所取代。
aroundF z@(LF f' :<-: (x :: x)) = LF (fmap (\ (f' :<-: x) -> LF f' :<-: x) . cxF $ aroundF (f' :<-: x :: ZF fx)) :<-: z aroundF z@(RF g' :<-: (x :: x)) = RF (fmap (\ (g' :<-: x) -> RF g' :<-: x) . cxF $ aroundF (g' :<-: x :: ZF gx)) :<-: z
请注意，我不得不使用ScopedTypeVariables消除ScopedTypeVariables的recursion调用。 作为一个types函数， DF不是内射的，所以f' :: D fx不足以强制f' :<-: x :: Z fx 。
产品保持可区分性。
data (f :*: g) x = fx :*: gx instance (Functor f, Functor g) => Functor (f :*: g) where fmap h (f :*: g) = fmap hf :*: fmap hg
要将注意力集中在一对中的一个元素上，您可以将注意力集中在左侧，让右侧单独放置，反之亦然。 莱布尼茨着名的产品规则相当于一个简单的空间直觉！
instance (Diff1 f, Diff1 g) => Diff1 (f :*: g) where type DF (f :*: g) = (DF f :*: g) :+: (f :*: DF g) upF (LF (f' :*: g) :<-: x) = upF (f' :<-: x) :*: g upF (RF (f :*: g') :<-: x) = f :*: upF (g' :<-: x)
现在， downF工作方式和它所做的相似，不同之处在于我们不仅需要使用标记来修正拉链上下文（以显示我们去过哪个方向），还要修改其他组件。
downF (f :*: g) = fmap (\ (f' :<-: x) -> LF (f' :*: g) :<-: x) (downF f) :*: fmap (\ (g' :<-: x) -> RF (f :*: g') :<-: x) (downF g)
但是， aroundF是aroundF笑声。 无论我们正在访问哪一方，我们有两个select：
- 在那边移动。
- 向上移动，
upF移动到另一侧。
每种情况都要求我们利用子结构的操作，然后修复上下文。
aroundF z@(LF (f' :*: g) :<-: (x :: x)) = LF (fmap (\ (f' :<-: x) -> LF (f' :*: g) :<-: x) (cxF $ aroundF (f' :<-: x :: ZF fx)) :*: fmap (\ (g' :<-: x) -> RF (f :*: g') :<-: x) (downF g)) :<-: z where f = upF (f' :<-: x) aroundF z@(RF (f :*: g') :<-: (x :: x)) = RF (fmap (\ (f' :<-: x) -> LF (f' :*: g) :<-: x) (downF f) :*: fmap (\ (g' :<-: x) -> RF (f :*: g') :<-: x) (cxF $ aroundF (g' :<-: x :: ZF gx))) :<-: z where g = upF (g' :<-: x)
唷！ 多项式都是可微的，从而给我们提供了连接。
嗯。 这一切都有点抽象。 所以我加上了我所能deriving Show ，然后投入
deriving instance (Show (DF fx), Show x) => Show (ZF fx)
允许下面的交互（手工整理）
> downF (IF 1 :*: IF 2) IF (LF (KF () :*: IF 2) :<-: 1) :*: IF (RF (IF 1 :*: KF ()) :<-: 2) > fmap aroundF it IF (LF (KF () :*: IF (RF (IF 1 :*: KF ()) :<-: 2)) :<-: (LF (KF () :*: IF 2) :<-: 1)) :*: IF (RF (IF (LF (KF () :*: IF 2) :<-: 1) :*: KF ()) :<-: (RF (IF 1 :*: KF ()) :<-: 2))
练习使用链式规则表明可微函数的组成是可微的。
甜！ 我们现在能回家吗？ 当然不是。 我们还没有区分任何recursion结构。
从双函数recursion函数
一个Bifunctor ，就像关于数据typesgenerics编程的现有文献一样（参见Patrik Jansson和Johan Jeuring的工作，或者Jeremy Gibbons的优秀讲义），是一个具有两个参数的types构造器，对应于两种子结构。 我们应该能够“映射”两者。
class Bifunctor b where bimap :: (x -> x') -> (y -> y') -> bxy -> bx' y'
我们可以使用Bifunctor来给出recursion容器的节点结构。 每个节点都有子节点和元素 。 这些只能是两种子结构。
data Mu by = In (b (Mu by) y)
看到？ 我们在b的第一个参数中“绑定recursion结”，并将参数y保留在第二个参数中。 因此，我们获得一次
instance Bifunctor b => Functor (Mu b) where fmap f (In b) = In (bimap (fmap f) fb)
要使用这个，我们将需要一套Bifunctor实例。
Bifunctor套件
常量是双重的。
newtype K axy = K a instance Bifunctor (K a) where bimap fg (K a) = K a
你可以告诉我先写这个位，因为标识符较短，但这很好，因为代码更长。
variables是双重的。
我们需要对应于一个参数或另一个参数的双函数，所以我做了一个数据types来区分它们，然后定义了一个合适的GADT。
data Var = X | Y data V :: Var -> * -> * -> * where XX :: x -> VX xy YY :: y -> VY xy
这使得VX xy是x的副本，而VY xy是y的副本。 于是
instance Bifunctor (V v) where bimap fg (XX x) = XX (fx) bimap fg (YY y) = YY (gy)
双折扣的总和和产品是双折扣
data (:++:) fgxy = L (fxy) | R (gxy) deriving Show instance (Bifunctor b, Bifunctor c) => Bifunctor (b :++: c) where bimap fg (L b) = L (bimap fgb) bimap fg (R b) = R (bimap fgb) data (:**:) fgxy = fxy :**: gxy deriving Show instance (Bifunctor b, Bifunctor c) => Bifunctor (b :**: c) where bimap fg (b :**: c) = bimap fgb :**: bimap fgc
到目前为止，这样的样板，但现在我们可以定义的东西
List = Mu (K () :++: (VY :**: VX)) Bin = Mu (VY :**: (K () :++: (VX :**: VX)))
如果你想使用这些types的实际数据，而不是在Georges Seurat的pointilliste传统中盲目使用，使用模式同义词 。
但拉链是什么？ 我们如何表明Mu b是可微的？ 我们需要certificate在这两个variables中b是可微的。 铛！ 现在是了解部分区分的时候了。
双翅膀的部分衍生物
因为我们有两个variables，所以我们需要在其他时候集体讨论它们。 我们需要单身家庭：
data Vary :: Var -> * where VX :: Vary X VY :: Vary Y
现在我们可以说一个Bifunctor对每个variables都有偏导数，并给出了相应的拉链概念。
class (Bifunctor b, Bifunctor (D b X), Bifunctor (D b Y)) => Diff2 b where type D b (v :: Var) :: * -> * -> * up :: Vary v -> Z bvxy -> bxy down :: bxy -> b (Z b X xy) (Z b Y xy) around :: Vary v -> Z bvxy -> Z bv (Z b X xy) (Z b Y xy) data Z bvxy = (:<-) {cxZ :: D bvxy, elZ :: V vxy}
这个D操作需要知道要定位哪个variables。 相应的拉链Z bv告诉我们哪个variablesv必须在焦点上。 当我们用“上下文”来装饰时，我们必须用X -contexts和y elements来装饰x element。 但除此之外，这是一回事。
我们还有两个任务：首先，表明我们的双联套件是可区分的; 其次，为了表明Diff2 b允许我们build立Diff1 (Mu b) 。
区分Bifunctor套件
恐怕这一点很费劲，而不是鼓励。 随意跳过。
常数和以前一样。
instance Diff2 (K a) where type D (K a) v = K Void up _ (K q :<- _) = absurd q down (K a) = K a around _ (K q :<- _) = absurd q
在这种情况下，生命太短，无法发展types水平的Kronecker-delta理论，所以我只是分别处理这些variables。
instance Diff2 (VX) where type D (VX) X = K () type D (VX) Y = K Void up VX (K () :<- XX x) = XX x up VY (K q :<- _) = absurd q down (XX x) = XX (K () :<- XX x) around VX z@(K () :<- XX x) = K () :<- XX z around VY (K q :<- _) = absurd q instance Diff2 (VY) where type D (VY) X = K Void type D (VY) Y = K () up VX (K q :<- _) = absurd q up VY (K () :<- YY y) = YY y down (YY y) = YY (K () :<- YY y) around VX (K q :<- _) = absurd q around VY z@(K () :<- YY y) = K () :<- YY z
对于结构性案例，我发现介绍一个帮助者可以统一处理variables。
vV :: Vary v -> Z bvxy -> V v (Z b X xy) (Z b Y xy) vV VX z = XX z vV VY z = YY z
然后，我build立了小工具，以促进我们需要的“重复”types。 （当然，我在工作时看到了我需要的那些小工具。）
zimap :: (Bifunctor c) => (forall v. Vary v -> D bvxy -> D b' vxy) -> c (Z b X xy) (Z b Y xy) -> c (Z b' X xy) (Z b' Y xy) zimap f = bimap (\ (d :<- XX x) -> f VX d :<- XX x) (\ (d :<- YY y) -> f VY d :<- YY y) dzimap :: (Bifunctor (D c X), Bifunctor (D c Y)) => (forall v. Vary v -> D bvxy -> D b' vxy) -> Vary v -> Z cv (Z b X xy) (Z b Y xy) -> D cv (Z b' X xy) (Z b' Y xy) dzimap f VX (d :<- _) = bimap (\ (d :<- XX x) -> f VX d :<- XX x) (\ (d :<- YY y) -> f VY d :<- YY y) d dzimap f VY (d :<- _) = bimap (\ (d :<- XX x) -> f VX d :<- XX x) (\ (d :<- YY y) -> f VY d :<- YY y) d
随着这一切准备就绪，我们可以研究细节。 总和很容易。
instance (Diff2 b, Diff2 c) => Diff2 (b :++: c) where type D (b :++: c) v = D bv :++: D cv up v (L b' :<- vv) = L (up v (b' :<- vv)) down (L b) = L (zimap (const L) (down b)) down (R c) = R (zimap (const R) (down c)) around vz@(L b' :<- vv :: Z (b :++: c) vxy) = L (dzimap (const L) v ba) :<- vV vz where ba = around v (b' :<- vv :: Z bvxy) around vz@(R c' :<- vv :: Z (b :++: c) vxy) = R (dzimap (const R) v ca) :<- vV vz where ca = around v (c' :<- vv :: Z cvxy)
产品是艰苦的工作，这就是为什么我是math家而不是工程师。
instance (Diff2 b, Diff2 c) => Diff2 (b :**: c) where type D (b :**: c) v = (D bv :**: c) :++: (b :**: D cv) up v (L (b' :**: c) :<- vv) = up v (b' :<- vv) :**: c up v (R (b :**: c') :<- vv) = b :**: up v (c' :<- vv) down (b :**: c) = zimap (const (L . (:**: c))) (down b) :**: zimap (const (R . (b :**:))) (down c) around vz@(L (b' :**: c) :<- vv :: Z (b :**: c) vxy) = L (dzimap (const (L . (:**: c))) v ba :**: zimap (const (R . (b :**:))) (down c)) :<- vV vz where b = up v (b' :<- vv :: Z bvxy) ba = around v (b' :<- vv :: Z bvxy) around vz@(R (b :**: c') :<- vv :: Z (b :**: c) vxy) = R (zimap (const (L . (:**: c))) (down b):**: dzimap (const (R . (b :**:))) v ca) :<- vV vz where c = up v (c' :<- vv :: Z cvxy) ca = around v (c' :<- vv :: Z cvxy)
从概念上讲，就像以前一样，但官僚作风更多。 我使用pre-type-hole技术构build了这些技术，在未准备好工作的地方使用undefined作为存根，并在一个地方（任何给定的时间）引入故意的types错误，我希望从typechecker。 即使在Haskell中，您也可以通过video游戏体验进行types检查。
用于recursion容器的子节点拉链
b关于X的偏导数告诉我们如何在一个节点内find一个子节点，所以我们得到了拉链的传统概念。
data MuZpr by = MuZpr { aboveMu :: [D b X (Mu by) y] , hereMu :: Mu by }
通过重复插入X位，我们可以一路缩小到根部。
muUp :: Diff2 b => MuZpr by -> Mu by muUp (MuZpr {aboveMu = [], hereMu = t}) = t muUp (MuZpr {aboveMu = (dX : dXs), hereMu = t}) = muUp (MuZpr {aboveMu = dXs, hereMu = In (up VX (dX :<- XX t))})
但是我们需要元素 -zippers。
元素拉链的bifunctors固定点
每个元素都在一个节点的某个地方。 这个节点坐在一堆X衍生物下面。 但是该节点中元素的位置是由Y导出的。 我们得到
data MuCx by = MuCx { aboveY :: [D b X (Mu by) y] , belowY :: D b Y (Mu by) y } instance Diff2 b => Functor (MuCx b) where fmap f (MuCx { aboveY = dXs, belowY = dY }) = MuCx { aboveY = map (bimap (fmap f) f) dXs , belowY = bimap (fmap f) f dY }
大胆地说，我声称
instance Diff2 b => Diff1 (Mu b) where type DF (Mu b) = MuCx b
但在开展这些行动之前，我需要一些零碎的东西。
我可以在仿函数拉链和bifunctor-zippers之间交换数据，如下所示：
zAboveY :: ZF (Mu b) y -> [D b X (Mu by) y] -- the stack of `X`-derivatives above me zAboveY (d :<-: y) = aboveY d zZipY :: ZF (Mu b) y -> Z b Y (Mu by) y -- the `Y`-zipper where I am zZipY (d :<-: y) = belowY d :<- YY y
这足以让我定义：
upF z = muUp (MuZpr {aboveMu = zAboveY z, hereMu = In (up VY (zZipY z))})
也就是说，我们首先重新组装元素所在的节点，将一个元素拉链变成一个子节点拉链，然后如上所述一路缩小。
接下来，我说
downF = yOnDown []
从空的堆栈开始往下，定义从任何堆栈下面反复down的辅助函数：
yOnDown :: Diff2 b => [D b X (Mu by) y] -> Mu by -> Mu b (ZF (Mu b) y) yOnDown dXs (In b) = In (contextualize dXs (down b))
现在， down b只把我们带入节点。 我们需要的拉链也必须携带节点的上下文。 contextualise就是这样做的：
contextualize :: (Bifunctor c, Diff2 b) => [D b X (Mu by) y] -> c (Z b X (Mu by) y) (Z b Y (Mu by) y) -> c (Mu b (ZF (Mu b) y)) (ZF (Mu b) y) contextualize dXs = bimap (\ (dX :<- XX t) -> yOnDown (dX : dXs) t) (\ (dY :<- YY y) -> MuCx {aboveY = dXs, belowY = dY} :<-: y)
对于每一个Y位置，我们必须给出一个元素拉链，所以我们知道整个上下文dXs回到根节点，以及描述元素如何在节点中的dY 。 对于每一个X位置，都有一个进一步的子树来探索，所以我们发展壮大，继续前进！
这只留下了转移焦点的业务。 我们可能会留下来，或者从我们现在的位置上下去，或者上去，或者上去，然后往下走。 开始。
aroundF z@(MuCx {aboveY = dXs, belowY = dY} :<-: _) = MuCx { aboveY = yOnUp dXs (In (up VY (zZipY z))) , belowY = contextualize dXs (cxZ $ around VY (zZipY z)) } :<-: z
与以往一样，现有的元素被其整个拉链取代。 对于belowY部分，我们看看现有节点还有哪些可以去的地方：我们将find可选的元素Y位置或者更多的X节点来探索，所以我们contextualise它们置于contextualise 。 对于上述部分，我们必须在重新组装我们正在访问的节点之后，回到X衍生物的堆栈上。
yOnUp :: Diff2 b => [D b X (Mu by) y] -> Mu by -> [D b X (Mu b (ZF (Mu b) y)) (ZF (Mu b) y)] yOnUp [] t = [] yOnUp (dX : dXs) (t :: Mu by) = contextualize dXs (cxZ $ around VX (dX :<- XX t)) : yOnUp dXs (In (up VX (dX :<- XX t)))
在路上的每一步，我们都可以转向其他地方，或继续前进。
而就是这样！ 我还没有给出正式的法律certificate，但是在我看来，这些行动在抓取这个结构的时候，正确地保持了上下文的正确性。
我们学到了什么？
可区分性引发了事物在上下文中的概念，引发了一个共同的结构，在这个结构中， extract为你提供了事物，而duplicate探索了上下文中寻找其他事物的上下文。 如果我们有适当的节点差分结构，我们可以开发整棵树的差分结构。
哦，分别对待每一个单独的构造函数是非常可怕的。 更好的方法是在索引集之间使用函子
f :: (i -> *) -> (o -> *)
我们在哪里制作不同types的结构来存储i不同种类的元素。 这些在雅可比结构下closures
J f :: (i -> *) -> ((o, i) -> *)
(o, i)结构中的每一个都是偏导数，告诉你如何在o结构中创build一个i元素孔。 但是，这是另一个时间，依赖于input乐趣。
Comonad拉链实例不是
instance (Diff t, Diff (D t)) => Comonad (Zipper t) where extract = here duplicate = fmap outOf . inTo
outOf和inTo来自inTo实例本身的Diff实例。 上面的例子违反了Comonad法则的fmap extract . duplicate == id fmap extract . duplicate == id 。 相反，它的行为如下所示：
fmap extract . duplicate == \z -> fmap (const (here z)) z
差异（拉链t）
Zipper的Diff实例是通过将它们标识为产品并重用产品的代码（如下所示）来提供的。
-- Zippers are themselves products toZipper :: (D t :*: Identity) a -> Zipper ta toZipper (d :*: (Identity h)) = Zipper dh fromZipper :: Zipper ta -> (D t :*: Identity) a fromZipper (Zipper dh) = (d :*: (Identity h))
给定数据types之间的同构以及它们派生之间的同构，我们可以将一个types的inTo和outOf用于另一个types。
inToFor' :: (Diff r) => (forall a. ra -> ta) -> (forall a. ta -> ra) -> (forall a. D ra -> D ta) -> (forall a. D ta -> D ra) -> ta -> t (Zipper ta) inToFor' to from toD fromD = to . fmap (onDiff toD) . inTo . from outOfFor' :: (Diff r) => (forall a. ra -> ta) -> (forall a. ta -> ra) -> (forall a. D ra -> D ta) -> (forall a. D ta -> D ra) -> Zipper ta -> ta outOfFor' to from toD fromD = to . outOf . onDiff fromD
对于只有现有Diff实例的newType的types，它们的派生types是相同的types。 如果我们告诉types检查者关于types相等性D r ~ D t ，我们可以利用这一点，而不是为导数提供一个同构。
inToFor :: (Diff r, D r ~ D t) => (forall a. ra -> ta) -> (forall a. ta -> ra) -> ta -> t (Zipper ta) inToFor to from = inToFor' to from id id outOfFor :: (Diff r, D r ~ D t) => (forall a. ra -> ta) -> (forall a. ta -> ra) -> Zipper ta -> ta outOfFor to from = outOfFor' to from id id
配备这些工具，我们可以重用产品的Diff实例来实现Diff (Zipper t)
-- This requires undecidable instances, due to the need to take D (D t) instance (Diff t, Diff (D t)) => Diff (Zipper t) where type D (Zipper t) = D ((D t) :*: Identity) -- inTo :: ta -> t (Zipper ta) -- inTo :: Zipper ta -> Zipper t (Zipper (Zipper t) a) inTo = inToFor toZipper fromZipper -- outOf :: Zipper ta -> ta -- outOf :: Zipper (Zipper t) a -> Zipper ta outOf = outOfFor toZipper fromZipper
样板
为了实际使用这里提供的代码，我们需要一些语言扩展，导入和重新提出的问题。
{-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE DeriveFunctor #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} {-# LANGUAGE RankNTypes #-} import Control.Monad.Identity import Data.Proxy import Control.Comonad data Zipper ta = Zipper { diff :: D ta, here :: a } onDiff :: (D ta -> D ua) -> Zipper ta -> Zipper ua onDiff f (Zipper da) = Zipper (fd) a deriving instance Diff t => Functor (Zipper t) deriving instance (Eq (D ta), Eq a) => Eq (Zipper ta) deriving instance (Show (D ta), Show a) => Show (Zipper ta) class (Functor t, Functor (D t)) => Diff t where type D t :: * -> * inTo :: ta -> t (Zipper ta) outOf :: Zipper ta -> ta
产品，总和和常量
Diff (Zipper t)实例依赖Diff的产品实现:*: ：，总和:+: ：，常量Identity和零Proxy 。
data (:+:) abx = InL (ax) | InR (bx) deriving (Eq, Show) data (:*:) abx = ax :*: bx deriving (Eq, Show) infixl 7 :*: infixl 6 :+: deriving instance (Functor a, Functor b) => Functor (a :*: b) instance (Functor a, Functor b) => Functor (a :+: b) where fmap f (InL a) = InL . fmap f $ a fmap f (InR b) = InR . fmap f $ b instance (Diff a, Diff b) => Diff (a :*: b) where type D (a :*: b) = D a :*: b :+: a :*: D b inTo (a :*: b) = (fmap (onDiff (InL . (:*: b))) . inTo) a :*: (fmap (onDiff (InR . (a :*:))) . inTo) b outOf (Zipper (InL (a :*: b)) x) = (:*: b) . outOf . Zipper a $ x outOf (Zipper (InR (a :*: b)) x) = (a :*:) . outOf . Zipper b $ x instance (Diff a, Diff b) => Diff (a :+: b) where type D (a :+: b) = D a :+: D b inTo (InL a) = InL . fmap (onDiff InL) . inTo $ a inTo (InR b) = InR . fmap (onDiff InR) . inTo $ b outOf (Zipper (InL a) x) = InL . outOf . Zipper a $ x outOf (Zipper (InR a) x) = InR . outOf . Zipper a $ x instance Diff (Identity) where type D (Identity) = Proxy inTo = Identity . (Zipper Proxy) . runIdentity outOf = Identity . here instance Diff (Proxy) where type D (Proxy) = Proxy inTo = const Proxy outOf = const Proxy
Bin示例
我把Bin例子作为一个同构的产品。 我们不仅需要它的衍生物，还需要它的二阶导数
newtype Bin a = Bin {unBin :: (Bin :*: Identity :*: Bin :+: Identity) a} deriving (Functor, Eq, Show) newtype DBin a = DBin {unDBin :: D (Bin :*: Identity :*: Bin :+: Identity) a} deriving (Functor, Eq, Show) newtype DDBin a = DDBin {unDDBin :: D (D (Bin :*: Identity :*: Bin :+: Identity)) a} deriving (Functor, Eq, Show) instance Diff Bin where type D Bin = DBin inTo = inToFor' Bin unBin DBin unDBin outOf = outOfFor' Bin unBin DBin unDBin instance Diff DBin where type D DBin = DDBin inTo = inToFor' DBin unDBin DDBin unDDBin outOf = outOfFor' DBin unDBin DDBin unDDBin
以前答案的示例数据是
aTree :: Bin Int aTree = (Bin . InL) ( (Bin . InL) ( (Bin . InR) (Identity 2) :*: (Identity 1) :*: (Bin . InR) (Identity 3) ) :*: (Identity 0) :*: (Bin . InR) (Identity 4) )
不是Comonad实例
上面的Bin例子提供了fmap outOf . inTo的反例fmap outOf . inTo fmap outOf . inTo是正确的实现duplicate的Zipper t 。 特别是，它提供了一个fmap extract . duplicate = id的反例fmap extract . duplicate = id fmap extract . duplicate = id法：
fmap ( \z -> (fmap extract . duplicate) z == z) . inTo $ aTree
其中评估（注意它到处充满了False的东西，任何False都足以反驳法律）
Bin {unBin = InL ((Bin {unBin = InL ((Bin {unBin = InR (Identity False)} :*: Identity False) :*: Bin {unBin = InR (Identity False)})} :*: Identity False) :*: Bin {unBin = InR (Identity False)})}
inTo aTree是一棵与Tree相同结构的树，但是到处都是一个值，而不是一个带有值的拉链，剩余的树的所有原始值都是完整的。 fmap (fmap extract . duplicate) . inTo $ aTree fmap (fmap extract . duplicate) . inTo $ aTree也是一棵与fmap (fmap extract . duplicate) . inTo $ aTree具有相同结构的树，但是每个值都有一个值，而值为一个拉链，树的其余部分将所有值replace为相同的值 。 换一种说法：
fmap extract . duplicate == \z -> fmap (const (here z)) z
所有三个Comonad法律的完整testing套件， extract . duplicate == id extract . duplicate == id ， fmap extract . duplicate == id fmap extract . duplicate == id和duplicate . duplicate == fmap duplicate . duplicate duplicate . duplicate == fmap duplicate . duplicate duplicate . duplicate == fmap duplicate . duplicate是
main = do putStrLn "fmap (\\z -> (extract . duplicate) z == z) . inTo $ aTree" print . fmap ( \z -> (extract . duplicate) z == z) . inTo $ aTree putStrLn "" putStrLn "fmap (\\z -> (fmap extract . duplicate) z == z) . inTo $ aTree" print . fmap ( \z -> (fmap extract . duplicate) z == z) . inTo $ aTree putStrLn "" putStrLn "fmap (\\z -> (duplicate . duplicate) z) == (fmap duplicate . duplicate) z) . inTo $ aTree" print . fmap ( \z -> (duplicate . duplicate) z == (fmap duplicate . duplicate) z) . inTo $ aTree
给定一个无限可微的Diff类：
class (Functor t, Functor (D t)) => Diff t where type D t :: * -> * up :: Zipper ta -> ta down :: ta -> t (Zipper ta) -- Require that types be infinitely differentiable ddiff :: pt -> Dict (Diff (D t))
around可以写在Zipper的diff的基础上，在本质上如同
around z@(Zipper dh) = Zipper ctx z where ctx = fmap (\z' -> Zipper (up z') (here z')) (down d)
Zipper ta由D ta和a 。 我们down D ta走，每个洞都有一个拉链D t (Zipper (D t) a) 。 这些拉链由一个D (D t) a和a在洞里的a组成。 我们up每一个，得到一个D ta ，并用洞中的a去掉。 一个D ta和一个Zipper ta ，给了我们一个D t (Zipper ta) ，这是Zipper t (Zipper ta)所需的上下文。
那么Comonad实例就是简单的
instance Diff t => Comonad (Zipper t) where extract = here duplicate = around
捕获派生的Diff字典需要一些额外的pipe道，这可以使用Data.Constraint或根据相关答案中提供的方法来完成
around :: Diff t => Zipper ta -> Zipper t (Zipper ta) around z = Zipper (withDict d' (fmap (\z' -> Zipper (up z') (here z')) (down (diff z)))) z where d' = ddiff . p' $ z p' :: Zipper tx -> Proxy t p' = const Proxy
