拉链共轭，一般 [英] Zipper Comonads, Generically

问题描述

给定任何容器类型，我们可以形成(以元素为中心的)Zipper 并且知道这个结构是一个 Comonad.最近在 another Stack 中详细探讨了这一点以下类型的溢出问题:

Given any container type we can form the (element-focused) Zipper and know that this structure is a Comonad. This was recently explored in wonderful detail in another Stack Overflow question for the following type:

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 派生出来，并且(我相信)任何以这种方式派生的类型都会自动成为 Comonad，所以我觉得应该是这样，我们可以通用地和自动地构造这些类型及其共子.

It is the case that Zip is a Comonad though the construction of its instance is a little hairy. That said, Zip can be completely mechanically derived from Tree and (I believe) any type derived this way is automatically a Comonad, so I feel it ought to be the case that we can construct these types and their comonads generically and automatically.

实现拉链构造通用性的一种方法是使用以下类和类型族

One method for achieving generality for zipper construction is the use the following class and type family

data Zipper t a = Zipper { diff :: D t a, here :: a }

deriving instance Diff t => Functor (Zipper t)

class (Functor t, Functor (D t)) => Diff t where
  data D t :: * -> *
  inTo  :: t a -> t (Zipper t a)
  outOf :: Zipper t a -> t a

已(或多或少)出现在 Haskell Cafe 主题和 Conal Elliott 的博客上.此类可以针对各种核心代数类型进行实例化，从而为讨论 ADT 的导数提供了一个通用框架.

which has (more or less) shown up in Haskell Cafe threads and on Conal Elliott's blog. This class can be instantiated for the various core algebraic types and thus provides a general framework for talking about the derivatives of ADTs.

所以，归根结底，我的问题是我们是否可以写

So, ultimately, my question is whether or not we can write

instance Diff t => Comonad (Zipper t) where ...

可用于包含上述特定的 Comonad 实例:

which could be used to subsume the specific Comonad instance described above:

instance Diff Bin where
  data D Bin a = DBin { context :: [Step a], descend :: Maybe (Bin a, Bin a) }
  ...

不幸的是，我没有写出这样的例子.inTo/outOf 签名是否足够?是否还需要其他东西来限制类型?这种情况甚至可能吗?

Unfortunately, I've had no luck writing such an instance. Is the inTo/outOf signature sufficient? Is there something else needed to constrain the types? Is this instance even possible?

推荐答案

就像 Chitty-Chitty-Bang-Bang 的 childcatcher 用糖果和玩具引诱孩子们被囚禁一样，本科物理的招聘人员喜欢用肥皂泡和回旋镖开玩笑，但是当门砰地关上时，是对了，孩子们，是时候学习偏微分了！".我也是.别说我没提醒你.

Like the childcatcher in Chitty-Chitty-Bang-Bang luring kids into captivity with sweets and toys, recruiters to undergraduate Physics like to fool about with soap bubbles and boomerangs, but when the door clangs shut, it's "Right, children, time to learn about partial differentiation!". Me too. Don't say I didn't warn you.

这是另一个警告:以下代码需要 {-# LANGUAGE KitchenSink #-}，或者更确切地说

Here's another warning: the following code needs {-# LANGUAGE KitchenSink #-}, or rather

{-# 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 f x  ->  f x
  downF    ::  f x     ->  f (ZF f x)
  aroundF  ::  ZF f x  ->  ZF f (ZF f x)

data ZF f x = (:<-:) {cxF :: DF f x, elF :: x}

它是一个具有导数的函子，它也是一个函子.导数表示元素的单孔上下文.拉链类型 ZF f x 表示一对单孔上下文和孔中的元素.

It's a functor which has a derivative, which is also a functor. The derivative represents a one-hole context for an element. The zipper type ZF f x represents the pair of a one-hole context and the element in the hole.

Diff1 的操作描述了我们可以在拉链上进行的导航类型(没有任何向左"和向右"的概念，参见我的 小丑和小丑 论文).我们可以向上"，通过将元件插入孔中来重新组装结构.我们可以向下"，找到访问给定结构中元素的各种方法:我们用它的上下文装饰每个元素.我们可以四处走走"，使用现有的拉链并用其上下文装饰每个元素，因此我们找到了重新聚焦的所有方法(以及如何保持当前的焦点).

The operations for Diff1 describe the kinds of navigation we can do on zippers (without any notion of "leftward" and "rightward", for which see my Clowns and Jokers paper). We can go "upward", reassembling the structure by plugging the element in its hole. We can go "downward", finding every way to visit an element in a give structure: we decorate every element with its context. We can go "around", taking an existing zipper and decorating each element with its context, so we find all the ways to refocus (and how to keep our current focus).

现在，aroundF 的类型可能会让你们想起

Now, the type of aroundF might remind some of you of

class Functor c => Comonad c where
  extract    :: c x -> x
  duplicate  :: c x -> c (c x)

你被提醒是对的！我们有，一跳一跳，

and you're right to be reminded! We have, with a hop and a skip,

instance Diff1 f => Functor (ZF f) where
  fmap f (df :<-: x) = fmap f df :<-: f x

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 a x = 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

元素无处可放，因此无法形成上下文.upF 或 downF 无处可去，而且我们很容易找到所有 downF 的方法.

There's nowhere to put an element, so it's impossible to form a context. There's nowhere to go upF or downF from, and we easily find all none of the ways to go downF.

恒等函子是可微的.

data IF x = IF x
instance Functor IF where
  fmap f (IF x) = IF (f x)

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

在一个微不足道的上下文中有一个元素，downF 找到它，upF 重新打包它，aroundF 只能原地不动.

There's one element in a trivial context, downF finds it, upF repacks it, and aroundF can only stay put.

求和保持可微性.

data (f :+: g) x = LF (f x) | RF (g x)
instance (Functor f, Functor g) => Functor (f :+: g) where
  fmap h (LF f) = LF (fmap h f)
  fmap h (RF g) = RF (fmap h g)

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))

其他的点点滴滴都比较少.要转到 downF，我们必须在标记组件中转到 downF，然后修复生成的拉链以在上下文中显示标记.

The other bits and pieces are a bit more of a handful. To go downF, we must go downF inside the tagged component, then fix up the resulting zippers to show the tag in the context.

  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，我们去除标签，弄清楚如何绕过未标记的东西，然后在所有生成的拉链中恢复标签.焦点元素 x 被其整个拉链替换，z.

To go aroundF, we strip the tag, figure out how to go around the untagged thing, then restore the tag in all the resulting zippers. The element in focus, x, is replaced by its entire zipper, z.

  aroundF z@(LF f' :<-: (x :: x)) =
    LF (fmap ( (f' :<-: x) -> LF f' :<-: x) . cxF $ aroundF (f' :<-: x :: ZF f x))
    :<-: z
  aroundF z@(RF g' :<-: (x :: x)) =
    RF (fmap ( (g' :<-: x) -> RF g' :<-: x) . cxF $ aroundF (g' :<-: x :: ZF g x))
    :<-: z

请注意，我必须使用 ScopedTypeVariables 来消除对 aroundF 的递归调用的歧义.作为类型函数，DF 不是单射的，所以 f' :: D fx 不足以强制 f' :<-: x:: Z fx.

Note that I had to use ScopedTypeVariables to disambiguate the recursive calls to aroundF. As a type function, DF is not injective, so the fact that f' :: D f x is not enough to force f' :<-: x :: Z f x.

产品保持可区分性.

data (f :*: g) x = f x :*: g x
instance (Functor f, Functor g) => Functor (f :*: g) where
  fmap h (f :*: g) = fmap h f :*: fmap h g

要关注成对中的一个元素，您要么关注左边，而不管右边，反之亦然.莱布尼茨著名的乘积法则对应一个简单的空间直觉！

To focus on an element in a pair, you either focus on the left and leave the right alone, or vice versa. Leibniz's famous product rule corresponds to a simple spatial intuition!

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 的工作方式与它对总和的处理方式类似，除了我们必须修复拉链上下文，不仅要使用标签(以显示我们走了哪条路)，还要使用未触及其他组件.

Now, downF works similarly to the way it did for sums, except that we have to fix up the zipper context not only with a tag (to show which way we went) but also with the untouched other component.

  downF (f :*: g)
    =    fmap ( (f' :<-: x) -> LF (f' :*: g) :<-: x) (downF f)
    :*:  fmap ( (g' :<-: x) -> RF (f :*: g') :<-: x) (downF g)

但是aroundF 是一大堆笑声.无论我们目前访问哪一边，我们都有两个选择:

But aroundF is a massive bag of laughs. Whichever side we are currently visiting, we have two choices:

1. 将 aroundF 移动到那一侧.
2. 将 upF 从那一侧移出，将 downF 移到另一侧.

1. Move aroundF on that side.
2. Move upF out of that side and downF into the other side.

每种情况都要求我们利用子结构的操作，然后修复上下文.

Each case requires us to make use of the operations for the substructure, then fix up contexts.

  aroundF z@(LF (f' :*: g) :<-: (x :: x)) =
    LF (fmap ( (f' :<-: x) -> LF (f' :*: g) :<-: x)
          (cxF $ aroundF (f' :<-: x :: ZF f x))
        :*: 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 g x)))
    :<-: z
    where g = upF (g' :<-: x)

呸！多项式都是可微的，因此给了我们共子.

Phew! The polynomials are all differentiable, and thus give us comonads.

嗯.这一切都有些抽象.所以我在任何可能的地方添加了 deriving Show 并投入了

Hmm. It's all a bit abstract. So I added deriving Show everywhere I could, and threw in

deriving instance (Show (DF f x), Show x) => Show (ZF f x)

允许以下交互(手动整理)

which allowed the following interaction (tidied up by hand)

> 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))

练习证明可微函子的组合是可微的，使用链式法则.

Exercise Show that the composition of differentiable functors is differentiable, using the chain rule.

甜！我们现在可以回家了吗?当然不是.我们还没有区分任何递归结构.

Sweet! Can we go home now? Of course not. We haven't differentiated any recursive structures yet.

Bifunctor，正如关于数据类型泛型编程的现有文献(参见 Patrik Jansson 和 Johan Jeuring 的著作，或 Jeremy Gibbons 的优秀讲义)详细解释的是具有两个参数的类型构造函数，对应两种子结构.我们应该能够映射"两者.

A Bifunctor, as the existing literature on datatype generic programming (see work by Patrik Jansson and Johan Jeuring, or excellent lecture notes by Jeremy Gibbons) explains at length is a type constructor with two parameters, corresponding to two sorts of substructure. We should be able to "map" both.

class Bifunctor b where
  bimap :: (x -> x') -> (y -> y') -> b x y -> b x' y'

我们可以使用Bifunctor来给出递归容器的节点结构.每个节点都有子节点和元素.这些可以只是两种子结构.

We can use Bifunctors to give the node structure of recursive containers. Each node has subnodes and elements. These can just be the two sorts of substructure.

data Mu b y = In (b (Mu b y) y)

看到了吗?我们在 b 的第一个参数中打上递归结"，并将参数 y 保留在第二个参数中.因此，我们一劳永逸地获得了

See? We "tie the recursive knot" in b's first argument, and keep the parameter y in its second. Accordingly, we obtain once for all

instance Bifunctor b => Functor (Mu b) where
  fmap f (In b) = In (bimap (fmap f) f b)

要使用它，我们需要一套 Bifunctor 实例.

To use this, we'll need a kit of Bifunctor instances.

常量是双函数的.

newtype K a x y = K a

instance Bifunctor (K a) where
  bimap f g (K a) = K a

你可以说是我先写了这一点，因为标识符更短，但这很好，因为代码更长.

You can tell I wrote this bit first, because the identifiers are shorter, but that's good because the code is longer.

变量是双函数的.

我们需要一个或另一个参数对应的双函子，所以我做了一个数据类型来区分它们，然后定义了一个合适的GADT.

We need the bifunctors corresponding to one parameter or the other, so I made a datatype to distinguish them, then defined a suitable GADT.

data Var = X | Y

data V :: Var -> * -> * -> * where
  XX :: x -> V X x y
  YY :: y -> V Y x y

这使得 V X x y 成为 x 的副本，V Y x y 成为 y 的副本.相应地

That makes V X x y a copy of x and V Y x y a copy of y. Accordingly

instance Bifunctor (V v) where
  bimap f g (XX x) = XX (f x)
  bimap f g (YY y) = YY (g y)

双函子的

和和乘积是双函子

data (:++:) f g x y = L (f x y) | R (g x y) deriving Show

instance (Bifunctor b, Bifunctor c) => Bifunctor (b :++: c) where
  bimap f g (L b) = L (bimap f g b)
  bimap f g (R b) = R (bimap f g b)

data (:**:) f g x y = f x y :**: g x y deriving Show

instance (Bifunctor b, Bifunctor c) => Bifunctor (b :**: c) where
  bimap f g (b :**: c) = bimap f g b :**: bimap f g c

到目前为止，都是样板，但现在我们可以定义诸如

So far, so boilerplate, but now we can define things like

List = Mu (K () :++: (V Y :**: V X))

Bin = Mu (V Y :**: (K () :++: (V X :**: V X)))

如果您想将这些类型用于实际数据，而不是在 Georges Seurat 的点画传统中盲目，请使用模式同义词.

If you want to use these types for actual data and not go blind in the pointilliste tradition of Georges Seurat, use pattern synonyms.

但是拉链呢?我们如何证明 Mu b 是可微的?我们需要证明 b 在 both 变量中是可微的.铛！是时候了解偏微分了.

But what of zippers? How shall we show that Mu b is differentiable? We shall need to show that b is differentiable in both variables. Clang! It's time to learn about partial differentiation.

因为我们有两个变量，所以我们需要能够有时集体讨论它们，有时单独讨论它们.我们将需要单身家庭:

Because we have two variables, we shall need to be able to talk about them collectively sometimes and individually at other times. We shall need the singleton family:

data Vary :: Var -> * where
  VX :: Vary X
  VY :: Vary Y

现在我们可以说 Bifunctor 在每个变量上都有偏导数意味着什么，并给出相应的 zipper 概念.

Now we can say what it means for a Bifunctor to have partial derivatives at each variable, and give the corresponding notion of zipper.

class (Bifunctor b, Bifunctor (D b X), Bifunctor (D b Y)) => Diff2 b where
  type D b (v :: Var) :: * -> * -> *
  up      :: Vary v -> Z b v x y -> b x y
  down    :: b x y -> b (Z b X x y) (Z b Y x y)
  around  :: Vary v -> Z b v x y -> Z b v (Z b X x y) (Z b Y x y)

data Z b v x y = (:<-) {cxZ :: D b v x y, elZ :: V v x y}

这个 D 操作需要知道要定位哪个变量.对应的 zipper Z b v 告诉我们哪个变量 v 必须是焦点.当我们用上下文装饰"时，我们必须用X-contexts和y-元素用Y<装饰x-元素/代码>-上下文.但除此之外，这是同一个故事.

This D operation needs to know which variable to target. The corresponding zipper Z b v tells us which variable v must be in focus. When we "decorate with context", we have to decorate x-elements with X-contexts and y-elements with Y-contexts. But otherwise, it's the same story.

我们还有两个任务:首先，证明我们的双函子套件是可微的；其次，证明Diff2 b允许我们建立Diff1 (Mu b).

We have two remaining tasks: firstly, to show that our bifunctor kit is differentiable; secondly, to show that Diff2 b allows us to establish Diff1 (Mu b).

恐怕这一点是繁琐而不是有启发性的.随意跳过.

I'm afraid this bit is fiddly rather than edifying. Feel free to skip along.

常量和以前一样.

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

在这种情况下，生命太短暂，无法发展类型级别的 Kronecker-delta 理论，所以我只对变量进行了单独处理.

On this occasion, life is too short to develop the theory of the type level Kronecker-delta, so I just treated the variables separately.

instance Diff2 (V X) where
  type D (V X) X = K ()
  type D (V X) 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 (V Y) where
  type D (V Y) X = K Void
  type D (V Y) 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

对于结构性案例，我发现引入一个帮助器可以让我统一处理变量很有用.

For the structural cases, I found it useful to introduce a helper allowing me to treat variables uniformly.

vV :: Vary v -> Z b v x y -> V v (Z b X x y) (Z b Y x y)
vV VX z = XX z
vV VY z = YY z

然后，我构建了小工具来促进我们对 down 和 around 所需的那种重新标记".(当然，我在工作时看到了我需要哪些小工具.)

I then built gadgets to facilitate the kind of "retagging" we need for down and around. (Of course, I saw which gadgets I needed as I was working.)

zimap :: (Bifunctor c) => (forall v. Vary v -> D b v x y -> D b' v x y) ->
         c (Z b X x y) (Z b Y x y) -> c (Z b' X x y) (Z b' Y x y)
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 b v x y -> D b' v x y) ->
         Vary v -> Z c v (Z b X x y) (Z b Y x y) -> D c v (Z b' X x y) (Z b' Y x y)
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

准备好这么多，我们就可以细化细节了.求和很容易.

And with that lot ready to go, we can grind out the details. Sums are easy.

instance (Diff2 b, Diff2 c) => Diff2 (b :++: c) where
  type D (b :++: c) v = D b v :++: D c v
  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 v z@(L b' :<- vv :: Z (b :++: c) v x y)
    = L (dzimap (const L) v ba) :<- vV v z
    where ba = around v (b' :<- vv :: Z b v x y)
  around v z@(R c' :<- vv :: Z (b :++: c) v x y)
    = R (dzimap (const R) v ca) :<- vV v z
    where ca = around v (c' :<- vv :: Z c v x y)

产品是艰苦的工作，这就是为什么我是一名数学家而不是工程师.

Products are hard work, which is why I'm a mathematician rather than an engineer.

instance (Diff2 b, Diff2 c) => Diff2 (b :**: c) where
  type D (b :**: c) v = (D b v :**: c) :++: (b :**: D c v)
  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 v z@(L (b' :**: c) :<- vv :: Z (b :**: c) v x y)
    = L (dzimap (const (L . (:**: c))) v ba :**:
        zimap (const (R . (b :**:))) (down c))
      :<- vV v z where
      b = up v (b' :<- vv :: Z b v x y)
      ba = around v (b' :<- vv :: Z b v x y)
  around v z@(R (b :**: c') :<- vv :: Z (b :**: c) v x y)
    = R (zimap (const (L . (:**: c))) (down b):**:
        dzimap (const (R . (b :**:))) v ca)
      :<- vV v z where
      c = up v (c' :<- vv :: Z c v x y)
      ca = around v (c' :<- vv :: Z c v x y)

从概念上讲，它和以前一样，但官僚作风更多.我使用 pre-type-hole 技术构建这些，在我还没有准备好工作的地方使用 undefined 作为存根，并在一个地方(在任何给定的时间)引入一个故意的类型错误我想要来自类型检查器的有用提示.即使在 Haskell 中，您也可以将类型检查作为视频游戏体验.

Conceptually, it's just as before, but with more bureaucracy. I built these using pre-type-hole technology, using undefined as a stub in places I wasn't ready to work, and introducing a deliberate type error in the one place (at any given time) where I wanted a useful hint from the typechecker. You too can have the typechecking as videogame experience, even in Haskell.

b 相对于 X 的偏导数告诉我们如何在节点内部一步找到一个子节点，所以我们得到了拉链的传统概念.>

The partial derivative of b with respect to X tells us how to find a subnode one step inside a node, so we get the conventional notion of zipper.

data MuZpr b y = MuZpr
  {  aboveMu  :: [D b X (Mu b y) y]
  ,  hereMu   :: Mu b y
  }

通过重复插入 X 位置，我们可以一直放大到根.

We can zoom all the way up to the root by repeated plugging in X positions.

muUp :: Diff2 b => MuZpr b y -> Mu b y
muUp (MuZpr {aboveMu = [], hereMu = t}) = t
muUp (MuZpr {aboveMu = (dX : dXs), hereMu = t}) =
  muUp (MuZpr {aboveMu = dXs, hereMu = In (up VX (dX :<- XX t))})

但是我们需要element-zippers.

But we need element-zippers.

每个元素都在一个节点内的某处.该节点位于一堆 X 衍生物下.但是该节点中元素的位置由 Y 导数给出.我们得到

Each element is somewhere inside a node. That node is sitting under a stack of X-derivatives. But the position of the element in that node is given by a Y-derivative. We get

data MuCx b y = MuCx
  {  aboveY  :: [D b X (Mu b y) y]
  ,  belowY  :: D b Y (Mu b y) 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

但在我开发操作之前，我需要一些零碎的东西.

but before I develop the operations, I'll need some bits and pieces.

我可以在 functor-zippers 和 bifunctor-zippers 之间交换数据，如下所示:

I can trade data between functor-zippers and bifunctor-zippers as follows:

zAboveY :: ZF (Mu b) y -> [D b X (Mu b y) y]  -- the stack of `X`-derivatives above me
zAboveY (d :<-: y) = aboveY d

zZipY :: ZF (Mu b) y -> Z b Y (Mu b y) 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))})

也就是说，我们首先重新组装元素所在的节点，将元素拉链变成子节点拉链，然后一直放大，如上.

That is, we go up by first reassembling the node where the element is, turning an element-zipper into a subnode-zipper, then zooming all the way out, as above.

接下来说

  downF  = yOnDown []

从空栈开始往下走，并定义从任何栈下面重复down的辅助函数:

to go down starting with the empty stack, and define the helper function which goes down repeatedly from below any stack:

yOnDown :: Diff2 b => [D b X (Mu b y) y] -> Mu b y -> Mu b (ZF (Mu b) y)
yOnDown dXs (In b) = In (contextualize dXs (down b))

现在，down b 只带我们进入节点.我们需要的拉链也必须携带节点的上下文.这就是 contextualise 所做的:

Now, down b only takes us inside the node. The zippers we need must also carry the node's context. That's what contextualise does:

contextualize :: (Bifunctor c, Diff2 b) =>
  [D b X (Mu b y) y] ->
  c (Z b X (Mu b y) y) (Z b Y (Mu b y) 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 位置，还有一个进一步的子树需要探索，所以我们增加堆栈并继续前进！

For every Y-position, we must give an element-zipper, so it is good we know the whole context dXs back to the root, as well as the dY which describes how the element sits in its node. For every X-position, there is a further subtree to explore, so we grow the stack and keep going!

剩下的就是转移焦点的事情了.我们可能会留在原地，或者从我们所在的地方下来，或者向上，或者向上然后沿着其他路径走.来了.

That leaves only the business of shifting focus. We might stay put, or go down from where we are, or go up, or go up and then down some other path. Here goes.

  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 部分，我们查看在现有节点中还可以去哪里:我们将找到替代元素 Y-positions 或进一步的 X- 要探索的子节点，因此我们上下文化它们.对于 aboveY 部分，我们必须在重新组装我们正在访问的节点后，以自己的方式备份 X 衍生物的堆栈.

As ever, the existing element is replaced by its entire zipper. For the belowY part, we look where else we can go in the existing node: we will find either alternative element Y-positions or further X-subnodes to explore, so we contextualise them. For the aboveY part, we must work our way back up the stack of X-derivatives after reassembling the node we were visiting.

yOnUp :: Diff2 b => [D b X (Mu b y) y] -> Mu b y ->
         [D b X (Mu b (ZF (Mu b) y)) (ZF (Mu b) y)]
yOnUp [] t = []
yOnUp (dX : dXs) (t :: Mu b y)
  =  contextualize dXs (cxZ $ around VX (dX :<- XX t))
  :  yOnUp dXs (In (up VX (dX :<- XX t)))

在每一步，我们要么在around的其他地方转弯，要么继续向上.

At each step of the way, we can either turn somewhere else that's around, or keep going up.

就是这样！我没有给出规律的正式证明，但在我看来，这些操作在爬行结构时仔细地正确维护了上下文.

And that's it! I haven't given a formal proof of the laws, but it looks to me as if the operations carefully maintain the context correctly as they crawl the structure.

可微分诱导事物在其上下文中的概念，产生一个共调结构，其中 extract 为您提供事物，而 duplicate 探索上下文以寻找其他事物以进行上下文化.如果我们有合适的节点微分结构，我们就可以开发整棵树的微分结构.

Differentiability induces notions of thing-in-its-context, inducing a comonadic structure where extract gives you the thing and duplicate explores the context looking for other things to contextualise. If we have the appropriate differential structure for nodes, we can develop differential structure for whole trees.

哦，单独处理类型构造函数的每个单独的arity是非常可怕的.更好的方法是在索引集之间使用函子

Oh, and treating each individual arity of type constructor separately is blatantly horrendous. The better way is to work with functors between indexed sets

f :: (i -> *) -> (o -> *)

我们在哪里制作 o 不同种类的结构来存储 i 不同种类的元素.这些在雅可比结构下封闭

where we make o different sorts of structure storing i different sorts of element. These are closed under the Jacobian construction

J f :: (i -> *) -> ((o, i) -> *)

其中每个结果 (o, i)-structures 都是偏导数，告诉您如何在 中制作 i-element-holeo-结构.但这是依赖类型的乐趣，下次再说吧.

where each of the resulting (o, i)-structures is a partial derivative, telling you how to make an i-element-hole in an o-structure. But that's dependently typed fun, for another time.

这篇关于拉链共轭，一般的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！