Haskell Language
Gratis monaden

Gratis monaden splitsen monadische berekeningen op in gegevensstructuren en tolken

Bijvoorbeeld een berekening met opdrachten om vanaf de prompt te lezen en te schrijven:

Eerst beschrijven we de "commando's" van onze berekening als een Functor-gegevenstype

{-# LANGUAGE DeriveFunctor #-}

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

Vervolgens gebruiken we Free om de "Free Monad over TeletypeF " te maken en enkele basisbewerkingen uit te voeren.

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)

Aangezien Free f is een Monad wanneer f is een Functor , kunnen we de standaard gebruiken Monad combinators (met inbegrip van do notatie) op te bouwen Teletype berekeningen.

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

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

mockingbird :: Teletype a
mockingbird = forever echo

Ten slotte schrijven we een "tolk" die van Teletype a waarde maakt waarvan we weten hoe we ermee moeten werken, zoals 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

Die we kunnen gebruiken om het Teletype a berekening in IO te "draaien"

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

Gratis monaden zijn als vaste punten

Vergelijk de definitie van Free met die van Fix :

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

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

Vergelijk met name het type Free constructor met het type Fix constructor. Free stapelt een functor op net als Fix , behalve dat Free een extra Return a case heeft.

Hoe werken foldFree en iterM?

Er zijn enkele functies om Free berekeningen af te breken door ze in een andere monade m interpreteren: iterM :: (Functor f, Monad m) => (f (ma) -> ma) -> (Free fa -> ma) en foldFree :: Monad m => (forall x. fx -> mx) -> (Free fa -> ma) . Wat zijn ze aan het doen?

Laten we eerst eens kijken wat er nodig zou zijn om een Teletype a functie handmatig in IO . We kunnen Free fa als gedefinieerd

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

De Pure case is eenvoudig:

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

Hoe interpreteer je een Teletype berekening die is gebouwd met de Free constructor? We willen graag een waarde van type IO a door teletypeF :: TeletypeF (Teletype a) . Om te beginnen schrijven we een functie runIO :: TeletypeF a -> IO a die een enkele laag van de vrije monade toewijst aan een IO actie:

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

Nu kunnen we runIO gebruiken om de rest van interpretTeletype in te vullen. Bedenk dat teletypeF :: TeletypeF (Teletype a) een laag van de TeletypeF functor is die de rest van de Free berekening bevat. We zullen runIO om de buitenste laag te interpreteren (dus we hebben runIO teletypeF :: IO (Teletype a) ) en gebruiken vervolgens de IO monad's >>= combinator om het geretourneerde Teletype a te interpreteren.

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

De definitie van foldFree is alleen die van interpretTeletype , behalve dat de runIO functie buiten beschouwing is runIO . Als gevolg foldFree werkt foldFree onafhankelijk van een bepaalde foldFree en van elke doelmonade.

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 heeft een rang-2 type: eta is een natuurlijke transformatie. We hadden foldFree een type Monad m => (f (Free fa) -> m (Free fa)) -> Free fa -> ma , maar dat geeft eta de vrijheid om de Free berekening in de f laag te inspecteren. foldFree geven dit beperktere type zorgt ervoor dat eta slechts één laag tegelijk kan verwerken.

iterM geeft de vouwfunctie de mogelijkheid om de subcomputatie te onderzoeken. Het (monadische) resultaat van de vorige iteratie is beschikbaar voor de volgende, binnen de parameter f . iterM is analoog aan een paramorfisme, terwijl foldFree als een catamorfisme is .

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)

De vrijere monade

Er is een alternatieve formulering van de vrije monade genaamd de vrijere (of prompt of operationele) monade. De Freer-monade heeft geen Functor-instantie nodig voor de onderliggende instructieset en heeft een meer herkenbare lijstachtige structuur dan de standaard vrije monade.

De vrijere monade vertegenwoordigt programma's als een reeks atomaire instructies behorende bij de instructieset i :: * -> * . Elke instructie gebruikt zijn parameter om het retourtype aan te geven. Bijvoorbeeld, de set van de basis-instructies voor de State monade zijn als volgt:

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

Volgorde van deze instructies vindt plaats met de :>>= constructor. :>>= neemt een enkele instructie die een a retourneert en bereidt deze voor op de rest van het programma, waarbij de retourwaarde naar de voortzetting wordt geleid. Met andere woorden, gegeven een instructie die een a retourneert, en een functie om van een a een programma te maken dat een b retourneert b :>>= zal een programma produceren dat een b retourneert.

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

Merk op dat a existentieel wordt gekwantificeerd in de :>>= constructor. De enige manier voor een tolk om te leren wat a is, is door patroonvergelijking op de GADT i .

Terzijde : het co-Yoneda-lemma vertelt ons dat Freer isomorf is voor Free . Denk aan de definitie van de CoYoneda functor:

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

Freer i is gelijk aan Free (CoYoneda i) . Als je de constructeurs van Free neemt en f ~ CoYoneda i , krijg je:

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

waaruit we de constructeurs van Freer i kunnen herstellen door gewoon Freer i ~ Free (CoYoneda i) .

Omdat CoYoneda i een Functor voor elke i , is Freer een Monad voor elke i , zelfs als i geen 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 = (.)

Tolken kunnen worden gebouwd voor Freer door instructies toe te wijzen aan een monteur.

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)

We kunnen bijvoorbeeld de Freer (StateI s) monade interpreteren met behulp van de reguliere State s monade als handler:

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