Agda
Safe HaskellNone
LanguageHaskell2010

Agda.Utils.StrictReader

Synopsis

Documentation

class Monad m => MonadReader r (m :: Type -> Type) | m -> r where #

See examples in Control.Monad.Reader. Note, the partially applied function type (->) r is a simple reader monad. See the instance declaration below.

Minimal complete definition

(ask | reader), local

Methods

ask :: m r #

Retrieves the monad environment.

local #

Arguments

:: (r -> r)

The function to modify the environment.

-> m a

Reader to run in the modified environment.

-> m a 

Executes a computation in a modified environment.

reader #

Arguments

:: (r -> a)

The selector function to apply to the environment.

-> m a 

Retrieves a function of the current environment.

Instances

Instances details
MonadReader NiceEnv Nice Source # 
Instance details

Defined in Agda.Syntax.Concrete.Definitions.Monad

Methods

ask :: Nice NiceEnv #

local :: (NiceEnv -> NiceEnv) -> Nice a -> Nice a #

reader :: (NiceEnv -> a) -> Nice a #

MonadReader e m => MonadReader e (CatchT m) # 
Instance details

Defined in Control.Monad.Catch.Pure

Methods

ask :: CatchT m e #

local :: (e -> e) -> CatchT m a -> CatchT m a #

reader :: (e -> a) -> CatchT m a #

MonadReader r m => MonadReader r (ListT m) Source # 
Instance details

Defined in Agda.Utils.ListT

Methods

ask :: ListT m r #

local :: (r -> r) -> ListT m a -> ListT m a #

reader :: (r -> a) -> ListT m a #

MonadReader r (Reader r) Source # 
Instance details

Defined in Agda.Utils.StrictReader

Methods

ask :: Reader r r #

local :: (r -> r) -> Reader r a -> Reader r a #

reader :: (r -> a) -> Reader r a #

MonadReader r m => MonadReader r (MaybeT m) # 
Instance details

Defined in Control.Monad.Reader.Class

Methods

ask :: MaybeT m r #

local :: (r -> r) -> MaybeT m a -> MaybeT m a #

reader :: (r -> a) -> MaybeT m a #

Monad m => MonadReader r (ReaderT r m) Source # 
Instance details

Defined in Agda.Utils.StrictReader

Methods

ask :: ReaderT r m r #

local :: (r -> r) -> ReaderT r m a -> ReaderT r m a #

reader :: (r -> a) -> ReaderT r m a #

MonadReader r m => MonadReader r (StateT s m) Source # 
Instance details

Defined in Agda.Utils.StrictState

Methods

ask :: StateT s m r #

local :: (r -> r) -> StateT s m a -> StateT s m a #

reader :: (r -> a) -> StateT s m a #

(Monoid w, MonadReader r m) => MonadReader r (AccumT w m) #

Since: mtl-2.3

Instance details

Defined in Control.Monad.Reader.Class

Methods

ask :: AccumT w m r #

local :: (r -> r) -> AccumT w m a -> AccumT w m a #

reader :: (r -> a) -> AccumT w m a #

MonadReader r m => MonadReader r (ExceptT e m) #

Since: mtl-2.2

Instance details

Defined in Control.Monad.Reader.Class

Methods

ask :: ExceptT e m r #

local :: (r -> r) -> ExceptT e m a -> ExceptT e m a #

reader :: (r -> a) -> ExceptT e m a #

MonadReader r m => MonadReader r (IdentityT m) # 
Instance details

Defined in Control.Monad.Reader.Class

Methods

ask :: IdentityT m r #

local :: (r -> r) -> IdentityT m a -> IdentityT m a #

reader :: (r -> a) -> IdentityT m a #

Monad m => MonadReader r (ReaderT r m) # 
Instance details

Defined in Control.Monad.Reader.Class

Methods

ask :: ReaderT r m r #

local :: (r -> r) -> ReaderT r m a -> ReaderT r m a #

reader :: (r -> a) -> ReaderT r m a #

MonadReader r m => MonadReader r (StateT s m) # 
Instance details

Defined in Control.Monad.Reader.Class

Methods

ask :: StateT s m r #

local :: (r -> r) -> StateT s m a -> StateT s m a #

reader :: (r -> a) -> StateT s m a #

MonadReader r m => MonadReader r (StateT s m) # 
Instance details

Defined in Control.Monad.Reader.Class

Methods

ask :: StateT s m r #

local :: (r -> r) -> StateT s m a -> StateT s m a #

reader :: (r -> a) -> StateT s m a #

(Monoid w, MonadReader r m) => MonadReader r (WriterT w m) #

Since: mtl-2.3

Instance details

Defined in Control.Monad.Reader.Class

Methods

ask :: WriterT w m r #

local :: (r -> r) -> WriterT w m a -> WriterT w m a #

reader :: (r -> a) -> WriterT w m a #

(Monoid w, MonadReader r m) => MonadReader r (WriterT w m) # 
Instance details

Defined in Control.Monad.Reader.Class

Methods

ask :: WriterT w m r #

local :: (r -> r) -> WriterT w m a -> WriterT w m a #

reader :: (r -> a) -> WriterT w m a #

(Monoid w, MonadReader r m) => MonadReader r (WriterT w m) # 
Instance details

Defined in Control.Monad.Reader.Class

Methods

ask :: WriterT w m r #

local :: (r -> r) -> WriterT w m a -> WriterT w m a #

reader :: (r -> a) -> WriterT w m a #

MonadReader r' m => MonadReader r' (SelectT r m) #

Since: mtl-2.3

Instance details

Defined in Control.Monad.Reader.Class

Methods

ask :: SelectT r m r' #

local :: (r' -> r') -> SelectT r m a -> SelectT r m a #

reader :: (r' -> a) -> SelectT r m a #

MonadReader r ((->) r) # 
Instance details

Defined in Control.Monad.Reader.Class

Methods

ask :: r -> r #

local :: (r -> r) -> (r -> a) -> r -> a #

reader :: (r -> a) -> r -> a #

MonadReader r' m => MonadReader r' (ContT r m) # 
Instance details

Defined in Control.Monad.Reader.Class

Methods

ask :: ContT r m r' #

local :: (r' -> r') -> ContT r m a -> ContT r m a #

reader :: (r' -> a) -> ContT r m a #

MonadReader r m => MonadReader r (EquivT s c v m) # 
Instance details

Defined in Data.Equivalence.Monad

Methods

ask :: EquivT s c v m r #

local :: (r -> r) -> EquivT s c v m a -> EquivT s c v m a #

reader :: (r -> a) -> EquivT s c v m a #

(Monad m, Monoid w) => MonadReader r (RWST r w s m) #

Since: mtl-2.3

Instance details

Defined in Control.Monad.Reader.Class

Methods

ask :: RWST r w s m r #

local :: (r -> r) -> RWST r w s m a -> RWST r w s m a #

reader :: (r -> a) -> RWST r w s m a #

(Monad m, Monoid w) => MonadReader r (RWST r w s m) # 
Instance details

Defined in Control.Monad.Reader.Class

Methods

ask :: RWST r w s m r #

local :: (r -> r) -> RWST r w s m a -> RWST r w s m a #

reader :: (r -> a) -> RWST r w s m a #

(Monad m, Monoid w) => MonadReader r (RWST r w s m) # 
Instance details

Defined in Control.Monad.Reader.Class

Methods

ask :: RWST r w s m r #

local :: (r -> r) -> RWST r w s m a -> RWST r w s m a #

reader :: (r -> a) -> RWST r w s m a #

newtype Reader r a Source #

Constructors

Reader 

Fields

Instances

Instances details
MonadReader r (Reader r) Source # 
Instance details

Defined in Agda.Utils.StrictReader

Methods

ask :: Reader r r #

local :: (r -> r) -> Reader r a -> Reader r a #

reader :: (r -> a) -> Reader r a #

Applicative (Reader r) Source # 
Instance details

Defined in Agda.Utils.StrictReader

Methods

pure :: a -> Reader r a #

(<*>) :: Reader r (a -> b) -> Reader r a -> Reader r b #

liftA2 :: (a -> b -> c) -> Reader r a -> Reader r b -> Reader r c #

(*>) :: Reader r a -> Reader r b -> Reader r b #

(<*) :: Reader r a -> Reader r b -> Reader r a #

Functor (Reader r) Source # 
Instance details

Defined in Agda.Utils.StrictReader

Methods

fmap :: (a -> b) -> Reader r a -> Reader r b #

(<$) :: a -> Reader r b -> Reader r a #

Monad (Reader r) Source # 
Instance details

Defined in Agda.Utils.StrictReader

Methods

(>>=) :: Reader r a -> (a -> Reader r b) -> Reader r b #

(>>) :: Reader r a -> Reader r b -> Reader r b #

return :: a -> Reader r a #

ExpandCase a => ExpandCase (Reader r a) Source # 
Instance details

Defined in Agda.Utils.StrictReader

Associated Types

type Result (Reader r a) 
Instance details

Defined in Agda.Utils.StrictReader

type Result (Reader r a) = Result a

Methods

expand :: ((Reader r a -> Result (Reader r a)) -> Result (Reader r a)) -> Reader r a Source #

Monoid a => Monoid (Reader r a) Source # 
Instance details

Defined in Agda.Utils.StrictReader

Methods

mempty :: Reader r a #

mappend :: Reader r a -> Reader r a -> Reader r a #

mconcat :: [Reader r a] -> Reader r a #

Semigroup a => Semigroup (Reader r a) Source # 
Instance details

Defined in Agda.Utils.StrictReader

Methods

(<>) :: Reader r a -> Reader r a -> Reader r a #

sconcat :: NonEmpty (Reader r a) -> Reader r a #

stimes :: Integral b => b -> Reader r a -> Reader r a #

type Result (Reader r a) Source # 
Instance details

Defined in Agda.Utils.StrictReader

type Result (Reader r a) = Result a

newtype ReaderT r (m :: Type -> Type) a Source #

Constructors

ReaderT 

Fields

Instances

Instances details
Monad m => MonadReader r (ReaderT r m) Source # 
Instance details

Defined in Agda.Utils.StrictReader

Methods

ask :: ReaderT r m r #

local :: (r -> r) -> ReaderT r m a -> ReaderT r m a #

reader :: (r -> a) -> ReaderT r m a #

MonadState s m => MonadState s (ReaderT r m) Source # 
Instance details

Defined in Agda.Utils.StrictReader

Methods

get :: ReaderT r m s #

put :: s -> ReaderT r m () #

state :: (s -> (a, s)) -> ReaderT r m a #

MonadTransControl (ReaderT r) Source # 
Instance details

Defined in Agda.Utils.StrictReader

Methods

liftWith :: Monad m => (Run (ReaderT r) -> m a) -> ReaderT r m a #

restoreT :: Monad m => m (StT (ReaderT r) a) -> ReaderT r m a #

MonadTrans (ReaderT r) Source # 
Instance details

Defined in Agda.Utils.StrictReader

Methods

lift :: Monad m => m a -> ReaderT r m a #

Monad m => Applicative (ReaderT r m) Source # 
Instance details

Defined in Agda.Utils.StrictReader

Methods

pure :: a -> ReaderT r m a #

(<*>) :: ReaderT r m (a -> b) -> ReaderT r m a -> ReaderT r m b #

liftA2 :: (a -> b -> c) -> ReaderT r m a -> ReaderT r m b -> ReaderT r m c #

(*>) :: ReaderT r m a -> ReaderT r m b -> ReaderT r m b #

(<*) :: ReaderT r m a -> ReaderT r m b -> ReaderT r m a #

Monad m => Functor (ReaderT r m) Source # 
Instance details

Defined in Agda.Utils.StrictReader

Methods

fmap :: (a -> b) -> ReaderT r m a -> ReaderT r m b #

(<$) :: a -> ReaderT r m b -> ReaderT r m a #

Monad m => Monad (ReaderT r m) Source # 
Instance details

Defined in Agda.Utils.StrictReader

Methods

(>>=) :: ReaderT r m a -> (a -> ReaderT r m b) -> ReaderT r m b #

(>>) :: ReaderT r m a -> ReaderT r m b -> ReaderT r m b #

return :: a -> ReaderT r m a #

MonadIO m => MonadIO (ReaderT r m) Source # 
Instance details

Defined in Agda.Utils.StrictReader

Methods

liftIO :: IO a -> ReaderT r m a #

ExpandCase (m a) => ExpandCase (ReaderT r m a) Source # 
Instance details

Defined in Agda.Utils.StrictReader

Associated Types

type Result (ReaderT r m a) 
Instance details

Defined in Agda.Utils.StrictReader

type Result (ReaderT r m a) = Result (m a)

Methods

expand :: ((ReaderT r m a -> Result (ReaderT r m a)) -> Result (ReaderT r m a)) -> ReaderT r m a Source #

(Monoid a, Monad m) => Monoid (ReaderT r m a) Source # 
Instance details

Defined in Agda.Utils.StrictReader

Methods

mempty :: ReaderT r m a #

mappend :: ReaderT r m a -> ReaderT r m a -> ReaderT r m a #

mconcat :: [ReaderT r m a] -> ReaderT r m a #

(Semigroup a, Monad m) => Semigroup (ReaderT r m a) Source # 
Instance details

Defined in Agda.Utils.StrictReader

Methods

(<>) :: ReaderT r m a -> ReaderT r m a -> ReaderT r m a #

sconcat :: NonEmpty (ReaderT r m a) -> ReaderT r m a #

stimes :: Integral b => b -> ReaderT r m a -> ReaderT r m a #

type StT (ReaderT r) a Source # 
Instance details

Defined in Agda.Utils.StrictReader

type StT (ReaderT r) a = a
type Result (ReaderT r m a) Source # 
Instance details

Defined in Agda.Utils.StrictReader

type Result (ReaderT r m a) = Result (m a)

asks #

Arguments

:: MonadReader r m 
=> (r -> a)

The selector function to apply to the environment.

-> m a 

Retrieves a function of the current environment.