haskell - leibniz - ¿Qué son las mónadas libres?

monadas filosofia

Question

He visto el término Free Monad aparecer de every then durante algún tiempo, pero todo el mundo parece usarlos / discutirlos sin dar una explicación de lo que son. Entonces, ¿qué son las mónadas libres? (Diría que estoy familiarizado con las mónadas y los conceptos básicos de Haskell, pero que tengo un conocimiento muy aproximado de la teoría de categorías).

Answer 1

Aquí hay una respuesta aún más simple: una mónada es algo que "computa" cuando el contexto monádico se contrae con join :: m (ma) -> ma (recordando que >>= se puede definir como (join .) . flip fmap ). Así es como las Mónadas llevan el contexto a través de una cadena secuencial de cálculos: porque en cada punto de la serie, el contexto de la llamada anterior se contrae con el siguiente.

Una mónada libre satisface todas las leyes de la mónada, pero no hace ningún colapso (es decir, cálculo). Simplemente construye una serie de contextos anidados. El usuario que crea un valor monádico libre de este tipo es responsable de hacer algo con esos contextos anidados, de modo que el significado de dicha composición pueda diferirse hasta después de que se haya creado el valor monádico.

Answer 2

Creo que un simple ejemplo concreto ayudará. Supongamos que tenemos un funtor

data F a = One a | Two a a | Two'' a a | Three Int a a a

Con el obvio fmap . Entonces Free F a es el tipo de árboles cuyas hojas tienen tipo a y cuyos nodos están etiquetados con One , Two , Two'' y Three . One nodos tienen un hijo, Two'' nodos dos y dos tienen dos hijos y los nodos tres tienen tres y también están marcados con un Int .

Free F es una mónada. return mapas x al árbol que es solo una hoja con valor x . t >>= f mira cada una de las hojas y las reemplaza con árboles. Cuando la hoja tiene valor y reemplaza esa hoja con el árbol fy .

Un diagrama lo hace más claro, ¡pero no tengo las facilidades para dibujar uno fácilmente!

Answer 3

La mónada libre (estructura de datos) corresponde a la mónada (clase), como la Lista (estructura de datos) a Monoides (clase): es la implementación trivial, donde puede decidir cómo se combinará el contenido.

Probablemente sepa qué es una mónada y que cada mónada necesita una implementación específica (que cumpla con la ley de la mónada) de fmap + join + return o bind + return .

Supongamos que tiene un Functor (una implementación de fmap ) pero el resto depende de los valores y las opciones realizadas en el tiempo de ejecución, lo que significa que desea poder usar las propiedades de la mónada pero luego desea elegir las funciones de la mónada.

Esto se puede hacer usando la mónada libre (estructura de datos), que envuelve el Functor (tipo) de tal manera que la join sea ​​más un apilamiento de esos functores que una reducción.

La return real y la join que desea utilizar, ahora se pueden dar como parámetros a la función de reducción foldFree :

foldFree :: Functor f => (a -> b) -> (f b -> b) -> Free f a -> b
foldFree return join :: Monad m => Free m a -> m a

Para explicar los tipos, podemos reemplazar el Functor f con Monad m y b con (ma) :

foldFree :: Monad m => (a -> (m a)) -> (m (m a) -> (m a)) -> Free m a -> (m a)

Answer 4

La respuesta de Edward Kmett es obviamente genial. Pero, es un poco técnico. Aquí hay una explicación quizás más accesible.

Las mónadas libres son solo una forma general de convertir los funtores en mónadas. Es decir, dado cualquier functor f Free f es una mónada. Esto no sería muy útil, excepto que obtienes un par de funciones

liftFree :: Functor f => f a -> Free f a
foldFree :: Functor f => (f r -> r) -> Free f r -> r

El primero de estos te permite "entrar" en tu mónada, y el segundo te da una manera de "salir" de él.

Más generalmente, si X es una Y con algunas cosas extra P, entonces una "X libre" es una forma de ir de una Y a una X sin ganar nada extra.

Ejemplos: un monoide (X) es un conjunto (Y) con estructura extra (P) que básicamente dice que tiene operaciones (se puede pensar en la adición) y cierta identidad (como cero).

asi que

class Monoid m where
mempty :: m
mappend :: m -> m -> m

ahora todos sabemos listas

data [a] = [] | a : [a]

bueno, dado cualquier tipo de t , sabemos que [t] es un monoide

instance Monoid [t] where
mempty = []
mappend = (++)

y así las listas son el "monoide libre" sobre conjuntos (o en tipos de Haskell).

De acuerdo, las mónadas libres son la misma idea. Tomamos un funtor, y devolvemos una mónada. De hecho, dado que las mónadas se pueden ver como monoides en la categoría de functores endo, la definición de una lista

data [a] = [] | a : [a]

se parece mucho a la definición de mónadas libres

data Free f a = Pure a | Roll (f (Free f a))

y la instancia de Monad tiene una similitud con la instancia de Monoid para listas

--it needs to be a functor
instance Functor f => Functor (Free f) where
fmap f (Pure a) = Pure (f a)
fmap f (Roll x) = Roll (fmap (fmap f) x)
--this is the same thing as (++) basically
concatFree :: Functor f => Free f (Free f a) -> Free f a
concatFree (Pure x) = x
concatFree (Roll y) = Roll (fmap concatFree y)
instance Functor f => Monad (Free f) where
return = Pure -- just like []
x >>= f = concatFree (fmap f x) --this is the standard concatMap definition of bind

Ahora, tenemos nuestras dos operaciones.

-- this is essentially the same as /x -> [x]
liftFree :: Functor f => f a -> Free f a
liftFree x = Roll (fmap Pure x)
-- this is essentially the same as folding a list
foldFree :: Functor f => (f r -> r) -> Free f r -> r
foldFree _ (Pure a) = a
foldFree f (Roll x) = f (fmap (foldFree f) x)

Answer 5

Un foo gratuito es la cosa más simple que satisface todas las leyes de "foo". Es decir, satisface exactamente las leyes necesarias para ser un foo y nada más.

Un funtor olvidadizo es uno que "olvida" parte de la estructura a medida que va de una categoría a otra.

Dados los funtores F : D -> C , y G : C -> D , decimos F -| G F -| G , F está junto a G , o G está junto a F siempre que para a, b: F a -> b es isomorfo para a -> G b , donde las flechas provienen de las categorías correspondientes.

Formalmente, un funtor libre se deja adjunto a un funtor olvidadizo.

El Monoide Gratis

Comencemos con un ejemplo más simple, el monoide libre.

Tome un monoide, que está definido por algún conjunto de portadores T , una función binaria para combinar un par de elementos f :: T → T → T , y una unit :: T , de manera que tenga una ley asociativa y una identidad. ley: f(unit,x) = x = f(x,unit) .

Puedes hacer un functor U de la categoría de monoides (donde las flechas son homomorfismos de monoides, es decir, aseguran que mapean unit a unit en el otro monoide y que puedes componer antes o después del mapeo al otro monoide sin cambiar el significado) a la categoría de conjuntos (donde las flechas son solo flechas de función) que se "olvida" de la operación y la unit , y solo le da el conjunto de transportistas.

Luego, puede definir un functor F desde la categoría de conjuntos a la categoría de monoides que se deja junto a este functor. Ese functor es el functor que asigna un conjunto a al monoide [a] , donde unit = [] , y mappend = (++) .

Así que para revisar nuestro ejemplo hasta ahora, en pseudo-Haskell:

U : Mon → Set -- is our forgetful functor
U (a,mappend,mempty) = a
F : Set → Mon -- is our free functor
F a = ([a],(++),[])

Luego, para mostrar que F es libre, es necesario demostrar que está junto a U , un funtor olvidadizo, es decir, como hemos mencionado anteriormente, debemos mostrar que

F a → b es isomorfo a a → U b

ahora, recuerde que el objetivo de F está en la categoría Mon de monoides, donde las flechas son homomorfismos de monoides, por lo que necesitamos a para mostrar que un homomorfismo de monoides de [a] → b se puede describir con precisión mediante una función de a → b .

En Haskell, llamamos al lado de esto que vive en Set (er, Hask , la categoría de los tipos de Haskell que pretendemos que es Set), simplemente foldMap , que cuando se especializa desde Data.Foldable to Lists tiene el tipo Monoid m => (a → m) → [a] → m .

Hay consecuencias que se derivan de este ser un complemento. Cabe destacar que si olvida, aumente con gratis, luego vuelva a olvidar, es como si se hubiera olvidado una vez, y podemos usar esto para construir la unión monádica. Desde UFUF ~ U(FUF) ~ UF , y podemos pasar la identidad del homomorfismo monoide de [a] a [a] través del isomorfismo que define nuestra adjunción, obtenga un isomorfismo de la lista de [a] → [a] es un función de tipo a -> [a] , y esto es solo un retorno para las listas.

Puede componer todo esto más directamente describiendo una lista en estos términos con:

newtype List a = List (forall b. Monoid b => (a -> b) -> b)

La Mónada Libre

Entonces, ¿qué es una mónada libre ?

Bueno, hacemos lo mismo que hicimos antes, comenzamos con un funtor olvidadizo U de la categoría de mónadas donde las flechas son homomorfismos de mónada a una categoría de endofunctores donde las flechas son transformaciones naturales, y buscamos un funtor que quede adjunto. a ese.

Entonces, ¿cómo se relaciona esto con la noción de una mónada libre como se usa generalmente?

Sabiendo que algo es una mónada libre, Free f , te dice que dar un homomorfismo de mónada de Free f -> m , es lo mismo (isomorfo a) que dar una transformación natural (un homomorfismo de funtor) de f -> m . Recuerde que F a -> b debe ser isomorfo a a -> U b para que F se deje junto a U. U aquí asignó las mónadas a los funtores.

F es al menos isomorfo al tipo Free que uso en mi paquete free en hackage.

También podríamos construirlo en una analogía más estricta con el código anterior para la lista libre, definiendo

class Algebra f x where
phi :: f x -> x
newtype Free f a = Free (forall x. Algebra f x => (a -> x) -> x)

Cofree Comonads

Podemos construir algo similar, mirando el adjunto correcto a un funtor olvidadizo asumiendo que existe. Un funtor de cofree es simplemente / derecho adjunto a un funtor olvidadizo, y por simetría, saber que algo es un comonad de cofree es lo mismo que saber que dar un homomorfismo de comonad de w -> Cofree f es lo mismo que dar una transformación natural de w -> f .

Answer 6

Una mónada libre de Haskell es una lista de funtores. Comparar:

data List a = Nil | Cons a (List a )
data Free f r = Pure r | Free (f (Free f r))

Pure es análogo a Nil y Free es análogo a Cons . Una mónada libre almacena una lista de functores en lugar de una lista de valores. Técnicamente, podría implementar mónadas gratuitas utilizando un tipo de datos diferente, pero cualquier implementación debe ser isomorfa a la anterior.

Utiliza mónadas gratuitas siempre que necesites un árbol de sintaxis abstracta. El funtor base de la mónada libre es la forma de cada paso del árbol de sintaxis.

haskellforall.com/2012/06/… , que alguien ya ha vinculado, da varios ejemplos de cómo construir árboles de sintaxis abstractos con mónadas gratuitas