module Pandora.Paradigm.Primary.Functor.Delta where

import Pandora.Pattern.Category ((.))
import Pandora.Pattern.Functor.Covariant (Covariant ((<$>)))
import Pandora.Pattern.Functor.Pointable (Pointable (point))
import Pandora.Pattern.Functor.Applicative (Applicative ((<*>)))
import Pandora.Pattern.Functor.Distributive (Distributive ((>>-)))
import Pandora.Pattern.Functor.Traversable (Traversable ((->>)))
import Pandora.Pattern.Functor.Extendable (Extendable ((=>>)))
import Pandora.Pattern.Functor.Representable (Representable (Representation, (<#>), tabulate))
import Pandora.Pattern.Object.Setoid (Setoid ((==)))
import Pandora.Pattern.Object.Semigroup (Semigroup ((+)))
import Pandora.Pattern.Object.Ringoid (Ringoid ((*)))
import Pandora.Paradigm.Primary.Object.Boolean (Boolean (True, False))

infixr 1 :^:

data Delta a = a :^: a

instance Covariant Delta where
	a -> b
f <$> :: (a -> b) -> Delta a -> Delta b
<$> (a
x :^: a
y) = a -> b
f a
x b -> b -> Delta b
forall a. a -> a -> Delta a
:^: a -> b
f a
y

instance Pointable Delta where
	point :: a |-> Delta
point a
x = a
x a -> a |-> Delta
forall a. a -> a -> Delta a
:^: a
x

instance Applicative Delta where
	(a -> b
f :^: a -> b
g) <*> :: Delta (a -> b) -> Delta a -> Delta b
<*> (a
x :^: a
y) = a -> b
f a
x b -> b -> Delta b
forall a. a -> a -> Delta a
:^: a -> b
g a
y

instance Distributive Delta where
	u a
t >>- :: u a -> (a -> Delta b) -> (Delta :. u) := b
>>- a -> Delta b
f = (Representation Delta
Boolean
True Representation Delta -> Delta b -> b
forall (t :: * -> *) a.
Representable t =>
Representation t -> a <-| t
<#>) (Delta b -> b) -> (a -> Delta b) -> a -> b
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. a -> Delta b
f (a -> b) -> u a -> u b
forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b
<$> u a
t u b -> u b -> (Delta :. u) := b
forall a. a -> a -> Delta a
:^: (Representation Delta
Boolean
False Representation Delta -> Delta b -> b
forall (t :: * -> *) a.
Representable t =>
Representation t -> a <-| t
<#>) (Delta b -> b) -> (a -> Delta b) -> a -> b
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. a -> Delta b
f (a -> b) -> u a -> u b
forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b
<$> u a
t

instance Traversable Delta where
	(a
x :^: a
y) ->> :: Delta a -> (a -> u b) -> (u :. Delta) := b
->> a -> u b
f = b -> b -> Delta b
forall a. a -> a -> Delta a
(:^:) (b -> b -> Delta b) -> u b -> u (b -> Delta b)
forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b
<$> a -> u b
f a
x u (b -> Delta b) -> u b -> (u :. Delta) := b
forall (t :: * -> *) a b. Applicative t => t (a -> b) -> t a -> t b
<*> a -> u b
f a
y

instance Extendable Delta where
	Delta a
x =>> :: Delta a -> (Delta a -> b) -> Delta b
=>> Delta a -> b
f = Delta a -> b
f Delta a
x b -> b -> Delta b
forall a. a -> a -> Delta a
:^: Delta a -> b
f Delta a
x

instance Representable Delta where
	type Representation Delta = Boolean
	Representation Delta
True <#> :: Representation Delta -> a <-| Delta
<#> (a
x :^: a
_) = a
x
	Representation Delta
False <#> (a
_ :^: a
y) = a
y
	tabulate :: (Representation Delta -> a) -> Delta a
tabulate Representation Delta -> a
f = Representation Delta -> a
f Representation Delta
Boolean
True a -> a -> Delta a
forall a. a -> a -> Delta a
:^: Representation Delta -> a
f Representation Delta
Boolean
False

instance Setoid a => Setoid (Delta a) where
	(a
x :^: a
y) == :: Delta a -> Delta a -> Boolean
== (a
x' :^: a
y') = (a
x a -> a -> Boolean
forall a. Setoid a => a -> a -> Boolean
== a
x') Boolean -> Boolean -> Boolean
forall a. Ringoid a => a -> a -> a
* (a
y a -> a -> Boolean
forall a. Setoid a => a -> a -> Boolean
== a
y')

instance Semigroup a => Semigroup (Delta a) where
	(a
x :^: a
y) + :: Delta a -> Delta a -> Delta a
+ (a
x' :^: a
y') = (a
x a -> a -> a
forall a. Semigroup a => a -> a -> a
+ a
x') a -> a -> Delta a
forall a. a -> a -> Delta a
:^: (a
y a -> a -> a
forall a. Semigroup a => a -> a -> a
+ a
y')

instance Ringoid a => Ringoid (Delta a) where
	(a
x :^: a
y) * :: Delta a -> Delta a -> Delta a
* (a
x' :^: a
y') = (a
x a -> a -> a
forall a. Ringoid a => a -> a -> a
* a
x') a -> a -> Delta a
forall a. a -> a -> Delta a
:^: (a
y a -> a -> a
forall a. Ringoid a => a -> a -> a
* a
y')