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


¿Quién dijo primero lo siguiente?

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

Y en una nota menos importante, ¿es cierto y, de ser así, podrías dar una explicación (con suerte, una que pueda ser comprendida por alguien que no tenga mucha experiencia Haskell)?


619
2017-10-06 06:55


origen


Respuestas:


Ese particular fraseo es de James Iry, de su muy entretenido Historia breve, incompleta y en su mayoría incorrecta de lenguajes de programación, en la cual lo atribuye ficticiamente a Philip Wadler.

La cita original es de Saunders Mac Lane en Categorías para el matemático que trabaja, 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, 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 endofunctors de X, con producto × reemplazado por composición de endofunctors y unidad establecida por el endofunctor de identidad.

X aquí hay una categoría Los endofunctors son funtores de una categoría en sí misma (que generalmente es todas  Functors 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 "endofunctors on X". Esta es una categoría en la que los objetos son endofunctors y los morfismos son transformaciones naturales.

Y de esos endofunctors, algunos de ellos podrían ser mónadas. ¿Cuáles son mónadas? Solo exactamente los que son monoidal en un sentido particular En lugar de deletrear el mapeo exacto de las mónadas a los monoides (ya que Mac Lane lo hace mucho mejor de lo que podía esperar), pondré sus respectivas definiciones una al lado de la otra y te dejaré 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 un, segundo y do en S
  • e • a = a • e = a, para todos un en S

Una mónada es ...

  • Un endofunctor, T: X → X (en Haskell, un constructor tipo de tipo * -> * con un Functor ejemplo)
  • Una transformación natural, μ: T × T → T, dónde × significa la composición del functor (también conocida como join en Haskell)
  • Una transformación natural, η: I → T, dónde yo es la identidad endofunctor en X (también conocido como return en Haskell)

... satisfaciendo estas leyes:

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

Con un poco de entrecerrar los ojos, es posible que pueda ver que ambas definiciones son ejemplos de lo mismo concepto abstracto.


680
2017-10-06 07:35



Intuitivamente, creo que lo que el vocabulario matemático de lujo está diciendo es que:

Monoide

UN monoide es un conjunto de objetos y un método para combinarlos. Los monoides bien conocidos son:

  • números que puedes agregar
  • listas que puedes concatenar
  • establece que puedes sindicato

Hay ejemplos más complejos también.

Promover, cada monoid tiene un identidad, que es ese elemento "no operativo" que no tiene ningún efecto cuando lo combinas con otra cosa:

  • 0 + 7 == 7 + 0 == 7
  • [] ++ [1,2,3] == [1,2,3] ++ [] == [1,2,3]
  • {} Unión {manzana} == {manzana} Unión {} == {manzana}

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

  1. Calcule 0 o más resultados
  2. Combine esos resultados a una sola respuesta de alguna manera.

Ejemplos:

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

Combinar objetos

Además, nuestra forma de combinar funciones es especial. Una forma simple de combinar la función es composición: Tomemos nuestros ejemplos de arriba, y redactemos cada función consigo mismo:

  • 1 -> [1] -> [[1]] (envuelva la entrada, dos veces)
  • 1 -> [] -> [] (descartar la entrada, ajustar 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. (Funciones con tipo a -> a  compondrá, pero a-> [a] no lo hará)

Entonces, definamos una manera diferente de combinar funciones. Cuando combinamos dos de estas funciones, no queremos "doble-envolver" los resultados.

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

  1. Calcule los "resultados" de F pero no los combine.
  2. Calcule los resultados de aplicar G a cada uno de los resultados de F por separado, obteniendo una colección de recolección de resultados.
  3. Aplane la colección de 2 niveles y combine todos los resultados.

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

  • 1 -> [1] -> [1] (envuelva la entrada, dos veces)
  • 1 -> [] -> [] (descartar la entrada, ajustar la nada en una lista, dos veces)
  • 1 -> [2] -> [3] (agregue 1, luego agregue 1 de nuevo y ajuste 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 hágalo todo de nuevo en ambos resultados, y luego ajuste el resultado final resultados en una lista).

Esta forma más sofisticada de combinar funciones es asociativo (siguiendo la forma en que la composición de la función es asociativa cuando no se está haciendo el envoltorio).

Atando todo,

  • una mónada es una estructura que define una forma de combinar (los resultados de) funciones,
  • análogamente 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 se puede combinar con cualquier alguna cosa para resultar en alguna cosa sin alterar.

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, adjuntar un sidecar de estado, imprimir 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 funciona en funciones de tipo a -> [a]. De hecho, las mónadas trabajan en funciones de tipo a -> m b, pero la generalización es una especie de detalle técnico que no es la percepción principal.


463
2018-05-02 00:07



Primero, las extensiones y bibliotecas que vamos a usar:

{-# LANGUAGE RankNTypes, TypeOperators #-}

import Control.Monad (join)

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

Citando Excelente respuesta de Tom Crockett, tenemos:

Una mónada es ...

  • Un endofunctor, T: X -> X
  • Una transformación natural, μ: T × T -> T, dónde × significa composición del funtor
  • Una transformación natural, η: I -> T, dónde yo es la identidad endofunctor 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 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 pensarlo como un función entre dos tipos (de amable *), piense en ello como 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 f x a otro tipo g x de tal manera que x la variable tipo es "inaccesible" para la persona que llama. Así por ejemplo, sort :: Ord a => [a] -> [a] no se puede convertir en una transformación natural, porque es "quisquilloso" con respecto a qué tipos podemos instanciar para a. Una forma intuitiva que suelo usar para pensar en esto es la siguiente:

  • Un functor es una forma de operar en el contenido de algo sin tocar el estructura.
  • Una transformación natural es una forma de operar en el 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 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 eso Functor f :: * -> * te da los medios para construir un tipo f a :: * para cualquier a :: * y una función fmap f :: f a -> f b fuera de cualquier f :: a -> b, y que estos obedezcan las leyes de funtores.

Segunda cláusula: el Identity Functor 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)

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

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

Tercera cláusula: la composición de dos funtores 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)

Entonces 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 este es un monoide en la categoría de endofunctors significa que Compose (aplicado parcialmente a solo sus dos primeros parámetros) es asociativo, y eso Identity es su elemento de identidad Es decir, que los siguientes isomorfismos son válidos:

  • 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 y Identity ambos se definen como newtype, y los Informes Haskell definen la semántica de newtype como un isomorfismo entre el tipo que se define y el tipo de argumento para el newtypeconstructor de datos Entonces, por ejemplo, demostremos 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.

76
2017-09-16 06:58



Nota: No, esto no es verdad En algún momento hubo un comentario sobre esta respuesta del propio Dan Piponi que decía que la causa y efecto aquí era exactamente lo opuesto, que escribió su artículo en respuesta a la broma de James Iry. Pero parece haber sido eliminado, tal vez por algún orden compulsivo.

A continuación está mi respuesta original.


Es muy posible que Iry haya leído De Monoids a las Mónadas, un post en el que Dan Piponi (sigfpe) deriva mónadas de monoides en Haskell, con mucha discusión de la teoría de categorías y mención explícita de "la categoría de endofunctors en Hask". En cualquier caso, cualquiera que se pregunte qué significa que una mónada sea un monoide en la categoría de endofunctors podría beneficiarse al leer esta derivación.


5
2018-04-20 22:53



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

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 para las mónadas. Tengan paciencia conmigo. Para desarrollar una comprensión más amplia de la declaración, creo que debe quedar claro que él es no describiendo algo que es exclusivo de las mónadas; la declaración describe igualmente Applicative y Arrows entre otros. Por la misma razón podemos tener dos monoides en Int (Suma y Producto), podemos tener varios monoides en X en la categoría de endofunctors. Pero aún hay más en las similitudes.

Tanto Monad como Applicative 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 día a día Tree a -> List b, pero en la categoría Tree -> List)

  • monoid => objeto individual; es decir, un único tipo, pero en este contexto, solo con respecto a la capa externa; entonces, no podemos tener Tree -> List, solamente List -> 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 decir, Any functor -> Any functor, p.ej., Tree * -> List * o Tree * -> Tree *.

Lo que una declaración categórica no especifica describe dónde cualquier cosa y todo está permitido.

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

Entonces la declaración se une de la siguiente manera:

  • alcance del funcionador :: f a -> g b (es decir, cualquier tipo parametrizado a cualquier tipo parametrizado)
  • endo + functor :: f a -> f b (es decir, cualquier tipo parametrizado al 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 los dibujos típicos de un monoide (un solo objeto con lo que parece una flecha de identidad, :: single object -> single object), no ilustra que se me permite usar una flecha parametrizada con cualquier número de los valores de monoid, de uno tipo de objeto permitido en Monoid. La definición de equivalencia de endo, ~ identity arrow ignora el functor valor de tipo y tanto el tipo como el valor de la capa más interna, "carga útil". Por lo tanto, vuelve la equivalencia true en cualquier situación donde los tipos de funcionamientos coincidan (p. Nothing -> Just * -> Nothing es equivalente a Just * -> Just * -> Just * porque ambos son Maybe -> Maybe -> Maybe)

Barra lateral: ~ afuera es conceptual, pero es el símbolo más a la izquierda en f a. También describe lo que "Haskell" lee primero (imagen grande); por lo que Type 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 utiliza para describir Tipos (Int, Strings, Maybe Int, etc.) que incluye la Categoría de Functor (Tipos parametrizados). La cadena de referencia: Tipo de Functor, valores de Functor (elementos de ese conjunto de Functor, por ejemplo, Nothing, Just) y, a su vez, todo lo demás a los que apunta cada valor de functor. En 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 neutro, la afirmación termina describiendo una construcción computacional increíblemente poderosa nacida de su estructura paradójica:

  • en el exterior aparece como un solo objeto (p. :: List); estático
  • pero adentro, permite muchas dinámicas
    • cualquier cantidad de valores del mismo tipo (por ejemplo, Empty | ~ NonEmpty) como forraje para funciones de cualquier arity. El producto tensor reducirá cualquier cantidad de entradas a un solo valor ... para la capa externa (~fold eso no dice nada sobre la carga útil)
    • rango infinito de ambos el tipo y 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 tiene absolutamente nada que ver con una mónada per se. En otras palabras, la construcción no depende de lo que hace que una mónada sea única.

Al tratar de averiguar si se debe construir un código con un contexto compartido para respaldar cálculos que dependen el uno del otro, en comparación con 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 iguales. Para la decisión a mano, la declaración es discutible.

Esto a menudo es malentendido. La declaración continúa describiendo 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 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 Suma y Producto para Int porque generan resultados diferentes cuando se combinan Ints).

Entonces, para recapitular: Un monoide en la categoría de endofunctors describe:

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

(<*>) y (>>=) ambos proporcionan acceso simultáneo a los dos m valores para calcular el único valor de retorno. 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 versus k :: a -> m b) 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 tensor, para su reutilización en ambas definiciones. Como ejercicio para aclarar el asunto, intente e implemente ~ty terminas con (<*>) y (>>=) dependiendo de cómo decidas definirlo forall a b.

Si mi último punto es al menos conceptualmente verdadero, entonces explica la diferencia computacional precisa y única entre Applicative y Monad: las funciones que parametrizan. En otras palabras, la diferencia es externo 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 meme "goto", una guía para que lo referenciara mientras navegaba a través de Category para comprender mejor los modismos utilizados en Haskell. Logra capturar el alcance de una poderosa capacidad de cómputo hecha maravillosamente accesible en Haskell.

Sin embargo, hay ironía en cómo malinterpreté por primera vez la aplicabilidad de la declaración fuera de la mónada, y lo que espero transmitir aquí. Todo lo que describe resulta ser lo que es similar entre Aplicativo y Mónadas (y Flechas, entre otros). Lo que no dice es precisamente la pequeña pero útil distinción entre ellos.

- E


2