haskell - ¿Qué estructura general tiene este tipo?

types higher-kinded-types

Question

Mientras pirateaba algo antes, creé el siguiente código:

newtype Callback a = Callback { unCallback :: a -> IO (Callback a) }
liftCallback :: (a -> IO ()) -> Callback a
liftCallback f = let cb = Callback $ /x -> (f x >> return cb) in cb
runCallback :: Callback a -> IO (a -> IO ())
runCallback cb =
do ref <- newIORef cb
return $ /x -> readIORef ref >>= ($ x) . unCallback >>= writeIORef ref

Callback a representa una función que maneja algunos datos y devuelve una nueva devolución de llamada que debería usarse para la siguiente notificación. Una devolución de llamada que básicamente puede reemplazarse, por así decirlo. liftCallback simplemente eleva una función normal a mi tipo, mientras que runCallback usa un IORef para convertir una Callback de Callback a una función simple.

La estructura general del tipo es:

data T m a = T (a -> m (T m a))

Parece mucho que esto podría ser isomorfo a alguna estructura matemática bien conocida de la teoría de categorías.

¿Pero, qué es esto? ¿Es una mónada o algo así? ¿Un functor aplicativo? Una mónada transformada? Una flecha, incluso? ¿Hay un motor de búsqueda similar a Hoogle que me permita buscar patrones generales como este?

Answer 1

Creo que este tipo es muy parecido a lo que he escuchado llamar ''Circuito'', que es un tipo de flecha. Ignorando por un momento la parte IO (ya que podemos tener esto simplemente transformando una flecha Kliesli), el transformador de circuito es:

newtype CircuitT a b c = CircuitT { unCircuitT :: a b (c, CircuitT a b c) }

Esto es básicamente una flecha que devuelve una nueva flecha para usar en la siguiente entrada cada vez. Todas las clases de flechas comunes (incluido el bucle) pueden implementarse para este transformador de flecha, siempre que la flecha base las admita. Ahora, todo lo que tenemos que hacer para que sea teóricamente el mismo que el tipo que menciona es deshacerse de ese resultado adicional. Esto se hace fácilmente, y entonces encontramos:

Callback a ~=~ CircuitT (Kleisli IO) a ()

Como si miramos el lado derecho:

CircuitT (Kleisli IO) a () ~=~
(Kliesli IO) a ((), CircuitT (Kleisli IO) a ()) ~=~
a -> IO ((), CircuitT (Kliesli IO) a ())

Y a partir de aquí, puede ver cómo es similar a Callback a, excepto que también damos un valor unitario. Como el valor unitario está en una tupla con otra cosa de todos modos, esto realmente no nos dice mucho, así que diría que básicamente son iguales.

NB Usé ~ = ~ para similar pero no totalmente equivalente, por alguna razón. Sin embargo, son muy similares, en particular, se puede convertir una Callback a en un CircuitT (Kleisli IO) a () y viceversa.

EDITAR: También estoy totalmente de acuerdo con las ideas de que se trata de A) un costo de vida monádico (operación monádica que espera un número infinito de valores, creo que esto significa) y B) un tubo de consumo único (que es en muchos aspectos muy similar a el tipo de circuito sin salida, o más bien salida ajustada a (), ya que tal tubería también podría tener salida).

Answer 2

El término que está buscando es un transformador de mónada gratuito . El mejor lugar para aprender cómo funcionan es leer el artículo "Piñones de Corutina" en el número 19 de The Monad Reader . Mario Blazevic da una descripción muy lúcida de cómo funciona este tipo, excepto que él lo llama el tipo "Coroutine".

Escribí su tipo en el paquete transformers-free y luego se fusionó en el paquete free , que es su nuevo hogar oficial.

Su tipo de Callback es isomorfo a:

type Callback a = forall r . FreeT ((->) a) IO r

Para comprender los transformadores de mónada libres, primero debe comprender las mónadas libres , que son simplemente árboles de sintaxis abstracta. Le das a la mónada gratuita un functor que define un solo paso en el árbol de sintaxis, y luego crea una Monad de ese Functor que es básicamente una lista de esos tipos de pasos. Entonces si tuvieras:

Free ((->) a) r

Eso sería un árbol de sintaxis que acepta cero o más a como entrada y luego devuelve un valor r .

Sin embargo, generalmente queremos incrustar efectos o hacer que el siguiente paso del árbol de sintaxis dependa de algún efecto. Para hacer eso, simplemente promovemos nuestra mónada gratuita a un transformador de mónada gratuito, que intercala la mónada base entre los pasos del árbol de sintaxis. En el caso de su tipo de Callback de Callback , está intercalando IO entre cada paso de entrada, por lo que su mónada base es IO :

FreeT ((->) a) IO r

Lo bueno de las mónadas libres es que son mónadas automáticamente para cualquier functor, por lo que podemos aprovechar esto para usar la notación do para ensamblar nuestro árbol de sintaxis. Por ejemplo, puedo definir un comando de await que vinculará la entrada dentro de la mónada:

import Control.Monad.Trans.Free
await :: (Monad m) => FreeT ((->) a) m a
await = liftF id

Ahora tengo una DSL para escribir Callback :

import Control.Monad
import Control.Monad.Trans.Free
printer :: (Show a) => FreeT ((->) a) IO r
printer = forever $ do
a <- await
lift $ print a

Tenga en cuenta que nunca tuve que definir la instancia de Monad necesaria. Tanto FreeT f como Free f son automáticamente Monad s para cualquier functor f , y en este caso ((->) a) es nuestro functor, por lo que automáticamente hace lo correcto. ¡Esa es la magia de la teoría de categorías!

Además, nunca tuvimos que definir una instancia de MonadTrans para usar el lift . FreeT f es automáticamente un transformador de mónada, dado cualquier f functor, por lo que también se encargó de eso.

Nuestra impresora es una Callback adecuada, por lo que podemos alimentar sus valores simplemente deconstruyendo el transformador de mónadas gratuito:

feed :: [a] -> FreeT ((->) a) IO r -> IO ()
feed as callback = do
x <- runFreeT callback
case x of
Pure _ -> return ()
Free k -> case as of
[] -> return ()
b:bs -> feed bs (k b)

La impresión real se produce cuando runFreeT callback , que luego nos da el siguiente paso en el árbol de sintaxis, que alimentamos el siguiente elemento de la lista.

Vamos a intentarlo:

>>> feed [1..5] printer
1
2
3
4
5

Sin embargo, ni siquiera necesita escribir todo esto usted mismo. Como señaló Petr, mi biblioteca de pipes abstrae patrones comunes de transmisión como estos para usted. Tu devolución de llamada es justa:

forall r . Consumer a IO r

La forma en que definiríamos la printer usando pipes es:

printer = forever $ do
a <- await
lift $ print a

... y podemos darle una lista de valores como esta:

>>> runEffect $ each [1..5] >-> printer
1
2
3
4
5

Diseñé las pipes para abarcar una gran variedad de abstracciones de transmisión como estas, de tal manera que siempre puedes utilizar la notación do para compilar cada componente de transmisión. pipes también vienen con una amplia variedad de soluciones elegantes para manejo de estado y errores, y flujo de información bidireccional, por lo que si formula su abstracción de Callback en términos de pipes , aprovechará una tonelada de maquinaria útil de forma gratuita.

Si desea obtener más información sobre las pipes , le recomiendo que lea el tutorial .

Answer 3

La estructura general del tipo me parece

data T (~>) a = T (a ~> T (~>) a)

donde (~>) = Kleisli m en sus términos (una flecha).

Callback sí no parece una instancia de ninguna clase de tipo Haskell estándar en la que pueda pensar, pero es un Funcionador contravariante (también conocido como Cofunctor, por engañoso que resulte). Como no está incluido en ninguna de las bibliotecas que vienen con GHC, existen varias definiciones en Hackage ( use esta ), pero todas se ven así:

class Contravariant f where
contramap :: (b -> a) -> f a -> f b
-- c.f. fmap :: (a -> b) -> f a -> f b

Entonces

instance Contravariant Callback where
contramap f (Callback k) = Callback ((fmap . liftM . contramap) f (f . k))

¿Hay alguna estructura más exótica de la teoría de categorías que posee Callback ? No lo sé.

Answer 4

Solo una observación, su tipo parece bastante relacionado con el Consumer pam aparece en la biblioteca de tuberías (y probablemente también otras librarties similares):

type Consumer p a = p () a () C
-- A Pipe that consumes values
-- Consumers never respond.

donde C es un tipo de datos vacío p es una instancia de clase de tipo Proxy . Consume valores de tipo a y nunca produce ninguno (porque su tipo de salida está vacío).

Por ejemplo, podríamos convertir una Callback en un Consumer :

import Control.Proxy
import Control.Proxy.Synonym
newtype Callback m a = Callback { unCallback :: a -> m (Callback m a) }
-- No values produced, hence the polymorphic return type `r`.
-- We could replace `r` with `C` as well.
consumer :: (Proxy p, Monad m) => Callback m a -> () -> Consumer p a m r
consumer c () = runIdentityP (run c)
where
run (Callback c) = request () >>= lift . c >>= run

Mira el tutorial .

(Esto debería haber sido más bien un comentario, pero es demasiado largo).