[resolves #1333] writer transformer

[cmcmA20]

I'm aware of Data.Sum.Effectful.* but it didn't help me much, I have no idea how to properly organize all the stuff about ExceptT reusing those modules.

I'm also asking for tips about improving the current code. First of all I couldn't come up with a really indexed construction for ExceptT because short-circuiting computations mess with the indices. Exceptions can be modeled with Effect.Monad.Continuation but is it a good definition for stdlib? Also there's no standard definition of categories in this library so indexed writer as in Bob Atkey's paper is out of reach.

[gallais]

Note that we now have: http://agda.github.io/agda-stdlib/Effect.Monad.Error.Transformer.html

[cmcmA20]

Very good! I think your changes subsume my ExceptT version, so I'm withdrawing it. Take a look at the updated Writer though.

[gallais]

Looks good!

My main concern is that this gives a blessed implementation

record WriterT
       (M : Set w → Set g)
       (A : Set w)
       : Set (w ⊔ g) where
  constructor mkWriterT
  field runWriterT : M (W × A)

but there are other valid ones, including the CPS-based (cf. this thread for instance)

record WriterT
      (M : Set w → Set g)
      (A : Set w)
      : Set (w ⊔ g) where
 constructor mkWriterT
 field runWriterT : W → M (W × A)

Should we have two modules, one with each implementation?
Maybe in Effect.Monad.Writer.Transformer.FirstOrder vs. Effect.Monad.Writer.Transformer.CPS?

[gallais]

Should WriterT be the CPS-based one? Because the other one is the left-product transformer
(just like we have it for Sum).

[cmcmA20]

Thanks for the link! Looks like the naive version is not that useful from the performance perspective.

I agree with making WriterT default implementation CPS-based, let the other one be in Data.Product.Effectful. Maybe you should also add a comment about it being direct but impractical for programming?

[cmcmA20]

agda-stdlib/src/Effect/Monad/Error/Transformer.agda

Lines 29 to 31 in 7b72307

	record RawMonadError
	(M : Set (e ⊔ a) → Set (e ⊔ a))
	: Set (suc (e ⊔ a)) where

There was no chance of using it with RawMonadIO which bumps the level.

[cmcmA20]

This error shows up in the monad/fibonacci test:

———— Errors ————————————————————————————————————————————————
Failed to solve the following constraints:
  Resolve instance argument
    _r_79 : RawMonadState Fib (λ v → _M_161 v)
  Candidates
    stateTMonadState :
      {s S : Agda.Primitive.Level} {f : Set s → Set S} {M : Set s}
      ⦃ mon : RawMonad f ⦄ →
      RawMonadState M (Effect.Monad.State.Transformer.Base.StateT M f)
    stateTLiftWriterT :
      {R s S : Agda.Primitive.Level} {f : Set R → Set S} {M : Set R}
      ⦃ fun : Effect.Functor.RawFunctor f ⦄
      ⦃ mo : Algebra.Bundles.Raw.RawMonoid R s ⦄
      ⦃ ms : RawMonadState M f ⦄ →
      RawMonadState M
      (Effect.Monad.Writer.Transformer.Base.WriterT
       (Algebra.Bundles.Raw.RawMonoid.Carrier mo) f)
    (stuck)

Bad naming of level variables aside, the error is not illuminating at all. I think it's the same problem as with stateTLiftStateT instance. What's your plan on this?

I doubt Writer is useful in this form without the corresponding lifts. Should I abandon this PR or convert it to draft?

[MatthewDaggitt]

@gallais do you have any more comments?

[gallais]

I think I may have found the source of the error.

[MatthewDaggitt]

@gallais are you happy for this to be merged?

[MatthewDaggitt]

Ah sorry @cmcmA20, one last thing! Please could add an entry in the CHANGELOG about the new modules you've added?

Then I promise this is merging in 👍

[cmcmA20]

Sorry I forgot about the changelog, fixed now.

[MatthewDaggitt]

Great. Merging now. Thanks again for the great first PR!

[jamesmckinna]

I think I have to apologise profusely to all involved with this PR. I think my reverted commits in sorting out the parity-bis (now deleted!) branch/PR #1894 seem to have undone the effect of PR #1850... But I honestly don't understand how this has happened, nor how (best) to fix it.

[MatthewDaggitt]

No worries, it's my fault for not checking the PR properly before hitting merge. I'll fix it with a revert

[MatthewDaggitt]

Done. @jamesmckinna could you reopen a clean parity semiring PR please? 👍 (but it might be at the end of the week... deadline/etc. crunch this week...)

[jamesmckinna]

OK, checked out a clean branch parity-clean
EDITED (but maybe from the wrong base?), but the associated PR doesn't look right in terms of the diffs... please advise... invalidated one PR, submitted a fresh one. Sigh/:facepalm: