Экземпляр MonadFix для преобразователя монад интерпретатора, созданного FreeT?

У меня есть упрощенная версия стандартного интерпретатора монад трансформатора, сгенерированного FreeT:

data InteractiveF p r a = Interact p (r -> a)

type Interactive p r = FreeT (InteractiveF p r)

p это "подсказка", и r это "среда"... можно было бы запустить что-то вроде:

runInteractive :: Monad m => (p -> m r) -> Interactive p r m a -> m a
runInteractive prompt iact = do
  ran <- runFreeT iact
  case ran of
    Pure x -> return x
    Free (Interact p f) -> do
      response <- prompt p
      runInteractive prompt (f resp)

instance MonadFix m => MonadFix (FreeT (InteractiveF p r)) m a)
mfix = -- ???

Я чувствую, что этот тип более или менее просто ограниченная версия StateT... если что, Interactive p r IO Я думаю, что ограниченная версия IO... я думаю... но... в любом случае, моя интуиция говорит, что должен быть хороший пример.

Я пытался написать один, но не могу понять. Моя самая близкая попытка была:

mfix f = FreeT (mfix (runFreeT . f . breakdown))
  where
    breakdown :: FreeF (InteractiveF p r) a (FreeT (InteractiveF p r) m a) -> a
    breakdown (Pure x) = x
    breakdown (Free (Interact p r)) = -- ...?

Я также попытался использовать версию, используя преимущества MonadFix экземпляр mно тоже не повезло -

mfix f = FreeT $ do
  rec ran <- runFreeT (f z)
      z   <- case ran of
               Pure x -> return x
               Free iact -> -- ...
  return -- ...

Кто-нибудь знает, возможно ли это вообще вообще или почему нет? Если это так, то для чего мне продолжать искать?

Кроме того, в моем реальном приложении мне даже не нужно использовать FreeT... я могу просто использовать Free; то есть Interactive быть просто монадой, а не просто монадой-трансформером, и иметь

runInteractive :: Monad m => (p -> m r) -> Interactive p r a -> m a
runInteractive _ (Pure x) = return x
runInteractive prompt (Free (Interact p f) = do
    response <- prompt p
    runInteractive prompt (f response)

Если что-то возможно для этого случая, а не для общего случая FreeT, я также был бы счастлив:)

Источник

2 ответа

Решение

Представьте, что у вас уже есть переводчик для Interactive,

interpret :: FreeT (InteractiveF p r) m a -> m a
interpret = undefined

Было бы тривиально написать MonadFix пример:

instance MonadFix m => MonadFix (FreeT (InteractiveF p r) m) where
    mfix = lift . mfix . (interpret .)

Мы можем напрямую уловить эту идею "знания переводчика", не обращаясь к переводчику заранее.

{-# LANGUAGE RankNTypes #-}

data UnFreeT t m a = UnFree {runUnFreeT :: (forall x. t m x -> m x) -> t m a}
--   given an interpreter from `t m` to `m` ^                          |
--                                  we have a value in `t m` of type a ^

UnFreeT это просто ReaderT это читает переводчик.

Если t это монадный трансформатор, UnFreeT t также монадный трансформатор. Мы можем легко построить UnFreeT из вычислений, которые не требуют знания интерпретатора, просто игнорируя интерпретатор.

unfree :: t m a -> UnFreeT t m a
--unfree = UnFree . const
unfree x = UnFree $ \_ -> x

instance (MonadTrans t) => MonadTrans (UnFreeT t) where
    lift = unfree . lift

Если t это монад трансормер, m это Monad, а также t m также Monad, затем UnFree t m это Monad, При наличии интерпретатора мы можем связать вместе два вычисления, которые требуют интерпретатора.

{-# LANGUAGE FlexibleContexts #-}

refree :: (forall x. t m x -> m x) -> UnFreeT t m a -> t m a
-- refree = flip runUnFreeT
refree interpreter x = runUnFreeT x interpreter

instance (MonadTrans t, Monad m, Monad (t m)) => Monad (UnFreeT t m) where
    return = lift . return
    x >>= k = UnFree $ \interpreter -> runUnFreeT x interpreter >>= refree interpreter . k

Наконец, с учетом интерпретатора, мы можем исправить вычисления, пока основная монада имеет MonadFix пример.

instance (MonadTrans t, MonadFix m, Monad (t m)) => MonadFix (UnFreeT t m) where
    mfix f = UnFree $ \interpreter -> lift . mfix $ interpreter . refree interpreter . f

На самом деле мы можем сделать все, что может сделать лежащая в основе монада, как только у нас будет интерпретатор. Это потому, что, как только мы имеем interpreter :: forall x. t m x -> m x мы можем сделать все из следующего. Мы можем пойти из m x через t m x вплоть до UnFreeT t m x и снова отступи.

                      forall x.
lift               ::           m x ->         t m x
unfree             ::         t m x -> UnFreeT t m x
refree interpreter :: UnFreeT t m x ->         t m x
interpreter        ::         t m x ->           m x

использование

Для тебя Interactiveоберните FreeT в UnFreeT,

type Interactive p r = UnFreeT (FreeT (InteractiveF p r))

Ваши переводчики все равно будут написаны, чтобы произвести FreeT (InteractiveF p r) m a -> m a, Интерпретировать новое Interactive p r m a вплоть до m a вы бы использовали

interpreter . refree interpreter

UnFreeT больше не "освобождает переводчика настолько, насколько это возможно". Переводчик больше не может принимать произвольные решения о том, что делать, где он хочет. Вычисление в UnFreeT могу попросить переводчика. Когда вычисление требует и использует интерпретатор, тот же интерпретатор будет использоваться для интерпретации той части программы, которая использовалась для начала интерпретации программы.

Источник

Невозможно написать MonadFix m => MonadFix (Interactive p r) пример.

Ваш InteractiveF является базовым функтором хорошо изученных машин Мура. Машина Мура обеспечивает вывод, в вашем случае приглашение, а затем определяет следующее, что нужно сделать на основе ввода, в вашем случае среды. Машина Мура всегда выводит первой.

data MooreF a b next = MooreF b (a -> next)
    deriving (Functor)

Если мы будем следовать аргументу CA Макканна о написании MonadFix случаи для Free но ограничимся конкретным случаем Free (MooreF a b)мы в конечном итоге определим, что если есть MonadFix экземпляр для Free (MooreF a b) тогда должна существовать функция

mooreFfix :: (next -> MooreF a b next) -> MooreF a b next

Чтобы написать эту функцию, мы должны построить MooreF b (f :: a -> next), У нас нет bs для вывода. Вполне возможно, что мы могли бы получить b если у нас уже было следующее a, но машина Мура всегда выводит первой.

Вроде бы в штат

Вы можете написать что-то близкое к mooreFfix если вы читаете только один a вперед.

almostMooreFfix :: (next -> MooreF a b next) -> a -> MooreF a b next
almostMooreFfix f a = let (MooreF b g) = f (g a)
                      in (MooreF b g)

Затем становится необходимым, чтобы f быть в состоянии определить g независимо от аргумента next, Все возможное fs для использования имеют форму f next = MooreF (f' next) g' где f' а также g' некоторые другие функции.

almostMooreFFix :: (next -> b) -> (a -> next) -> a -> MooreF a b next
almostMooreFFix f' g' a = let (MooreF b g) = f (g a)
                          in (MooreF b g)
                          where
                              f next = MooreF (f' next) g'

С некоторыми уравновешенными рассуждениями мы можем заменить f на правой стороне let

almostMooreFFix :: (next -> b) -> (a -> next) -> a -> MooreF a b next
almostMooreFFix f' g' a = let (MooreF b g) = MooreF (f' (g a)) g'
                          in (MooreF b g)

Мы связываем g в g',

almostMooreFFix :: (next -> b) -> (a -> next) -> a -> MooreF a b next
almostMooreFFix f' g' a = let (MooreF b _) = MooreF (f' (g' a)) g'
                          in (MooreF b g')

Когда мы связываем b в f' (g' a) let становится ненужным, и функция не имеет рекурсивного узла.

almostMooreFFix :: (next -> b) -> (a -> next) -> a -> MooreF a b next
almostMooreFFix f' g' a = MooreF (f' (g' a)) g'

Все almostMooreFFixесли это не так undefined даже не нужно let,

Источник
Другие вопросы по тегам