Haskell Language
Kostenlose Monaden

Freie Monaden teilen monadische Berechnungen in Datenstrukturen und Interpreter auf

Zum Beispiel eine Berechnung mit Befehlen zum Lesen und Schreiben an der Eingabeaufforderung:

Zuerst beschreiben wir die "Befehle" unserer Berechnung als einen Functor-Datentyp

{-# LANGUAGE DeriveFunctor #-}

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

Dann verwenden wir Free , um "Free Monad über TeletypeF " zu erstellen und einige grundlegende Operationen zu erstellen.

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)

Da Free f eine Monad wenn f ein Functor , können wir die Standard- Monad Kombinatoren (einschließlich do Notation) verwenden, um Teletype Berechnungen zu erstellen.

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

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

mockingbird :: Teletype a
mockingbird = forever echo

Schließlich schreiben wir einen "Interpreter", der Teletype a Werte in etwas verwandelt, mit dem wir wie 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

Damit können wir dem Teletype a Berechnung in IO "ausführen"

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

Freie Monaden sind wie Fixpunkte

Vergleichen Sie die Definition von Free mit der von Fix :

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

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

Vergleichen Sie insbesondere den Typ des Free Konstruktors mit dem Typ des Fix Konstruktors. Free Schichten bis ein Funktor wie Fix , mit der Ausnahme , dass Free einen zusätzlichen Return a Fall.

Wie funktionieren foldFree und iterM?

Es gibt einige Funktionen, mit denen Sie Free Berechnungen iterM :: (Functor f, Monad m) => (f (ma) -> ma) -> (Free fa -> ma) indem Sie sie in eine andere Monade m interpretieren: iterM :: (Functor f, Monad m) => (f (ma) -> ma) -> (Free fa -> ma) und foldFree :: Monad m => (forall x. fx -> mx) -> (Free fa -> ma) . Was machen sie?

Lassen Sie uns zuerst sehen, was nötig ist, um eine interpretierte Funktion Teletype a IO manuell in IO zerlegen. Wir können Free fa als definiert sehen

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

Der Pure Fall ist einfach:

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

Wie interpretiert man nun eine mit dem Free Konstruktor erstellte Teletype Berechnung? Wir möchten zu einem Wert des Typs IO a durch Untersuchung von teletypeF :: TeletypeF (Teletype a) . runIO :: TeletypeF a -> IO a schreiben wir eine Funktion runIO :: TeletypeF a -> IO a die eine einzelne Schicht der freien Monade einer IO Aktion runIO :: TeletypeF a -> IO a :

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

Jetzt können wir runIO , um den Rest von interpretTeletype auszufüllen. Es sei daran erinnert, dass teletypeF :: TeletypeF (Teletype a) eine Schicht des TeletypeF Funktors ist, die den Rest der Free Berechnung enthält. Wir werden runIO , um die äußerste Schicht zu interpretieren (also haben wir runIO teletypeF :: IO (Teletype a) ) und dann den >>= Kombinator des IO - >>= zur Interpretation des zurückgegebenen Teletype a .

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

Die Definition von foldFree ist genau die von interpretTeletype , nur dass die runIO Funktion herausgefiltert wurde. foldFree arbeitet daher unabhängig von einem bestimmten Basis-Funktor und einer Ziel-Monade.

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 hat einen Rang-2-Typ: eta ist eine natürliche Transformation. Wir hätten foldFree einen Typ von Monad m => (f (Free fa) -> m (Free fa)) -> Free fa -> ma , aber dies gibt eta die Freiheit, die Free Berechnung innerhalb der f Schicht zu untersuchen. Durch die Verwendung von foldFree dieser restriktivere Typ sichergestellt, dass eta nur eine einzelne Schicht gleichzeitig verarbeiten kann.

iterM gibt der Faltfunktion die Möglichkeit, die Teilberechnung zu untersuchen. Das (monadische) Ergebnis der vorherigen Iteration steht dem nächsten Parameter innerhalb von f zur Verfügung. iterM ist analog zu einem Paramorphismus, während foldFree wie ein Katamorphismus ist .

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)

Die Freer Monade

Es gibt eine alternative Formulierung der freien Monade, die als Freer- (oder Prompt- oder Operational-) Monade bezeichnet wird. Für die Freer-Monade ist keine Functor-Instanz für den zugrunde liegenden Befehlssatz erforderlich, und sie hat eine erkennbar auflistenartige Struktur als die standardmäßige freie Monade.

Die Freer-Monade stellt Programme als Folge von atomaren Anweisungen dar, die zum Befehlssatz i :: * -> * . Jede Anweisung verwendet ihren Parameter, um ihren Rückgabetyp anzugeben. Die Basisanweisungen für die State lauten beispielsweise wie folgt:

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

Die Sequenzierung dieser Anweisungen erfolgt mit dem Konstruktor :>>= . :>>= nimmt eine einzelne Anweisung, die ein a zurückgibt, dem Rest des Programms voran und leitet dessen Rückgabewert in die Fortsetzung. Mit anderen Worten, eine Anweisung gegeben eine Rückkehr a , und eine Funktion , um ein drehen a in ein Programm ein Rückkehr b , :>>= ein Programm Zurückgeben ein produzieren b .

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

Beachten Sie, dass a im :>>= existentiell quantifiziert wird. Die einzige Möglichkeit für einen Interpreter zu erfahren, was a ist, ist die Mustererkennung auf der GADT i .

Nebenbei : Das Co-Yoneda-Lemma sagt uns, dass Freer isomorph zu Free . Erinnern Sie sich an die Definition des CoYoneda Funktors:

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

Freer i ist gleichbedeutend mit Free (CoYoneda i) . Wenn Sie die Konstruktoren von Free nehmen und f ~ CoYoneda i , erhalten Sie:

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

von dem wir erholen Freer i nur durch Einstellung ‚s Konstrukteurs Freer i ~ Free (CoYoneda i) .

Da CoYoneda i ein Functor für jedes i , ist Freer eine Monad für jedes i , auch wenn i kein 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 = (.)

Interpreter können für Freer indem Anweisungen zu einigen Handler-Monadern zugeordnet werden.

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)

Zum Beispiel können wir die Freer (StateI s) Verwendung der regulären State s Monad als Handler interpretieren:

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