
  0 | module Control.Effect.Writer
  1 | 
  2 | import Control.EffectAlgebra
  3 | 
  4 | import Control.Monad.Writer
  5 | 
  6 | ||| Writer effect.
  7 | public export
  8 | data WriterE : Type -> (Type -> Type) -> Type -> Type where
  9 |   Tell : w -> WriterE w m ()
 10 | 
 11 | export
 12 | Functor (\w => WriterE w m a) where
 13 |   map f (Tell x) = Tell (f x)
 14 | 
 15 | ||| Write the value to the context within a monadic computation that supports it.
 16 | public export
 17 | tell : Inj (WriterE w) sig => Algebra sig m => w -> m ()
 18 | tell s = send (Tell s)
 19 | 
 20 | namespace Algebra
 21 |   ||| Successive writes overwrite the preceding state.
 22 |   public export
 23 |   [Overwrite] Algebra sig m => Algebra (WriterE s :+: sig) (WriterT s m) where
 24 |     alg ctx hdl (Inl (Tell s)) = MkWriterT $ \_ => pure (ctx, s)
 25 |     alg ctxx hdl (Inr x) = MkWriterT $ \r => do
 26 |      res <- alg
 27 |        {f = Functor.Compose @{Functor.LeftPair}}
 28 |        (ctxx, r) h x
 29 |      pure res
 30 |      where
 31 |       h : Handler ((,s) . ctx) n m
 32 |       h =
 33 |          (~<~) {g = Functor.LeftPair}
 34 |           {ctx1 = (,s), ctx2 = ctx}
 35 |           {l = n}
 36 |           {m = WriterT s m} {n = m} (uncurry unWriterT) hdl
 37 | 
 38 |   ||| Newer writes are concatenated from the left, via the `Monoid` instance.
 39 |   public export
 40 |   [ConcatLeft] Monoid s => Algebra sig m => Algebra (WriterE s :+: sig) (WriterT s m) where
 41 |     alg ctxx hdl (Inl (Tell s)) = MkWriterT $ \s' => pure (ctxx, (s <+> s'))
 42 |     alg ctxx hdl (Inr x) = MkWriterT $ \r => do
 43 |      -- hdl : Hander ctx n (WriterT s m)
 44 |      -- h : Handler (,s) (WriterT s m) m
 45 |      -- h ~<~ hdl : Handler ((, s) . ctx) n m
 46 |      res <- alg
 47 |        {f = Functor.Compose @{Functor.LeftPair}}
 48 |        (ctxx, r) h x
 49 |      pure res
 50 |      where
 51 |       h : Handler ((,s) . ctx) n m
 52 |       h =
 53 |          (~<~) {g = Functor.LeftPair}
 54 |           {ctx1 = (,s), ctx2 = ctx}
 55 |           {l = n}
 56 |           {m = WriterT s m} {n = m} (uncurry unWriterT) hdl
 57 |