Comonads de cremallera, genéricamente

Dado cualquier tipo de contenedor, podemos formar el Zipper (centrado en elementos) y saber que esta estructura es un Comonad. Esto se exploró recientemente con maravilloso detalle en otra pregunta de Stack Overflow para el siguiente tipo:

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

con la siguiente cremallera

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

Es el caso que Zipes un Comonadaunque la construcción de su instancia es un poco peluda. Dicho esto, Zippuede derivarse completamente mecánicamente de Treey (creo) cualquier tipo derivado de esta manera es automáticamente a Comonad, por lo que creo que debería ser el caso de que podamos construir estos tipos y sus comonads de forma genérica y automática.

Un método para lograr la generalidad para la construcción de cremalleras es el uso de la siguiente clase y familia de tipos

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

que ha aparecido (más o menos) en los hilos de Haskell Cafe y en el blog de Conal Elliott. Esta clase se puede instanciar para los diversos tipos algebraicos centrales y, por lo tanto, proporciona un marco general para hablar sobre las derivadas de ADT.

Entonces, en última instancia, mi pregunta es si podemos o no escribir

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

que podría usarse para subsumir la instancia específica de Comonad descrita anteriormente:

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

Desafortunadamente, no he tenido suerte al escribir una instancia así. ¿Es suficiente la firma inTo/ outOf? ¿Se necesita algo más para restringir los tipos? ¿Es esta instancia siquiera posible?

Al igual que el cazador de niños en Chitty-Chitty-Bang-Bang que atrae a los niños al cautiverio con dulces y juguetes, a los reclutadores de Física les gusta jugar con pompas de jabón y bumeranes, pero cuando la puerta se cierra de golpe, es "Bien, niños, es hora de aprender sobre la diferenciación parcial! ". Yo también. No digas que no te lo advertí.

Aquí hay otra advertencia: el siguiente código necesita {-# LANGUAGE KitchenSink #-}, o mejor dicho

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

sin ningún orden en particular.

Los functores diferenciables dan cremalleras comonádicas

¿Qué es un functor diferenciable, de todos modos?

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}

Es un funtor que tiene una derivada, que también es un funtor. La derivada representa un contexto de un solo agujero para un elemento . El tipo de cremallera ZF f xrepresenta el par de un contexto de un orificio y el elemento en el orificio.

Las operaciones para Diff1describen los tipos de navegación que podemos hacer en cremalleras (sin ninguna noción de "hacia la izquierda" y "hacia la derecha", para lo cual vea mi artículo de Clowns and Jokers ). Podemos ir "hacia arriba", reensamblando la estructura taponando el elemento en su agujero. Podemos ir "hacia abajo", encontrando todas las formas de visitar un elemento en una estructura determinada: decoramos cada elemento con su contexto. Podemos ir "alrededor", tomando una cremallera existente y decorando cada elemento con su contexto, de modo que encontremos todas las formas de reenfocarnos (y cómo mantener nuestro enfoque actual).

Ahora, el tipo de aroundFpodría recordarles a algunos de ustedes

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

¡Y tienes razón en que te lo recuerden! Tenemos, con un salto y un salto,

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

e insistimos en que

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

También lo necesitamos

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

Los functores polinomiales son diferenciables

Los functores constantes son diferenciables.

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

No hay ningún lugar para colocar un elemento, por lo que es imposible formar un contexto. No hay ningún lugar adonde ir upFo downFdesde donde ir , y fácilmente no encontramos ninguno de los caminos a donde ir downF.

El funtor de identidad es diferenciable.

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

Hay un elemento en un contexto trivial, lo downFencuentra, lo upFvuelve a empaquetar y aroundFsolo puede quedarse.

Sum preserva la diferenciabilidad.

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

Las otras partes y piezas son un poco más complicadas. Para ir downF, debemos ir downFdentro del componente etiquetado, luego arreglar las cremalleras resultantes para mostrar la etiqueta en el contexto.

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

Para continuar aroundF, quitamos la etiqueta, averiguamos cómo rodear la cosa sin etiquetar y luego restauramos la etiqueta en todas las cremalleras resultantes. El elemento de enfoque, xse sustituye por la totalidad de su cremallera, 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

Tenga en cuenta que tuve que usar ScopedTypeVariablespara eliminar la ambigüedad de las llamadas recursivas a aroundF. Como función de tipo, DFno es inyectiva, por lo que el hecho de que f' :: D f xno sea suficiente para forzar f' :<-: x :: Z f x.

El producto conserva la diferenciación.

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

Para enfocarse en un elemento de un par, se enfoca en la izquierda y deja la derecha sola, o viceversa. ¡La famosa regla del producto de Leibniz corresponde a una simple intuición espacial!

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)

Ahora, downFfunciona de manera similar a como lo hizo para las sumas, excepto que tenemos que arreglar el contexto de la cremallera no solo con una etiqueta (para mostrar en qué dirección fuimos) sino también con el otro componente intacto.

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

Pero aroundFes una enorme bolsa de risas. Cualquiera que sea el lado que estemos visitando actualmente, tenemos dos opciones:

1. Muévete aroundFpor ese lado.
2. Mover upFde ese lado y downFen el otro lado.

Cada caso requiere que hagamos uso de las operaciones para la subestructura y luego arreglemos los contextos.

  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)

¡Uf! Todos los polinomios son diferenciables y, por lo tanto, nos dan comónadas.

Hmm. Todo es un poco abstracto. Así que agregué deriving Showtodo lo que pude, y agregué

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

que permitió la siguiente interacción (arreglada a mano)

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

Ejercicio Demuestre que la composición de los functores diferenciables es diferenciable, usando la regla de la cadena .

¡Dulce! ¿Podemos ir a casa ahora? Por supuesto no. Aún no hemos diferenciado ninguna estructura recursiva .

Haciendo functores recursivos a partir de bifunctores

A Bifunctor, como explica extensamente la literatura existente sobre programación genérica de tipos de datos (ver el trabajo de Patrik Jansson y Johan Jeuring, o excelentes notas de conferencias de Jeremy Gibbons), es un constructor de tipos con dos parámetros, correspondientes a dos tipos de subestructura. Deberíamos poder "mapear" ambos.

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

Podemos usar Bifunctors para dar la estructura de nodo de contenedores recursivos. Cada nodo tiene subnodos y elementos . Estos pueden ser solo los dos tipos de subestructura.

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

¿Ver? "Atamos el nudo recursivo" en bel primer argumento y mantenemos el parámetro yen el segundo. En consecuencia, obtenemos de una vez por todas

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

Para usar esto, necesitaremos un kit de Bifunctorinstancias.

El kit bifunctor

Las constantes son bifunctoriales.

newtype K a x y = K a

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

Se puede decir que escribí este bit primero, porque los identificadores son más cortos, pero eso es bueno porque el código es más largo.

Las variables son bifunctoriales.

Necesitamos los bifunctores correspondientes a un parámetro u otro, así que hice un tipo de datos para distinguirlos y luego definí un GADT adecuado.

data Var = X | Y

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

Eso hace V X x yuna copia de xy V Y x yuna copia de y. En consecuencia

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

Las sumas y productos de bifunctores son bifunctores

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

Hasta ahora, es repetitivo, pero ahora podemos definir cosas como

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

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

Si desea utilizar estos tipos para datos reales y no quedarse ciego en la tradición puntillista de Georges Seurat, utilice sinónimos de patrones .

Pero, ¿qué pasa con las cremalleras? ¿Cómo demostraremos que Mu bes diferenciable? Tendremos que demostrar que bes diferenciable en ambas variables. ¡Sonido metálico! Es hora de aprender sobre la diferenciación parcial.

Derivadas parciales de bifunctores

Debido a que tenemos dos variables, necesitaremos poder hablar de ellas colectivamente a veces e individualmente en otras ocasiones. Necesitaremos la familia singleton:

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

Ahora podemos decir qué significa que un bifunctor tenga derivadas parciales en cada variable y dar la noción correspondiente de cremallera.

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}

Esta Doperación necesita saber a qué variable apuntar. La cremallera correspondiente Z b vnos dice qué variable vdebe estar enfocada. Cuando "decoramos con contexto", tenemos que decorar x-elementos con X-contextos y y-elementos con Y-contextos. Pero por lo demás, es la misma historia.

Nos quedan dos tareas pendientes: en primer lugar, demostrar que nuestro kit bifunctor es diferenciable; en segundo lugar, mostrar que Diff2 bnos permite establecernos Diff1 (Mu b).

Diferenciando el kit Bifunctor

Me temo que esta parte es más complicada que edificante. Siéntase libre de seguir adelante.

Las constantes son como antes.

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

En esta ocasión, la vida es demasiado corta para desarrollar la teoría del nivel de tipo Kronecker-delta, por lo que acabo de tratar las variables por separado.

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

Para los casos estructurales, encontré útil introducir un ayudante que me permitiera tratar las variables de manera uniforme.

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

Luego construí dispositivos para facilitar el tipo de "re-etiquetado" que necesitamos para downy around. (Por supuesto, vi qué dispositivos necesitaba mientras trabajaba).

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

Y con ese lote listo para funcionar, podemos pulir los detalles. Las sumas son fáciles.

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)

Los productos son un trabajo duro, por eso soy matemático en lugar de ingeniero.

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)

Conceptualmente, es como antes, pero con más burocracia. Los construí usando tecnología de pre-type-hole, usándolos undefinedcomo un talón en lugares en los que no estaba listo para trabajar e introduciendo un error de tipo deliberado en el único lugar (en un momento dado) donde quería una pista útil del comprobador de tipos . Usted también puede tener la verificación de tipos como experiencia de videojuego, incluso en Haskell.

Cremalleras de subnodo para contenedores recursivos

La derivada parcial de bcon respecto a Xnos dice cómo encontrar un subnodo un paso dentro de un nodo, por lo que obtenemos la noción convencional de cremallera.

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

Podemos acercarnos hasta la raíz mediante la inserción repetida de Xposiciones.

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

Pero necesitamos elementos -zippers.

Elementos-cremalleras para puntos de fijación de bifunctores

Cada elemento está en algún lugar dentro de un nodo. Ese nodo está sentado debajo de una pila de Xderivados. Pero la posición del elemento en ese nodo viene dada por una Y-derivada. Obtenemos

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
    }

Audazmente, reclamo

instance Diff2 b => Diff1 (Mu b) where
  type DF (Mu b) = MuCx b

pero antes de desarrollar las operaciones, necesitaré algunos fragmentos.

Puedo intercambiar datos entre functor-zippers y bifunctor-zippers de la siguiente manera:

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

Eso es suficiente para dejarme definir:

  upF z  = muUp (MuZpr {aboveMu = zAboveY z, hereMu = In (up VY (zZipY z))})

Es decir, subimos volviendo a ensamblar primero el nodo donde está el elemento, convirtiendo un elemento-cremallera en un subnodo-cremallera, luego haciendo zoom hacia afuera, como se muestra arriba.

A continuación, digo

  downF  = yOnDown []

para bajar comenzando con la pila vacía, y definir la función auxiliar que va downrepetidamente desde debajo de cualquier pila:

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

Ahora, down bsolo nos lleva dentro del nodo. Las cremalleras que necesitamos también deben llevar el contexto del nodo. Eso es lo que contextualisehace:

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)

Para cada posición Y, debemos dar un elemento-cremallera, por lo que es bueno que conozcamos todo el contexto dXsdesde la raíz, así como también el dYque describe cómo se encuentra el elemento en su nodo. Para cada posición X, hay un subárbol adicional para explorar, ¡así que aumentamos la pila y seguimos adelante!

Eso deja solo el asunto de cambiar el enfoque. Podríamos quedarnos quietos, o bajar de donde estamos, o subir, o subir y luego bajar por algún otro camino. Aquí va.

  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

Como siempre, el elemento existente se reemplaza por su cremallera completa. Por lo que respecta a la belowYparte, buscamos dónde más podemos ir en el nodo existente: encontraremos posiciones de elementos alternativos Yo Xsubnodos adicionales para explorar, así que los contextualiseencontraremos. Por el aboveYlado, debemos trabajar para hacer una copia de seguridad de la pila de X-derivatives después de volver a ensamblar el nodo que estábamos visitando.

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

En cada paso del camino, podemos girar hacia otro lado aroundo seguir subiendo.

¡Y eso es! No he dado una prueba formal de las leyes, pero me parece que las operaciones mantienen cuidadosamente el contexto correctamente a medida que avanzan por la estructura.

¿Qué hemos aprendido?

La diferenciabilidad induce nociones de cosa-en-su-contexto, induciendo una estructura comonádica donde extractte da la cosa y duplicateexplora el contexto buscando otras cosas para contextualizar. Si tenemos la estructura diferencial adecuada para los nodos, podemos desarrollar una estructura diferencial para árboles completos.

Ah, y tratar a cada aridad individual de constructor de tipos por separado es descaradamente horrendo. La mejor forma es trabajar con functores entre conjuntos indexados

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

donde hacemos odiferentes tipos de estructura almacenando idiferentes tipos de elementos. Estos están cerrados bajo la construcción jacobiana.

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

donde cada una de las (o, i)estructuras resultantes es una derivada parcial, lo que le indica cómo hacer un iagujero de elemento en una oestructura. Pero eso es divertido de manera dependiente, para otro momento.

La Comonadinstancia de cremalleras no es

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

de dónde outOfy inTovienen de la Diffinstancia por Zipper tsí misma. La instancia anterior viola la Comonadley fmap extract . duplicate == id. En cambio, se comporta como:

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

Diferenciar (cremallera t)

La Diffinstancia de Zipperse proporciona identificándolos como productos y reutilizando el código para los productos (a continuación).

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

Dado un isomorfismo entre los tipos de datos y un isomorfismo entre sus derivados, podemos reutilizar un tipo inToy outOfel otro.

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

Para los tipos que son solo newTypes para una Diffinstancia existente , sus derivados son del mismo tipo. Si le decimos al verificador de tipos sobre la igualdad de tipos D r ~ D t, podemos aprovechar eso en lugar de proporcionar un isomorfismo para las derivadas.

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

Equipados con estas herramientas, podemos reutilizar la Diffinstancia de productos para implementarDiff (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

Calderería

Para poder utilizar realmente el código presentado aquí, necesitamos algunas extensiones de lenguaje, importaciones y una reformulación del problema propuesto.

{-# 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

Productos, sumas y constantes

La Diff (Zipper t)instancia se basa en implementaciones de Diffproductos :*:, sumas :+:, constantes Identityy cero 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

Ejemplo de contenedor

Planteé el Binejemplo como un isomorfismo a una suma de productos. Necesitamos no solo su derivada sino también su segunda derivada

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

Los datos de ejemplo de la respuesta anterior son

aTree :: Bin Int    
aTree =
    (Bin . InL) (
        (Bin . InL) (
            (Bin . InR) (Identity 2)
            :*: (Identity 1) :*:
            (Bin . InR) (Identity 3)
        )
        :*: (Identity 0) :*:
        (Bin . InR) (Identity 4)
    )

No es la instancia de Comonad

El Binejemplo anterior proporciona un contraejemplo de fmap outOf . inTola implementación correcta de duplicatefor Zipper t. En particular, proporciona un contraejemplo a la fmap extract . duplicate = idley:

fmap ( \z -> (fmap extract . duplicate) z == z) . inTo $ aTree

Lo que evalúa a (observe cómo está lleno de Falses en todas partes, cualquiera Falsesería suficiente para refutar la ley)

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 aTreees un árbol con la misma estructura que aTree, pero dondequiera que haya un valor, hay una cremallera con el valor, y el resto del árbol con todos los valores originales intactos. fmap (fmap extract . duplicate) . inTo $ aTreetambién es un árbol con la misma estructura que aTree, pero cada vez que hay un valor, hay una cremallera con el valor, y el resto del árbol con todos los valores reemplazados por ese mismo valor . En otras palabras:

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

La prueba completa de baño para las tres Comonadleyes, extract . duplicate == id, fmap extract . duplicate == id, y duplicate . duplicate == fmap duplicate . duplicatees

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

Dada una Diffclase infinitamente diferenciable :

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

aroundpuede escribirse en términos de upy downsobre la derivada de Zipperla diff's, esencialmente como

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

El Zipper t aconsta de una D t ay una a. Vamos downla D t a, para conseguir una D t (Zipper (D t) a)con una cremallera en cada hoyo. Esas cremalleras consisten en una D (D t) ay la aque estaba en el agujero. Vamos a upcada uno de ellos, cogiendo un D t ay emparejándolo con el aque estaba en el agujero. A D t ay an ahacen a Zipper t a, dándonos a D t (Zipper t a), que es el contexto necesario para a Zipper t (Zipper t a).

La Comonadinstancia es entonces simplemente

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

La captura del Diffdiccionario del derivado requiere un poco de plomería adicional, que se puede hacer con Data.Constraint o en términos del método presentado en una respuesta relacionada

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