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

【问题标题】：How do I use ST in Idris to get the functionality of ReaderT r Maybe a?如何在 Idris 中使用 ST 来获得 ReaderT r Maybe a 的功能？
【发布时间】：2020-01-10 08:41:25
【问题描述】：

我已经读过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（以及其中的东西）来实现这样的东西？

【问题讨论】：

标签： monads idris

【解决方案1】：

所以首先要做的就是定义一个接口来描述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

希望对你有帮助。

【讨论】：