{-# 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, swapInner
  )
import Proarrow.Category.Monoidal.Action (MonoidalAction (..), SelfAction, Strong (..), 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 (..))
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 (..))
import Proarrow.Profunctor.Day (Day(..))

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
              )

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 a ~> (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 ~> (w ** b)) -> p (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 ~> (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

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