Skip to content

Commit 5384fc1

Browse files
cmcmA20cmcmA20
cmcmA20
authored and
cmcmA20
committed
Writer monad
1 parent 7b72307 commit 5384fc1

File tree

9 files changed

+457
-2
lines changed

9 files changed

+457
-2
lines changed

‎src/Effect/Monad/Reader/Instances.agda‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -22,6 +22,7 @@ instance
2222
readerTMonadPlus = λ {s} {S} {f} {M} {{mpl}} → monadPlus {s} {S} {f} {M} mpl
2323
readerTMonadT = λ {s} {S} {f} {M} {{mon}} → monadT {s} {S} {f} {M} mon
2424
readerTMonadReader = λ {s} {S} {f} {M} {{mon}} → monadReader {s} {S} {f} {M} mon
25-
readerTLiftStateT = λ {s} {S₁} {S₂} {f} {M} {{mon}} {{ms}} → liftStateT {s} {S₁} {S₂} {f} {M} mon ms
25+
readerTLiftWriterT = λ {s} {S₁} {S₂} {f} {M} {{mo}} {{fun}} {{mr}} → liftWriterT {s} {S₁} {S₂} {f} {M} {mo} fun mr
26+
readerTLiftStateT = λ {s} {S₁} {S₂} {f} {M} {{fun}} {{mr}} → liftStateT {s} {S₁} {S₂} {f} {M} fun mr
2627
-- the following instance conflicts with readerTMonadReader so we don't include it
2728
-- readerTLiftReaderT = λ {R} {s} {S} {f} {M} {{ms}} → liftReaderT {R} {s} {S} {f} {M} ms

‎src/Effect/Monad/Reader/Transformer.agda‎

Lines changed: 17 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -9,6 +9,7 @@
99

1010
module Effect.Monad.Reader.Transformer where
1111

12+
open import Algebra using (RawMonoid)
1213
open import Effect.Choice
1314
open import Effect.Empty
1415
open import Effect.Functor
@@ -115,7 +116,22 @@ liftReaderT MRead = record
115116
; local = λ f mx → mkReaderT (λ r₂ → local f (runReaderT mx r₂))
116117
} where open RawMonadReader MRead
117118

118-
open import Data.Product using (_,_)
119+
open import Data.Product using (_×_; _,_)
120+
open import Effect.Monad.Writer.Transformer.Base
121+
122+
module _ {MR' : RawMonoid r g} where
123+
124+
open RawMonoid MR' renaming (Carrier to R')
125+
126+
liftWriterT : RawFunctor M →
127+
RawMonadReader R M →
128+
RawMonadReader R (WriterT R' M)
129+
liftWriterT M MRead = record
130+
{ reader = λ k → mkWriterT ((ε ,_) <$> reader k)
131+
; local = λ f mx → mkWriterT (local f (runWriterT mx))
132+
} where open RawMonadReader MRead
133+
open RawFunctor M
134+
119135
open import Effect.Monad.State.Transformer.Base
120136

121137
liftStateT : RawFunctor M →

‎src/Effect/Monad/State/Instances.agda‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -25,3 +25,4 @@ instance
2525
-- the following instance conflicts with stateTMonadState so we don't include it
2626
-- stateTLiftStateT = λ {s} {S₁} {S₂} {f} {M} {{mon}} {{ms}} → liftStateT {s} {S₁} {S₂} {f} {M} mon ms
2727
stateTLiftReaderT = λ {R} {s} {S} {f} {M} {{ms}} → liftReaderT {R} {s} {S} {f} {M} ms
28+
stateTLiftWriterT = λ {R} {s} {S} {f} {M} {{fun}} {{mo}} {{ms}} → liftWriterT {R} {s} {S} {f} {M} {mo} fun ms

‎src/Effect/Monad/State/Transformer.agda‎

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -10,6 +10,7 @@ open import Level using (Level; suc; _⊔_)
1010

1111
module Effect.Monad.State.Transformer where
1212

13+
open import Algebra using (RawMonoid)
1314
open import Data.Product using (_×_; _,_; map₂; proj₁; proj₂)
1415
open import Data.Unit.Polymorphic.Base
1516
open import Effect.Choice
@@ -136,3 +137,18 @@ liftReaderT Mon = record
136137
{ gets = λ f → mkReaderT (const (gets f))
137138
; modify = λ f → mkReaderT (const (modify f))
138139
} where open RawMonadState Mon
140+
141+
open import Effect.Monad.Writer.Transformer.Base
142+
143+
module _ {MS' : RawMonoid s f} where
144+
145+
open RawMonoid MS' renaming (Carrier to S')
146+
147+
liftWriterT : RawFunctor M →
148+
RawMonadState S M →
149+
RawMonadState S (WriterT S' M)
150+
liftWriterT M Mon = record
151+
{ gets = λ f → mkWriterT (gets ((ε ,_) ∘′ f))
152+
; modify = λ f → mkWriterT (const (ε , tt) <$> modify f)
153+
} where open RawMonadState Mon
154+
open RawFunctor M

‎src/Effect/Monad/Writer.agda‎

Lines changed: 64 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,64 @@
1+
------------------------------------------------------------------------
2+
-- The Agda standard library
3+
--
4+
-- The writer monad
5+
------------------------------------------------------------------------
6+
7+
{-# OPTIONS --without-K --safe #-}
8+
9+
module Effect.Monad.Writer where
10+
11+
open import Algebra using (RawMonoid)
12+
open import Data.Product using (_×_)
13+
open import Effect.Applicative
14+
open import Effect.Choice
15+
open import Effect.Empty
16+
open import Effect.Functor
17+
open import Effect.Monad
18+
open import Effect.Monad.Identity as Id using (Identity; runIdentity)
19+
open import Function.Base using (_∘′_)
20+
open import Level using (Level)
21+
22+
import Effect.Monad.Writer.Transformer as Trans
23+
24+
private
25+
variable
26+
w : Level
27+
W A : Set w
28+
29+
------------------------------------------------------------------------
30+
-- Re-export the monad writer operations
31+
32+
open Trans public
33+
using (RawMonadWriter)
34+
35+
------------------------------------------------------------------------
36+
-- Writer monad
37+
38+
Writer : (W A : Set w) → Set w
39+
Writer W = Trans.WriterT W Identity
40+
41+
runWriter : Writer W A → W × A
42+
runWriter = runIdentity ∘′ Trans.runWriterT
43+
44+
------------------------------------------------------------------------
45+
-- Structure
46+
47+
functor : RawFunctor (Writer W)
48+
functor = Trans.functor Id.functor
49+
50+
module _ {MW : RawMonoid w w} where
51+
52+
open RawMonoid MW renaming (Carrier to W')
53+
54+
applicative : RawApplicative (Writer W')
55+
applicative = Trans.applicative {MW = MW} Id.applicative
56+
57+
monad : RawMonad (Writer W')
58+
monad = Trans.monad {MW = MW} Id.monad
59+
60+
------------------------------------------------------------------------
61+
-- Writer monad specifics
62+
63+
monadWriter : RawMonadWriter W (Writer W)
64+
monadWriter = Trans.monadWriter Id.monad

‎src/Effect/Monad/Writer/Indexed.agda‎

Lines changed: 123 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,123 @@
1+
------------------------------------------------------------------------
2+
-- The Agda standard library
3+
--
4+
-- The indexed writer monad
5+
------------------------------------------------------------------------
6+
7+
{-# OPTIONS --without-K --safe #-}
8+
9+
open import Level
10+
11+
module Effect.Monad.Writer.Indexed (a : Level) where
12+
13+
open import Algebra using (RawMonoid)
14+
open import Data.Product using (_×_; _,_; map₁)
15+
open import Data.Unit.Polymorphic
16+
open import Effect.Applicative.Indexed
17+
open import Effect.Monad
18+
open import Effect.Monad.Indexed
19+
open import Function
20+
open import Function.Identity.Effectful as Id using (Identity)
21+
22+
private
23+
variable
24+
w ℓ : Level
25+
A B I : Set ℓ
26+
27+
------------------------------------------------------------------------
28+
-- Indexed writer
29+
30+
IWriterT : Set w → IFun I (w ⊔ a) → IFun I (w ⊔ a)
31+
IWriterT W M i j A = M i j (W × A)
32+
33+
module _ {M : IFun I (w ⊔ a)} {MW' : RawMonoid w ℓ} where
34+
35+
open RawMonoid MW' renaming (Carrier to W')
36+
37+
------------------------------------------------------------------------
38+
-- Indexed writer applicative
39+
40+
WriterTIApplicative : RawIApplicative M → RawIApplicative (IWriterT W' M)
41+
WriterTIApplicative App = record
42+
{ pure = λ x → pure (ε , x)
43+
; _⊛_ = λ m n → go <$> m ⊛ n
44+
} where
45+
open RawIApplicative App
46+
go : W' × (A → B) → W' × A → W' × B
47+
go (w₁ , f) (w₂ , x) = w₁ ∙ w₂ , f x
48+
49+
WriterTIApplicativeZero : RawIApplicativeZero M →
50+
RawIApplicativeZero (IWriterT W' M)
51+
WriterTIApplicativeZero App = record
52+
{ applicative = WriterTIApplicative applicative
53+
; ∅ = ∅
54+
} where open RawIApplicativeZero App
55+
56+
WriterTIAlternative : RawIAlternative M → RawIAlternative (IWriterT W' M)
57+
WriterTIAlternative Alt = record
58+
{ applicativeZero = WriterTIApplicativeZero applicativeZero
59+
; _∣_ = _∣_
60+
} where open RawIAlternative Alt
61+
62+
------------------------------------------------------------------------
63+
-- Indexed writer monad
64+
65+
WriterTIMonad : RawIMonad M → RawIMonad (IWriterT W' M)
66+
WriterTIMonad Mon = record
67+
{ return = λ x → return (ε , x)
68+
; _>>=_ = λ m f → do
69+
w₁ , x ← m
70+
w₂ , fx ← f x
71+
return (w₁ ∙ w₂ , fx)
72+
} where open RawIMonad Mon
73+
74+
WriterTIMonadZero : RawIMonadZero M → RawIMonadZero (IWriterT W' M)
75+
WriterTIMonadZero Mon = record
76+
{ monad = WriterTIMonad monad
77+
; applicativeZero = WriterTIApplicativeZero applicativeZero
78+
} where open RawIMonadZero Mon
79+
80+
WriterTIMonadPlus : RawIMonadPlus M → RawIMonadPlus (IWriterT W' M)
81+
WriterTIMonadPlus Mon = record
82+
{ monad = WriterTIMonad monad
83+
; alternative = WriterTIAlternative alternative
84+
} where open RawIMonadPlus Mon
85+
86+
------------------------------------------------------------------------
87+
-- Writer monad operations
88+
89+
record RawIMonadWriter {I : Set ℓ} (W : Set w) (M : IFun I (w ⊔ a))
90+
: Set (ℓ ⊔ suc (w ⊔ a)) where
91+
field
92+
monad : RawIMonad M
93+
writer : ∀ {i} → (W × A) → M i i A
94+
listen : ∀ {i j} → M i j A → M i j (W × A)
95+
pass : ∀ {i j} → M i j ((W → W) × A) → M i j A
96+
97+
open RawIMonad monad public
98+
99+
tell : ∀ {i} → W → M i i ⊤
100+
tell = writer ∘′ (_, tt)
101+
102+
listens : ∀ {i j} {Z : Set w} → (W → Z) → M i j A → M i j (Z × A)
103+
listens f m = listen m >>= return ∘′ map₁ f
104+
105+
censor : ∀ {i j} → (W → W) → M i j A → M i j A
106+
censor f m = pass (m >>= return ∘′ (f ,_))
107+
108+
module _ {MW' : RawMonoid w ℓ} where
109+
110+
open RawMonoid MW' renaming (Carrier to W')
111+
112+
WriterTIMonadWriter : {I : Set ℓ} {M : IFun I (w ⊔ a)} →
113+
RawIMonad M → RawIMonadWriter W' (IWriterT W' M)
114+
WriterTIMonadWriter Mon = record
115+
{ monad = WriterTIMonad {MW' = MW'} Mon
116+
; writer = return
117+
; listen = λ m → do
118+
w , a ← m
119+
return (w , w , a)
120+
; pass = λ m → do
121+
w , f , a ← m
122+
return (f w , a)
123+
} where open RawIMonad Mon

‎src/Effect/Monad/Writer/Instances.agda‎

Lines changed: 26 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,26 @@
1+
------------------------------------------------------------------------
2+
-- The Agda standard library
3+
--
4+
-- Instances for the writer monad
5+
------------------------------------------------------------------------
6+
7+
{-# OPTIONS --without-K --safe #-}
8+
9+
module Effect.Monad.Writer.Instances where
10+
11+
open import Effect.Monad.Writer.Transformer
12+
13+
instance
14+
writerTFunctor = λ {s} {S} {f} {M} {{fun}} → functor {s} {S} {f} {M} fun
15+
writerTApplicative = λ {s} {S} {f} {M} {{mo}} {{mon}} → applicative {s} {S} {f} {M} {mo} mon
16+
writerTEmpty = λ {s} {S} {f} {M} {{e}} → empty {s} {S} {f} {M} e
17+
writerTChoice = λ {s} {S} {f} {M} {{ch}} → choice {s} {S} {f} {M} ch
18+
writerTApplicativeZero = λ {s} {S} {f} {M} {{mo}} {{mon}} → applicativeZero {s} {S} {f} {M} {mo} mon
19+
writerTAlternative = λ {s} {S} {f} {M} {{mo}} {{mpl}} → alternative {s} {S} {f} {M} {mo} mpl
20+
writerTMonad = λ {s} {S} {f} {M} {{mo}} {{mon}} → monad {s} {S} {f} {M} {mo} mon
21+
writerTMonadZero = λ {s} {S} {f} {M} {{mo}} {{mz}} → monadZero {s} {S} {f} {M} {mo} mz
22+
writerTMonadPlus = λ {s} {S} {f} {M} {{mo}} {{mpl}} → monadPlus {s} {S} {f} {M} {mo} mpl
23+
writerTMonadT = λ {s} {S} {f} {M} {{mo}} {{mon}} → monadT {s} {S} {f} {M} {mo} mon
24+
writerTMonadWriter = λ {s} {S} {f} {M} {{mon}} → monadWriter {s} {S} {f} {M} mon
25+
writerTLiftReaderT = λ {s} {S₁} {S₂} {f} {M} {{fun}} {{mw}} → liftReaderT {s} {S₁} {S₂} {f} {M} fun mw
26+
writerTLiftStateT = λ {s} {S₁} {S₂} {f} {M} {{fun}} {{mw}} → liftStateT {s} {S₁} {S₂} {f} {M} fun mw

0 commit comments

Comments
 (0)