Haskell Language
Gratis monader

Gratis monader delar upp monadiska beräkningar i datastrukturer och tolkar

Till exempel en beräkning som involverar kommandon att läsa och skriva från prompten:

Först beskriver vi "kommandona" för vår beräkning som en Functor-datatyp

{-# LANGUAGE DeriveFunctor #-}

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

Sedan använder vi Free att skapa "Free Monad over TeletypeF " och bygga några grundläggande operationer.

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)

Eftersom Free f är en Monad när f är en Functor , kan vi använda de vanliga Monad kombinatorer (inklusive do notation) för att bygga Teletype beräkningar.

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

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

mockingbird :: Teletype a
mockingbird = forever echo

Slutligen skriver vi en "tolk" som förvandlar Teletype a värden till något vi vet hur vi arbetar med som 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

Som vi kan använda för att "köra" Teletype a beräkning i IO

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

Gratis monader är som fasta punkter

Jämför definitionen av Free med Fix :

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

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

Jämför i synnerhet typen av Free konstruktör med typen av Fix . Free lager upp en funktor precis som Fix , förutom att Free har en extra Return a case.

Hur fungerar foldFree och iterM?

Det finns några funktioner som hjälper till att riva ned Free beräkningar genom att tolka dem till en annan monad m : iterM :: (Functor f, Monad m) => (f (ma) -> ma) -> (Free fa -> ma) och foldFree :: Monad m => (forall x. fx -> mx) -> (Free fa -> ma) . Vad håller de på med?

Låt oss först se vad som krävs för att riva ner en tolkning av en Teletype a funktion till IO manuellt. Vi kan se Free fa definieras

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

Pure fallet är enkelt:

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

Hur tolkar Teletype en Teletype beräkning som byggdes med Free constructor? Vi vill komma fram till ett värde av typ IO a genom att undersöka teletypeF :: TeletypeF (Teletype a) . Till att börja med skriver vi en funktion runIO :: TeletypeF a -> IO a som kartlägger ett enda lager av den fria monaden till en IO åtgärd:

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

Nu kan vi använda runIO att fylla i resten av interpretTeletype . Minns att teletypeF :: TeletypeF (Teletype a) är ett skikt av den TeletypeF funktor som innehåller resten av Free beräkning. Vi använder runIO att tolka det yttersta lagret (så vi har runIO teletypeF :: IO (Teletype a) ) och använder sedan IO monaden >>= combinator för att tolka den returnerade Teletype a .

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

Definitionen av foldFree är bara den för interpretTeletype , förutom att runIO funktionen har tagits bort. Som ett resultat fungerar foldFree oberoende av någon speciell basfunktor och vilken målmonad som helst.

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 har en rang-2-typ: eta är en naturlig transformation. Vi kunde ha gett foldFree en typ av Monad m => (f (Free fa) -> m (Free fa)) -> Free fa -> ma , men det ger eta friheten att inspektera den Free beräkningen inuti f lagret. Ge foldFree denna mer restriktiva typ säkerställer att eta bara kan behandla ett enda lager åt gången.

iterM ger vikningsfunktionen förmågan att undersöka underkomputationen. (Monadiskt) resultat från den föregående iterationen är tillgängligt för nästa, inre f 's parameter. iterM är analog med en paramorfism medan foldFree är som en katamorfism .

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)

Den friare monaden

Det finns en alternativ formulering av den fria monaden som kallas Freer (eller Prompt eller Operational) monad. Freer-monaden kräver inte en Functor-instans för den underliggande instruktionsuppsättningen, och den har en mer kännbar listliknande struktur än den standardfria monaden.

Den Freer monad representerar program som en sekvens av atom instruktioner som hör till instruktionsuppsättning i :: * -> * . Varje instruktion använder sin parameter för att deklarera sin returtyp. Till exempel uppsättningen bas instruktioner för State mona är följande:

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

Sekvensering av dessa instruktioner sker med :>>= konstruktören. :>>= tar en enda instruktion som returnerar ett a och beror på det till resten av programmet och rör dess returvärde till fortsättningen. Med andra ord, med tanke på en instruktion som returnerar en a , och en funktion för att förvandla a till ett program som returnerar a b , kommer :>>= att producera ett program som returnerar a b .

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

Observera att a är existentiellt kvantifierat i :>>= konstruktören. Det enda sättet för en tolk att lära sig vad a är är genom att matcha mönster på GADT i .

Vid sidan : Sam-Yoneda-lemmet berättar att Freer är isomorf för Free . Kom ihåg definitionen av CoYoneda funktorn:

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

Freer i motsvarar Free (CoYoneda i) . Om du tar Free 's konstruktörer och ställer in f ~ CoYoneda i , får du:

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

från vilken vi kan återfå Freer i 's konstruktörer genom att bara ställa in Freer i ~ Free (CoYoneda i) .

Eftersom CoYoneda i är en Functor för alla i , är Freer en Monad för alla i , även om i inte är en 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 = (.)

Tolkar kan byggas för Freer genom att kartlägga instruktioner till någon hanteringsmonad.

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)

Vi kan till exempel tolka Freer (StateI s) monaden med den vanliga State s monaden som en hanterare:

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