{-# 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