{-# LANGUAGE AllowAmbiguousTypes #-}

module Proarrow.Category.Monoidal.Applicative where

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

import Proarrow.Category.Monoidal (Monoidal (..), MonoidalProfunctor (..))
import Proarrow.Category.Monoidal.Distributive (Distributive, DistributiveProfunctor)
import Proarrow.Core (CategoryOf (..), Profunctor (..), type (+->))
import Proarrow.Functor (FromProfunctor (..), Functor (..), Prelude (..))
import Proarrow.Monoid (Comonoid (..))
import Proarrow.Object.Initial (HasInitialObject (..))
import Proarrow.Object.BinaryCoproduct (HasBinaryCoproducts (..), COPROD(..), copar, copar0, unCoprod)
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

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 (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 {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 (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 {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 []
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 {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.
(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 {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)

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