haskell - Escribir cojoin o cobind para tipo de rejilla n-dimensional

comonad

Question

Utilizando la definición típica de elementos naturales de nivel de tipo, he definido una cuadrícula n-dimensional.

{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}

data Nat = Z | S Nat

data U (n :: Nat) x where
  Point :: x -> U Z x
  Dimension :: [U n x] -> U n x -> [U n x] -> U (S n) x

dmap :: (U n x -> U m r) -> U (S n) x -> U (S m) r
dmap f (Dimension ls mid rs) = Dimension (map f ls) (f mid) (map f rs)

instance Functor (U n) where
  fmap f (Point x) = Point (f x)
  fmap f d@Dimension{} = dmap (fmap f) d

Ahora quiero que sea una instancia de Comonad, pero no puedo adaptar mi cerebro a eso.

class Functor w => Comonad w where
  (=>>)    :: w a -> (w a -> b) -> w b
  coreturn :: w a -> a
  cojoin   :: w a -> w (w a)

  x =>> f = fmap f (cojoin x)
  cojoin xx = xx =>> id

instance Comonad (U n) where
  coreturn (Point x) = x
  coreturn (Dimension _ mid _) = coreturn mid

  -- cojoin :: U Z x -> U Z (U Z x)
  cojoin (Point x) = Point (Point x)
  -- cojoin ::U (S n) x -> U (S n) (U (S n) x)
  cojoin d@Dimension{} = undefined

  -- =>> :: U Z x -> (U Z x -> r) -> U Z r
  p@Point{} =>> f = Point (f p)
  -- =>> :: U (S n) x -> (U (S n) x -> r) -> U (S n) r
  d@Dimension{} =>> f = undefined

El uso de cojoin en una grilla n-dimensional producirá una grilla n-dimensional de grillas n-dimensionales. Me gustaría proporcionar una instancia con la misma idea que esta , que es que el valor de la cuadrícula combinada en (x, y, z) debe ser la cuadrícula original centrada en (x, y, z). Para adaptar ese código, parece que necesitamos reificar n para realizar n "fmaps" n "rollos". No tienes que hacerlo de esa manera, pero si eso te ayuda, entonces ahí tienes.

Answer 1

Entonces esto resulta ser incorrecto. Lo dejaré aquí en caso de que alguien quiera intentar arreglarlo.

Esta implementación es la forma en que sugirió @pigworker, creo. Compila, pero no lo he probado. (Tomé la implementación de cojoin1 de http://blog.sigfpe.com/2006/12/evaluating-cellular-automata-is.html )

{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}

data Nat = Z | S Nat

data U (n :: Nat) x where
  Point :: x -> U Z x
  Dimension :: [U n x] -> U n x -> [U n x] -> U (S n) x

unPoint :: U Z x -> x
unPoint (Point x) = x

dmap :: (U n x -> U m r) -> U (S n) x -> U (S m) r
dmap f (Dimension ls mid rs) = Dimension (map f ls) (f mid) (map f rs)

right, left :: U (S n) x -> U (S n) x
right (Dimension a b (c:cs)) = Dimension (b:a) c cs
left  (Dimension (a:as) b c) = Dimension as a (b:c)

instance Functor (U n) where
  fmap f (Point x) = Point (f x)
  fmap f d@Dimension{} = dmap (fmap f) d

class Functor w => Comonad w where
  (=>>)    :: w a -> (w a -> b) -> w b
  coreturn :: w a -> a
  cojoin   :: w a -> w (w a)

  x =>> f = fmap f (cojoin x)
  cojoin xx = xx =>> id

instance Comonad (U n) where
  coreturn (Point x) = x
  coreturn (Dimension _ mid _) = coreturn mid
  cojoin (Point x) = Point (Point x)
  cojoin d@Dimension{} = fmap unlayer . unlayer . fmap dist . cojoin1 . fmap cojoin . layer $ d

dist :: U (S Z) (U n x) -> U n (U (S Z) x)
dist = layerUnder . unlayer

layerUnder :: U (S n) x -> U n (U (S Z) x)
layerUnder d@(Dimension _ Point{} _) = Point d
layerUnder d@(Dimension _ Dimension{} _) = dmap layerUnder d

unlayer :: U (S Z) (U n x) -> U (S n) x
unlayer = dmap unPoint

layer :: U (S n) x -> U (S Z) (U n x)
layer = dmap Point

cojoin1 :: U (S Z) x -> U (S Z) (U (S Z) x)
cojoin1 a = layer $ Dimension (tail $ iterate left a) a (tail $ iterate right a)

Answer 2

Una prueba más, inspirada en publicaciones de pigworkers y hackage.haskell.org/packages/archive/representable-functors/… .

¡Un functor representable (o naperiano) es una comonad en sí mismo, si la clave (o log) es un monoide! Entonces coreturn obtiene el valor en la posición mempty . Y cojoin mappend s las dos teclas que tiene disponibles. (Así como la instancia de comonad para (p ->) .)

{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}

import Data.List (genericIndex)
import Data.Monoid
import Data.Key
import Data.Functor.Representable

data Nat = Z | S Nat

data U (n :: Nat) x where
  Point :: x -> U Z x
  Dimension :: [U n x] -> U n x -> [U n x] -> U (S n) x

dmap :: (U n x -> U m r) -> U (S n) x -> U (S m) r
dmap f (Dimension ls mid rs) = Dimension (map f ls) (f mid) (map f rs)

instance Functor (U n) where
  fmap f (Point x) = Point (f x)
  fmap f d@Dimension{} = dmap (fmap f) d

class Functor w => Comonad w where
  (=>>)    :: w a -> (w a -> b) -> w b
  coreturn :: w a -> a
  cojoin   :: w a -> w (w a)

  x =>> f = fmap f (cojoin x)
  cojoin xx = xx =>> id

U es representable si las listas son infinitamente largas. Entonces solo hay una forma. La clave de U n es un vector de n enteros.

type instance Key (U n) = UKey n

data UKey (n :: Nat) where
  P :: UKey Z
  D :: Integer -> UKey n -> UKey (S n)

instance Lookup (U n) where lookup = lookupDefault
instance Indexable (U n) where
  index (Point x) P = x
  index (Dimension ls mid rs) (D i k) 
    | i < 0 = index (ls `genericIndex` (-i - 1)) k
    | i > 0 = index (rs `genericIndex` ( i - 1)) k
    | otherwise = index mid k

Necesitamos dividir la instancia Representable en dos casos, uno para Z y otro para S , porque no tenemos un valor de tipo U n para coincidencia de patrones.

instance Representable (U Z) where
  tabulate f = Point (f P)
instance Representable (U n) => Representable (U (S n)) where
  tabulate f = Dimension 
    (map (/i -> tabulate (f . D (-i))) [1..]) 
    (tabulate (f . D 0))
    (map (/i -> tabulate (f . D   i)) [1..])

instance Monoid (UKey Z) where
  mempty = P
  mappend P P = P
instance Monoid (UKey n) => Monoid (UKey (S n)) where
  mempty = D 0 mempty
  mappend (D il kl) (D ir kr) = D (il + ir) (mappend kl kr)

Y la clave de U n es de hecho un monoide, por lo que podemos convertir a U n en una comonad, usando las implementaciones predeterminadas del paquete representable-funtor.

instance (Monoid (UKey n), Representable (U n)) => Comonad (U n) where
  coreturn = extractRep
  cojoin = duplicateRep
  (=>>) = flip extendRep

Esta vez hice algunas pruebas.

testVal :: U (S (S Z)) Int
testVal = Dimension 
  (repeat (Dimension (repeat (Point 1)) (Point 2) (repeat (Point 3))))
          (Dimension (repeat (Point 4)) (Point 5) (repeat (Point 6)))
  (repeat (Dimension (repeat (Point 7)) (Point 8) (repeat (Point 9))))

-- Hacky Eq instance, just for testing
instance Eq x => Eq (U n x) where
  Point a == Point b = a == b
  Dimension la a ra == Dimension lb b rb = take 3 la == take 3 lb && a == b && take 3 ra == take 3 rb

instance Show x => Show (U n x) where
  show (Point x) = "(Point " ++ show x ++ ")"
  show (Dimension l a r) = "(Dimension " ++ show (take 2 l) ++ " " ++ show a ++ " " ++ show (take 2 r) ++ ")"

test = 
  coreturn (cojoin testVal) == testVal && 
  fmap coreturn (cojoin testVal) == testVal && 
  cojoin (cojoin testVal) == fmap cojoin (cojoin testVal)

Answer 3

Jagger / Richards: no siempre puedes obtener lo que quieres, pero si lo intentas alguna vez, es posible que encuentres que obtienes lo que necesitas.

Cursores en listas

Permítanme reconstruir los componentes de su estructura usando snoc- y cons-lists para mantener claras las propiedades espaciales. Yo defino

data Bwd x = B0 | Bwd x :< x deriving (Functor, Foldable, Traversable, Show)
data Fwd x = F0 | x :> Fwd x deriving (Functor, Foldable, Traversable, Show)
infixl 5 :<
infixr 5 :>

data Cursor x = Cur (Bwd x) x (Fwd x) deriving (Functor, Foldable, Traversable, Show)

Tengamos comonads

class Functor f => Comonad f where
  counit  :: f x -> x
  cojoin  :: f x -> f (f x)

y asegurémonos de que los cursores sean comonads

instance Comonad Cursor where
  counit (Cur _ x _) = x
  cojoin c = Cur (lefts c) c (rights c) where
    lefts (Cur B0 _ _) = B0
    lefts (Cur (xz :< x) y ys) = lefts c :< c where c = Cur xz x (y :> ys)
    rights (Cur _ _ F0) = F0
    rights (Cur xz x (y :> ys)) = c :> rights c where c = Cur (xz :< x) y ys

Si está conectado a este tipo de cosas, InContext [] que Cursor es una variante espacialmente agradable de InContext []

InContext f x = (x, ∂f x)

donde ∂ toma la derivada formal de un funtor, dando su noción de contexto de un agujero. InContext f es siempre una Comonad , como se menciona en esta respuesta , y lo que tenemos aquí es simplemente esa Comonad inducida por la estructura diferencial, donde counit extrae el elemento en el foco y cojoin decora cada elemento con su propio contexto, efectivamente dándole una contexto lleno de cursores reenfocados y con un cursor inmóvil en su foco. Vamos a tener un ejemplo.

> cojoin (Cur (B0 :< 1) 2 (3 :> 4 :> F0))
Cur (B0 :< Cur B0 1 (2 :> 3 :> 4 :> F0))
    (Cur (B0 :< 1) 2 (3 :> 4 :> F0))
    (  Cur (B0 :< 1 :< 2) 3 (4 :> F0)
    :> Cur (B0 :< 1 :< 2 :< 3) 4 F0
    :> F0)

¿Ver? El 2 en foco ha sido decorado para convertirse en el cursor-en-2; a la izquierda, tenemos la lista del cursor-a-1; a la derecha, la lista del cursor-a-3 y el cursor-a-4.

Componer cursores, transposición de cursores?

Ahora, la estructura que estás pidiendo que sea una Comonad es la composición n-fold de Cursor . Tengamos

newtype (:.:) f g x = C {unC :: f (g x)} deriving Show

Para persuadir a las comonads f g a componer, los counit componen bien, pero se necesita una "ley distributiva"

transpose :: f (g x) -> g (f x)

para que pueda hacer que el compuesto se cojoin como este

f (g x)
  -(fmap cojoin)->
f (g (g x))
  -cojoin->
f (f (g (g x)))
  -(fmap transpose)->
f (g (f (g x)))

¿Qué leyes deberían transpose ? Probablemente algo así como

counit . transpose = fmap counit
cojoin . transpose = fmap transpose . transpose . fmap cojoin

o lo que sea necesario para garantizar que cualquiera de las dos formas de shoogle alguna secuencia de f''s yg de una orden a otra dé el mismo resultado.

¿Podemos definir una transpose para Cursor consigo mismo? Una forma de obtener algún tipo de transposición a bajo costo es notar que Bwd y Fwd son muy rápidos , por lo que también lo es Cursor .

instance Applicative Bwd where
  pure x = pure x :< x
  (fz :< f) <*> (sz :< s) = (fz <*> sz) :< f s
  _ <*> _ = B0

instance Applicative Fwd where
  pure x = x :> pure x
  (f :> fs) <*> (s :> ss) = f s :> (fs <*> ss)
  _ <*> _ = F0

instance Applicative Cursor where
  pure x = Cur (pure x) x (pure x)
  Cur fz f fs <*> Cur sz s ss = Cur (fz <*> sz) (f s) (fs <*> ss)

Y aquí deberías comenzar a oler a la rata. La falta de coincidencia de la forma da como resultado el truncamiento , y eso va a romper la propiedad obviamente deseable que la auto-transposición es auto-inversa. Cualquier tipo de hastío no sobrevivirá. Obtenemos un operador de transposición: sequenceA , y para datos completamente regulares, todo es brillante y hermoso.

> regularMatrixCursor
Cur (B0 :< Cur (B0 :< 1) 2 (3 :> F0))
          (Cur (B0 :< 4) 5 (6 :> F0))
          (Cur (B0 :< 7) 8 (9 :> F0) :> F0)
> sequenceA regularMatrixCursor
Cur (B0 :< Cur (B0 :< 1) 4 (7 :> F0))
          (Cur (B0 :< 2) 5 (8 :> F0))
          (Cur (B0 :< 3) 6 (9 :> F0) :> F0)

Pero incluso si solo muevo uno de los cursores internos fuera de alineación (no importa hacer los tamaños irregulares), las cosas salen mal.

> raggedyMatrixCursor
Cur (B0 :< Cur ((B0 :< 1) :< 2) 3 F0)
          (Cur (B0 :< 4) 5 (6 :> F0))
          (Cur (B0 :< 7) 8 (9 :> F0) :> F0)
> sequenceA raggedyMatrixCursor
Cur (B0 :< Cur (B0 :< 2) 4 (7 :> F0))
          (Cur (B0 :< 3) 5 (8 :> F0))
          F0

Cuando tiene una posición de cursor exterior y múltiples posiciones de cursor interno, no hay transposición que se comporte bien. El Cursor permite que las estructuras interiores se cojoin entre sí, por lo que no se transpose , no se cojoin . Puedes, y yo lo hice, definir

instance (Comonad f, Traversable f, Comonad g, Applicative g) =>
  Comonad (f :.: g) where
    counit = counit . counit . unC
    cojoin = C . fmap (fmap C . sequenceA) . cojoin . fmap cojoin . unC

pero es nuestra responsabilidad asegurarnos de mantener las estructuras internas de forma regular. Si está dispuesto a aceptar esa carga, puede iterar, porque Applicative y Traversable se cierran fácilmente en la composición. Aquí están los pedazos y pedazos

instance (Functor f, Functor g) => Functor (f :.: g) where
  fmap h (C fgx) = C (fmap (fmap h) fgx)

instance (Applicative f, Applicative g) => Applicative (f :.: g) where
  pure = C . pure . pure
  C f <*> C s = C (pure (<*>) <*> f <*> s)

instance (Functor f, Foldable f, Foldable g) => Foldable (f :.: g) where
  fold = fold . fmap fold . unC

instance (Traversable f, Traversable g) => Traversable (f :.: g) where
  traverse h (C fgx) = C <$> traverse (traverse h) fgx

Editar: para completar, esto es lo que hace cuando todo es regular,

> cojoin (C regularMatrixCursor)
C {unC = Cur (B0 :< Cur (B0 :<
  C {unC = Cur B0 (Cur B0 1 (2 :> (3 :> F0))) (Cur B0 4 (5 :> (6 :> F0)) :> (Cur B0 7 (8 :> (9 :> F0)) :> F0))}) 
 (C {unC = Cur B0 (Cur (B0 :< 1) 2 (3 :> F0)) (Cur (B0 :< 4) 5 (6 :> F0) :> (Cur (B0 :< 7) 8 (9 :> F0) :> F0))})
 (C {unC = Cur B0 (Cur ((B0 :< 1) :< 2) 3 F0) (Cur ((B0 :< 4) :< 5) 6 F0 :> (Cur ((B0 :< 7) :< 8) 9 F0 :> F0))} :> F0))
(Cur (B0 :<
  C {unC = Cur (B0 :< Cur B0 1 (2 :> (3 :> F0))) (Cur B0 4 (5 :> (6 :> F0))) (Cur B0 7 (8 :> (9 :> F0)) :> F0)})
 (C {unC = Cur (B0 :< Cur (B0 :< 1) 2 (3 :> F0)) (Cur (B0 :< 4) 5 (6 :> F0)) (Cur (B0 :< 7) 8 (9 :> F0) :> F0)}) 
 (C {unC = Cur (B0 :< Cur ((B0 :< 1) :< 2) 3 F0) (Cur ((B0 :< 4) :< 5) 6 F0) (Cur ((B0 :< 7) :< 8) 9 F0 :> F0)} :> F0))
(Cur (B0 :<
  C {unC = Cur ((B0 :< Cur B0 1 (2 :> (3 :> F0))) :< Cur B0 4 (5 :> (6 :> F0))) (Cur B0 7 (8 :> (9 :> F0))) F0})
 (C {unC = Cur ((B0 :< Cur (B0 :< 1) 2 (3 :> F0)) :< Cur (B0 :< 4) 5 (6 :> F0)) (Cur (B0 :< 7) 8 (9 :> F0)) F0})
 (C {unC = Cur ((B0 :< Cur ((B0 :< 1) :< 2) 3 F0) :< Cur ((B0 :< 4) :< 5) 6 F0) (Cur ((B0 :< 7) :< 8) 9 F0) F0} :> F0)
:> F0)}

Producto Tensor de Hancock

Para la regularidad, necesitas algo más fuerte que la composición. Debe poder capturar la noción de "una estructura f de estructuras-g-todas-iguales-forma". Esto es lo que el inestimable Peter Hancock llama el "producto tensorial", que escribiré f :><: g : hay una forma de f "externa" y una forma de g "interna" común a todas las estructuras g internas , entonces la transposición es fácilmente definible y siempre auto inverso. El tensor de Hancock no es convenientemente definible en Haskell, pero en un contexto dependiente de tipeo, es fácil formular una noción de "contenedor" que tenga este tensor.

Para darle la idea, considere una noción degenerada de contenedor

data (:<|) s p x = s :<| (p -> x)

donde decimos s es el tipo de "formas" p el tipo de "posiciones". Un valor consiste en la elección de una forma y el almacenamiento de una x en cada posición. En el caso dependiente, el tipo de posiciones puede depender de la elección de la forma (por ejemplo, para las listas, la forma es un número (la longitud), y usted tiene esa cantidad de posiciones). Estos contenedores tienen un producto tensor

(s :<| p) :><: (s'' :<| p'')  =  (s, s'') :<| (p, p'')

que es como una matriz generalizada: un par de formas dan las dimensiones, y luego tienes un elemento en cada par de posiciones. Puedes hacer esto perfectamente bien cuando los tipos p y p'' dependen de los valores en s y s'' , y esa es exactamente la definición de Hancock del producto tensorial de los contenedores.

InContext para productos tensores

Ahora, como habrás aprendido en la escuela secundaria, ∂(s :<| p) = (s, p) :<| (p-1) ∂(s :<| p) = (s, p) :<| (p-1) donde p-1 es de algún tipo con un elemento menos que p . Como ∂ (s x ^ p) = (s p) * x ^ (p-1). Selecciona una posición (registrándola en la forma) y la elimina. El inconveniente es que p-1 es difícil de conseguir sin tipos dependientes. Pero InContext selecciona una posición sin eliminarla .

InContext (s :<| p) ~= (s, p) :<| p

Esto funciona igual de bien para el caso dependiente, y nosotros adquirimos gozosamente

InContext (f :><: g) ~= InContext f :><: InContext g

Ahora sabemos que InContext f es siempre una Comonad , y esto nos dice que los productos tensores de InContext s son comonadic porque ellos mismos son InContext s. Es decir, usted elige una posición por dimensión (y eso le da exactamente una posición en todo), donde antes teníamos una posición externa y muchas posiciones internas. Con el producto tensor reemplazando la composición, todo funciona dulcemente.

Funtores Naperianos

Pero hay una subclase de Functor para la cual el producto tensorial y la composición coinciden. Estos son los f Functor para los cuales f () ~ () : es decir, solo hay una forma de todos modos, por lo que los valores raídos en las composiciones se descartan en primer lugar. Estos Functor son todos isomorfos a (p ->) para un conjunto de posiciones p que podemos considerar como el logaritmo (el exponente al cual x debe elevarse para dar fx ). En consecuencia, Hancock llama a estos funtores Naperian después de John Napier (cuyo fantasma atormenta la parte de Edimburgo donde vive Hancock).

class Applicative f => Naperian f where
  type Log f
  project :: f x -> Log f -> x
  positions :: f (Log f)
  --- project positions = id

Un functor de Naperian tiene un logaritmo, lo que induce una función de iones de project posiciones a los elementos que se encuentran allí. Naperian funtores Naperian son todos zippily Applicative , con pure y <*> correspondientes a los K y S combinators para las proyecciones. También es posible construir un valor donde en cada posición se almacena la representación de esa misma posición. Las leyes de los logaritmos que puede recordar aparecen de forma agradable.

newtype Id x = Id {unId :: x} deriving Show

instance Naperian Id where
  type Log Id = ()
  project (Id x) () = x
  positions = Id ()

newtype (:*:) f g x = Pr (f x, g x) deriving Show

instance (Naperian f, Naperian g) => Naperian (f :*: g) where
  type Log (f :*: g) = Either (Log f) (Log g)
  project (Pr (fx, gx)) (Left p) = project fx p
  project (Pr (fx, gx)) (Right p) = project gx p
  positions = Pr (fmap Left positions, fmap Right positions)

Tenga en cuenta que una matriz de tamaño fijo (un vector ) viene dada por (Id :*: Id :*: ... :*: Id :*: One) , donde One es el funtor de la unidad constante, cuyo logaritmo es Void . Entonces una matriz es Naperian . Ahora, también tenemos

instance (Naperian f, Naperian g) => Naperian (f :.: g) where
  type Log (f :.: g) = (Log f, Log g)
  project (C fgx) (p, q) = project (project fgx p) q
  positions = C $ fmap (/ p -> fmap (p ,) positions) positions

lo que significa que las matrices multidimensionales son Naperian .

Para construir una versión de InContext f para Naperian f , solo apunta a una posición.

data Focused f x = f x :@ Log f

instance Functor f => Functor (Focused f) where
  fmap h (fx :@ p) = fmap h fx :@ p

instance Naperian f => Comonad (Focused f) where
  counit (fx :@ p) = project fx p
  cojoin (fx :@ p) = fmap (fx :@) positions :@ p

Entonces, en particular, una matriz n-dimensional Focused será una comadre. Una composición de vectores es un producto tensorial de n vectores, porque los vectores son Naperian . Pero el conjunto n-dimensional Focused será el producto tensor de n-plegamiento, no la composición , de los n vectores Focused que determinan sus dimensiones. Para expresar esta comonad en términos de cremalleras, necesitaremos expresarlas en una forma que permita construir el producto tensor. Lo dejo como un ejercicio para el futuro.