Как использовать ST в Idris для получения функциональности ReaderT r Может быть? - PullRequest
Новая
       28

Как использовать ST в Idris для получения функциональности ReaderT r Может быть?

2 голосов
/ 10 января 2020

Я прочитал учебник Control.ST несколько раз, но я до сих пор не понимаю, как его использовать для реализации тех эффектов, для которых я бы использовал монадные преобразователи в Haskell. Мой конкретный случай c заключается в том, что я хочу иметь что-то с той же функциональностью, что и 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 (и все в нем) для реализации чего-то подобного?

1 Ответ

2 голосов
/ 17 января 2020

Итак, первое, что нужно сделать, это определить интерфейс для описания ресурса, управляемого 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

Надеюсь, это поможет.

...