module Proarrow.Category.Instance.Ap where

import Control.Applicative (liftA3)
import Data.Kind (Type)
import Prelude qualified as P

import Proarrow.Core (CategoryOf (..), Is, Profunctor (..), Promonad (..), UN, type (+->))
import Proarrow.Object.BinaryProduct (HasBinaryProducts (..))
import Proarrow.Object.Initial (HasInitialObject (..))
import Proarrow.Object.Terminal (HasTerminalObject (..))
import Proarrow.Object.BinaryCoproduct (HasBinaryCoproducts (..))

type data AP (f :: Type -> Type) k = A k
type instance UN A (A k) = k

type Ap :: (j +-> k) -> AP f j +-> AP f k
data Ap p a b where
  Ap :: forall {j} {k} a b f p. (Ob a, Ob b) => {forall {j} {k} (a :: j) (b :: k) (f :: Type -> Type)
       (p :: k +-> j).
Ap p (A a) (A b) -> f (p a b)
unAp :: f (p a b)} -> Ap p (A a :: AP f j) (A b :: AP f k)

instance (P.Applicative f, Profunctor p) => Profunctor (Ap (p :: j +-> k) :: AP f j +-> AP f k) where
  dimap :: forall (c :: AP f k) (a :: AP f k) (b :: AP f j) (d :: AP f j).
(c ~> a) -> (b ~> d) -> Ap p a b -> Ap p c d
dimap (Ap f (a ~> b)
l) (Ap f (a ~> b)
r) (Ap f (p a b)
x) = f (p a b) -> Ap p (A a) (A b)
forall {j} {k} (a :: j) (b :: k) (f :: Type -> Type)
       (p :: k +-> j).
(Ob a, Ob b) =>
f (p a b) -> Ap p (A a) (A b)
Ap (((a ~> b) -> (a ~> b) -> p a b -> p a b)
-> f (a ~> b) -> f (a ~> b) -> f (p a b) -> f (p a b)
forall (f :: Type -> Type) a b c d.
Applicative f =>
(a -> b -> c -> d) -> f a -> f b -> f c -> f d
liftA3 (a ~> b) -> (a ~> b) -> p a b -> p a b
(a ~> a) -> (b ~> b) -> p a b -> p a b
forall (c :: k) (a :: k) (b :: j) (d :: j).
(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 f (a ~> b)
l f (a ~> b)
r f (p a b)
x)
  (Ob a, Ob b) => r
r \\ :: forall (a :: AP f k) (b :: AP f j) r.
((Ob a, Ob b) => r) -> Ap p a b -> r
\\ Ap{} = r
(Ob a, Ob b) => r
r
instance (P.Applicative f, Promonad p) => Promonad (Ap (p :: k +-> k) :: AP f k +-> AP f k) where
  id :: forall (a :: AP f k). Ob a => Ap p a a
id = f (p (UN A a) (UN A a)) -> Ap p (A (UN A a)) (A (UN A a))
forall {j} {k} (a :: j) (b :: k) (f :: Type -> Type)
       (p :: k +-> j).
(Ob a, Ob b) =>
f (p a b) -> Ap p (A a) (A b)
Ap (p (UN A a) (UN A a) -> f (p (UN A a) (UN A a))
forall a. a -> f a
forall (f :: Type -> Type) a. Applicative f => a -> f a
P.pure p (UN A a) (UN A a)
forall (a :: k). Ob a => p a a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id)
  Ap f (p a b)
f . :: forall (b :: AP f k) (c :: AP f k) (a :: AP f k).
Ap p b c -> Ap p a b -> Ap p a c
. Ap f (p a b)
g = f (p a b) -> Ap p (A a) (A b)
forall {j} {k} (a :: j) (b :: k) (f :: Type -> Type)
       (p :: k +-> j).
(Ob a, Ob b) =>
f (p a b) -> Ap p (A a) (A b)
Ap ((p a b -> p a a -> p a b) -> f (p a b) -> f (p a a) -> f (p a b)
forall a b c. (a -> b -> c) -> f a -> f b -> f c
forall (f :: Type -> Type) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
P.liftA2 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 :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
(.) f (p a b)
f f (p a a)
f (p a b)
g)
instance (P.Applicative f, CategoryOf k) => CategoryOf (AP f k) where
  type (~>) = Ap (~>)
  type Ob a = (Is A a, Ob (UN A a))

instance (P.Applicative f, HasInitialObject k) => HasInitialObject (AP f k) where
  type InitialObject = A InitialObject
  initiate :: forall (a :: AP f k). Ob a => InitialObject ~> a
initiate = f (InitialObject ~> UN A a)
-> Ap (~>) (A InitialObject) (A (UN A a))
forall {j} {k} (a :: j) (b :: k) (f :: Type -> Type)
       (p :: k +-> j).
(Ob a, Ob b) =>
f (p a b) -> Ap p (A a) (A b)
Ap ((InitialObject ~> UN A a) -> f (InitialObject ~> UN A a)
forall a. a -> f a
forall (f :: Type -> Type) a. Applicative f => a -> f a
P.pure InitialObject ~> UN A a
forall (a :: k). Ob a => InitialObject ~> a
forall k (a :: k). (HasInitialObject k, Ob a) => InitialObject ~> a
initiate)
instance (P.Applicative f, HasTerminalObject k) => HasTerminalObject (AP f k) where
  type TerminalObject = A TerminalObject
  terminate :: forall (a :: AP f k). Ob a => a ~> TerminalObject
terminate = f (UN A a ~> TerminalObject)
-> Ap (~>) (A (UN A a)) (A TerminalObject)
forall {j} {k} (a :: j) (b :: k) (f :: Type -> Type)
       (p :: k +-> j).
(Ob a, Ob b) =>
f (p a b) -> Ap p (A a) (A b)
Ap ((UN A a ~> TerminalObject) -> f (UN A a ~> TerminalObject)
forall a. a -> f a
forall (f :: Type -> Type) a. Applicative f => a -> f a
P.pure UN A a ~> TerminalObject
forall (a :: k). Ob a => a ~> TerminalObject
forall k (a :: k).
(HasTerminalObject k, Ob a) =>
a ~> TerminalObject
terminate)
instance (P.Applicative f, HasBinaryProducts k) => HasBinaryProducts (AP f k) where
  type a && b = A (UN A a && UN A b)
  withObProd :: forall (a :: AP f k) (b :: AP f k) r.
(Ob a, Ob b) =>
(Ob (a && b) => r) -> r
withObProd @(A a) @(A b) Ob (a && b) => r
r = forall k (a :: k) (b :: k) r.
(HasBinaryProducts k, Ob a, Ob b) =>
(Ob (a && b) => r) -> r
withObProd @k @a @b r
Ob (UN A a && UN A b) => r
Ob (a && b) => r
r
  fst :: forall (a :: AP f k) (b :: AP f k). (Ob a, Ob b) => (a && b) ~> a
fst @(A a) @(A b) = forall k (a :: k) (b :: k) r.
(HasBinaryProducts k, Ob a, Ob b) =>
(Ob (a && b) => r) -> r
withObProd @k @a @b ((Ob (UN A a && UN A b) => (a && b) ~> a) -> (a && b) ~> a)
-> (Ob (UN A a && UN A b) => (a && b) ~> a) -> (a && b) ~> a
forall a b. (a -> b) -> a -> b
P.$ f ((UN A a && UN A b) ~> UN A a)
-> Ap (~>) (A (UN A a && UN A b)) (A (UN A a))
forall {j} {k} (a :: j) (b :: k) (f :: Type -> Type)
       (p :: k +-> j).
(Ob a, Ob b) =>
f (p a b) -> Ap p (A a) (A b)
Ap (((UN A a && UN A b) ~> UN A a) -> f ((UN A a && UN A b) ~> UN A a)
forall a. a -> f a
forall (f :: Type -> Type) a. Applicative f => a -> f a
P.pure (forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> a
fst @_ @a @b))
  snd :: forall (a :: AP f k) (b :: AP f k). (Ob a, Ob b) => (a && b) ~> b
snd @(A a) @(A b) = forall k (a :: k) (b :: k) r.
(HasBinaryProducts k, Ob a, Ob b) =>
(Ob (a && b) => r) -> r
withObProd @k @a @b ((Ob (UN A a && UN A b) => (a && b) ~> b) -> (a && b) ~> b)
-> (Ob (UN A a && UN A b) => (a && b) ~> b) -> (a && b) ~> b
forall a b. (a -> b) -> a -> b
P.$ f ((UN A a && UN A b) ~> UN A b)
-> Ap (~>) (A (UN A a && UN A b)) (A (UN A b))
forall {j} {k} (a :: j) (b :: k) (f :: Type -> Type)
       (p :: k +-> j).
(Ob a, Ob b) =>
f (p a b) -> Ap p (A a) (A b)
Ap (((UN A a && UN A b) ~> UN A b) -> f ((UN A a && UN A b) ~> UN A b)
forall a. a -> f a
forall (f :: Type -> Type) a. Applicative f => a -> f a
P.pure (forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> b
snd @_ @a @b))
  Ap @al @bl f (a ~> b)
f &&& :: forall (a :: AP f k) (x :: AP f k) (y :: AP f k).
(a ~> x) -> (a ~> y) -> a ~> (x && y)
&&& Ap @ar @br f (a ~> b)
g = forall k (a :: k) (b :: k) r.
(HasBinaryProducts k, Ob a, Ob b) =>
(Ob (a && b) => r) -> r
withObProd @k @al @ar ((Ob (a && a) => a ~> (x && y)) -> a ~> (x && y))
-> (Ob (a && a) => a ~> (x && y)) -> a ~> (x && y)
forall a b. (a -> b) -> a -> b
P.$ forall k (a :: k) (b :: k) r.
(HasBinaryProducts k, Ob a, Ob b) =>
(Ob (a && b) => r) -> r
withObProd @k @bl @br ((Ob (b && b) => a ~> (x && y)) -> a ~> (x && y))
-> (Ob (b && b) => a ~> (x && y)) -> a ~> (x && y)
forall a b. (a -> b) -> a -> b
P.$ f (a ~> (b && b)) -> Ap (~>) (A a) (A (b && b))
forall {j} {k} (a :: j) (b :: k) (f :: Type -> Type)
       (p :: k +-> j).
(Ob a, Ob b) =>
f (p a b) -> Ap p (A a) (A b)
Ap (((a ~> b) -> (a ~> b) -> a ~> (b && b))
-> f (a ~> b) -> f (a ~> b) -> f (a ~> (b && b))
forall a b c. (a -> b -> c) -> f a -> f b -> f c
forall (f :: Type -> Type) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
P.liftA2 (a ~> b) -> (a ~> b) -> a ~> (b && b)
(a ~> b) -> (a ~> b) -> a ~> (b && b)
forall (a :: k) (x :: k) (y :: k).
(a ~> x) -> (a ~> y) -> a ~> (x && y)
forall k (a :: k) (x :: k) (y :: k).
HasBinaryProducts k =>
(a ~> x) -> (a ~> y) -> a ~> (x && y)
(&&&) f (a ~> b)
f f (a ~> b)
g)
instance (P.Applicative f, HasBinaryCoproducts k) => HasBinaryCoproducts (AP f k) where
  type a || b = A (UN A a || UN A b)
  withObCoprod :: forall (a :: AP f k) (b :: AP f k) r.
(Ob a, Ob b) =>
(Ob (a || b) => r) -> r
withObCoprod @(A a) @(A b) Ob (a || b) => r
r = forall k (a :: k) (b :: k) r.
(HasBinaryCoproducts k, Ob a, Ob b) =>
(Ob (a || b) => r) -> r
withObCoprod @k @a @b r
Ob (UN A a || UN A b) => r
Ob (a || b) => r
r
  lft :: forall (a :: AP f k) (b :: AP f k). (Ob a, Ob b) => a ~> (a || b)
lft @(A a) @(A b) = forall k (a :: k) (b :: k) r.
(HasBinaryCoproducts k, Ob a, Ob b) =>
(Ob (a || b) => r) -> r
withObCoprod @k @a @b ((Ob (UN A a || UN A b) => a ~> (a || b)) -> a ~> (a || b))
-> (Ob (UN A a || UN A b) => a ~> (a || b)) -> a ~> (a || b)
forall a b. (a -> b) -> a -> b
P.$ f (UN A a ~> (UN A a || UN A b))
-> Ap (~>) (A (UN A a)) (A (UN A a || UN A b))
forall {j} {k} (a :: j) (b :: k) (f :: Type -> Type)
       (p :: k +-> j).
(Ob a, Ob b) =>
f (p a b) -> Ap p (A a) (A b)
Ap ((UN A a ~> (UN A a || UN A b)) -> f (UN A a ~> (UN A a || UN A b))
forall a. a -> f a
forall (f :: Type -> Type) a. Applicative f => a -> f a
P.pure (forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
a ~> (a || b)
lft @_ @a @b))
  rgt :: forall (a :: AP f k) (b :: AP f k). (Ob a, Ob b) => b ~> (a || b)
rgt @(A a) @(A b) = forall k (a :: k) (b :: k) r.
(HasBinaryCoproducts k, Ob a, Ob b) =>
(Ob (a || b) => r) -> r
withObCoprod @k @a @b ((Ob (UN A a || UN A b) => b ~> (a || b)) -> b ~> (a || b))
-> (Ob (UN A a || UN A b) => b ~> (a || b)) -> b ~> (a || b)
forall a b. (a -> b) -> a -> b
P.$ f (UN A b ~> (UN A a || UN A b))
-> Ap (~>) (A (UN A b)) (A (UN A a || UN A b))
forall {j} {k} (a :: j) (b :: k) (f :: Type -> Type)
       (p :: k +-> j).
(Ob a, Ob b) =>
f (p a b) -> Ap p (A a) (A b)
Ap ((UN A b ~> (UN A a || UN A b)) -> f (UN A b ~> (UN A a || UN A b))
forall a. a -> f a
forall (f :: Type -> Type) a. Applicative f => a -> f a
P.pure (forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
b ~> (a || b)
rgt @_ @a @b))
  Ap @al @bl f (a ~> b)
f ||| :: forall (x :: AP f k) (a :: AP f k) (y :: AP f k).
(x ~> a) -> (y ~> a) -> (x || y) ~> a
||| Ap @ar @br f (a ~> b)
g = forall k (a :: k) (b :: k) r.
(HasBinaryCoproducts k, Ob a, Ob b) =>
(Ob (a || b) => r) -> r
withObCoprod @k @al @ar ((Ob (a || a) => (x || y) ~> a) -> (x || y) ~> a)
-> (Ob (a || a) => (x || y) ~> a) -> (x || y) ~> a
forall a b. (a -> b) -> a -> b
P.$ forall k (a :: k) (b :: k) r.
(HasBinaryCoproducts k, Ob a, Ob b) =>
(Ob (a || b) => r) -> r
withObCoprod @k @bl @br ((Ob (b || b) => (x || y) ~> a) -> (x || y) ~> a)
-> (Ob (b || b) => (x || y) ~> a) -> (x || y) ~> a
forall a b. (a -> b) -> a -> b
P.$ f ((a || a) ~> b) -> Ap (~>) (A (a || a)) (A b)
forall {j} {k} (a :: j) (b :: k) (f :: Type -> Type)
       (p :: k +-> j).
(Ob a, Ob b) =>
f (p a b) -> Ap p (A a) (A b)
Ap (((a ~> b) -> (a ~> b) -> (a || a) ~> b)
-> f (a ~> b) -> f (a ~> b) -> f ((a || a) ~> b)
forall a b c. (a -> b -> c) -> f a -> f b -> f c
forall (f :: Type -> Type) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
P.liftA2 (a ~> b) -> (a ~> b) -> (a || a) ~> b
(a ~> b) -> (a ~> b) -> (a || a) ~> b
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
(|||) f (a ~> b)
f f (a ~> b)
g)