¿Quién dijo primero lo siguiente?
Una mónada es solo un monoide en la categoría de endofunctores, ¿cuál es el problema?
Y en una nota menos importante, ¿es esto cierto y, de ser así, podría dar una explicación (con suerte, una que pueda entender alguien que no tenga mucha experiencia con Haskell)?
haskell
monads
category-theory
monoids
Roman A. Taycher
fuente
fuente
Respuestas:
Esa frase en particular es de James Iry, de su muy entretenida historia breve, incompleta y mayormente incorrecta de lenguajes de programación , en la que lo atribuye ficticiamente a Philip Wadler.
La cita original es de Saunders Mac Lane en Categorías para el matemático de trabajo , uno de los textos fundamentales de la teoría de categorías. Aquí está en contexto , que es probablemente el mejor lugar para aprender exactamente lo que significa.
Pero, voy a apuñalar. La oración original es esta:
X aquí es una categoría. Los endofunctores son functores de una categoría en sí misma (que generalmente es todo
Functor
en lo que respecta a los programadores funcionales, ya que en su mayoría se trata de una sola categoría; la categoría de tipos, pero estoy divagando). Pero podrías imaginar otra categoría que es la categoría de "endofunctores en X ". Esta es una categoría en la que los objetos son endofunctores y los morfismos son transformaciones naturales.Y de esos endofunctores, algunos de ellos podrían ser mónadas. ¿Cuáles son las mónadas? Exactamente los que son monoidales en un sentido particular. En lugar de detallar el mapeo exacto de mónadas a monoides (ya que Mac Lane lo hace mucho mejor de lo que podría esperar), simplemente pondré sus respectivas definiciones una al lado de la otra y te dejaré comparar:
Un monoide es ...
... cumpliendo estas leyes:
Una mónada es ...
* -> *
con unaFunctor
instancia)join
en Haskell)return
en Haskell)... cumpliendo estas leyes:
Al entrecerrar los ojos, puede ver que ambas definiciones son instancias del mismo concepto abstracto .
fuente
S
es un tipo, todo lo que puede hacer al escribir una funciónf :: () -> S
es elegir un término particular de tipoS
(un "elemento" de la misma, si lo desea) y regresar ... no se le ha dado información real con el argumento, por lo que no hay forma de variar el comportamiento de la función. Porf
lo tanto, debe ser una función constante que simplemente devuelva lo mismo cada vez.()
("Unidad") es el objeto terminal de la categoría Hask , y no es coincidencia que haya exactamente un valor (no divergente) que lo habita.Intuitivamente, creo que lo que dice el elegante vocabulario matemático es que:
Monoide
Un monoide es un conjunto de objetos y un método para combinarlos. Los monoides bien conocidos son:
Hay ejemplos más complejos también.
Además, cada monoide tiene una identidad , que es ese elemento "no operativo" que no tiene efecto cuando se combina con algo más:
Finalmente, un monoide debe ser asociativo . (puede reducir una larga cadena de combinaciones de la forma que desee, siempre que no cambie el orden de izquierda a derecha de los objetos) La adición está bien ((5 + 3) +1 == 5+ (3+ 1)), pero la resta no es ((5-3) -1! = 5- (3-1)).
Monada
Ahora, consideremos un tipo especial de conjunto y una forma especial de combinar objetos.
Objetos
Supongamos que su conjunto contiene objetos de un tipo especial: funciones . Y estas funciones tienen una firma interesante: no llevan números a números o cadenas a cadenas. En cambio, cada función lleva un número a una lista de números en un proceso de dos pasos.
Ejemplos:
Combinando objetos
Además, nuestra forma de combinar funciones es especial. Una forma sencilla de combinar la función es la composición. : tomemos nuestros ejemplos anteriores y compongamos cada función consigo misma:
Sin entrar demasiado en la teoría de tipos, el punto es que puedes combinar dos enteros para obtener un entero, pero no siempre puedes componer dos funciones y obtener una función del mismo tipo. (Las funciones con tipo a -> a compondrán, pero a-> [a] no).
Entonces, definamos una forma diferente de combinar funciones. Cuando combinamos dos de estas funciones, no queremos "ajustar dos veces" los resultados.
Esto es lo que hacemos. Cuando queremos combinar dos funciones F y G, seguimos este proceso (llamado enlace ):
Volviendo a nuestros ejemplos, combinemos (vinculemos) una función consigo misma usando esta nueva forma de "vincular" funciones:
Esta forma más sofisticada de combinar funciones es asociativa (a partir de cómo la composición de funciones es asociativa cuando no está haciendo el envoltorio elegante).
Atarlo todo junto
Notas
Hay muchas formas de "ajustar" los resultados. Puede hacer una lista, o un conjunto, o descartar todos menos el primer resultado mientras observa si no hay resultados, adjunte un sidecar de estado, imprima un mensaje de registro, etc., etc.
He jugado un poco con las definiciones con la esperanza de transmitir la idea esencial de forma intuitiva.
He simplificado un poco las cosas al insistir en que nuestra mónada opera en funciones de tipo a -> [a] . De hecho, las mónadas trabajan en funciones de tipo a -> mb , pero la generalización es una especie de detalle técnico que no es la idea principal.
fuente
a -> [b]
yc -> [d]
(sólo se puede hacer esto sib
=c
), esto no acaba de describir un monoide. En realidad, es la operación de aplanamiento que describió, en lugar de la composición de la función, que es el "operador monoide".a -> [a]
, esto sería un monoide (porque estaría reduciendo la categoría Kleisli a un solo objeto, y cualquier categoría de un solo objeto ¡es por definición un monoide!), pero no capturaría la generalidad completa de la mónada.Primero, las extensiones y bibliotecas que vamos a usar:
De estos,
RankNTypes
es el único que es absolutamente esencial para lo siguiente. Una vez escribí una explicación deRankNTypes
que algunas personas parecen haber encontrado útil , así que me referiré a eso.Citando la excelente respuesta de Tom Crockett , tenemos:
¿Cómo traducimos esto al código Haskell? Bueno, comencemos con la noción de una transformación natural :
Un tipo de formulario
f :-> g
es análogo a un tipo de función, pero en lugar de pensarlo como una función entre dos tipos (de tipo*
), piense en él como un morfismo entre dos functores (cada uno de tipo* -> *
). Ejemplos:Básicamente, en Haskell, las transformaciones naturales son funciones de un tipo
f x
a otro, deg x
modo que lax
variable de tipo es "inaccesible" para la persona que llama. Entonces, por ejemplo,sort :: Ord a => [a] -> [a]
no se puede convertir en una transformación natural, porque es "exigente" sobre qué tipos podemos crear instanciasa
. Una forma intuitiva que suelo usar para pensar en esto es la siguiente:Ahora, con eso fuera del camino, abordemos las cláusulas de la definición.
La primera cláusula es "un endofunctor, T: X -> X ". Bueno, todo
Functor
en Haskell es un endofunctor en lo que la gente llama "la categoría Hask", cuyos objetos son tipos Haskell (de tipo*
) y cuyos morfismos son funciones Haskell. Esto suena como una declaración complicada, pero en realidad es muy trivial. Todo lo que significa es que unFunctor f :: * -> *
le brinda los medios para construir un tipof a :: *
para cualquieraa :: *
y una función afmap f :: f a -> f b
partir de cualquieraf :: a -> b
, y que estos obedecen las leyes de los functores.Segunda cláusula: el
Identity
functor en Haskell (que viene con la Plataforma, por lo que puede importarlo) se define de esta manera:Entonces la transformación natural η: I -> T de la definición de Tom Crockett se puede escribir de esta manera para cualquier
Monad
casot
:Tercera cláusula: la composición de dos functores en Haskell se puede definir de esta manera (que también viene con la Plataforma):
Entonces la transformación natural μ: T × T -> T de la definición de Tom Crockett se puede escribir así:
La afirmación de que este es un monoide en la categoría de endofunctores significa que
Compose
(aplicado parcialmente a sus dos primeros parámetros) es asociativo, y eseIdentity
es su elemento de identidad. Es decir, que tienen los siguientes isomorfismos:Compose f (Compose g h) ~= Compose (Compose f g) h
Compose f Identity ~= f
Compose Identity g ~= g
Estos son muy fáciles de probar porque
Compose
yIdentity
ambos se definen comonewtype
, y los Informes Haskell definen la semántica denewtype
como un isomorfismo entre el tipo que se está definiendo y el tipo de argumento para elnewtype
constructor de datos. Entonces, por ejemplo, demostremosCompose f Identity ~= f
:fuente
Natural
nuevo tipo, no puedo entender qué(Functor f, Functor g)
está haciendo la restricción. ¿Podrías explicar?Functor
restricciones ya que no parecen necesarias. Si no está de acuerdo, no dude en agregarlos nuevamente.join
está definido. Y esajoin
es la proyección del morfismo. Pero no estoy seguro.Nota: No, esto no es cierto. En algún momento hubo un comentario sobre esta respuesta del propio Dan Piponi que decía que la causa y el efecto aquí era exactamente lo contrario, que escribió su artículo en respuesta al comentario de James Iry. Pero parece haber sido eliminado, quizás por algún tidier compulsivo.
A continuación se muestra mi respuesta original.
Es muy posible que Iry haya leído From Monoids to Monads , una publicación en la que Dan Piponi (sigfpe) deriva mónadas de monoids en Haskell, con mucha discusión sobre la teoría de categorías y mención explícita de "la categoría de endofunctores en Hask ". En cualquier caso, cualquiera que se pregunte qué significa para una mónada ser un monoide en la categoría de endofunctores podría beneficiarse al leer esta derivación.
fuente
:-)
.Llegué a esta publicación para comprender mejor la inferencia de la cita infame de la teoría de la categoría de Mac Lane para el matemático que trabaja .
Al describir qué es algo, a menudo es igualmente útil describir lo que no es.
El hecho de que Mac Lane use la descripción para describir una mónada, podría implicar que describe algo único de las mónadas. Tengan paciencia conmigo. Para desarrollar una comprensión más amplia de la declaración, creo que es necesario aclarar que él no describiendo algo que es único para mónadas; la declaración describe igualmente Aplicativo y Flechas entre otros. Por la misma razón, podemos tener dos monoides en Int (Sum y Product), podemos tener varios monoides en X en la categoría de endofunctores. Pero hay aún más en las similitudes.
Tanto Monad como aplicativo cumplen los criterios:
(por ejemplo, en el día a día
Tree a -> List b
, pero en la categoríaTree -> List
)Tree -> List
, soloList -> List
.La declaración usa "Categoría de ..." Esto define el alcance de la declaración. Como ejemplo, la categoría Functor describe el alcance de
f * -> g *
, es decirAny functor -> Any functor
, por ejemplo,Tree * -> List *
oTree * -> Tree *
.Lo que una declaración categórica no especifica describe dónde se permite cualquier cosa y todo .
En este caso, dentro de los functores,
* -> *
akaa -> b
no se especifica qué significaAnything -> Anything including Anything else
. A medida que mi imaginación salta a Int -> String, también incluyeInteger -> Maybe Int
, o inclusoMaybe Double -> Either String Int
dóndea :: Maybe Double; b :: Either String Int
.Entonces la declaración se une de la siguiente manera:
:: f a -> g b
(es decir, cualquier tipo parametrizado a cualquier tipo parametrizado):: f a -> f b
(es decir, cualquier tipo parametrizado al mismo tipo parametrizado) ... dicho de manera diferente,Entonces, ¿dónde está el poder de esta construcción? Para apreciar la dinámica completa, necesitaba ver que los dibujos típicos de un monoide (objeto único con lo que parece una flecha de identidad
:: single object -> single object
) no logran ilustrar que se me permite usar una flecha parametrizada con cualquier número de valores de monoide, del uno objeto de tipo permitido en Monoid. La definición de equivalencia de la flecha endo, ~ ignora el valor de tipo del functor y tanto el tipo como el valor de la capa más interna de "carga útil". Por lo tanto, la equivalencia regresatrue
en cualquier situación en la que coincidan los tipos de functorial (por ejemplo,Nothing -> Just * -> Nothing
es equivalente aJust * -> Just * -> Just *
porque son ambosMaybe -> Maybe -> Maybe
).Barra lateral: ~ afuera es conceptual, pero es el símbolo más a la izquierda adentro
f a
. También describe lo que "Haskell" lee primero (panorama general); por lo que Tipo está "afuera" en relación con un Valor de tipo. La relación entre capas (una cadena de referencias) en la programación no es fácil de relacionar en la Categoría. La Categoría de conjunto se usa para describir Tipos (Int, Strings, Quizás Int, etc.) que incluye la Categoría de Functor (Tipos parametrizados). La cadena de referencia: Tipo de Functor, valores de Functor (elementos del conjunto de ese Functor, por ejemplo, Nothing, Just) y, a su vez, todo lo demás a lo que apunta cada valor de functor. En la categoría, la relación se describe de manera diferente, por ejemplo,return :: a -> m a
se considera una transformación natural de un Functor a otro Functor, diferente de todo lo mencionado hasta ahora.Volviendo al hilo principal, en general, para cualquier producto tensor definido y un valor neutral, la declaración termina describiendo una construcción computacional increíblemente poderosa nacida de su estructura paradójica:
:: List
); estáticofold
que no dice nada sobre la carga útil)En Haskell, es importante aclarar la aplicabilidad de la declaración. El poder y la versatilidad de esta construcción, no tiene absolutamente nada que ver con una mónada per se . En otras palabras, la construcción no se basa en lo que hace que una mónada sea única.
Cuando se trata de averiguar si se debe crear código con un contexto compartido para admitir cálculos que dependen unos de otros, frente a los cálculos que se pueden ejecutar en paralelo, esta declaración infame, con todo lo que describe, no es un contraste entre la elección de Aplicativo, flechas y mónadas, pero más bien es una descripción de cuánto son lo mismo. Para la decisión en cuestión, la declaración es discutible.
Esto a menudo se entiende mal. La declaración continúa describiéndose
join :: m (m a) -> m a
como el producto tensor para el endofunctor monoidal. Sin embargo, no articula cómo, en el contexto de esta declaración,(<*>)
también podría haber sido elegida. Realmente es un ejemplo de seis / media docena. La lógica para combinar valores es exactamente igual; la misma entrada genera la misma salida de cada uno (a diferencia de los monoides de Suma y Producto para Int porque generan resultados diferentes al combinar Ints).Entonces, para recapitular: un monoide en la categoría de endofunctores describe:
(<*>)
y(>>=)
ambos proporcionan acceso simultáneo a los dosm
valores para calcular el valor de retorno único. La lógica utilizada para calcular el valor de retorno es exactamente la misma. Si no fuera por las diferentes formas de las funciones que parametrizan (f :: a -> b
versusk :: a -> m b
) y la posición del parámetro con el mismo tipo de retorno del cálculo (es decir,a -> b -> b
versusb -> a -> b
para cada uno respectivamente), sospecho que podríamos haber parametrizado la lógica monoidal, la producto tensor, para reutilizar en ambas definiciones. A modo de ejercicio para hacer el punto, tratar de poner en práctica~t
, y se termina con(<*>)
y(>>=)
dependiendo de lo que decida definirloforall a b
.Si mi último punto es mínimo conceptualmente verdadero, entonces explica la diferencia computacional precisa y única entre Applicative y Monad: las funciones que parametrizan. En otras palabras, la diferencia es externa a la implementación de estas clases de tipos.
En conclusión, según mi propia experiencia, la cita infame de Mac Lane proporcionó un gran meme "goto", una guía a la que debo referirme mientras navego por la Categoría para comprender mejor los modismos utilizados en Haskell. Logra capturar el alcance de una poderosa capacidad de computación hecha maravillosamente accesible en Haskell.
Sin embargo, hay ironía en cómo primero entendí mal la aplicabilidad de la declaración fuera de la mónada, y lo que espero transmitió aquí. Todo lo que describe resulta ser similar entre Aplicativo y Mónadas (y Arrows entre otros). Lo que no dice es precisamente la pequeña pero útil distinción entre ellos.
- E
fuente
Las respuestas aquí hacen un excelente trabajo al definir tanto monoides como mónadas, sin embargo, todavía no parecen responder la pregunta:
El quid de la cuestión que falta aquí es la noción diferente de "monoide", la denominada categorización más precisamente: la de monoide en una categoría monoidal. Lamentablemente, el libro de Mac Lane lo hace muy confuso :
Confusión principal
¿Por qué es esto confuso? Porque no define qué es "monoide en la categoría de endofunctores" de
X
. En cambio, esta oración sugiere tomar un monoide dentro del conjunto de todos los endofunctores junto con la composición del functor como operación binaria y el functor de identidad como una unidad monoidal. Que funciona perfectamente bien y convierte en un monoide cualquier subconjunto de endofunctores que contiene el functor de identidad y está cerrado bajo la composición del functor.Sin embargo, esta no es la interpretación correcta, que el libro no deja en claro en esa etapa. Una mónada
f
es un endofunctor fijo , no un subconjunto de endofunctores cerrados en composición. Una construcción común es usarf
para generar un monoide tomando el conjunto dek
composiciones plegadasf^k = f(f(...))
def
sí mismo, incluido elk=0
que corresponde a la identidadf^0 = id
. Y ahora el conjuntoS
de todos estos poderes para todosk>=0
es de hecho un monoide "con producto × reemplazado por composición de endofunctores y unidad establecida por el endofunctor de identidad".Y todavía:
S
se puede definir para cualquier functorf
o incluso literalmente para cualquier auto-mapa deX
. Es el monoide generado porf
.S
dada por la composición functor y el functor de identidad no tiene nada que ver conf
ser o no ser una mónada.Y para hacer las cosas más confusas, la definición de "monoide en la categoría monoidal" aparece más adelante en el libro, como puede ver en la tabla de contenido . Y, sin embargo, comprender esta noción es absolutamente fundamental para comprender la conexión con las mónadas.
Categorías (estrictas) monoidales
Pasando al Capítulo VII sobre Monoides (que viene después del Capítulo VI sobre Mónadas), encontramos la definición de la llamada categoría monoidal estricta como triple
(B, *, e)
, dondeB
es una categoría,*: B x B-> B
un bifunctor (functor con respecto a cada componente con otro componente fijo ) ye
es un objeto unitario queB
satisface las leyes de asociatividad y unidad:para cualquier objeto
a,b,c
deB
, y las mismas identidades para cualquier morfismoa,b,c
cone
reemplazado porid_e
, el morfismo de identidad dee
. Ahora es instructivo observar que en nuestro caso de interés, donde seB
encuentra la categoría de endofunctoresX
con transformaciones naturales como morfismos,*
la composición del functor ye
el functor de identidad, se cumplen todas estas leyes, como puede verificarse directamente.Lo que viene después en el libro es la definición de la categoría monoidal "relajada" , donde las leyes solo contienen algunas transformaciones naturales fijas que satisfacen las llamadas relaciones de coherencia , lo que sin embargo no es importante para nuestros casos de las categorías de endofunctores.
Monoides en categorías monoidales
Finalmente, en la sección 3 "Monoides" del Capítulo VII, se da la definición real:
Haciendo 3 diagramas conmutativos. Recordemos que en nuestro caso, estos son morfismos en la categoría de endofunctores, que son transformaciones naturales correspondientes a una mónada
join
y precisamentereturn
. La conexión se vuelve aún más clara cuando hacemos que la composición sea*
más explícita, reemplazandoc * c
porc^2
dóndec
está nuestra mónada.Finalmente, observe que los 3 diagramas conmutativos (en la definición de un monoide en la categoría monoidal) están escritos para categorías monoidales generales (no estrictas), mientras que en nuestro caso todas las transformaciones naturales que surgen como parte de la categoría monoidal son en realidad identidades. Eso hará que los diagramas sean exactamente iguales a los de la definición de una mónada, completando la correspondencia.
Conclusión
En resumen, cualquier mónada es, por definición, un endofunctor, por lo tanto, un objeto en la categoría de endofunctores, donde el monádico
join
y losreturn
operadores satisfacen la definición de un monoide en esa categoría monoidal particular (estricta) . Viceversa, cualquier monoide en la categoría monoidal de endofunctores es, por definición, un triple que(c, mu, nu)
consiste en un objeto y dos flechas, por ejemplo, transformaciones naturales en nuestro caso, que satisfacen las mismas leyes que una mónada.Finalmente, observe la diferencia clave entre los monoides (clásicos) y los monoides más generales en categorías monoidales. Las dos flechas
mu
ynu
arriba ya no son una operación binaria y una unidad en un conjunto. En cambio, tiene un endofunctor fijoc
. La composición del functor*
y el functor de identidad por sí solos no proporcionan la estructura completa necesaria para la mónada, a pesar de esa observación confusa en el libro.Otro enfoque sería comparar con el monoide estándar
C
de todos los auto-mapas de un conjuntoA
, donde la operación binaria es la composición, que se puede ver a mapear el producto cartesiano estándarC x C
enC
. Pasando al monoide categorizado, estamos reemplazando el producto cartesianox
con la composición del functor*
, y la operación binaria se reemplaza con la transformación naturalmu
dec * c
ac
, que es una colección dejoin
operadorespara cada objeto
T
(escriba en la programación). Y los elementos de identidad en monoides clásicos, que pueden identificarse con imágenes de mapas de un conjunto fijo de un punto, se reemplazan con la colección dereturn
operadoresPero ahora no hay más productos cartesianos, por lo que no hay pares de elementos y, por lo tanto, no hay operaciones binarias.
fuente