如何在Idris中使用ST来获得ReaderT的功能?也许是a？

module Main

import Control.ST

-- 定义环境类型
record Env where
  constructor MkEnv
  envValue : Int

-- 定义状态类型
record State where
  constructor MkState
  stateValue : Int

-- 获取环境值
getEnvValue : ST (Env, State) Int
getEnvValue = do
  (env, _) <- get
  pure env.envValue

-- 使用环境值更新状态
updateStateWithEnv : ST (Env, State) ()
updateStateWithEnv = do
  (env, st) <- get
  let newState = st { stateValue = st.stateValue + env.envValue }
  put (env, newState)

-- 运行 ST 操作
runSTWithEnv : Env -> State -> (Int, State)
runSTWithEnv env st = runST (env, st) $ do
  val <- getEnvValue
  updateStateWithEnv
  (_, newState) <- get
  pure (val, newState)

-- 示例
main : IO ()
main = do
  let env = MkEnv 10
  let st = MkState 5
  let (envVal, newState) = runSTWithEnv(env, st)
  putStrLn $ "Environment Value: " ++ show envVal
  putStrLn $ "New State Value: " ++ show newState.stateValue