Преобразование этой функции FreeT (явно рекурсивный тип данных) для работы на FT (церковное кодирование) - PullRequest
Новая
       27

Преобразование этой функции FreeT (явно рекурсивный тип данных) для работы на FT (церковное кодирование)

5 голосов
/ 22 декабря 2019

Я использую тип FreeT из библиотеки free , чтобы написать эту функцию, которая "запускает" базовый StateT: 

runStateFree
    :: (Functor f, Monad m)
    => s
    -> FreeT f (StateT s m) a
    -> FreeT f m (a, s)
runStateFree s0 (FreeT x) = FreeT $ do
    flip fmap (runStateT x s0) $ \(r, s1) -> case r of
      Pure y -> Pure (y, s1)
      Free z -> Free (runStateFree s1 <$> z)

ОднакоЯ пытаюсь преобразовать его для работы на FT , церковно-закодированной версии, вместо этого: 

runStateF
    :: (Functor f, Monad m)
    => s
    -> FT f (StateT s m) a
    -> FT f m (a, s)
runStateF s0 (FT x) = FT $ \ka kf -> ...

, но мне не совсем везет. Кажется, что все виды комбинаций вещей не работают. Самое близкое, что я получил, это 

runStateF s0 (FT x) = FT $ \ka kf ->
    ka =<< runStateT (x pure (\n -> _ . kf (_ . n)) s0

Но тип первого отверстия m r -> StateT s m r, а тип второго отверстия StateT s m r -> m r ... что означает, что мы обязательно потеряем состояние в процессе.

Я знаю, что все функции FreeT можно записать с помощью FT. Есть ли хороший способ написать это, который не включает в себя циклическое переключение через FreeT (то есть таким способом, который требует явного соответствия для Pure и Free)? (Я пробовал встраивать вещи вручную, но я не знаю, как справиться с рекурсией, используя разные s s в определении runStateFree). Или, может быть, это один из тех случаев, когда явный рекурсивный тип данных обязательно более производительный, чем кодировка церковной (му)?

Ответы [ 2 ]

1 голос
/ 22 декабря 2019

Вот определение. В самой реализации нет хитростей. Не думай, сделай проверку типа. Да, по крайней мере, одна из этих fmap морально сомнительна, но на самом деле трудность заключается в том, чтобы убедить себя в том, что она поступает правильно. 

runStateF
    :: (Functor f, Monad m)
    => s
    -> FT f (StateT s m) a
    -> FT f m (a, s)
runStateF s0 (FT run) = FT $ \return0 handle0 ->
  let returnS a = StateT (\s -> fmap (\r -> (r, s)) (return0 (a, s)))
      handleS k e = StateT (\s -> fmap (\r -> (r, s)) (handle0 (\x -> evalStateT (k x) s) e))
  in evalStateT (run returnS handleS) s0

У нас есть две функции без сохранения состояния (т. Е. Простая m)

return0 :: a -> m r
handle0 :: forall x. (x -> m r) -> f x -> m r

и мы должны заключить их в два варианта с состоянием (StateT s m) с подписями ниже. Следующие комментарии дают некоторые подробности о том, что происходит в определении handleS. 

returnS :: a -> StateT s m r
handleS :: forall x. (x -> StateT s m r) -> f x -> StateT s m r

-- 1.                                               --    ^   grab the current state 's' here
-- 2.                                               --      ^ call handle0 to produce that 'm'
-- 3.                             ^ here we will have to provide some state 's': pass the current state we just grabbed.
--                                  The idea is that 'handle0' is stateless in handling 'f x',
--                                  so it is fine for this continuation (x -> StateT s m r) to get the state from before the call to 'handle0'

Существует явно сомнительное использование fmap в handleS, но оно действительно до тех пор, покапоскольку run никогда не смотрит на состояния, создаваемые handleS. Он почти сразу же отбрасывается одним из evalStateT.

В теории существуют термины типа FT f (StateT s m) a, которые нарушают этот инвариант. На практике это почти наверняка не происходит;вам бы действительно пришлось приложить все усилия, чтобы сделать что-то морально неправильное с этими продолжениями.

В следующем полном описании я также покажу, как проверить с помощью QuickCheck, что это действительно эквивалентно вашей первоначальной версии с использованием FreeT, с конкретными доказательствами того, что вышеупомянутый инвариант имеет место:

https://gist.github.com/Lysxia/a0afa3ca2ea9e39b400cde25b5012d18

1 голос
/ 22 декабря 2019

Я бы сказал, что нет, поскольку даже что-то столь простое, как cutoff, преобразуется в FreeT: 

cutoff :: (Functor f, Monad m) => Integer -> FT f m a -> FT f m (Maybe a)
cutoff n = toFT . FreeT.cutoff n . fromFT

В общем, вы, вероятно, смотрите на: 

improve :: Functor f => (forall m. MonadFree f m => m a) -> Free f a

Улучшение асимптотической эффективности кода, который создает свободную монаду только с привязками и возвратами, используя закулисную область F.

Т.е. вы эффективно создадите Free, но затем делайте все, что вам нужно, с Free (может быть, снова, с помощью improve ing).

...