haskell - Zipper Comonads, genéricamente

deriving

Question

Dado cualquier tipo de contenedor, podemos formar Zipper (centrado en el elemento) y saber que esta estructura es una Comonad. Esto se exploró recientemente con detalles maravillosos en otra pregunta sobre desbordamiento de pila 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 de que Zip sea ​​un Comonad aunque la construcción de su instancia es un poco peluda. Dicho esto, Zip puede derivarse mecánicamente de Tree y (creo) cualquier tipo derivado de esta manera es automáticamente Comonad , así 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 familia de clase y tipo

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 se ha mostrado (más o menos) en las conversaciones de Haskell Cafe y en el blog de Conal Elliott. Esta clase puede crearse una instancia para los diversos tipos algebraicos centrales y, por lo tanto, proporciona un marco general para hablar sobre los derivados de los 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) }
...

Lamentablemente, no he tenido suerte escribiendo esta instancia. ¿Es suficiente la firma inTo / outOf ? ¿Hay algo más necesario para restringir los tipos? ¿Es esta instancia incluso posible?

Answer 1

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

Aquí hay otra advertencia: el siguiente código necesita {-# LANGUAGE KitchenSink #-} , o más bien

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

sin ningún orden en particular.

Functors 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 functor que tiene un derivado, que también es un funtor. La derivada representa un contexto de un agujero para un elemento . La cremallera tipo ZF fx representa el par de un contexto de un agujero y el elemento en el agujero.

Las operaciones para Diff1 describen los tipos de navegación que podemos hacer en las cremalleras (sin ninguna noción de "hacia la izquierda" y "hacia la derecha", para los cuales vea mi papel de Clowns and Jokers ). Podemos ir "hacia arriba", volviendo a ensamblar la estructura al tapar el elemento en su agujero. Podemos ir "hacia abajo", encontrando todos los caminos para visitar un elemento en una estructura de dar: decoramos cada elemento con su contexto. Podemos "dar la vuelta", tomar una cremallera existente y decorar cada elemento con su contexto, por lo que encontramos todas las formas de reenfoque (y cómo mantener nuestro enfoque actual).

Ahora, el tipo de aroundF podrí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 para 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 necesitamos eso

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 funtores polinomiales son diferenciables

Los funtores 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 poner un elemento, por lo que es imposible formar un contexto. No hay ningún lugar para ir hacia upF o hacia downF desde, y encontramos fácilmente ninguna de las formas de ir hacia downF .

El functor 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, downF encuentra, upF reempaqueta, y aroundF solo puede quedarse.

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

Los otros bits y piezas son un poco más de un puñado. Para ir downF , debemos ir downF dentro 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 ir aroundF , tiramos la etiqueta, descubrimos cómo rodear la cosa sin etiquetar, luego restauramos la etiqueta en todas las cremalleras resultantes. El elemento en foco, x , se reemplaza por su cremallera completa, 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 ScopedTypeVariables para ScopedTypeVariables de las llamadas recursivas a aroundF . Como función de tipo, DF no es inyectiva, por lo que el hecho de que f'' :: D fx no sea suficiente para forzar a f'' :<-: x :: Z fx .

El producto preserva la diferenciabilidad.

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 centrarse en un elemento de un par, o bien se centra en la izquierda y deja el derecho solo, o viceversa. ¡La famosa regla de producto de Leibniz corresponde a una intuición espacial simple!

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, downF funciona de manera similar a como lo hacía con las sumas, excepto que tenemos que arreglar el contexto de la cremallera no solo con una etiqueta (para mostrar en qué dirección nos dirigimos) 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 aroundF es una bolsa masiva de risas. Cualquiera sea el lado que estemos visitando actualmente, tenemos dos opciones:

1. Muévete en ese lado.
2. Mueve hacia upF de ese lado y hacia downF hacia el otro lado.

Cada caso requiere que hagamos uso de las operaciones para la subestructura, 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! Los polinomios son todos diferenciables, y por lo tanto nos dan comonads.

Hmm. Es todo un poco abstracto. Así que agregué deriving Show todo lo que pude y lancé

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

lo 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 Mostrar que la composición de los funtores diferenciables es diferenciable, utilizando la regla de la cadena .

¡Dulce! ¿Podemos ir a casa ahora? Por supuesto no. No hemos diferenciado ninguna estructura recursiva todavía.

Hacer funtores recursivos de bifunctors

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

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

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

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

¿Ver? "Atamos el nudo recursivo" en el primer argumento de b , y mantenemos el parámetro y en el segundo. En consecuencia, obtenemos 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 instancias de Bifunctor .

El kit Bifunctor

Las constantes son bifuncionales.

newtype K a x y = K a
instance Bifunctor (K a) where
bimap f g (K a) = K a

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

Necesitamos los bifuncionantes correspondientes a un parámetro u otro, así que hice un tipo de datos para distinguirlos, 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 que VX xy una copia de VY xy una 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 bifunctors son 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

Hasta ahora, tan 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 de datos reales y no quedarse ciego en la tradición puntillista de Georges Seurat, use sinónimos de patrones .

Pero, ¿y las cremalleras? ¿Cómo demostraremos que Mu b es diferenciable? Tendremos que mostrar que b es diferenciable en ambas variables. ¡Sonido metálico! Es hora de aprender sobre la diferenciación parcial.

Derivadas parciales de bifuncionantes

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

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

Ahora podemos decir lo que significa para un Bifunctor tener 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 operación D necesita saber qué variable atacar. La cremallera correspondiente Z bv nos dice qué variable v debe estar en foco. Cuando "decoramos con contexto", tenemos que decorar elementos x con X -contextos y elementos- y con -contextos. Pero de lo contrario, es la misma historia.

Tenemos dos tareas restantes: en primer lugar, para demostrar que nuestro kit bifunctor es diferenciable; en segundo lugar, para mostrar que Diff2 b nos permite establecer Diff1 (Mu b) .

Diferenciando el kit Bifunctor

Me temo que este poco es complicado en lugar de edificante. Siéntete libre de saltarte.

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 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í gadgets para facilitar el tipo de "retagging" que necesitamos para down around y around . (Por supuesto, vi qué gadgets 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 ir, 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 lo que soy un matemático en lugar de un 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 igual que antes, pero con más burocracia. Construí estos usando la tecnología de pre-type-hole, usando undefined como un stub en lugares donde no estaba listo para trabajar, e introduciendo un error de tipo deliberado en un solo lugar (en un momento dado) donde quería una sugerencia útil del typechecker Usted también puede tener la experiencia de verificación de tipografía como videojuego, incluso en Haskell.

Cremalleras de subnodos para recipientes recursivos

La derivada parcial de b con respecto a X nos 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 hacer un zoom hasta la raíz repitiendo repetidamente las posiciones 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))})

Pero necesitamos elementos -zippers.

Elemento-cremalleras para puntos de fijación de bifunctors

Cada elemento está en algún lugar dentro de un nodo. Ese nodo está sentado debajo de una pila de X derivados. Pero la posición del elemento en ese nodo viene dada por una Y derivativa. 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, yo reclamo

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

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

Puedo intercambiar datos entre funcionador-cremalleras y cremalleras bifunctor 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 al volver a armar el nodo donde se encuentra el elemento, convirtiendo una cremallera de elemento en una cremallera de subnodo, y luego haciendo zoom hasta el final, como se indicó anteriormente.

A continuación, digo

 downF = yOnDown []

para bajar comenzando con la pila vacía, y definir la función de ayuda que down repetidamente desde abajo 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 b solo nos lleva dentro del nodo. Las cremalleras que necesitamos también deben llevar el contexto del nodo. Eso es lo que hace la contextualise :

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 Y -position, debemos dar un elemento-zipper, por lo que es bueno que conozcamos todo el contexto dXs vuelta a la raíz, así como el dY que describe cómo se sienta el elemento en su nodo. Para cada X -position, hay un subárbol adicional para explorar, ¡así que crecemos la pila y seguimos adelante!

Eso solo deja el negocio de cambiar el enfoque. Podríamos quedarnos o bajar de donde estamos, subir o subir y bajar por 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 es reemplazado por su cremallera completa. Para la parte de belowY , buscamos en qué otro lugar podemos ir en el nodo existente: encontraremos el elemento alternativo Y -positions o más X -subnodes para explorar, por lo que los contextualise . Para la parte anterior, debemos volver a la pila de X derivados después de volver a armar 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 dar la vuelta a cualquier otro lugar o 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 rastrean la estructura.

¿Qué hemos aprendido?

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

Ah, y tratar cada aridad individual del constructor de tipo por separado es evidentemente horrendo. La mejor manera es trabajar con funtores entre conjuntos indexados

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

donde hacemos diferentes tipos de estructuras almacenando diferentes tipos de elementos. Estos se cierran bajo la construcción jacobiana

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

donde cada una de las estructuras resultantes (o, i) es una derivada parcial, que le indica cómo hacer un i -agujero de elementos en una estructura o . Pero eso es diversión dependiente de tipo, para otro momento.

Answer 2

Dada una clase Diff 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))

se puede escribir en términos de up y down en el derivado de la diff Zipper , esencialmente como

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

La Zipper ta consiste en una D ta y una a . Bajamos down la D ta , obteniendo una D t (Zipper (D t) a) con una cremallera en cada hoyo. Esas cremalleras consisten en un D (D t) a el a que estaba en el agujero. Subimos up cada uno de ellos, sacamos una D ta y la nivelamos con la a que estaba en el hoyo. A D ta y a a hacen un Zipper ta , dándonos un D t (Zipper ta) , que es el contexto necesario para un Zipper t (Zipper ta) .

La instancia de Comonad es entonces simplemente

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

La captura del diccionario Diff la derivada 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

Answer 3

La instancia de Comonad para cremalleras no es

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

donde outOf y inTo vienen de la instancia Diff para Zipper t sí. La instancia anterior viola el fmap extract . duplicate == id Comonad ley de fmap extract . duplicate == id fmap extract . duplicate == id . En cambio, se comporta como:

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

Diff (Cremallera t)

La instancia de Diff para Zipper se proporciona identificándolos como productos y reutilizando el código de 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 de inTo y outOf para el 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 simplemente newTypes para una instancia de Diff existente, sus derivados son del mismo tipo. Si le decimos al verificador de tipos sobre ese tipo de igualdad D r ~ D t , podemos aprovechar eso en lugar de proporcionar un isomorfismo para los derivados.

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

Equipado con estas herramientas, podemos reutilizar la instancia Diff para productos para implementar 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

Boilerplate

Para utilizar realmente el código presentado aquí, necesitamos algunas extensiones de idioma, 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 instancia Diff (Zipper t) basa en implementaciones de Diff para productos :*: sumas :+: constantes Identity y zero 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

Puse el ejemplo Bin como un isomorfismo a una suma de productos. No solo necesitamos su derivado 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 ejemplo de Bin anterior proporciona un contraejemplo para fmap outOf . inTo fmap outOf . inTo ser la implementación correcta de duplicate para Zipper t . En particular, proporciona un contraejemplo al fmap extract . duplicate = id fmap extract . duplicate = id ley de fmap extract . duplicate = id :

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

Lo cual se evalúa como (observe cómo está lleno de False s en todas partes, cualquier False serí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 aTree es un árbol con la misma estructura que a aTree , pero en todas partes había un valor, en cambio, había una cremallera con el valor y el resto del árbol con todos los valores originales intactos. fmap (fmap extract . duplicate) . inTo $ aTree fmap (fmap extract . duplicate) . inTo $ aTree también es un árbol con la misma estructura que aTree , pero cada vez que había un valor, en cambio, había 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

El conjunto de pruebas completo para las tres leyes de Comonad , extract . duplicate == id extract . duplicate == id , fmap extract . duplicate == id fmap extract . duplicate == id y duplicate . duplicate == fmap duplicate . duplicate duplicate . duplicate == fmap duplicate . duplicate duplicate . duplicate == fmap duplicate . duplicate es

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