Haskell Language
Monades gratuites

Monades gratuites divisent les calculs monadiques en structures de données et interprètes

Par exemple, un calcul impliquant des commandes à lire et à écrire à l'invite:

Nous décrivons tout d'abord les "commandes" de notre calcul en tant que type de données Functor

{-# LANGUAGE DeriveFunctor #-}

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

Ensuite, nous utilisons Free pour créer "Free Monad over TeletypeF " et créer des opérations de base.

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)

Comme Free f est une Monad lorsque f est un Functor , nous pouvons utiliser les combinateurs Monad standard (y compris la notation do ) pour construire des calculs Teletype .

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

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

mockingbird :: Teletype a
mockingbird = forever echo

Enfin, nous écrivons un "interprète" qui transforme les valeurs Teletype a en quelque chose que nous savons utiliser avec 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 nous pouvons utiliser pour "exécuter" le Teletype a calcul en IO

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

Les Monades gratuites sont comme des points fixes

Comparez la définition de Free à celle de Fix :

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

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

En particulier, comparez le type du constructeur Free avec le type du constructeur Fix . Free couches Free montent un foncteur comme Fix , sauf que Free a un Return a supplémentaire.

Comment foldFree et iterM fonctionnent-ils?

Il y a quelques fonctions pour aider à décomposer Free calculs Free en les interprétant dans une autre monade m : iterM :: (Functor f, Monad m) => (f (ma) -> ma) -> (Free fa -> ma) et foldFree :: Monad m => (forall x. fx -> mx) -> (Free fa -> ma) . Que font-ils?

Tout d'abord, voyons ce qu'il faudrait pour IO manuellement Teletype a fonction de Teletype a dans IO . On peut voir Free fa comme étant défini

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

Le cas Pure est facile:

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

Maintenant, comment interpréter un calcul de Teletype construit avec le constructeur Free ? Nous aimerions obtenir une valeur de type IO a en examinant teletypeF :: TeletypeF (Teletype a) . Pour commencer, nous allons écrire une fonction runIO :: TeletypeF a -> IO a qui mappe une seule couche de monad libre sur une action IO :

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

Maintenant, nous pouvons utiliser runIO pour remplir le reste de interpretTeletype . Rappelons que teletypeF :: TeletypeF (Teletype a) est une couche du foncteur TeletypeF qui contient le reste du calcul Free . Nous utiliserons runIO pour interpréter la couche la plus externe (nous avons donc runIO teletypeF :: IO (Teletype a) ) et utilisons ensuite le combinateur >>= monade IO pour interpréter le Teletype a renvoyé Teletype a .

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

La définition de foldFree est juste celle de interpretTeletype , sauf que la fonction runIO a été runIO . Par conséquent, foldFree fonctionne indépendamment de tout foncteur de base particulier et de toute monade cible.

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 a un type rank-2: eta est une transformation naturelle. On aurait pu donner à foldFree un type de Monad m => (f (Free fa) -> m (Free fa)) -> Free fa -> ma , mais cela donne à eta la liberté d’inspecter le calcul Free dans le calque f . Donner à foldFree ce type plus restrictif garantit que eta ne peut traiter qu'un seul calque à la fois.

iterM donne à la fonction de pliage la possibilité d'examiner le sous-calcul. Le résultat (monadique) de l'itération précédente est disponible pour le suivant, à l'intérieur du paramètre de f . iterM est analogue à un paramorphisme, alors que foldFree est comme un catamorphisme .

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 monade plus libre

Il existe une autre formulation de la monade libre appelée la monade Freer (ou Prompt ou Operational). Le Monad Freer ne nécessite pas d'instance Functor pour son jeu d'instructions sous-jacent, et sa structure ressemble à celle d'une monade libre standard.

La monade Freer représente les programmes sous la forme d'une séquence d' instructions atomiques appartenant au jeu d'instructions i :: * -> * . Chaque instruction utilise son paramètre pour déclarer son type de retour. Par exemple, les instructions de base pour la monade d' State sont les suivantes:

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 ()

Le séquençage de ces instructions s'effectue avec le constructeur :>>= . :>>= prend une seule instruction renvoyant un a et le ajoute au reste du programme, introduisant sa valeur de retour dans la suite. En d'autres termes, étant donné une instruction renvoyant un a , et une fonction pour transformer a en un programme renvoyant un b :>>= produira un programme renvoyant un b .

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

Notez que a est quantifié existentiellement dans le constructeur :>>= . La seule manière pour un interprète d'apprendre ce qu'est a est de faire correspondre un motif sur le GADT i .

À part : Le lemme co-Yoneda nous dit que Freer est isomorphe à Free . Rappelons la définition du foncteur CoYoneda :

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

Freer i est équivalent à Free (CoYoneda i) . Si vous prenez les constructeurs de Free et définissez f ~ CoYoneda i , vous obtenez:

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

à partir de laquelle nous pouvons récupérer Freer i constructeurs d » en tout réglage Freer i ~ Free (CoYoneda i) .

Parce que CoYoneda i est un Functor pour tout i , Freer est une Monad pour tout i , même si i ne i pas 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 = (.)

Des interpréteurs peuvent être construits pour Freer en mappant des instructions à certains gestionnaires de monade.

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)

Par exemple, nous pouvons interpréter la monade Freer (StateI s) utilisant la monade de l' State s normal comme gestionnaire:

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