module Pandora.Paradigm.Primary.Functor.Maybe where

import Pandora.Core.Functor (type (:.), type (>>>))
import Pandora.Core.Interpreted (Interpreted (Primary, run, unite, (<~)))
import Pandora.Pattern.Semigroupoid ((.))
import Pandora.Pattern.Category (identity, (<--), (<---))
import Pandora.Pattern.Morphism.Flip (Flip (Flip))
import Pandora.Pattern.Morphism.Straight (Straight (Straight))
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.Bindable (Bindable ((=<<)))
import Pandora.Pattern.Functor.Monad (Monad)
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.Semilattice (Infimum ((/\)), Supremum ((\/)))
import Pandora.Pattern.Object.Lattice (Lattice)
import Pandora.Paradigm.Primary.Object.Boolean (Boolean (True, False))
import Pandora.Paradigm.Primary.Object.Ordering (Ordering (Less, Equal, Greater))
import Pandora.Paradigm.Controlflow.Effect.Transformer.Monadic (Monadic (wrap), (:>) (TM))
import Pandora.Paradigm.Controlflow.Effect.Adaptable (Adaptable (adapt))
import Pandora.Paradigm.Structure.Ability.Monotonic (Monotonic (reduce))
import Pandora.Paradigm.Algebraic.Exponential (type (<--), type (-->))
import Pandora.Paradigm.Algebraic.Product ((:*:) ((:*:)))
import Pandora.Paradigm.Algebraic.Sum ((:+:) (Option, Adoption))
import Pandora.Paradigm.Algebraic.One (One (One))
import Pandora.Paradigm.Algebraic (point)
import Pandora.Paradigm.Schemes (Schematic, UT (UT), type (<.:>))

-- TODO: better to rename it to Option a = Some a | None?
data Maybe a = Nothing | Just a

instance Covariant (->) (->) Maybe where
	a -> b
f <-|- :: (a -> b) -> Maybe a -> Maybe b
<-|- Just a
x = b -> Maybe b
forall a. a -> Maybe a
Just (b -> Maybe b) -> b -> Maybe b
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- a -> b
f a
x
	a -> b
_ <-|- Maybe a
Nothing = Maybe b
forall a. Maybe a
Nothing

instance Semimonoidal (-->) (:*:) (:*:) Maybe where
	mult :: (Maybe a :*: Maybe b) --> Maybe (a :*: b)
mult = ((Maybe a :*: Maybe b) -> Maybe (a :*: b))
-> (Maybe a :*: Maybe b) --> Maybe (a :*: b)
forall (v :: * -> * -> *) a e. v a e -> Straight v a e
Straight (((Maybe a :*: Maybe b) -> Maybe (a :*: b))
 -> (Maybe a :*: Maybe b) --> Maybe (a :*: b))
-> ((Maybe a :*: Maybe b) -> Maybe (a :*: b))
-> (Maybe a :*: Maybe b) --> Maybe (a :*: b)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- \case
		Just a
x :*: Just b
y -> (a :*: b) -> Maybe (a :*: b)
forall a. a -> Maybe a
Just ((a :*: b) -> Maybe (a :*: b)) -> (a :*: b) -> Maybe (a :*: b)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- a
x a -> b -> a :*: b
forall s a. s -> a -> s :*: a
:*: b
y
		Maybe a
Nothing :*: Maybe b
_ -> Maybe (a :*: b)
forall a. Maybe a
Nothing
		Maybe a
_ :*: Maybe b
Nothing -> Maybe (a :*: b)
forall a. Maybe a
Nothing

instance Semimonoidal (-->) (:*:) (:+:) Maybe where
	mult :: (Maybe a :*: Maybe b) --> Maybe (a :+: b)
mult = ((Maybe a :*: Maybe b) -> Maybe (a :+: b))
-> (Maybe a :*: Maybe b) --> Maybe (a :+: b)
forall (v :: * -> * -> *) a e. v a e -> Straight v a e
Straight (((Maybe a :*: Maybe b) -> Maybe (a :+: b))
 -> (Maybe a :*: Maybe b) --> Maybe (a :+: b))
-> ((Maybe a :*: Maybe b) -> Maybe (a :+: b))
-> (Maybe a :*: Maybe b) --> Maybe (a :+: b)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- \case
		Just a
x :*: Maybe b
_ -> (a :+: b) -> Maybe (a :+: b)
forall a. a -> Maybe a
Just ((a :+: b) -> Maybe (a :+: b)) -> (a :+: b) -> Maybe (a :+: b)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- a -> a :+: b
forall o a. o -> o :+: a
Option a
x
		Maybe a
Nothing :*: Just b
y -> (a :+: b) -> Maybe (a :+: b)
forall a. a -> Maybe a
Just ((a :+: b) -> Maybe (a :+: b)) -> (a :+: b) -> Maybe (a :+: b)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- b -> a :+: b
forall o a. a -> o :+: a
Adoption b
y
		Maybe a
Nothing :*: Maybe b
Nothing -> Maybe (a :+: b)
forall a. Maybe a
Nothing

instance Monoidal (-->) (-->) (:*:) (:*:) Maybe where
	unit :: Proxy (:*:) -> (Unit (:*:) --> a) --> Maybe a
unit Proxy (:*:)
_ = (Straight (->) One a -> Maybe a)
-> Straight (->) (Straight (->) One a) (Maybe a)
forall (v :: * -> * -> *) a e. v a e -> Straight v a e
Straight ((Straight (->) One a -> Maybe a)
 -> Straight (->) (Straight (->) One a) (Maybe a))
-> (Straight (->) One a -> Maybe a)
-> Straight (->) (Straight (->) One a) (Maybe a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- a -> Maybe a
forall a. a -> Maybe a
Just (a -> Maybe a)
-> (Straight (->) One a -> a) -> Straight (->) One a -> Maybe 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
<~ One
One)

instance Monoidal (-->) (-->) (:*:) (:+:) Maybe where
	unit :: Proxy (:*:) -> (Unit (:+:) --> a) --> Maybe a
unit Proxy (:*:)
_ = ((Zero --> a) -> Maybe a) -> Straight (->) (Zero --> a) (Maybe a)
forall (v :: * -> * -> *) a e. v a e -> Straight v a e
Straight (((Zero --> a) -> Maybe a) -> Straight (->) (Zero --> a) (Maybe a))
-> ((Zero --> a) -> Maybe a)
-> Straight (->) (Zero --> a) (Maybe a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- \Zero --> a
_ -> Maybe a
forall a. Maybe a
Nothing

-- TODO: Check laws
instance Semimonoidal (<--) (:*:) (:*:) Maybe where
	mult :: (Maybe a :*: Maybe b) <-- Maybe (a :*: b)
mult = (Maybe (a :*: b) -> Maybe a :*: Maybe b)
-> (Maybe a :*: Maybe b) <-- Maybe (a :*: b)
forall (v :: * -> * -> *) a e. v e a -> Flip v a e
Flip ((Maybe (a :*: b) -> Maybe a :*: Maybe b)
 -> (Maybe a :*: Maybe b) <-- Maybe (a :*: b))
-> (Maybe (a :*: b) -> Maybe a :*: Maybe b)
-> (Maybe a :*: Maybe b) <-- Maybe (a :*: b)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- \case
		Just (a
x :*: b
y) -> a -> Maybe a
forall a. a -> Maybe a
Just a
x Maybe a -> Maybe b -> Maybe a :*: Maybe b
forall s a. s -> a -> s :*: a
:*: b -> Maybe b
forall a. a -> Maybe a
Just b
y
		Maybe (a :*: b)
Nothing -> Maybe a
forall a. Maybe a
Nothing Maybe a -> Maybe b -> Maybe a :*: Maybe b
forall s a. s -> a -> s :*: a
:*: Maybe b
forall a. Maybe a
Nothing

instance Traversable (->) (->) Maybe where
	a -> u b
_ <-/- :: (a -> u b) -> Maybe a -> u (Maybe b)
<-/- Maybe a
Nothing = Maybe b -> u (Maybe b)
forall (t :: * -> *) a. Pointable t => a -> t a
point Maybe b
forall a. Maybe a
Nothing
	a -> u b
f <-/- Just a
x = b -> Maybe b
forall a. a -> Maybe a
Just (b -> Maybe b) -> u b -> u (Maybe 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 Bindable (->) Maybe where
	a -> Maybe b
f =<< :: (a -> Maybe b) -> Maybe a -> Maybe b
=<< Just a
x = a -> Maybe b
f a
x
	a -> Maybe b
_ =<< Maybe a
Nothing = Maybe b
forall a. Maybe a
Nothing

--instance Monad Maybe where

instance Setoid a => Setoid (Maybe a) where
	Just a
x == :: Maybe a -> Maybe a -> Boolean
== Just a
y = a
x a -> a -> Boolean
forall a. Setoid a => a -> a -> Boolean
== a
y
	Maybe a
Nothing == Maybe a
Nothing = Boolean
True
	Maybe a
_ == Maybe a
_ = Boolean
False

instance Chain a => Chain (Maybe a) where
	Just a
x <=> :: Maybe a -> Maybe a -> Ordering
<=> Just a
y = a
x a -> a -> Ordering
forall a. Chain a => a -> a -> Ordering
<=> a
y
	Maybe a
Nothing <=> Maybe a
Nothing = Ordering
Equal
	Maybe a
Nothing <=> Just a
_ = Ordering
Less
	Just a
_ <=> Maybe a
Nothing = Ordering
Greater

instance Semigroup a => Semigroup (Maybe a) where
	Just a
x + :: Maybe a -> Maybe a -> Maybe a
+ Just a
y = a -> Maybe a
forall a. a -> Maybe a
Just (a -> Maybe a) -> a -> Maybe 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
	Maybe a
Nothing + Maybe a
x = Maybe a
x
	Maybe a
x + Maybe a
Nothing = Maybe a
x

instance Semigroup a => Monoid (Maybe a) where
	zero :: Maybe a
zero = Maybe a
forall a. Maybe a
Nothing

instance Infimum a => Infimum (Maybe a) where
	Just a
x /\ :: Maybe a -> Maybe a -> Maybe a
/\ Just a
y = a -> Maybe a
forall a. a -> Maybe a
Just (a -> Maybe a) -> a -> Maybe 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
	Maybe a
_ /\ Maybe a
Nothing = Maybe a
forall a. Maybe a
Nothing
	Maybe a
Nothing /\ Maybe a
_ = Maybe a
forall a. Maybe a
Nothing

instance Supremum a => Supremum (Maybe a) where
	Just a
x \/ :: Maybe a -> Maybe a -> Maybe a
\/ Just a
y = a -> Maybe a
forall a. a -> Maybe a
Just (a -> Maybe a) -> a -> Maybe 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
	Maybe a
x \/ Maybe a
Nothing = Maybe a
x
	Maybe a
Nothing \/ Maybe a
x = Maybe a
x

instance Lattice a => Lattice (Maybe a) where

type instance Schematic Monad Maybe = (<.:>) Maybe

instance Interpreted (->) Maybe where
	type Primary Maybe a = Maybe a
	run :: ((->) < Maybe a) < Primary Maybe a
run = ((->) < Maybe a) < Primary Maybe a
forall (m :: * -> * -> *) a. Category m => m a a
identity
	unite :: ((->) < Primary Maybe a) < Maybe a
unite = ((->) < Primary Maybe a) < Maybe a
forall (m :: * -> * -> *) a. Category m => m a a
identity

instance Monadic (->) Maybe where
	wrap :: ((->) < Maybe a) < (:>) Maybe u a
wrap = (<.:>) Maybe u a -> (:>) Maybe u a
forall (t :: * -> *) (u :: * -> *) a.
Schematic Monad t u a -> (:>) t u a
TM ((<.:>) Maybe u a -> (:>) Maybe u a)
-> (Maybe a -> (<.:>) Maybe u a)
-> ((->) < Maybe a) < (:>) Maybe u a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. ((u :. Maybe) >>> a) -> (<.:>) Maybe u a
forall k k k k (ct :: k) (cu :: k) (t :: k -> k) (u :: k -> *)
       (a :: k).
((u :. t) >>> a) -> UT ct cu t u a
UT (((u :. Maybe) >>> a) -> (<.:>) Maybe u a)
-> (Maybe a -> (u :. Maybe) >>> a) -> Maybe a -> (<.:>) Maybe u a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Maybe a -> (u :. Maybe) >>> a
forall (t :: * -> *) a. Pointable t => a -> t a
point

instance Monotonic a (Maybe a) where
	reduce :: (a -> r -> r) -> r -> Maybe a -> r
reduce a -> r -> r
f r
r (Just a
x) = a -> r -> r
f a
x r
r
	reduce a -> r -> r
_ r
r Maybe a
Nothing = r
r

instance Monotonic a (t a) => Monotonic a (Maybe :. t >>> a) where
	reduce :: (a -> r -> r) -> r -> ((Maybe :. t) >>> a) -> r
reduce a -> r -> r
f r
r (Just t a
x) = (a -> r -> r) -> r -> t a -> r
forall a e r. Monotonic a e => (a -> r -> r) -> r -> e -> r
reduce a -> r -> r
f r
r t a
x
	reduce a -> r -> r
_ r
r (Maybe :. t) >>> a
Nothing = r
r

type Optional t = Adaptable t (->) Maybe

nothing :: Optional t => t a
nothing :: t a
nothing = ((->) < Maybe a) < t a
forall k k k (u :: k -> k) (m :: k -> k -> *) (t :: k -> k)
       (a :: k).
Adaptable u m t =>
(m < t a) < u a
adapt Maybe a
forall a. Maybe a
Nothing