monadas monada monad haskell category-theory

haskell - monadas



Plegable, monoide y mónada. (3)

Considera la siguiente firma de foldMap

foldMap :: (Foldable t, Monoid m) => (a -> m) -> t a -> m

Esto es muy similar a "bind", solo con los argumentos intercambiados:

(>>=) :: Monad m => m a -> (a -> m b) -> m b

Me parece que, por lo tanto, debe haber algún tipo de relación entre Foldable , Monoid y Monad , pero no puedo encontrarlo en las superclases. Presumiblemente puedo transformar uno o dos de estos en el otro, pero no estoy seguro de cómo.

¿Podría esa relación ser detallada?


Monoid y Monad

Wow, esta es una de las pocas veces en que podemos usar la cita:

Una mónada es solo un monoide en la categoría de endofunctores, [...]

Vamos a empezar con un monoide. Un monoide en la categoría Set de conjuntos es un conjunto de elementos m con un elemento vacío mempty y una función asociativa mappend para combinar elementos tales que

mempty `mappend` x == x -- for any x x `mappend` mempty == x -- for any x -- and a `mappend` (b `mappend` c) == (a `mappend` b) `mappend` c -- for all a, b, c

Tenga en cuenta que un monoide no está limitado a conjuntos, también existen monoides en la categoría Cat de categorías (mónadas) y así sucesivamente. Básicamente, en cualquier momento usted tiene una operación binaria asociativa y una identidad para ello.

Ahora una mónada, que es un "monoide en la categoría de endofunctores" tiene las siguientes propiedades:

Es un endofunctor, eso significa que tiene el tipo * -> * en los Hask de Categoría Hask de Haskell.

Ahora, para ir más lejos, debe conocer un poco de la teoría de categorías que intentaré explicar aquí: dados dos functors F y G , existe una transformación natural de F a G si existe una función α tal que cada F a pueda ser mapeado a un G a . α puede ser de muchos a uno, pero tiene que mapear cada elemento de F a . En términos generales, una transformación natural es una función entre los funtores.

Ahora en la teoría de categorías, puede haber muchos funtores entre dos categorías. En una vista simplificada, se puede decir que ni siquiera nos importa qué mapa de los funtores desde dónde a dónde, solo nos preocupan las transformaciones naturales entre ellos.

Volviendo a la mónada, ahora podemos ver que un "monoide en la categoría de endofunctores" debe tener dos transformaciones naturales. Llamemos a nuestro endofunctor mónada M :

Una transformación natural del functor de identidad (endo) a la mónada:

η :: 1 -> M -- this is return

Y una transformación natural de la conposición de dos mónadas y produce una tercera:

μ :: M × M -> M

Como × es la composición de los funtores, podemos (en términos generales) escribir también:

μ :: m a × m a -> m a μ :: (m × m) a -> m a μ :: m (m a) -> m a -- join in Haskell

Cumpliendo estas leyes:

μ . M μ == μ . μ M μ . M η == μ . η M

Por lo tanto, una mónada es un caso especial de un monoide en la categoría de endofunctores. No se puede escribir una instancia de monoide para la mónada en Haskell normal, ya que la noción de composición de Haskell es demasiado débil (creo; esto se debe a que las funciones están restringidas a Hask y son más débiles que Cat ). Vea this para más información.

¿Qué hay de Foldable ?

Ahora en cuanto a Foldable : existen definiciones de fold s que usan una función binaria personalizada para combinar los elementos. Ahora, por supuesto, podría proporcionar cualquier función para combinar elementos, o podría usar un concepto existente de combinación de elementos, el monoide. De nuevo, tenga en cuenta que este monoide está restringido al monoide establecido, no a la definición catorial de monoide.

Dado que el mappend del monoide es asociativo, foldl y foldr producen el mismo resultado, por lo que el plegamiento de monoids puede reducirse para fold :: Monoid m, Foldable t => tm -> m . Esta es una conexión obvia entre monoide y plegable.

@danidiaz ya señaló la conexión entre Applicative , Monoid y Foldable utilizando el Const Const ab = Const a , cuya instancia aplicativa requiere que el primer parámetro de Const sea ​​un monoid (no pure sin mempty (sin mempty cuenta lo undefined )).

En mi opinión, comparar mónada y plegable es un poco exagerado, ya que la mónada es más poderosa que la plegable en el sentido de que plegable solo puede acumular los valores de una lista de acuerdo con una función de mapeo, pero el enlace de mónada puede alterar estructuralmente el contexto ( a -> mb ).


Cuando un contenedor es Foldable , existe una relación entre foldMap y Applicative (que es una superclase de Monad ).

Foldable tiene una función llamada traverse_ , con firma:

traverse_ :: Applicative f => (a -> f b) -> t a -> f ()

Un posible Applicative es Constant . Para ser un Aplicativo, se requiere que el parámetro "acumulador" sea un Monoid :

newtype Constant a b = Constant { getConstant :: a } -- no b value at the term level! Monoid a => Applicative (Constant a)

por ejemplo:

gchi> Constant (Sum 1) <*> Constant (Sum 2) :: Constant (Sum Int) whatever Constant (Sum {getSum = 3})

Podemos definir foldMap en términos de traverse_ y Constant esta manera:

foldMap'' :: (Monoid m, Foldable t) => (a -> m) -> t a -> m foldMap'' f = getConstant . traverse_ (Constant . f)

Usamos traverse_ para recorrer el contenedor, acumulando valores con Constant , y luego usamos getConstant para deshacernos del newtype.


Resumen : (>>=) y traverse parecen similares porque ambos son mapeos de flecha de functors, mientras que foldMap es (casi) un traverse especializado.

Antes de comenzar, hay un poco de terminología para explicar. Considere fmap :

fmap :: Functor f => (a -> b) -> (f a -> f b)

Un Haskell Functor es un functor de la categoría Hask (la categoría con funciones Haskell como flechas) a sí mismo. En términos de teoría de categorías, decimos que el fmap (especializado) es el mapa de flechas de este functor, ya que es la parte del functor que lleva las flechas de las flechas. (En aras de la integridad: un functor consiste en una asignación de flechas más una asignación de objetos . En este caso, los objetos son de tipo Haskell, por lo que la asignación de objetos lleva tipos a tipos, más específicamente, la asignación de objetos de un Functor es su tipo constructor.)

También desearemos tener en cuenta las leyes de categoría y función:

-- Category laws for Hask: f . id = id id . f = f h . (g . f) = (h . g) . f -- Functor laws for a Haskell Functor: fmap id = id fmap (g . f) = fmap g . fmap f

En lo que sigue, trabajaremos con categorías distintas a Hask y con functors que no son Functor s. En tales casos, reemplazaremos id y (.) Por la identidad y composición apropiadas, fmap por el mapeo de flechas apropiado y, en un caso, = por una igualdad de flechas apropiada.

(= <<)

Para comenzar con la parte más familiar de la respuesta, para una mónada m dada las funciones a a -> mb (también conocidas como flechas de Kleisli) forman una categoría (la categoría de Kleisli de m ), con el return como identidad y (<=<) como composicion Las tres leyes de categoría, en este caso, son solo las leyes de la mónada :

f <=< return = return return <=< f = f h <=< (g <=< f) = (h <=< g) <=< f

Ahora, su pregunta sobre el enlace volteado:

(=<<) :: Monad m => (a -> m b) -> (m a -> m b)

Resulta que (=<<) es el mapa de flechas de un functor de la categoría de Kleisli de m a Hask . Las leyes de functor aplicadas a (=<<) equivalen a dos de las leyes de la mónada:

return =<< x = x -- right unit (g <=< f) =<< x = g =<< (f =<< x) -- associativity

atravesar

A continuación, necesitamos un desvío a través de Traversable (al final de la respuesta se proporciona un bosquejo de una prueba de los resultados en esta sección). Primero, notamos que las funciones a a -> fb para todos los funtores aplicativos f tomados a la vez (en oposición a uno en cada momento, como cuando se especifica una categoría de Kleisli) forman una categoría, con Identity como identidad y Compose . fmap g . f Compose . fmap g . f Compose . fmap g . f como composicion Para que eso funcione, también tenemos que adoptar una igualdad de flechas más relajada, que ignora la placa de Identity y componer (que solo es necesaria porque escribo esto en pseudo-Haskell, en oposición a la notación matemática adecuada). Más precisamente, consideraremos que cualquiera de las dos funciones que pueden interconvertirse utilizando cualquier composición de los isomorfismos de Identity y Compose como flechas iguales (o, en otras palabras, no distinguiremos entre a e Identity a , ni entre f (ga) y Compose fga ).

Llamemos a esa categoría la "categoría transitable" (ya que no puedo pensar en un nombre mejor en este momento). En términos concretos de Haskell, una flecha en esta categoría es una función que agrega una capa adicional de contexto Applicative "debajo" de cualquier capa anterior existente. Ahora, considere traverse :

traverse :: (Traversable t, Applicative f) => (a -> f b) -> (t a -> f (t b))

Dada la opción de contenedor traverse , traverse es el mapeo de flecha de un functor desde la "categoría transitable" a sí mismo. Las leyes funtoras equivalen a las leyes transitables.

En resumen, tanto (=<<) como el traverse son análogos de fmap para los funtores que incluyen categorías distintas de Hask , por lo que no es sorprendente que sus tipos sean un poco similares entre sí.

foldMap

Todavía tenemos que explicar qué tiene que ver todo eso con foldMap . La respuesta es que foldMap se puede recuperar de la traverse ( consulte la respuesta de danidiaz : utiliza traverse_ , pero como el functor aplicativo es Const m el resultado es esencialmente el mismo):

-- cf. Data.Traversable foldMapDefault :: (Traversable t, Monoid m) => (a -> m) -> (t a -> m) foldMapDefault f = getConst . traverse (Const . f)

Gracias al isomorfismo const / getConst , esto es claramente equivalente a:

foldMapDefault'' :: (Traversable t, Monoid m) => (a -> Const m b) -> (t a -> Const m (t b)) foldMapDefault'' f = traverse f

El cual es simplemente traverse especializado para los funtores aplicativos Monoid m => Const m . Aunque Traversable no es Foldable y foldMapDefault no es foldMap , esto proporciona una justificación decente de por qué el tipo de foldMap parece al de traverse y, de forma transitoria, al de (=<<) .

Como observación final, tenga en cuenta que las flechas de la "categoría transitable" con función del funtor aplicativo para algunos Monoid m no forman una subcategoría, ya que no hay identidad a menos que la Identity encuentre entre las posibles opciones del functor aplicativo. Eso probablemente significa que no hay nada más interesante que decir sobre foldMap desde la perspectiva de esta respuesta. La única opción única de functor aplicativo que da una subcategoría es Identity , que no es para nada sorprendente, dado que el recorrido con Identity equivale a fmap en el contenedor.

Apéndice

Aquí hay un bosquejo aproximado de la derivación del resultado traverse , sacado de mis notas de hace varios meses con una edición mínima. ~ significa "igual a (algunos relevantes) isomorfismo".

-- Identity and composition for the "traversable category". idT = Identity g .*. f = Compose . fmap g . f -- Category laws: right identity f .*. idT ~ f f .*. idT Compose . fmap f . idT Compose . fmap f . Identity Compose . Identity . f f -- using getIdentity . getCompose -- Category laws: left identity idT .*. f ~ f idT .*. f Compose . fmap Identity . f f -- using fmap getIdentity . getCompose -- Category laws: associativity h .*. (g .*. f) ~ (h .*. g) .*. f h .*. (g .*. f) -- LHS h .*. (Compose . fmap g . f) Compose . fmap h . (Compose . fmap g . f) Compose . Compose . fmap (fmap h) . fmap g . f (h .*. g) .*. f -- RHS (Compose . fmap h . g) .*. f Compose . fmap (Compose . fmap h . g) . f Compose . fmap (Compose . fmap h) . fmap g . f Compose . fmap Compose . fmap (fmap h) . fmap g . f -- using Compose . Compose . fmap getCompose . getCompose Compose . Compose . fmap (fmap h) . fmap g . f -- RHS ~ LHS

-- Functor laws for traverse: identity traverse idT ~ idT traverse Identity ~ Identity -- i.e. the identity law of Traversable -- Functor laws for traverse: composition traverse (g .*. f) ~ traverse g .*. traverse f traverse (Compose . fmap g . f) ~ Compose . fmap (traverse g) . traverse f -- i.e. the composition law of Traversable