{-# OPTIONS_GHC -Wno-orphans #-}
module Proarrow.Category.Instance.Kleisli where

import Proarrow.Core (CAT, PRO, UN, Is, CategoryOf(..), Promonad(..), Profunctor(..), dimapDefault, lmap, rmap)
import Proarrow.Profunctor.Composition ((:.:)(..))
import Proarrow.Adjunction (Adjunction)
import Proarrow.Adjunction qualified as Adj


newtype KLEISLI (p :: CAT k) = KL k
type instance UN KL (KL k) = k

type Kleisli :: CAT (KLEISLI p)
data Kleisli (a :: KLEISLI p) b where
  Kleisli :: p a b -> Kleisli (KL a :: KLEISLI p) (KL b)

instance Promonad p => Profunctor (Kleisli :: CAT (KLEISLI p)) where
  dimap :: forall (c :: KLEISLI p) (a :: KLEISLI p) (b :: KLEISLI p)
       (d :: KLEISLI p).
(c ~> a) -> (b ~> d) -> Kleisli a b -> Kleisli c d
dimap = (c ~> a) -> (b ~> d) -> Kleisli a b -> Kleisli c d
Kleisli c a -> Kleisli b d -> Kleisli a b -> Kleisli c d
forall {k} (p :: PRO k k) (c :: k) (a :: k) (b :: k) (d :: k).
Promonad p =>
p c a -> p b d -> p a b -> p c d
dimapDefault
  (Ob a, Ob b) => r
r \\ :: forall (a :: KLEISLI p) (b :: KLEISLI p) r.
((Ob a, Ob b) => r) -> Kleisli a b -> r
\\ Kleisli p a b
p = r
(Ob a, Ob b) => r
(Ob a, Ob b) => r
r ((Ob a, Ob b) => r) -> p a b -> r
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
p

-- | Every promonad makes a category.
instance Promonad p => CategoryOf (KLEISLI p) where
  type (~>) = Kleisli
  type Ob a = (Is KL a, Ob (UN KL a))

instance Promonad p => Promonad (Kleisli :: CAT (KLEISLI p)) where
  id :: forall (a :: KLEISLI p). Ob a => Kleisli a a
id = p (UN 'KL a) (UN 'KL a)
-> Kleisli ('KL (UN 'KL a)) ('KL (UN 'KL a))
forall {k} (p :: CAT k) (b :: k) (b :: k).
p b b -> Kleisli ('KL b) ('KL b)
Kleisli (forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
forall (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id @p)
  Kleisli p a b
f . :: forall (b :: KLEISLI p) (c :: KLEISLI p) (a :: KLEISLI p).
Kleisli b c -> Kleisli a b -> Kleisli a c
. Kleisli p a b
g = p a b -> Kleisli ('KL a) ('KL b)
forall {k} (p :: CAT k) (b :: k) (b :: k).
p b b -> Kleisli ('KL b) ('KL b)
Kleisli (p a b
f p a b -> p a a -> p a b
forall (b :: k) (c :: k) (a :: k). p b c -> p a b -> p 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
. p a a
p a b
g)


type KleisliFree :: forall (p :: PRO k k) -> PRO (KLEISLI p) k
data KleisliFree p a b where
  KleisliFree :: p a b -> KleisliFree p (KL a) b
instance Promonad p => Profunctor (KleisliFree p) where
  dimap :: forall (c :: KLEISLI p) (a :: KLEISLI p) (b :: k) (d :: k).
(c ~> a) -> (b ~> d) -> KleisliFree p a b -> KleisliFree p c d
dimap (Kleisli p a b
l) b ~> d
r (KleisliFree p a b
p) = p a d -> KleisliFree p ('KL a) d
forall {k} (p :: PRO k k) (b :: k) (b :: k).
p b b -> KleisliFree p ('KL b) b
KleisliFree ((b ~> d) -> p a b -> p a d
forall {j} {k} (p :: PRO j k) (b :: k) (d :: k) (a :: j).
Profunctor p =>
(b ~> d) -> p a b -> p a d
rmap b ~> d
r p a b
p p a d -> p a a -> p a d
forall (b :: k) (c :: k) (a :: k). p b c -> p a b -> p 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
. p a b
p a a
l)
  (Ob a, Ob b) => r
r \\ :: forall (a :: KLEISLI p) (b :: k) r.
((Ob a, Ob b) => r) -> KleisliFree p a b -> r
\\ KleisliFree p a b
p = r
(Ob a, Ob b) => r
(Ob a, Ob b) => r
r ((Ob a, Ob b) => r) -> p a b -> r
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
p

type KleisliForget :: forall (p :: PRO k k) -> PRO k (KLEISLI p)
data KleisliForget p a b where
  KleisliForget :: p a b -> KleisliForget p a (KL b)
instance Promonad p => Profunctor (KleisliForget p) where
  dimap :: forall (c :: j) (a :: j) (b :: KLEISLI p) (d :: KLEISLI p).
(c ~> a) -> (b ~> d) -> KleisliForget p a b -> KleisliForget p c d
dimap c ~> a
l (Kleisli p a b
r) (KleisliForget p a b
p) = p c b -> KleisliForget p c ('KL b)
forall {k} (p :: PRO k k) (a :: k) (b :: k).
p a b -> KleisliForget p a ('KL b)
KleisliForget (p a b
p b b
r p b b -> p c b -> p c b
forall (b :: j) (c :: j) (a :: j). p b c -> p a b -> p 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) -> p a b -> p c b
forall {j} {k} (p :: PRO j k) (c :: j) (a :: j) (b :: k).
Profunctor p =>
(c ~> a) -> p a b -> p c b
lmap c ~> a
l p a b
p)
  (Ob a, Ob b) => r
r \\ :: forall (a :: j) (b :: KLEISLI p) r.
((Ob a, Ob b) => r) -> KleisliForget p a b -> r
\\ KleisliForget p a b
p = r
(Ob a, Ob b) => r
(Ob a, Ob b) => r
r ((Ob a, Ob b) => r) -> p a b -> r
forall (a :: j) (b :: j) 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
p

instance Promonad p => Adjunction (KleisliFree p) (KleisliForget p) where
  unit :: forall (a :: k).
Ob a =>
(:.:) (KleisliForget p) (KleisliFree p) a a
unit = p a a -> KleisliForget p a ('KL a)
forall {k} (p :: PRO k k) (a :: k) (b :: k).
p a b -> KleisliForget p a ('KL b)
KleisliForget p a a
forall (a :: k). Ob a => p a a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id KleisliForget p a ('KL a)
-> KleisliFree p ('KL a) a
-> (:.:) (KleisliForget p) (KleisliFree p) a a
forall {i} {j} {k} (p :: PRO i j) (a :: i) (b :: j) (q :: PRO j k)
       (c :: k).
p a b -> q b c -> (:.:) p q a c
:.: p a a -> KleisliFree p ('KL a) a
forall {k} (p :: PRO k k) (b :: k) (b :: k).
p b b -> KleisliFree p ('KL b) b
KleisliFree p a a
forall (a :: k). Ob a => p a a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id
  counit :: (KleisliFree p :.: KleisliForget p) :~> (~>)
counit (KleisliFree p a b
p :.: KleisliForget p b b
q) = p a b -> Kleisli ('KL a) ('KL b)
forall {k} (p :: CAT k) (b :: k) (b :: k).
p b b -> Kleisli ('KL b) ('KL b)
Kleisli (p b b
q p b b -> p a b -> p a b
forall (b :: k) (c :: k) (a :: k). p b c -> p a b -> p 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
. p a b
p)