{-# OPTIONS_GHC -fno-warn-orphans #-}

module Pandora.Paradigm.Primary.Algebraic (module Exports, Applicative_, Alternative_, Extractable_, ($>-), ($$>-), ($$$>-), (-<*>-), (*>-), forever_, (-+-), void, empty, point, extract) where

import Pandora.Paradigm.Primary.Algebraic.Exponential as Exports
import Pandora.Paradigm.Primary.Algebraic.Product as Exports
import Pandora.Paradigm.Primary.Algebraic.Sum as Exports
import Pandora.Paradigm.Primary.Algebraic.Zero as Exports
import Pandora.Paradigm.Primary.Algebraic.One as Exports

import Pandora.Pattern.Category (($))
import Pandora.Pattern.Functor.Covariant (Covariant ((-<$>-)), (-<$$>-), (-<$$$>-))
import Pandora.Pattern.Functor.Semimonoidal (Semimonoidal (multiply))
import Pandora.Pattern.Functor.Monoidal (Monoidal (unit), Unit)
import Pandora.Pattern.Functor.Comonad (Comonad)
import Pandora.Pattern.Functor.Traversable (Traversable ((<<-)))
import Pandora.Pattern.Functor.Adjoint (Adjoint ((-|), (|-)))
import Pandora.Paradigm.Primary.Functor.Proxy (Proxy (Proxy))
import Pandora.Paradigm.Primary.Transformer.Flip (Flip (Flip))

type instance Unit (:*:) = One
type instance Unit (:+:) = Zero

infixl 4 -<*>-

($>-) :: Covariant (->) (->) t => t a -> b -> t b
t a
x $>- :: t a -> b -> t b
$>- b
r = (b
r b -> a -> b
forall a b. a -> b -> a
!.) (a -> b) -> t a -> t b
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
-<$>- t a
x

($$>-) :: (Covariant (->) (->) t, Covariant (->) (->) u) => t (u a) -> b -> t (u b)
t (u a)
x $$>- :: t (u a) -> b -> t (u b)
$$>- b
r = (b
r b -> a -> b
forall a b. a -> b -> a
!.) (a -> b) -> t (u a) -> t (u b)
forall (t :: * -> *) (u :: * -> *) (category :: * -> * -> *) a b.
(Covariant category category u, Covariant category category t) =>
category a b -> category (t (u a)) (t (u b))
-<$$>- t (u a)
x

($$$>-) :: (Covariant (->) (->) t, Covariant (->) (->) u, Covariant (->) (->) v) => t (u (v a)) -> b -> t (u (v b))
t (u (v a))
x $$$>- :: t (u (v a)) -> b -> t (u (v b))
$$$>- b
r = (b
r b -> a -> b
forall a b. a -> b -> a
!.) (a -> b) -> t (u (v a)) -> t (u (v b))
forall (t :: * -> *) (u :: * -> *) (v :: * -> *)
       (category :: * -> * -> *) a b.
(Covariant category category t, Covariant category category u,
 Covariant category category v) =>
category a b -> category (t (u (v a))) (t (u (v b)))
-<$$$>- t (u (v a))
x

void :: Covariant (->) (->) t => t a -> t ()
void :: t a -> t ()
void t a
x = t a
x t a -> () -> t ()
forall (t :: * -> *) a b. Covariant (->) (->) t => t a -> b -> t b
$>- ()

instance Traversable (->) (->) ((:*:) s) where
	a -> u b
f <<- :: (a -> u b) -> (s :*: a) -> u (s :*: b)
<<- s :*: a
x = ((s :*: a) -> s
forall a b. (a :*: b) -> a
attached s :*: a
x s -> b -> s :*: b
forall s a. s -> a -> s :*: a
:*:) (b -> s :*: b) -> u b -> u (s :*: b)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
-<$>- a -> u b
f ((s :*: a) -> a
forall (t :: * -> *) a. Extractable_ t => t a -> a
extract s :*: a
x)

instance Adjoint (->) (->) ((:*:) s) ((->) s) where
	(-|) :: ((s :*: a) -> b) -> a -> (s -> b)
	(s :*: a) -> b
f -| :: ((s :*: a) -> b) -> a -> s -> b
-| a
x = \s
s -> (s :*: a) -> b
f ((s :*: a) -> b) -> (s :*: a) -> b
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ s
s s -> a -> s :*: a
forall s a. s -> a -> s :*: a
:*: a
x
	(|-) :: (a -> s -> b) -> (s :*: a) -> b
	a -> s -> b
f |- :: (a -> s -> b) -> (s :*: a) -> b
|- ~(s
s :*: a
x) = a -> s -> b
f a
x s
s

instance Semimonoidal (->) (:*:) (:*:) ((->) e) where
	multiply :: ((e -> a) :*: (e -> b)) -> e -> (a :*: b)
	multiply :: ((e -> a) :*: (e -> b)) -> e -> a :*: b
multiply (e -> a
g :*: e -> b
h) = \e
x -> e -> a
g e
x a -> b -> a :*: b
forall s a. s -> a -> s :*: a
:*: e -> b
h e
x

instance Semimonoidal (<--) (:*:) (:*:) ((->) e) where
	multiply :: ((e -> a) :*: (e -> b)) <-- (e -> a :*: b)
multiply = ((e -> a :*: b) -> (e -> a) :*: (e -> b))
-> ((e -> a) :*: (e -> b)) <-- (e -> a :*: b)
forall (v :: * -> * -> *) a e. v e a -> Flip v a e
Flip (((e -> a :*: b) -> (e -> a) :*: (e -> b))
 -> ((e -> a) :*: (e -> b)) <-- (e -> a :*: b))
-> ((e -> a :*: b) -> (e -> a) :*: (e -> b))
-> ((e -> a) :*: (e -> b)) <-- (e -> a :*: b)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ \e -> a :*: b
f -> (\e
e -> (a :*: b) -> a
forall a b. (a :*: b) -> a
attached ((a :*: b) -> a) -> (a :*: b) -> a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ e -> a :*: b
f e
e) (e -> a) -> (e -> b) -> (e -> a) :*: (e -> b)
forall s a. s -> a -> s :*: a
:*: (\e
e -> (a :*: b) -> b
forall (t :: * -> *) a. Extractable_ t => t a -> a
extract ((a :*: b) -> b) -> (a :*: b) -> b
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ e -> a :*: b
f e
e)

instance Semimonoidal (->) (:*:) (:+:) ((:+:) e) where
	multiply :: ((e :+: a) :*: (e :+: b)) -> e :+: a :+: b
	multiply :: ((e :+: a) :*: (e :+: b)) -> e :+: (a :+: b)
multiply (Option e
_ :*: Option e
e') = e -> e :+: (a :+: b)
forall s a. s -> s :+: a
Option e
e'
	multiply (Option e
_ :*: Adoption b
y) = (a :+: b) -> e :+: (a :+: b)
forall s a. a -> s :+: a
Adoption ((a :+: b) -> e :+: (a :+: b)) -> (a :+: b) -> e :+: (a :+: b)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ b -> a :+: b
forall s a. a -> s :+: a
Adoption b
y
	multiply (Adoption a
x :*: e :+: b
_) = (a :+: b) -> e :+: (a :+: b)
forall s a. a -> s :+: a
Adoption ((a :+: b) -> e :+: (a :+: b)) -> (a :+: b) -> e :+: (a :+: b)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ a -> a :+: b
forall s a. s -> s :+: a
Option a
x

instance Semimonoidal (->) (:*:) (:*:) ((:+:) e) where
	multiply :: ((e :+: a) :*: (e :+: b)) -> e :+: (a :*: b)
multiply (Adoption a
x :*: Adoption b
y) = (a :*: b) -> e :+: (a :*: b)
forall s a. a -> s :+: a
Adoption ((a :*: b) -> e :+: (a :*: b)) -> (a :*: b) -> e :+: (a :*: b)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ a
x a -> b -> a :*: b
forall s a. s -> a -> s :*: a
:*: b
y
	multiply (Option e
e :*: e :+: b
_) = e -> e :+: (a :*: b)
forall s a. s -> s :+: a
Option e
e
	multiply (e :+: a
_ :*: Option e
e) = e -> e :+: (a :*: b)
forall s a. s -> s :+: a
Option e
e

instance Monoidal (->) (->) (:*:) (:*:) ((:+:) e) where
	unit :: Proxy (:*:) -> (Unit (:*:) -> a) -> e :+: a
unit Proxy (:*:)
_ Unit (:*:) -> a
f = a -> e :+: a
forall s a. a -> s :+: a
Adoption (a -> e :+: a) -> a -> e :+: a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ Unit (:*:) -> a
f One
Unit (:*:)
One

instance Semimonoidal (<--) (:*:) (:*:) ((:*:) s) where
	multiply :: ((s :*: a) :*: (s :*: b)) <-- (s :*: (a :*: b))
multiply = ((s :*: (a :*: b)) -> (s :*: a) :*: (s :*: b))
-> ((s :*: a) :*: (s :*: b)) <-- (s :*: (a :*: b))
forall (v :: * -> * -> *) a e. v e a -> Flip v a e
Flip (((s :*: (a :*: b)) -> (s :*: a) :*: (s :*: b))
 -> ((s :*: a) :*: (s :*: b)) <-- (s :*: (a :*: b)))
-> ((s :*: (a :*: b)) -> (s :*: a) :*: (s :*: b))
-> ((s :*: a) :*: (s :*: b)) <-- (s :*: (a :*: b))
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ \(s
s :*: a
x :*: b
y) -> (s
s s -> a -> s :*: a
forall s a. s -> a -> s :*: a
:*: a
x) (s :*: a) -> (s :*: b) -> (s :*: a) :*: (s :*: b)
forall s a. s -> a -> s :*: a
:*: (s
s s -> b -> s :*: b
forall s a. s -> a -> s :*: a
:*: b
y)

instance Monoidal (<--) (->) (:*:) (:*:) ((:*:) s) where
	unit :: Proxy (:*:) -> (Unit (:*:) -> a) <-- (s :*: a)
unit Proxy (:*:)
_ = ((s :*: a) -> One -> a) -> Flip (->) (One -> a) (s :*: a)
forall (v :: * -> * -> *) a e. v e a -> Flip v a e
Flip (((s :*: a) -> One -> a) -> Flip (->) (One -> a) (s :*: a))
-> ((s :*: a) -> One -> a) -> Flip (->) (One -> a) (s :*: a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ \(s
_ :*: a
x) -> (\One
_ -> a
x)

instance Comonad ((:*:) s) (->) where

instance Semimonoidal (<--) (:*:) (:*:) (Flip (:*:) a) where
	multiply :: (Flip (:*:) a a :*: Flip (:*:) a b) <-- Flip (:*:) a (a :*: b)
multiply = (Flip (:*:) a (a :*: b) -> Flip (:*:) a a :*: Flip (:*:) a b)
-> (Flip (:*:) a a :*: Flip (:*:) a b) <-- Flip (:*:) a (a :*: b)
forall (v :: * -> * -> *) a e. v e a -> Flip v a e
Flip ((Flip (:*:) a (a :*: b) -> Flip (:*:) a a :*: Flip (:*:) a b)
 -> (Flip (:*:) a a :*: Flip (:*:) a b) <-- Flip (:*:) a (a :*: b))
-> (Flip (:*:) a (a :*: b) -> Flip (:*:) a a :*: Flip (:*:) a b)
-> (Flip (:*:) a a :*: Flip (:*:) a b) <-- Flip (:*:) a (a :*: b)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ \(Flip ((a
sx :*: b
sy) :*: a
r)) -> (a :*: a) -> Flip (:*:) a a
forall (v :: * -> * -> *) a e. v e a -> Flip v a e
Flip (a
sx a -> a -> a :*: a
forall s a. s -> a -> s :*: a
:*: a
r) Flip (:*:) a a
-> Flip (:*:) a b -> Flip (:*:) a a :*: Flip (:*:) a b
forall s a. s -> a -> s :*: a
:*: (b :*: a) -> Flip (:*:) a b
forall (v :: * -> * -> *) a e. v e a -> Flip v a e
Flip (b
sy b -> a -> b :*: a
forall s a. s -> a -> s :*: a
:*: a
r)

instance Monoidal (<--) (->) (:*:) (:*:) (Flip (:*:) a) where
	unit :: Proxy (:*:) -> (Unit (:*:) -> a) <-- Flip (:*:) a a
unit Proxy (:*:)
_ = (Flip (:*:) a a -> One -> a)
-> Flip (->) (One -> a) (Flip (:*:) a a)
forall (v :: * -> * -> *) a e. v e a -> Flip v a e
Flip ((Flip (:*:) a a -> One -> a)
 -> Flip (->) (One -> a) (Flip (:*:) a a))
-> (Flip (:*:) a a -> One -> a)
-> Flip (->) (One -> a) (Flip (:*:) a a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ \(Flip (a
s :*: a
_)) -> (\One
_ -> a
s)

type Applicative_ t = (Covariant (->) (->) t, Semimonoidal (->) (:*:) (:*:) t, Monoidal (->) (->) (:*:) (:*:) t)
type Alternative_ t = (Covariant (->) (->) t, Semimonoidal (->) (:*:) (:+:) t, Monoidal (->) (->) (:*:) (:+:) t)

(-<*>-) :: (Covariant (->) (->) t, Semimonoidal (->) (:*:) (:*:) t)
	=> t (a -> b) -> t a -> t b
t (a -> b)
f -<*>- :: t (a -> b) -> t a -> t b
-<*>- t a
x = (a -> (a -> b) -> b) -> ((a -> b) :*: a) -> b
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) (u :: * -> *) a b.
Adjoint source target t u =>
target a (u b) -> source (t a) b
(|-) @(->) @(->) a -> (a -> b) -> b
forall a b. a -> (a -> b) -> b
(&) (((a -> b) :*: a) -> b) -> t ((a -> b) :*: a) -> t b
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
-<$>- (t (a -> b) :*: t a) -> t ((a -> b) :*: a)
forall k (p :: * -> * -> *) (source :: * -> * -> *)
       (target :: k -> k -> k) (t :: k -> *) (a :: k) (b :: k).
Semimonoidal p source target t =>
p (source (t a) (t b)) (t (target a b))
multiply @_ @_ @(:*:) (t (a -> b)
f t (a -> b) -> t a -> t (a -> b) :*: t a
forall s a. s -> a -> s :*: a
:*: t a
x)

forever_ :: (Covariant (->) (->) t, Semimonoidal (->) (:*:) (:*:) t) => t a -> t b
forever_ :: t a -> t b
forever_ t a
x = let r :: t b
r = t a
x t a -> t b -> t b
forall (t :: * -> *) a b.
(Covariant (->) (->) t, Semimonoidal (->) (:*:) (:*:) t) =>
t a -> t b -> t b
*>- t b
r in t b
r

(*>-) :: (Covariant (->) (->) t, Semimonoidal (->) (:*:) (:*:) t) => t a -> t b -> t b
t a
x *>- :: t a -> t b -> t b
*>- t b
y = (b -> a -> b
forall a b. a -> b -> a
(!.) (b -> a -> b) -> a -> b -> b
forall a b c. (a -> b -> c) -> b -> a -> c
%) (a -> b -> b) -> t a -> t (b -> b)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
-<$>- t a
x t (b -> b) -> t b -> t b
forall (t :: * -> *) a b.
(Covariant (->) (->) t, Semimonoidal (->) (:*:) (:*:) t) =>
t (a -> b) -> t a -> t b
-<*>- t b
y

(-+-) :: (Covariant (->) (->) t, Semimonoidal (->) (:*:) (:+:) t)
	  => t a -> t b -> (a :+: b -> r) -> t r
t a
x -+- :: t a -> t b -> ((a :+: b) -> r) -> t r
-+- t b
y = \(a :+: b) -> r
f -> (a :+: b) -> r
f ((a :+: b) -> r) -> t (a :+: b) -> t r
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
-<$>- (t a :*: t b) -> t (a :+: b)
forall k (p :: * -> * -> *) (source :: * -> * -> *)
       (target :: k -> k -> k) (t :: k -> *) (a :: k) (b :: k).
Semimonoidal p source target t =>
p (source (t a) (t b)) (t (target a b))
multiply (t a
x t a -> t b -> t a :*: t b
forall s a. s -> a -> s :*: a
:*: t b
y)

point :: Monoidal (->) (->) (:*:) (:*:) t => a -> t a
point :: a -> t a
point a
x = Proxy (:*:) -> (One -> a) -> t a
forall (p :: * -> * -> *) (q :: * -> * -> *)
       (source :: * -> * -> *) (target :: * -> * -> *) (t :: * -> *) a.
Monoidal p q source target t =>
Proxy source -> p (q (Unit target) a) (t a)
unit (Proxy (:*:)
forall k (a :: k). Proxy a
Proxy @(:*:)) (\One
One -> a
x)

empty :: Monoidal (->) (->) (:*:) (:+:) t => t a
empty :: t a
empty = Proxy (:*:) -> (Zero -> a) -> t a
forall (p :: * -> * -> *) (q :: * -> * -> *)
       (source :: * -> * -> *) (target :: * -> * -> *) (t :: * -> *) a.
Monoidal p q source target t =>
Proxy source -> p (q (Unit target) a) (t a)
unit (Proxy (:*:)
forall k (a :: k). Proxy a
Proxy @(:*:)) Zero -> a
forall a. Zero -> a
absurd

type Extractable_ t = Monoidal (<--) (->) (:*:) (:*:) t

extract :: Extractable_ t => t a -> a
extract :: t a -> a
extract t a
j = let Flip t a -> One -> a
f = Proxy (:*:) -> (Unit (:*:) -> a) <-- t a
forall (p :: * -> * -> *) (q :: * -> * -> *)
       (source :: * -> * -> *) (target :: * -> * -> *) (t :: * -> *) a.
Monoidal p q source target t =>
Proxy source -> p (q (Unit target) a) (t a)
unit @(<--) @(->) @(:*:) @(:*:) Proxy (:*:)
forall k (a :: k). Proxy a
Proxy in t a -> One -> a
forall a. t a -> One -> a
f t a
j (One -> a) -> One -> a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ One
One