Haskell Language
Monadi gratuiti

Le monadi libere dividono i calcoli monadici in strutture dati e interpreti

Ad esempio, un calcolo che coinvolge i comandi da leggere e scrivere dal prompt:

Per prima cosa descriviamo i "comandi" del nostro calcolo come un tipo di dati Functor

{-# LANGUAGE DeriveFunctor #-}

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

Quindi usiamo Free per creare il "Free Monad over TeletypeF " e creare alcune operazioni di 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)

Dal momento Free f è un Monad ogni volta che f è un Functor , siamo in grado di utilizzare lo standard Monad combinatori (compreso do la notazione) per costruire Teletype calcoli.

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

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

mockingbird :: Teletype a
mockingbird = forever echo

Infine, scriviamo un "interprete" che trasforma i valori di Teletype a in qualcosa che sappiamo come lavorare con 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

Che possiamo usare per "eseguire" il Teletype a calcolo in IO

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

Le Monade libere sono come punti fissi

Confronta la definizione di Free con quella di Fix :

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

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

In particolare, confronta il tipo di costruttore Free con il tipo di costruttore Fix . Free livelli di un functor come Fix , tranne che Free ha un Return a case aggiuntivo.

Come funzionano foldFree e iterM?

Ci sono alcune funzioni che aiutano a demolire i calcoli Free interpretandoli in un altro monad m : iterM :: (Functor f, Monad m) => (f (ma) -> ma) -> (Free fa -> ma) e foldFree :: Monad m => (forall x. fx -> mx) -> (Free fa -> ma) . Cosa stanno facendo?

Per prima cosa vediamo cosa servirebbe per eliminare un'interpretazione Teletype a funzione in IO manualmente. Possiamo vedere Free fa come definito

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

Il caso Pure è semplice:

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

Ora, come interpretare un calcolo Teletype che è stato creato con il costruttore Free ? Vorremmo arrivare a un valore di tipo IO a esaminando teletypeF :: TeletypeF (Teletype a) . Per cominciare, scriveremo una funzione runIO :: TeletypeF a -> IO a che mappa un singolo livello della monade libera in un'azione IO :

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

Ora possiamo usare runIO per riempire il resto di interpretTeletype . Ricordiamo che teletypeF :: TeletypeF (Teletype a) è uno strato del functor TeletypeF che contiene il resto del calcolo Free . Useremo runIO per interpretare il livello più esterno (quindi abbiamo runIO teletypeF :: IO (Teletype a) ) e poi usiamo il monitore di IO >>= combinatore per interpretare il Teletype a restituito Teletype a .

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

La definizione di foldFree è proprio quella di interpretTeletype , tranne per il fatto che la funzione runIO è stata runIO . Di conseguenza, foldFree funziona indipendentemente da un particolare foldFree di base e da qualsiasi monade bersaglio.

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 ha un tipo rank-2: l' eta è una trasformazione naturale. Potremmo aver dato foldFree un tipo di Monad m => (f (Free fa) -> m (Free fa)) -> Free fa -> ma , ma che dà a eta la libertà di ispezionare il calcolo Free all'interno del livello f . Dare foldFree questo tipo più restrittivo garantisce che eta possa elaborare solo un singolo livello alla volta.

iterM conferisce alla funzione di piegatura la possibilità di esaminare la subcomputazione. Il risultato (monadico) della precedente iterazione è disponibile per il parametro successivo, inside f . iterM è analogo a un paramorfismo mentre foldFree è come 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 monade Freer

C'è una formulazione alternativa della monade libera chiamata monade Freer (o Prompt o Operational). La monade Freer non richiede un'istanza di Functor per il suo set di istruzioni sottostante, e ha una struttura più simile a una lista rispetto alla monade libera standard.

La monade Freer rappresenta i programmi come una sequenza di istruzioni atomiche appartenenti all'insieme di istruzioni i :: * -> * . Ogni istruzione usa il suo parametro per dichiarare il suo tipo di ritorno. Ad esempio, il set di istruzioni di base per la monade di State sono i seguenti:

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

Il sequenziamento di queste istruzioni avviene con :>>= costruttore. :>>= accetta una singola istruzione restituendo una a e la antepone al resto del programma, convogliando il suo valore di ritorno nella continuazione. In altre parole, data un'istruzione che restituisce un a , e una funzione per trasformare un a in un programma che restituisce un b :>>= produrrà un programma che restituisce un b .

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

Si noti che a è quantificato in modo esistenziale nel :>>= costruttore. L'unico modo in cui un interprete può imparare cos'è a pattern matching per GADT i .

A parte : il lemma del co-Yoneda ci dice che Freer è isomorfo a Free . Richiama la definizione del CoYoneda :

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

Freer i è equivalente a Free (CoYoneda i) . Se prendi i costruttori di Free e imposta f ~ CoYoneda i , ottieni:

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

da cui possiamo recuperare Freer i costruttori di Freer i ~ Free (CoYoneda i) semplicemente impostando Freer i ~ Free (CoYoneda i) .

Perché CoYoneda i è un Functor per qualsiasi i , Freer è un Monad per qualsiasi i , anche se i non è 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 = (.)

Gli interpreti possono essere costruiti per Freer mappando le istruzioni su una monade di gestori.

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)

Ad esempio, possiamo interpretare la monade Freer (StateI s) usando la monade dello State s regolare come gestore:

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