module Proarrow.Profunctor.Constant where

import Data.Kind (Type)
import Prelude (Monoid (..), ($))

import Proarrow.Category.Monoidal (Monoidal (..), MonoidalProfunctor (..))
import Proarrow.Category.Monoidal.Action (SelfAction, strongPar0)
import Proarrow.Category.Monoidal.Distributive (Cotraversable (..), Traversable (..))
import Proarrow.Core (CategoryOf (..), Profunctor (..), Promonad (..), type (+->))
import Proarrow.Profunctor.Composition ((:.:) ((:.:)))

type Constant :: Type -> j +-> k
data Constant c a b where
  Constant :: (Ob a, Ob b) => c -> Constant c a b

instance (CategoryOf j, CategoryOf k) => Profunctor (Constant c :: j +-> k) where
  dimap :: forall (c :: k) (a :: k) (b :: j) (d :: j).
(c ~> a) -> (b ~> d) -> Constant c a b -> Constant c c d
dimap c ~> a
l b ~> d
r (Constant c
c) = c -> Constant c c d
forall {k} {j} (a :: k) (b :: j) c.
(Ob a, Ob b) =>
c -> Constant c a b
Constant c
c ((Ob c, Ob a) => Constant c c d) -> (c ~> a) -> Constant c 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 b, Ob d) => Constant c c d) -> (b ~> d) -> Constant c c d
forall (a :: j) (b :: j) 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 a, Ob b) => r
r \\ :: forall (a :: k) (b :: j) r.
((Ob a, Ob b) => r) -> Constant c a b -> r
\\ Constant{} = r
(Ob a, Ob b) => r
r

instance (Monoid c, CategoryOf k) => Promonad (Constant c :: k +-> k) where
  id :: forall (a :: k). Ob a => Constant c a a
id = c -> Constant c a a
forall {k} {j} (a :: k) (b :: j) c.
(Ob a, Ob b) =>
c -> Constant c a b
Constant c
forall a. Monoid a => a
mempty
  Constant c
c1 . :: forall (b :: k) (c :: k) (a :: k).
Constant c b c -> Constant c a b -> Constant c a c
. Constant c
c2 = c -> Constant c a c
forall {k} {j} (a :: k) (b :: j) c.
(Ob a, Ob b) =>
c -> Constant c a b
Constant (c -> c -> c
forall a. Monoid a => a -> a -> a
mappend c
c1 c
c2)

instance (Monoid c, Monoidal j, Monoidal k) => MonoidalProfunctor (Constant c :: j +-> k) where
  par0 :: Constant c Unit Unit
par0 = c -> Constant c Unit Unit
forall {k} {j} (a :: k) (b :: j) c.
(Ob a, Ob b) =>
c -> Constant c a b
Constant c
forall a. Monoid a => a
mempty
  Constant @a1 @b1 c
c1 par :: forall (x1 :: k) (x2 :: j) (y1 :: k) (y2 :: j).
Constant c x1 x2
-> Constant c y1 y2 -> Constant c (x1 ** y1) (x2 ** y2)
`par` Constant @a2 @b2 c
c2 = forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @k @a1 @a2 ((Ob (x1 ** y1) => Constant c (x1 ** y1) (x2 ** y2))
 -> Constant c (x1 ** y1) (x2 ** y2))
-> (Ob (x1 ** y1) => Constant c (x1 ** y1) (x2 ** y2))
-> Constant c (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 @j @b1 @b2 ((Ob (x2 ** y2) => Constant c (x1 ** y1) (x2 ** y2))
 -> Constant c (x1 ** y1) (x2 ** y2))
-> (Ob (x2 ** y2) => Constant c (x1 ** y1) (x2 ** y2))
-> Constant c (x1 ** y1) (x2 ** y2)
forall a b. (a -> b) -> a -> b
$ c -> Constant c (x1 ** y1) (x2 ** y2)
forall {k} {j} (a :: k) (b :: j) c.
(Ob a, Ob b) =>
c -> Constant c a b
Constant (c -> c -> c
forall a. Monoid a => a -> a -> a
mappend c
c1 c
c2)

instance (SelfAction k) => Traversable (Constant c :: k +-> k) where
  traverse :: forall (p :: k +-> k).
(DistributiveProfunctor p, Strong k p, SelfAction k) =>
(Constant c :.: p) :~> (p :.: Constant c)
traverse (Constant c
c :.: p b b
r) = p a a
forall {k} {p :: CAT k} (a :: k).
(SelfAction k, Strong k p, MonoidalProfunctor p, Ob a) =>
p a a
strongPar0 p a a -> Constant c a b -> (:.:) p (Constant c) 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
:.: c -> Constant c a b
forall {k} {j} (a :: k) (b :: j) c.
(Ob a, Ob b) =>
c -> Constant c a b
Constant c
c ((Ob b, Ob b) => (:.:) p (Constant c) a b)
-> p b b -> (:.:) p (Constant c) a b
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> p 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
\\ p b b
r

instance (SelfAction k) => Cotraversable (Constant c :: k +-> k) where
  cotraverse :: forall (p :: k +-> k).
(DistributiveProfunctor p, Strong k p, SelfAction k) =>
(p :.: Constant c) :~> (Constant c :.: p)
cotraverse (p a b
r :.: Constant c
c) = c -> Constant c a b
forall {k} {j} (a :: k) (b :: j) c.
(Ob a, Ob b) =>
c -> Constant c a b
Constant c
c Constant c a b -> p b b -> (:.:) (Constant c) p 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
:.: p b b
forall {k} {p :: CAT k} (a :: k).
(SelfAction k, Strong k p, MonoidalProfunctor p, Ob a) =>
p a a
strongPar0 ((Ob a, Ob b) => (:.:) (Constant c) p a b)
-> p a b -> (:.:) (Constant c) p a b
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> p 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
\\ p a b
r