Jus*_* L. 6 haskell church-encoding free-monad
我正在使用免费库中的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)
Run Code Online (Sandbox Code Playgroud)
但是,我正在尝试将其转换为适用于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 -> ...
Run Code Online (Sandbox Code Playgroud)
但我的运气不太一样。我得到的各种组合似乎都不太奏效。我得到的最接近的是
runStateF s0 (FT x) = FT $ \ka kf ->
ka =<< runStateT (x pure (\n -> _ . kf (_ . n)) s0
Run Code Online (Sandbox Code Playgroud)
但是第一个孔m r -> StateT s m r的类型是第二个孔的类型StateT s m r -> m r……这意味着我们在此过程中必然会丢失状态。
我知道所有FreeT函数都可以用FT. 有没有一种很好的方法来编写它而不涉及往返FreeT(也就是说,以一种需要显式匹配Pureand 的方式Free)?(我尝试手动内联事物,但我不知道如何s在 的定义中使用不同的s处理递归runStateFree)。或者,这可能是显式递归数据类型必然比教堂 (mu) 编码性能更高的情况之一?
这是定义。实现本身没有任何技巧。不要思考并进行类型检查。是的,至少其中一项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
Run Code Online (Sandbox Code Playgroud)
我们有两个无状态函数(即 plain m)
return0 :: a -> m r
handle0 :: forall x. (x -> m r) -> f x -> m r
Run Code Online (Sandbox Code Playgroud)
我们必须将它们包装在两个有状态 ( 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'
Run Code Online (Sandbox Code Playgroud)
fmapin的用法显然很可疑handleS,但只要run 不查看由 产生的状态,它就是有效的handleS。它几乎立刻就被其中一个扔掉了evalStateT。
理论上,存在FT f (StateT s m) a打破该不变量的类型项。实际上,这几乎肯定不会发生;你真的必须不遗余力地对这些延续做出一些道德上错误的事情。
在下面的完整要点中,我还展示了如何使用 QuickCheck 测试它确实与使用的初始版本等效FreeT,并有具体证据表明上述不变量成立:
https://gist.github.com/Lysxia/a0afa3ca2ea9e39b400cde25b5012d18