haskell - zipper 共轭，一般来说

Question

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

data Bin a = Branch (Bin a) a (Bin a) | Leaf a deriving Functor

带有以下 zipper

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 ，所以我觉得我们应该是通用的并且可以自动构造这些类型和它们

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

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 的导数提供了一个通用框架。

所以，最终，我的问题是我们是否可以写

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 签名是否足够？是否还需要其他东西来限制类型？这个例子甚至可能吗？

Answer 1

就像 Chitty-Chitty-Bang-Bang 中的 child 捕手用糖果和玩具引诱 children 被囚禁一样，本科物理的招聘人员喜欢用肥皂泡和回旋镖来愚弄，但是当门砰地关上时，是“对了， children ，是时候学习了关于偏微分!”。我也是。别说我没有警告你。

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

{-# LANGUAGE TypeFamilies, FlexibleContexts, TupleSections, GADTs, DataKinds,
    TypeOperators, FlexibleInstances, RankNTypes, ScopedTypeVariables,
    StandaloneDeriving, UndecidableInstances #-}

没有特别的顺序。

可微仿函数给出了comonadic zippers

什么是可微仿函数？

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}

它是一个具有导数的仿函数，它也是一个仿函数。导数表示元素的单孔上下文。 zipper 类型 ZF f x 表示一对单孔上下文和孔中的元素。
Diff1 的操作描述了我们可以在 zipper 上进行的导航类型(没有任何“向左”和“向右”的概念，请参见我的 Clowns and Jokers 论文)。我们可以“向上”，通过将元件插入孔中来重新组装结构。我们可以“向下”，找到访问给定结构中元素的各种方法:我们用它的上下文装饰每个元素。我们可以“四处走走”，
使用现有的 zipper 并用其上下文装饰每个元素，因此我们找到了重新聚焦的所有方法(以及如何保持当前的焦点)。

现在， aroundF 的类型可能会让你们中的一些人想起

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

你被提醒是对的!我们有，随着跳跃和跳跃，

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 。

标识 仿函数是可微的。

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 只能留在原地。

Sum 保持可微性。

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 ，然后修复生成的 zipper 以在上下文中显示标记。

  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 ，我们剥离标签，弄清楚如何绕过未标记的东西，然后在所有生成的 zipper 中恢复标签。焦点元素 x 被其整个 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 f x 的事实不足以强制 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

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

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

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

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

将 aroundF 移动到那一侧。

将 upF 移出该侧，将 downF 移至另一侧。

每个案例都要求我们利用子结构的操作，然后修复上下文。

  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)

呼!多项式都是可微的，因此给了我们共数。

唔。这一切都有些抽象。所以我在任何地方都添加了 deriving Show，然后扔进去

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

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

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

练习 使用链式法则证明可微仿函数的组合是可微的。

甜的!我们现在可以回家了吗？当然不是。我们还没有区分任何递归结构。

从二元仿函数制作递归仿函数

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

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

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

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

看？我们在 b 的第一个参数中“打上递归结”，并将参数 y 保留在第二个参数中。因此，我们一劳永逸地获得

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

要使用它，我们需要一组 Bifunctor 实例。

双仿函数套件

常量 是双函的。

newtype K a x y = K a

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

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

变量 是双函的。

我们需要一个参数或另一个参数对应的双仿函数，所以我做了一个数据类型来区分它们，然后定义了一个合适的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 的副本。因此

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

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

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

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

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

但是 zipper 呢？我们如何证明 Mu b 是可微的？我们需要证明 b 在两个变量中都是可微的。铛!是时候学习偏微分了。

双仿函数的偏导数

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

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

现在我们可以说 Bifunctor 在每个变量上都有偏导数意味着什么，并给出相应的 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 和 X -elements 装饰 y -elements 和 0x251812231314312431343433433434313431343243134313431343141-elements但除此之外，这是同一个故事。

我们还有两个任务:首先，证明我们的双仿函数套件是可微的；其次，为了表明 Y 允许我们建立 Diff2 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

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

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

对于结构性案例，我发现引入一个帮助器使我能够统一处理变量很有用。

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

然后，我构建了小工具，以促进我们对 Diff1 (Mu b) 和 down 所需的那种“重新标记”。 (当然，我在工作时看到了我需要哪些小工具。)

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

有了这么多准备好了，我们可以磨出细节。总和很容易。

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)

产品是艰苦的工作，这就是为什么我是数学家而不是工程师的原因。

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 技术构建了这些，在我还没有准备好工作的地方使用 around 作为 stub ，并在一个地方(在任何给定的时间)引入了一个故意的类型错误，我想要从类型检查器。即使在 Haskell 中，您也可以将类型检查作为视频游戏体验。

递归容器的子节点 zipper
undefined 相对于 b 的偏导数告诉我们如何在节点内一步找到子节点，因此我们得到了 zipper 的传统概念。

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

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

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

但是我们需要元素 zipper 。

用于双仿函数固定点的元素 zipper

每个元素都在节点内的某个地方。该节点位于 X 衍生物的堆栈下。但是该节点中元素的位置由 X 衍生物给出。我们得到

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

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

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

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

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

接下来我说

  downF  = yOnDown []

从空堆栈开始向下，并定义从任何堆栈下方重复 Y 的辅助函数:

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 只带我们进入节点。我们需要的 zipper 也必须携带节点的上下文。这就是 down b 所做的:

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)

对于每个 contextualise 位置，我们必须给出一个元素 zipper ，所以我们知道整个上下文 Y 回到根，以及描述元素如何位于其节点中的 dXs 是很好的。对于每个 dY 位置，还有一个进一步的子树需要探索，所以我们增加堆栈并继续前进!

那只剩下转移焦点的业务了。我们可能会留在原地，或者从我们所在的地方下来，或者向上，或者向上然后沿着其他路径走。开始。

  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

与以往一样，现有元素被其整个 zipper 所取代。对于 X 部分，我们看看在现有节点中我们还能去哪里:我们会找到替代元素 belowY -positions 或进一步的 Y -subnodes 来探索，所以我们 0x23413418对于 X 部分，我们必须在重新组装我们正在访问的节点后，以自己的方式备份 contextualise 衍生物的堆栈。

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

在每一步，我们要么转向 aboveY 的其他地方，要么继续向上。

就是这样!我还没有给出法律的正式证明，但在我看来，操作好像在爬行结构时小心地正确地维护了上下文。

我们学到了什么？

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

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

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

我们制作了 extract 种不同类型的结构来存储 duplicate 种不同类型的元素。这些在雅可比结构下是封闭的

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

其中每个结果 o -结构都是偏导数，告诉您如何在 i -结构中制作 (o, i) -element-hole。但这又是依赖类型的乐趣。