Haskell Language
Darmowe Monady

Darmowe monady dzielą obliczenia monadyczne na struktury danych i interpretatory

Na przykład obliczenia obejmujące polecenia do odczytu i zapisu z monitu:

Najpierw opisujemy „polecenia” naszego obliczenia jako typ danych Functor

{-# LANGUAGE DeriveFunctor #-}

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

Następnie używamy Free aby stworzyć „Free Monad over TeletypeF ” i zbudować kilka podstawowych operacji.

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)

Ponieważ Free f jest Monad gdy f jest Functor , możemy użyć standardowych Monad kombinatorów (w tym do notacji), aby zbudować Teletype obliczeń.

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

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

mockingbird :: Teletype a
mockingbird = forever echo

Na koniec piszemy „tłumacza” zmieniającego Teletype a wartości w coś, co wiemy, jak pracować z 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

Którego możemy użyć do „uruchomienia” Teletype a obliczeń w IO

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

Darmowe monady są jak stałe punkty

Porównaj definicję Free z definicją Fix :

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

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

W szczególności porównaj typ konstruktora Free z typem konstruktora Fix . Free nakłada funktor podobnie jak Fix , z tym wyjątkiem, że Free ma dodatkowy Return a skrzynkę.

Jak działają foldFree i iterM?

Istnieje kilka funkcji, które pomagają zburzyć Free obliczenia, interpretując je na inną iterM :: (Functor f, Monad m) => (f (ma) -> ma) -> (Free fa -> ma) m : iterM :: (Functor f, Monad m) => (f (ma) -> ma) -> (Free fa -> ma) i foldFree :: Monad m => (forall x. fx -> mx) -> (Free fa -> ma) . Co oni robią?

Najpierw zobaczmy, czego potrzeba, aby ręcznie zinterpretować funkcję Teletype a funkcji w IO . Widzimy Free fa jako zdefiniowane

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

Obudowa Pure jest łatwa:

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

Jak interpretować obliczenia Teletype zbudowane za pomocą konstruktora Free ? Chcielibyśmy osiągnąć wartość typu IO a , badając teletypeF :: TeletypeF (Teletype a) . Na początek napiszemy funkcję runIO :: TeletypeF a -> IO a która odwzorowuje pojedynczą warstwę wolnej monady na akcję IO :

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

Teraz możemy użyć runIO aby wypełnić resztę interpretTeletype . Przypomnijmy, że teletypeF :: TeletypeF (Teletype a) to warstwa funktora TeletypeF która zawiera resztę obliczeń Free . Użyjemy runIO do interpretacji zewnętrznej warstwy (więc mamy runIO teletypeF :: IO (Teletype a) ), a następnie użyjemy kombinatora >>= monady IO >>= do interpretacji zwróconego Teletype a .

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

Definicja foldFree to po prostu interpretTeletype , z tą różnicą, że funkcja runIO została uwzględniona. W rezultacie foldFree działa niezależnie od konkretnego funktora podstawowego i dowolnej docelowej monady.

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 ma typ rangi 2: eta jest naturalną transformacją. Moglibyśmy dać foldFree rodzaj Monad m => (f (Free fa) -> m (Free fa)) -> Free fa -> ma , ale daje to eta swobodę w sprawdzaniu Free obliczenia wewnątrz warstwy f . foldFree Ten bardziej restrykcyjny typ zapewnia, że eta może przetwarzać tylko jedną warstwę na raz.

iterM daje funkcji składania możliwość zbadania podliczenia. (Monadyczny) wynik poprzedniej iteracji jest dostępny dla następnego, wewnątrz parametru f . iterM jest analogiczny do paramorfizmu, podczas gdy foldFree jest jak katamorfizm .

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)

Monada Freera

Istnieje alternatywne sformułowanie wolnej monady zwanej monadą Freer (lub Monit lub Operacyjna). Monada Freera nie wymaga instancji Functor dla podstawowego zestawu instrukcji i ma bardziej rozpoznawalną strukturę listy niż standardowa wolna monada.

Monada Freera reprezentuje programy jako sekwencję instrukcji atomowych należących do zestawu instrukcji i :: * -> * . Każda instrukcja używa swojego parametru, aby zadeklarować swój typ zwracany. Na przykład zestaw instrukcji podstawowych dla monady State jest następujący:

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

Sekwencjonowanie tych instrukcji odbywa się za pomocą konstruktora :>>= . :>>= pobiera pojedynczą instrukcję zwracającą a i przygotowuje ją do reszty programu, przekazując jej wartość zwrotną do kontynuacji. Innymi słowy, biorąc pod uwagę dyspozycję zwrócenie a i funkcję przekształcić a do programu Zwracanie b , :>>= będzie produkować program przekazujących b .

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

Zauważ, że a jest egzystencjalnie określone ilościowo w :>>= konstruktor. Jedynym sposobem dla tłumacza, aby dowiedzieć się, co a jest, jest dopasowanie wzoru w GADT i .

Bok: Jednoczesne Yoneda lemat mówi nam, że Freer jest izomorficzna Free . Przywołaj definicję funktora CoYoneda :

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

Freer i jest równoważny Free (CoYoneda i) . Jeśli weźmiesz konstruktory Free i ustawisz f ~ CoYoneda i , otrzymasz:

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

z którego możemy odzyskać Freer i „s konstruktorów po prostu ustawienie Freer i ~ Free (CoYoneda i) .

Ponieważ CoYoneda i to Functor dla każdego i , Freer jest Monad dla każdego i , nawet jeśli i nie jest 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 = (.)

Tłumacze mogą być budowane dla Freer poprzez mapowanie instrukcji do niektórych monad obsługi.

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)

Na przykład możemy interpretować Freer (StateI s) używając zwykłej monady State s jako procedury obsługi:

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