haskell - quiere - ¿Qué es una mónada en FP, en términos categóricos?

neo monadología

Question

Cada vez que alguien promete "explicar las mónadas", mi interés despierta, solo para ser reemplazado por la frustración cuando la supuesta "explicación" es una larga lista de ejemplos terminados por alguna observación externa de que la "teoría matemática" detrás de lo "esotérico" las ideas "son" demasiado complicadas de explicar en este punto ".

Ahora estoy pidiendo lo opuesto. Tengo una sólida comprensión de la teoría de categorías y no le temo a la persecución de diagramas, el lema de Yoneda o los funtores derivados (y de hecho en mónadas y adjunciones en el sentido categórico).

¿Podría alguien darme una definición clara y concisa de qué es una mónada en la programación funcional? Cuantos menos ejemplos, mejor: a veces un concepto claro dice más de cien ejemplos tímidos. Haskell lo haría muy bien como un lenguaje para la demostración, aunque no soy exigente.

Answer 1

Como complemento a la respuesta de Carl, una Mónada en Haskell es (teóricamente) esto:

class Monad m where
join :: m (m a) -> m a
return :: a -> m a
fmap :: (a -> b) -> m a -> m b

Tenga en cuenta que "bind" ( >>= ) se puede definir como

x >>= f = join (fmap f x)

De acuerdo con Haskell Wiki

Una mónada en una categoría C es una triple ( F : C → C, η: Id → F , μ: F ∘ F → F )

... con algunos axiomas. Para Haskell, fmap , return y join line up con F , η y μ, respectivamente. ( fmap en Haskell define un Functor). Si no me equivoco, Scala llama a estos map , pure , y se join respectivamente. (Scala llama bind "flatMap")

Answer 2

Como entiendes las mónadas en el sentido de la categoría teórica, estoy interpretando que tu pregunta se trata de la presentación de las mónadas en la programación funcional. Por lo tanto, mi respuesta evita cualquier explicación de lo que es una mónada, o cualquier intuición sobre su significado o uso.

Respuesta : En Haskell se presenta una mónada, en un idioma interno para alguna categoría, como los mapas (internalizados) de un Kleisli triple.

Explicación : Es difícil ser preciso sobre las propiedades de la "categoría Hask ", y estas propiedades son en gran medida irrelevantes para entender la presentación de mónadas de Haskell. En cambio, para esta discusión, es más útil entender a Haskell como un lenguaje interno para alguna categoría C. Las funciones de Haskell definen morfismos en C y los tipos de Haskell son objetos en C , pero la categoría particular en la que se realizan estas definiciones no es importante.

Los tipos de datos paramétricos, por ejemplo, los data F a = ... , son mapeos de objetos , por ejemplo, F : | C | -> | | -> | C | .

La descripción habitual de una mónada en Haskell está en la forma Kleisli triple (o extensión Kleisli ):

class Monad m where
return :: a -> m a
(>>=) :: m a -> (a -> m b) -> m b

dónde:

• m es el mapeo de objetos m :| C | -> | | -> | C |
• return es la operación de la unidad en los objetos
• >>= (pronunciado "bind" por Haskellers) es la operación de extensión sobre morfismos pero con sus dos primeros parámetros intercambiados (compárese la firma habitual de extensión (-)* : (a -> mb) -> ma -> mb )

(Estos mapas se internalizan a sí mismos como familias de morfismos en C , lo que es posible desde m :| C | -> | C | ).

La nota de Haskell (si se ha encontrado con esto) es, por lo tanto, un lenguaje interno para las categorías de Kleisli.

Answer 3

Debería leer el artículo de Eugenio Moggi "Nociones de cómputos y mónadas" que explican el papel propuesto entonces de las mónadas para estructurar la semántica denotacional de los lenguajes efectivos.

También hay una pregunta relacionada:

¿Referencias para aprender la teoría detrás de lenguajes funcionales puros como Haskell?

Como no quieres agitar las manos, tienes que leer artículos científicos, no respuestas de foros o tutoriales.

Answer 4

Esta pregunta tiene algunas buenas respuestas: las mónadas como adjunciones

Más al punto, el artículo de Derek Elkins "Cálculo de mónadas con teoría de categorías" en TMR # 13 debería tener el tipo de construcciones que estás buscando: http://www.haskell.org/wikiupload/8/85/TMR-Issue13.pdf

Finalmente, y tal vez esto es realmente lo más cercano a lo que está buscando, puede ir directamente a la fuente y ver los documentos fundamentales de Moggi sobre el tema desde 1988-91: http://www.disi.unige.it/person/MoggiE/publications.html

Ver en particular "Nociones de computación y mónadas".

La mía, estoy segura, demasiado condensada / impreciso:

Comienza con una categoría Hask cuyos objetos son tipos Haskell y cuyos morfismos son funciones. Las funciones también son objetos en Hask , al igual que los productos. Así que Hask es cartesiano cerrado. Ahora introduce una flecha mapeando cada objeto en Hask a MHask que es un subconjunto de los objetos en Hask . ¡Unidad! Luego, introduzca una flecha mapeando cada flecha en Hask a una flecha en MHask . Esto nos da un mapa y hace que MHask sea ​​un MHask covariante. Ahora introduzca una flecha mapeando cada objeto en MHask que se genera desde un objeto en MHask (por unidad) hasta el objeto en MHask que lo genera. ¡Unirse! Y a partir de eso, MHask es una mónada (y un endofunctor monoidal para ser más preciso).

Estoy seguro de que hay una razón por la que lo anterior es deficiente, por lo que realmente lo dirigiría, si está buscando el formalismo, a los documentos de Moggi en particular.

Answer 5

La página de wikibook de Haskell tiene una buena explicación básica.

Answer 6

Ok, usando la terminología y ejemplos de Haskell ...

Una mónada, en programación funcional, es un patrón de composición para tipos de datos con el tipo * -> * .

class Monad (m :: * -> *) where
return :: a -> m a
(>>=) :: m a -> (a -> m b) -> m b

(Hay más en la clase que en Haskell, pero esas son las partes importantes).

Un tipo de datos es una mónada si puede implementar esa interfaz al tiempo que cumple tres condiciones en la implementación. Estas son las "leyes de mónadas", y lo dejo con esas explicaciones largas para la explicación completa. Resumo las leyes ya que " (>>= return) es una función de identidad, y (>>=) es asociativo". Realmente no es más que eso, incluso si se puede expresar de manera más precisa.

Y eso es todo lo que es una mónada. Si puede implementar esa interfaz conservando esas propiedades de comportamiento, tiene una mónada.

Esa explicación es probablemente más corta de lo que esperabas. Eso es porque la interfaz de mónada realmente es muy abstracta. El increíble nivel de abstracción es parte de por qué se pueden modelar tantas cosas diferentes como mónadas.

Lo que es menos obvio es que, por más abstracta que sea la interfaz, permite modelar genéricamente cualquier patrón de flujo de control, independientemente de la implementación real de la mónada. Esta es la razón por la cual el paquete Control.Monad en la biblioteca base de GHC tiene combinadores como when , forever , etc. Y esta es la razón por la cual la capacidad de abstraer explícitamente sobre cualquier implementación de mónada es poderosa, especialmente con soporte de un sistema de tipo.

Answer 7

Realmente no sé de lo que estoy hablando, pero esta es mi opinión:

Las mónadas se usan para representar cómputos. Puede pensar en un programa de procedimiento normal, que es básicamente una lista de enunciados, como un conjunto de cálculos compuestos. Las mónadas son una generalización de este concepto, lo que le permite definir cómo se componen las declaraciones. Cada cálculo tiene un valor (podría ser simplemente () ); la mónada simplemente determina cómo se comporta el valor encadenado a través de una serie de cálculos.

Hacer la notación es lo que deja esto en claro: es básicamente un tipo especial de lenguaje basado en declaraciones que le permite definir qué sucede entre las declaraciones. Es como si pudieras definir cómo ";" trabajado en C-como los idiomas.

Desde este punto de vista, todas las mónadas que he utilizado hasta ahora tienen sentido: el State no afecta el valor, pero actualiza un segundo valor que se transfiere de computación a computación en segundo plano; Maybe cortocircuite el valor si alguna vez encuentra una Nothing ; List permite tener una cantidad variable de valores pasados; IO permite tener valores impuros pasados ​​de una manera segura. Las mónadas más especializadas que he usado, como los analizadores Gen y Parsec, también son similares.

Con suerte, esta es una explicación clara que no está completamente fuera de base.

Answer 8

Una mónada es un monoide en la categoría de endofunctors, ¿cuál es el problema? .

Dejando de lado el humor, personalmente creo que las mónadas, tal como se usan en Haskell y en la programación funcional, se comprenden mejor desde el punto de vista de las mónadas como interfaz (como en las respuestas de Carl y Dan) en lugar de las mónadas como tales. el punto de vista de la teoría del término de la categoría . Tengo que confesar que solo interioricé todo el asunto de la mónada cuando tuve que usar una library monadic de otro idioma en un proyecto real.

Menciona que no le gustaron todos los tutoriales de "muchos ejemplos". ¿Alguna vez alguien te ha señalado el papel del escuadrón Torpe ? Se centra varonil en la mónada IO, pero la introducción ofrece una buena explicación técnica e histórica de por qué el concepto de mónada fue adoptado por Haskell en primer lugar.