module Pandora.Paradigm.Algebraic.Sum where

import Pandora.Core.Functor (type (>>>>>>))
import Pandora.Pattern.Semigroupoid ((.))
import Pandora.Pattern.Category ((<--))
import Pandora.Pattern.Functor.Covariant (Covariant ((<-|-)))
import Pandora.Paradigm.Algebraic.Exponential ()
import Pandora.Pattern.Morphism.Flip (Flip (Flip))
import Pandora.Paradigm.Schemes.T_U (type (<:.:>), type (>:.:>), type (<:.:<), type (>:.:<))

infixr 7 :+:

data (:+:) o a = Option o | Adoption a

instance Covariant (->) (->) ((:+:) o) where
	a -> b
_ <-|- :: (a -> b) -> (o :+: a) -> o :+: b
<-|- Option o
s = o -> o :+: b
forall o a. o -> o :+: a
Option o
s
	a -> b
f <-|- Adoption a
x = b -> o :+: b
forall o a. a -> o :+: a
Adoption (b -> o :+: b) -> b -> o :+: b
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- a -> b
f a
x

instance Covariant (->) (->) (Flip (:+:) a) where
	a -> b
_ <-|- :: (a -> b) -> Flip (:+:) a a -> Flip (:+:) a b
<-|- Flip (Adoption a
x) = (b :+: a) -> Flip (:+:) a b
forall (v :: * -> * -> *) a e. v e a -> Flip v a e
Flip ((b :+: a) -> Flip (:+:) a b)
-> (a -> b :+: a) -> a -> Flip (:+:) a b
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. a -> b :+: a
forall o a. a -> o :+: a
Adoption (a -> Flip (:+:) a b) -> a -> Flip (:+:) a b
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- a
x
	a -> b
f <-|- Flip (Option a
y) = (b :+: a) -> Flip (:+:) a b
forall (v :: * -> * -> *) a e. v e a -> Flip v a e
Flip ((b :+: a) -> Flip (:+:) a b)
-> (b -> b :+: a) -> b -> Flip (:+:) a b
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. b -> b :+: a
forall o a. o -> o :+: a
Option (b -> Flip (:+:) a b) -> b -> Flip (:+:) a b
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- a -> b
f a
y

sum :: (e -> r) -> (a -> r) -> e :+: a -> r
sum :: (e -> r) -> (a -> r) -> (e :+: a) -> r
sum e -> r
f a -> r
_ (Option e
x) = e -> r
f e
x
sum e -> r
_ a -> r
s (Adoption a
x) = a -> r
s a
x

-- TODO: keep it until we realize how to implement n-ary functors
bitraverse_sum :: Covariant (->) (->) t => (e -> t e') -> (a -> t a') -> (e :+: a) -> t (e' :+: a')
bitraverse_sum :: (e -> t e') -> (a -> t a') -> (e :+: a) -> t (e' :+: a')
bitraverse_sum e -> t e'
f a -> t a'
_ (Option e
x) = e' -> e' :+: a'
forall o a. o -> o :+: a
Option (e' -> e' :+: a') -> t e' -> t (e' :+: a')
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|- e -> t e'
f e
x
bitraverse_sum e -> t e'
_ a -> t a'
g (Adoption a
x) = a' -> e' :+: a'
forall o a. a -> o :+: a
Adoption (a' -> e' :+: a') -> t a' -> t (e' :+: a')
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|- a -> t a'
g a
x

type (<:+:>) t u = t <:.:> u >>>>>> (:+:)
type (>:+:>) t u = t >:.:> u >>>>>> (:+:)
type (<:+:<) t u = t <:.:< u >>>>>> (:+:)
type (>:+:<) t u = t >:.:< u >>>>>> (:+:)