tabla - ¿Cuáles son algunos ejemplos motivadores para Cofree CoMonad en Haskell?

suma en haskell

Question

He estado jugando con Cofree , y no puedo asimilarlo.

Por ejemplo, quiero jugar con Cofree [] Num en ghci y no puedo obtener ningún ejemplo interesante.

Por ejemplo, si construyo un tipo Cofree:

let a = 1 :< [2, 3]

Esperaría extract a == 1 , pero en cambio me sale este error:

No instance for (Num (Cofree [] a0)) arising from a use of ‘it’
    In the first argument of ‘print’, namely ‘it’
    In a stmt of an interactive GHCi command: print it

Y un tipo de:

extract a :: (Num a, Num (Cofree [] a)) => a

¿Puedo obtener algunos ejemplos simples, incluso triviales, de cómo usar Cofree con, por ejemplo, functors: [] , o Maybe , o Either , that demuestra

• extract
• extend
• unwrap
• duplicate ?

Cross Publicado: https://www.reddit.com/r/haskell/comments/4wlw70/what_are_some_motivating_examples_for_cofree/

EDITAR: Guiados por el comentario de David Young, aquí hay algunos ejemplos mejores que muestran que mis primeros intentos fueron equivocados, sin embargo, aún me encantan algunos ejemplos que pueden guiar la intuición de Cofree:

> let a = 1 :< []
> extract a
    1
> let b = 1 :< [(2 :< []), (3 :< [])]
> extract b
    1
> unwrap b
    [2 :< [],3 :< []]
> map extract $ unwrap b
    [2,3]

Answer 1

Recapitulemos la definición del tipo de datos Cofree .

data Cofree f a = a :< f (Cofree f a)

Eso es al menos suficiente para diagnosticar el problema con el ejemplo. Cuando escribiste

1 :< [2, 3]

cometió un pequeño error que se informó de forma más sutil que útil. Aquí, f = [] y a es algo numérico, porque 1 :: a . En consecuencia, necesitas

[2, 3] :: [Cofree [] a]

y por lo tanto

2 :: Cofree [] a

lo que podría estar bien si Cofree [] a también fuera Cofree [] a instancia de Num . Su definición adquiere así una restricción que es poco probable que se satisfaga, y de hecho, cuando usa su valor, el intento de satisfacer la restricción falla.

Intenta nuevamente con

1 :< [2 :< [], 3 :< []]

y deberías tener mejor suerte.

Ahora, veamos qué tenemos. Comience por mantenerlo simple. ¿Qué es Cofree f () ? ¿Qué es, en particular, Cofree [] () ? Este último es isomorfo al punto fijo de [] : las estructuras de los árboles donde cada nodo es una lista de subárboles, también conocidos como "rosales no etiquetados". P.ej,

() :< [  () :< [  () :< []
               ,  () :< []
               ]
      ,  () :< []
      ]

Del mismo modo, Cofree Maybe () es más o menos el punto fijo de Maybe : una copia de los números naturales, porque Maybe nos da una posición cero o una posición para conectar un subárbol.

zero :: Cofree Maybe ()
zero = () :< Nothing
succ :: Cofree Maybe () -> Cofree Maybe ()
succ n = () :< Just n

Un caso trivial importante es Cofree (Const y) () , que es una copia de y . El functor Const y no da posiciones para los subárboles.

pack :: y -> Cofree (Const y) ()
pack y = () :< Const y

Luego, vamos a ocuparnos del otro parámetro. Te dice qué tipo de etiqueta adjuntas a cada nodo. Cambiar el nombre de los parámetros de manera más sugestiva

data Cofree nodeOf label = label :< nodeOf (Cofree nodeOf label)

Cuando etiquetamos el ejemplo (Const y) , obtenemos pares

pair :: x -> y -> Cofree (Const y) x
pair x y = x :< Const y

Cuando adjuntamos etiquetas a los nodos de nuestros números, obtenemos listas no vacías

one :: x -> Cofree Maybe x
one = x :< Nothing
cons :: x -> Cofree Maybe x -> Cofree Maybe x
cons x xs = x :< Just xs

Y para las listas, nos etiquetan los rosales.

0 :< [  1 :< [  3 :< []
             ,  4 :< []
             ]
     ,  2 :< []
     ]

Estas estructuras son siempre "no vacías", porque hay al menos un nodo superior, incluso si no tiene hijos, y ese nodo siempre tendrá una etiqueta. La operación de extract le da la etiqueta del nodo superior.

extract :: Cofree f a -> a
extract (a :< _) = a

Es decir, extract elimina el contexto de la etiqueta superior.

Ahora, la operación duplicate decora cada etiqueta con su propio contexto.

duplicate :: Cofree f a -> Cofree f (Cofree f a)
duplicate a :< fca = (a :< fca) :< fmap duplicate fca  -- f''s fmap

Podemos obtener una instancia de Functor para Cofree f visitando todo el árbol

fmap :: (a -> b) -> Cofree f a -> Cofree f b
fmap g (a :< fca) = g a :< fmap (fmap g) fca
    --                     ^^^^  ^^^^
    --                 f''s fmap  ||||
    --                           (Cofree f)''s fmap, used recursively

No es difícil ver eso

fmap extract . duplicate = id

porque el duplicate decora cada nodo con su contexto, luego el fmap extract descarta la decoración.

Tenga en cuenta que fmap solo mira las etiquetas de la entrada para calcular las etiquetas de la salida. Supongamos que queremos calcular las etiquetas de salida según cada etiqueta de entrada en su contexto . Por ejemplo, dado un árbol no etiquetado, podríamos etiquetar cada nodo con el tamaño de su subárbol completo. Gracias a la instancia Foldable para Cofree f , deberíamos poder contar nodos con.

length :: Foldable f => Cofree f a -> Int

Entonces eso significa

fmap length . duplicate :: Cofree f a -> Cofree f Int

La idea clave de Comonads es capturar "cosas con cierto contexto", y te permiten aplicar mapas dependientes del contexto en cualquier lugar.

extend :: Comonad c => (c a -> b) -> c a -> c b
extend f = fmap f       -- context-dependent map everywhere
           .            -- after
           duplicate    -- decorating everything with its context

Definir extend más directamente le ahorra el problema de la duplicación (aunque eso solo equivale a compartir).

extend :: (Cofree f a -> b) -> Cofree f a -> Cofree f b
extend g ca@(_ :< fca) = g ca :< fmap (extend g) fca

Y puedes obtener duplicate tomando

duplicate = extend id -- the output label is the input label in its context

Además, si selecciona extract como lo que debe hacer para cada etiqueta en contexto, simplemente coloca cada etiqueta en su lugar original:

extend extract = id

Estas "operaciones en etiquetas en contexto" se llaman "flechas co-Kleisli",

g :: c a -> b

y el trabajo de extend es interpretar una flecha co-Kleisli como una función en estructuras enteras. La operación de extract es la flecha de co-Kleisli de identidad, y se interpreta por extend como la función de identidad. Por supuesto, hay una composición co-Kleisli

(=<=) :: Comonad c => (c s -> t) -> (c r -> s) -> (c r -> t)
(g =<= h) = g . extend h

y las leyes de comonad aseguran que =<= es asociativo y absorbe el extract , dándonos la categoría co-Kleisli. Además, tenemos

extend (g =<= h)  =  extend g . extend h

de modo que extend es un funtor (en el sentido categórico) de la categoría co-Kleisli a sets-and-functions. Estas leyes no son difíciles de verificar para Cofree , ya que siguen las leyes de Functor para la forma del nodo.

Ahora, una forma útil de ver una estructura en una comonad de cofres es como una especie de "servidor de juegos". Una estructura

a :< fca

representa el estado del juego. Un movimiento en el juego consiste en "detener", en cuyo caso obtienes la a , o "continuar", al elegir un subárbol de fca . Por ejemplo, considere

Cofree ((->) move) prize

Un cliente para este servidor debe detenerse o continuar dando un move : es una lista de move . El juego se juega de la siguiente manera:

play :: [move] -> Cofree ((->) move) prize -> prize
play []       (prize :< _) = prize
play (m : ms) (_     :< f) = play ms (f m)

Tal vez un move es un Char y el prize es el resultado de analizar la secuencia de caracteres.

Si miras con suficiente atención, verás que [move] es una versión de Free ((,) move) () . Las mónadas libres representan estrategias del cliente. El ((,) move) functor ((,) move) equivale a una interfaz de comando con solo el comando "enviar un move ". El functor ((->) move) es la estructura correspondiente "responder al envío de un move ".

Algunos funtores se pueden ver como capturar una interfaz de comando; la mónada libre para dicho functor representa programas que hacen comandos; el funtor tendrá un "doble" que representa cómo responder a los comandos; el cofre comonad del dual es la noción general de entorno en el que se pueden ejecutar los programas que hacen los comandos, con la etiqueta que dice qué hacer si el programa se detiene y devuelve un valor, y las subestructuras que dicen cómo continuar ejecutando el programa si emite un comando.

Por ejemplo,

data Comms x = Send Char x | Receive (Char -> x)

describe que se le permite enviar o recibir caracteres. Su doble es

data Responder x = Resp {ifSend :: Char -> x, ifReceive :: (Char, x)}

Como ejercicio, mira si puedes implementar la interacción

chatter :: Free Comms x -> Cofree Responder y -> (x, y)