{-# LANGUAGE TupleSections #-}

module Proarrow.Promonad.Writer where

import Proarrow.Category.Monoidal (Monoidal (..), MonoidalProfunctor (..), leftUnitorInvWith, obj2)
import Proarrow.Core (CategoryOf (..), Profunctor (..), Promonad (..), obj, type (+->))
import Proarrow.Helper.CCC
import Proarrow.Monoid (Monoid (..))
import Proarrow.Object.BinaryProduct (HasBinaryProducts (..), associatorProd, associatorProdInv, diag, second)
import Proarrow.Object.Exponential (BiCCC)
import Proarrow.Profunctor.Composition ((:.:) (..))
import Proarrow.Promonad (Procomonad (..))

data Writer m a b where
  Writer :: (Ob a, Ob b) => a ~> m && b -> Writer m a b

instance (BiCCC k, Ob m) => Profunctor (Writer m :: k +-> k) where
  dimap :: forall (c :: k) (a :: k) (b :: k) (d :: k).
(c ~> a) -> (b ~> d) -> Writer m a b -> Writer m c d
dimap c ~> a
l b ~> d
r (Writer a ~> (m && b)
f) = (c ~> (m && d)) -> Writer m c d
forall {k} (a :: k) (b :: k) (m :: k).
(Ob a, Ob b) =>
(a ~> (m && b)) -> Writer m a b
Writer (forall (c :: k) (a :: k) (b :: k).
(HasBinaryProducts k, Ob c) =>
(a ~> b) -> (c && a) ~> (c && b)
forall {k} (c :: k) (a :: k) (b :: k).
(HasBinaryProducts k, Ob c) =>
(a ~> b) -> (c && a) ~> (c && b)
second @m b ~> d
r ((m && b) ~> (m && d)) -> (c ~> (m && b)) -> c ~> (m && d)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. a ~> (m && b)
f (a ~> (m && b)) -> (c ~> a) -> c ~> (m && b)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. c ~> a
l) ((Ob b, Ob d) => Writer m c d) -> (b ~> d) -> Writer m c d
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ b ~> d
r ((Ob c, Ob a) => Writer m c d) -> (c ~> a) -> Writer m c d
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ c ~> a
l
  (Ob a, Ob b) => r
r \\ :: forall (a :: k) (b :: k) r.
((Ob a, Ob b) => r) -> Writer m a b -> r
\\ Writer a ~> (m && b)
f = r
(Ob a, Ob b) => r
(Ob a, Ob (m && b)) => r
r ((Ob a, Ob (m && b)) => r) -> (a ~> (m && b)) -> r
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ a ~> (m && b)
f

instance (BiCCC k, Monoid m) => Promonad (Writer m :: k +-> k) where
  id :: forall (a :: k). Ob a => Writer m a a
id = (a ~> (m && a)) -> Writer m a a
forall {k} (a :: k) (b :: k) (m :: k).
(Ob a, Ob b) =>
(a ~> (m && b)) -> Writer m a b
Writer ((Unit ~> m) -> a ~> (m ** 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 @m))
  Writer @_ @c b ~> (m && c)
g . :: forall (b :: k) (c :: k) (a :: k).
Writer m b c -> Writer m a b -> Writer m a c
. Writer a ~> (m && b)
f = (a ~> (m && c)) -> Writer m a c
forall {k} (a :: k) (b :: k) (m :: k).
(Ob a, Ob b) =>
(a ~> (m && b)) -> Writer m a b
Writer ((((m ** m) ~> m
(m && m) ~> m
forall {k} (m :: k). Monoid m => (m ** m) ~> m
mappend :: m && m ~> m) ((m && m) ~> m) -> (c ~> c) -> ((m && m) && c) ~> (m && c)
forall (a :: k) (b :: k) (x :: k) (y :: k).
(a ~> x) -> (b ~> y) -> (a && b) ~> (x && y)
forall k (a :: k) (b :: k) (x :: k) (y :: k).
HasBinaryProducts k =>
(a ~> x) -> (b ~> y) -> (a && b) ~> (x && y)
*** forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @c) (((m && m) && c) ~> (m && c))
-> (a ~> ((m && m) && c)) -> a ~> (m && c)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO 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).
(HasProducts k, Ob a, Ob b, Ob c) =>
(a && (b && c)) ~> ((a && b) && c)
forall {k} (a :: k) (b :: k) (c :: k).
(HasProducts k, Ob a, Ob b, Ob c) =>
(a && (b && c)) ~> ((a && b) && c)
associatorProdInv @m @m @c ((m && (m && c)) ~> ((m && m) && c))
-> (a ~> (m && (m && c))) -> a ~> ((m && m) && c)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO 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 @m Obj m -> (b ~> (m && c)) -> (m && b) ~> (m && (m && c))
forall (a :: k) (b :: k) (x :: k) (y :: k).
(a ~> x) -> (b ~> y) -> (a && b) ~> (x && y)
forall k (a :: k) (b :: k) (x :: k) (y :: k).
HasBinaryProducts k =>
(a ~> x) -> (b ~> y) -> (a && b) ~> (x && y)
*** b ~> (m && c)
g) ((m && b) ~> (m && (m && c)))
-> (a ~> (m && b)) -> a ~> (m && (m && c))
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. a ~> (m && b)
f)

instance (BiCCC k, Ob m) => Procomonad (Writer m :: k +-> k) where
  extract :: Writer m :~> (~>)
extract (Writer a ~> (m && b)
f) = forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> b
snd @_ @m ((m && b) ~> b) -> (a ~> (m && b)) -> a ~> b
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. a ~> (m && b)
f
  duplicate :: Writer m :~> (Writer m :.: Writer m)
duplicate (Writer @_ @b a ~> (m && b)
f) = (a ~> (m && (m && b))) -> Writer m a (m && b)
forall {k} (a :: k) (b :: k) (m :: k).
(Ob a, Ob b) =>
(a ~> (m && b)) -> Writer m a b
Writer (forall (a :: k) (b :: k) (c :: k).
(HasProducts k, Ob a, Ob b, Ob c) =>
((a && b) && c) ~> (a && (b && c))
forall {k} (a :: k) (b :: k) (c :: k).
(HasProducts k, Ob a, Ob b, Ob c) =>
((a && b) && c) ~> (a && (b && c))
associatorProd @m @m @b (((m && m) && b) ~> (m && (m && b)))
-> (a ~> ((m && m) && b)) -> a ~> (m && (m && b))
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (forall (a :: k). (HasBinaryProducts k, Ob a) => a ~> (a && a)
forall {k} (a :: k). (HasBinaryProducts k, Ob a) => a ~> (a && a)
diag @m (m ~> (m && m)) -> (b ~> b) -> (m && b) ~> ((m && m) && b)
forall (a :: k) (b :: k) (x :: k) (y :: k).
(a ~> x) -> (b ~> y) -> (a && b) ~> (x && y)
forall k (a :: k) (b :: k) (x :: k) (y :: k).
HasBinaryProducts k =>
(a ~> x) -> (b ~> y) -> (a && b) ~> (x && y)
*** forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @b) ((m && b) ~> ((m && m) && b))
-> (a ~> (m && b)) -> a ~> ((m && m) && b)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. a ~> (m && b)
f) Writer m a (m && b)
-> Writer m (m && b) b -> (:.:) (Writer m) (Writer m) 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
:.: ((m && b) ~> (m && b)) -> Writer m (m && b) b
forall {k} (a :: k) (b :: k) (m :: k).
(Ob a, Ob b) =>
(a ~> (m && b)) -> Writer m a b
Writer (m && b) ~> (m && b)
forall (a :: k). Ob a => a ~> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id ((Ob (m && b), Ob (m && b)) => (:.:) (Writer m) (Writer m) a b)
-> ((m && b) ~> (m && b)) -> (:.:) (Writer m) (Writer m) a b
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @m Obj m -> (b ~> b) -> (m && b) ~> (m && b)
forall (a :: k) (b :: k) (x :: k) (y :: k).
(a ~> x) -> (b ~> y) -> (a && b) ~> (x && y)
forall k (a :: k) (b :: k) (x :: k) (y :: k).
HasBinaryProducts k =>
(a ~> x) -> (b ~> y) -> (a && b) ~> (x && y)
*** forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @b)

instance (BiCCC k, Monoid m) => MonoidalProfunctor (Writer m :: k +-> k) where
  par0 :: Writer m Unit Unit
par0 = Writer m Unit Unit
Writer m TerminalObject TerminalObject
forall (a :: k). Ob a => Writer m a a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id
  Writer @x1 @x2 x1 ~> (m && x2)
f par :: forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
Writer m x1 x2 -> Writer m y1 y2 -> Writer m (x1 ** y1) (x2 ** y2)
`par` Writer @y1 @y2 y1 ~> (m && y2)
g =
    ((x1 ** y1) ~> (m && (x2 ** y2))) -> Writer m (x1 ** y1) (x2 ** y2)
forall {k} (a :: k) (b :: k) (m :: k).
(Ob a, Ob b) =>
(a ~> (m && b)) -> Writer m a b
Writer
      ( (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @m Obj m
-> ((x2 && y2) ~> (x2 ** y2))
-> (m && (x2 && y2)) ~> (m && (x2 ** y2))
forall (a :: k) (b :: k) (x :: k) (y :: k).
(a ~> x) -> (b ~> y) -> (a && b) ~> (x && y)
forall k (a :: k) (b :: k) (x :: k) (y :: k).
HasBinaryProducts k =>
(a ~> x) -> (b ~> y) -> (a && b) ~> (x && y)
*** (forall (a :: k) (b :: k). (Monoidal k, Ob a, Ob b) => Obj (a ** b)
forall {k} (a :: k) (b :: k).
(Monoidal k, Ob a, Ob b) =>
Obj (a ** b)
obj2 @x2 @y2 :: x2 && y2 ~> x2 ** y2))
          ((m && (x2 && y2)) ~> (m && (x2 ** y2)))
-> ((x1 ** y1) ~> (m && (x2 && y2)))
-> (x1 ** y1) ~> (m && (x2 ** y2))
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall {k} (a :: FK k) (b :: FK k).
(BiCCC k, Ob a, Ob b) =>
(TermF ~> (a --> b)) -> FromFree a ~> FromFree b
forall (a :: FK k) (b :: FK k).
(BiCCC k, Ob a, Ob b) =>
(TermF ~> (a --> b)) -> FromFree a ~> FromFree b
toCCC @(F x1 * F y1) @(F m * (F x2 * F y2))
            ( ((forall (x :: FK k).
  Cast x (TermF && ('F x1 * 'F y1)) =>
  x ~> ('F x1 * 'F y1))
 -> (TermF && ('F x1 * 'F y1)) ~> ('F m * ('F x2 * 'F y2)))
-> TermF ~> (('F x1 * 'F y1) ~~> ('F m * ('F x2 * 'F y2)))
forall {k} (a :: k) (b :: k) (i :: k).
(CCC k, Ob i, Ob a, Ob b) =>
((forall (x :: k). Cast x (i && a) => x ~> a) -> (i && a) ~> b)
-> i ~> (a ~~> b)
lam \((TermF * ('F x1 * 'F y1)) ~> 'F x1
x1 :& (TermF * ('F x1 * 'F y1)) ~> 'F y1
y1) ->
                let f' :: ((TermF * ('F x1 * 'F y1)) ~> 'F x1)
-> (TermF * ('F x1 * 'F y1)) ~> ('F m * 'F x2)
f' = forall {k} (a :: FK k) (b :: FK k) (i :: FK k).
(BiCCC k, Ob a, Ob b) =>
(FromFree a ~> FromFree b) -> (i ~> a) -> i ~> b
forall (a :: FK k) (b :: FK k) (i :: FK k).
(BiCCC k, Ob a, Ob b) =>
(FromFree a ~> FromFree b) -> (i ~> a) -> i ~> b
lift @(F x1) @(F m * F x2) x1 ~> (m && x2)
FromFree ('F x1) ~> FromFree ('F m * 'F x2)
f
                    g' :: ((TermF * ('F x1 * 'F y1)) ~> 'F y1)
-> (TermF * ('F x1 * 'F y1)) ~> ('F m * 'F y2)
g' = forall {k} (a :: FK k) (b :: FK k) (i :: FK k).
(BiCCC k, Ob a, Ob b) =>
(FromFree a ~> FromFree b) -> (i ~> a) -> i ~> b
forall (a :: FK k) (b :: FK k) (i :: FK k).
(BiCCC k, Ob a, Ob b) =>
(FromFree a ~> FromFree b) -> (i ~> a) -> i ~> b
lift @(F y1) @(F m * F y2) y1 ~> (m && y2)
FromFree ('F y1) ~> FromFree ('F m * 'F y2)
g
                    mappend' :: ((TermF * ('F x1 * 'F y1)) ~> ('F m * 'F m))
-> (TermF * ('F x1 * 'F y1)) ~> 'F m
mappend' = forall {k} (a :: FK k) (b :: FK k) (i :: FK k).
(BiCCC k, Ob a, Ob b) =>
(FromFree a ~> FromFree b) -> (i ~> a) -> i ~> b
forall (a :: FK k) (b :: FK k) (i :: FK k).
(BiCCC k, Ob a, Ob b) =>
(FromFree a ~> FromFree b) -> (i ~> a) -> i ~> b
lift @(F m * F m) @(F m) (m ** m) ~> m
FromFree ('F m * 'F m) ~> FromFree ('F m)
forall {k} (m :: k). Monoid m => (m ** m) ~> m
mappend
                in case (((TermF * ('F x1 * 'F y1)) ~> 'F x1)
-> (TermF * ('F x1 * 'F y1)) ~> ('F m * 'F x2)
f' (TermF * ('F x1 * 'F y1)) ~> 'F x1
x1, ((TermF * ('F x1 * 'F y1)) ~> 'F y1)
-> (TermF * ('F x1 * 'F y1)) ~> ('F m * 'F y2)
g' (TermF * ('F x1 * 'F y1)) ~> 'F y1
y1) of ((TermF * ('F x1 * 'F y1)) ~> 'F m
m :& (TermF * ('F x1 * 'F y1)) ~> 'F x2
x2, (TermF * ('F x1 * 'F y1)) ~> 'F m
m' :& (TermF * ('F x1 * 'F y1)) ~> 'F y2
y2) -> ((TermF * ('F x1 * 'F y1)) ~> ('F m * 'F m))
-> (TermF * ('F x1 * 'F y1)) ~> 'F m
mappend' ((TermF * ('F x1 * 'F y1)) ~> 'F m
m ((TermF * ('F x1 * 'F y1)) ~> 'F m)
-> ((TermF * ('F x1 * 'F y1)) ~> 'F m)
-> (TermF * ('F x1 * 'F y1)) ~> ('F m && 'F m)
forall {k} (i :: k) (a :: k) (b :: k).
(CCC k, Ob a, Ob b) =>
(i ~> a) -> (i ~> b) -> i ~> (a && b)
:& (TermF * ('F x1 * 'F y1)) ~> 'F m
m') ((TermF * ('F x1 * 'F y1)) ~> 'F m)
-> ((TermF * ('F x1 * 'F y1)) ~> ('F x2 * 'F y2))
-> (TermF * ('F x1 * 'F y1)) ~> ('F m && ('F x2 * 'F y2))
forall {k} (i :: k) (a :: k) (b :: k).
(CCC k, Ob a, Ob b) =>
(i ~> a) -> (i ~> b) -> i ~> (a && b)
:& ((TermF * ('F x1 * 'F y1)) ~> 'F x2
x2 ((TermF * ('F x1 * 'F y1)) ~> 'F x2)
-> ((TermF * ('F x1 * 'F y1)) ~> 'F y2)
-> (TermF * ('F x1 * 'F y1)) ~> ('F x2 && 'F y2)
forall {k} (i :: k) (a :: k) (b :: k).
(CCC k, Ob a, Ob b) =>
(i ~> a) -> (i ~> b) -> i ~> (a && b)
:& (TermF * ('F x1 * 'F y1)) ~> 'F y2
y2)
            )
      )
      ((Ob (x1 ** y1), Ob (x1 ** y1)) => Writer m (x1 ** y1) (x2 ** y2))
-> ((x1 ** y1) ~> (x1 ** y1)) -> Writer m (x1 ** y1) (x2 ** y2)
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ forall (a :: k) (b :: k). (Monoidal k, Ob a, Ob b) => Obj (a ** b)
forall {k} (a :: k) (b :: k).
(Monoidal k, Ob a, Ob b) =>
Obj (a ** b)
obj2 @x1 @y1
      ((Ob (x2 ** y2), Ob (x2 ** y2)) => Writer m (x1 ** y1) (x2 ** y2))
-> Obj (x2 ** y2) -> Writer m (x1 ** y1) (x2 ** y2)
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ forall (a :: k) (b :: k). (Monoidal k, Ob a, Ob b) => Obj (a ** b)
forall {k} (a :: k) (b :: k).
(Monoidal k, Ob a, Ob b) =>
Obj (a ** b)
obj2 @x2 @y2