Haskell Language
Monades gratuites
Recherche…
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 foncteurCoYoneda
: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 deFree
et définissezf ~ 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églageFreer 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