我已阅读 the Control.ST
tutorial好几次了,但我仍然不清楚如何使用它来实现我在 Haskell 中使用 monad 变压器的效果。我的具体情况是,我想要具有与 ReaderT r Maybe a 相同功能的东西;具体来说,有以下功能:
ask :: ReaderT r Maybe r
local :: (r -> r') -> ReaderT r Maybe a -> ReaderT r' Maybe a
runReaderT :: ReaderT r Maybe a -> r -> Maybe a
我如何使用Control.ST
(以及其中的内容)来实现这样的东西?
最佳答案
所以首先要做的就是定义一个接口(interface)来描述Reader所管理的资源以及对该资源的原始操作:
interface Reader where
我们为读取资源定义自定义类型,以控制对它们的访问。
Read : Type -> Type
然后我们需要一种方法来引入和删除读取资源:
setRead : a -> ST m Var [add (Read a)]
unsetRead : (env : Var) -> ST m () [remove env (Read a)]
当然,询问
和本地:
ask : (env : Var) -> ST m () [env ::: Read a]
local : (env : Var) -> (f : r -> r') ->
ST m a [env ::: Read r'] ->
ST m a [env ::: Read r]
从那里,我们可以定义 runReaderT
来插入资源,运行依赖于它的计算并删除它:
runReaderT : Reader m =>
((env : Var) -> ST m a [env ::: Read {m} b]) -> b -> ST m a []
runReaderT f x = do
e <- set x
res <- f e
unset e
pure res
我们现在可以依靠State
继续实现:
implementation Reader Maybe where
Read = State
setRead x = do
env <- new x
pure env
unsetRead env = delete env
ask env = read env
local env f st = do
r <- ask env
write env (f r)
x <- st
write env r
pure x
然后,您就可以开始使用它了:
runReader : (Applicative m, Reader m) =>
((env : Var) -> STrans m a [env ::: Read {m} b] (const [env ::: Read {m} b])) ->
b -> m a
runReader f x = run $ runReaderT f x
incrementRead : Reader m => (env : Var) -> ST m Nat [env ::: Read {m} Nat]
incrementRead env = pure $ 1 + !(ask env)
test : Nat -> Maybe Nat
test y = do
x <- run (runReaderT incrementRead y)
guard (x >= 42) *> pure x
希望有帮助。
关于monads - 如何在 Idris 中使用 ST 来获取 ReaderT r Maybe a 的功能?,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/59678105/