Mónadas como adjuntos

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

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

El código actual de adjunción categoría-extras ahora está en el paquete adjunciones: http://hackage.haskell.org/package/adjunctions

sólo voy a trabajar a través de la mónada estado de forma explícita y sencilla. Este código usa Data.Functor.Compose del paquete de transformadores, pero 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 funtor identidad en C, y la "a" en la unidad es realmente el funtor identidad en D.

También podemos recuperar el hom-set definición de adjunción 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, podemos ahora definir una mónada de nuestra unidad/adjunción counit así:

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 aplicar la adjunción clásico 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 sinónimo de tipo

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 hacer en las mónadas de esta manera (como (Bool,) Par), 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. Nos puede hacer cont, pero como describe copumpkin, que requiere una adjunción de una categoría opuesta, por lo que en realidad utiliza una "forma" diferente de la clase de tipo "adjunta" 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 Derek Elkins' en La Mónada Lector 13 - Cálculo de mónadas con la teoría de categorías: http://www.haskell.org/wikiupload/8/85/TMR-Issue13.pdf

Además, recientes extensiones Kan de Hinze para papel optimización del Programa de paseos a través de la construcción de la lista mónada de la adjunción entre Mon y Set: http://www.cs.ox.ac.uk/ralf.hinze/Kan.pdf

---

vieja respuesta:

Dos referencias.

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

2) -Cafe también entrega con una discusión breve pero prometedora sobre el papel de 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

Answer 2

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

Para obtener un código de Agda que lo ilustre y lo pruebe, consulte http://hpaste.org/68257.

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 alguna idea al problema. La segunda categoría en la construcción es una categoría de T-álgebras. Un álgebra T agrega un "producto" a la categoría inicial.

Entonces, ¿cómo funcionaría para una lista de mónada? El funtor en la lista de mónada consiste en un constructor de tipo, por ejemplo, Int->[Int] y un mapeo de funciones (por ejemplo, aplicación estándar de mapa a 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 para construir la mónada de la forma habitual.

Debo decir que no soy más sabio.

Answer 4

Este es un tema antiguo, pero encontré la pregunta interesante, , así que hice algunos cálculos yo mismo. Afortunadamente 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. (voy a utilizar la notación CWM con Haskell como sintaxis)

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

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

Por definición, h debe cumplir h.T h == h.mu a y h.eta a== id.

Ahora, algunos fáciles persecución diagrama de prueba que h realidad provoca una estructura en un monoide (definido por x*y = h[x,y]), y que h se convierte en un homomorfismo monoid para esta estructura.

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

De esta manera (h = foldr (*) a0, una función que 'sustituye' (:) con (*) y mapas []-a0, la identidad).

Por lo tanto, 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 de T-álgebras en realidad son homomorfismos monoides.)

También caracteriza a las listas como objetos universales en HaskMon, al igual que los productos libres en GRP, anillos de polinomios en CRNG, etc.

el adjuction correspondiente a la construcción anterior es < F,G,eta,epsilon >

donde

• F:Hask -> HaskMon, que tiene un tipo de una a la 'monoid libre generado por a', es decir, [a],
• G:HaskMon -> Hask, el funtor de olvido (olvidar la multiplicación),
• eta:1 -> GF, la transformación natural definido por \x::a -> [x],
• epsilon: FG -> 1 , la transformación natural definido por la función de plegado anteriormente (la 'surjection canónica' de un monoid gratuito a su monoid cociente)

a continuación, hay otra 'categoría Kleisli' y la adjunción correspondiente . Se puede comprobar que es sólo la categoría de tipos de Haskell con morfismos a -> T b, donde sus composiciones se dan en el llamado 'Kleisli composición' (>=>). Un programador típico de Haskell encontrará esta categoría más familiar.

Por último, como se ilustra en CWM, la categoría de T-álgebras (resp. Categoría Kleisli) se convierte en el objeto terminal (resp. Inicial) en la categoría de adjuctions que definen la lista mónada T en un sentido adecuado .

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

Answer 5

Si usted está interesado, aquí hay algunos pensamientos de una persona no experta sobre el papel de las mónadas y adjunciones en lenguajes de programación:

En primer lugar, existe una mónada dada T una adjunción única para la Kleisli categoría 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 restringe solo a la economía de notación.Una vulnerabilidad de asociatividad de morfismos para poder escribir (decir) [0,1,2] en 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, para el sistema actual de tipos de Haskell es de gran alcance suficiente para darse cuenta de encapsulación de datos (tipos existenciales).

Esta es mi respuesta a su pregunta original, , pero tengo curiosidad de saber lo que los expertos de Haskell tienen para decir al respecto.

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

En el caso de Hask y la lista mónada T, la estructura que T introduce es que de monoide, y esto nos puede ayudar a establecer las propiedades (incluyendo la corrección) de código a través algebraica métodos que la teoría de monoides proporciona. Por ejemplo, la función foldr (*) e::[a]->a puede 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 los 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ías (MacLane, Eilenberg, etc.), , es decir, para establecer equivalencia natural de categorías y transferir un método conocido en una categoría a otra (por ejemplo, métodos homológicos para espacios topológicos, métodos algebraicos para programación, etc.). Aquí, adjuntos y mónadas son herramientas indispensables para explotar esta conexión de categorías. (Incidentalmente, la noción de mónadas (y su dual, comonads) es tan general que incluso se puede llegar a definir 'cohomologies' de tipos de Haskell. Pero no he pensado aún.)

En cuanto a las funciones no deterministas que mencionó, tengo mucho menos que decir ... Pero tenga en cuenta que; si una adjunción <F,G>:Hask->A para alguna categoría A define la lista monad T, , debe existir un único 'functor de 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.

Por último, algunas observaciones:

El funtor árbol binario he mencionado en mi último puesto generaliza fácilmente al arbitraria tipo de datos 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 una sintaxis azucarera (que es bastante importante en la práctica, por supuesto).