module Pandora.Paradigm.Primary.Functor.Tagged where

import Pandora.Core.Functor (type (:=>), type (~>))
import Pandora.Pattern.Semigroupoid ((.))
import Pandora.Pattern.Morphism.Flip (Flip (Flip))
import Pandora.Pattern.Morphism.Straight (Straight (Straight))
import Pandora.Pattern.Category (($))
import Pandora.Pattern.Functor.Covariant (Covariant ((<$>)))
import Pandora.Pattern.Functor.Semimonoidal (Semimonoidal (mult))
import Pandora.Pattern.Functor.Monoidal (Monoidal (unit))
import Pandora.Pattern.Functor.Traversable (Traversable ((<<-)))
import Pandora.Pattern.Functor.Distributive (Distributive ((-<<)))
import Pandora.Pattern.Functor.Bindable (Bindable ((=<<)))
import Pandora.Pattern.Functor.Extendable (Extendable ((<<=)))
import Pandora.Pattern.Functor.Monad (Monad)
import Pandora.Pattern.Functor.Comonad (Comonad)
import Pandora.Pattern.Functor.Bivariant (Bivariant ((<->)))
import Pandora.Pattern.Object.Setoid (Setoid ((==)))
import Pandora.Pattern.Object.Chain (Chain ((<=>)))
import Pandora.Pattern.Object.Semigroup (Semigroup ((+)))
import Pandora.Pattern.Object.Monoid (Monoid (zero))
import Pandora.Pattern.Object.Ringoid (Ringoid ((*)))
import Pandora.Pattern.Object.Quasiring (Quasiring (one))
import Pandora.Pattern.Object.Semilattice (Infimum ((/\)), Supremum ((\/)))
import Pandora.Pattern.Object.Lattice (Lattice)
import Pandora.Pattern.Object.Group (Group (invert))
import Pandora.Paradigm.Primary.Algebraic.Exponential (type (<--), type (-->))
import Pandora.Paradigm.Primary.Algebraic.Product ((:*:) ((:*:)))
import Pandora.Paradigm.Primary.Algebraic.One (One (One))
import Pandora.Paradigm.Primary.Algebraic (extract)

newtype Tagged tag a = Tag a

infixr 0 :#
type (:#) tag = Tagged tag

instance Covariant (->) (->) (Tagged tag) where
	a -> b
f <$> :: (a -> b) -> Tagged tag a -> Tagged tag b
<$> Tag a
x = b -> Tagged tag b
forall k (tag :: k) a. a -> Tagged tag a
Tag (b -> Tagged tag b) -> b -> Tagged tag b
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ a -> b
f a
x

instance Covariant (->) (->) (Flip Tagged a) where
	a -> b
_ <$> :: (a -> b) -> Flip Tagged a a -> Flip Tagged a b
<$> Flip (Tag a
x) = Tagged b a -> Flip Tagged a b
forall (v :: * -> * -> *) a e. v e a -> Flip v a e
Flip (Tagged b a -> Flip Tagged a b) -> Tagged b a -> Flip Tagged a b
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ a -> Tagged b a
forall k (tag :: k) a. a -> Tagged tag a
Tag a
x

instance Semimonoidal (-->) (:*:) (:*:) (Tagged tag) where
	mult :: (Tagged tag a :*: Tagged tag b) --> Tagged tag (a :*: b)
mult = ((Tagged tag a :*: Tagged tag b) -> Tagged tag (a :*: b))
-> (Tagged tag a :*: Tagged tag b) --> Tagged tag (a :*: b)
forall (v :: * -> * -> *) a e. v a e -> Straight v a e
Straight (((Tagged tag a :*: Tagged tag b) -> Tagged tag (a :*: b))
 -> (Tagged tag a :*: Tagged tag b) --> Tagged tag (a :*: b))
-> ((Tagged tag a :*: Tagged tag b) -> Tagged tag (a :*: b))
-> (Tagged tag a :*: Tagged tag b) --> Tagged tag (a :*: b)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ (a :*: b) -> Tagged tag (a :*: b)
forall k (tag :: k) a. a -> Tagged tag a
Tag ((a :*: b) -> Tagged tag (a :*: b))
-> ((Tagged tag a :*: Tagged tag b) -> a :*: b)
-> (Tagged tag a :*: Tagged tag b)
-> Tagged tag (a :*: b)
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (Tagged tag a -> a
forall (t :: * -> *) a. Extractable t => t a -> a
extract (Tagged tag a -> a)
-> (Tagged tag b -> b)
-> (Tagged tag a :*: Tagged tag b)
-> a :*: b
forall (left :: * -> * -> *) (right :: * -> * -> *)
       (target :: * -> * -> *) (v :: * -> * -> *) a b c d.
Bivariant left right target v =>
left a b -> right c d -> target (v a c) (v b d)
<-> Tagged tag b -> b
forall (t :: * -> *) a. Extractable t => t a -> a
extract)

instance Monoidal (-->) (->) (:*:) (:*:) (Tagged tag) where
	unit :: Proxy (:*:) -> (Unit (:*:) -> a) --> Tagged tag a
unit Proxy (:*:)
_ = ((One -> a) -> Tagged tag a)
-> Straight (->) (One -> a) (Tagged tag a)
forall (v :: * -> * -> *) a e. v a e -> Straight v a e
Straight (((One -> a) -> Tagged tag a)
 -> Straight (->) (One -> a) (Tagged tag a))
-> ((One -> a) -> Tagged tag a)
-> Straight (->) (One -> a) (Tagged tag a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ a -> Tagged tag a
forall k (tag :: k) a. a -> Tagged tag a
Tag (a -> Tagged tag a)
-> ((One -> a) -> a) -> (One -> a) -> Tagged tag a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. ((One -> a) -> One -> a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ One
One)

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

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

instance Traversable (->) (->) (Tagged tag) where
	a -> u b
f <<- :: (a -> u b) -> Tagged tag a -> u (Tagged tag b)
<<- Tag a
x = b -> Tagged tag b
forall k (tag :: k) a. a -> Tagged tag a
Tag (b -> Tagged tag b) -> u b -> u (Tagged tag b)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<$> a -> u b
f a
x

instance Distributive (->) (->) (Tagged tag) where
	a -> Tagged tag b
f -<< :: (a -> Tagged tag b) -> u a -> Tagged tag (u b)
-<< u a
x = u b -> Tagged tag (u b)
forall k (tag :: k) a. a -> Tagged tag a
Tag (u b -> Tagged tag (u b)) -> u b -> Tagged tag (u b)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ Tagged tag b -> b
forall (t :: * -> *) a. Extractable t => t a -> a
extract (Tagged tag b -> b) -> (a -> Tagged tag b) -> a -> b
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. a -> Tagged tag b
f (a -> b) -> u a -> u b
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<$> u a
x

instance Bindable (->) (Tagged tag) where
	a -> Tagged tag b
f =<< :: (a -> Tagged tag b) -> Tagged tag a -> Tagged tag b
=<< Tag a
x = a -> Tagged tag b
f a
x

instance Monad (->) (Tagged tag)

instance Extendable (->) (Tagged tag) where
	Tagged tag a -> b
f <<= :: (Tagged tag a -> b) -> Tagged tag a -> Tagged tag b
<<= Tagged tag a
x = b -> Tagged tag b
forall k (tag :: k) a. a -> Tagged tag a
Tag (b -> Tagged tag b)
-> (Tagged tag a -> b) -> Tagged tag a -> Tagged tag b
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Tagged tag a -> b
f (Tagged tag a -> Tagged tag b) -> Tagged tag a -> Tagged tag b
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ Tagged tag a
x

instance Comonad (->) (Tagged tag)

instance Bivariant (->) (->) (->) Tagged where
	a -> b
_ <-> :: (a -> b) -> (c -> d) -> Tagged a c -> Tagged b d
<-> c -> d
g = \(Tag c
x) -> d -> Tagged b d
forall k (tag :: k) a. a -> Tagged tag a
Tag (d -> Tagged b d) -> d -> Tagged b d
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ c -> d
g c
x

instance Setoid a => Setoid (Tagged tag a) where
	Tag a
x == :: Tagged tag a -> Tagged tag a -> Boolean
== Tag a
y = a
x a -> a -> Boolean
forall a. Setoid a => a -> a -> Boolean
== a
y

instance Chain a => Chain (Tagged tag a) where
	Tag a
x <=> :: Tagged tag a -> Tagged tag a -> Ordering
<=> Tag a
y = a
x a -> a -> Ordering
forall a. Chain a => a -> a -> Ordering
<=> a
y

instance Semigroup a => Semigroup (Tagged tag a) where
	Tag a
x + :: Tagged tag a -> Tagged tag a -> Tagged tag a
+ Tag a
y = a -> Tagged tag a
forall k (tag :: k) a. a -> Tagged tag a
Tag (a -> Tagged tag a) -> a -> Tagged tag a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ a
x a -> a -> a
forall a. Semigroup a => a -> a -> a
+ a
y

instance Monoid a => Monoid (Tagged tag a) where
	 zero :: Tagged tag a
zero = a -> Tagged tag a
forall k (tag :: k) a. a -> Tagged tag a
Tag a
forall a. Monoid a => a
zero

instance Ringoid a => Ringoid (Tagged tag a) where
	Tag a
x * :: Tagged tag a -> Tagged tag a -> Tagged tag a
* Tag a
y = a -> Tagged tag a
forall k (tag :: k) a. a -> Tagged tag a
Tag (a -> Tagged tag a) -> a -> Tagged tag a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ a
x a -> a -> a
forall a. Ringoid a => a -> a -> a
* a
y

instance Quasiring a => Quasiring (Tagged tag a) where
	one :: Tagged tag a
one = a -> Tagged tag a
forall k (tag :: k) a. a -> Tagged tag a
Tag a
forall a. Quasiring a => a
one

instance Infimum a => Infimum (Tagged tag a) where
	Tag a
x /\ :: Tagged tag a -> Tagged tag a -> Tagged tag a
/\ Tag a
y = a -> Tagged tag a
forall k (tag :: k) a. a -> Tagged tag a
Tag (a -> Tagged tag a) -> a -> Tagged tag a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ a
x a -> a -> a
forall a. Infimum a => a -> a -> a
/\ a
y

instance Supremum a => Supremum (Tagged tag a) where
	Tag a
x \/ :: Tagged tag a -> Tagged tag a -> Tagged tag a
\/ Tag a
y = a -> Tagged tag a
forall k (tag :: k) a. a -> Tagged tag a
Tag (a -> Tagged tag a) -> a -> Tagged tag a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ a
x a -> a -> a
forall a. Supremum a => a -> a -> a
\/ a
y

instance Lattice a => Lattice (Tagged tag a) where

instance Group a => Group (Tagged tag a) where
	invert :: Tagged tag a -> Tagged tag a
invert (Tag a
x) = a -> Tagged tag a
forall k (tag :: k) a. a -> Tagged tag a
Tag (a -> Tagged tag a) -> a -> Tagged tag a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ a -> a
forall a. Group a => a -> a
invert a
x

retag :: forall new old . Tagged old ~> Tagged new
retag :: Tagged old a -> Tagged new a
retag (Tag a
x) = a -> Tagged new a
forall k (tag :: k) a. a -> Tagged tag a
Tag a
x

tagself :: a :=> Tagged a
tagself :: a :=> Tagged a
tagself = a :=> Tagged a
forall k (tag :: k) a. a -> Tagged tag a
Tag