haskell - prestabilita - monadas leibniz

Las mónadas como adjunciones

Question

He estado leyendo acerca de las mónadas en la teoría de categorías. Una definición de mónadas usa un par de funtores adjuntos. Una mónada se define mediante un viaje de ida y vuelta utilizando esos funtores. Aparentemente, las adjunciones son muy importantes en la teoría de categorías, pero no he visto ninguna explicación de las mónadas Haskell en términos de funtores adjuntos. Alguien lo ha pensado?

Answer 1

Derek Elkins me mostró recientemente durante la cena cómo surge Cont Monad al componer el functor contravariante (_ -> k) consigo mismo, ya que resulta ser autoadjunto. Así es como obtienes (a -> k) -> k de eso. Su counit, sin embargo, lleva a la eliminación de doble negación, que no puede escribirse en Haskell.

Para obtener algún código de Agda que lo ilustre y lo demuestre, consulte http://hpaste.org/68257 .

Answer 2

Este es un hilo antiguo, pero la pregunta me pareció interesante, así que hice algunos cálculos yo mismo. Con suerte Bartosz todavía está allí y podría leer esto ...

De hecho, la construcción de Eilenberg-Moore da una imagen muy clara en este caso. (Usaré la notación CWM con la sintaxis de Haskell)

Sea T la lista mónada < T,eta,mu > ( eta = return y mu = concat ) y considere un T-álgebra h:T a -> a .

(Tenga en cuenta que T a = [a] es un monoide libre <[a],[],(++)> , es decir, identidad [] y multiplicación (++) .)

Por definición, h debe satisfacer hT h == h.mu a y h.eta a== id .

Ahora bien, una búsqueda fácil de diagramas demuestra que h realidad induce una estructura monoide en a (definida por x*y = h[x,y] ), y que h convierte en un homomorfismo monoide para esta estructura.

Por el contrario, cualquier estructura monoide < a,a0,* > definida en Haskell se define naturalmente como una T-álgebra.

De esta forma ( h = foldr ( * ) a0 , una función que ''reemplaza'' (:) con (*) , y asigna [] a a0 , la identidad).

Entonces, en este caso, la categoría de T-álgebras es solo la categoría de estructuras monoides definibles en Haskell, HaskMon.

(Por favor, compruebe que los morfismos en T-álgebras son en realidad homomorfismos monoides).

También caracteriza listas como objetos universales en HaskMon, al igual que productos gratuitos en Grp, anillos polinómicos en CRng, etc.

La corrección correspondiente a la construcción anterior es < F,G,eta,epsilon >

dónde

• F:Hask -> HaskMon , que toma un tipo a al ''monoid libre generado por a '', es decir, [a] ,
• G:HaskMon -> Hask , el functor olvidadizo (olvida la multiplicación),
• eta:1 -> GF , la transformación natural definida por /x::a -> [x] ,
• epsilon: FG -> 1 , la transformación natural definida por la función de plegado anterior (la ''sobreyección canónica'' de un monoide libre a su cociente monoide)

Luego, hay otra ''categoría Kleisli'' y la adjunción correspondiente. Puedes comprobar que es solo la categoría de tipos Haskell con morfismos a -> T b , donde sus composiciones están dadas por la llamada ''composición Kleisli'' (>=>) . Un programador típico de Haskell encontrará esta categoría más familiar.

Finalmente, como se ilustra en CWM, la categoría de T-álgebras (respectivamente categoría Kleisli) se convierte en el objeto terminal (respectivamente inicial) en la categoría de adjuntos que definen la lista de mónadas T en un sentido adecuado.

Sugiero hacer un cálculo similar para el binario tree functor T a = L a | B (T a) (T a) T a = L a | B (T a) (T a) para verificar su comprensión.

Answer 3

He encontrado una construcción estándar de funtores adjuntos para cualquier mónada de Eilenberg-Moore, pero no estoy seguro de si agrega algún conocimiento al problema. La segunda categoría en la construcción es una categoría de T-álgebras. AT álgebra agrega un "producto" a la categoría inicial.

Entonces, ¿cómo funcionaría para una lista de mónadas? El funtor en la lista de la mónada consiste en un constructor de tipo, por ejemplo, Int->[Int] y un mapeo de funciones (p. Ej., Aplicación estándar del mapa a las listas). Un álgebra agrega un mapeo de listas a elementos. Un ejemplo sería agregar (o multiplicar) todos los elementos de una lista de enteros. El funtor F toma cualquier tipo, por ejemplo, Int, y lo mapea en el álgebra definida en las listas de Int, donde el producto está definido por unión monádica (o viceversa, la unión se define como el producto). El functor olvidadizo G toma un álgebra y olvida el producto. El par F , G , de funtores adjuntos se usa luego para construir la mónada de la manera habitual.

Debo decir que no soy más sabio.

Answer 4

Si está interesado, aquí hay algunas ideas de un no experto sobre el papel de las mónadas y los adjuntos en los lenguajes de programación:

En primer lugar, existe para una mónada determinada T una adjunción única para la categoría Kleisli de T En Haskell, el uso de mónadas se limita principalmente a operaciones en esta categoría (que es esencialmente una categoría de álgebras libres, sin cocientes). De hecho, todo lo que uno puede hacer con una Mónada Haskell es componer algunos morfismos Kleisli de tipo a->T b mediante el uso de expresiones do, (>>=) , etc., para crear un nuevo morfismo. En este contexto, el papel de las mónadas se limita a la economía de la notación. Uno explota la asociatividad de los morfismos para poder escribir (decir) [0,1,2] lugar de (Cons 0 (Cons 1 (Cons 2 Nil))) , es decir, puede escribir la secuencia como secuencia, no como un árbol.

Incluso el uso de mónadas IO no es esencial, ya que el sistema de tipo Haskell actual es lo suficientemente potente como para realizar encapsulación de datos (tipos existenciales).

Esta es mi respuesta a su pregunta original, pero tengo curiosidad por saber qué opinan los expertos de Haskell al respecto.

Por otro lado, como hemos notado, también hay una correspondencia 1-1 entre las mónadas y las adjunciones a las álgebras (T). Los adjuntos, en términos de MacLane, son "una forma de expresar equivalencias de categorías". En un entorno típico de adjuntos <F,G>:X->A donde F es una especie de ''generador de álgebra libre'' y G ''functor olvidadizo'', la mónada correspondiente (mediante el uso de álgebras T) describe cómo (y cuando) la estructura algebraica de A se construye sobre los objetos de X

En el caso de Hask y la lista de mónadas T, la estructura que T introduce es la de monoide, y esto puede ayudarnos a establecer propiedades (incluida la corrección) de código a través de métodos algebraicos que proporciona la teoría de monoides. Por ejemplo, la función foldr (*) e::[a]->a se puede ver fácilmente como una operación asociativa siempre que <a,(*),e> sea ​​un monoide, un hecho que podría ser explotado por el compilador para optimizar el cálculo (por ejemplo, por paralelismo). Otra aplicación es identificar y clasificar los "patrones de recursión" en la programación funcional usando métodos categóricos con la esperanza de (parcialmente) disponer de "la parte de la programación funcional", Y (el combinador de recursión arbitrario).

Aparentemente, este tipo de aplicaciones es una de las principales motivaciones de los creadores de la Teoría de Categoría (MacLane, Eilenberg, etc.), a saber, para establecer equivalencia natural de categorías y transferir un método bien conocido de una categoría a otra (p. Ej. métodos homológicos para espacios topológicos, métodos algebraicos para programación, etc.). Aquí, los adjuntos y las mónadas son herramientas indispensables para explotar esta conexión de categorías. (Por cierto, la noción de mónadas (y su dual, comonads) es tan general que incluso se puede llegar a definir "cohomologías" de tipos Haskell. Pero todavía no he pensado en ello).

En cuanto a las funciones no deterministas que mencionaste, tengo mucho menos que decir ... Pero ten en cuenta que; si una adjunción <F,G>:Hask->A para alguna categoría A define la lista de mónadas T , debe haber un único '' K:A->MonHask comparación'' K:A->MonHask (la categoría de monoides definibles en Haskell), ver CWM . Esto significa, en efecto, que su categoría de interés debe ser una categoría de monoides en alguna forma restringida (por ejemplo, puede carecer de algunos cocientes pero no de álgebras libres) para definir la lista de mónadas.

Finalmente, algunas observaciones:

El binary tree functor que mencioné en mi última publicación se generaliza fácilmente a datos de tipo arbitrario T a1 .. an = T1 T11 .. T1m | ... T a1 .. an = T1 T11 .. T1m | ... A saber, cualquier tipo de datos en Haskell define naturalmente una mónada (junto con la categoría correspondiente de álgebras y la categoría Kleisli), que es solo el resultado de que cualquier constructor de datos en Haskell sea total. Esta es otra razón por la que considero que la clase Monad de Haskell no es mucho más que un azúcar de sintaxis (que es bastante importante en la práctica, por supuesto).

Answer 5

Editar : solo por diversión, voy a hacer esto bien. Respuesta original conservada debajo

El código adjunto actual para extras de categoría ahora está en el paquete adjuntos: http://hackage.haskell.org/package/adjunctions

Voy a trabajar a través de la mónada de estado explícita y simplemente. Este código usa Data.Functor.Compose del paquete de transformadores, pero de otro modo es autónomo.

Una adjunción entre f (D -> C) yg (C -> D), escrita f - | g, se puede caracterizar de varias maneras. Utilizaremos la descripción counit / unit (épsilon / eta), que ofrece dos transformaciones naturales (morfismos entre funtores).

class (Functor f, Functor g) => Adjoint f g where
counit :: f (g a) -> a
unit :: a -> g (f a)

Tenga en cuenta que la "a" en counit es realmente el functor de identidad en C, y la "a" en la unidad es realmente el functor de identidad en D.

También podemos recuperar la definición de adjuntos hom-set de la definición de counit / unit.

phiLeft :: Adjoint f g => (f a -> b) -> (a -> g b)
phiLeft f = fmap f . unit
phiRight :: Adjoint f g => (a -> g b) -> (f a -> b)
phiRight f = counit . fmap f

En cualquier caso, ahora podemos definir una mónada de nuestra adjunción de unidad / counit como sigue:

instance Adjoint f g => Monad (Compose g f) where
return x = Compose $ unit x
x >>= f = Compose . fmap counit . getCompose $ fmap (getCompose . f) x

Ahora podemos implementar la adjunción clásica entre (a,) y (a ->):

instance Adjoint ((,) a) ((->) a) where
-- counit :: (a,a -> b) -> b
counit (x, f) = f x
-- unit :: b -> (a -> (a,b))
unit x = /y -> (y, x)

Y ahora un tipo sinónimo

type State s = Compose ((->) s) ((,) s)

Y si cargamos esto en ghci, podemos confirmar que State es precisamente nuestra mónada de estado clásica. Tenga en cuenta que podemos tomar la composición opuesta y obtener la Costate Comonad (también conocida como la tienda comonad).

Hay un montón de otras adjunciones que podemos convertir en mónadas de esta manera (como (Bool,) Pair), pero son una especie de mónadas extrañas. Desafortunadamente no podemos hacer las adicciones que inducen al Lector y el Escritor directamente en Haskell de una manera agradable. Podemos hacer Cont, pero como describe copumpkin, eso requiere una adjunción de una categoría opuesta, por lo que en realidad usa una "forma" diferente de la clase de tipo "Adjoint" que invierte algunas flechas. Esa forma también se implementa en un módulo diferente en el paquete de adjuntos.

este material está cubierto de una manera diferente por el artículo de Derek Elkins en The Monad Reader 13 - Cálculo de mónadas con teoría de categorías: http://www.haskell.org/wikiupload/8/85/TMR-Issue13.pdf

Además, el reciente documento Kan Extensions for Optimization Program de Hinze aborda la construcción de la lista de mónadas de la adjunción entre Mon y Set : http://www.cs.ox.ac.uk/ralf.hinze/Kan.pdf

Respuesta anterior:

Dos referencias

1) Category-extras ofrece, como siempre, una representación de los adjuntos y cómo surgen las mónadas de ellos. Como de costumbre, es bueno pensar con, pero bastante ligero en la documentación: http://hackage.haskell.org/packages/archive/category-extras/0.53.5/doc/html/Control-Functor-Adjunction.html

2) -Cafe también ofrece una discusión prometedora pero breve sobre el papel de la adjunción. Algunos de los cuales pueden ayudar a interpretar los extras de categoría: http://www.haskell.org/pipermail/haskell-cafe/2007-December/036328.html