{-# LANGUAGE AllowAmbiguousTypes #-}
module Proarrow.Category.Monoidal.Applicative where

import Data.Kind (Constraint)
import Data.Function (($))
import Prelude qualified as P
import Control.Applicative qualified as P

import Proarrow.Core (Promonad(..), CategoryOf(..), (//), lmap, Profunctor (..), PRO, obj)
import Proarrow.Functor (Functor(..), Prelude (..))
import Proarrow.Object.Terminal (El, terminate)
import Proarrow.Object.BinaryCoproduct (HasBinaryCoproducts(..), HasCoproducts, COPROD (..), Coprod (..), lft, rgt)
import Proarrow.Object.BinaryProduct (HasBinaryProducts (..), HasProducts, PROD (..), Prod (..), fst, snd)
import Proarrow.Profunctor.Star (Star(..))
import Proarrow.Category.Monoidal (MonoidalProfunctor (..))


type Applicative :: forall {j} {k}. (j -> k) -> Constraint
class (HasProducts j, HasProducts k, Functor f) => Applicative (f :: j -> k) where
  pure :: El a -> El (f a)
  liftA2 :: (a && b ~> c) -> f a && f b ~> f c

instance P.Applicative f => Applicative (Prelude f) where
  pure :: forall a. El a -> El (Prelude f a)
pure El a
a () = f a -> Prelude f a
forall {k} (f :: k -> Type) (a :: k). f a -> Prelude f a
Prelude (a -> f a
forall a. a -> f a
forall (f :: Type -> Type) a. Applicative f => a -> f a
P.pure (El a
() -> a
a ()))
  liftA2 :: forall a b c.
((a && b) ~> c) -> (Prelude f a && Prelude f b) ~> Prelude f c
liftA2 (a && b) ~> c
f (Prelude f a
fa, Prelude f b
fb) = f c -> Prelude f c
forall {k} (f :: k -> Type) (a :: k). f a -> Prelude f a
Prelude ((a -> b -> c) -> f a -> f b -> f c
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) -> c) -> a -> b -> c
forall a b c. ((a, b) -> c) -> a -> b -> c
P.curry (a && b) ~> c
(a, b) -> c
f) f a
fa f b
fb)

deriving via Prelude ((,) a) instance P.Monoid a => Applicative ((,) a)
deriving via Prelude ((->) a) instance Applicative ((->) a)
deriving via Prelude [] instance Applicative []


class Profunctor p => Proapplicative p where
  pureP :: Ob a => El b -> p a b
  apP :: p a b -> p a c -> p a (b && c)

instance Applicative f => Proapplicative (Star f) where
  pureP :: forall (a :: j) (b :: k). Ob a => El b -> Star f a b
pureP El b
b = El b
b El b -> ((Ob TerminalObject, Ob b) => Star f a b) -> Star f a b
forall {k1} {k2} (p :: PRO k1 k2) (a :: k1) (b :: k2) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
// (a ~> f b) -> Star f a b
forall {k1} {k2} (b :: k1) (a :: k2) (f :: k1 -> k2).
Ob b =>
(a ~> f b) -> Star f a b
Star ((a ~> TerminalObject) -> (TerminalObject ~> f b) -> a ~> f 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 a ~> TerminalObject
forall {k} (a :: k).
(HasTerminalObject k, Ob a) =>
a ~> TerminalObject
terminate (El b -> TerminalObject ~> f b
forall (a :: k). El a -> El (f a)
forall {j} {k} (f :: j -> k) (a :: j).
Applicative f =>
El a -> El (f a)
pure El b
b))
  apP :: forall (a :: j) (b :: k) (c :: k).
Star f a b -> Star f a c -> Star f a (b && c)
apP (Star @b a ~> f b
f) (Star @c a ~> f c
g) =
    let bc :: (b && c) ~> (b && c)
bc = forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @b Obj b -> (c ~> c) -> (b && c) ~> (b && c)
forall (a :: k) (b :: k) (x :: k) (y :: k).
(a ~> x) -> (b ~> y) -> (a && b) ~> (x && y)
forall k (a :: k) (b :: k) (x :: k) (y :: k).
HasBinaryProducts k =>
(a ~> x) -> (b ~> y) -> (a && b) ~> (x && y)
*** forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @c
    in (b && c) ~> (b && c)
bc ((b && c) ~> (b && c))
-> ((Ob (b && c), Ob (b && c)) => Star f a (b && c))
-> Star f a (b && c)
forall {k1} {k2} (p :: PRO k1 k2) (a :: k1) (b :: k2) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
// (a ~> f (b && c)) -> Star f a (b && c)
forall {k1} {k2} (b :: k1) (a :: k2) (f :: k1 -> k2).
Ob b =>
(a ~> f b) -> Star f a b
Star (forall {j} {k} (f :: j -> k) (a :: j) (b :: j) (c :: j).
Applicative f =>
((a && b) ~> c) -> (f a && f b) ~> f c
forall (f :: k -> j) (a :: k) (b :: k) (c :: k).
Applicative f =>
((a && b) ~> c) -> (f a && f b) ~> f c
liftA2 @f @b @c (b && c) ~> (b && c)
bc ((f b && f c) ~> f (b && c))
-> (a ~> (f b && f c)) -> a ~> f (b && c)
forall (b :: j) (c :: j) (a :: j). (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 ~> f b
f (a ~> f b) -> (a ~> f c) -> a ~> (f b && f c)
forall (a :: j) (x :: j) (y :: j).
(a ~> x) -> (a ~> y) -> a ~> (x && y)
forall k (a :: k) (x :: k) (y :: k).
HasBinaryProducts k =>
(a ~> x) -> (a ~> y) -> a ~> (x && y)
&&& a ~> f c
g))

type App :: PRO j k -> PRO (PROD j) (PROD k)
data App p a b where
  App :: p a b -> App p (PR a) (PR b)
instance Profunctor p => Profunctor (App p) where
  dimap :: forall (c :: PROD j) (a :: PROD j) (b :: PROD k) (d :: PROD k).
(c ~> a) -> (b ~> d) -> App p a b -> App p c d
dimap (Prod UN 'PR c ~> UN 'PR a
l) (Prod UN 'PR b ~> UN 'PR d
r) (App p a b
p) = p (UN 'PR c) (UN 'PR d) -> App p ('PR (UN 'PR c)) ('PR (UN 'PR d))
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k).
p a b -> App p ('PR a) ('PR b)
App ((UN 'PR c ~> a)
-> (b ~> UN 'PR d) -> p a b -> p (UN 'PR c) (UN 'PR d)
forall (c :: j) (a :: j) (b :: k) (d :: k).
(c ~> a) -> (b ~> d) -> p a b -> p c d
forall {j} {k} (p :: PRO j k) (c :: j) (a :: j) (b :: k) (d :: k).
Profunctor p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimap UN 'PR c ~> a
UN 'PR c ~> UN 'PR a
l b ~> UN 'PR d
UN 'PR b ~> UN 'PR d
r p a b
p)
  (Ob a, Ob b) => r
r \\ :: forall (a :: PROD j) (b :: PROD k) r.
((Ob a, Ob b) => r) -> App p a b -> r
\\ App 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 :: 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
instance (HasProducts j, HasProducts k, Proapplicative p) => MonoidalProfunctor (App (p :: PRO j k)) where
  lift0 :: App p Unit Unit
lift0 = p TerminalObject TerminalObject
-> App p ('PR TerminalObject) ('PR TerminalObject)
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k).
p a b -> App p ('PR a) ('PR b)
App (El TerminalObject -> p TerminalObject TerminalObject
forall (a :: j) (b :: k). Ob a => El b -> p a b
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k).
(Proapplicative p, Ob a) =>
El b -> p a b
pureP El TerminalObject
forall (a :: k). Ob a => a ~> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id)
  lift2 :: forall (x1 :: PROD j) (x2 :: PROD k) (y1 :: PROD j) (y2 :: PROD k).
App p x1 x2 -> App p y1 y2 -> App p (x1 ** y1) (x2 ** y2)
lift2 (App @_ @a1 p a b
p) (App @_ @a2 p a b
q) = p (a && a) (b && b) -> App p ('PR (a && a)) ('PR (b && b))
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k).
p a b -> App p ('PR a) ('PR b)
App (p (a && a) b -> p (a && a) b -> p (a && a) (b && b)
forall (a :: j) (b :: k) (c :: k). p a b -> p a c -> p a (b && c)
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) (c :: k).
Proapplicative p =>
p a b -> p a c -> p a (b && c)
apP (((a && a) ~> a) -> p a b -> p (a && a) 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 (forall (a :: j) (b :: j).
(HasBinaryProducts j, Ob a, Ob b) =>
(a && b) ~> a
forall {k} (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> a
fst @a1 @a2) p a b
p) (((a && a) ~> a) -> p a b -> p (a && a) 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 (forall (a :: j) (b :: j).
(HasBinaryProducts j, Ob a, Ob b) =>
(a && b) ~> b
forall {k} (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> b
snd @a1 @a2) p a b
q)) ((Ob a, Ob b) => App p ('PR (a && a)) ('PR (b && b)))
-> p a b -> App p ('PR (a && a)) ('PR (b && b))
forall (a :: j) (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 ((Ob a, Ob b) => App p ('PR (a && a)) ('PR (b && b)))
-> p a b -> App p ('PR (a && a)) ('PR (b && b))
forall (a :: j) (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
q



type Alternative :: forall {j} {k}. (j -> k) -> Constraint
class (HasCoproducts j, Applicative f) => Alternative (f :: j -> k) where
  empty :: El (f a)
  alt :: (a || b ~> c) -> f a && f b ~> f c

instance P.Alternative f => Alternative (Prelude f) where
  empty :: forall a. El (Prelude f a)
empty () = f a -> Prelude f a
forall {k} (f :: k -> Type) (a :: k). f a -> Prelude f a
Prelude f a
forall a. f a
forall (f :: Type -> Type) a. Alternative f => f a
P.empty
  alt :: forall a b c.
((a || b) ~> c) -> (Prelude f a && Prelude f b) ~> Prelude f c
alt (a || b) ~> c
abc (Prelude f a
fl, Prelude f b
fr) = f c -> Prelude f c
forall {k} (f :: k -> Type) (a :: k). f a -> Prelude f a
Prelude ((Either a b -> c) -> f (Either a b) -> f c
forall a b. (a -> b) -> f a -> f b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
P.fmap (a || b) ~> c
Either a b -> c
abc (f (Either a b) -> f c) -> f (Either a b) -> f c
forall a b. (a -> b) -> a -> b
$ (a -> Either a b) -> f a -> f (Either a b)
forall a b. (a -> b) -> f a -> f b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
P.fmap a -> Either a b
forall a b. a -> Either a b
P.Left f a
fl f (Either a b) -> f (Either a b) -> f (Either a b)
forall a. f a -> f a -> f a
forall (f :: Type -> Type) a. Alternative f => f a -> f a -> f a
P.<|> (b -> Either a b) -> f b -> f (Either a b)
forall a b. (a -> b) -> f a -> f b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
P.fmap b -> Either a b
forall a b. b -> Either a b
P.Right f b
fr)


class Proapplicative p => Proalternative p where
  emptyP :: (Ob a, Ob b) => p a b
  altP :: p a b -> p a b -> p a b

instance Alternative f => Proalternative (Star f) where
  emptyP :: forall (a :: j) (b :: k). (Ob a, Ob b) => Star f a b
emptyP = (a ~> f b) -> Star f a b
forall {k1} {k2} (b :: k1) (a :: k2) (f :: k1 -> k2).
Ob b =>
(a ~> f b) -> Star f a b
Star (El (f b)
forall (a :: k). El (f a)
forall {j} {k} (f :: j -> k) (a :: j). Alternative f => El (f a)
empty El (f b) -> (a ~> TerminalObject) -> a ~> f b
forall (b :: j) (c :: j) (a :: j). (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 ~> TerminalObject
forall {k} (a :: k).
(HasTerminalObject k, Ob a) =>
a ~> TerminalObject
terminate)
  altP :: forall (a :: j) (b :: k). Star f a b -> Star f a b -> Star f a b
altP (Star @b a ~> f b
f) (Star a ~> f b
g) =
    let bb :: (b || b) ~> b
bb = forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @b Obj b -> Obj b -> (b || b) ~> 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
||| forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @b
    in (b || b) ~> b
bb ((b || b) ~> b)
-> ((Ob (b || b), Ob b) => Star f a b) -> Star f a b
forall {k1} {k2} (p :: PRO k1 k2) (a :: k1) (b :: k2) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
// (a ~> f b) -> Star f a b
forall {k1} {k2} (b :: k1) (a :: k2) (f :: k1 -> k2).
Ob b =>
(a ~> f b) -> Star f a b
Star (forall {j} {k} (f :: j -> k) (a :: j) (b :: j) (c :: j).
Alternative f =>
((a || b) ~> c) -> (f a && f b) ~> f c
forall (f :: k -> j) (a :: k) (b :: k) (c :: k).
Alternative f =>
((a || b) ~> c) -> (f a && f b) ~> f c
alt @f @b @b (b || b) ~> b
bb ((f b && f b) ~> f b) -> (a ~> (f b && f b)) -> a ~> f b
forall (b :: j) (c :: j) (a :: j). (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 ~> f b
f (a ~> f b) -> (a ~> f b) -> a ~> (f b && f b)
forall (a :: j) (x :: j) (y :: j).
(a ~> x) -> (a ~> y) -> a ~> (x && y)
forall k (a :: k) (x :: k) (y :: k).
HasBinaryProducts k =>
(a ~> x) -> (a ~> y) -> a ~> (x && y)
&&& a ~> f b
g))

type Alt :: PRO j k -> PRO (PROD j) (COPROD k)
data Alt p a b where
  Alt :: p a b -> Alt p (PR a) (COPR b)
instance Profunctor p => Profunctor (Alt p) where
  dimap :: forall (c :: PROD j) (a :: PROD j) (b :: COPROD k) (d :: COPROD k).
(c ~> a) -> (b ~> d) -> Alt p a b -> Alt p c d
dimap (Prod UN 'PR c ~> UN 'PR a
l) (Coprod UN 'COPR b ~> UN 'COPR d
r) (Alt p a b
p) = p (UN 'PR c) (UN 'COPR d)
-> Alt p ('PR (UN 'PR c)) ('COPR (UN 'COPR d))
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k).
p a b -> Alt p ('PR a) ('COPR b)
Alt ((UN 'PR c ~> a)
-> (b ~> UN 'COPR d) -> p a b -> p (UN 'PR c) (UN 'COPR d)
forall (c :: j) (a :: j) (b :: k) (d :: k).
(c ~> a) -> (b ~> d) -> p a b -> p c d
forall {j} {k} (p :: PRO j k) (c :: j) (a :: j) (b :: k) (d :: k).
Profunctor p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimap UN 'PR c ~> a
UN 'PR c ~> UN 'PR a
l b ~> UN 'COPR d
UN 'COPR b ~> UN 'COPR d
r p a b
p)
  (Ob a, Ob b) => r
r \\ :: forall (a :: PROD j) (b :: COPROD k) r.
((Ob a, Ob b) => r) -> Alt p a b -> r
\\ Alt 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 :: 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
instance (HasProducts j, HasCoproducts k, Proalternative p) => MonoidalProfunctor (Alt (p :: PRO j k)) where
  lift0 :: Alt p Unit Unit
lift0 = p TerminalObject InitialObject
-> Alt p ('PR TerminalObject) ('COPR InitialObject)
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k).
p a b -> Alt p ('PR a) ('COPR b)
Alt p TerminalObject InitialObject
forall (a :: j) (b :: k). (Ob a, Ob b) => p a b
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k).
(Proalternative p, Ob a, Ob b) =>
p a b
emptyP
  lift2 :: forall (x1 :: PROD j) (x2 :: COPROD k) (y1 :: PROD j)
       (y2 :: COPROD k).
Alt p x1 x2 -> Alt p y1 y2 -> Alt p (x1 ** y1) (x2 ** y2)
lift2 (Alt @_ @a1 @b1 p a b
p) (Alt @_ @a2 @b2 p a b
q) = p (a && a) (b || b) -> Alt p ('PR (a && a)) ('COPR (b || b))
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k).
p a b -> Alt p ('PR a) ('COPR b)
Alt (p (a && a) (b || b) -> p (a && a) (b || b) -> p (a && a) (b || b)
forall (a :: j) (b :: k). p a b -> p a b -> p a b
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k).
Proalternative p =>
p a b -> p a b -> p a b
altP (((a && a) ~> a) -> (b ~> (b || b)) -> p a b -> p (a && a) (b || b)
forall (c :: j) (a :: j) (b :: k) (d :: k).
(c ~> a) -> (b ~> d) -> p a b -> p c d
forall {j} {k} (p :: PRO j k) (c :: j) (a :: j) (b :: k) (d :: k).
Profunctor p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimap (forall (a :: j) (b :: j).
(HasBinaryProducts j, Ob a, Ob b) =>
(a && b) ~> a
forall {k} (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> a
fst @a1 @a2) (forall (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
a ~> (a || b)
forall {k} (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
a ~> (a || b)
lft @b1 @b2) p a b
p) (((a && a) ~> a) -> (b ~> (b || b)) -> p a b -> p (a && a) (b || b)
forall (c :: j) (a :: j) (b :: k) (d :: k).
(c ~> a) -> (b ~> d) -> p a b -> p c d
forall {j} {k} (p :: PRO j k) (c :: j) (a :: j) (b :: k) (d :: k).
Profunctor p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimap (forall (a :: j) (b :: j).
(HasBinaryProducts j, Ob a, Ob b) =>
(a && b) ~> b
forall {k} (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> b
snd @a1 @a2) (forall (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
b ~> (a || b)
forall {k} (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
b ~> (a || b)
rgt @b1 @b2) p a b
q)) ((Ob a, Ob b) => Alt p ('PR (a && a)) ('COPR (b || b)))
-> p a b -> Alt p ('PR (a && a)) ('COPR (b || b))
forall (a :: j) (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 ((Ob a, Ob b) => Alt p ('PR (a && a)) ('COPR (b || b)))
-> p a b -> Alt p ('PR (a && a)) ('COPR (b || b))
forall (a :: j) (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
q