Haskell Language
Mónadas Libres

Las mónadas libres dividen los cálculos monádicos en estructuras de datos e intérpretes

Por ejemplo, un cálculo que involucra comandos para leer y escribir desde el indicador:

Primero describimos los "comandos" de nuestro cálculo como un tipo de datos de Functor

{-# LANGUAGE DeriveFunctor #-}

data TeletypeF next
    = PrintLine String next
    | ReadLine (String -> next)
    deriving Functor

Luego usamos Free para crear la "Monad libre sobre TeletypeF " y construir algunas operaciones básicas.

import Control.Monad.Free (Free, liftF, iterM)

type Teletype = Free TeletypeF

printLine :: String -> Teletype ()
printLine str = liftF (PrintLine str ())

readLine :: Teletype String
readLine = liftF (ReadLine id)

Dado que Free f es una Monad siempre que f es un Functor , podemos usar los combinadores de Monad estándar (incluida la notación do ) para crear cálculos de Teletype .

import Control.Monad -- we can use the standard combinators

echo :: Teletype ()
echo = readLine >>= printLine

mockingbird :: Teletype a
mockingbird = forever echo

Finalmente, escribimos un "intérprete" que convierte a Teletype a valores en algo que sabemos cómo trabajar como IO a

interpretTeletype :: Teletype a -> IO a
interpretTeletype = foldFree run where
  run :: TeletypeF a -> IO a
  run (PrintLine str x) = putStrLn *> return x
  run (ReadLine f) = fmap f getLine

Que podemos usar para "ejecutar" el cálculo del Teletype a en IO

> interpretTeletype mockingbird
hello
hello
goodbye
goodbye
this will go on forever
this will go on forever

Las mónadas libres son como puntos fijos.

Compara la definición de Free con la de Fix :

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

newtype Fix f = Fix { unFix :: f (Fix f) }

En particular, compare el tipo del constructor Free con el tipo del constructor Fix . Free coloca un funtor como Fix , excepto que Free tiene un Return a case adicional.

¿Cómo funcionan foldFree y iterM?

Existen algunas funciones para ayudar a eliminar los cálculos de Free interpretándolos en otra mónada m : iterM :: (Functor f, Monad m) => (f (ma) -> ma) -> (Free fa -> ma) y foldFree :: Monad m => (forall x. fx -> mx) -> (Free fa -> ma) . ¿Qué están haciendo?

Primero veamos qué se necesitaría para derribar e interpretar manualmente Teletype a función de Teletype a en IO . Podemos ver a Free fa como siendo definido

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

El caso Pure es fácil:

interpretTeletype :: Teletype a -> IO a
interpretTeletype (Pure x) = return x
interpretTeletype (Free teletypeF) = _

Ahora, ¿cómo interpretar un cálculo de Teletype que se construyó con el constructor Free ? Nos gustaría llegar a un valor de tipo IO a mediante el examen de teletypeF :: TeletypeF (Teletype a) . Para empezar, escribiremos una función runIO :: TeletypeF a -> IO a que asigna una sola capa de la mónada libre a una acción IO :

runIO :: TeletypeF a -> IO a
runIO (PrintLine msg x) = putStrLn msg *> return x
runIO (ReadLine k) = fmap k getLine

Ahora podemos usar runIO para completar el resto de interpretTeletype . Recuerde que teletypeF :: TeletypeF (Teletype a) es una capa del functor TeletypeF que contiene el resto de la computación Free . Usaremos runIO para interpretar la capa más externa (por lo tanto, tenemos runIO teletypeF :: IO (Teletype a) ) y luego usaremos el combinador >>= la mónada IO para interpretar el Teletype a devuelto Teletype a .

interpretTeletype :: Teletype a -> IO a
interpretTeletype (Pure x) = return x
interpretTeletype (Free teletypeF) = runIO teletypeF >>= interpretTeletype

La definición de foldFree es solo la de interpretTeletype , excepto que la función runIO ha sido eliminada. Como resultado, foldFree funciona independientemente de cualquier funtor base particular y de cualquier mónada objetivo.

foldFree :: Monad m => (forall x. f x -> m x) -> Free f a -> m a
foldFree eta (Pure x) = return x
foldFree eta (Free fa) = eta fa >>= foldFree eta

foldFree tiene un tipo de rango 2: eta es una transformación natural. Podríamos haber dado a foldFree un tipo de Monad m => (f (Free fa) -> m (Free fa)) -> Free fa -> ma , pero eso da a eta la libertad de inspeccionar el cálculo de Free dentro de la capa f . Darle a foldFree este tipo más restrictivo garantiza que eta solo pueda procesar una capa a la vez.

iterM le da a la función de plegado la capacidad de examinar la subcomputación. El resultado (monádico) de la iteración anterior está disponible para el siguiente, dentro del parámetro f . iterM es análogo a un paramorfismo, mientras que foldFree es como un catamorfismo .

iterM :: (Monad m, Functor f) => (f (m a) -> m a) -> Free f a -> m a
iterM phi (Pure x) = return x
iterM phi (Free fa) = phi (fmap (iterM phi) fa)

La mónada Freer

Hay una formulación alternativa de la mónada libre llamada mónada Freer (o Prompt, u ​​Operational). La mónada Freer no requiere una instancia de Functor para su conjunto de instrucciones subyacentes, y tiene una estructura similar a una lista más reconocible que la mónada estándar gratuita.

La mónada Freer representa programas como una secuencia de instrucciones atómicas que pertenecen al conjunto de instrucciones i :: * -> * . Cada instrucción usa su parámetro para declarar su tipo de retorno. Por ejemplo, el conjunto de instrucciones básicas para la mónada State es el siguiente:

data StateI s a where
    Get :: StateI s s  -- the Get instruction returns a value of type 's'
    Put :: s -> StateI s ()  -- the Put instruction contains an 's' as an argument and returns ()

La secuenciación de estas instrucciones se realiza con :>>= constructor. :>>= toma una sola instrucción que devuelve una a y la precede al resto del programa, canalizando su valor de retorno a la continuación. En otras palabras, dada una instrucción que devuelve una a , y una función para convertir una a en un programa que devuelve una b :>>= producirá un programa que devuelve una b .

data Freer i a where
    Return :: a -> Freer i a
    (:>>=) :: i a -> (a -> Freer i b) -> Freer i b

Tenga en cuenta que a se cuantifica existencialmente en :>>= constructor. La única manera para que un intérprete para aprender lo que a es es por coincidencia de patrones en el GADT i .

Aparte : el lema co-Yoneda nos dice que Freer es isomorfo a Free . Recordemos la definición del funtor de CoYoneda :

data CoYoneda i b where
  CoYoneda :: i a -> (a -> b) -> CoYoneda i b

Freer i es equivalente a Free (CoYoneda i) . Si tomas los constructores de Free y configuras f ~ CoYoneda i , obtienes:

Pure :: a -> Free (CoYoneda i) a
Free :: CoYoneda i (Free (CoYoneda i) b) -> Free (CoYonda i) b ~
        i a -> (a -> Free (CoYoneda i) b) -> Free (CoYoneda i) b

a partir del cual podemos recuperar Freer i constructores 's por sólo la creación de Freer i ~ Free (CoYoneda i) .

Debido CoYoneda i es un Functor para cualquier i , Freer es una Monad para cualquier i , aunque i no es un Functor .

instance Monad (Freer i) where
    return = Return
    Return x >>= f = f x
    (i :>>= g) >>= f = i :>>= fmap (>>= f) g  -- using `(->) r`'s instance of Functor, so fmap = (.)

Los intérpretes se pueden construir para Freer asignando instrucciones a alguna mónada de manejador.

foldFreer :: Monad m => (forall x. i x -> m x) -> Freer i a -> m a
foldFreer eta (Return x) = return x
foldFreer eta (i :>>= f) = eta i >>= (foldFreer eta . f)

Por ejemplo, podemos interpretar la mónada Freer (StateI s) utilizando la mónada State s regular como un controlador:

runFreerState :: Freer (StateI s) a -> s -> (a, s)
runFreerState = State.runState . foldFreer toState
    where toState :: StateI s a -> State s a
          toState Get = State.get
          toState (Put x) = State.put x