haskell - leibniz - Visualizando la Mónada Libre

monadas filosofía

Question

Creo que tengo una idea aproximada de lo que es la mónada gratuita, pero me gustaría tener una mejor manera de visualizarla.

Es lógico que los magmas libres sean solo árboles binarios porque es tan "general" como puede ser sin perder ninguna información.

De manera similar, tiene sentido que los monoides libres son solo listas, porque el orden de las operaciones no importa. Ahora hay una redundancia en el "árbol binario", por lo que puede aplanarlo, si tiene sentido.

Tiene sentido que los grupos libres se vean como fractales, por una razón similar: https://en.wikipedia.org/wiki/Cayley_graph#/media/File:Cayley_graph_of_F2.svg y para obtener otros grupos, solo identificamos diferentes elementos Del grupo como siendo "el mismo" y obtenemos otros grupos.

¿Cómo debo estar visualizando la mónada libre? En este momento, solo lo veo como el árbol de sintaxis abstracta más general que puedas imaginar. ¿Es eso esencialmente? ¿O estoy simplificándolo demasiado?

Además, de manera similar, ¿qué perdemos al pasar de una mónada libre a una lista u otras mónadas? ¿Qué nos estamos identificando para ser el "mismo"?

Agradezco todos los comentarios que arrojan luz sobre esto. ¡Gracias!

Answer 1

En este momento, solo pienso en [la mónada libre] como el árbol de sintaxis abstracta más general que puedas imaginar. ¿Es eso esencialmente? ¿O estoy simplificándolo demasiado?

Lo estás simplificando demasiado

1. "Mónada libre" es la abreviatura de "la mónada libre sobre un funtor específico " o el tipo de datos Free fa , que en realidad es una mónada libre diferente para cada elección de f .
2. No hay una estructura general que tengan todas las mónadas libres. Su estructura se descompone en:
   • Lo que aporta el propio Free
   • ¿Qué aportan las diferentes opciones para f

Pero vamos a tomar un enfoque diferente. Aprendí mónadas libres estudiando primero la mónada operacional estrechamente relacionada, que tiene una estructura más uniforme y más fácil de visualizar. Te recomiendo que estudies eso desde el enlace mismo.

La forma más sencilla de definir la mónada operativa es la siguiente:

{-# LANGUAGE GADTs #-}
data Program instr a where
Return :: a -> Program instr a
Bind :: instr x -- an "instruction" with result type `x`
-> (x -> Program instr a) -- function that computes rest of program
-> Program instr a -- a program with result type `a`

... donde el parámetro de tipo instr representa el tipo de "instrucción" de la mónada, generalmente un GADT. Por ejemplo (tomado del enlace):

data StackInstruction a where
Pop :: StackInstruction Int
Push :: Int -> StackInstruction ()

Así que un Program en la mónada operacional, informalmente, lo visualizaría como una "lista dinámica" de instrucciones, donde el resultado producido por la ejecución de cualquier instrucción se usa como entrada a la función que decide cuál es la "cola" de la "lista de instrucciones" es. El constructor Bind empareja una instrucción con una función de "selector de cola".

Muchas mónadas libres también se pueden visualizar en términos similares: puede decir que el functor elegido para una mónada libre sirve como su "conjunto de instrucciones". Pero con las mónadas libres las "colas" o "hijos" de la "instrucción" son manejadas por el propio Functor . Así que un ejemplo simple (tomado de la popular entrada de blog de Gabriel González sobre el tema ):

data Free f r = Free (f (Free f r)) | Pure r
-- The `next` parameter represents the "tails" of the computation.
data Toy b next =
Output b next
| Bell next
| Done
instance Functor (Toy b) where
fmap f (Output b next) = Output b (f next)
fmap f (Bell next) = Bell (f next)
fmap _ Done = Done

Mientras que en la mónada operacional, la función utilizada para generar la "cola" pertenece al tipo de Program (en el constructor de Bind ), en las mónadas libres las colas pertenecen a la "instrucción" / tipo de Functor . Esto permite que las "instrucciones" de la mónada libre (una analogía que ahora se está rompiendo) tengan una sola "cola" (como Output o Bell ), cero colas (como Done ) o múltiples colas si así lo eliges. O, en otro patrón común, el next parámetro puede ser el tipo de resultado de una función incrustada:

data Terminal a next =
PutStrLn String next
| GetLine (String -> next) -- can''t access the next "instruction" unless
-- you supply a `String`.
instance Functor Terminal where
fmap f (PutStrLn str next) = PutStrLn str (f next)
fmap f (GetLine g) = GetLine (fmap f g)

Esto, por cierto, es una objeción que he tenido durante mucho tiempo para las personas que se refieren a las mónadas libres u operativas como "árboles de sintaxis"; su uso práctico requiere que los "hijos" de un nodo estén ocultos dentro de una función. ¡Generalmente no puedes inspeccionar completamente este "árbol"!

Entonces, realmente, cuando llegas a eso, la forma de visualizar una mónada libre se reduce completamente a la estructura del Functor que utilizas para parametrizarla. Algunas parecen listas, otras parecen árboles y otras parecen "árboles opacos" con funciones como nodos. (Una vez alguien respondió a mi objeción con una línea como "una función es un nodo de árbol con tantos hijos como posibles argumentos").

Answer 2

Puede que hayas escuchado

Monad es un monoide en una categoría de endofunctores

Y ya mencionaste que los monoides son solo listas. Así que ahí estás.

Ampliando un poco en eso:

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

No es una lista normal de a , sino una lista en la que la cola está dentro de f . Lo verá si escribe una estructura de valor de varios enlaces anidados:

pure x >>= f >>= g >>= h :: Free m a

podría resultar en

Free $ m1 $ Free $ m2 $ Free $ m3 $ Pure x
where m1, m2, m3 :: a -> m a -- Some underlying functor "constructors"

Si m en el ejemplo anterior es tipo de suma:

data Sum a = Inl a | Inr a
deriving Functor

Entonces la lista es en realidad un árbol, ya que en cada constructor podemos bifurcar hacia la izquierda o hacia la derecha.

Puede que hayas oído eso

El aplicativo es un monoide en una categoría de endofunctores

... la categoría es diferente Hay agradables visualizaciones de diferentes codificaciones aplicativas gratuitas en la publicación del blog de Roman Cheplyaka .

Applicative tan libre es también una lista. Me lo imagino como una lista heterogénea de valores de fa , y función única:

 x :: FreeA f a
x = FreeA g [ s, t, u, v]
where g :: b -> c -> d -> e -> a
s :: f b
t :: f c
u :: f d
v :: f e

En este caso, la cola en sí no está envuelta en f , sino en cada elemento por separado. Esto podría o no ayudar a entender la diferencia entre Applicative y Monad .

Tenga en cuenta que f no necesita ser Functor para hacer Applicative (FreeA fa) , en oposición a la mónada Free arriba.

También hay funcional gratis.

data Coyoneda f a = Coyoneda :: (b -> a) -> f b -> Coyoneda f a 

lo que hace que cualquier * -> * tipo Functor . Compáralo con el Applicative gratis arriba. En el caso de aplicación, tuvimos una lista heterogénea de longitud n de valores de fa y una función n-aria que los combina. Coyoneda es el caso especial 1-ary de arriba.

Podemos combinar Coyoneda y Free para hacer una mónada Operational free. Y como lo menciona otra respuesta, ese es difícilmente imaginable como un árbol, ya que hay funciones involucradas. OTOH, puedes imaginar esas continuaciones como flechas mágicas diferentes en tu foto :)