Source code on Github
{-# OPTIONS --safe --without-K #-}

module Class.MonadReader where

open import Meta.Prelude

open import Class.Core
open import Class.Functor
open import Class.Applicative
open import Class.Monad
open import Class.MonadError

open MonadError ⦃...⦄

record MonadReader (R : Set ) (M : Type↑)  _ : Monad M  : Setω where
  field
    ask : M R
    local :  {a} {A : Set a}  (R  R)  M A  M A

  reader :  {a} {A : Set a}  (R  A)  M A
  reader f = f <$> ask

open MonadReader ⦃...⦄

ReaderT : (R : Set) (M :  {a}  Set a  Set a)   {a}  Set a  Set a
ReaderT R M A = R  M A

module _ {R : Set} {M :  {a}  Set a  Set a} where

  Functor-ReaderT :  Functor M   Functor (ReaderT R M)
  Functor-ReaderT ._<$>_ f ra r = f <$> ra r

  instance _ = Functor-ReaderT

  Applicative-ReaderT :  Applicative M   Applicative (ReaderT R M)
  Applicative-ReaderT .pure a = const (pure a)
  Applicative-ReaderT ._<*>_ rf ra r = rf r <*> ra r

  instance _ = Applicative-ReaderT

  Monad-ReaderT :  Monad M   Monad (ReaderT R M)
  Monad-ReaderT .return a _ = return a
  Monad-ReaderT ._>>=_ x f r = x r >>= flip f r

  instance _ = Monad-ReaderT

  MonadReader-ReaderT :  _ : Monad M   MonadReader R (ReaderT R M)
  MonadReader-ReaderT .ask r = return r
  MonadReader-ReaderT .local f x = x  f

  MonadError-ReaderT :  {e} {E : Set e}   MonadError E M   MonadError E (ReaderT R M)
  MonadError-ReaderT .error e _ = error e
  MonadError-ReaderT .catch x h r = catch (x r) (flip h r)