    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- The reader monad
    ------------------------------------------------------------------------

    {-# OPTIONS --cubical-compatible --safe #-}

    module Effect.Monad.Reader where

    open import Effect.Functor using (RawFunctor)
    open import Effect.Applicative using (RawApplicative)
    open import Effect.Monad using (RawMonad; module Join)
    open import Effect.Monad.Identity as Id using (Identity; runIdentity)
    open import Level using (Level)

    import Effect.Monad.Reader.Transformer as Trans

    private
      variable
        r : Level
        R A : Set r

    ------------------------------------------------------------------------
    -- Re-export the monad reader operations

    open Trans public
      using (RawMonadReader)

    ------------------------------------------------------------------------
    -- Reader monad

    Reader : (R A : Set r) → Set r
    Reader R = Trans.ReaderT R Identity

    runReader : Reader R A → R → A
    runReader mr r = runIdentity (Trans.runReaderT mr r)

    ------------------------------------------------------------------------
    -- Structure

    functor : RawFunctor (Reader R)
    functor = Trans.functor Id.functor

    applicative : RawApplicative (Reader R)
    applicative = Trans.applicative Id.applicative

    monad : RawMonad (Reader R)
    monad = Trans.monad Id.monad

    join : Reader R (Reader R A) → Reader R A
    join = Join.join monad

    ------------------------------------------------------------------------
    -- Reader monad specifics

    monadReader : RawMonadReader R (Reader R)
    monadReader = Trans.monadReader Id.monad