agda-stdlib/src/Effect/Monad/Reader.agda at e95bf760a3b1c9b0aa32784a31e8452578c62187 · jamesmckinna/agda-stdlib · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
------------------------------------------------------------------------
-- The Agda standard library
--
-- The reader monad
------------------------------------------------------------------------

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

open import Level

module Effect.Monad.Reader where

open import Effect.Choice
open import Effect.Empty
open import Effect.Functor
open import Effect.Applicative
open import Effect.Monad
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 where instance _ = monad

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

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