haskell - monad - La mónada del "lector".

reader monad learn you a haskell

Question

Bien, entonces la mónada del escritor te permite escribir cosas en [generalmente] algún tipo de contenedor, y recuperar ese contenedor al final. En la mayoría de las implementaciones, el "contenedor" puede ser cualquier monoide.

Ahora, también hay una mónada "lector". Se podría pensar que esto ofrecería la operación dual: lectura incremental de algún tipo de contenedor, un elemento a la vez. De hecho, esta no es la funcionalidad que proporciona la mónada habitual del lector. (En su lugar, simplemente ofrece un fácil acceso a una constante semi-global).

Para escribir realmente una mónada que es dual a la mónada del escritor habitual, necesitaríamos algún tipo de estructura que sea dual a un monoide.

1. ¿Alguien tiene alguna idea de lo que podría ser esta estructura dual?
2. ¿Alguien ha escrito esta mónada? ¿Hay un nombre bien conocido para ello?

Answer 1

El dual de un monoide es un comonoide. Recuerde que un monoide se define como (algo isomorfo a)

 class Monoid m where
create :: () -> m
combine :: (m,m) -> m

con estas leyes

 combine (create (),x) = x
combine (x,create ()) = x
combine (combine (x,y),z) = combine (x,combine (y,z))

así

 class Comonoid m where
delete :: m -> ()
split :: m -> (m,m)

algunas operaciones estándar son necesarias

 first :: (a -> b) -> (a,c) -> (b,c)
second :: (c -> d) -> (a,c) -> (a,d)
idL :: ((),x) -> x
idR :: (x,()) -> x
assoc :: ((x,y),z) -> (x,(y,z))

con leyes como

idL $ first delete $ (split x) = x
idR $ second delete $ (split x) = x
assoc $ first split (split x) = second split (split x)

Esta clase de tipos se ve rara por una razón. Tiene una instancia

instance Comonoid m where
split x = (x,x)
delete x = ()

En Haskell, esta es la única instancia. Podemos volver a redactar el lector como el doble exacto del escritor, pero como solo hay una instancia para comonoides, obtenemos algo isomorfo para el tipo de lector estándar.

Tener todos los tipos de comonoides es lo que hace que la categoría "Cartesiana" en "Categoría Cerrada Cartesiana". Las "Categorías Cerradas Monoidales" son como CCC pero sin esta propiedad, y están relacionadas con sistemas de tipo subestructural. Parte del atractivo de la lógica lineal es la simetría incrementada de la que es un ejemplo. Mientras que, tener tipos de estructura le permite definir comonoides con propiedades más interesantes (que admiten cosas como la gestión de recursos). De hecho, esto proporciona un marco para comprender el papel de los constructores y destructores de copia en C ++ (aunque C ++ no aplica las propiedades importantes debido a la existencia de punteros).

EDITAR: Lector de comonoides

newtype Reader r x = Reader {runReader :: r -> x}
forget :: Comonoid m => (m,a) -> a
forget = idL . first delete
instance Comonoid r => Monad (Reader r) where
return x = Reader $ /r -> forget (r,x)
m >>= f = /r -> let (r1,r2) = split r in runReader (f (runReader m r1)) r2
ask :: Comonoid r => Reader r r
ask = Reader id

tenga en cuenta que en el código anterior, cada variable se usa exactamente una vez después de la vinculación (de modo que todas estas se tipearán con tipos lineales). Las pruebas de la ley de la mónada son triviales, y solo requieren que las leyes de comonoides funcionen. Por lo tanto, el Reader realmente es dual al Writer .

Answer 2

La oferta se basa en el estado, lo que la hace subóptima para algunas aplicaciones. Por ejemplo, podríamos querer hacer un árbol infinito de valores suministrados (por ejemplo, randoms):

tree :: (Something r) => Supply r (Tree r)
tree = Branch <$> supply <*> sequenceA [tree, tree]

Pero como la oferta se basa en el estado, todas las etiquetas estarán en la parte inferior, excepto las que se encuentran en el camino que se encuentra más a la izquierda en el árbol.

Necesitas algo que se pueda dividir (como en Comonoid de Comonoid ). Pero hay un problema si intentas convertir esto en una Mónada:

newtype Supply r a = Supply { runSupply :: r -> a }
instance (Splittable r) => Monad (Supply r) where
return = Supply . const
Supply m >>= f = Supply $ /r ->
let (r'',r'''') = split r in
runSupply (f (m r'')) r''''

Debido a que las leyes de la mónada requieren f >>= return = f , entonces eso significa que r'''' = r en la definición de (>>=) . Pero, las leyes de la mónada también requieren que return x >>= f = fx , así que r'' = r también. Por lo tanto, para que Supply sea ​​una mónada, split x = (x,x) , y así tendrás nuevamente el antiguo Reader normal.

Muchas de las mónadas que se usan en Haskell no son reales, es decir, solo cumplen con las leyes hasta una cierta relación de equivalencia . Por ejemplo, muchas mónadas no deterministas darán resultados en un orden diferente si se transforma de acuerdo con las leyes. Pero está bien, eso es suficiente para la mónada si te estás preguntando si un elemento en particular aparece en la lista de resultados, en lugar de dónde .

Si permites que Supply sea ​​una mónada hasta una cierta relación de equivalencia, entonces puedes obtener splits no triviales. Por ejemplo value-supply construirá entidades divisibles que distribuirán etiquetas únicas de una lista en un orden no especificado (utilizando magia unsafe* ), por lo que una mónada de suministro de valor sería una mónada hasta la permutación de etiquetas. Esto es todo lo que se necesita para muchas aplicaciones. Y, de hecho, hay una función.

runSupply :: (forall r. Eq r => Supply r a) -> a

que abstrae sobre esta relación de equivalencia para proporcionar una interfaz pura bien definida, porque lo único que le permite hacer a las etiquetas es ver si son iguales, y eso no cambia si las permuta. Si este runSupply es la única observación que permite en el Supply , entonces el Supply en un suministro de etiquetas únicas es una mónada real.

Answer 3

No estoy completamente seguro de lo que debería ser el dual de un monoide, pero pensar en dual (probablemente incorrectamente) como lo opuesto a algo (simplemente sobre la base de que un Comonad es el dual de una Mónada y tiene todas las mismas operaciones) pero al revés). En lugar de basarlo en mappend y mempty , lo basaría en:

fold :: (Foldable f, Monoid m) => f m -> m

Si nos especializamos en una lista aquí, obtenemos:

fold :: Monoid m => [m] -> m

Esto me parece que contiene toda la clase monoide, en particular.

mempty == fold []
mappend x y == fold [x, y]

Entonces, supongo que el dual de esta clase de monoides diferente sería:

unfold :: (Comonoid m) => m -> [m]

Esto se parece mucho a la clase factorial monoide que he visto en hackage here .

Entonces, sobre esta base, creo que la mónada ''lector'' que usted describe sería una mónada de oferta . La mónada de suministro es efectivamente un transformador de estado de una lista de valores, por lo que en cualquier momento podemos elegir que se nos suministre un artículo de la lista. En este caso, la lista sería el resultado de la mónada de suministro desplegado.

Debo recalcar que no soy un experto en Haskell, ni un experto en teoría. Pero esto es lo que tu descripción me hizo pensar.