{-# LANGUAGE AllowAmbiguousTypes #-}

module Proarrow.Category.Monoidal.Applicative where

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

import Proarrow.Category.Monoidal (MonoidalProfunctor (..))
import Proarrow.Core (CategoryOf (..), Profunctor (..), type (+->))
import Proarrow.Functor (FromProfunctor (..), Functor (..), Prelude (..))
import Proarrow.Object.BinaryCoproduct (HasBinaryCoproducts (..), HasCoproducts)
import Proarrow.Object.BinaryProduct (Cartesian, HasBinaryProducts (..), HasProducts, diag)
import Proarrow.Object.Terminal (El, terminate)

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 :: (Ob a, Ob b) => (a && b ~> c) -> f a && f b ~> f c

instance (MonoidalProfunctor (p :: j +-> k), Ob x, Cartesian j, Cartesian k) => Applicative (FromProfunctor p x) where
  pure :: forall (a :: j). El a -> El (FromProfunctor p x a)
pure El 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 ~> TerminalObject)
-> El a -> p TerminalObject TerminalObject -> 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 :: PRO j k) (c :: j) (a :: j) (b :: k) (d :: k).
Profunctor p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimap x ~> TerminalObject
forall (a :: k). Ob a => a ~> TerminalObject
forall k (a :: k).
(HasTerminalObject k, Ob a) =>
a ~> TerminalObject
terminate El a
a p Unit Unit
p TerminalObject TerminalObject
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 :: PRO j k) (c :: j) (a :: j) (b :: k) (d :: k).
Profunctor p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimap x ~> (x && x)
forall {k} (a :: k). (HasBinaryProducts k, Ob a) => a ~> (a && a)
diag (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. 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.
(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.Maybe instance Applicative P.Maybe

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

-- TODO: only works without Applicative as superclass of Alternative. This needs Distributive.
-- instance (MonoidalProfunctor (p :: j +-> k), Ob (x :: k), Cocartesian j, Cartesian k) => Alternative (FromProfunctor p x) where
--   empty () = FromProfunctor $ dimap terminate initiate par0
--   alt abc (FromProfunctor pxa, FromProfunctor pxb) = FromProfunctor $ dimap diag abc (pxa `par` pxb)

instance (P.Alternative f) => Alternative (Prelude f) where
  empty :: forall a. Ob 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.
(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 []