haskell - Zipper Comonads, genéricamente
deriving (3)
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?
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:
- Muévete en ese lado.
- Mueve hacia
upF
de ese lado y haciadownF
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.
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
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