6

我正在使用免费库中的FreeT类型来编写这个“运行”底层的函数：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（也就是说，以一种需要明确匹配Pureand的方式Free）？（我尝试过手动内联事物，但我不知道如何使用s定义中的不同 s来处理递归runStateFree）。或者这可能是显式递归数据类型必然比教堂（mu）编码更高效的情况之一？

4

2 回答 2

1

我会说不，甚至像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 来提高构建仅使用绑定和返回的自由 monad 的代码的渐近性能。

即，您将Free有效地构建，然后做任何您需要做的事情Free（也许再次，通过improveing）。

于 2019-12-22T04:02:28.350 回答
1

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

我们有两个无状态函数（即 plain 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'

fmapin的使用显然是可疑的handleS，但只要run 从不查看由 生成的状态，它就有效handleS。它几乎立即被其中一个扔掉evalStateT。

理论上，存在FT f (StateT s m) a打破该不变量的类型术语。在实践中，这几乎肯定不会发生。你真的必须不遗余力地在这些延续中做一些道德上的错误。

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

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

于 2019-12-22T20:18:37.783 回答