{-# LANGUAGE AllowAmbiguousTypes #-}
{-# OPTIONS_GHC -Wno-orphans #-}

module Proarrow.Category.Monoidal.Applicative where

import Control.Applicative qualified as P
import Data.Function (($))
import Data.Kind (Constraint, Type)
import Data.List.NonEmpty qualified as P
import Prelude qualified as P

import Proarrow.Category.Monoidal (Monoidal (..), MonoidalProfunctor (..), first, leftUnitorInvWith)
import Proarrow.Category.Monoidal.Distributive (Distributive, DistributiveProfunctor)
import Proarrow.Core (CategoryOf (..), Profunctor (..), Promonad (..), type (+->))
import Proarrow.Functor (FromProfunctor (..), Functor (..), Prelude (..))
import Proarrow.Monoid (Comonoid (..))
import Proarrow.Object.BinaryCoproduct (COPROD (..), HasBinaryCoproducts (..), copar, copar0, unCoprod)
import Proarrow.Object.Exponential (Closed (..))
import Proarrow.Object.Initial (HasInitialObject (..))
import Proarrow.Profunctor.Identity (Id (..))

type Applicative :: forall {j} {k}. (j -> k) -> Constraint
class (Monoidal j, Monoidal k, Functor f) => Applicative (f :: j -> k) where
  pure :: Unit ~> a -> Unit ~> f a
  liftA2 :: (Ob a, Ob b) => (a ** b ~> c) -> f a ** f b ~> f c

ap :: forall {j} {k} f a b. (Applicative (f :: j -> k), Closed j, Closed k, Ob a, Ob b) => f (a ~~> b) ~> f a ~~> f b
ap :: forall {j} {k} (f :: j -> k) (a :: j) (b :: j).
(Applicative f, Closed j, Closed k, Ob a, Ob b) =>
f (a ~~> b) ~> (f a ~~> f b)
ap = forall k (a :: k) (b :: k) r.
(Closed k, Ob a, Ob b) =>
(Ob (a ~~> b) => r) -> r
withObExp @j @a @b ((Ob (a ~~> b) => f (a ~~> b) ~> (f a ~~> f b))
 -> f (a ~~> b) ~> (f a ~~> f b))
-> (Ob (a ~~> b) => f (a ~~> b) ~> (f a ~~> f b))
-> f (a ~~> b) ~> (f a ~~> f b)
forall a b. (a -> b) -> a -> b
$ forall k (a :: k) (b :: k) (c :: k).
(Closed k, Ob a, Ob b) =>
((a ** b) ~> c) -> a ~> (b ~~> c)
curry @k @_ @(f a) @(f b) (forall {j} {k} (f :: j -> k) (a :: j) (b :: j) (c :: j).
(Applicative f, Ob a, Ob b) =>
((a ** b) ~> c) -> (f a ** f b) ~> f c
forall (f :: j -> k) (a :: j) (b :: j) (c :: j).
(Applicative f, Ob a, Ob b) =>
((a ** b) ~> c) -> (f a ** f b) ~> f c
liftA2 @f @(a ~~> b) @a (forall k (a :: k) (b :: k).
(Closed k, Ob a, Ob b) =>
((a ~~> b) ** a) ~> b
apply @j @a))

fmapDefault :: forall f a b. (Applicative f) => a ~> b -> f a ~> f b
fmapDefault :: forall {j} {k} (f :: j -> k) (a :: j) (b :: j).
Applicative f =>
(a ~> b) -> f a ~> f b
fmapDefault a ~> b
f = forall {j} {k} (f :: j -> k) (a :: j) (b :: j) (c :: j).
(Applicative f, Ob a, Ob b) =>
((a ** b) ~> c) -> (f a ** f b) ~> f c
forall (f :: j -> k) (a :: j) (b :: j) (c :: j).
(Applicative f, Ob a, Ob b) =>
((a ** b) ~> c) -> (f a ** f b) ~> f c
liftA2 @_ @Unit @a (a ~> b
f (a ~> b) -> ((Unit ** a) ~> a) -> (Unit ** a) ~> b
forall (b :: j) (c :: j) (a :: j). (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
. forall k (a :: k). (Monoidal k, Ob a) => (Unit ** a) ~> a
leftUnitor @_ @a) ((f Unit ** f a) ~> f b) -> (f a ~> (f Unit ** f a)) -> f a ~> f b
forall (b :: k) (c :: k) (a :: k). (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
. (Unit ~> f Unit) -> f a ~> (f Unit ** f a)
forall {k} (a :: k) (b :: k).
(Monoidal k, Ob a) =>
(Unit ~> b) -> a ~> (b ** a)
leftUnitorInvWith (forall {j} {k} (f :: j -> k) (a :: j).
Applicative f =>
(Unit ~> a) -> Unit ~> f a
forall (f :: j -> k) (a :: j).
Applicative f =>
(Unit ~> a) -> Unit ~> f a
pure @f Unit ~> Unit
forall (a :: j). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id) ((Ob a, Ob b) => f a ~> f b) -> (a ~> b) -> f a ~> f b
forall (a :: j) (b :: j) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ a ~> b
f

liftA3 :: forall f a b c d. (Applicative f, Ob a, Ob b, Ob c) => (a ** b ** c ~> d) -> f a ** f b ** f c ~> f d
liftA3 :: forall {j} {k} (f :: j -> k) (a :: j) (b :: j) (c :: j) (d :: j).
(Applicative f, Ob a, Ob b, Ob c) =>
(((a ** b) ** c) ~> d) -> ((f a ** f b) ** f c) ~> f d
liftA3 ((a ** b) ** c) ~> d
f = forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @a @b (forall {j} {k} (f :: j -> k) (a :: j) (b :: j) (c :: j).
(Applicative f, Ob a, Ob b) =>
((a ** b) ~> c) -> (f a ** f b) ~> f c
forall (f :: j -> k) (a :: j) (b :: j) (c :: j).
(Applicative f, Ob a, Ob b) =>
((a ** b) ~> c) -> (f a ** f b) ~> f c
liftA2 @_ @(a ** b) @c ((a ** b) ** c) ~> d
f ((f (a ** b) ** f c) ~> f d)
-> (((f a ** f b) ** f c) ~> (f (a ** b) ** f c))
-> ((f a ** f b) ** f c) ~> f d
forall (b :: k) (c :: k) (a :: k). (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
. forall (c :: k) (a :: k) (b :: k).
(Monoidal k, Ob c) =>
(a ~> b) -> (a ** c) ~> (b ** c)
forall {k} (c :: k) (a :: k) (b :: k).
(Monoidal k, Ob c) =>
(a ~> b) -> (a ** c) ~> (b ** c)
first @(f c) (forall {j} {k} (f :: j -> k) (a :: j) (b :: j) (c :: j).
(Applicative f, Ob a, Ob b) =>
((a ** b) ~> c) -> (f a ** f b) ~> f c
forall (f :: j -> k) (a :: j) (b :: j) (c :: j).
(Applicative f, Ob a, Ob b) =>
((a ** b) ~> c) -> (f a ** f b) ~> f c
liftA2 @f @a @b (a ** b) ~> (a ** b)
forall (a :: j). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id))

instance (MonoidalProfunctor (p :: j +-> k), Comonoid x) => Applicative (FromProfunctor p x) where
  pure :: forall (a :: j). (Unit ~> a) -> Unit ~> FromProfunctor p x a
pure Unit ~> a
a () = p x a -> FromProfunctor p x a
forall {k} {k1} (p :: k -> k1 -> Type) (a :: k) (b :: k1).
p a b -> FromProfunctor p a b
FromProfunctor (p x a -> FromProfunctor p x a) -> p x a -> FromProfunctor p x a
forall a b. (a -> b) -> a -> b
$ (x ~> Unit) -> (Unit ~> a) -> p Unit Unit -> p x a
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 x ~> Unit
forall {k} (c :: k). Comonoid c => c ~> Unit
counit Unit ~> a
a p Unit Unit
forall {j} {k} (p :: j +-> k). MonoidalProfunctor p => p Unit Unit
par0
  liftA2 :: forall (a :: j) (b :: j) (c :: j).
(Ob a, Ob b) =>
((a ** b) ~> c)
-> (FromProfunctor p x a ** FromProfunctor p x b)
   ~> FromProfunctor p x c
liftA2 (a ** b) ~> c
abc (FromProfunctor p x a
pxa, FromProfunctor p x b
pxb) = p x c -> FromProfunctor p x c
forall {k} {k1} (p :: k -> k1 -> Type) (a :: k) (b :: k1).
p a b -> FromProfunctor p a b
FromProfunctor (p x c -> FromProfunctor p x c) -> p x c -> FromProfunctor p x c
forall a b. (a -> b) -> a -> b
$ (x ~> (x ** x)) -> ((a ** b) ~> c) -> p (x ** x) (a ** b) -> p x c
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 x ~> (x ** x)
forall {k} (c :: k). Comonoid c => c ~> (c ** c)
comult (a ** b) ~> c
abc (p x a
pxa p x a -> p x b -> p (x ** x) (a ** b)
forall (x1 :: k) (x2 :: j) (y1 :: k) (y2 :: j).
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)
`par` p x b
pxb)
instance (MonoidalProfunctor (p :: Type +-> Type)) => P.Applicative (FromProfunctor p x) where
  pure :: forall a. a -> FromProfunctor p x a
pure a
a = (Unit ~> a) -> Unit ~> FromProfunctor p x a
forall a. (Unit ~> a) -> Unit ~> FromProfunctor p x a
forall {j} {k} (f :: j -> k) (a :: j).
Applicative f =>
(Unit ~> a) -> Unit ~> f a
pure (\() -> a
a) ()
  liftA2 :: forall a b c.
(a -> b -> c)
-> FromProfunctor p x a
-> FromProfunctor p x b
-> FromProfunctor p x c
liftA2 a -> b -> c
f = ((FromProfunctor p x a ** FromProfunctor p x b)
 ~> FromProfunctor p x c)
-> FromProfunctor p x a
   ~> (FromProfunctor p x b ~~> FromProfunctor p x c)
forall k (a :: k) (b :: k) (c :: k).
(Closed k, Ob a, Ob b) =>
((a ** b) ~> c) -> a ~> (b ~~> c)
forall a b c. (Ob a, Ob b) => ((a ** b) ~> c) -> a ~> (b ~~> c)
curry (((a ** b) ~> c)
-> (FromProfunctor p x a ** FromProfunctor p x b)
   ~> FromProfunctor p x c
forall a b c.
(Ob a, Ob b) =>
((a ** b) ~> c)
-> (FromProfunctor p x a ** FromProfunctor p x b)
   ~> FromProfunctor p x c
forall {j} {k} (f :: j -> k) (a :: j) (b :: j) (c :: j).
(Applicative f, Ob a, Ob b) =>
((a ** b) ~> c) -> (f a ** f b) ~> f c
liftA2 ((a -> b -> c) -> (a, b) -> c
forall a b c. (a -> b -> c) -> (a, b) -> c
P.uncurry a -> b -> c
f))

instance (P.Applicative f) => Applicative (Prelude f) where
  pure :: forall a. (Unit ~> a) -> Unit ~> Prelude f a
pure Unit ~> a
a () = f a -> Prelude f a
forall (f :: Type -> Type) a. 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 (Unit ~> a
() -> a
a ()))
  liftA2 :: forall a b c.
(Ob a, Ob b) =>
((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 (f :: Type -> Type) a. 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 []
deriving via Prelude (P.Either e) instance Applicative (P.Either e)
deriving via Prelude P.IO instance Applicative P.IO
deriving via Prelude P.Maybe instance Applicative P.Maybe
deriving via Prelude P.NonEmpty instance Applicative P.NonEmpty

type Alternative :: forall {j} {k}. (j -> k) -> Constraint
class (Distributive j, Functor f) => Alternative (f :: j -> k) where
  empty :: (Ob a) => Unit ~> f a
  alt :: (Ob a, Ob b) => (a || b ~> c) -> f a ** f b ~> f c

-- Note: Comonoid (COPR x) means we need x ~> InitialObject.
instance (DistributiveProfunctor (p :: j +-> k), Distributive j, Comonoid (COPR x)) => Alternative (FromProfunctor p x) where
  empty :: forall (a :: j). Ob a => Unit ~> FromProfunctor p x a
empty () = p x a -> FromProfunctor p x a
forall {k} {k1} (p :: k -> k1 -> Type) (a :: k) (b :: k1).
p a b -> FromProfunctor p a b
FromProfunctor ((x ~> InitialObject)
-> (InitialObject ~> a) -> p InitialObject InitialObject -> p x a
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 (Id x InitialObject -> x ~> InitialObject
forall k (a :: k) (b :: k). Id a b -> a ~> b
unId (Coprod Id ('COPR x) ('COPR InitialObject) -> Id x InitialObject
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Coprod p ('COPR a) ('COPR b) -> p a b
unCoprod (forall {k} (c :: k). Comonoid c => c ~> Unit
forall (c :: COPROD k). Comonoid c => c ~> Unit
counit @(COPR x)))) InitialObject ~> a
forall (a :: j). Ob a => InitialObject ~> a
forall k (a :: k). (HasInitialObject k, Ob a) => InitialObject ~> a
initiate (forall {j} {k} (p :: j +-> k).
MonoidalProfunctor (Coprod p) =>
p InitialObject InitialObject
forall (p :: j +-> k).
MonoidalProfunctor (Coprod p) =>
p InitialObject InitialObject
copar0 @p))
  alt :: forall (a :: j) (b :: j) (c :: j).
(Ob a, Ob b) =>
((a || b) ~> c)
-> (FromProfunctor p x a ** FromProfunctor p x b)
   ~> FromProfunctor p x c
alt (a || b) ~> c
abc (FromProfunctor p x a
pxa, FromProfunctor p x b
pyb) =
    p x c -> FromProfunctor p x c
forall {k} {k1} (p :: k -> k1 -> Type) (a :: k) (b :: k1).
p a b -> FromProfunctor p a b
FromProfunctor (p x c -> FromProfunctor p x c) -> p x c -> FromProfunctor p x c
forall a b. (a -> b) -> a -> b
$ (x ~> (x || x)) -> ((a || b) ~> c) -> p (x || x) (a || b) -> p x c
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 (Id x (x || x) -> x ~> (x || x)
forall k (a :: k) (b :: k). Id a b -> a ~> b
unId (Coprod Id ('COPR x) ('COPR (x || x)) -> Id x (x || x)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Coprod p ('COPR a) ('COPR b) -> p a b
unCoprod (forall {k} (c :: k). Comonoid c => c ~> (c ** c)
forall (c :: COPROD k). Comonoid c => c ~> (c ** c)
comult @(COPR x)))) (a || b) ~> c
abc (p x a
pxa p x a -> p x b -> p (x || x) (a || b)
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)
`copar` p x b
pyb)

instance (P.Alternative f) => Alternative (Prelude f) where
  empty :: forall a. Ob a => Unit ~> Prelude f a
empty () = f a -> Prelude f a
forall (f :: Type -> Type) a. 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.
(Ob a, Ob b) =>
((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 (f :: Type -> Type) a. 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)

deriving via Prelude [] instance Alternative []
deriving via Prelude P.Maybe instance Alternative P.Maybe
deriving via Prelude P.IO instance Alternative P.IO