¿Qué mónadas se pueden expresar como Libres sobre algún funtor?

Para responder a la pregunta como se dice, la mayoría de las mónadas familiares que no mencionaste en la pregunta no son ellas mismas mónadas libres. La respuesta de Philip JF alude a cómo se puede relacionar una mónada dada con una nueva mónada libre, pero la nueva mónada será "más grande": tiene más valores distintos que la mónada original. Por ejemplo, la mónada real State s satisface get >>= put = return (), pero la mónada libre en StateF no lo hace. Como mónada libre, no satisface ecuaciones adicionales por definición; que es el muy noción de libertad.

Voy a mostrar que el Reader r, Writer w y State s mónadas no son libres excepto bajo condiciones especiales en r/w/s.

Permítanme introducir algo de terminología. Si m es una mónada entonces llamamos a cualquier valor de un tipo m a una acción (m -). Llamamos a una m-acción trivial si es igual a return x para algunos x; de lo contrario la llamamos no trivial.

Si m = Free f es cualquier mónada libre en un funtor f, entonces m admite un homomorfismo de mónada a Maybe. Esto se debe a que Free es functorial en su argumento f y Maybe = Free (Const ()) donde Const () es el objeto terminal en la categoría de funtores. Concretamente, este homomorfismo se puede escribir

toMaybe :: Free f a -> Maybe a
toMaybe (Pure a) = Just a
toMaybe (Impure _) = Nothing

Debido a que toMaybe es un homomorfismo mónada, en particular satisface toMaybe (v >> w) = toMaybe v >> toMaybe w para cualquier m-acciones v y w. Observar ahora que toMaybe envía trivial m-acciones trivial Maybe-acciones y no trivial m-acciones para el trivial Maybe-acción Nothing. Ahora Maybe tiene la propiedad que >>ing un trivial acción con cualquier acción, en cualquier orden, se obtiene un trivial de acción (Nothing >> w = v >> Nothing = Nothing); lo mismo es cierto para m, ya que toMaybe es una monada homomorphism que se conserva (no), la trivialidad.

(Si lo prefiere, también puede verificar esto directamente desde la fórmula para >> para una mónada libre.)

Para mostrar que una mónada en particular m no es isomórfica a ninguna mónada libre, entonces, basta con encontrar m-acciones v y w tales que al menos una de v y w no es trivial, pero v >> w es trivial.

Reader r satisface v >> w = w, por lo que solo necesitamos elegir w = return () y cualquier acción no trivial v, que exista siempre que r tenga al menos dos valores (entonces ask no sea constante, es decir, no trivial).

Para Writer w, supongamos que hay un elemento invertible k :: w que no sea la identidad. Sea kinv :: w su inversa. Entonces tell k >> tell kinv = return (), pero tell k y tell kinv no son triviales. Cualquier grupo no trivial (por ejemplo, enteros en adición) tiene tal elemento k. Presumo que las mónadas libres de la forma Writer w son solo aquellas para las cuales el monoide w es libre, i. e., w = [a], Writer w ~ Free ((,) a).

Para State s, similarmente si s admite cualquier automorfismo no trivial f :: s -> s con inverso finv :: s -> s, entonces modify f >> modify finv = return (). Cualquier tipo s con al menos dos elementos e igualdad decidible tiene tales automorfismos.

Escribí una prueba de que la mónada de la lista no es libre en una publicación en la lista de correo de haskell-cafe , basada en las ideas en la respuesta de Reid:{[46]]}

Recordemos que podemos construir, para cualquier funtor f, la mónada libre sobre f:{[46]]}

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

Intuitivamente, f a libre es el tipo de árboles en forma de f con hojas de tipo a. La operación join simplemente injerta árboles juntos y no realiza ninguna más cálculos. Se llamarán los valores del formulario (Roll _) "no trivial" en este publicación.

Algunas de las mónadas usuales son de hecho mónadas libres sobre algún funtor: {[46]]}

• La mónada árbol es la mónada libre sobre el funtor Pair, donde data Pair a = MkPair a a. La intuición como árboles en forma de pareja es más fuerte en este ejemplo. Cada nodo padre tiene un par de niño.

• La mónada Maybe es la mónada libre sobre el funtor Unit, donde data Unit a = MkUnit. En la imagen gráfica los nodos padre tienen un Unit de los niños, por lo que no hay niños en absoluto. Así que hay exactamente dos Unit árboles con forma: el árbol que consiste solo en una hoja (correspondiente a Just _) y los tres consisten en un nodo padre sin hijos (correspondiente a Nothing).

• La Identity mónada es la mónada libre sobre el funtor {[14]]}, donde Void a es un tipo sin constructores.

• La Partiality mónada es la mónada libre sobre Maybe.

• La Writer [r] mónada es la mónada libre sobre el funtor (r,). En un árbol con forma de (r,), un nodo padre es decorado con un valor de tipo r y tiene exactamente un nodo hijo. Atravesando tal camino produce una lista de r ' s y un valor de hoja de tipo a, por lo que en total un valor de tipo ([r],a) = Writer r a.

  (En particular, Free (r,) () es isomorfo a [r]. Esta observación llevó a la afirmación de que la lista mónada es libre. Pero esta afirmación es falsa y de hecho no se desprende de la observación. Para mostrar que una mónada m es libre, uno tiene que exhibir un isomorfismo mónada forall a. m a -> Free f a para algún funtor f. En contraste, exhibiendo un isomorfismo de m a con Free (f a) () no es suficiente ni necesario.)

Aún más mónadas son cocientes de mónadas libres. Por ejemplo, State s es un cociente de Free (StateF s), donde

data StateF s a = Put s a | Get (s -> a).
-- NB: This functor is itself a free functor over a type constructor
-- which is sometimes called StateI [1], rendering Free (StateF s) what
-- Oleg and Hiromi Ishii call a "freer monad" [2].

El cociente se exhibe por el siguiente morfismo mónada, que da semántica a los valores puramente sintácticos de la mónada libre.

run :: Free (StateF s) a -> State s a
run (Pure x)         = return x
run (Roll (Put s m)) = put s >> run m
run (Roll (Get k))   = get >>= run . k

This point of view is the basis of the operational package by apfelmus [1] y también se habla en un Hilo StackOverflow [3]. Es la principal razón por la que las mónadas libres son útiles en un contexto de programación.

Entonces, ¿es la mónada lista una mónada libre? Intuitivamente, no lo es, porque el la operación de unión de la mónada de lista (concatenación) no se limita a injertar expresiones juntas, pero las aplana [4].

Aquí hay una prueba de que la mónada de la lista no es libre. Lo estoy grabando desde He estado interesado en una prueba durante bastante tiempo, pero buscando no dio ningún resultado. Hilo [3] y [5] estuvo cerca, sin embargo.

En la mónada libre sobre cualquier funtor, el resultado de la unión de un la acción con cualquier función es siempre no trivial, es decir,

(Roll _ >>= _) = Roll _

Esto se puede comprobar directamente desde la definición de (>>=) para el libre mónada o alternativamente con el truco de Reid Barton de explotar una mónada morfismo a Tal vez, ver [3].

Si la mónada de la lista era isomorfa-como-una-mónada a la mónada libre sobre algunos funtor, el isomorfismo mapearía solo singleton listas [x] a valores de la forma (Pure _) y todas las demás listas a valores no triviales. Esto es debido a que los isomorfismos mónadas tienen que conmutar con" retorno " y return x está [x] en la mónada de la lista y Pure x en la mónada libre.

Estos dos hechos se contradicen entre sí, como se puede ver con lo siguiente ejemplo:

do
    b <- [False,True]  -- not of the form (return _)
    if b
        then return 47
        else []
-- The result is the singleton list [47], so of the form (return _).

Después de aplicar un isomorfismo hipotético a la mónada libre sobre algunos funtor, tendríamos que la unión de un valor no trivial (la imagen de [False,True] en el isomorfismo) con alguna función resulta en un valor trivial (la imagen de [47], es decir, return 47).

Saludos, Ingo

[1] http://projects.haskell.org/operational/Documentation.html

[2] http://okmij.org/ftp/Haskell/extensible/more.pdf

[3] ¿Qué mónadas se pueden expresar como Libres sobre algún funtor?

[4] https://hackage.haskell.org/package/free-4.12.4/docs/Control-Monad-Free.html

[5] https://www.reddit.com/r/haskell/comments/50zvyb/why_is_liststate_not_a_free_monad /

Todas las mónadas pueden ser expresadas como la Mónada Libre. Sus propiedades adicionales (como MonadFix y Cont) podrían eliminarse de esa manera porque la Mónada Libre no es una MonadFix Libre o Cont Libre.

La forma general es definir el fmap del Funtor en términos de liftM y luego envolver libremente alrededor de ese Funtor. La Mónada resultante se puede reducir a la Mónada anterior/real especificando cómo las funciones return y join (Puras e Impuras) tienen que ser mapeadas a la Mónada real.