How do I use ST in Idris to get the functionality of ReaderT r Maybe a?

I've read the Control.ST tutorial several times, but I am still not clear on how to use it to implement the kind of effects I would use monad transformers for in Haskell. My specific case is that I want to have something with the same functionality as ReaderT r Maybe a; specifically, the following functions:

ask :: ReaderT r Maybe r
local :: (r -> r') -> ReaderT r Maybe a -> ReaderT r' Maybe a
runReaderT :: ReaderT r Maybe a -> r -> Maybe a

How can I use Control.ST (and the stuff in it) to implement something like this?

Solution

So the first thing to do is to define an interface to describe the resource managed by the Reader and primitive operations on this resource:

interface Reader where

We define a custom type for read resources, to control access to them.

  Read : Type -> Type

We then need a way to introduce and remove read resources:

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

And of course, ask and local:

  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]

From there, we can define runReaderT that insert the resource, run a computation that depends on it and delete it:

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

We can now move on to the implementation, relying on 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

And then, you're ready to play with it:

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

Hope it helps.