Поиск…


Свободные монады разделяют монадические вычисления на структуры данных и интерпретаторы

Например, вычисление, включающее команды для чтения и записи из приглашения:

Сначала мы описываем «команды» нашего вычисления как типа данных «Фунтор»

{-# LANGUAGE DeriveFunctor #-}

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

Затем мы используем Free для создания «Free Monad over TeletypeF » и создаем некоторые основные операции.

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)

Поскольку Free f является Monad , когда f является Functor , мы можем использовать стандартную Monad комбинатор (включая do запись) , чтобы построить Teletype вычисления.

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

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

mockingbird :: Teletype a
mockingbird = forever echo

Наконец, мы пишем «интерпретатор», который превращает Teletype a ценности, которые мы знаем, как работать с 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

Что мы можем использовать для «запуска» Teletype a вычисления в IO

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

Свободные монады похожи на неподвижные точки

Сравните определение Free с определением Fix :

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

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

В частности, сравните тип конструктора Free с типом конструктора Fix . Free слои создают функтор так же, как Fix , за исключением того, что Free имеет дополнительный Return a .

Как работают foldFree и iterM?

Есть несколько функций, которые помогут свести Free вычисления, интерпретируя их в другую монаду m : iterM :: (Functor f, Monad m) => (f (ma) -> ma) -> (Free fa -> ma) и foldFree :: Monad m => (forall x. fx -> mx) -> (Free fa -> ma) . Что они делают?

Сначала давайте посмотрим, что потребуется, чтобы скрыть интерпретацию функции Teletype a в IO вручную. Мы можем видеть, что Free fa определяется

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

Pure случай прост:

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

Теперь, как интерпретировать вычисление Teletype которое было построено с помощью конструктора Free ? Мы хотели бы получить значение типа IO a , исследуя teletypeF :: TeletypeF (Teletype a) . Для начала напишем функцию runIO :: TeletypeF a -> IO a которая отображает один слой свободной монады в действие IO :

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

Теперь мы можем использовать runIO для заполнения остальной interpretTeletype . Напомним, что teletypeF :: TeletypeF (Teletype a) является слоем функтора TeletypeF который содержит остальные вычисления Free . Мы будем использовать runIO интерпретировать внешний слой (таким образом , мы имеем runIO teletypeF :: IO (Teletype a) ) , а затем использовать IO монады >>= комбинатор интерпретировать Возвращенный Teletype a .

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

Определение foldFree - это просто interpretTeletype , за исключением того, что функция runIO была runIO . В результате foldFree работает независимо от любого конкретного базового функтора и любой целевой монады.

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 имеет тип ранга-2: eta - естественное преобразование. Мы могли бы дать foldFree типа Monad m => (f (Free fa) -> m (Free fa)) -> Free fa -> ma , но это дает eta свободу осматривая Free вычисления внутри f слоя. Предоставление foldFree этого более ограничительного типа гарантирует, что eta может обрабатывать только один слой за раз.

iterM дает функции свертывания возможность изучить подкоманду. Результат (monadic) предыдущей итерации доступен для следующего параметра внутри f . iterM аналогичен параморфизму, тогда как foldFree подобен катаморфизму .

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)

Свободная монада

Существует альтернативная формулировка свободной монады, называемой монадой фрира (или приглашением, или оперативной). Мост Freer не требует экземпляра Functor для своего базового набора команд, и он имеет более узнаваемую структуру списка, чем стандартная свободная монада.

Freer monad представляет программы как последовательность атомных инструкций, принадлежащих набору команд i :: * -> * . Каждая команда использует свой параметр для объявления своего типа возврата. Например, набор базовых инструкций для State монады выглядит следующим образом:

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

Секвенирование этих инструкций происходит с помощью :>>= constructor. :>>= принимает одну инструкцию, возвращающую a и добавляет ее к остальной части программы, передавая ее возвращаемое значение в продолжение. Другими словами, учитывая инструкцию, возвращающую a и функцию, чтобы превратить a в программу, возвращающую b :>>= создаст программу, возвращающую b .

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

Заметим, что a существует в количественном выражении в конструкторе :>>= . Единственный способ для интерпретатора узнать, что такое a - это сопоставление шаблонов на GADT i .

Кроме того, лемма совместной Йонеды говорит нам, что Freer изоморфен Free . Напомним определение функтора CoYoneda :

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

Freer i эквивалентен Free (CoYoneda i) . Если вы берете конструкторы Free и устанавливаете f ~ CoYoneda i , вы получаете:

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

из которого мы можем восстановить конструкторы Freer i , просто установив Freer i ~ Free (CoYoneda i) .

Поскольку CoYoneda i является Functor для любого i , Freer является Monad для любого i , даже если i не является 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 = (.)

Интерпретаторы могут быть созданы для Freer путем сопоставления инструкций некоторым монахам-обработчикам.

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)

Например, мы можем интерпретировать монаду Freer (StateI s) использующую монаду обычного State s в качестве обработчика:

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


Modified text is an extract of the original Stack Overflow Documentation
Лицензировано согласно CC BY-SA 3.0
Не связан с Stack Overflow