{-# OPTIONS_GHC -Wno-orphans #-}

module Proarrow.Profunctor.Coyoneda where

import Data.Kind (Type)

import Proarrow.Category.Instance.Prof (Prof (..))
import Proarrow.Core (CategoryOf (..), PRO, Profunctor (..), Promonad (..), (:~>))
import Proarrow.Functor (Functor (..))
import Proarrow.Profunctor.Free (HasFree (..))
import Proarrow.Profunctor.Star (Star (..))

type Coyoneda :: (j -> k -> Type) -> PRO j k
data Coyoneda p a b where
  Coyoneda :: (a ~> c) -> (d ~> b) -> p c d -> Coyoneda p a b

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

instance (Functor Coyoneda) where
  map :: forall (a :: j -> k -> Type) (b :: j -> k -> Type).
(a ~> b) -> Coyoneda a ~> Coyoneda b
map (Prof a :~> b
n) = (Coyoneda a :~> Coyoneda b) -> Prof (Coyoneda a) (Coyoneda b)
forall {k} {j} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \(Coyoneda a ~> c
g d ~> b
h a c d
p) -> (a ~> c) -> (d ~> b) -> b c d -> Coyoneda b a b
forall {k} {k} (a :: k) (c :: k) (d :: k) (b :: k)
       (p :: k -> k -> Type).
(a ~> c) -> (d ~> b) -> p c d -> Coyoneda p a b
Coyoneda a ~> c
g d ~> b
h (a c d -> b c d
a :~> b
n a c d
p)

instance HasFree Profunctor where
  type Free Profunctor = Star Coyoneda
  lift' :: forall (a :: PRO j k) (b :: PRO j k).
(a ~> b) -> Free Profunctor a b
lift' (Prof a :~> b
n) = (a ~> Coyoneda b) -> Star Coyoneda a b
forall {k1} {k2} (b :: k1) (a :: k2) (f :: k1 -> k2).
Ob b =>
(a ~> f b) -> Star f a b
Star ((a :~> Coyoneda b) -> Prof a (Coyoneda b)
forall {k} {j} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \a a b
p -> b a b -> Coyoneda b a b
forall j k (a :: j) (b :: k) (p :: j -> k -> Type).
(CategoryOf j, CategoryOf k, Ob a, Ob b) =>
p a b -> Coyoneda p a b
coyoneda (a a b -> b a b
a :~> b
n a a b
p) ((Ob a, Ob b) => Coyoneda b a b) -> a a b -> Coyoneda b a b
forall (a :: j) (b :: k) r. ((Ob a, Ob b) => r) -> a 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 a b
p)
  retract' :: forall (b :: PRO j k) (a :: PRO j k).
Profunctor b =>
Free Profunctor a b -> a ~> b
retract' (Star (Prof a :~> Coyoneda b
f)) = (a :~> b) -> Prof a b
forall {k} {j} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof (Coyoneda b a b -> b a b
Coyoneda b :~> b
forall {k} {k1} (p :: PRO k k1). Profunctor p => Coyoneda p :~> p
unCoyoneda (Coyoneda b a b -> b a b)
-> (a a b -> Coyoneda b a b) -> a a b -> b a b
forall b c a. (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 a b -> Coyoneda b a b
a :~> Coyoneda b
f)

coyoneda :: (CategoryOf j, CategoryOf k, Ob a, Ob b) => p a b -> Coyoneda (p :: j -> k -> Type) a b
coyoneda :: forall j k (a :: j) (b :: k) (p :: j -> k -> Type).
(CategoryOf j, CategoryOf k, Ob a, Ob b) =>
p a b -> Coyoneda p a b
coyoneda = (a ~> a) -> (b ~> b) -> p a b -> Coyoneda p a b
forall {k} {k} (a :: k) (c :: k) (d :: k) (b :: k)
       (p :: k -> k -> Type).
(a ~> c) -> (d ~> b) -> p c d -> Coyoneda p a b
Coyoneda a ~> a
forall (a :: j). Ob a => a ~> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id b ~> b
forall (a :: k). Ob a => a ~> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id

unCoyoneda :: (Profunctor p) => Coyoneda p :~> p
unCoyoneda :: forall {k} {k1} (p :: PRO k k1). Profunctor p => Coyoneda p :~> p
unCoyoneda (Coyoneda a ~> c
f d ~> b
g p c d
p) = (a ~> c) -> (d ~> b) -> p c d -> p a b
forall (c :: k) (a :: k) (b :: k1) (d :: k1).
(c ~> a) -> (b ~> d) -> p a b -> p c d
forall {j} {k} (p :: PRO j k) (c :: j) (a :: j) (b :: k) (d :: k).
Profunctor p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimap a ~> c
f d ~> b
g p c d
p