haskell - Una mónada es solo un monoide en la categoría de endofunctores, ¿cuál es el problema?

monads category-theory

Question

¿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 ser entendida por alguien que no tiene mucha experiencia con Haskell)?

Answer 1

Esa frase en particular es de James Iry, de su muy entretenida historia breve, incompleta y en su mayoría incorrecta de los lenguajes de programación , en la que se la atribuye a Philip Wadler.

La cita original es de Saunders Mac Lane en Categories for the Mathematician , 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 tomar una puñalada. La oración original es esta:

En total, una mónada en X es solo un monoide en la categoría de endofunctores de X, con el producto × reemplazado por la composición de endofunctores y la unidad establecida por el endofunctor de identidad.

X aquí hay una categoría. Los endofunctores son functors de una categoría a sí mismos (que generalmente son todos los Functor s en lo que concierne a los programadores funcionales, ya que en su mayoría se trata de una sola categoría: la categoría de tipos, pero me desvío del tema). Pero podría imaginar otra categoría que sea 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 pueden ser mónadas. ¿Cuáles son las mónadas? Justo exactamente los que son monoides en un sentido particular. En lugar de detallar la asignación exacta de las mónadas a los monoides (ya que Mac Lane lo hace mucho mejor de lo que podría esperar), solo pondré sus respectivas definiciones de lado a lado y le permitiré comparar:

Un monoide es ...

• Un conjunto, s
• Una operación, •: S × S → S
• Un elemento de S , e: 1 → S

... satisfaciendo estas leyes:

• (a • b) • c = a • (b • c) , para todos a , b y c en S
• e • a = a • e = a , para todas a en S

Una mónada es ...

• Un endofunctor, T: X → X (en Haskell, un tipo constructor de tipo * -> * con una instancia de Functor )
• Una transformación natural, μ: T × T → T , donde x significa composición del funtor (también conocido como join en Haskell)
• Una transformación natural, η: I → T , donde I es el endofunctor de identidad en X (también conocido como return en Haskell)

... satisfaciendo estas leyes:

• μ ∘ Tμ = μ ∘ μT
• μ ∘ Tη = μ ∘ ηT = 1 (la transformación natural de la identidad)

Con un poco de entrecerrar los ojos, podría ver que ambas definiciones son instancias del mismo concepto abstracto .

Answer 2

Intuitivamente, creo que lo que dice el vocabulario matemático de fantasía es que:

Monoide

Un monoide es un conjunto de objetos y un método para combinarlos. Monoides bien conocidos son:

• números que puedes agregar
• listas que puedes concatenar
• establece que puedes unión

También hay ejemplos más complejos.

Además, cada monoide tiene una identidad , que es ese elemento "no-op" que no tiene efecto cuando lo combinas con otra cosa:

• 0 + 7 == 7 + 0 == 7
• [] ++ [1,2,3] == [1,2,3] ++ [] == [1,2,3]
• {} union {apple} == {apple} union {} == {apple}

Finalmente, un monoide debe ser asociativo . (puede reducir una larga cadena de combinaciones de todas formas, siempre que no cambie el orden de los objetos de izquierda a derecha) 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 su lugar, cada función lleva un número a una lista de números en un proceso de dos pasos.

1. Calcular 0 o más resultados
2. Combina esos resultados para una sola respuesta de alguna manera.

Ejemplos:

• 1 -> [1] (solo envuelve la entrada)
• 1 -> [] (descartar la entrada, envolver la nada en una lista)
• 1 -> [2] (agregue 1 a la entrada y envuelva el resultado)
• 3 -> [4, 6] (agregue 1 a la entrada, multiplique la entrada por 2 y ajuste los resultados múltiples )

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 con ella misma:

• 1 -> [1] -> [[1]] (envuelva la entrada dos veces)
• 1 -> [] -> [] (descartar la entrada, envolver la nada en una lista, dos veces)
• 1 -> [2] -> [UH-OH! ] (no podemos "agregar 1" a una lista! ")
• 3 -> [4, 6] -> [UH-OH! ] (no podemos agregar 1 una lista!)

Sin entrar demasiado en la teoría de tipos, el punto es que puede combinar dos enteros para obtener un entero, pero no siempre puede componer dos funciones y obtener una función del mismo tipo. (Las funciones con tipo a -> a se compondrán, pero a-> [a] no lo harán).

Entonces, vamos a definir una forma diferente de combinar funciones. Cuando combinamos dos de estas funciones, no queremos "envolver dos veces" los resultados.

Esto es lo que hacemos. Cuando queremos combinar dos funciones F y G, seguimos este proceso (llamado enlace ):

1. Calcule los "resultados" de F pero no los combine.
2. Calcule los resultados de la aplicación de G a cada uno de los resultados de F por separado, produciendo una recopilación de la colección de resultados.
3. Aplana la colección de 2 niveles y combina todos los resultados.

Volviendo a nuestros ejemplos, combinemos (unamos) una función con ella misma utilizando esta nueva forma de funciones de "enlace":

• 1 -> [1] -> [1] (envuelva la entrada, dos veces)
• 1 -> [] -> [] (descartar la entrada, envolver la nada en una lista, dos veces)
• 1 -> [2] -> [3] (agregue 1, luego agregue 1 nuevamente, y envuelva el resultado).
• 3 -> [4,6] -> [5,8,7,12] (agregue 1 a la entrada, y también multiplique la entrada por 2, manteniendo ambos resultados, luego vuelva a hacerlo todo para ambos resultados, y luego ajuste la final resultados en una lista.)

Esta forma más sofisticada de combinar funciones es asociativa (a partir de cómo la composición de la función es asociativa cuando no estás haciendo las cosas más sofisticadas).

Atando todo junto,

• una mónada es una estructura que define una forma de combinar (los resultados de) funciones,
• de manera análoga a cómo un monoide es una estructura que define una forma de combinar objetos,
• donde el método de combinación es asociativo,
• y donde hay un ''No-op'' especial que puede combinarse con cualquier cosa para obtener algo sin cambios.

Notas

Hay muchas formas de "envolver" los resultados. Puede hacer una lista, 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 manera intuitiva.

He simplificado un poco las cosas insistiendo en que nuestra mónada opera en funciones de tipo a -> [a] . De hecho, las mónadas funcionan en funciones de tipo a -> mb , pero la generalización es una especie de detalle técnico que no es la idea principal.

Answer 3

Llegué a este post para comprender mejor la inferencia de la infame cita de la Teoría de la Categoría de Mac Lane para el matemático trabajador .

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 exclusivo 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 no está describiendo algo que sea exclusivo de las mónadas; La declaración también describe el Aplicativo y las Flechas entre otros. Por la misma razón que podemos tener dos monoides en Int (Suma y Producto), podemos tener varios monoides en X en la categoría de endofunctores. Pero hay aún más a las similitudes.

Tanto la mónada como el aplicativo cumplen los criterios:

• endo => cualquier flecha, o morfismo que comienza y termina en el mismo lugar
• functor => cualquier flecha, o morfismo entre dos categorías

  (por ejemplo, en el Tree a -> List b día a día Tree a -> List b , pero en el Tree -> List categorías Tree -> List )

• monoide => objeto único; es decir, un solo tipo, pero en este contexto, solo en lo que respecta a la capa externa; entonces, no podemos tener Tree -> List , solo List -> List .

La declaración usa "Categoría de ..." Esto define el alcance de la declaración. Como ejemplo, la Categoría de Functor describe el alcance de f * -> g * , es decir, Any functor -> Any functor , por ejemplo, Tree * -> List * o Tree * -> Tree * .

Lo que no especifica una declaración categórica describe dónde se permite cualquier cosa y todo .

En este caso, dentro de los funtores, * -> * aka a -> b no se especifica, lo que significa Anything -> Anything including Anything else . Cuando mi imaginación salta a Int -> String, también incluye Integer -> Maybe Int , o incluso Maybe Double -> Either String Int donde a :: Maybe Double; b :: Either String Int a :: Maybe Double; b :: Either String Int .

Así que la declaración viene de la siguiente manera:

• functor scope :: fa -> gb (es decir, cualquier tipo parametrizado a cualquier tipo parametrizado)
• endo + functor :: fa -> fb (es decir, cualquier tipo parametrizado para el mismo tipo parametrizado) ... dicho de otra manera,
• Un monoide en la categoría de endofunctor.

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 (un solo objeto con lo que parece una flecha de identidad, :: single object -> single object ), no ilustran que tengo permiso para usar una flecha parametrizado con cualquier número de valores monoides, a partir del único tipo de objeto permitido en Monoid. La definición de equivalencia de la flecha endo, ~ identidad, ignora el valor de tipo del functor y tanto el tipo como el valor de la capa más interna, "carga útil". Por lo tanto, la equivalencia se vuelve true en cualquier situación en la que los tipos de funciones coincidan (p. Ej., Nothing -> Just * -> Nothing es equivalente a Just * -> Just * -> Just * porque ambos son Maybe -> Maybe -> Maybe ).

Barra lateral: ~ el exterior es conceptual, pero es el símbolo más a la izquierda en fa . También describe lo que "Haskell" lee primero (imagen general); por lo que el Tipo está "fuera" 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 Categoría. La Categoría de conjunto se usa para describir los Tipos (Int, Cadenas, Tal vez Int, etc.) que incluyen 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 al que apunta cada valor de functor. En Categoría, la relación se describe de manera diferente, por ejemplo, return :: a -> ma se considera una transformación natural de un Functor a otro Functor, diferente de cualquier cosa mencionada hasta ahora.

De vuelta al hilo principal, en definitiva, para cualquier producto de tensor definido y un valor neutral, la declaración termina describiendo una construcción computacional asombrosamente poderosa nacida de su estructura paradójica:

• en el exterior aparece como un solo objeto (por ejemplo, :: List ); estático
• Pero por dentro, permite mucha dinámica.
  • cualquier número de valores del mismo tipo (p. ej., Vacío | ~ No vacío) como forraje para funciones de cualquier aridad. El producto tensorial reducirá cualquier cantidad de entradas a un solo valor ... para la capa externa (~ fold que no dice nada sobre la carga útil)
  • Rango infinito tanto del tipo como de los valores para la capa más interna.

En Haskell, aclarar la aplicabilidad de la declaración es importante. El poder y la versatilidad de esta construcción no tienen absolutamente nada que ver con una mónada en sí . 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 construir código con un contexto compartido para admitir cálculos que dependen unos de otros, en comparación con los cálculos que se pueden ejecutar en paralelo, esta infame declaración, con todo lo que describe, no es un contraste entre la elección de Aplicativo, flechas y mónadas, sino que más bien es una descripción de cuánto son iguales. Para la decisión en cuestión, la declaración es discutible.

Esto es a menudo mal entendido. La declaración continúa describiendo join :: m (ma) -> ma como el producto tensorial para el endofunctor monoidal. Sin embargo, no expresa cómo, en el contexto de esta declaración, (<*>) también podría haber sido elegido. 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 Sum y Product para Int porque generan diferentes resultados al combinar Ints).

Entonces, para recapitular: un monoide en la categoría de endofunctores describe:

   ~t :: m * -> m * -> m *
   and a neutral value for m *

(<*>) y (>>=) proporcionan acceso simultáneo a los dos valores de m 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, se parametrizan ( f :: a -> b versus k :: a -> mb ) y la posición del parámetro con el mismo tipo de retorno del cálculo (es decir, a -> b -> b versus b -> a -> b para cada uno respectivamente), sospecho que podríamos haber parametrizado la lógica monoidal, el producto tensorial, para reutilizarla en ambas definiciones. Como ejercicio para hacer el punto, intente e implemente ~t , y terminará con (<*>) y (>>=) dependiendo de cómo decida definirlo para todo forall ab .

Si mi último punto es, como mínimo, conceptualmente verdadero, entonces explica la diferencia precisa, y solo computacional, entre el Aplicativo y la Mónada: las funciones que parametrizan. En otras palabras, la diferencia es externa a la implementación de estas clases de tipos.

En conclusión, en mi propia experiencia, la infame cita de Mac Lane me proporcionó un gran memo "goto", una guía para que yo haga referencia mientras navego por la Categoría para comprender mejor los modismos utilizados en Haskell. Tiene éxito en capturar el alcance de una poderosa capacidad de cómputo hecha maravillosamente accesible en Haskell.

Sin embargo, hay una ironía en la forma en que primero entendí mal la aplicabilidad de la declaración fuera de la mónada y lo que espero transmitir aquí. Todo lo que describe resulta ser similar entre el Aplicativo y las Mónadas (y las Flechas entre otras). Lo que no dice es precisamente la pequeña pero útil distinción entre ellos.

- E

Answer 4

Primero, las extensiones y bibliotecas que vamos a utilizar:

{-# LANGUAGE RankNTypes, TypeOperators #-}

import Control.Monad (join)

De estos, RankNTypes es el único que es absolutamente esencial para lo siguiente. Una vez escribí una explicación de RankNTypes que algunas personas parecen haber encontrado útil , así que me referiré a eso.

Citando la excelente respuesta de Tom Crockett , tenemos:

Una mónada es ...

• Un endofunctor, T: X -> X
• Una transformación natural, μ: T × T -> T , donde x significa composición del funtor
• Una transformación natural, η: I -> T , donde I es el endofunctor de identidad en X

... satisfaciendo estas leyes:

• μ (μ (T × T) × T)) = μ (T × μ (T × T))
• μ (η (T)) = T = μ (T (η))

¿Cómo traducimos esto al código de Haskell? Bueno, comencemos con la noción de una transformación natural :

-- | A natural transformations between two ''Functor'' instances.  Law:
--
-- > fmap f . eta g == eta g . fmap f
--
-- Neat fact: the type system actually guarantees this law.
--
newtype f :-> g =
    Natural { eta :: forall x. f x -> g x }

Un tipo de la forma f :-> g es análogo a un tipo de función, pero en lugar de pensar en él como una función entre dos tipos (de tipo * ), considérelo como un morfismo entre dos funtores (cada uno de tipo * -> * ). Ejemplos:

listToMaybe :: [] :-> Maybe
listToMaybe = Natural go
    where go [] = Nothing
          go (x:_) = Just x

maybeToList :: Maybe :-> []
maybeToList = Natural go
    where go Nothing = []
          go (Just x) = [x]

reverse'' :: [] :-> []
reverse'' = Natural reverse

Básicamente, en Haskell, las transformaciones naturales son funciones de algún tipo fx a otro tipo gx , por lo que la variable de tipo x es "inaccesible" para el llamador. Entonces, por ejemplo, sort :: Ord a => [a] -> [a] no puede convertirse en una transformación natural, porque es "delicado" sobre qué tipos podemos instanciar para a . Una forma intuitiva que a menudo utilizo para pensar en esto es la siguiente:

• Un functor es una forma de operar sobre el contenido de algo sin tocar la estructura .
• Una transformación natural es una forma de operar en la estructura de algo sin tocar o mirar el contenido .

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, cada Functor en Haskell es un endofunctor en lo que la gente llama "la categoría Hask", cuyos objetos son tipos de Haskell (de tipo * ) y cuyos morfismos son funciones de Haskell. Esto suena como una declaración complicada, pero en realidad es muy trivial. Todo lo que significa es que un Functor f :: * -> * le proporciona los medios para construir un tipo fa :: * para cualquier a :: * y una función fmap f :: fa -> fb fuera de cualquier f :: a -> b , y que estas obedecen a las leyes funtoras.

Segunda cláusula: el functor de Identity en Haskell (que viene con la plataforma, por lo que puede importarlo) se define de esta manera:

newtype Identity a = Identity { runIdentity :: a }

instance Functor Identity where
    fmap f (Identity a) = Identity (f a)

Así que la transformación natural η: I -> T de la definición de Tom Crockett se puede escribir de esta manera para cualquier instancia de Monad t :

return'' :: Monad t => Identity :-> t
return'' = Natural (return . runIdentity)

Tercera cláusula: la composición de dos functors en Haskell se puede definir de esta manera (que también viene con la plataforma):

newtype Compose f g a = Compose { getCompose :: f (g a) }

-- | The composition of two ''Functor''s is also a ''Functor''.
instance (Functor f, Functor g) => Functor (Compose f g) where
    fmap f (Compose fga) = Compose (fmap (fmap f) fga)

Así que la transformación natural μ: T × T -> T de la definición de Tom Crockett se puede escribir así:

join'' :: Monad t => Compose t t :-> t
join'' = Natural (join . getCompose)

La afirmación de que se trata de un monoide en la categoría de endofunctores significa que Compose (parcialmente aplicado a sus dos primeros parámetros) es asociativo, y que Identity es su elemento de identidad. Es decir, que sostienen los siguientes isomorfismos:

• Compose f (Compose gh) ~= Compose (Compose fg) h
• Compose f Identity ~= f
• Compose Identity g ~= g

Estos son muy fáciles de probar porque Compose e Identity se definen como newtype , y los Informes de Haskell definen la semántica de newtype como un isomorfismo entre el tipo que se define y el tipo del argumento para el constructor de datos del newtype . Entonces, por ejemplo, vamos a probar Compose f Identity ~= f :

Compose f Identity a
    ~= f (Identity a)                 -- newtype Compose f g a = Compose (f (g a))
    ~= f a                            -- newtype Identity a = Identity a
Q.E.D.

Answer 5

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 a la broma de James Iry. Pero parece que se ha eliminado, tal vez por algún orden compulsivo compulsivo.

A continuación se muestra mi respuesta original.

Es muy posible que Iry haya leído From Monoids to Monads , un post en el que Dan Piponi (sigfpe) deriva las mónadas de monoids en Haskell, con mucha discusión sobre la teoría de categorías y la mención explícita de "la categoría de Hask 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.