将此 FreeT(显式递归数据类型)函数转换为适用于 FT(教会编码)

Converting this FreeT (explicitly recursive data type) function to work on FT (church encoding)

我正在使用 free 库中的 FreeT 类型来编写此函数,其中 "runs" 一个底层 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 进行往返(即需要在 PureFree 上显式匹配的方式)的好方法? (我尝试过手动内联,但我不知道如何在 runStateFree 的定义中使用不同的 s 来处理递归)。或者这可能是显式递归数据类型必然比 church (mu) 编码更高效的情况之一?

我会说不,即使像 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

Improve the asymptotic performance of code that builds a free monad with only binds and returns by using F behind the scenes.

即您将有效地构建 Free,然后使用 Free 做任何您需要做的事情(也许再次通过 improveing)。

这是定义。实现本身没有技巧。不要考虑并进行类型检查。是的,其中至少有一个 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'

handleSfmap 的用法明显可疑,但只要 run 从不查看 handleS 产生的状态。它几乎立即被 evalStateT.

之一扔掉了

理论上,存在 FT f (StateT s m) a 类型的项可以打破该不变量。实际上,这几乎肯定不会发生。您真的必须竭尽全力为这些延续做一些道德上错误的事情。

在下面的完整要点中,我还展示了如何使用 QuickCheck 测试它确实等同于使用 FreeT 的初始版本,并提供上述不变量成立的具体证据:

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