module Pandora.Paradigm.Primary.Functor.Convergence where

import Pandora.Pattern.Category ((<--))
import Pandora.Pattern.Morphism.Straight (Straight (Straight))
import Pandora.Pattern.Functor.Contravariant (Contravariant ((>-|-)))
import Pandora.Pattern.Functor.Semimonoidal (Semimonoidal (mult))
import Pandora.Pattern.Functor.Monoidal (Monoidal (unit))
import Pandora.Pattern.Object.Semigroup (Semigroup ((+)))
import Pandora.Pattern.Object.Monoid (Monoid (zero))
import Pandora.Paradigm.Algebraic.Exponential (type (-->), type (<--))
import Pandora.Paradigm.Algebraic.Product ((:*:)((:*:)))
import Pandora.Paradigm.Algebraic ()

data Convergence r a = Convergence (a -> a -> r)

instance Contravariant (->) (->) (Convergence r) where
	a -> b
f >-|- :: (a -> b) -> Convergence r b -> Convergence r a
>-|- Convergence b -> b -> r
g = (a -> a -> r) -> Convergence r a
forall r a. (a -> a -> r) -> Convergence r a
Convergence ((a -> a -> r) -> Convergence r a)
-> (a -> a -> r) -> Convergence r a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- \a
x a
y -> b -> b -> r
g (b -> b -> r) -> b -> b -> r
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- a -> b
f a
x (b -> r) -> b -> r
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- a -> b
f a
y

instance Semigroup r => Semimonoidal (-->) (:*:) (:*:) (Convergence r) where
	mult :: (Convergence r a :*: Convergence r b) --> Convergence r (a :*: b)
mult = ((Convergence r a :*: Convergence r b) -> Convergence r (a :*: b))
-> (Convergence r a :*: Convergence r b)
   --> Convergence r (a :*: b)
forall (v :: * -> * -> *) a e. v a e -> Straight v a e
Straight (((Convergence r a :*: Convergence r b) -> Convergence r (a :*: b))
 -> (Convergence r a :*: Convergence r b)
    --> Convergence r (a :*: b))
-> ((Convergence r a :*: Convergence r b)
    -> Convergence r (a :*: b))
-> (Convergence r a :*: Convergence r b)
   --> Convergence r (a :*: b)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- \(Convergence a -> a -> r
f :*: Convergence b -> b -> r
g) -> ((a :*: b) -> (a :*: b) -> r) -> Convergence r (a :*: b)
forall r a. (a -> a -> r) -> Convergence r a
Convergence (((a :*: b) -> (a :*: b) -> r) -> Convergence r (a :*: b))
-> ((a :*: b) -> (a :*: b) -> r) -> Convergence r (a :*: b)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- \(a
a :*: b
b) (a
a' :*: b
b') -> a -> a -> r
f a
a a
a' r -> r -> r
forall a. Semigroup a => a -> a -> a
+ b -> b -> r
g b
b b
b'

instance Monoid r => Monoidal (-->) (<--) (:*:) (:*:) (Convergence r) where
	unit :: Proxy (:*:) -> (Unit (:*:) <-- a) --> Convergence r a
unit Proxy (:*:)
_ = ((One <-- a) -> Convergence r a)
-> Straight (->) (One <-- a) (Convergence r a)
forall (v :: * -> * -> *) a e. v a e -> Straight v a e
Straight (((One <-- a) -> Convergence r a)
 -> Straight (->) (One <-- a) (Convergence r a))
-> ((One <-- a) -> Convergence r a)
-> Straight (->) (One <-- a) (Convergence r a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- \One <-- a
_ -> (a -> a -> r) -> Convergence r a
forall r a. (a -> a -> r) -> Convergence r a
Convergence ((a -> a -> r) -> Convergence r a)
-> (a -> a -> r) -> Convergence r a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- \a
_ a
_ -> r
forall a. Monoid a => a
zero