我如何在Idris中使用ST来获得ReaderT r可能是a？

Question

我已经读过几次the Control.ST tutorial，但是我仍然不清楚如何使用它来实现在Haskell中使用monad转换器的那种效果。我的具体情况是我想要具有与Control.ST相同功能的东西。具体来说，以下功能：

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

（及其中的内容）实现类似的内容？

Answer 1

因此，要做的第一件事是定义一个接口，以描述由Reader管理的资源以及对该资源的原始操作：

Control.ST

我们为读取资源定义了自定义类型，以控制对它们的访问。

interface Reader where

然后我们需要一种引入和删除阅读资源的方法：

  Read : Type -> Type

当然还有

  setRead   : a -> ST m Var [add (Read a)]
  unsetRead : (env : Var) -> ST m () [remove env (Read a)]

和本地：

ask

从那里，我们可以定义

  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 IO 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

希望有帮助。