{-# OPTIONS_GHC -Wno-orphans #-}

module Proarrow.Profunctor.Instance.Arrow where

import Control.Arrow
  ( Arrow (..)
  , ArrowApply (..)
  , ArrowChoice (..)
  , ArrowLoop (..)
  , Kleisli (..)
  , (>>>)
  )
import Control.Category qualified as P
import Control.Monad (MonadPlus)
import Control.Monad.Fix (MonadFix)
import Data.Kind (Type)
import Prelude (Either (..), Functor (..), Monad (..))

import Proarrow.Category.Monoidal (MonoidalProfunctor (..), Tensor)
import Proarrow.Category.Monoidal.Action (CoprodAction)
import Proarrow.Category.Monoidal.Distributive (DistributiveProfunctor)
import Proarrow.Category.Monoidal.Strength (Costrong (..), Strong (..))
import Proarrow.Colimit.BinaryCoproduct (Coprod (..), (++))
import Proarrow.Core (CAT, Profunctor (..), Promonad (..), rmap, type (+->))
import Proarrow.Functor (FromProfunctor (..))
import Proarrow.Limit.BinaryProduct ()
import Proarrow.Profunctor.Representable (Representable (..))

swap :: (b, a) -> (a, b)
swap :: forall b a. (b, a) -> (a, b)
swap ~(b
x, a
y) = (a
y, b
x)

type Arr :: CAT Type -> CAT Type
newtype Arr arr a b = Arr {forall (arr :: CAT Type) a b. Arr arr a b -> arr a b
unArr :: arr a b}

instance (Arrow arr) => Profunctor (Arr arr) where
  dimap :: forall c a b d. (c ~> a) -> (b ~> d) -> Arr arr a b -> Arr arr c d
dimap c ~> a
l b ~> d
r (Arr arr a b
a) = arr c d -> Arr arr c d
forall (arr :: CAT Type) a b. arr a b -> Arr arr a b
Arr ((c -> a) -> arr c a
forall b c. (b -> c) -> arr b c
forall (a :: CAT Type) b c. Arrow a => (b -> c) -> a b c
arr c ~> a
c -> a
l arr c a -> arr a d -> arr c d
forall {k} (cat :: k -> k -> Type) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> arr a b
a arr a b -> arr b d -> arr a d
forall {k} (cat :: k -> k -> Type) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> (b -> d) -> arr b d
forall b c. (b -> c) -> arr b c
forall (a :: CAT Type) b c. Arrow a => (b -> c) -> a b c
arr b ~> d
b -> d
r)

instance (Arrow arr) => Promonad (Arr arr) where
  id :: forall a. Ob a => Arr arr a a
id = arr a a -> Arr arr a a
forall (arr :: CAT Type) a b. arr a b -> Arr arr a b
Arr ((a -> a) -> arr a a
forall b c. (b -> c) -> arr b c
forall (a :: CAT Type) b c. Arrow a => (b -> c) -> a b c
arr a -> a
forall a. Ob a => a -> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id)
  Arr arr b c
f . :: forall b c a. Arr arr b c -> Arr arr a b -> Arr arr a c
. Arr arr a b
g = arr a c -> Arr arr a c
forall (arr :: CAT Type) a b. arr a b -> Arr arr a b
Arr (arr a b
g arr a b -> arr b c -> arr a c
forall {k} (cat :: k -> k -> Type) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> arr b c
f)

instance (Arrow arr) => Strong Tensor (Arr arr) where
  act :: forall a x y.
Ob a =>
Arr arr x y -> Arr arr (Act Tensor a x) (Act Tensor a y)
act (Arr arr x y
a) = arr (a, x) (a, y) -> Arr arr (a, x) (a, y)
forall (arr :: CAT Type) a b. arr a b -> Arr arr a b
Arr (arr x y -> arr (a, x) (a, y)
forall b c d. arr b c -> arr (d, b) (d, c)
forall (a :: CAT Type) b c d. Arrow a => a b c -> a (d, b) (d, c)
second arr x y
a)

instance (ArrowLoop arr) => Costrong Tensor (Arr arr) where
  coact :: forall a x y.
(Ob a, Ob x, Ob y) =>
Arr arr (Act Tensor a x) (Act Tensor a y) -> Arr arr x y
coact (Arr arr (Act Tensor a x) (Act Tensor a y)
f) = arr x y -> Arr arr x y
forall (arr :: CAT Type) a b. arr a b -> Arr arr a b
Arr (arr (x, a) (y, a) -> arr x y
forall b d c. arr (b, d) (c, d) -> arr b c
forall (a :: CAT Type) b d c.
ArrowLoop a =>
a (b, d) (c, d) -> a b c
loop (((x, a) -> (a, x)) -> arr (x, a) (a, x)
forall b c. (b -> c) -> arr b c
forall (a :: CAT Type) b c. Arrow a => (b -> c) -> a b c
arr (x, a) -> (a, x)
forall b a. (b, a) -> (a, b)
swap arr (x, a) (a, x) -> arr (a, x) (y, a) -> arr (x, a) (y, a)
forall {k} (cat :: k -> k -> Type) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> arr (a, x) (a, y)
arr (Act Tensor a x) (Act Tensor a y)
f arr (a, x) (a, y) -> arr (a, y) (y, a) -> arr (a, x) (y, a)
forall {k} (cat :: k -> k -> Type) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> ((a, y) -> (y, a)) -> arr (a, y) (y, a)
forall b c. (b -> c) -> arr b c
forall (a :: CAT Type) b c. Arrow a => (b -> c) -> a b c
arr (a, y) -> (y, a)
forall b a. (b, a) -> (a, b)
swap))

instance (Arrow arr) => MonoidalProfunctor (Arr arr) where
  one :: Arr arr Unit Unit
one = arr () () -> Arr arr () ()
forall (arr :: CAT Type) a b. arr a b -> Arr arr a b
Arr ((() -> ()) -> arr () ()
forall b c. (b -> c) -> arr b c
forall (a :: CAT Type) b c. Arrow a => (b -> c) -> a b c
arr () -> ()
forall a. Ob a => a -> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id)
  Arr arr x1 x2
l ** :: forall x1 x2 y1 y2.
Arr arr x1 x2 -> Arr arr y1 y2 -> Arr arr (x1 ** y1) (x2 ** y2)
** Arr arr y1 y2
r = arr (x1, y1) (x2, y2) -> Arr arr (x1, y1) (x2, y2)
forall (arr :: CAT Type) a b. arr a b -> Arr arr a b
Arr (arr x1 x2
l arr x1 x2 -> arr y1 y2 -> arr (x1, y1) (x2, y2)
forall b c b' c'. arr b c -> arr b' c' -> arr (b, b') (c, c')
forall (a :: CAT Type) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** arr y1 y2
r)

instance (ArrowChoice arr) => MonoidalProfunctor (Coprod (Arr arr)) where
  one :: Coprod (Arr arr) Unit Unit
one = Arr arr Void Void -> Coprod (Arr arr) ('COPR Void) ('COPR Void)
forall {j} {k} (p :: j +-> k) (a1 :: k) (b1 :: j).
p a1 b1 -> Coprod p ('COPR a1) ('COPR b1)
Coprod (arr Void Void -> Arr arr Void Void
forall (arr :: CAT Type) a b. arr a b -> Arr arr a b
Arr ((Void -> Void) -> arr Void Void
forall b c. (b -> c) -> arr b c
forall (a :: CAT Type) b c. Arrow a => (b -> c) -> a b c
arr Void -> Void
forall a. Ob a => a -> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id))
  Coprod (Arr arr a1 b1
l) ** :: forall (x1 :: COPROD Type) (x2 :: COPROD Type) (y1 :: COPROD Type)
       (y2 :: COPROD Type).
Coprod (Arr arr) x1 x2
-> Coprod (Arr arr) y1 y2 -> Coprod (Arr arr) (x1 ** y1) (x2 ** y2)
** Coprod (Arr arr a1 b1
r) = Arr arr (Either a1 a1) (Either b1 b1)
-> Coprod (Arr arr) ('COPR (Either a1 a1)) ('COPR (Either b1 b1))
forall {j} {k} (p :: j +-> k) (a1 :: k) (b1 :: j).
p a1 b1 -> Coprod p ('COPR a1) ('COPR b1)
Coprod (arr (Either a1 a1) (Either b1 b1)
-> Arr arr (Either a1 a1) (Either b1 b1)
forall (arr :: CAT Type) a b. arr a b -> Arr arr a b
Arr (arr a1 b1
l arr a1 b1 -> arr a1 b1 -> arr (Either a1 a1) (Either b1 b1)
forall b c b' c'.
arr b c -> arr b' c' -> arr (Either b b') (Either c c')
forall (a :: CAT Type) b c b' c'.
ArrowChoice a =>
a b c -> a b' c' -> a (Either b b') (Either c c')
+++ arr a1 b1
r))

instance (ArrowApply arr) => Representable (Arr arr) where
  type Arr arr % a = arr () a
  index :: forall a b. Arr arr a b -> a ~> (Arr arr % b)
index (Arr arr a b
a) a
b = (() -> a) -> arr () a
forall b c. (b -> c) -> arr b c
forall (a :: CAT Type) b c. Arrow a => (b -> c) -> a b c
arr (\() -> a
b) arr () a -> arr a b -> arr () b
forall {k} (cat :: k -> k -> Type) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> arr a b
a
  tabulate :: forall b a. Ob b => (a ~> (Arr arr % b)) -> Arr arr a b
tabulate a ~> (Arr arr % b)
f = arr a b -> Arr arr a b
forall (arr :: CAT Type) a b. arr a b -> Arr arr a b
Arr ((a -> (arr () b, ())) -> arr a (arr () b, ())
forall b c. (b -> c) -> arr b c
forall (a :: CAT Type) b c. Arrow a => (b -> c) -> a b c
arr (\a
a -> (a ~> (Arr arr % b)
a -> arr () b
f a
a, ())) arr a (arr () b, ()) -> arr (arr () b, ()) b -> arr a b
forall {k} (cat :: k -> k -> Type) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> arr (arr () b, ()) b
forall b c. arr (arr b c, b) c
forall (a :: CAT Type) b c. ArrowApply a => a (a b c, b) c
app)
  repMap :: forall a b. (a ~> b) -> (Arr arr % a) ~> (Arr arr % b)
repMap a ~> b
f arr () a
a = arr () a
a arr () a -> arr a b -> arr () b
forall {k} (cat :: k -> k -> Type) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> (a -> b) -> arr a b
forall b c. (b -> c) -> arr b c
forall (a :: CAT Type) b c. Arrow a => (b -> c) -> a b c
arr a ~> b
a -> b
f

instance (Functor m) => Profunctor (Kleisli m) where
  dimap :: forall c a b d.
(c ~> a) -> (b ~> d) -> Kleisli m a b -> Kleisli m c d
dimap c ~> a
l b ~> d
r (Kleisli a -> m b
a) = (c -> m d) -> Kleisli m c d
forall (m :: Type -> Type) a b. (a -> m b) -> Kleisli m a b
Kleisli ((b -> d) -> m b -> m d
forall a b. (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap b ~> d
b -> d
r (m b -> m d) -> (c -> m b) -> c -> m d
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 -> m b
a (a -> m b) -> (c -> a) -> c -> m b
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 ~> a
c -> a
l)

instance (Monad m) => Promonad (Kleisli m) where
  id :: forall a. Ob a => Kleisli m a a
id = (a -> a) -> Kleisli m a a
forall b c. (b -> c) -> Kleisli m b c
forall (a :: CAT Type) b c. Arrow a => (b -> c) -> a b c
arr a -> a
forall a. Ob a => a -> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id
  Kleisli m b c
f . :: forall b c a. Kleisli m b c -> Kleisli m a b -> Kleisli m a c
. Kleisli m a b
g = Kleisli m a b
g Kleisli m a b -> Kleisli m b c -> Kleisli m a c
forall {k} (cat :: k -> k -> Type) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> Kleisli m b c
f

instance (Monad m) => Strong Tensor (Kleisli m) where
  act :: forall a x y.
Ob a =>
Kleisli m x y -> Kleisli m (Act Tensor a x) (Act Tensor a y)
act = Kleisli m x y -> Kleisli m (a, x) (a, y)
Kleisli m x y -> Kleisli m (Tensor % '(a, x)) (Tensor % '(a, y))
forall b c d. Kleisli m b c -> Kleisli m (d, b) (d, c)
forall (a :: CAT Type) b c d. Arrow a => a b c -> a (d, b) (d, c)
second

instance (MonadPlus m) => Strong CoprodAction (Kleisli m) where
  act :: forall (a :: COPROD Type) x y.
Ob a =>
Kleisli m x y
-> Kleisli m (Act CoprodAction a x) (Act CoprodAction a y)
act (Kleisli x -> m y
a) = (Either (UN 'COPR a) x -> m (Either (UN 'COPR a) y))
-> Kleisli m (Either (UN 'COPR a) x) (Either (UN 'COPR a) y)
forall (m :: Type -> Type) a b. (a -> m b) -> Kleisli m a b
Kleisli ((Either (UN 'COPR a) y -> m (Either (UN 'COPR a) y)
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Either (UN 'COPR a) y -> m (Either (UN 'COPR a) y))
-> (UN 'COPR a -> Either (UN 'COPR a) y)
-> UN 'COPR a
-> m (Either (UN 'COPR a) y)
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
. UN 'COPR a -> Either (UN 'COPR a) y
forall a b. a -> Either a b
Left) (UN 'COPR a -> m (Either (UN 'COPR a) y))
-> (x -> m (Either (UN 'COPR a) y))
-> Either (UN 'COPR a) x
-> m (Either (UN 'COPR a) y)
forall b d c. (b -> d) -> (c -> d) -> Either b c -> d
forall (a :: CAT Type) b d c.
ArrowChoice a =>
a b d -> a c d -> a (Either b c) d
||| (x -> m y
a (x -> m y)
-> (m y -> m (Either (UN 'COPR a) y))
-> x
-> m (Either (UN 'COPR a) y)
forall {k} (cat :: k -> k -> Type) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> (y -> Either (UN 'COPR a) y) -> m y -> m (Either (UN 'COPR a) y)
forall a b. (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap y -> Either (UN 'COPR a) y
forall a b. b -> Either a b
Right))

instance (MonadFix m) => Costrong Tensor (Kleisli m) where
  coact :: forall a x y.
(Ob a, Ob x, Ob y) =>
Kleisli m (Act Tensor a x) (Act Tensor a y) -> Kleisli m x y
coact Kleisli m (Act Tensor a x) (Act Tensor a y)
f = Kleisli m (x, a) (y, a) -> Kleisli m x y
forall b d c. Kleisli m (b, d) (c, d) -> Kleisli m b c
forall (a :: CAT Type) b d c.
ArrowLoop a =>
a (b, d) (c, d) -> a b c
loop (((x, a) -> (a, x)) -> Kleisli m (x, a) (a, x)
forall b c. (b -> c) -> Kleisli m b c
forall (a :: CAT Type) b c. Arrow a => (b -> c) -> a b c
arr (x, a) -> (a, x)
forall b a. (b, a) -> (a, b)
swap Kleisli m (x, a) (a, x)
-> Kleisli m (a, x) (y, a) -> Kleisli m (x, a) (y, a)
forall {k} (cat :: k -> k -> Type) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> Kleisli m (a, x) (a, y)
Kleisli m (Act Tensor a x) (Act Tensor a y)
f Kleisli m (a, x) (a, y)
-> Kleisli m (a, y) (y, a) -> Kleisli m (a, x) (y, a)
forall {k} (cat :: k -> k -> Type) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> ((a, y) -> (y, a)) -> Kleisli m (a, y) (y, a)
forall b c. (b -> c) -> Kleisli m b c
forall (a :: CAT Type) b c. Arrow a => (b -> c) -> a b c
arr (a, y) -> (y, a)
forall b a. (b, a) -> (a, b)
swap)

instance (Monad m) => MonoidalProfunctor (Kleisli m) where
  one :: Kleisli m Unit Unit
one = (() -> ()) -> Kleisli m () ()
forall b c. (b -> c) -> Kleisli m b c
forall (a :: CAT Type) b c. Arrow a => (b -> c) -> a b c
arr () -> ()
forall a. Ob a => a -> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id
  Kleisli m x1 x2
l ** :: forall x1 x2 y1 y2.
Kleisli m x1 x2
-> Kleisli m y1 y2 -> Kleisli m (x1 ** y1) (x2 ** y2)
** Kleisli m y1 y2
r = Kleisli m x1 x2
l Kleisli m x1 x2 -> Kleisli m y1 y2 -> Kleisli m (x1, y1) (x2, y2)
forall b c b' c'.
Kleisli m b c -> Kleisli m b' c' -> Kleisli m (b, b') (c, c')
forall (a :: CAT Type) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** Kleisli m y1 y2
r

instance (MonadPlus m) => MonoidalProfunctor (Coprod (Kleisli m)) where
  one :: Coprod (Kleisli m) Unit Unit
one = Kleisli m Void Void -> Coprod (Kleisli m) ('COPR Void) ('COPR Void)
forall {j} {k} (p :: j +-> k) (a1 :: k) (b1 :: j).
p a1 b1 -> Coprod p ('COPR a1) ('COPR b1)
Coprod ((Void -> m Void) -> Kleisli m Void Void
forall (m :: Type -> Type) a b. (a -> m b) -> Kleisli m a b
Kleisli Void -> m Void
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return)
  Coprod (Kleisli a1 -> m b1
l) ** :: forall (x1 :: COPROD Type) (x2 :: COPROD Type) (y1 :: COPROD Type)
       (y2 :: COPROD Type).
Coprod (Kleisli m) x1 x2
-> Coprod (Kleisli m) y1 y2
-> Coprod (Kleisli m) (x1 ** y1) (x2 ** y2)
** Coprod (Kleisli a1 -> m b1
r) = Kleisli m (Either a1 a1) (Either b1 b1)
-> Coprod (Kleisli m) ('COPR (Either a1 a1)) ('COPR (Either b1 b1))
forall {j} {k} (p :: j +-> k) (a1 :: k) (b1 :: j).
p a1 b1 -> Coprod p ('COPR a1) ('COPR b1)
Coprod ((Either a1 a1 -> m (Either b1 b1))
-> Kleisli m (Either a1 a1) (Either b1 b1)
forall (m :: Type -> Type) a b. (a -> m b) -> Kleisli m a b
Kleisli ((a1 -> m b1
l (a1 -> m b1)
-> (m b1 -> m (Either b1 b1)) -> a1 -> m (Either b1 b1)
forall {k} (cat :: k -> k -> Type) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> (b1 -> Either b1 b1) -> m b1 -> m (Either b1 b1)
forall a b. (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap b1 -> Either b1 b1
forall a b. a -> Either a b
Left) (a1 -> m (Either b1 b1))
-> (a1 -> m (Either b1 b1)) -> Either a1 a1 -> m (Either b1 b1)
forall b d c. (b -> d) -> (c -> d) -> Either b c -> d
forall (a :: CAT Type) b d c.
ArrowChoice a =>
a b d -> a c d -> a (Either b c) d
||| (a1 -> m b1
r (a1 -> m b1)
-> (m b1 -> m (Either b1 b1)) -> a1 -> m (Either b1 b1)
forall {k} (cat :: k -> k -> Type) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> (b1 -> Either b1 b1) -> m b1 -> m (Either b1 b1)
forall a b. (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap b1 -> Either b1 b1
forall a b. b -> Either a b
Right)))

instance (Functor m) => Representable (Kleisli m) where
  type Kleisli m % a = m a
  index :: forall a b. Kleisli m a b -> a ~> (Kleisli m % b)
index = Kleisli m a b -> a ~> (Kleisli m % b)
Kleisli m a b -> a -> m b
forall (m :: Type -> Type) a b. Kleisli m a b -> a -> m b
runKleisli
  tabulate :: forall b a. Ob b => (a ~> (Kleisli m % b)) -> Kleisli m a b
tabulate = (a ~> (Kleisli m % b)) -> Kleisli m a b
(a -> m b) -> Kleisli m a b
forall (m :: Type -> Type) a b. (a -> m b) -> Kleisli m a b
Kleisli
  repMap :: forall a b. (a ~> b) -> (Kleisli m % a) ~> (Kleisli m % b)
repMap = (a ~> b) -> (Kleisli m % a) ~> (Kleisli m % b)
(a -> b) -> m a -> m b
forall a b. (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap

instance (Promonad p) => P.Category (FromProfunctor p :: Type +-> Type) where
  id :: forall a. FromProfunctor p a a
id = FromProfunctor p a a
forall a. Ob a => FromProfunctor p a a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id
  . :: forall b c a.
FromProfunctor p b c
-> FromProfunctor p a b -> FromProfunctor p a c
(.) = FromProfunctor p b c
-> FromProfunctor p a b -> FromProfunctor p a c
forall b c a.
FromProfunctor p b c
-> FromProfunctor p a b -> FromProfunctor p a c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
(.)

instance (MonoidalProfunctor p, Promonad p) => Arrow (FromProfunctor p :: Type +-> Type) where
  arr :: forall b c. (b -> c) -> FromProfunctor p b c
arr b -> c
f = (b ~> c) -> FromProfunctor p b b -> FromProfunctor p b c
forall b d a.
(b ~> d) -> FromProfunctor p a b -> FromProfunctor p a d
forall {j} {k} (p :: j +-> k) (b :: j) (d :: j) (a :: k).
Profunctor p =>
(b ~> d) -> p a b -> p a d
rmap b ~> c
b -> c
f FromProfunctor p b b
forall a. Ob a => FromProfunctor p a a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id
  FromProfunctor p b c
f *** :: forall b c b' c'.
FromProfunctor p b c
-> FromProfunctor p b' c' -> FromProfunctor p (b, b') (c, c')
*** FromProfunctor p b' c'
g = p (b, b') (c, c') -> FromProfunctor p (b, b') (c, c')
forall {k} {k1} (p :: k -> k1 -> Type) (a :: k) (b :: k1).
p a b -> FromProfunctor p a b
FromProfunctor (p b c
f p b c -> p b' c' -> p (b ** b') (c ** c')
forall x1 x2 y1 y2. p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
** p b' c'
g)

instance (DistributiveProfunctor p, Promonad p) => ArrowChoice (FromProfunctor p :: Type +-> Type) where
  FromProfunctor p b c
f +++ :: forall b c b' c'.
FromProfunctor p b c
-> FromProfunctor p b' c'
-> FromProfunctor p (Either b b') (Either c c')
+++ FromProfunctor p b' c'
g = p (Either b b') (Either c c')
-> FromProfunctor p (Either b b') (Either c c')
forall {k} {k1} (p :: k -> k1 -> Type) (a :: k) (b :: k1).
p a b -> FromProfunctor p a b
FromProfunctor (p b c
f p b c -> p b' c' -> p (b || b') (c || c')
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) (c :: k2)
       (d :: k1).
MonoidalProfunctor (Coprod p) =>
p a b -> p c d -> p (a || c) (b || d)
++ p b' c'
g)

instance (Representable p, MonoidalProfunctor p, Promonad p) => ArrowApply (FromProfunctor p :: Type +-> Type) where
  app :: forall b c. FromProfunctor p (FromProfunctor p b c, b) c
app = p (FromProfunctor p b c, b) c
-> FromProfunctor p (FromProfunctor p b c, b) c
forall {k} {k1} (p :: k -> k1 -> Type) (a :: k) (b :: k1).
p a b -> FromProfunctor p a b
FromProfunctor (((FromProfunctor p b c, b) ~> (p % c))
-> p (FromProfunctor p b c, b) c
forall b a. Ob b => (a ~> (p % b)) -> p a b
forall {j} {k} (p :: j +-> k) (b :: j) (a :: k).
(Representable p, Ob b) =>
(a ~> (p % b)) -> p a b
tabulate \(FromProfunctor p b c
p, b
b) -> p b c -> b ~> (p % c)
forall a b. p a b -> a ~> (p % b)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Representable p =>
p a b -> a ~> (p % b)
index p b c
p b
b)

instance (Costrong Tensor p, MonoidalProfunctor p, Promonad p) => ArrowLoop (FromProfunctor p :: Type +-> Type) where
  loop :: forall b d c.
FromProfunctor p (b, d) (c, d) -> FromProfunctor p b c
loop (FromProfunctor p (b, d) (c, d)
p) = p b c -> FromProfunctor p b c
forall {k} {k1} (p :: k -> k1 -> Type) (a :: k) (b :: k1).
p a b -> FromProfunctor p a b
FromProfunctor (forall {m} {k} (t :: (m, k) +-> k) (p :: k +-> k) (a :: m) (x :: k)
       (y :: k).
(Costrong t p, Ob a, Ob x, Ob y) =>
p (Act t a x) (Act t a y) -> p x y
forall (t :: (Type, Type) +-> Type) (p :: CAT Type) a x y.
(Costrong t p, Ob a, Ob x, Ob y) =>
p (Act t a x) (Act t a y) -> p x y
coact @Tensor (((d, b) ~> (b, d))
-> ((c, d) ~> (d, c)) -> p (b, d) (c, d) -> p (d, b) (d, c)
forall c a b d. (c ~> a) -> (b ~> d) -> p a b -> p c d
forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j) (d :: j).
Profunctor p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimap (d, b) ~> (b, d)
(d, b) -> (b, d)
forall b a. (b, a) -> (a, b)
swap (c, d) ~> (d, c)
(c, d) -> (d, c)
forall b a. (b, a) -> (a, b)
swap p (b, d) (c, d)
p))