Zipper Comonads,一般来说

Question

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

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,所以我觉得应该是这样我们可以通用和自动地构造这些类型及其组合.

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

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

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.

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

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

in no particular order.

Differentiable functors give comonadic zippers

What is a differentiable functor, anyway?

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}

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.

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

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

and we insist that

extract . duplicate == id
fmap extract . duplicate == id
duplicate . duplicate == fmap duplicate . duplicate

We also need that

fmap extract (downF xs) == xs              -- downF decorates the element in position
fmap upF (downF xs) = fmap (const xs) xs   -- downF gives the correct context

Polynomial functors are differentiable

恒定的算子是可区分的.

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只能保持不变.

总和保留了可分性.

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标记组件,然后修复生成的拉链以在上下文中显示标记.

  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.

  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)

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)

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

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.

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.

Making recursive functors from bifunctors

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'

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)

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)

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

The Bifunctor Kit

Constants are bifunctorial.

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.

Variables are bifunctorial.

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

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)

Sums and Products of bifunctors are bifunctors

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

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

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.

Partial derivatives of bifunctors

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

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}

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.

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

Differentiating the Bifunctor kit

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

The constants are as before.

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

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

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)

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.

Subnode zippers for recursive containers

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
  }

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

But we need element-zippers.

Element-zippers for fixpoints of bifunctors

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
    }

Boldly, I claim

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.

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

That's enough to let me define:

  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.

Next, I say

  downF  = yOnDown []

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

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)

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

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

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.

What have we learned?

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.

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

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)结构都是偏导数,告诉你如何在i-structure中制作一个元素孔o.但这又取决于其他时间的乐趣.

Answer 2

Comonad拉链的实例不是

instance (Diff t, Diff (D t)) => Comonad (Zipper t) where
    extract = here
    duplicate = fmap outOf . inTo

来自实例的地方outOf和inTo来自.以上情况违反了法律.相反,它的行为如下:DiffZipper tComonadfmap extract . duplicate == id

fmap extract . duplicate == \z -> fmap (const (here z)) z

差异(拉链t)

在Diff例如Zipper通过识别它们作为产品和再利用产品(下面)提供的代码.

-- Zippers are themselves products
toZipper :: (D t :*: Identity) a -> Zipper t a
toZipper (d :*: (Identity h)) = Zipper d h

fromZipper :: Zipper t a -> (D t :*: Identity) a
fromZipper (Zipper d h) = (d :*: (Identity h))

鉴于数据类型之间的同构,以及它们的派生之间的同构,我们可以重用一种类型inTo而outOf另一种类型.

inToFor' :: (Diff r) =>
            (forall a.   r a ->   t a) ->
            (forall a.   t a ->   r a) ->
            (forall a. D r a -> D t a) ->
            (forall a. D t a -> D r a) ->
            t a -> t (Zipper t a)
inToFor' to from toD fromD = to . fmap (onDiff toD) . inTo . from

outOfFor' :: (Diff r) =>
            (forall a.   r a ->   t a) ->
            (forall a.   t a ->   r a) ->
            (forall a. D r a -> D t a) ->
            (forall a. D t a -> D r a) ->
            Zipper t a -> t a
outOfFor' to from toD fromD = to . outOf . onDiff fromD

对于仅为现有Diff实例的newTypes的类型,它们的派生类型相同.如果我们告诉类型检查器关于该类型相等D r ~ D t,我们可以利用它而不是为衍生物提供同构.

inToFor :: (Diff r, D r ~ D t) =>
           (forall a. r a -> t a) ->
           (forall a. t a -> r a) ->
           t a -> t (Zipper t a)
inToFor to from = inToFor' to from id id

outOfFor :: (Diff r, D r ~ D t) =>
            (forall a. r a -> t a) ->
            (forall a. t a -> r a) ->
            Zipper t a -> t a
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 :: t        a -> t        (Zipper  t         a)
    -- inTo :: Zipper t a -> Zipper t (Zipper (Zipper t) a)
    inTo = inToFor toZipper fromZipper
    -- outOf :: Zipper  t         a -> t        a
    -- outOf :: Zipper (Zipper t) a -> Zipper t a
    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 t a = Zipper { diff :: D t a, here :: a }

onDiff :: (D t a -> D u a) -> Zipper t a -> Zipper u a
onDiff f (Zipper d a) = Zipper (f d) a

deriving instance Diff t => Functor (Zipper t)
deriving instance (Eq (D t a), Eq a) => Eq (Zipper t a)
deriving instance (Show (D t a), Show a) => Show (Zipper t a)

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

产品,总和和常数

该Diff (Zipper t)实例依赖于Diff产品:*:,总和:+:,常量Identity和零的实现Proxy.

data (:+:) a b x = InL (a x) | InR (b x)
    deriving (Eq, Show)
data (:*:) a b x = a x :*: b x
    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作为duplicatefor 的正确实现Zipper t.特别是,它为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是一个结构相同的树aTree,但到处都有一个值,而是一个带有值的拉链,以及树的其余部分,所有原始值都保持不变.fmap (fmap extract . duplicate) . inTo $ aTree也是一个结构相同的树aTree,但是每个都有一个值,而不是带有值的拉链,而树的其余部分用所有值替换为相同的值.换一种说法:

fmap extract . duplicate == \z -> fmap (const (here z)) z

完整的测试套件的全部三个Comonad法律extract . duplicate == id,fmap extract . duplicate == id和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

Answer 3

鉴于一个无限可分的Diff类:

class (Functor t, Functor (D t)) => Diff t where
    type D t :: * -> *
    up :: Zipper t a -> t a
    down :: t a -> t (Zipper t a)  
    -- Require that types be infinitely differentiable
    ddiff :: p t -> Dict (Diff (D t))

around可以写成的术语up和down对Zipper的diff的derivitive,基本上如

around z@(Zipper d h) = Zipper ctx z
    where
        ctx = fmap (\z' -> Zipper (up z') (here z')) (down d)

该Zipper t a由一个D t a和a.我们去down了D t a,D t (Zipper (D t) a)每个洞都有拉链.那些拉链由a D (D t) a和a孔中的拉链组成.我们去up了他们每个人,得到了一个D t a并且把它与a洞里的东西一起削减.A D t a和aa Zipper t a,给我们一个D t (Zipper t a),这是一个所需的上下文Zipper t (Zipper t a).

该Comonad实例然后简单地

instance Diff t => Comonad (Zipper t) where
    extract   = here
    duplicate = around

捕获衍生Diff词典需要一些额外的管道,可以使用Data.Constraint或相关答案中提供的方法来完成

around :: Diff t => Zipper t a -> Zipper t (Zipper t a)
around z = Zipper (withDict d' (fmap (\z' -> Zipper (up z') (here z')) (down (diff z)))) z
    where
        d' = ddiff . p' $ z
        p' :: Zipper t x -> Proxy t
        p' = const Proxy