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

This reverts commit f7bfeba.

Author: jamesmckinna

CHANGELOG.md

@@ -591,15 +591,6 @@ 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
@@ -622,11 +613,6 @@ 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 ℓ
+    M : Set f → Set f
 
 ------------------------------------------------------------------------
 -- Error monad operations
 
 record RawMonadError
-       (M : Set (e ⊔ a) → Set ℓ)
-       : Set (suc (e ⊔ a) ⊔ ℓ) where
+       (M : Set (e ⊔ a) → Set (e ⊔ a))
+       : 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
 
 ------------------------------------------------------------------------
--- IO monad specifics
+-- Reader monad specifics
 
 monadIO : RawMonadIO {f} IO
 monadIO = record { liftIO = id }
@@ -50,10 +50,3 @@ 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,4 +14,3 @@ 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,7 +22,6 @@ 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
-  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
+  readerTLiftStateT = λ {s} {S₁} {S₂} {f} {M} {{mon}} {{ms}} → liftStateT {s} {S₁} {S₂} {f} {M} mon ms
   -- 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,7 +9,6 @@
 
 module Effect.Monad.Reader.Transformer where
 
-open import Algebra using (RawMonoid)
 open import Effect.Choice
 open import Effect.Empty
 open import Effect.Functor
@@ -116,19 +115,7 @@ liftReaderT MRead = record
   ; local = λ f mx → mkReaderT (λ r₂ → local f (runReaderT mx r₂))
   } where open RawMonadReader MRead
 
-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 Data.Product using (_,_)
 open import Effect.Monad.State.Transformer.Base
 
 liftStateT : RawFunctor M →

src/Effect/Monad/State/Instances.agda

@@ -22,7 +22,6 @@ 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
-  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
+  -- 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

src/Effect/Monad/State/Transformer.agda

@@ -10,7 +10,6 @@ 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
@@ -137,15 +136,3 @@ 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