monads - 如何在 Idris 中使用 ST 来获得 ReaderT r Maybe a 的功能？

Question

我已阅读 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 (以及里面的东西)来实现这样的东西？

Answer 1

所以首先要做的就是定义一个接口(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和本地:

  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

希望能帮助到你。