module Proarrow.Promonad.Cont where

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

import Proarrow.Category.Instance.Kleisli (KLEISLI (..), Kleisli (..))
import Proarrow.Category.Monoidal (MonoidalProfunctor (..))
import Proarrow.Category.Monoidal.Action (Strong (..))
import Proarrow.Core (CategoryOf (..), Profunctor (..), Promonad (..))
import Proarrow.Object.Dual (ExpSA, StarAutonomous (..), applySA, currySA, expSA)
import Proarrow.Object.Exponential (Closed (..), curry, uncurry)
import Proarrow.Object.BinaryCoproduct (Coprod (..), HasBinaryCoproducts (..), HasCoproducts)

data Cont r a b where
  Cont :: (Ob a, Ob b) => {forall {k} (a :: k) (b :: k) (r :: k).
Cont r a b -> (b ~> r) -> a ~> r
runCont :: (b ~> r) -> (a ~> r)} -> Cont r a b
instance CategoryOf k => Profunctor (Cont (r :: k)) where
  dimap :: forall (c :: k) (a :: k) (b :: k) (d :: k).
(c ~> a) -> (b ~> d) -> Cont r a b -> Cont r c d
dimap c ~> a
l b ~> d
r (Cont (b ~> r) -> a ~> r
f) = ((d ~> r) -> c ~> r) -> Cont r c d
forall {k} (a :: k) (b :: k) (r :: k).
(Ob a, Ob b) =>
((b ~> r) -> a ~> r) -> Cont r a b
Cont (((a ~> r) -> (c ~> a) -> c ~> r
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 ~> a
l) ((a ~> r) -> c ~> r) -> ((d ~> r) -> a ~> r) -> (d ~> r) -> c ~> r
forall b c a. (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
. (b ~> r) -> a ~> r
f ((b ~> r) -> a ~> r) -> ((d ~> r) -> b ~> r) -> (d ~> r) -> a ~> r
forall b c a. (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
. ((d ~> r) -> (b ~> d) -> b ~> r
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
. b ~> d
r)) ((Ob c, Ob a) => Cont r c d) -> (c ~> a) -> Cont r 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) => Cont r c d) -> (b ~> d) -> Cont r 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
\\ b ~> d
r
  (Ob a, Ob b) => r
r \\ :: forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> Cont r a b -> r
\\ Cont{} = r
(Ob a, Ob b) => r
r
instance CategoryOf k => Promonad (Cont (r :: k)) where
  id :: forall (a :: k). Ob a => Cont r a a
id = ((a ~> r) -> a ~> r) -> Cont r a a
forall {k} (a :: k) (b :: k) (r :: k).
(Ob a, Ob b) =>
((b ~> r) -> a ~> r) -> Cont r a b
Cont (a ~> r) -> a ~> r
forall a. Ob a => a -> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id
  Cont (c ~> r) -> b ~> r
f . :: forall (b :: k) (c :: k) (a :: k).
Cont r b c -> Cont r a b -> Cont r a c
. Cont (b ~> r) -> a ~> r
g = ((c ~> r) -> a ~> r) -> Cont r a c
forall {k} (a :: k) (b :: k) (r :: k).
(Ob a, Ob b) =>
((b ~> r) -> a ~> r) -> Cont r a b
Cont ((b ~> r) -> a ~> r
g ((b ~> r) -> a ~> r) -> ((c ~> r) -> b ~> r) -> (c ~> r) -> a ~> r
forall b c a. (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) -> b ~> r
f)
instance Strong Type (Cont (r :: Type)) where
  act :: forall a b x y.
(a ~> b) -> Cont r x y -> Cont r (Act a x) (Act b y)
act a ~> b
ab (Cont (y ~> r) -> x ~> r
yrxy) = (((b, y) ~> r) -> (a, x) ~> r) -> Cont r (a, x) (b, y)
forall {k} (a :: k) (b :: k) (r :: k).
(Ob a, Ob b) =>
((b ~> r) -> a ~> r) -> Cont r a b
Cont \(b, y) ~> r
byr -> (a ~> (x ~~> r)) -> (a ** x) ~> r
forall {k} (b :: k) (c :: k) (a :: k).
(Closed k, Ob b, Ob c) =>
(a ~> (b ~~> c)) -> (a ** b) ~> c
uncurry ((y ~> r) -> x ~> r
(y -> r) -> x -> r
yrxy ((y -> r) -> x -> r) -> (a -> y -> r) -> a -> x -> r
forall b c a. (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
. ((b ** y) ~> r) -> b ~> (y ~~> r)
forall k (a :: k) (b :: k) (c :: k).
(Closed k, Ob a, Ob b) =>
((a ** b) ~> c) -> a ~> (b ~~> c)
forall a b c. (Ob a, Ob b) => ((a ** b) ~> c) -> a ~> (b ~~> c)
curry (b, y) ~> r
(b ** y) ~> r
byr (b -> (y -> r)) -> (a -> b) -> a -> y -> r
forall b c a. (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
a -> b
ab)

-- | Only premonoidal not monoidal?
instance MonoidalProfunctor (Cont (r :: Type)) where
  par0 :: Cont r Unit Unit
par0 = ((() ~> r) -> () ~> r) -> Cont r () ()
forall {k} (a :: k) (b :: k) (r :: k).
(Ob a, Ob b) =>
((b ~> r) -> a ~> r) -> Cont r a b
Cont (() ~> r) -> () ~> r
(() -> r) -> () -> r
forall a. Ob a => a -> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id
  Cont (x2 ~> r) -> x1 ~> r
f par :: forall x1 x2 y1 y2.
Cont r x1 x2 -> Cont r y1 y2 -> Cont r (x1 ** y1) (x2 ** y2)
`par` Cont (y2 ~> r) -> y1 ~> r
g = (((x2, y2) ~> r) -> (x1, y1) ~> r) -> Cont r (x1, y1) (x2, y2)
forall {k} (a :: k) (b :: k) (r :: k).
(Ob a, Ob b) =>
((b ~> r) -> a ~> r) -> Cont r a b
Cont \(x2, y2) ~> r
k (x1
x1, y1
y1) -> (x2 ~> r) -> x1 ~> r
f (\x2
x2 -> (y2 ~> r) -> y1 ~> r
g (\y2
y2 -> (x2, y2) ~> r
(x2, y2) -> r
k (x2
x2, y2
y2)) y1
y1) x1
x1

instance HasCoproducts k => MonoidalProfunctor (Coprod (Cont (r :: k))) where
  par0 :: Coprod (Cont r) Unit Unit
par0 = Cont r InitialObject InitialObject
-> Coprod (Cont r) ('COPR InitialObject) ('COPR InitialObject)
forall {j} {k} (p :: j +-> k) (a1 :: k) (b1 :: j).
p a1 b1 -> Coprod p ('COPR a1) ('COPR b1)
Coprod (((InitialObject ~> r) -> InitialObject ~> r)
-> Cont r InitialObject InitialObject
forall {k} (a :: k) (b :: k) (r :: k).
(Ob a, Ob b) =>
((b ~> r) -> a ~> r) -> Cont r a b
Cont (InitialObject ~> r) -> InitialObject ~> r
forall a. Ob a => a -> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id)
  Coprod (Cont @af @bf (b1 ~> r) -> a1 ~> r
f) par :: forall (x1 :: COPROD k) (x2 :: COPROD k) (y1 :: COPROD k)
       (y2 :: COPROD k).
Coprod (Cont r) x1 x2
-> Coprod (Cont r) y1 y2 -> Coprod (Cont r) (x1 ** y1) (x2 ** y2)
`par` Coprod (Cont @ag @bg (b1 ~> r) -> a1 ~> r
g) = forall k (a :: k) (b :: k) r.
(HasBinaryCoproducts k, Ob a, Ob b) =>
(Ob (a || b) => r) -> r
withObCoprod @k @af @ag ((Ob (a1 || a1) => Coprod (Cont r) (x1 ** y1) (x2 ** y2))
 -> Coprod (Cont r) (x1 ** y1) (x2 ** y2))
-> (Ob (a1 || a1) => Coprod (Cont r) (x1 ** y1) (x2 ** y2))
-> Coprod (Cont r) (x1 ** y1) (x2 ** y2)
forall a b. (a -> b) -> a -> b
$ forall k (a :: k) (b :: k) r.
(HasBinaryCoproducts k, Ob a, Ob b) =>
(Ob (a || b) => r) -> r
withObCoprod @k @bf @bg ((Ob (b1 || b1) => Coprod (Cont r) (x1 ** y1) (x2 ** y2))
 -> Coprod (Cont r) (x1 ** y1) (x2 ** y2))
-> (Ob (b1 || b1) => Coprod (Cont r) (x1 ** y1) (x2 ** y2))
-> Coprod (Cont r) (x1 ** y1) (x2 ** y2)
forall a b. (a -> b) -> a -> b
$
    Cont r (a1 || a1) (b1 || b1)
-> Coprod (Cont r) ('COPR (a1 || a1)) ('COPR (b1 || b1))
forall {j} {k} (p :: j +-> k) (a1 :: k) (b1 :: j).
p a1 b1 -> Coprod p ('COPR a1) ('COPR b1)
Coprod ((((b1 || b1) ~> r) -> (a1 || a1) ~> r)
-> Cont r (a1 || a1) (b1 || b1)
forall {k} (a :: k) (b :: k) (r :: k).
(Ob a, Ob b) =>
((b ~> r) -> a ~> r) -> Cont r a b
Cont (\(b1 || b1) ~> r
k -> (b1 ~> r) -> a1 ~> r
f ((b1 || b1) ~> r
k ((b1 || b1) ~> r) -> (b1 ~> (b1 || b1)) -> b1 ~> r
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).
(HasBinaryCoproducts k, Ob a, Ob b) =>
a ~> (a || b)
lft @_ @bf @bg) (a1 ~> r) -> (a1 ~> r) -> (a1 || a1) ~> r
forall (x :: k) (a :: k) (y :: k).
(x ~> a) -> (y ~> a) -> (x || y) ~> a
forall k (x :: k) (a :: k) (y :: k).
HasBinaryCoproducts k =>
(x ~> a) -> (y ~> a) -> (x || y) ~> a
||| (b1 ~> r) -> a1 ~> r
g ((b1 || b1) ~> r
k ((b1 || b1) ~> r) -> (b1 ~> (b1 || b1)) -> b1 ~> r
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).
(HasBinaryCoproducts k, Ob a, Ob b) =>
b ~> (a || b)
rgt @_ @bf @bg)))

instance StarAutonomous (KLEISLI (Cont (r :: Type))) where
  type Dual @(KLEISLI (Cont r)) (KL a) = KL (a ~~> r)
  dual :: forall (a :: KLEISLI (Cont r)) (b :: KLEISLI (Cont r)).
(a ~> b) -> Dual b ~> Dual a
dual (Kleisli (Cont (b1 ~> r) -> a1 ~> r
f)) = Cont r (b1 -> r) (a1 -> r)
-> Kleisli ('KL (b1 -> r)) ('KL (a1 -> r))
forall {k} (p :: CAT k) (a1 :: k) (b1 :: k).
p a1 b1 -> Kleisli ('KL a1) ('KL b1)
Kleisli ((((a1 -> r) ~> r) -> (b1 -> r) ~> r) -> Cont r (b1 -> r) (a1 -> r)
forall {k} (a :: k) (b :: k) (r :: k).
(Ob a, Ob b) =>
((b ~> r) -> a ~> r) -> Cont r a b
Cont \(a1 -> r) ~> r
k b1 -> r
br -> (a1 -> r) ~> r
(a1 -> r) -> r
k ((b1 ~> r) -> a1 ~> r
f b1 ~> r
b1 -> r
br))
  dualInv :: forall (a :: KLEISLI (Cont r)) (b :: KLEISLI (Cont r)).
(Ob a, Ob b) =>
(Dual a ~> Dual b) -> b ~> a
dualInv (Kleisli (Cont (b1 ~> r) -> a1 ~> r
f)) = Cont r (UN 'KL b) (UN 'KL a)
-> Kleisli ('KL (UN 'KL b)) ('KL (UN 'KL a))
forall {k} (p :: CAT k) (a1 :: k) (b1 :: k).
p a1 b1 -> Kleisli ('KL a1) ('KL b1)
Kleisli (((UN 'KL a ~> r) -> UN 'KL b ~> r) -> Cont r (UN 'KL b) (UN 'KL a)
forall {k} (a :: k) (b :: k) (r :: k).
(Ob a, Ob b) =>
((b ~> r) -> a ~> r) -> Cont r a b
Cont \UN 'KL a ~> r
k UN 'KL b
b -> (b1 ~> r) -> a1 ~> r
f (\UN 'KL b -> r
g -> UN 'KL b -> r
g UN 'KL b
b) UN 'KL a ~> r
UN 'KL a -> r
k)
  linDist :: forall (a :: KLEISLI (Cont r)) (b :: KLEISLI (Cont r))
       (c :: KLEISLI (Cont r)).
(Ob a, Ob b, Ob c) =>
((a ** b) ~> Dual c) -> a ~> Dual (b ** c)
linDist (Kleisli (Cont (b1 ~> r) -> a1 ~> r
f)) = Cont r (UN 'KL a) ((UN 'KL b, UN 'KL c) -> r)
-> Kleisli ('KL (UN 'KL a)) ('KL ((UN 'KL b, UN 'KL c) -> r))
forall {k} (p :: CAT k) (a1 :: k) (b1 :: k).
p a1 b1 -> Kleisli ('KL a1) ('KL b1)
Kleisli (((((UN 'KL b, UN 'KL c) -> r) ~> r) -> UN 'KL a ~> r)
-> Cont r (UN 'KL a) ((UN 'KL b, UN 'KL c) -> r)
forall {k} (a :: k) (b :: k) (r :: k).
(Ob a, Ob b) =>
((b ~> r) -> a ~> r) -> Cont r a b
Cont \((UN 'KL b, UN 'KL c) -> r) ~> r
k UN 'KL a
a -> ((UN 'KL b, UN 'KL c) -> r) ~> r
((UN 'KL b, UN 'KL c) -> r) -> r
k (\(UN 'KL b
b, UN 'KL c
c) -> (b1 ~> r) -> a1 ~> r
f (\UN 'KL c -> r
g -> UN 'KL c -> r
g UN 'KL c
c) (UN 'KL a
a, UN 'KL b
b)))
  linDistInv :: forall (a :: KLEISLI (Cont r)) (b :: KLEISLI (Cont r))
       (c :: KLEISLI (Cont r)).
(Ob a, Ob b, Ob c) =>
(a ~> Dual (b ** c)) -> (a ** b) ~> Dual c
linDistInv (Kleisli (Cont (b1 ~> r) -> a1 ~> r
f)) = Cont r (UN 'KL a, UN 'KL b) (UN 'KL c -> r)
-> Kleisli ('KL (UN 'KL a, UN 'KL b)) ('KL (UN 'KL c -> r))
forall {k} (p :: CAT k) (a1 :: k) (b1 :: k).
p a1 b1 -> Kleisli ('KL a1) ('KL b1)
Kleisli ((((UN 'KL c -> r) ~> r) -> (UN 'KL a, UN 'KL b) ~> r)
-> Cont r (UN 'KL a, UN 'KL b) (UN 'KL c -> r)
forall {k} (a :: k) (b :: k) (r :: k).
(Ob a, Ob b) =>
((b ~> r) -> a ~> r) -> Cont r a b
Cont \(UN 'KL c -> r) ~> r
k (UN 'KL a
a, UN 'KL b
b) -> (UN 'KL c -> r) ~> r
(UN 'KL c -> r) -> r
k (\UN 'KL c
c -> (b1 ~> r) -> a1 ~> r
f (\(UN 'KL b, UN 'KL c) -> r
g -> (UN 'KL b, UN 'KL c) -> r
g (UN 'KL b
b, UN 'KL c
c)) UN 'KL a
a))
instance Closed (KLEISLI (Cont (r :: Type))) where
  type a ~~> b = ExpSA a b
  withObExp :: forall (a :: KLEISLI (Cont r)) (b :: KLEISLI (Cont r)) r.
(Ob a, Ob b) =>
(Ob (a ~~> b) => r) -> r
withObExp Ob (a ~~> b) => r
r = r
Ob (a ~~> b) => r
r
  curry :: forall (a :: KLEISLI (Cont r)) (b :: KLEISLI (Cont r))
       (c :: KLEISLI (Cont r)).
(Ob a, Ob b) =>
((a ** b) ~> c) -> a ~> (b ~~> c)
curry = ((a ** b) ~> c) -> a ~> (b ~~> c)
(('KL (UN 'KL a) ** 'KL (UN 'KL b)) ~> c)
-> 'KL (UN 'KL a) ~> ExpSA ('KL (UN 'KL b)) c
forall {k} (a :: k) (b :: k) (c :: k).
(StarAutonomous k, Ob a, Ob b) =>
((a ** b) ~> c) -> a ~> ExpSA b c
currySA
  apply :: forall (a :: KLEISLI (Cont r)) (b :: KLEISLI (Cont r)).
(Ob a, Ob b) =>
((a ~~> b) ** a) ~> b
apply = ((a ~~> b) ** a) ~> b
(ExpSA ('KL (UN 'KL a)) ('KL (UN 'KL b)) ** 'KL (UN 'KL a))
~> 'KL (UN 'KL b)
forall {k} (b :: k) (c :: k).
(StarAutonomous k, Ob b, Ob c) =>
(ExpSA b c ** b) ~> c
applySA
  ^^^ :: forall (a :: KLEISLI (Cont r)) (b :: KLEISLI (Cont r))
       (x :: KLEISLI (Cont r)) (y :: KLEISLI (Cont r)).
(b ~> y) -> (x ~> a) -> (a ~~> b) ~> (x ~~> y)
(^^^) = (b ~> y) -> (x ~> a) -> (a ~~> b) ~> (x ~~> y)
(b ~> y) -> (x ~> a) -> ExpSA a b ~> ExpSA x y
forall {k} (a :: k) (b :: k) (x :: k) (y :: k).
StarAutonomous k =>
(b ~> y) -> (x ~> a) -> ExpSA a b ~> ExpSA x y
expSA