[resolves agda#1333] writer transformer (agda#1850)

* Writer monad (CPS encoded)

add more instances for writer, change output level in RawMonadError

Co-authored-by: Guillaume Allais <[email protected]>

Author: cmcmA20

CHANGELOG.md

@@ -591,6 +591,15 @@ Non-backwards compatible changes
   This is needed because `MonadState S M` does not pack a `Monad M` instance anymore
   and so we cannot define `modify f` as `get >>= λ s → put (f s)`.
 
+* `MonadWriter 𝕎 M` is defined similarly:
+   ```agda
+   writer : W × A → M A
+   listen : M A → M (W × A)
+   pass   : M ((W → W) × A) → M A
+   ```
+   with `tell` defined as a derived notion.
+   Note that `𝕎` is a `RawMonoid`, not a `Set` and `W` is the carrier of the monoid.
+
 * New modules:
   ```
   Data.List.Effectful.Transformer
@@ -613,6 +622,11 @@ Non-backwards compatible changes
   Effect.Monad.State.Instances
   Effect.Monad.State.Transformer
   Effect.Monad.State.Transformer.Base
+  Effect.Monad.Writer
+  Effect.Monad.Writer.Indexed
+  Effect.Monad.Writer.Instances
+  Effect.Monad.Writer.Transformer
+  Effect.Monad.Writer.Transformer.Base
   IO.Effectful
   IO.Instances
   ```

src/Effect/Monad/Error/Transformer.agda

@@ -21,14 +21,14 @@ private
   variable
     f ℓ : Level
     A B : Set ℓ
-    M : Set f → Set f
+    M : Set f → Set ℓ
 
 ------------------------------------------------------------------------
 -- Error monad operations
 
 record RawMonadError
-       (M : Set (e ⊔ a) → Set (e ⊔ a))
-       : Set (suc (e ⊔ a)) where
+       (M : Set (e ⊔ a) → Set ℓ)
+       : Set (suc (e ⊔ a) ⊔ ℓ) where
   field
     throw : E → M A
     catch : M A → (E → M A) → M A

src/Effect/Monad/IO.agda

@@ -32,7 +32,7 @@ record RawMonadIO
     liftIO : IO A → M A
 
 ------------------------------------------------------------------------
--- Reader monad specifics
+-- IO monad specifics
 
 monadIO : RawMonadIO {f} IO
 monadIO = record { liftIO = id }
@@ -50,3 +50,10 @@ liftReaderT : ∀ {R} → RawMonadIO M → RawMonadIO (ReaderT R M)
 liftReaderT MIO = record
   { liftIO = λ io → mkReaderT (λ r → liftIO io)
   } where open RawMonadIO MIO
+
+open import Effect.Monad.Writer.Transformer.Base using (WriterT; mkWriterT)
+
+liftWriterT : ∀ {f 𝕎} → RawFunctor M → RawMonadIO M → RawMonadIO (WriterT {f = f} 𝕎 M)
+liftWriterT M MIO = record
+  { liftIO = λ io → mkWriterT (λ w → (w ,_) <$> liftIO io)
+  } where open RawFunctor M; open RawMonadIO MIO

src/Effect/Monad/IO/Instances.agda

@@ -14,3 +14,4 @@ instance
   ioMonadIO = monadIO
   stateTMonadIO = λ {s} {S} {M} {{m}} {{mio}} → liftStateT {s} {S} {M} m mio
   readerTMonadIO = λ {r} {R} {M} {{mio}} → liftReaderT  {r} {R} {M} mio
+  writerTMonadIO = λ {f} {w} {W} {M} {{m}} {{mio}} → liftWriterT {f} {w} {W} {M} m mio

src/Effect/Monad/Reader/Instances.agda

@@ -22,6 +22,7 @@ instance
   readerTMonadPlus = λ {s} {S} {f} {M} {{mpl}} → monadPlus {s} {S} {f} {M} mpl
   readerTMonadT = λ {s} {S} {f} {M} {{mon}} → monadT {s} {S} {f} {M} mon
   readerTMonadReader = λ {s} {S} {f} {M} {{mon}} → monadReader {s} {S} {f} {M} mon
-  readerTLiftStateT = λ {s} {S₁} {S₂} {f} {M} {{mon}} {{ms}} → liftStateT {s} {S₁} {S₂} {f} {M} mon ms
+  readerTLiftWriterT = λ {s} {S₁} {S₂} {f} {M} {{mo}} {{fun}} {{mr}} → liftWriterT {s} {S₁} {S₂} {f} {M} mo fun mr
+  readerTLiftStateT = λ {s} {S₁} {S₂} {f} {M} {{fun}} {{mr}} → liftStateT {s} {S₁} {S₂} {f} {M} fun mr
   -- the following instance conflicts with readerTMonadReader so we don't include it
   -- readerTLiftReaderT = λ {R} {s} {S} {f} {M} {{ms}} → liftReaderT {R} {s} {S} {f} {M} ms

src/Effect/Monad/Reader/Transformer.agda

@@ -9,6 +9,7 @@
 
 module Effect.Monad.Reader.Transformer where
 
+open import Algebra using (RawMonoid)
 open import Effect.Choice
 open import Effect.Empty
 open import Effect.Functor
@@ -115,7 +116,19 @@ liftReaderT MRead = record
   ; local = λ f mx → mkReaderT (λ r₂ → local f (runReaderT mx r₂))
   } where open RawMonadReader MRead
 
-open import Data.Product using (_,_)
+open import Data.Product using (_×_; _,_)
+open import Effect.Monad.Writer.Transformer.Base
+
+liftWriterT : (MR : RawMonoid r g) →
+              RawFunctor M →
+              RawMonadReader R M →
+              RawMonadReader R (WriterT MR M)
+liftWriterT MR M MRead = record
+  { reader = λ k → mkWriterT λ w → ((w ,_) <$> reader k)
+  ; local = λ f mx → mkWriterT λ w → (local f (runWriterT mx w))
+  } where open RawMonadReader MRead
+          open RawFunctor M
+
 open import Effect.Monad.State.Transformer.Base
 
 liftStateT : RawFunctor M →

src/Effect/Monad/State/Instances.agda

@@ -22,6 +22,7 @@ instance
   stateTMonadPlus = λ {s} {S} {f} {M} {{mpl}} → monadPlus {s} {S} {f} {M} mpl
   stateTMonadT = λ {s} {S} {f} {M} {{mon}} → monadT {s} {S} {f} {M} mon
   stateTMonadState = λ {s} {S} {f} {M} {{mon}} → monadState {s} {S} {f} {M} mon
-  -- the following instance conflicts with stateTMonadState so we don't include it
-  -- stateTLiftStateT = λ {s} {S₁} {S₂} {f} {M} {{mon}} {{ms}} → liftStateT {s} {S₁} {S₂} {f} {M} mon ms
   stateTLiftReaderT = λ {R} {s} {S} {f} {M} {{ms}} → liftReaderT {R} {s} {S} {f} {M} ms
+  stateTLiftWriterT = λ {R} {s} {S} {f} {M} {{fun}} {{mo}} {{ms}} → liftWriterT {R} {s} {S} {f} {M} mo fun ms
+  -- the following instances conflicts with stateTMonadState so we don't include it
+  -- stateTLiftStateT = λ {s} {S₁} {S₂} {f} {M} {{mon}} {{ms}} → liftStateT {s} {S₁} {S₂} {f} {M} mon ms

src/Effect/Monad/State/Transformer.agda

@@ -10,6 +10,7 @@ open import Level using (Level; suc; _⊔_)
 
 module Effect.Monad.State.Transformer where
 
+open import Algebra using (RawMonoid)
 open import Data.Product using (_×_; _,_; map₂; proj₁; proj₂)
 open import Data.Unit.Polymorphic.Base
 open import Effect.Choice
@@ -136,3 +137,15 @@ liftReaderT Mon = record
   { gets   = λ f → mkReaderT (const (gets f))
   ; modify = λ f → mkReaderT (const (modify f))
   } where open RawMonadState Mon
+
+open import Effect.Monad.Writer.Transformer.Base
+
+liftWriterT : (MS : RawMonoid s f) →
+              RawFunctor M →
+              RawMonadState S M →
+              RawMonadState S (WriterT MS M)
+liftWriterT MS M Mon = record
+  { gets   = λ f → mkWriterT λ w → (gets ((w ,_) ∘′ f))
+  ; modify = λ f → mkWriterT λ w → (const (w , tt) <$> modify f)
+  } where open RawMonadState Mon
+          open RawFunctor M

src/Effect/Monad/Writer.agda

@@ -0,0 +1,62 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- The writer monad
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+module Effect.Monad.Writer where
+
+open import Algebra using (RawMonoid)
+open import Data.Product using (_×_)
+open import Effect.Applicative
+open import Effect.Choice
+open import Effect.Empty
+open import Effect.Functor
+open import Effect.Monad
+open import Effect.Monad.Identity as Id using (Identity; runIdentity)
+open import Function.Base using (_∘′_)
+open import Level using (Level)
+
+import Effect.Monad.Writer.Transformer as Trans
+
+private
+  variable
+    w ℓ : Level
+    A : Set w
+    𝕎 : RawMonoid w ℓ
+
+------------------------------------------------------------------------
+-- Re-export the monad writer operations
+
+open Trans public
+  using (RawMonadWriter)
+
+------------------------------------------------------------------------
+-- Writer monad
+
+Writer : (𝕎 : RawMonoid w ℓ) (A : Set w) → Set w
+Writer 𝕎 = Trans.WriterT 𝕎 Identity
+
+functor : RawFunctor (Writer 𝕎)
+functor = Trans.functor Id.functor
+
+module _ {𝕎 : RawMonoid w ℓ} where
+
+  open RawMonoid 𝕎 renaming (Carrier to W)
+
+  runWriter : Writer 𝕎 A → W × A
+  runWriter ma = runIdentity (Trans.runWriterT ma ε)
+
+  applicative : RawApplicative (Writer 𝕎)
+  applicative = Trans.applicative Id.applicative
+
+  monad : RawMonad (Writer 𝕎)
+  monad = Trans.monad Id.monad
+
+  ----------------------------------------------------------------------
+  -- Writer monad specifics
+
+  monadWriter : RawMonadWriter 𝕎 (Writer 𝕎)
+  monadWriter = Trans.monadWriter Id.monad

src/Effect/Monad/Writer/Indexed.agda

@@ -0,0 +1,122 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- The indexed writer monad
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+open import Level
+
+module Effect.Monad.Writer.Indexed (a : Level) where
+
+open import Algebra using (RawMonoid)
+open import Data.Product using (_×_; _,_; map₁)
+open import Data.Unit.Polymorphic
+open import Effect.Applicative.Indexed
+open import Effect.Monad
+open import Effect.Monad.Indexed
+open import Function
+open import Function.Identity.Effectful as Id using (Identity)
+
+private
+  variable
+    w ℓ : Level
+    A B I : Set ℓ
+
+------------------------------------------------------------------------
+-- Indexed writer
+
+IWriterT : (𝕎 : RawMonoid w ℓ) → IFun I (w ⊔ a) → IFun I (w ⊔ a)
+IWriterT 𝕎 M i j A = M i j (RawMonoid.Carrier 𝕎 × A)
+
+module _ {M : IFun I (w ⊔ a)} {𝕎 : RawMonoid w ℓ} where
+
+  open RawMonoid 𝕎 renaming (Carrier to W)
+
+  ------------------------------------------------------------------------
+  -- Indexed writer applicative
+
+  WriterTIApplicative : RawIApplicative M → RawIApplicative (IWriterT 𝕎 M)
+  WriterTIApplicative App = record
+    { pure = λ x → pure (ε , x)
+    ; _⊛_ = λ m n → go <$> m ⊛ n
+    } where
+        open RawIApplicative App
+        go : W × (A → B) → W × A → W × B
+        go (w₁ , f) (w₂ , x) = w₁ ∙ w₂ , f x
+
+  WriterTIApplicativeZero : RawIApplicativeZero M →
+                            RawIApplicativeZero (IWriterT 𝕎 M)
+  WriterTIApplicativeZero App = record
+    { applicative = WriterTIApplicative applicative
+    ; ∅ = ∅
+    } where open RawIApplicativeZero App
+
+  WriterTIAlternative : RawIAlternative M → RawIAlternative (IWriterT 𝕎 M)
+  WriterTIAlternative Alt = record
+    { applicativeZero = WriterTIApplicativeZero applicativeZero
+    ; _∣_ = _∣_
+    } where open RawIAlternative Alt
+
+  ------------------------------------------------------------------------
+  -- Indexed writer monad
+
+  WriterTIMonad : RawIMonad M → RawIMonad (IWriterT 𝕎 M)
+  WriterTIMonad Mon = record
+    { return = λ x → return (ε , x)
+    ; _>>=_ = λ m f → do
+        w₁ , x  ← m
+        w₂ , fx ← f x
+        return (w₁ ∙ w₂ , fx)
+    } where open RawIMonad Mon
+
+  WriterTIMonadZero : RawIMonadZero M → RawIMonadZero (IWriterT 𝕎 M)
+  WriterTIMonadZero Mon = record
+    { monad = WriterTIMonad monad
+    ; applicativeZero = WriterTIApplicativeZero applicativeZero
+    } where open RawIMonadZero Mon
+
+  WriterTIMonadPlus : RawIMonadPlus M → RawIMonadPlus (IWriterT 𝕎 M)
+  WriterTIMonadPlus Mon = record
+    { monad = WriterTIMonad monad
+    ; alternative = WriterTIAlternative alternative
+    } where open RawIMonadPlus Mon
+
+------------------------------------------------------------------------
+-- Writer monad operations
+
+record RawIMonadWriter {I : Set ℓ} (𝕎 : RawMonoid w ℓ) (M : IFun I (w ⊔ a))
+                       : Set (ℓ ⊔ suc (w ⊔ a)) where
+  open RawMonoid 𝕎 renaming (Carrier to W)
+  field
+    monad  : RawIMonad M
+    writer : ∀ {i} → (W × A) → M i i A
+    listen : ∀ {i j} → M i j A → M i j (W × A)
+    pass   : ∀ {i j} → M i j ((W → W) × A) → M i j A
+
+  open RawIMonad monad public
+
+  tell : ∀ {i} → W → M i i ⊤
+  tell = writer ∘′ (_, tt)
+
+  listens : ∀ {i j} {Z : Set w} → (W → Z) → M i j A → M i j (Z × A)
+  listens f m = listen m >>= return ∘′ map₁ f
+
+  censor : ∀ {i j} → (W → W) → M i j A → M i j A
+  censor f m = pass (m >>= return ∘′ (f ,_))
+
+
+WriterTIMonadWriter : {I : Set ℓ} {𝕎 : RawMonoid w ℓ} {M : IFun I (w ⊔ a)} →
+                      RawIMonad M → RawIMonadWriter 𝕎 (IWriterT 𝕎 M)
+WriterTIMonadWriter {𝕎 = 𝕎} Mon = record
+  { monad = WriterTIMonad {𝕎 = 𝕎} Mon
+  ; writer = return
+  ; listen = λ m → do
+      w , a ← m
+      return (w , w , a)
+  ; pass = λ m → do
+      w , f , a ← m
+      return (f w , a)
+  } where open RawIMonad Mon
+          open RawMonoid 𝕎 renaming (Carrier to W)