module Proarrow.Profunctor.HaskValue 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 HaskValue :: Type -> j +-> k
data HaskValue c a b where
  HaskValue :: (Ob a, Ob b) => c -> HaskValue c a b

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

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

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

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

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