Explicación sencilla de una mónada

Question

Recientemente he estado aprendiendo algo de programación funcional y me he encontrado con las mónadas. Entiendo lo que son en términos de programación, pero me gustaría entender lo que son matemáticamente. ¿Puede alguien explicar lo que es una mónada usando la menor teoría de categorías posible?

Answer 1

Si quieres evitar demasiada teoría de categorías, puedes leer primero este enlace para entender la definición de mónadas en Haskell . Entonces mira Wikilibros para una mirada más matemática (gracias Jonathan Fischoff).

Hay dos descripciones que conozco. La primera se puede encontrar fácilmente buscando en la wiki bajo Mónada o consultando el bonito resumen de Harry. La segunda es más interesante en mi opinión.

Asumiré que no conoces la definición de una acción monoidal, si la conoces, pasa de largo.

Una acción monoidal es un functor de un monoide a la categoría de endofunctores sobre una categoría que satisface dos relaciones de coherencia. Estas dos relaciones de coherencia simplemente verifican que su producto monoidal es el mismo que la composición en el objetivo, y que el objeto identidad se comporta con la acción. Las relaciones se escriben normalmente como diagramas, pero sin el implemento de látex, no las escribiré aquí.

Para hacernos una idea de una acción monoidal, consideremos una acción de grupo, y formulémosla un poco más categóricamente, escribiendo los dos axiomas como diagramas. Estos diagramas, cuando se convierten al lenguaje de las categorías monoidales, son exactamente los de una acción monoidal.

Ahora la mejor parte es que una vez que tienes una acción monoidal, las mónadas en una categoría son simplemente la categoría de acciones monoidales desde la categoría monoidal trivial a tu categoría. Nótese aquí que la categoría monoidal trivial será la categoría monoidal con un objeto un morfismo y todos los demás datos monoidales están determinados trivialmente. Las relaciones de coherencia monádica provienen gratuitamente de sus relaciones de coherencia de acciones monoidales.

Entonces, ¿mi simple explicación?

De este modo, podemos formular las mónadas funtorialmente como "representaciones" de la categoría monoidal trivial.

Se puede demostrar fácilmente que las dos definiciones son iguales.

Answer 2

Las mónadas en Haskell y las mónadas en la teoría de categorías son muy parecidas: A mónada consiste en un functor $T: C \to C$ y dos transformaciones naturales $\eta_X : X \to T(X)$ ( return en Haskell) y $\mu_X : T(T(X)) \to T(X)$ ( join en Haskell) con sujeción a las siguientes leyes

$\mu_X \circ T(\eta_X) = \mu_X \circ \eta_{T(X)} = 1_{T(X)}$ (leyes unitarias izquierda y derecha)

$\mu_X \circ \mu_{T(X)} = \mu_X \circ T(\mu_X)$ (asociatividad)

Así, en comparación con Haskell, la mónada se define en términos de return , join y fmap en lugar de return y (>>=) . Para más detalles al respecto, véase también el wikilibro de Haskell .

Dos ejemplos pueden iluminar esta definición.

Le site functor powerset

• $\mathcal{P} = X \mapsto \mathcal{P}(X)$ asigna un conjunto al conjunto de sus subconjuntos.
• Funciones $f:X \to Y$ se extienden puntualmente a $\mathcal{P}(f):\mathcal{P}(X) \to \mathcal{P}(Y)$
• $\eta_X : X \to \mathcal{P}(X)$ es la función $x \mapsto \left\{x\right\}$
• $\mu_X : \mathcal{P}(\mathcal{P}(X)) \to \mathcal{P}(X)$ aplana la capa interna de subconjuntos: $\mu_X(A) = \left\{ b | a \in A, b \in a \right\}$ .
• Esto es similar a la mónada de la lista en Haskell.

Le site cierre operación sobre los subconjuntos de un espacio topológico $S$ también es una mónada.

• Los objetos de la categoría $C$ son los subconjuntos de un espacio topológico dado $S$ .
• Hay una flecha única $X \to Y$ entre a los objetos $X$ y $Y$ exactamente cuando $X \subseteq Y$ .
• La mónada viene dada por el functor que mapea cada objeto $X$ a su cierre topológico $\bar X$ y la flecha $X \subseteq Y$ a la flecha $\bar{X}\subseteq \bar{Y}$ .
• Claramente, tenemos $X \subseteq \bar X$ esto es $\eta_X$ .
• Además, sabemos que $\bar{\bar X} = \bar X$ En particular $\bar{\bar X} \subseteq \bar X$ esto es $\mu_X$ .

Answer 3

Dejemos que $C$ sea una categoría. Entonces una mónada con sede en $C$ es un monoide en la categoría monoidal estricta

$$\mathcal{End}(C)=\mathcal{Hom}_{Cat}(C,C),$$

donde el producto monoidal natural viene dado por la composición de endofunctores, y la unidad monoidal es el funtor de identidad.

Un monoide en una categoría monoidal se define aquí .

Si necesitas más explicaciones, llámame.

Notación: La categoría de funtores $C\to D$ también se escribe como $Fun(C,D)$ pero esta notación no es estándar. Las notaciones estándar son $\mathcal{Hom}_{Cat}(C,D)$ o simplemente $Cat(C,D)$ .