{-# LANGUAGE TupleSections #-}

module Proarrow.Promonad.Writer where

import Prelude (($))

import Proarrow.Category.Instance.Prof (Prof (..))
import Proarrow.Category.Monoidal
  ( Monoidal (..)
  , MonoidalProfunctor (..)
  , SymMonoidal (..)
  , first
  , leftUnitorInvWith
  , leftUnitorWith
  , second
  , swap'
  , unitObj
  )
import Proarrow.Category.Monoidal.Action (MonoidalAction (..), SelfAction, Strong (..), actHom, strongPar0)
import Proarrow.Category.Monoidal.Distributive (Traversable (..))
import Proarrow.Core (CategoryOf (..), Profunctor (..), Promonad (..), lmap, obj, tgt, (//), type (+->))
import Proarrow.Functor (Functor (..))
import Proarrow.Monoid (Comonoid, Monoid (..), comultAct, counitAct, mappendAct, memptyAct)
import Proarrow.Object.Dual
  ( CompactClosed (..)
  , ExpSA
  , StarAutonomous (..)
  , combineDual
  , doubleNeg
  , doubleNegInv
  , dualityCounit
  , dualityUnit, expSA
  )
import Proarrow.Profunctor.Composition ((:.:) (..))
import Proarrow.Profunctor.Corepresentable (Corepresentable (..))
import Proarrow.Profunctor.Identity (Id (..))
import Proarrow.Profunctor.Representable (Representable (..), dimapRep)
import Proarrow.Promonad (Procomonad (..))

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

instance (Ob (w :: m), MonoidalAction m 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 ~> Act w b
f = r
(Ob a, Ob b) => r
(Ob a, Ob (Act w b)) => r
r ((Ob a, Ob (Act w b)) => r) -> (a ~> Act 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 ~> Act w b
f

-- | The writer monad given the Promonad instance.
instance (Ob (w :: m), MonoidalAction m k) => Representable (Writer w :: k +-> k) where
  type Writer w % a = Act w a
  index :: forall (a :: k) (b :: k). Writer w a b -> a ~> (Writer w % b)
index (Writer a ~> Act w b
f) = a ~> (Writer w % b)
a ~> Act 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 ~> Act w b) -> Writer w a b
forall {k} {m} (b :: k) (a :: k) (w :: m).
Ob b =>
(a ~> Act w b) -> Writer w a b
Writer a ~> (Writer w % b)
a ~> Act w b
f
  repMap :: forall (a :: k) (b :: k).
(a ~> b) -> (Writer w % a) ~> (Writer w % b)
repMap a ~> b
f = (w ~> w) -> (a ~> b) -> Act w a ~> Act w b
forall m k (a :: m) (b :: m) (x :: k) (y :: k).
MonoidalAction m k =>
(a ~> b) -> (x ~> y) -> Act a x ~> Act b y
actHom (forall (a :: m). (CategoryOf m, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @w) 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 ~> Act 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) ~> Act w b)
-> (Dual w ** Dual (Dual a)) ~> (Dual w ** Act 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 ~> Act w b
f (a ~> Act w b) -> (Dual (Dual a) ~> a) -> Dual (Dual a) ~> Act 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 (Act w b)) => Dual (w ** Dual a) ~> b)
-> (a ~> Act 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 ~> Act 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 ~> Act w b) -> Writer w a b
forall {k} {m} (b :: k) (a :: k) (w :: m).
Ob b =>
(a ~> Act 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))) ~> Act w b)
-> (a ~> (w ** (Dual w ** Dual (Dual a)))) -> a ~> Act 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 (MonoidalAction m k) => Functor (Writer :: m -> k +-> k) where
  map :: forall (a :: m) (b :: m). (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 ~> Act a b
g) -> (a ~> Act b b) -> Writer b a b
forall {k} {m} (b :: k) (a :: k) (w :: m).
Ob b =>
(a ~> Act w b) -> Writer w a b
Writer ((a ~> b) -> (b ~> b) -> Act a b ~> Act b b
forall m k (a :: m) (b :: m) (x :: k) (y :: k).
MonoidalAction m k =>
(a ~> b) -> (x ~> y) -> Act a x ~> Act b y
actHom a ~> b
f (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @b) (Act a b ~> Act b b) -> (a ~> Act a b) -> a ~> Act 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 ~> Act a b
g)

instance (Monoid (w :: m), MonoidalAction m k) => Promonad (Writer w :: k +-> k) where
  id :: forall (a :: k). Ob a => Writer w a a
id = (a ~> Act w a) -> Writer w a a
forall {k} {m} (b :: k) (a :: k) (w :: m).
Ob b =>
(a ~> Act w b) -> Writer w a b
Writer (forall (a :: m) (n :: k).
(MonoidalAction m k, Monoid a, Ob n) =>
n ~> Act a n
forall {m} {c} (a :: m) (n :: c).
(MonoidalAction m c, Monoid a, Ob n) =>
n ~> Act a n
memptyAct @w)
  Writer @c b ~> Act w c
g . :: forall (b :: k) (c :: k) (a :: k).
Writer w b c -> Writer w a b -> Writer w a c
. Writer a ~> Act w b
f = (a ~> Act w c) -> Writer w a c
forall {k} {m} (b :: k) (a :: k) (w :: m).
Ob b =>
(a ~> Act w b) -> Writer w a b
Writer (forall (a :: m) (n :: k).
(MonoidalAction m k, Monoid a, Ob n) =>
Act a (Act a n) ~> Act a n
forall {m} {c} (a :: m) (n :: c).
(MonoidalAction m c, Monoid a, Ob n) =>
Act a (Act a n) ~> Act a n
mappendAct @w @c (Act w (Act w c) ~> Act w c)
-> (a ~> Act w (Act w c)) -> a ~> Act 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
. (w ~> w) -> (b ~> Act w c) -> Act w b ~> Act w (Act w c)
forall m k (a :: m) (b :: m) (x :: k) (y :: k).
MonoidalAction m k =>
(a ~> b) -> (x ~> y) -> Act a x ~> Act b y
actHom (forall (a :: m). (CategoryOf m, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @w) b ~> Act w c
g (Act w b ~> Act w (Act w c))
-> (a ~> Act w b) -> a ~> Act w (Act 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 ~> Act w b
f)

instance (Comonoid (w :: m), MonoidalAction m k) => Procomonad (Writer w :: k +-> k) where
  extract :: Writer w :~> (~>)
extract (Writer a ~> Act w b
f) = forall (a :: m) (n :: k).
(MonoidalAction m k, Comonoid a, Ob n) =>
Act a n ~> n
forall {m} {c} (a :: m) (n :: c).
(MonoidalAction m c, Comonoid a, Ob n) =>
Act a n ~> n
counitAct @w (Act w b ~> b) -> (a ~> Act 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 ~> Act w b
f
  duplicate :: Writer w :~> (Writer w :.: Writer w)
duplicate (Writer @b a ~> Act w b
f) = (a ~> Act w (Act w b)) -> Writer w a (Act w b)
forall {k} {m} (b :: k) (a :: k) (w :: m).
Ob b =>
(a ~> Act w b) -> Writer w a b
Writer (forall (a :: m) (n :: k).
(MonoidalAction m k, Comonoid a, Ob n) =>
Act a n ~> Act a (Act a n)
forall {m} {c} (a :: m) (n :: c).
(MonoidalAction m c, Comonoid a, Ob n) =>
Act a n ~> Act a (Act a n)
comultAct @w @b (Act w b ~> Act w (Act w b))
-> (a ~> Act w b) -> a ~> Act w (Act 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 ~> Act w b
f) Writer w a (Act w b)
-> Writer w (Act 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
:.: (Act w b ~> Act w b) -> Writer w (Act w b) b
forall {k} {m} (b :: k) (a :: k) (w :: m).
Ob b =>
(a ~> Act w b) -> Writer w a b
Writer Act w b ~> Act 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 (Act w b)) => (:.:) (Writer w) (Writer w) a b)
-> (a ~> Act 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 ~> Act w b
f

instance (Ob (w :: m), MonoidalAction m k, SymMonoidal m) => Strong m (Writer w :: k +-> k) where
  act :: forall (a :: m) (b :: m) (x :: k) (y :: k).
(a ~> b) -> Writer w x y -> Writer w (Act a x) (Act b y)
act @a @b @x @y a ~> b
f (Writer x ~> Act w y
g) =
    (Act a x ~> Act w (Act b y)) -> Writer w (Act a x) (Act b y)
forall {k} {m} (b :: k) (a :: k) (w :: m).
Ob b =>
(a ~> Act w b) -> Writer w a b
Writer (forall m k (a :: m) (b :: m) (x :: k).
(MonoidalAction m k, Ob a, Ob b, Ob x) =>
Act (a ** b) x ~> Act a (Act b x)
multiplicatorInv @m @k @w @b @y (Act (w ** b) y ~> Act w (Act b y))
-> (Act a x ~> Act (w ** b) y) -> Act a x ~> Act 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
. ((b ** w) ~> (w ** b))
-> (y ~> y) -> Act (b ** w) y ~> Act (w ** b) y
forall m k (a :: m) (b :: m) (x :: k) (y :: k).
MonoidalAction m k =>
(a ~> b) -> (x ~> y) -> Act a x ~> Act b y
actHom (forall k (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @_ @b @w) (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @y) (Act (b ** w) y ~> Act (w ** b) y)
-> (Act a x ~> Act (b ** w) y) -> Act a x ~> Act (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 m k (a :: m) (b :: m) (x :: k).
(MonoidalAction m k, Ob a, Ob b, Ob x) =>
Act a (Act b x) ~> Act (a ** b) x
multiplicator @m @k @b @w @y (Act b (Act w y) ~> Act (b ** w) y)
-> (Act a x ~> Act b (Act w y)) -> Act a x ~> Act (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) -> (x ~> Act w y) -> Act a x ~> Act b (Act w y)
forall m k (a :: m) (b :: m) (x :: k) (y :: k).
MonoidalAction m k =>
(a ~> b) -> (x ~> y) -> Act a x ~> Act b y
actHom a ~> b
f x ~> Act w y
g)
      ((Ob (Act a x), Ob (Act a x)) => Writer w (Act a x) (Act b y))
-> (Act a x ~> Act a x) -> Writer w (Act a x) (Act b y)
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 ~> a) -> (x ~> x) -> Act a x ~> Act a x
forall m k (a :: m) (b :: m) (x :: k) (y :: k).
MonoidalAction m k =>
(a ~> b) -> (x ~> y) -> Act a x ~> Act b y
actHom (forall (a :: m). (CategoryOf m, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @a) (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @x)
      ((Ob (Act b y), Ob (Act b y)) => Writer w (Act a x) (Act b y))
-> (Act b y ~> Act b y) -> Writer w (Act a x) (Act b y)
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
\\ (b ~> b) -> (y ~> y) -> Act b y ~> Act b y
forall m k (a :: m) (b :: m) (x :: k) (y :: k).
MonoidalAction m k =>
(a ~> b) -> (x ~> y) -> Act a x ~> Act b y
actHom (forall (a :: m). (CategoryOf m, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @b) (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @y)
      ((Ob a, Ob b) => Writer w (Act a x) (Act b y))
-> (a ~> b) -> Writer w (Act a x) (Act b y)
forall (a :: m) (b :: m) 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 ~> b
f
      ((Ob x, Ob (Act w y)) => Writer w (Act a x) (Act b y))
-> (x ~> Act w y) -> Writer w (Act a x) (Act b y)
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
\\ x ~> Act w y
g

-- | Note: This is only premonoidal, not monoidal, unless the monoid is commutative.
instance (Monoid (w :: k), SelfAction 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 ~> Act 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 ~> Act w y2
g =
    x1 ~> Act w x2
f (x1 ~> Act w x2)
-> ((Ob x1, Ob (Act 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 ~> Act w y2
g (y1 ~> Act w y2)
-> ((Ob y1, Ob (Act 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) ~> Act w (x2 ** y2)) -> Writer w (x1 ** y1) (x2 ** y2)
forall {k} {m} (b :: k) (a :: k) (w :: m).
Ob b =>
(a ~> Act 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) ~> Act w (x2 ** y2))
-> ((x1 ** y1) ~> ((w ** x2) ** y2))
-> (x1 ** y1) ~> Act 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 @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 ~> Act w x2) -> (w ~> w) -> (x1 ** w) ~> (w ** Act w x2)
forall {k} (a :: k) (a' :: k) (b :: k) (b' :: k).
SymMonoidal k =>
(a ~> a') -> (b ~> b') -> (a ** b) ~> (b' ** a')
swap' x1 ~> Act 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) ~> (w ** x2))
-> (y2 ~> y2) -> ((x1 ** w) ** y2) ~> ((w ** x2) ** y2)
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 @y2)
                  (((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 ~> Act w y2
g
              )

instance (Monoid (w :: k), SelfAction k) => Traversable (Writer w :: k +-> k) where
  traverse :: forall (p :: k +-> k).
(DistributiveProfunctor p, Strong k p, SelfAction k) =>
(Writer w :.: p) :~> (p :.: Writer w)
traverse (Writer a ~> Act w b
f :.: p b b
p) = let wp :: p (Act w b) (Act w b)
wp = Id w w -> w ~> w
forall k (a :: k) (b :: k). Id a b -> a ~> b
unId (forall (a :: k).
(SelfAction k, Strong k Id, MonoidalProfunctor Id, Ob a) =>
Id a a
forall {k} {p :: CAT k} (a :: k).
(SelfAction k, Strong k p, MonoidalProfunctor p, Ob a) =>
p a a
strongPar0 @w) (w ~> 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 ~> Act w b) -> p (Act w b) (Act w b) -> p a (Act w 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 ~> Act w b
f 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 ~> Act w b) -> Writer w (Act w b) b
forall {k} {m} (b :: k) (a :: k) (w :: m).
Ob b =>
(a ~> Act w b) -> Writer w a b
Writer (p (Act w b) (Act w b) -> Act w b ~> Act w b
forall {k1} {k2} (a :: k2) (b :: k1) (p :: k1 +-> k2).
Profunctor p =>
p a b -> Obj b
tgt 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