------------------------------------------------------------------------
-- The Agda standard library
--
-- Basic type and definition of the reader monad transformer
------------------------------------------------------------------------

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

module Effect.Monad.Reader.Transformer.Base {r} (R : Set r) where

open import Level using (Level; suc; _⊔_)
open import Function.Base using (id)

private
  variable
    g : Level
    A : Set r

------------------------------------------------------------------------
-- Reader monad operations

record RawMonadReader
       (M : Set r → Set g)
       : Set (suc r ⊔ g) where
  field
    reader : (R → A) → M A
    local  : (R → R) → M A → M A

  ask : M R
  ask = reader id

------------------------------------------------------------------------
-- Reader monad transformer

record ReaderT
       (M : Set r → Set g)
       (A : Set r)
       : Set (r ⊔ g) where
  constructor mkReaderT
  field runReaderT : R → M A
open ReaderT public