module Proarrow.Promonad.Cont where

import Data.Kind (Type)

import Proarrow.Category.Instance.Kleisli (KLEISLI (..), Kleisli (..))
import Proarrow.Category.Monoidal.Action (Strong (..))
import Proarrow.Core (Profunctor (..), Promonad (..))
import Proarrow.Object.Dual (ExpSA, StarAutonomous (..), currySA, expSA, uncurrySA)
import Proarrow.Object.Exponential (Closed (..), curry, uncurry)

newtype Cont r a b = Cont {forall r a b. Cont r a b -> (b -> r) -> a -> r
runCont :: (b -> r) -> (a -> r)}
instance Profunctor (Cont r) where
  dimap :: forall c a b d. (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 r a b. ((b -> r) -> a -> r) -> Cont r a b
Cont (((a ~> r) -> (c ~> a) -> c ~> r
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
. 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 :: PRO 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 :: PRO 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 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
. b ~> d
r))
  (Ob a, Ob b) => r
r \\ :: forall a b r. ((Ob a, Ob b) => r) -> Cont r a b -> r
\\ Cont r a b
_ = r
(Ob a, Ob b) => r
r
instance Promonad (Cont r) where
  id :: forall a. Ob a => Cont r a a
id = ((a -> r) -> a -> r) -> Cont r a a
forall r a b. ((b -> r) -> a -> r) -> Cont r a b
Cont (a -> r) -> a -> r
forall a. Ob a => a -> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id
  Cont (c -> r) -> b -> r
f . :: forall b c a. 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 r a 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 :: PRO 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) 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 r a b. ((b -> r) -> a -> r) -> Cont r a b
Cont \(b, y) -> r
byr -> (a ~> (x ~~> r)) -> (a ** x) ~> r
forall {k} (a :: k) (b :: k) (c :: k).
(Closed k, Ob b, Ob c) =>
(a ~> (b ~~> c)) -> (a ** b) ~> c
uncurry ((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 :: PRO 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)
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 :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. a ~> b
a -> b
ab)
instance StarAutonomous (KLEISLI (Cont r)) 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 r a b. ((b -> r) -> a -> r) -> Cont r a b
Cont \(a1 -> r) -> r
k b1 -> r
br -> (a1 -> r) -> r
k ((b1 -> r) -> a1 -> r
f 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 ((UN 'KL b -> r) -> r) -> (UN 'KL a -> r) -> 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 r a b. ((b -> r) -> a -> r) -> Cont r a b
Cont \UN 'KL a -> r
k UN 'KL b
b -> ((UN 'KL b -> r) -> r) -> (UN 'KL a -> r) -> r
f (\UN 'KL b -> r
g -> UN 'KL b -> r
g UN 'KL b
b) 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 ((UN 'KL c -> r) -> r) -> (UN 'KL a, UN 'KL b) -> 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 r a 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
k (\(UN 'KL b
b, UN 'KL c
c) -> ((UN 'KL c -> r) -> r) -> (UN 'KL a, UN 'KL b) -> 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 (((UN 'KL b, UN 'KL c) -> r) -> r) -> UN 'KL a -> 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 r a 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
k (\UN 'KL c
c -> (((UN 'KL b, UN 'KL c) -> r) -> r) -> UN 'KL a -> 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)) where
  type a ~~> b = ExpSA a b
  curry' :: forall (a :: KLEISLI (Cont r)) (b :: KLEISLI (Cont r))
       (c :: KLEISLI (Cont r)).
Obj a -> Obj b -> ((a ** b) ~> c) -> a ~> (b ~~> c)
curry' Kleisli{} Kleisli{} = ((a ** b) ~> c) -> a ~> (b ~~> c)
(('KL b1 ** 'KL b1) ~> c) -> 'KL b1 ~> ExpSA ('KL b1) c
forall {k} (a :: k) (b :: k) (c :: k).
(StarAutonomous k, Ob a, Ob b) =>
((a ** b) ~> c) -> a ~> ExpSA b c
currySA
  uncurry' :: forall (b :: KLEISLI (Cont r)) (c :: KLEISLI (Cont r))
       (a :: KLEISLI (Cont r)).
Obj b -> Obj c -> (a ~> (b ~~> c)) -> (a ** b) ~> c
uncurry' Kleisli{} Kleisli{} = (a ~> (b ~~> c)) -> (a ** b) ~> c
(a ~> ExpSA ('KL b1) ('KL b1)) -> (a ** 'KL b1) ~> 'KL b1
forall {k} (a :: k) (b :: k) (c :: k).
(StarAutonomous k, Ob b, Ob c) =>
(a ~> ExpSA b c) -> (a ** b) ~> c
uncurrySA
  ^^^ :: forall (b :: KLEISLI (Cont r)) (y :: KLEISLI (Cont r))
       (x :: KLEISLI (Cont r)) (a :: 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