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)
import Pandora.Paradigm.Controlflow.Effect.Interpreted (run)

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 (:*:)
_ = (Straight (->) One a -> Tagged tag a)
-> Straight (->) (Straight (->) One a) (Tagged tag a)
forall (v :: * -> * -> *) a e. v a e -> Straight v a e
Straight ((Straight (->) One a -> Tagged tag a)
 -> Straight (->) (Straight (->) One a) (Tagged tag a))
-> (Straight (->) One a -> Tagged tag a)
-> Straight (->) (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)
-> (Straight (->) One a -> a)
-> Straight (->) 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) ((One -> a) -> a)
-> (Straight (->) One a -> One -> a) -> Straight (->) One a -> a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Straight (->) One a -> One -> a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run

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 -> Straight (->) One a)
-> Flip (->) (Straight (->) One a) (Tagged tag a)
forall (v :: * -> * -> *) a e. v e a -> Flip v a e
Flip ((Tagged tag a -> Straight (->) One a)
 -> Flip (->) (Straight (->) One a) (Tagged tag a))
-> (Tagged tag a -> Straight (->) One a)
-> Flip (->) (Straight (->) One a) (Tagged tag a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ \(Tag a
x) -> (One -> a) -> Straight (->) One a
forall (v :: * -> * -> *) a e. v a e -> Straight v a e
Straight (\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