{-# OPTIONS_GHC -fno-warn-orphans #-}

module Pandora.Paradigm.Primary.Algebraic (module Exports, Applicative_, Alternative_, ($>-), ($$>-), ($$$>-), (-<*>-), (*>-), forever_, (-+-)) where

import Pandora.Paradigm.Primary.Algebraic.Exponential as Exports
import Pandora.Paradigm.Primary.Algebraic.Product as Exports
import Pandora.Paradigm.Primary.Algebraic.Sum as Exports

import Pandora.Pattern.Category (($))
import Pandora.Pattern.Functor (Endofunctor)
import Pandora.Pattern.Functor.Covariant (Covariant ((-<$>-)), (-<$$>-), (-<$$$>-))
import Pandora.Pattern.Functor.Extractable (Extractable (extract))
import Pandora.Pattern.Functor.Semimonoidal (Semimonoidal (multiply_))
import Pandora.Pattern.Functor.Traversable (Traversable ((<<-)))
import Pandora.Pattern.Functor.Adjoint (Adjoint ((-|), (|-)))

infixl 4 -<*>-

($>-) :: Covariant t (->) (->) => t a -> b -> t b
t a
x $>- :: t a -> b -> t b
$>- b
r = (b
r b -> a -> b
forall a b. a -> b -> a
!.) (a -> b) -> t a -> t b
forall (t :: * -> *) (source :: * -> * -> *)
       (target :: * -> * -> *) a b.
Covariant t source target =>
source a b -> target (t a) (t b)
-<$>- t a
x

($$>-) :: (Covariant t (->) (->), Covariant u (->) (->)) => t (u a) -> b -> t (u b)
t (u a)
x $$>- :: t (u a) -> b -> t (u b)
$$>- b
r = (b
r b -> a -> b
forall a b. a -> b -> a
!.) (a -> b) -> t (u a) -> t (u b)
forall (t :: * -> *) (u :: * -> *) (category :: * -> * -> *) a b.
(Covariant u category category, Covariant t category category) =>
category a b -> category (t (u a)) (t (u b))
-<$$>- t (u a)
x

($$$>-) :: (Covariant t (->) (->), Covariant u (->) (->), Covariant v (->) (->)) => t (u (v a)) -> b -> t (u (v b))
t (u (v a))
x $$$>- :: t (u (v a)) -> b -> t (u (v b))
$$$>- b
r = (b
r b -> a -> b
forall a b. a -> b -> a
!.) (a -> b) -> t (u (v a)) -> t (u (v b))
forall (t :: * -> *) (u :: * -> *) (v :: * -> *)
       (category :: * -> * -> *) a b.
(Covariant t category category, Covariant u category category,
 Covariant v category category) =>
category a b -> category (t (u (v a))) (t (u (v b)))
-<$$$>- t (u (v a))
x

instance Traversable ((:*:) s) (->) (->) where
	a -> u b
f <<- :: (a -> u b) -> (s :*: a) -> u (s :*: b)
<<- s :*: a
x = ((s :*: a) -> s
forall a b. (a :*: b) -> a
attached s :*: a
x s -> b -> s :*: b
forall s a. s -> a -> s :*: a
:*:) (b -> s :*: b) -> u b -> u (s :*: b)
forall (t :: * -> *) (source :: * -> * -> *)
       (target :: * -> * -> *) a b.
Covariant t source target =>
source a b -> target (t a) (t b)
-<$>- a -> u b
f ((s :*: a) -> a
forall (t :: * -> *) (source :: * -> * -> *) a.
Extractable t source =>
source (t a) a
extract s :*: a
x)

instance Adjoint ((:*:) s) ((->) s) (->) (->) where
	(-|) :: ((s :*: a) -> b) -> a -> (s -> b)
	(s :*: a) -> b
f -| :: ((s :*: a) -> b) -> a -> s -> b
-| a
x = \s
s -> (s :*: a) -> b
f ((s :*: a) -> b) -> (s :*: a) -> b
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ s
s s -> a -> s :*: a
forall s a. s -> a -> s :*: a
:*: a
x
	(|-) :: (a -> s -> b) -> (s :*: a) -> b
	a -> s -> b
f |- :: (a -> s -> b) -> (s :*: a) -> b
|- ~(s
s :*: a
x) = a -> s -> b
f a
x s
s

instance Semimonoidal ((->) e) (->) (:*:) (:*:) where
	multiply_ :: ((e -> a) :*: (e -> b)) -> e -> (a :*: b)
	multiply_ :: ((e -> a) :*: (e -> b)) -> e -> a :*: b
multiply_ (e -> a
g :*: e -> b
h) = \e
x -> e -> a
g e
x a -> b -> a :*: b
forall s a. s -> a -> s :*: a
:*: e -> b
h e
x

instance Semimonoidal ((:+:) e) (->) (:*:) (:+:) where
	multiply_ :: ((e :+: a) :*: (e :+: b)) -> e :+: a :+: b
	multiply_ :: ((e :+: a) :*: (e :+: b)) -> e :+: (a :+: b)
multiply_ (Option e
_ :*: Option e
e') = e -> e :+: (a :+: b)
forall s a. s -> s :+: a
Option e
e'
	multiply_ (Option e
_ :*: Adoption b
y) = (a :+: b) -> e :+: (a :+: b)
forall s a. a -> s :+: a
Adoption ((a :+: b) -> e :+: (a :+: b)) -> (a :+: b) -> e :+: (a :+: b)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ b -> a :+: b
forall s a. a -> s :+: a
Adoption b
y
	multiply_ (Adoption a
x :*: e :+: b
_) = (a :+: b) -> e :+: (a :+: b)
forall s a. a -> s :+: a
Adoption ((a :+: b) -> e :+: (a :+: b)) -> (a :+: b) -> e :+: (a :+: b)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ a -> a :+: b
forall s a. s -> s :+: a
Option a
x

type Applicative_ t = (Endofunctor Covariant t (->), Semimonoidal t (->) (:*:) (:*:))
type Alternative_ t = (Endofunctor Covariant t (->), Semimonoidal t (->) (:*:) (:+:))

(-<*>-) :: Applicative_ t => t (a -> b) -> t a -> t b
t (a -> b)
f -<*>- :: t (a -> b) -> t a -> t b
-<*>- t a
x = (a -> (a -> b) -> b) -> ((a -> b) :*: a) -> b
forall (t :: * -> *) (u :: * -> *) (source :: * -> * -> *)
       (target :: * -> * -> *) a b.
Adjoint t u source target =>
target a (u b) -> source (t a) b
(|-) @_ @_ @(->) @(->) a -> (a -> b) -> b
forall a b. a -> (a -> b) -> b
(&) (((a -> b) :*: a) -> b) -> t ((a -> b) :*: a) -> t b
forall (t :: * -> *) (source :: * -> * -> *)
       (target :: * -> * -> *) a b.
Covariant t source target =>
source a b -> target (t a) (t b)
-<$>- (t (a -> b) :*: t a) -> t ((a -> b) :*: a)
forall k (t :: k -> *) (p :: * -> * -> *) (source :: * -> * -> *)
       (target :: k -> k -> k) (a :: k) (b :: k).
Semimonoidal t p source target =>
p (source (t a) (t b)) (t (target a b))
multiply_ @_ @_ @_ @(:*:) (t (a -> b)
f t (a -> b) -> t a -> t (a -> b) :*: t a
forall s a. s -> a -> s :*: a
:*: t a
x)

forever_ :: Applicative_ t => t a -> t b
forever_ :: t a -> t b
forever_ t a
x = let r :: t b
r = t a
x t a -> t b -> t b
forall (t :: * -> *) a b. Applicative_ t => t a -> t b -> t b
*>- t b
r in t b
r

(*>-) :: Applicative_ t => t a -> t b -> t b
t a
x *>- :: t a -> t b -> t b
*>- t b
y = (b -> a -> b
forall a b. a -> b -> a
(!.) (b -> a -> b) -> a -> b -> b
forall a b c. (a -> b -> c) -> b -> a -> c
%) (a -> b -> b) -> t a -> t (b -> b)
forall (t :: * -> *) (source :: * -> * -> *)
       (target :: * -> * -> *) a b.
Covariant t source target =>
source a b -> target (t a) (t b)
-<$>- t a
x t (b -> b) -> t b -> t b
forall (t :: * -> *) a b.
Applicative_ t =>
t (a -> b) -> t a -> t b
-<*>- t b
y

(-+-) :: Alternative_ t => t a -> t b -> (a :+: b -> r) -> t r
t a
x -+- :: t a -> t b -> ((a :+: b) -> r) -> t r
-+- t b
y = \(a :+: b) -> r
f -> (a :+: b) -> r
f ((a :+: b) -> r) -> t (a :+: b) -> t r
forall (t :: * -> *) (source :: * -> * -> *)
       (target :: * -> * -> *) a b.
Covariant t source target =>
source a b -> target (t a) (t b)
-<$>- (t a :*: t b) -> t (a :+: b)
forall k (t :: k -> *) (p :: * -> * -> *) (source :: * -> * -> *)
       (target :: k -> k -> k) (a :: k) (b :: k).
Semimonoidal t p source target =>
p (source (t a) (t b)) (t (target a b))
multiply_ (t a
x t a -> t b -> t a :*: t b
forall s a. s -> a -> s :*: a
:*: t b
y)