haskell - ¿Es posible implementar MonadFix para `Free`?

free-monad

Question

http://hackage.haskell.org/package/free en Control.Monad.Free.Free permite a uno acceder a la "mónada gratuita" para cualquier Functor dado. Sin embargo, no tiene una instancia de MonadFix . ¿Esto se debe a que tal instancia no se puede escribir o simplemente se dejó de lado?

Si tal instancia no se puede escribir, ¿por qué no?

Answer 1

Bueno, inspirado por la instancia de MonadFix para Maybe , probé esta (usando las siguientes definiciones de Free ):

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

instance (Functor f) => Monad (Free f) where
    return = Pure
    Pure x >>= f = f x
    Impure x >>= f = Impure (fmap (>>= f) x)

instance (Functor f) => MonadFix (Free f) where
    mfix f = let Pure x = f x in Pure x

Las leyes son:

• Pureza: mfix (return . h) = return (fix h)
• mfix (/x -> a >>= /y -> fxy) = a >>= /y -> mfix (/x -> fxy) izquierda: mfix (/x -> a >>= /y -> fxy) = a >>= /y -> mfix (/x -> fxy)
• Deslizante: mfix (liftM h . f) = liftM h (mfix (f . h)) , para h estricto
• Anidamiento: mfix (/x -> mfix (fx)) = mfix (/x -> fxx)

La pureza es fácil de probar, pero me encontré con un problema al intentar demostrar que se está reduciendo:

mfix (/x -> a >>= /y -> f x y)
= let Pure x = (/x -> a >>= /y -> f x y) x in Pure x
= let Pure x = a >>= /y -> f x y in Pure x
-- case a = Pure z
  = let Pure x = Pure z >>= /y -> f x y in Pure x
  = let Pure x = f x z in Pure x
  = let Pure x = (/x -> f x z) x in Pure x
  = mfix (/x -> f x z)
  = Pure z >>= /y -> mfix (/x -> f x y)
-- case a = Impure t
  = let Pure x = Impure t >>= /y -> f x y in Pure x
  = let Pure x = Impure (fmap (>>= /y -> f x y) t) in Pure x
  = Pure _|_

pero

  Impure t >>= /y -> mfix (/x -> f x y)
  = Impure (fmap (>>= /y -> mfix (/x -> f x y)) t)
  /= Pure _|_

Entonces, al menos, si los constructores Pure e Impure son distinguibles, entonces mi implementación de mfix no cumple con las leyes. No puedo pensar en ninguna otra implementación, pero eso no significa que no exista. Lo siento, no pude seguir iluminando.

Answer 2

Considere la descripción de lo que hace mfix :

El punto fijo de un cómputo monádico. mfix f ejecuta la acción f solo una vez, con la salida final realimentada como entrada.

La palabra "ejecuta", en el contexto de Free , significa crear capas del Functor . Por lo tanto, "solo una vez" significa que en el resultado de evaluar mfix f , los valores mantenidos en los constructores Pure deben determinar completamente cuántas capas del functor se crean.

Ahora, digamos que tenemos una función específica una once que sabemos que siempre solo crearemos un único constructor Free , además de que se necesitan muchos constructores Pure para mantener los valores de la hoja. La salida de ''once'', entonces, será solo valores del tipo Free fa que son isomorfos a algún valor del tipo fa . Con este conocimiento, podemos liberar la salida de once forma segura para obtener un valor de tipo fa .

Ahora, tenga en cuenta que debido a que se requiere que mfix "ejecute la acción solo una vez", el resultado de mfix once debe, para una instancia conforme, contener una estructura monádica adicional que la que once crea en una sola aplicación. Por lo tanto, podemos deducir que el valor obtenido de mfix once también debe ser isomorfo a un valor de tipo fa .

Dada cualquier función con tipo a -> fa para algún Functor f , podemos envolver el resultado con un solo Free y obtener una función de tipo a -> Free fa que satisfaga la descripción de once arriba, y ya hemos establecido que puede desenvolver el resultado de mfix once para obtener un valor de tipo fa back.

Por lo tanto, una instancia conforme (Functor f) => MonadFix (Free f) implicaría poder escribir, mediante el ajuste y desenvolvimiento descritos anteriormente, una función ffix :: (Functor f) => (a -> fa) -> fa que funcionaría para todas las instancias de Functor .

Obviamente, eso no es una prueba de que no se puede escribir una instancia de este tipo ... pero si fuera posible, MonadFix sería completamente superfluo, ya que podría fácilmente escribir ffix directamente. (Y supongo que mfix a mfix como mfix con una restricción de liftM , usando liftM . Ugh.)

Answer 3

No, no se puede escribir en general, porque no todas las mónadas son una instancia de MonadFix. Cada mónada puede implementarse usando la FreeMonad debajo. Si pudiera implementar MonadFix de forma gratuita, entonces podría derivar MonadFix de cualquier Monad, lo cual no es posible. Pero, por supuesto, puede definir un FreeFix para la clase MonadFix.

Creo que podría parecerse a esto de alguna manera, pero esto es solo una tercera conjetura (aún sin probar):

data FreeFix m a = FreeFix { runFreeFix :: (forall r. (r -> m r) -> m r) -> m a }

instance (Monad m) => Monad (FreeFix m) where
    return a = FreeFix $ /_-> do
        return a
    f >>= g = FreeFix $ /mfx -> do
        x <- runFreeFix f mfx
        runFreeFix (g x) mfx

instance (Monad m) => MonadFix (FreeFix m) where
    mfix f = FreeFix $ /mfx -> do
        mfx (/r->runFreeFix (f r) mfx)

La idea es que m es una mónada que carece de una implementación para mfix; por lo que mfix debe ser un parámetro cuando se reducirá FreeFix.