
  0 | module Control.Effect.Reader
  1 | 
  2 | import Control.EffectAlgebra
  3 | 
  4 | import Control.Monad.Reader
  5 | 
  6 | ||| Reader effect.
  7 | public export
  8 | data ReaderE : Type -> (Type -> Type) -> Type -> Type where
  9 |   Ask : ReaderE r m r
 10 | 
 11 | export
 12 | Functor (\r => ReaderE r m r) where
 13 |   map _ Ask = Ask
 14 | 
 15 | ||| Read the value within a monadic context that supports it.
 16 | public export
 17 | ask : Inj (ReaderE r) sig => Algebra sig m => m r
 18 | ask = send Ask
 19 | 
 20 | namespace Algebra
 21 |   ||| Apply the reader effect of the signature to the underlying monad,
 22 |   ||| resulting in the ReaderT transformer.
 23 |   public export
 24 |   [Reader] (al : Algebra sig m) => Algebra (ReaderE s :+: sig) (ReaderT s m) where
 25 |     alg ctx hdl (Inl Ask) = MkReaderT $ \s => pure (s <$ ctx)
 26 |     alg ctx hdl (Inr x) = MkReaderT $ \r => alg ctx (runReaderT r . hdl) x
 27 | 
 28 |   %hint public export
 29 |   HintReader : (al : Algebra sig m) => Algebra (ReaderE s :+: sig) (ReaderT s m)
 30 |   HintReader = Reader
 31 |