{-# OPTIONS_GHC -Wno-orphans #-}

module Proarrow.Profunctor.Arrow where

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

import Proarrow.Category.Monoidal (MonoidalProfunctor (..))
import Proarrow.Category.Monoidal.Action (Costrong (..), Strong (..))
import Proarrow.Core (CAT, Profunctor (..), Promonad (..))
import Proarrow.Object.BinaryCoproduct (COPROD, Coprod (..))
import Proarrow.Object.BinaryProduct ()
import Proarrow.Profunctor.Identity (Id (..))
import Proarrow.Profunctor.Representable (Representable (..))

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 Type (Arr arr) where
  act :: forall a b x y.
(a ~> b) -> Arr arr x y -> Arr arr (Act a x) (Act b y)
act a ~> b
f (Arr arr x y
a) = arr (a, x) (b, y) -> Arr arr (a, x) (b, y)
forall (arr :: CAT Type) a b. arr a b -> Arr arr a b
Arr ((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 arr a b -> arr x y -> arr (a, x) (b, y)
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 x y
a)

instance (ArrowLoop arr) => Costrong Type (Arr arr) where
  coact :: forall a x y.
(Ob a, Ob x, Ob y) =>
Arr arr (Act a x) (Act a y) -> Arr arr x y
coact (Arr arr (Act a x) (Act 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 a x) (Act 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))
    where
      swap :: (b, a) -> (a, b)
swap ~(b
x, a
y) = (a
y, b
x)

instance (Arrow arr) => MonoidalProfunctor (Arr arr) where
  par0 :: Arr arr Unit Unit
par0 = 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 par :: forall x1 x2 y1 y2.
Arr arr x1 x2 -> Arr arr y1 y2 -> Arr arr (x1 ** y1) (x2 ** y2)
`par` 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
  par0 :: Coprod (Arr arr) Unit Unit
par0 = 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) par :: 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)
`par` 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 Type (Kleisli m) where
  act :: forall a b x y.
(a ~> b) -> Kleisli m x y -> Kleisli m (Act a x) (Act b y)
act a ~> b
f Kleisli m x y
a = (a -> b) -> Kleisli m a b
forall b c. (b -> c) -> Kleisli m b c
forall (a :: CAT Type) b c. Arrow a => (b -> c) -> a b c
arr a ~> b
a -> b
f Kleisli m a b -> Kleisli m x y -> Kleisli m (a, x) (b, y)
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 x y
a

instance (MonadPlus m) => Strong (COPROD Type) (Kleisli m) where
  act :: forall (a :: COPROD Type) (b :: COPROD Type) x y.
(a ~> b) -> Kleisli m x y -> Kleisli m (Act a x) (Act b y)
act (Coprod (Id a1 ~> b1
f)) (Kleisli x -> m y
a) = (Either a1 x -> m (Either b1 y))
-> Kleisli m (Either a1 x) (Either b1 y)
forall (m :: Type -> Type) a b. (a -> m b) -> Kleisli m a b
Kleisli ((a1 ~> b1
a1 -> b1
f (a1 -> b1) -> (b1 -> m (Either b1 y)) -> a1 -> m (Either b1 y)
forall {k} (cat :: k -> k -> Type) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> (Either b1 y -> m (Either b1 y)
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Either b1 y -> m (Either b1 y))
-> (b1 -> Either b1 y) -> b1 -> m (Either b1 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
. b1 -> Either b1 y
forall a b. a -> Either a b
Left)) (a1 -> m (Either b1 y))
-> (x -> m (Either b1 y)) -> Either a1 x -> m (Either b1 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 b1 y)) -> x -> m (Either b1 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 b1 y) -> m y -> m (Either b1 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 b1 y
forall a b. b -> Either a b
Right))

instance (MonadFix m) => Costrong Type (Kleisli m) where
  coact :: forall a x y.
(Ob a, Ob x, Ob y) =>
Kleisli m (Act a x) (Act a y) -> Kleisli m x y
coact Kleisli m (Act a x) (Act 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 a x) (Act 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)
    where
      swap :: (b, a) -> (a, b)
swap ~(b
x, a
y) = (a
y, b
x)

instance (Monad m) => MonoidalProfunctor (Kleisli m) where
  par0 :: Kleisli m Unit Unit
par0 = (() -> ()) -> 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 par :: forall x1 x2 y1 y2.
Kleisli m x1 x2
-> Kleisli m y1 y2 -> Kleisli m (x1 ** y1) (x2 ** y2)
`par` 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
  par0 :: Coprod (Kleisli m) Unit Unit
par0 = 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 Kleisli m Void Void
forall b c. Kleisli m b c
forall (a :: CAT Type) b c. ArrowZero a => a b c
zeroArrow
  Coprod (Kleisli a1 -> m b1
l) par :: 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)
`par` 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