{-# LANGUAGE TupleSections #-}

module Proarrow.Promonad.Writer where

import Prelude (($))

import Proarrow.Category.Instance.Nat (Nat (..))
import Proarrow.Category.Instance.Prof (Prof (..))
import Proarrow.Category.Monoidal
  ( Monoidal (..)
  , MonoidalProfunctor (..)
  , SymMonoidal (..)
  , first
  , leftUnitorInvWith
  , leftUnitorWith
  , second
  , swap'
  , swapInner
  , unitObj
  )
import Proarrow.Category.Monoidal.Action (MonoidalAction (..), SelfAction, Strong (..))
import Proarrow.Category.Monoidal.Distributive (Traversable (..))
import Proarrow.Core (CategoryOf (..), Profunctor (..), Promonad (..), lmap, obj, rmap, tgt, (//), (:~>), type (+->))
import Proarrow.Functor (Functor (..))
import Proarrow.Monoid (Comonoid (..), Monoid (..))
import Proarrow.Object.Dual
  ( CompactClosed (..)
  , ExpSA
  , StarAutonomous (..)
  , combineDual
  , doubleNeg
  , doubleNegInv
  , dualityCounit
  , dualityUnit
  , expSA
  )
import Proarrow.Profunctor.Composition (compComp, (:.:) (..))
import Proarrow.Profunctor.Corepresentable (Corepresentable (..))
import Proarrow.Profunctor.Day (Day (..))
import Proarrow.Profunctor.Representable (Representable (..), dimapRep)
import Proarrow.Profunctor.Star (Star, pattern Star)
import Proarrow.Promonad (Procomonad (..))

data Writer w a b where
  Writer :: (Ob b) => a ~> w ** b -> Writer w a b

instance (Ob (w :: k), Monoidal k) => Profunctor (Writer w :: k +-> k) where
  dimap :: forall (c :: k) (a :: k) (b :: k) (d :: k).
(c ~> a) -> (b ~> d) -> Writer w a b -> Writer w c d
dimap = (c ~> a) -> (b ~> d) -> Writer w a b -> Writer w c d
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) (c :: k) (d :: j).
Representable p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimapRep
  (Ob a, Ob b) => r
r \\ :: forall (a :: k) (b :: k) r.
((Ob a, Ob b) => r) -> Writer w a b -> r
\\ Writer a ~> (w ** b)
f = r
(Ob a, Ob b) => r
(Ob a, Ob (w ** b)) => r
r ((Ob a, Ob (w ** b)) => r) -> (a ~> (w ** b)) -> r
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ a ~> (w ** b)
f

-- | The writer monad given the Promonad instance.
instance (Ob (w :: k), Monoidal k) => Representable (Writer w :: k +-> k) where
  type Writer w % a = w ** a
  index :: forall (a :: k) (b :: k). Writer w a b -> a ~> (Writer w % b)
index (Writer a ~> (w ** b)
f) = a ~> (Writer w % b)
a ~> (w ** b)
f
  tabulate :: forall (b :: k) (a :: k).
Ob b =>
(a ~> (Writer w % b)) -> Writer w a b
tabulate a ~> (Writer w % b)
f = (a ~> (w ** b)) -> Writer w a b
forall {k} (b :: k) (a :: k) (w :: k).
Ob b =>
(a ~> (w ** b)) -> Writer w a b
Writer a ~> (Writer w % b)
a ~> (w ** b)
f
  repMap :: forall (a :: k) (b :: k).
(a ~> b) -> (Writer w % a) ~> (Writer w % b)
repMap a ~> b
f = forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @w Obj w -> (a ~> b) -> (w ** a) ~> (w ** b)
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(x1 ~> x2) -> (y1 ~> y2) -> (x1 ** y1) ~> (x2 ** y2)
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
`par` a ~> b
f

-- | The cowriter comonad given the Promonad instance.
instance (Ob (w :: k), SelfAction k, CompactClosed k) => Corepresentable (Writer w :: k +-> k) where
  type Writer w %% a = ExpSA w a
  coindex :: forall (a :: k) (b :: k). Writer w a b -> (Writer w %% a) ~> b
coindex (Writer @b @a a ~> (w ** b)
f) =
    ((Dual w ** w) ~> Unit) -> ((Dual w ** w) ** b) ~> b
forall {k} (a :: k) (b :: k).
(Monoidal k, Ob a) =>
(b ~> Unit) -> (b ** a) ~> a
leftUnitorWith (forall (a :: k). (CompactClosed k, Ob a) => (Dual a ** a) ~> Unit
forall {k} (a :: k).
(CompactClosed k, Ob a) =>
(Dual a ** a) ~> Unit
dualityCounit @w)
      (((Dual w ** w) ** b) ~> b)
-> (Dual (w ** Dual a) ~> ((Dual w ** w) ** b))
-> Dual (w ** Dual a) ~> b
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall k (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
(a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv @k @(Dual w) @w @b
      ((Dual w ** (w ** b)) ~> ((Dual w ** w) ** b))
-> (Dual (w ** Dual a) ~> (Dual w ** (w ** b)))
-> Dual (w ** Dual a) ~> ((Dual w ** w) ** b)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @(Dual w) Obj (Dual w)
-> (Dual (Dual a) ~> (w ** b))
-> (Dual w ** Dual (Dual a)) ~> (Dual w ** (w ** b))
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(x1 ~> x2) -> (y1 ~> y2) -> (x1 ** y1) ~> (x2 ** y2)
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
`par` (a ~> (w ** b)
f (a ~> (w ** b))
-> (Dual (Dual a) ~> a) -> Dual (Dual a) ~> (w ** b)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall (a :: k). (StarAutonomous k, Ob a) => Dual (Dual a) ~> a
forall {k} (a :: k). (StarAutonomous k, Ob a) => Dual (Dual a) ~> a
doubleNeg @a))
      ((Dual w ** Dual (Dual a)) ~> (Dual w ** (w ** b)))
-> (Dual (w ** Dual a) ~> (Dual w ** Dual (Dual a)))
-> Dual (w ** Dual a) ~> (Dual w ** (w ** b))
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall k (a :: k) (b :: k).
(CompactClosed k, Ob a, Ob b) =>
Dual (a ** b) ~> (Dual a ** Dual b)
distribDual @k @w @(Dual a)
      ((Ob a, Ob (w ** b)) => Dual (w ** Dual a) ~> b)
-> (a ~> (w ** b)) -> Dual (w ** Dual a) ~> b
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ a ~> (w ** b)
f
  cotabulate :: forall (a :: k) (b :: k).
Ob a =>
((Writer w %% a) ~> b) -> Writer w a b
cotabulate @a (Writer w %% a) ~> b
f =
    (a ~> (w ** b)) -> Writer w a b
forall {k} (b :: k) (a :: k) (w :: k).
Ob b =>
(a ~> (w ** b)) -> Writer w a b
Writer
      ( (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @w Obj w
-> ((Dual w ** Dual (Dual a)) ~> b)
-> (w ** (Dual w ** Dual (Dual a))) ~> (w ** b)
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(x1 ~> x2) -> (y1 ~> y2) -> (x1 ** y1) ~> (x2 ** y2)
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
`par` ((Writer w %% a) ~> b
Dual (w ** Dual a) ~> b
f (Dual (w ** Dual a) ~> b)
-> ((Dual w ** Dual (Dual a)) ~> Dual (w ** Dual a))
-> (Dual w ** Dual (Dual a)) ~> b
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall (a :: k) (b :: k).
(CompactClosed k, Ob a, Ob b) =>
(Dual a ** Dual b) ~> Dual (a ** b)
forall {k} (a :: k) (b :: k).
(CompactClosed k, Ob a, Ob b) =>
(Dual a ** Dual b) ~> Dual (a ** b)
combineDual @w @(Dual a)))
          ((w ** (Dual w ** Dual (Dual a))) ~> (w ** b))
-> (a ~> (w ** (Dual w ** Dual (Dual a)))) -> a ~> (w ** b)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall k (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator @k @w @(Dual w) @(Dual (Dual a))
          (((w ** Dual w) ** Dual (Dual a))
 ~> (w ** (Dual w ** Dual (Dual a))))
-> (a ~> ((w ** Dual w) ** Dual (Dual a)))
-> a ~> (w ** (Dual w ** Dual (Dual a)))
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (Unit ~> (w ** Dual w))
-> Dual (Dual a) ~> ((w ** Dual w) ** Dual (Dual a))
forall {k} (a :: k) (b :: k).
(Monoidal k, Ob a) =>
(Unit ~> b) -> a ~> (b ** a)
leftUnitorInvWith (forall (a :: k). (CompactClosed k, Ob a) => Unit ~> (a ** Dual a)
forall {k} (a :: k).
(CompactClosed k, Ob a) =>
Unit ~> (a ** Dual a)
dualityUnit @w)
          (Dual (Dual a) ~> ((w ** Dual w) ** Dual (Dual a)))
-> (a ~> Dual (Dual a)) -> a ~> ((w ** Dual w) ** Dual (Dual a))
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall (a :: k). (StarAutonomous k, Ob a) => a ~> Dual (Dual a)
forall {k} (a :: k). (StarAutonomous k, Ob a) => a ~> Dual (Dual a)
doubleNegInv @a
      )
      ((Ob (Dual (w ** Dual a)), Ob b) => Writer w a b)
-> (Dual (w ** Dual a) ~> b) -> Writer w a b
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ (Writer w %% a) ~> b
Dual (w ** Dual a) ~> b
f
  corepMap :: forall (a :: k) (b :: k).
(a ~> b) -> (Writer w %% a) ~> (Writer w %% b)
corepMap a ~> b
f = (a ~> b) -> Obj w -> ExpSA w a ~> ExpSA w b
forall {k} (a :: k) (b :: k) (x :: k) (y :: k).
StarAutonomous k =>
(b ~> y) -> (x ~> a) -> ExpSA a b ~> ExpSA x y
expSA a ~> b
f (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @w)

instance (Monoidal k) => Functor (Writer :: k -> k +-> k) where
  map :: forall (a :: k) (b :: k). (a ~> b) -> Writer a ~> Writer b
map a ~> b
f = a ~> b
f (a ~> b)
-> ((Ob a, Ob b) => Prof (Writer a) (Writer b))
-> Prof (Writer a) (Writer b)
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
// (Writer a :~> Writer b) -> Prof (Writer a) (Writer b)
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \(Writer @b a ~> (a ** b)
g) -> (a ~> (b ** b)) -> Writer b a b
forall {k} (b :: k) (a :: k) (w :: k).
Ob b =>
(a ~> (w ** b)) -> Writer w a b
Writer ((a ~> b
f (a ~> b) -> (b ~> b) -> (a ** b) ~> (b ** b)
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(x1 ~> x2) -> (y1 ~> y2) -> (x1 ** y1) ~> (x2 ** y2)
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
`par` forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @b) ((a ** b) ~> (b ** b)) -> (a ~> (a ** b)) -> a ~> (b ** b)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. a ~> (a ** b)
g)

instance (Monoid (w :: k), Monoidal k) => Promonad (Writer w :: k +-> k) where
  id :: forall (a :: k). Ob a => Writer w a a
id = (a ~> (w ** a)) -> Writer w a a
forall {k} (b :: k) (a :: k) (w :: k).
Ob b =>
(a ~> (w ** b)) -> Writer w a b
Writer ((Unit ~> w) -> a ~> (w ** a)
forall {k} (a :: k) (b :: k).
(Monoidal k, Ob a) =>
(Unit ~> b) -> a ~> (b ** a)
leftUnitorInvWith (forall (m :: k). Monoid m => Unit ~> m
forall {k} (m :: k). Monoid m => Unit ~> m
mempty @w))
  Writer @c b ~> (w ** c)
g . :: forall (b :: k) (c :: k) (a :: k).
Writer w b c -> Writer w a b -> Writer w a c
. Writer a ~> (w ** b)
f = (a ~> (w ** c)) -> Writer w a c
forall {k} (b :: k) (a :: k) (w :: k).
Ob b =>
(a ~> (w ** b)) -> Writer w a b
Writer (forall (c :: k) (a :: k) (b :: k).
(Monoidal k, Ob c) =>
(a ~> b) -> (a ** c) ~> (b ** c)
forall {k} (c :: k) (a :: k) (b :: k).
(Monoidal k, Ob c) =>
(a ~> b) -> (a ** c) ~> (b ** c)
first @c (forall (m :: k). Monoid m => (m ** m) ~> m
forall {k} (m :: k). Monoid m => (m ** m) ~> m
mappend @w) (((w ** w) ** c) ~> (w ** c))
-> (a ~> ((w ** w) ** c)) -> a ~> (w ** c)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall k (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
(a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv @k @w @w @c ((w ** (w ** c)) ~> ((w ** w) ** c))
-> (a ~> (w ** (w ** c))) -> a ~> ((w ** w) ** c)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall (c :: k) (a :: k) (b :: k).
(Monoidal k, Ob c) =>
(a ~> b) -> (c ** a) ~> (c ** b)
forall {k} (c :: k) (a :: k) (b :: k).
(Monoidal k, Ob c) =>
(a ~> b) -> (c ** a) ~> (c ** b)
second @w b ~> (w ** c)
g ((w ** b) ~> (w ** (w ** c)))
-> (a ~> (w ** b)) -> a ~> (w ** (w ** c))
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. a ~> (w ** b)
f)

instance (Comonoid (w :: k), Monoidal k) => Procomonad (Writer w :: k +-> k) where
  extract :: Writer w :~> (~>)
extract (Writer a ~> (w ** b)
f) = (w ~> Unit) -> (w ** b) ~> b
forall {k} (a :: k) (b :: k).
(Monoidal k, Ob a) =>
(b ~> Unit) -> (b ** a) ~> a
leftUnitorWith (forall (c :: k). Comonoid c => c ~> Unit
forall {k} (c :: k). Comonoid c => c ~> Unit
counit @w) ((w ** b) ~> b) -> (a ~> (w ** b)) -> a ~> b
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. a ~> (w ** b)
f
  duplicate :: Writer w :~> (Writer w :.: Writer w)
duplicate (Writer @b a ~> (w ** b)
f) = (a ~> (w ** (w ** b))) -> Writer w a (w ** b)
forall {k} (b :: k) (a :: k) (w :: k).
Ob b =>
(a ~> (w ** b)) -> Writer w a b
Writer (forall k (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator @k @w @w @b (((w ** w) ** b) ~> (w ** (w ** b)))
-> (a ~> ((w ** w) ** b)) -> a ~> (w ** (w ** b))
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall (c :: k) (a :: k) (b :: k).
(Monoidal k, Ob c) =>
(a ~> b) -> (a ** c) ~> (b ** c)
forall {k} (c :: k) (a :: k) (b :: k).
(Monoidal k, Ob c) =>
(a ~> b) -> (a ** c) ~> (b ** c)
first @b (forall (c :: k). Comonoid c => c ~> (c ** c)
forall {k} (c :: k). Comonoid c => c ~> (c ** c)
comult @w) ((w ** b) ~> ((w ** w) ** b))
-> (a ~> (w ** b)) -> a ~> ((w ** w) ** b)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. a ~> (w ** b)
f) Writer w a (w ** b)
-> Writer w (w ** b) b -> (:.:) (Writer w) (Writer w) a b
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: ((w ** b) ~> (w ** b)) -> Writer w (w ** b) b
forall {k} (b :: k) (a :: k) (w :: k).
Ob b =>
(a ~> (w ** b)) -> Writer w a b
Writer (w ** b) ~> (w ** b)
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id ((Ob a, Ob (w ** b)) => (:.:) (Writer w) (Writer w) a b)
-> (a ~> (w ** b)) -> (:.:) (Writer w) (Writer w) a b
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ a ~> (w ** b)
f

instance (Ob (w :: k), SelfAction k) => Strong k (Writer w :: k +-> k) where
  act :: forall (a :: k) (b :: k) (x :: k) (y :: k).
(a ~> b) -> Writer w x y -> Writer w (Act a x) (Act b y)
act @_ @b @_ @y a ~> b
f (Writer x ~> (w ** y)
g) =
    a ~> b
f (a ~> b)
-> ((Ob a, Ob b) => Writer w (Act a x) (Act b y))
-> Writer w (Act a x) (Act b y)
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
//
      forall m k (a :: m) (x :: k) r.
(MonoidalAction m k, Ob a, Ob x) =>
(Ob (Act a x) => r) -> r
withObAct @k @k @b @y ((Ob (Act b y) => Writer w (Act a x) (Act b y))
 -> Writer w (Act a x) (Act b y))
-> (Ob (Act b y) => Writer w (Act a x) (Act b y))
-> Writer w (Act a x) (Act b y)
forall a b. (a -> b) -> a -> b
$
        (Act a x ~> (w ** Act b y)) -> Writer w (Act a x) (Act b y)
forall {k} (b :: k) (a :: k) (w :: k).
Ob b =>
(a ~> (w ** b)) -> Writer w a b
Writer (forall k (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator @k @w @b @y (((w ** b) ** y) ~> (w ** Act b y))
-> (Act a x ~> ((w ** b) ** y)) -> Act a x ~> (w ** Act b y)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall (c :: k) (a :: k) (b :: k).
(Monoidal k, Ob c) =>
(a ~> b) -> (a ** c) ~> (b ** c)
forall {k} (c :: k) (a :: k) (b :: k).
(Monoidal k, Ob c) =>
(a ~> b) -> (a ** c) ~> (b ** c)
first @y (forall k (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @_ @b @w) (((b ** w) ** y) ~> ((w ** b) ** y))
-> (Act a x ~> ((b ** w) ** y)) -> Act a x ~> ((w ** b) ** y)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall k (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
(a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv @k @b @w @y ((b ** (w ** y)) ~> ((b ** w) ** y))
-> (Act a x ~> (b ** (w ** y))) -> Act a x ~> ((b ** w) ** y)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (a ~> b
f (a ~> b) -> (x ~> (w ** y)) -> (a ** x) ~> (b ** (w ** y))
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(x1 ~> x2) -> (y1 ~> y2) -> (x1 ** y1) ~> (x2 ** y2)
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
`par` x ~> (w ** y)
g))

-- | Note: This is only premonoidal, not monoidal, unless the monoid is commutative.
instance (Monoid (w :: k), SymMonoidal k) => MonoidalProfunctor (Writer w :: k +-> k) where
  par0 :: Writer w Unit Unit
par0 = Writer w Unit Unit
(Ob Unit, Ob Unit) => Writer w Unit Unit
forall (a :: k). Ob a => Writer w a a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id ((Ob Unit, Ob Unit) => Writer w Unit Unit)
-> (Unit ~> Unit) -> Writer w Unit Unit
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ forall k. Monoidal k => Obj Unit
unitObj @k
  Writer @x2 @x1 x1 ~> (w ** x2)
f par :: forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
Writer w x1 x2 -> Writer w y1 y2 -> Writer w (x1 ** y1) (x2 ** y2)
`par` Writer @y2 @y1 y1 ~> (w ** y2)
g =
    x1 ~> (w ** x2)
f (x1 ~> (w ** x2))
-> ((Ob x1, Ob (w ** x2)) => Writer w (x1 ** y1) (x2 ** y2))
-> Writer w (x1 ** y1) (x2 ** y2)
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
//
      y1 ~> (w ** y2)
g (y1 ~> (w ** y2))
-> ((Ob y1, Ob (w ** y2)) => Writer w (x1 ** y1) (x2 ** y2))
-> Writer w (x1 ** y1) (x2 ** y2)
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
//
        forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @x1 @y1 ((Ob (x1 ** y1) => Writer w (x1 ** y1) (x2 ** y2))
 -> Writer w (x1 ** y1) (x2 ** y2))
-> (Ob (x1 ** y1) => Writer w (x1 ** y1) (x2 ** y2))
-> Writer w (x1 ** y1) (x2 ** y2)
forall a b. (a -> b) -> a -> b
$
          forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @x2 @y2 ((Ob (x2 ** y2) => Writer w (x1 ** y1) (x2 ** y2))
 -> Writer w (x1 ** y1) (x2 ** y2))
-> (Ob (x2 ** y2) => Writer w (x1 ** y1) (x2 ** y2))
-> Writer w (x1 ** y1) (x2 ** y2)
forall a b. (a -> b) -> a -> b
$
            ((x1 ** y1) ~> (w ** (x2 ** y2))) -> Writer w (x1 ** y1) (x2 ** y2)
forall {k} (b :: k) (a :: k) (w :: k).
Ob b =>
(a ~> (w ** b)) -> Writer w a b
Writer
              ( forall k (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator @k @w @x2 @y2
                  (((w ** x2) ** y2) ~> (w ** (x2 ** y2)))
-> ((x1 ** y1) ~> ((w ** x2) ** y2))
-> (x1 ** y1) ~> (w ** (x2 ** y2))
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall (c :: k) (a :: k) (b :: k).
(Monoidal k, Ob c) =>
(a ~> b) -> (a ** c) ~> (b ** c)
forall {k} (c :: k) (a :: k) (b :: k).
(Monoidal k, Ob c) =>
(a ~> b) -> (a ** c) ~> (b ** c)
first @y2 (forall (c :: k) (a :: k) (b :: k).
(Monoidal k, Ob c) =>
(a ~> b) -> (a ** c) ~> (b ** c)
forall {k} (c :: k) (a :: k) (b :: k).
(Monoidal k, Ob c) =>
(a ~> b) -> (a ** c) ~> (b ** c)
first @x2 (forall (m :: k). Monoid m => (m ** m) ~> m
forall {k} (m :: k). Monoid m => (m ** m) ~> m
mappend @w) (((w ** w) ** x2) ~> (w ** x2))
-> ((x1 ** w) ~> ((w ** w) ** x2)) -> (x1 ** w) ~> (w ** x2)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall k (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
(a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv @k @w @w @x2 ((w ** (w ** x2)) ~> ((w ** w) ** x2))
-> ((x1 ** w) ~> (w ** (w ** x2))) -> (x1 ** w) ~> ((w ** w) ** x2)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (x1 ~> (w ** x2)) -> (w ~> w) -> (x1 ** w) ~> (w ** (w ** x2))
forall {k} (a :: k) (a' :: k) (b :: k) (b' :: k).
SymMonoidal k =>
(a ~> a') -> (b ~> b') -> (a ** b) ~> (b' ** a')
swap' x1 ~> (w ** x2)
f (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @w))
                  (((x1 ** w) ** y2) ~> ((w ** x2) ** y2))
-> ((x1 ** y1) ~> ((x1 ** w) ** y2))
-> (x1 ** y1) ~> ((w ** x2) ** y2)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall k (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
(a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv @k @x1 @w @y2
                  ((x1 ** (w ** y2)) ~> ((x1 ** w) ** y2))
-> ((x1 ** y1) ~> (x1 ** (w ** y2)))
-> (x1 ** y1) ~> ((x1 ** w) ** y2)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall (c :: k) (a :: k) (b :: k).
(Monoidal k, Ob c) =>
(a ~> b) -> (c ** a) ~> (c ** b)
forall {k} (c :: k) (a :: k) (b :: k).
(Monoidal k, Ob c) =>
(a ~> b) -> (c ** a) ~> (c ** b)
second @x1 y1 ~> (w ** y2)
g
              )

-- | A version of traverse specialized to `Writer`, with fewer requirements on @p@.
traverseWriter :: forall {k} p (w :: k). (Strong k p, SelfAction k, Ob w) => Writer w :.: p :~> p :.: Writer w
traverseWriter :: forall {k} (p :: k +-> k) (w :: k).
(Strong k p, SelfAction k, Ob w) =>
(Writer w :.: p) :~> (p :.: Writer w)
traverseWriter (Writer a ~> (w ** b)
f :.: p b b
p) = let wp :: p (Act w b) (Act w b)
wp = forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @w Obj w -> p b b -> p (Act w b) (Act w b)
forall (a :: k) (b :: k) (x :: k) (y :: k).
(a ~> b) -> p x y -> p (Act a x) (Act b y)
forall {c} {d} m (p :: c +-> d) (a :: m) (b :: m) (x :: d)
       (y :: c).
Strong m p =>
(a ~> b) -> p x y -> p (Act a x) (Act b y)
`act` p b b
p in (a ~> (w ** b)) -> p (w ** b) (Act w b) -> p a (Act w b)
forall (c :: k) (a :: k) (b :: k). (c ~> a) -> p a b -> p c b
forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j).
Profunctor p =>
(c ~> a) -> p a b -> p c b
lmap a ~> (w ** b)
f p (w ** b) (Act w b)
p (Act w b) (Act w b)
wp p a (Act w b) -> Writer w (Act w b) b -> (:.:) p (Writer w) a b
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: (Act w b ~> (w ** b)) -> Writer w (Act w b) b
forall {k} (b :: k) (a :: k) (w :: k).
Ob b =>
(a ~> (w ** b)) -> Writer w a b
Writer (p (Act w b) (w ** b) -> Obj (w ** b)
forall {k1} {k2} (a :: k2) (b :: k1) (p :: k1 +-> k2).
Profunctor p =>
p a b -> Obj b
tgt p (Act w b) (w ** b)
p (Act w b) (Act w b)
wp) ((Ob (Act w b), Ob (Act w b)) => (:.:) p (Writer w) a b)
-> p (Act w b) (Act w b) -> (:.:) p (Writer w) a b
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> p a b -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ p (Act w b) (Act w b)
wp ((Ob b, Ob b) => (:.:) p (Writer w) a b)
-> p b b -> (:.:) p (Writer w) a b
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> p a b -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ p b b
p

instance (Monoid (w :: k), Monoidal k) => Traversable (Writer w :: k +-> k) where
  traverse :: forall (p :: k +-> k).
StrongDistributiveProfunctor p =>
(Writer w :.: p) :~> (p :.: Writer w)
traverse = (:.:) (Writer w) p a b -> (:.:) p (Writer w) a b
(Writer w :.: p) :~> (p :.: Writer w)
forall {k} (p :: k +-> k) (w :: k).
(Strong k p, SelfAction k, Ob w) =>
(Writer w :.: p) :~> (p :.: Writer w)
traverseWriter

-- Writer is not Cotraversable

writerComp :: forall {k} (r :: k) (s :: k). (SymMonoidal k, Ob r, Ob s) => Writer r :.: Writer s ~> Writer (r ** s)
writerComp :: forall {k} (r :: k) (s :: k).
(SymMonoidal k, Ob r, Ob s) =>
(Writer r :.: Writer s) ~> Writer (r ** s)
writerComp = forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @k @r @s ((Ob (r ** s) => (Writer r :.: Writer s) ~> Writer (r ** s))
 -> (Writer r :.: Writer s) ~> Writer (r ** s))
-> (Ob (r ** s) => (Writer r :.: Writer s) ~> Writer (r ** s))
-> (Writer r :.: Writer s) ~> Writer (r ** s)
forall a b. (a -> b) -> a -> b
$
  ((Writer r :.: Writer s) :~> Writer (r ** s))
-> Prof (Writer r :.: Writer s) (Writer (r ** s))
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \(Writer a ~> (r ** b)
f :.: Writer @b b ~> (s ** b)
g) -> (a ~> ((r ** s) ** b)) -> Writer (r ** s) a b
forall {k} (b :: k) (a :: k) (w :: k).
Ob b =>
(a ~> (w ** b)) -> Writer w a b
Writer (forall k (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
(a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv @k @r @s @b ((r ** (s ** b)) ~> ((r ** s) ** b))
-> (a ~> (r ** (s ** b))) -> a ~> ((r ** s) ** b)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall (c :: k) (a :: k) (b :: k).
(Monoidal k, Ob c) =>
(a ~> b) -> (c ** a) ~> (c ** b)
forall {k} (c :: k) (a :: k) (b :: k).
(Monoidal k, Ob c) =>
(a ~> b) -> (c ** a) ~> (c ** b)
second @r b ~> (s ** b)
g ((r ** b) ~> (r ** (s ** b)))
-> (a ~> (r ** b)) -> a ~> (r ** (s ** b))
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. a ~> (r ** b)
f)

writerDay :: forall {k} (r :: k) (s :: k). (SymMonoidal k, Ob r, Ob s) => Writer r `Day` Writer s ~> Writer (r ** s)
writerDay :: forall {k} (r :: k) (s :: k).
(SymMonoidal k, Ob r, Ob s) =>
Day (Writer r) (Writer s) ~> Writer (r ** s)
writerDay = forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @k @r @s ((Ob (r ** s) => Day (Writer r) (Writer s) ~> Writer (r ** s))
 -> Day (Writer r) (Writer s) ~> Writer (r ** s))
-> (Ob (r ** s) => Day (Writer r) (Writer s) ~> Writer (r ** s))
-> Day (Writer r) (Writer s) ~> Writer (r ** s)
forall a b. (a -> b) -> a -> b
$
  (Day (Writer r) (Writer s) :~> Writer (r ** s))
-> Prof (Day (Writer r) (Writer s)) (Writer (r ** s))
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \(Day @_ @d @_ @f a ~> (c ** e)
f (Writer c ~> (r ** d)
p) (Writer e ~> (s ** f)
q) (d ** f) ~> b
g) -> (a ~> ((r ** s) ** b)) -> Writer (r ** s) a b
forall {k} (b :: k) (a :: k) (w :: k).
Ob b =>
(a ~> (w ** b)) -> Writer w a b
Writer (forall (c :: k) (a :: k) (b :: k).
(Monoidal k, Ob c) =>
(a ~> b) -> (c ** a) ~> (c ** b)
forall {k} (c :: k) (a :: k) (b :: k).
(Monoidal k, Ob c) =>
(a ~> b) -> (c ** a) ~> (c ** b)
second @(r ** s) (d ** f) ~> b
g (((r ** s) ** (d ** f)) ~> ((r ** s) ** b))
-> (a ~> ((r ** s) ** (d ** f))) -> a ~> ((r ** s) ** b)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall (a :: k) (b :: k) (c :: k) (d :: k).
(SymMonoidal k, Ob a, Ob b, Ob c, Ob d) =>
((a ** b) ** (c ** d)) ~> ((a ** c) ** (b ** d))
forall {k} (a :: k) (b :: k) (c :: k) (d :: k).
(SymMonoidal k, Ob a, Ob b, Ob c, Ob d) =>
((a ** b) ** (c ** d)) ~> ((a ** c) ** (b ** d))
swapInner @r @d @s @f (((r ** d) ** (s ** f)) ~> ((r ** s) ** (d ** f)))
-> (a ~> ((r ** d) ** (s ** f))) -> a ~> ((r ** s) ** (d ** f))
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (c ~> (r ** d)
p (c ~> (r ** d))
-> (e ~> (s ** f)) -> (c ** e) ~> ((r ** d) ** (s ** f))
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(x1 ~> x2) -> (y1 ~> y2) -> (x1 ** y1) ~> (x2 ** y2)
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
`par` e ~> (s ** f)
q) ((c ** e) ~> ((r ** d) ** (s ** f)))
-> (a ~> (c ** e)) -> a ~> ((r ** d) ** (s ** f))
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. a ~> (c ** e)
f) ((Ob (d ** f), Ob b) => Writer (r ** s) a b)
-> ((d ** f) ~> b) -> Writer (r ** s) a b
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ (d ** f) ~> b
g

type WriterT :: k -> k +-> k -> k +-> k
newtype WriterT w p a b where
  WriterT :: (p :.: Writer w) a b -> WriterT w p a b

runWriterT :: (Profunctor p) => WriterT w p a b -> p a (w ** b)
runWriterT :: forall {k} (p :: k +-> k) (w :: k) (a :: k) (b :: k).
Profunctor p =>
WriterT w p a b -> p a (w ** b)
runWriterT (WriterT (p a b
p :.: Writer b ~> (w ** b)
f)) = (b ~> (w ** b)) -> p a b -> p a (w ** b)
forall (b :: k) (d :: k) (a :: k). (b ~> d) -> p a b -> p a d
forall {j} {k} (p :: j +-> k) (b :: j) (d :: j) (a :: k).
Profunctor p =>
(b ~> d) -> p a b -> p a d
rmap b ~> (w ** b)
f p a b
p

tell :: (Promonad p, Monoidal k, Ob (w :: k)) => WriterT w p w Unit
tell :: forall k (p :: k +-> k) (w :: k).
(Promonad p, Monoidal k, Ob w) =>
WriterT w p w Unit
tell = (:.:) p (Writer w) w Unit -> WriterT w p w Unit
forall {i} (p :: i +-> i) (w :: i) (a :: i) (b :: i).
(:.:) p (Writer w) a b -> WriterT w p a b
WriterT (p w w
forall (a :: k). Ob a => p a a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id p w w -> Writer w w Unit -> (:.:) p (Writer w) w Unit
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: (w ~> (w ** Unit)) -> Writer w w Unit
forall {k} (b :: k) (a :: k) (w :: k).
Ob b =>
(a ~> (w ** b)) -> Writer w a b
Writer w ~> (w ** Unit)
forall (a :: k). Ob a => a ~> (a ** Unit)
forall k (a :: k). (Monoidal k, Ob a) => a ~> (a ** Unit)
rightUnitorInv)

listen :: forall {k} p w a b. (Promonad p, Monoidal k, Comonoid (w :: k)) => WriterT w p a b -> WriterT w p a (w ** b)
listen :: forall {k} (p :: k +-> k) (w :: k) (a :: k) (b :: k).
(Promonad p, Monoidal k, Comonoid w) =>
WriterT w p a b -> WriterT w p a (w ** b)
listen (WriterT (p a b
p :.: Writer b ~> (w ** b)
f)) = forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @k @w @b ((Ob (w ** b) => WriterT w p a (w ** b)) -> WriterT w p a (w ** b))
-> (Ob (w ** b) => WriterT w p a (w ** b))
-> WriterT w p a (w ** b)
forall a b. (a -> b) -> a -> b
$ (:.:) p (Writer w) a (w ** b) -> WriterT w p a (w ** b)
forall {i} (p :: i +-> i) (w :: i) (a :: i) (b :: i).
(:.:) p (Writer w) a b -> WriterT w p a b
WriterT (p a b
p p a b -> Writer w b (w ** b) -> (:.:) p (Writer w) a (w ** b)
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: (b ~> (w ** (w ** b))) -> Writer w b (w ** b)
forall {k} (b :: k) (a :: k) (w :: k).
Ob b =>
(a ~> (w ** b)) -> Writer w a b
Writer (forall k (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator @k @w @w @b (((w ** w) ** b) ~> (w ** (w ** b)))
-> (b ~> ((w ** w) ** b)) -> b ~> (w ** (w ** b))
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall (c :: k) (a :: k) (b :: k).
(Monoidal k, Ob c) =>
(a ~> b) -> (a ** c) ~> (b ** c)
forall {k} (c :: k) (a :: k) (b :: k).
(Monoidal k, Ob c) =>
(a ~> b) -> (a ** c) ~> (b ** c)
first @b (forall (c :: k). Comonoid c => c ~> (c ** c)
forall {k} (c :: k). Comonoid c => c ~> (c ** c)
comult @w) ((w ** b) ~> ((w ** w) ** b))
-> (b ~> (w ** b)) -> b ~> ((w ** w) ** b)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. b ~> (w ** b)
f))

censor :: forall {k} p w a b. (Monoidal k, Ob (w :: k)) => w ~> w -> WriterT w p a b -> WriterT w p a b
censor :: forall {k} (p :: k +-> k) (w :: k) (a :: k) (b :: k).
(Monoidal k, Ob w) =>
(w ~> w) -> WriterT w p a b -> WriterT w p a b
censor w ~> w
f (WriterT (p a b
p :.: Writer b ~> (w ** b)
w)) = (:.:) p (Writer w) a b -> WriterT w p a b
forall {i} (p :: i +-> i) (w :: i) (a :: i) (b :: i).
(:.:) p (Writer w) a b -> WriterT w p a b
WriterT (p a b
p p a b -> Writer w b b -> (:.:) p (Writer w) a b
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: (b ~> (w ** b)) -> Writer w b b
forall {k} (b :: k) (a :: k) (w :: k).
Ob b =>
(a ~> (w ** b)) -> Writer w a b
Writer (forall (c :: k) (a :: k) (b :: k).
(Monoidal k, Ob c) =>
(a ~> b) -> (a ** c) ~> (b ** c)
forall {k} (c :: k) (a :: k) (b :: k).
(Monoidal k, Ob c) =>
(a ~> b) -> (a ** c) ~> (b ** c)
first @b w ~> w
f ((w ** b) ~> (w ** b)) -> (b ~> (w ** b)) -> b ~> (w ** b)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. b ~> (w ** b)
w))

deriving newtype instance (Profunctor p, Monoidal k, Ob (w :: k)) => Profunctor (WriterT w p)
deriving newtype instance (Representable p, Ob (w :: k), Monoidal k) => Representable (WriterT w p)
deriving newtype instance
  (Corepresentable p, Ob (w :: k), SelfAction k, CompactClosed k) => Corepresentable (WriterT w p)
deriving newtype instance (Strong k p, Ob (w :: k), SelfAction k) => Strong k (WriterT w p)
deriving newtype instance
  (MonoidalProfunctor p, Monoid (w :: k), SelfAction k, SymMonoidal k) => MonoidalProfunctor (WriterT w p)
deriving newtype instance (Traversable p, Monoid (w :: k), SelfAction k) => Traversable (WriterT w p)

instance (Monoidal k, Ob w) => Functor (WriterT w :: k +-> k -> k +-> k) where
  map :: forall (a :: k +-> k) (b :: k +-> k).
(a ~> b) -> WriterT w a ~> WriterT w b
map n :: a ~> b
n@Prof{} = (WriterT w a :~> WriterT w b) -> Prof (WriterT w a) (WriterT w b)
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \(WriterT (:.:) a (Writer w) a b
p) -> (:.:) b (Writer w) a b -> WriterT w b a b
forall {i} (p :: i +-> i) (w :: i) (a :: i) (b :: i).
(:.:) p (Writer w) a b -> WriterT w p a b
WriterT (Prof (a :.: Writer w) (b :.: Writer w)
-> (a :.: Writer w) :~> (b :.: Writer w)
forall {k1} {k} (p :: k1 +-> k) (q :: k1 +-> k).
Prof p q -> p :~> q
unProf (Nat ((:.:) a) ((:.:) b) -> (:.:) a .~> (:.:) b
forall {k} {k1} (f :: k -> k1) (g :: k -> k1). Nat f g -> f .~> g
unNat ((a ~> b) -> (:.:) a ~> (:.:) b
forall {k1} {k2} (f :: k1 -> k2) (a :: k1) (b :: k1).
Functor f =>
(a ~> b) -> f a ~> f b
forall (a :: k +-> k) (b :: k +-> k).
(a ~> b) -> (:.:) a ~> (:.:) b
map a ~> b
n)) (:.:) a (Writer w) a b
p)

instance (Monoidal k) => Functor (WriterT :: k -> k +-> k -> k +-> k) where
  map :: forall (a :: k) (b :: k). (a ~> b) -> WriterT a ~> WriterT b
map a ~> b
f = a ~> b
f (a ~> b)
-> ((Ob a, Ob b) => Nat (WriterT a) (WriterT b))
-> Nat (WriterT a) (WriterT b)
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
// (WriterT a .~> WriterT b) -> Nat (WriterT a) (WriterT b)
forall {j} {k} (f :: j -> k) (g :: j -> k).
(Functor f, Functor g) =>
(f .~> g) -> Nat f g
Nat ((WriterT a .~> WriterT b) -> Nat (WriterT a) (WriterT b))
-> (WriterT a .~> WriterT b) -> Nat (WriterT a) (WriterT b)
forall a b. (a -> b) -> a -> b
$ (WriterT a a :~> WriterT b a) -> Prof (WriterT a a) (WriterT b a)
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \(WriterT (:.:) a (Writer a) a b
p) -> (:.:) a (Writer b) a b -> WriterT b a a b
forall {i} (p :: i +-> i) (w :: i) (a :: i) (b :: i).
(:.:) p (Writer w) a b -> WriterT w p a b
WriterT (Prof (a :.: Writer a) (a :.: Writer b)
-> (a :.: Writer a) :~> (a :.: Writer b)
forall {k1} {k} (p :: k1 +-> k) (q :: k1 +-> k).
Prof p q -> p :~> q
unProf ((Writer a ~> Writer b) -> (a :.: Writer a) ~> (a :.: Writer b)
forall {k1} {k2} (f :: k1 -> k2) (a :: k1) (b :: k1).
Functor f =>
(a ~> b) -> f a ~> f b
forall (a :: k +-> k) (b :: k +-> k).
(a ~> b) -> (a :.: a) ~> (a :.: b)
map ((a ~> b) -> Writer a ~> Writer b
forall (a :: k) (b :: k). (a ~> b) -> Writer a ~> Writer b
forall {k1} {k2} (f :: k1 -> k2) (a :: k1) (b :: k1).
Functor f =>
(a ~> b) -> f a ~> f b
map a ~> b
f)) (:.:) a (Writer a) a b
p)

instance (Monoid (w :: k), SelfAction k, Strong k p, Promonad p) => Promonad (WriterT w p) where
  id :: forall (a :: k). Ob a => WriterT w p a a
id = (:.:) p (Writer w) a a -> WriterT w p a a
forall {i} (p :: i +-> i) (w :: i) (a :: i) (b :: i).
(:.:) p (Writer w) a b -> WriterT w p a b
WriterT (p a a
forall (a :: k). Ob a => p a a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id p a a -> Writer w a a -> (:.:) p (Writer w) a a
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: Writer w a a
forall (a :: k). Ob a => Writer w a a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id)
  WriterT (:.:) p (Writer w) b c
l . :: forall (b :: k) (c :: k) (a :: k).
WriterT w p b c -> WriterT w p a b -> WriterT w p a c
. WriterT (:.:) p (Writer w) a b
r = (:.:) p (Writer w) a c -> WriterT w p a c
forall {i} (p :: i +-> i) (w :: i) (a :: i) (b :: i).
(:.:) p (Writer w) a b -> WriterT w p a b
WriterT (((Writer w :.: p) :~> (p :.: Writer w))
-> (:.:) p (Writer w) b c
-> (:.:) p (Writer w) a b
-> (:.:) p (Writer w) a c
forall {i} (p :: i +-> i) (q :: i +-> i) (b :: i) (c :: i)
       (a :: i).
(Promonad p, Promonad q) =>
((q :.: p) :~> (p :.: q))
-> (:.:) p q b c -> (:.:) p q a b -> (:.:) p q a c
compComp (:.:) (Writer w) p a b -> (:.:) p (Writer w) a b
(Writer w :.: p) :~> (p :.: Writer w)
forall {k} (p :: k +-> k) (w :: k).
(Strong k p, SelfAction k, Ob w) =>
(Writer w :.: p) :~> (p :.: Writer w)
traverseWriter (:.:) p (Writer w) b c
l (:.:) p (Writer w) a b
r)

-- | WriterT is a monad on profunctors, i.e. we have @p ~> WriterT p@ and @WriterT (WriterT p) ~> WriterT p@.
instance (Monoid w, Monoidal k) => Promonad (Star (WriterT w :: k +-> k -> k +-> k)) where
  id :: forall (a :: k +-> k). Ob a => Star (WriterT w) a a
id = (a ~> WriterT w a) -> Star (WriterT w) a a
forall {j} {k} (b :: j) (a :: k) (f :: j -> k).
Ob b =>
(a ~> f b) -> Star f a b
Star ((a ~> WriterT w a) -> Star (WriterT w) a a)
-> (a ~> WriterT w a) -> Star (WriterT w) a a
forall a b. (a -> b) -> a -> b
$ (a :~> WriterT w a) -> Prof a (WriterT w a)
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \a a b
p -> (:.:) a (Writer w) a b -> WriterT w a a b
forall {i} (p :: i +-> i) (w :: i) (a :: i) (b :: i).
(:.:) p (Writer w) a b -> WriterT w p a b
WriterT (a a b
p a a b -> Writer w b b -> (:.:) a (Writer w) a b
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: Writer w b b
forall (a :: k). Ob a => Writer w a a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id) ((Ob a, Ob b) => WriterT w a a b) -> a a b -> WriterT w a a b
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> a a b -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ a a b
p
  Star b ~> WriterT w c
l . :: forall (b :: k +-> k) (c :: k +-> k) (a :: k +-> k).
Star (WriterT w) b c
-> Star (WriterT w) a b -> Star (WriterT w) a c
. Star a ~> WriterT w b
r = (a ~> WriterT w c) -> Star (WriterT w) a c
forall {j} {k} (b :: j) (a :: k) (f :: j -> k).
Ob b =>
(a ~> f b) -> Star f a b
Star ((a ~> WriterT w c) -> Star (WriterT w) a c)
-> (a ~> WriterT w c) -> Star (WriterT w) a c
forall a b. (a -> b) -> a -> b
$ (WriterT w (WriterT w c) :~> WriterT w c)
-> Prof (WriterT w (WriterT w c)) (WriterT w c)
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof (\(WriterT (WriterT (c a b
p :.: Writer w b b
f) :.: Writer w b b
g)) -> (:.:) c (Writer w) a b -> WriterT w c a b
forall {i} (p :: i +-> i) (w :: i) (a :: i) (b :: i).
(:.:) p (Writer w) a b -> WriterT w p a b
WriterT (c a b
p c a b -> Writer w b b -> (:.:) c (Writer w) a b
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: (Writer w b b
g Writer w b b -> Writer w b b -> Writer w b b
forall (b :: k) (c :: k) (a :: k).
Writer w b c -> Writer w a b -> Writer w a c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. Writer w b b
f))) (WriterT w (WriterT w c) ~> WriterT w c)
-> (a ~> WriterT w (WriterT w c)) -> a ~> WriterT w c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
forall (b :: k +-> k) (c :: k +-> k) (a :: k +-> k).
(b ~> c) -> (a ~> b) -> a ~> c
. (b ~> WriterT w c) -> WriterT w b ~> WriterT w (WriterT w c)
forall {k1} {k2} (f :: k1 -> k2) (a :: k1) (b :: k1).
Functor f =>
(a ~> b) -> f a ~> f b
forall (a :: k +-> k) (b :: k +-> k).
(a ~> b) -> WriterT w a ~> WriterT w b
map b ~> WriterT w c
l Prof (WriterT w b) (WriterT w (WriterT w c))
-> Prof a (WriterT w b) -> Prof a (WriterT w (WriterT w c))
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
forall (b :: k +-> k) (c :: k +-> k) (a :: k +-> k).
Prof b c -> Prof a b -> Prof a c
. a ~> WriterT w b
Prof a (WriterT w b)
r