haskell - ¿Qué mónadas se pueden expresar como gratuitas sobre algún functor?

monads free-monad

Question

La documentación Free dice:

Varias mónadas comunes surgen como mónadas libres,

• Dados los data Empty a , Free Empty es isomorfo a la mónada de Identity .
• Free Maybe se puede usar para modelar una mónada de parcialidad donde cada capa representa ejecutar el cálculo por un tiempo más prolongado.

¿Qué otras mónadas se pueden usar con Free ?

Solo podría pensar en uno más: creo que Free (Const e) es isomorfo para Either e .

Editar: ¿Qué mónadas no se pueden expresar con Free y por qué?

Answer 1

Casi todos ellos (hasta problemas relacionados con bucle y mfix ) pero no Cont .

Considera la mónada del State

newtype State s a = State (s -> (a,s))

no se parece en nada a una mónada gratuita ... pero piensa en el State en términos de cómo lo usas

get :: m s --or equivalently (s -> m a) -> m a
set :: s -> m () --or (s,m a) -> m a
runState :: m a -> s -> (a,s)

podemos diseñar una mónada gratuita con esta interfaz enumerando las operaciones como constructores

data StateF s a
  = Get (s -> a) | Set s a deriving Functor

entonces nosotros tenemos

type State s a = Free (StateF s) a

con

get = Impure (Get Pure)
set x = Impure (Set x (Pure ())

y solo necesitamos una forma de usarlo

runState (Pure a) s = (a,s)
runState (Impure (Get f)) s = runState (f s) s
runState (Impure (Set s next)) _ = runState next s

puedes hacer esta construcción con la mayoría de las mónadas. Al igual que la mónada tal vez / parcialidad se define por

stop :: m a
maybe :: b -> (a -> b) -> m a -> b

la regla es que tratamos cada una de las funciones que terminan en mx para alguna x como un constructor en el funtor, y las otras funciones son formas de ejecutar la mónada libre resultante. En este caso

data StopF a = StopF deriving Functor

maybe _ f (Pure a)      = f a
maybe b _ (Impure Stop) = b

¿Por qué es genial? Bueno algunas cosas

1. La mónada gratuita le proporciona un dato que puede pensar que es un AST para el código monádico. Puede escribir funciones que operan con estos datos que son realmente útiles para DSL
2. Funcionarios componen, lo que significa romper sus mónadas como esto los hace semi composeables. En particular, dados dos funtores que comparten un álgebra (un álgebra es esencialmente solo una función fa -> a para algunos a cuando f es un funtor), la composición también tiene ese álgebra.

La composición de Functor es justa Podemos combinar funtores de varias maneras, la mayoría de las cuales conservan ese álgebra. En este caso, no queremos la composición de los funtores (f (g (x))) sino el coproducto del functor . Functors agregan

data f :+: g a = Inl (f a) | Inr (g a) 

instance (Functor f, Functor g) => Functor (f :+: g) where
  fmap f (Inl x) = Inl (fmap f x)
  fmap f (Inr x) = Inr (fmap f x)

compAlg :: (f a -> a) -> (g a -> a) -> f :+: g a -> a
compAlg f _ (Inl x) = f x
compAlf _ g (Inr x) = g x

también las mónadas libres conservan álgebras

freeAlg :: (f a -> a) -> Free f a -> a
freeAlg _ (Pure a) = a
freeAlg f (Impure x) = f $ fmap (freeAlg f) x

En el famoso documento de Wouter Swierstra, Tipos de datos a la carta, esto se usa con gran efecto. Un simple ejemplo de ese papel es la calculadora. Lo cual tomaremos una perspectiva monádica sobre lo nuevo en esta publicación. Dado el álgebra

class Calculator f where
 eval :: f Integer -> Integer

podemos pensar en varias instancias

data Mult a = Mult a a deriving Functor
instance Calculator Mult where
  eval (Mult a b) = a*b

data Add a = Add a a deriving Functor
instance Calculator Add where
  eval (Add a b) = a+b

data Neg a = Neg a deriving Functor
instance Calculator Neg where
  eval (Neg a) = negate a

instance Calculator (Const Integer) where
  eval (Const a) = a

data Signum a = Signum a deriving Functor
instance Calculator Signum where
  eval (Signum a) = signum a

data Abs a = Abs a deriving Functor
instance Calculator Abs where
  eval (Abs a) = abs a

y lo mas importante

instance (Calculator f, Calculator g) => Calculator (f :+: g) where
   eval = compAlg eval

puedes definir la mónada numérica

newtype Numerical a = Numerical (
        Free (Mult 
        :+: Add 
        :+: Neg 
        :+: Const Integer 
        :+: Signum
        :+: Abs) a deriving (Functor, Monad)

y luego puedes definir

 instance Num (Numerical a)

que podría ser totalmente inútil, pero me parece muy genial. Te deja definir otras cosas como

 class Pretty f where
    pretty :: f String -> String

 instance Pretty Mult where
    pretty (Mult a b) = a ++ "*" ++ b

y similar para todos los demás.

Es una estrategia de diseño útil: enumere las cosas que quiere que su mónada haga ==> defina funtores para cada operación ==> descubra cuáles deben ser algunas de sus álgebras ==> defina esos funtores para cada operación ==> hágala rápido.

Hacerlo rápido es difícil, pero tenemos algunos trucos. El truco 1 es simplemente envolver su mónada gratuita en Codensity (el botón "ir más rápido"), pero cuando eso no funciona, quiere deshacerse de la representación libre. Recuerda cuando tuvimos

runState (Pure a) s = (a,s)
runState (Impure (Get f)) s = runState (f s) s
runState (Impure (Set s next)) _ = runState next s

bueno, esta es una función de Free StateF a a s -> (a,s) simplemente usando el tipo de resultado, ya que nuestra definición de estado parece razonable ... ¿pero cómo definimos las operaciones? En este caso, usted conoce la respuesta, pero una forma de derivarla sería pensar en términos de lo que Conal Elliott denomina morfismos de clase de tipo. Usted quiere

runState (return a) = return a
runState (x >>= f) = (runState x) >>= (runState f)
runState (set x) = set x
runState get = get

lo que lo hace bastante fácil

runState (return a) = (Pure a) = /s -> (a,s)

runState (set x) 
   = runState (Impure (Set x (Pure ()))) 
   = /_ -> runState (Pure ()) x
   = /_ -> (/s -> (a,s)) x
   = /_ -> (a,x)

runState get
  = runState (Impure (Get Pure))
  = /s -> runState (Pure s) s
  = /s -> (s,s)

que es bastante útil. Derivar >>= de esta manera puede ser difícil, y no lo incluiré aquí, pero los otros son exactamente las definiciones que esperarías.

Answer 2

Escribí una prueba de que la lista de mónadas no es gratuita en una publicación en la lista de correo de haskell-cafe , en base a las ideas en la respuesta de Reid:

Recordemos que podemos construir, para cualquier functor f, la mónada libre sobre f:

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

Intuitivamente, Free fa es el tipo de árboles en forma de f con hojas del tipo a. La operación de unión simplemente injerta árboles juntos y no realiza ningún cálculo adicional. Los valores del formulario (Rollo _) se denominarán "no triviales" en esta publicación.

Algunas de las mónadas habituales son, de hecho, mónadas libres sobre algún functor:

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

• La Mónada Maybe es la mónada libre sobre la Unit , donde data Unit a = MkUnit . En la imagen gráfica, los nodos principales tienen una Unit de elementos secundarios, por lo que no hay hijos en absoluto. Entonces, hay exactamente dos árboles en forma de Unit : el árbol que consiste únicamente en una hoja (que corresponde a Just _ ) y los tres que consisten en un nodo padre sin hijos (que corresponde a Nothing ).

• La mónada Identity es la mónada gratuita sobre el functor Void , donde Void a es un tipo sin constructores.

• La mónada de Partiality es la mónada gratuita sobre Maybe .

• La mónada Writer [r] es la mónada libre sobre el functor (r,) . En un árbol en forma de (r,) , un nodo padre está decorado con un valor de tipo r y tiene exactamente un nodo secundario. Atravesar tal camino produce una lista de r y un valor de hoja de tipo a , de modo que en total un valor de tipo ([r],a) = Writer ra .

  (En particular, Free (r,) () es isomorfo a [r] . Esta observación llevó a la afirmación de que la lista de la mónada es libre. Pero esta afirmación es falsa y de hecho no se sigue de la observación. la mónada m es gratuita, uno tiene que exhibir un isomorfismo de mónada para todos forall a. ma -> Free fa para algunos funtores f . Por el contrario, exhibir un isomorfismo de ma con Free (fa) () no es suficiente ni requerido).

Incluso 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 de 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

Este punto de vista es la base del paquete operacional por apfelmus [1] y también se habla en un hilo de [3]. Es la razón principal por la cual las mónadas libres son útiles en un contexto de programación.

Entonces, ¿la lista de mónadas es una mónada libre? Intuitivamente, no lo es, porque la operación de combinación de la mónada de lista (concatenación) no solo injerta expresiones juntas, sino que las aplana [4].

Aquí hay una prueba de que la lista de mónadas no es gratuita. Lo estoy grabando ya que he estado interesado en una prueba durante bastante tiempo, pero la búsqueda no produjo ningún resultado. Sin embargo, los hilos [3] y [5] se acercaron.

En la mónada libre sobre cualquier functor, el resultado de vincular una acción no trivial con cualquier función es siempre no trivial, es decir,

(Roll _ >>= _) = Roll _

Esto se puede verificar directamente desde la definición de (>>=) para la mónada libre o alternativamente con el truco de Reid Barton de explotar un morfismo de mónada en Maybe, ver [3].

Si la lista de la mónada fuera isomorfa-como-una mónada para la mónada libre sobre algún functor, el isomorfismo mapearía solo listas singleton [x] a valores de la forma (Pure _) y todas las otras listas a valores no triviales. Esto se debe a que los isomorfismos de la mónada tienen que conmutar con "retorno" y return x es [x] en la lista de la mónada y Pure x en la mónada libre.

Estos dos hechos se contradicen entre sí, como se puede ver con el 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 algún functor, tendríamos que la unión de un valor no trivial (la imagen de [False,True] bajo el isomorfismo) con alguna función da como resultado 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 gratuitas sobre algún functor?

[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/

Answer 3

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

Mostraré que Reader r , Writer w y State s mónadas no son gratuitas, excepto bajo condiciones especiales en r / w / s .

Déjame introducir algo de terminología. Si m es una mónada, llamamos a cualquier valor de una acción tipo ma an ( m -). Llamamos a una m acción trivial si es igual a return x para alguna x ; de lo contrario, lo llamamos no trivial.

Si m = Free f es cualquier mónada libre en un funtor f , entonces m admite un homomorfismo de mónada en Maybe . Esto se debe a que Free es funcional 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 de mónada, en particular cumple con toMaybe (v >> w) = toMaybe v >> toMaybe w para cualquier m acciones v y w . Ahora observe que para toMaybe envía m acciones triviales a "trivial" Maybe acciones y m accciones no triviales a la no trivial " Maybe -acción Nothing . Ahora Maybe tiene la propiedad de que >> una acción no trivial con cualquier acción, en cualquier orden, produce una acción no trivial ( Nothing >> w = v >> Nothing = Nothing ); así que lo mismo es cierto para m , ya que para toMaybe es un homomorfismo de mónada que preserva la (no) trivialidad.

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

Para mostrar que una mónada particular m no es isomorfa a ninguna mónada libre, entonces, es suficiente encontrar m -acciones v y w tales que al menos uno de v y w no sea trivial, pero v >> w es trivial.

Reader r satisface v >> w = w , por lo que solo debe seleccionar w = return () y cualquier acción no trivial v , que existe siempre que r tenga al menos dos valores (luego ask es no constante, es decir, no trivial).

Para Writer w , supongamos que hay un elemento invertible k :: w no sea la identidad. Deje kinv :: w ser su inversa. Luego tell k >> tell kinv = return () , pero tell k y tell kinv no son triviales. Cualquier grupo no trivial (por ejemplo, enteros bajo adición) tiene dicho elemento k . Supongo que las mónadas libres de la forma Writer w son solo aquellas para las que el monoid w es en sí libre, es decir, w = [a] , Writer w ~ Free ((,) a) .

Para State s , de forma similar si s admite cualquier automorfismo no trivial f :: s -> s con finv :: s -> s inversos finv :: s -> s , entonces modify f >> modify finv = return () . Cualquier tipo s con al menos dos elementos y la igualdad decidable tiene tales automorfismos.

Answer 4

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

La forma general es definir fmap de Functor en términos de liftM y luego envolver Free alrededor de ese Functor. La mónada resultante se puede reducir a la mónada anterior / real especificando cómo deben return join las funciones y join (Pure e Impure) a la Mónada real.