Applicative.hs

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

-- | Lax monoidal functors between monoidal categories: 'Applicative' generalizes the Prelude class
-- with 'pure' and 'liftA2' stated via the tensor, and 'Alternative' adds coproduct structure over a
-- 'Proarrow.Category.Monoidal.Distributive.Distributive' base.
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.Closed (Closed (..))
import Proarrow.Category.Monoidal.Distributive (Distributive, DistributiveProfunctor)
import Proarrow.Colimit.BinaryCoproduct (COPROD (..), HasBinaryCoproducts (..), nil, unCoprod, (++))
import Proarrow.Colimit.Initial (HasInitialObject (..))
import Proarrow.Core (CategoryOf (..), Profunctor (..), Promonad (..), type (+->))
import Proarrow.Functor (FromProfunctor (..), Functor (..), Prelude (..))
import Proarrow.Monoid (Comonoid (..))

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 = withObExp @j @a @b $ curry @k @_ @(f a) @(f b) (liftA2 @f @(a ~~> b) @a (apply @j @a))

fmapDefault :: forall f a b. (Applicative f) => a ~> b -> f a ~> f b
fmapDefault f = liftA2 @_ @Unit @a (f . leftUnitor @_ @a) . leftUnitorInvWith (pure @f id) \\ 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 f = withOb2 @_ @a @b (liftA2 @_ @(a ** b) @c f . first @(f c) (liftA2 @f @a @b id))

instance (MonoidalProfunctor (p :: j +-> k), Comonoid x) => Applicative (FromProfunctor p x) where
  pure a () = FromProfunctor $ dimap counit a one
  liftA2 abc (FromProfunctor pxa, FromProfunctor pxb) = FromProfunctor $ dimap comult abc (pxa ** pxb)
instance (MonoidalProfunctor (p :: Type +-> Type)) => P.Applicative (FromProfunctor p x) where
  pure a = pure (\() -> a) ()
  liftA2 f = curry (liftA2 (P.uncurry f))

instance (P.Applicative f) => Applicative (Prelude f) where
  pure a () = Prelude (P.pure (a ()))
  liftA2 f (Prelude fa, Prelude fb) = Prelude (P.liftA2 (P.curry f) fa 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

-- Comonoid (COPR x) means we need x ~> InitialObject.
instance (DistributiveProfunctor (p :: j +-> k), Distributive j, Comonoid (COPR x)) => Alternative (FromProfunctor p x) where
  empty () = FromProfunctor (dimap (unCoprod (counit @(COPR x))) initiate (nil @p))
  alt abc (FromProfunctor pxa, FromProfunctor pyb) =
    FromProfunctor $ dimap (unCoprod (comult @(COPR x))) abc (pxa ++ pyb)

instance (P.Alternative f) => Alternative (Prelude f) where
  empty () = Prelude P.empty
  alt abc (Prelude fl, Prelude fr) = Prelude (P.fmap abc $ P.fmap P.Left fl P.<|> P.fmap P.Right fr)

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