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

module Pandora.Paradigm.Primary.Algebraic (module Exports, Applicative, Alternative, Divisible, Decidable, Extractable, Pointable, (!>-), (!!>-), (!!!>-), (<-*-), (.-*-), (<-*-*-), (.-*-*-), forever_, (<-+-), (.-+-), void, empty, point, pass, extract, (<-|-<-|-), (<-|->-|-), (>-|-<-|-), (>-|->-|-)) 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.Paradigm.Primary.Algebraic.Zero as Exports
import Pandora.Paradigm.Primary.Algebraic.One as Exports

import Pandora.Core.Functor (type (:=))
import Pandora.Pattern.Morphism.Flip (Flip (Flip))
import Pandora.Pattern.Morphism.Straight (Straight (Straight))
import Pandora.Pattern.Semigroupoid ((.))
import Pandora.Pattern.Kernel (constant)
import Pandora.Pattern.Functor.Covariant (Covariant ((<-|-)), (<-|-|-), (<-|-|-|-))
import Pandora.Pattern.Functor.Contravariant (Contravariant ((>-|-)))
import Pandora.Pattern.Functor.Semimonoidal (Semimonoidal (mult))
import Pandora.Pattern.Functor.Monoidal (Monoidal (unit), Unit)
import Pandora.Pattern.Functor.Comonad (Comonad)
import Pandora.Pattern.Functor.Traversable (Traversable ((<<-)))
import Pandora.Pattern.Functor.Adjoint (Adjoint ((-|), (|-)))
import Pandora.Paradigm.Primary.Functor.Proxy (Proxy (Proxy))
import Pandora.Paradigm.Schemes.T_U (T_U (T_U), type (<:.:>))
import Pandora.Paradigm.Controlflow.Effect.Interpreted (Interpreted ((!), (=||)))

type instance Unit (:*:) = One
type instance Unit (:+:) = Zero

infixl 4 <-*-, .-*-
infixl 3 <-*-*-, .-*-*-
infixl 3 <-+-, .-+-
infixl 0 <-|-<-|-, <-|->-|-, >-|-<-|-, >-|->-|-

(!>-) :: Covariant (->) (->) t => t a -> b -> t b
t a
x !>- :: t a -> b -> t b
!>- b
r = b -> a -> b
forall (m :: * -> * -> *) a i. Kernel m => m a (m i a)
constant b
r (a -> b) -> t a -> t b
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
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 -> a -> b
forall (m :: * -> * -> *) a i. Kernel m => m a (m i a)
constant b
r (a -> b) -> t (u a) -> t (u b)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) (u :: * -> *) a b.
(Covariant source target t,
 Covariant source (Betwixt source target) u,
 Covariant (Betwixt source target) target t) =>
source a b -> target (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 -> a -> b
forall (m :: * -> * -> *) a i. Kernel m => m a (m i a)
constant b
r (a -> b) -> t (u (v a)) -> t (u (v b))
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) (v :: * -> *) (u :: * -> *) a b.
(Covariant source target t,
 Covariant source (Betwixt source (Betwixt source target)) v,
 Covariant
   (Betwixt source (Betwixt source target))
   (Betwixt (Betwixt source target) target)
   u,
 Covariant (Betwixt (Betwixt source target) target) target t) =>
source a b -> target (t (u (v a))) (t (u (v b)))
<-|-|-|- t (u (v a))
x

void :: Covariant (->) (->) t => t a -> t ()
void :: t a -> t ()
void t a
x = t a
x t a -> () -> t ()
forall (t :: * -> *) a b. Covariant (->) (->) t => t a -> b -> t b
!>- ()

instance (Semimonoidal (<--) (:*:) (:*:) t, Semimonoidal (<--) (:*:) (:*:) u) => Semimonoidal (<--) (:*:) (:*:) (t <:.:> u := (:*:)) where
	mult :: ((:=) (t <:.:> u) (:*:) a :*: (:=) (t <:.:> u) (:*:) b)
<-- (:=) (t <:.:> u) (:*:) (a :*: b)
mult = ((:=) (t <:.:> u) (:*:) (a :*: b)
 -> (:=) (t <:.:> u) (:*:) a :*: (:=) (t <:.:> u) (:*:) b)
-> ((:=) (t <:.:> u) (:*:) a :*: (:=) (t <:.:> u) (:*:) b)
   <-- (:=) (t <:.:> u) (:*:) (a :*: b)
forall (v :: * -> * -> *) a e. v e a -> Flip v a e
Flip (((:=) (t <:.:> u) (:*:) (a :*: b)
  -> (:=) (t <:.:> u) (:*:) a :*: (:=) (t <:.:> u) (:*:) b)
 -> ((:=) (t <:.:> u) (:*:) a :*: (:=) (t <:.:> u) (:*:) b)
    <-- (:=) (t <:.:> u) (:*:) (a :*: b))
-> ((:=) (t <:.:> u) (:*:) (a :*: b)
    -> (:=) (t <:.:> u) (:*:) a :*: (:=) (t <:.:> u) (:*:) b)
-> ((:=) (t <:.:> u) (:*:) a :*: (:=) (t <:.:> u) (:*:) b)
   <-- (:=) (t <:.:> u) (:*:) (a :*: b)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! \(T_U t (a :*: b) :*: u (a :*: b)
lrxys) ->
		-- TODO: I need matrix transposing here
		let ((t a
lxs :*: t b
lys) :*: (u a
rxs :*: u b
rys)) = ((forall k (p :: * -> * -> *) (source :: * -> * -> *)
       (target :: k -> k -> k) (t :: k -> *) (a :: k) (b :: k).
Semimonoidal p source target t =>
p (source (t a) (t b)) (t (target a b))
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Semimonoidal (<--) source target t =>
source (t a) (t b) <-- t (target a b)
mult @(<--) ((t a :*: t b) <-- t (a :*: b)) -> t (a :*: b) -> t a :*: t b
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
!) (t (a :*: b) -> t a :*: t b)
-> (u (a :*: b) -> u a :*: u b)
-> (t (a :*: b) -> t a :*: t b) :*: (u (a :*: b) -> u a :*: u b)
forall s a. s -> a -> s :*: a
:*: (forall k (p :: * -> * -> *) (source :: * -> * -> *)
       (target :: k -> k -> k) (t :: k -> *) (a :: k) (b :: k).
Semimonoidal p source target t =>
p (source (t a) (t b)) (t (target a b))
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Semimonoidal (<--) source target t =>
source (t a) (t b) <-- t (target a b)
mult @(<--) ((u a :*: u b) <-- u (a :*: b)) -> u (a :*: b) -> u a :*: u b
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
!) ((t (a :*: b) -> t a :*: t b) :*: (u (a :*: b) -> u a :*: u b))
-> (t (a :*: b) :*: u (a :*: b)) -> (t a :*: t b) :*: (u a :*: u b)
forall (m :: * -> * -> *) (p :: * -> * -> *) a b c d.
(Covariant m m (p a), Covariant m m (Flip p d),
 Interpreted m (Flip p d)) =>
(m a b :*: m c d) -> m (p a c) (p b d)
<-|-<-|-) t (a :*: b) :*: u (a :*: b)
lrxys in
		(t a :*: u a) -> (:=) (t <:.:> u) (:*:) a
forall k k k k k (ct :: k) (cu :: k) (p :: k -> k -> *)
       (t :: k -> k) (u :: k -> k) (a :: k).
p (t a) (u a) -> T_U ct cu p t u a
T_U (t a
lxs t a -> u a -> t a :*: u a
forall s a. s -> a -> s :*: a
:*: u a
rxs) (:=) (t <:.:> u) (:*:) a
-> (:=) (t <:.:> u) (:*:) b
-> (:=) (t <:.:> u) (:*:) a :*: (:=) (t <:.:> u) (:*:) b
forall s a. s -> a -> s :*: a
:*: (t b :*: u b) -> (:=) (t <:.:> u) (:*:) b
forall k k k k k (ct :: k) (cu :: k) (p :: k -> k -> *)
       (t :: k -> k) (u :: k -> k) (a :: k).
p (t a) (u a) -> T_U ct cu p t u a
T_U (t b
lys t b -> u b -> t b :*: u b
forall s a. s -> a -> s :*: a
:*: u b
rys)

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 (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|- a -> u b
f ((s :*: a) -> a
forall (t :: * -> *) a. Extractable t => 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 :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! 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
	mult :: ((e -> a) :*: (e -> b)) --> (e -> (a :*: b))
	mult :: ((e -> a) :*: (e -> b)) --> (e -> a :*: b)
mult = (((e -> a) :*: (e -> b)) -> e -> a :*: b)
-> ((e -> a) :*: (e -> b)) --> (e -> a :*: b)
forall (v :: * -> * -> *) a e. v a e -> Straight v a e
Straight ((((e -> a) :*: (e -> b)) -> e -> a :*: b)
 -> ((e -> a) :*: (e -> b)) --> (e -> a :*: b))
-> (((e -> a) :*: (e -> b)) -> e -> a :*: b)
-> ((e -> a) :*: (e -> b)) --> (e -> a :*: b)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! \(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 Monoidal (-->) (-->) (:*:) (:*:) ((->) e) where
	unit :: Proxy (:*:) -> (Unit (:*:) --> a) --> (e -> a)
unit Proxy (:*:)
_ = ((One --> a) -> e -> a) -> Straight (->) (One --> a) (e -> a)
forall (v :: * -> * -> *) a e. v a e -> Straight v a e
Straight (((One --> a) -> e -> a) -> Straight (->) (One --> a) (e -> a))
-> ((One --> a) -> e -> a) -> Straight (->) (One --> a) (e -> a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! a -> e -> a
forall (m :: * -> * -> *) a i. Kernel m => m a (m i a)
constant (a -> e -> a) -> ((One --> a) -> a) -> (One --> a) -> e -> a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. ((One --> a) -> One -> a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! One
One)

instance Semimonoidal (<--) (:*:) (:*:) ((->) e) where
	mult :: ((e -> a) :*: (e -> b)) <-- (e -> a :*: b)
	mult :: ((e -> a) :*: (e -> b)) <-- (e -> a :*: b)
mult = ((e -> a :*: b) -> (e -> a) :*: (e -> b))
-> ((e -> a) :*: (e -> b)) <-- (e -> a :*: b)
forall (v :: * -> * -> *) a e. v e a -> Flip v a e
Flip (((e -> a :*: b) -> (e -> a) :*: (e -> b))
 -> ((e -> a) :*: (e -> b)) <-- (e -> a :*: b))
-> ((e -> a :*: b) -> (e -> a) :*: (e -> b))
-> ((e -> a) :*: (e -> b)) <-- (e -> a :*: b)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! \e -> a :*: b
f -> (a :*: b) -> a
forall a b. (a :*: b) -> a
attached ((a :*: b) -> a) -> (e -> a :*: b) -> e -> a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. e -> a :*: b
f (e -> a) -> (e -> b) -> (e -> a) :*: (e -> b)
forall s a. s -> a -> s :*: a
:*: (a :*: b) -> b
forall (t :: * -> *) a. Extractable t => t a -> a
extract ((a :*: b) -> b) -> (e -> a :*: b) -> e -> b
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. e -> a :*: b
f

instance Semimonoidal (-->) (:*:) (:+:) ((:+:) e) where
	mult :: ((e :+: a) :*: (e :+: b)) --> (e :+: a :+: b)
	mult :: ((e :+: a) :*: (e :+: b)) --> (e :+: (a :+: b))
mult = (((e :+: a) :*: (e :+: b)) -> e :+: (a :+: b))
-> ((e :+: a) :*: (e :+: b)) --> (e :+: (a :+: b))
forall (v :: * -> * -> *) a e. v a e -> Straight v a e
Straight ((((e :+: a) :*: (e :+: b)) -> e :+: (a :+: b))
 -> ((e :+: a) :*: (e :+: b)) --> (e :+: (a :+: b)))
-> (((e :+: a) :*: (e :+: b)) -> e :+: (a :+: b))
-> ((e :+: a) :*: (e :+: b)) --> (e :+: (a :+: b))
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! \case
		Option e
_ :*: Option e
e' -> e -> e :+: (a :+: b)
forall o a. o -> o :+: a
Option e
e'
		Option e
_ :*: Adoption b
y -> (a :+: b) -> e :+: (a :+: b)
forall o a. a -> o :+: a
Adoption ((a :+: b) -> e :+: (a :+: b)) -> (a :+: b) -> e :+: (a :+: b)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! b -> a :+: b
forall o a. a -> o :+: a
Adoption b
y
		Adoption a
x :*: e :+: b
_ -> (a :+: b) -> e :+: (a :+: b)
forall o a. a -> o :+: a
Adoption ((a :+: b) -> e :+: (a :+: b)) -> (a :+: b) -> e :+: (a :+: b)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! a -> a :+: b
forall o a. o -> o :+: a
Option a
x

instance Semimonoidal (-->) (:*:) (:*:) ((:+:) e) where
	mult :: ((e :+: a) :*: (e :+: b)) --> (e :+: (a :*: b))
mult = (((e :+: a) :*: (e :+: b)) -> e :+: (a :*: b))
-> ((e :+: a) :*: (e :+: b)) --> (e :+: (a :*: b))
forall (v :: * -> * -> *) a e. v a e -> Straight v a e
Straight ((((e :+: a) :*: (e :+: b)) -> e :+: (a :*: b))
 -> ((e :+: a) :*: (e :+: b)) --> (e :+: (a :*: b)))
-> (((e :+: a) :*: (e :+: b)) -> e :+: (a :*: b))
-> ((e :+: a) :*: (e :+: b)) --> (e :+: (a :*: b))
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! \case
		Adoption a
x :*: Adoption b
y -> (a :*: b) -> e :+: (a :*: b)
forall o a. a -> o :+: a
Adoption ((a :*: b) -> e :+: (a :*: b)) -> (a :*: b) -> e :+: (a :*: b)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! a
x a -> b -> a :*: b
forall s a. s -> a -> s :*: a
:*: b
y
		Option e
e :*: e :+: b
_ -> e -> e :+: (a :*: b)
forall o a. o -> o :+: a
Option e
e
		e :+: a
_ :*: Option e
e -> e -> e :+: (a :*: b)
forall o a. o -> o :+: a
Option e
e

instance Monoidal (-->) (-->) (:*:) (:*:) ((:+:) e) where
	unit :: Proxy (:*:) -> (Unit (:*:) --> a) --> (e :+: a)
unit Proxy (:*:)
_ = ((One --> a) -> e :+: a) -> Straight (->) (One --> a) (e :+: a)
forall (v :: * -> * -> *) a e. v a e -> Straight v a e
Straight (((One --> a) -> e :+: a) -> Straight (->) (One --> a) (e :+: a))
-> ((One --> a) -> e :+: a) -> Straight (->) (One --> a) (e :+: a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! a -> e :+: a
forall o a. a -> o :+: a
Adoption (a -> e :+: a) -> ((One --> a) -> a) -> (One --> a) -> e :+: a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. ((One --> a) -> One -> a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! One
One)

instance Semimonoidal (<--) (:*:) (:*:) ((:*:) s) where
	mult :: ((s :*: a) :*: (s :*: b)) <-- (s :*: (a :*: b))
mult = ((s :*: (a :*: b)) -> (s :*: a) :*: (s :*: b))
-> ((s :*: a) :*: (s :*: b)) <-- (s :*: (a :*: b))
forall (v :: * -> * -> *) a e. v e a -> Flip v a e
Flip (((s :*: (a :*: b)) -> (s :*: a) :*: (s :*: b))
 -> ((s :*: a) :*: (s :*: b)) <-- (s :*: (a :*: b)))
-> ((s :*: (a :*: b)) -> (s :*: a) :*: (s :*: b))
-> ((s :*: a) :*: (s :*: b)) <-- (s :*: (a :*: b))
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! \(s
s :*: a
x :*: b
y) -> (s
s s -> a -> s :*: a
forall s a. s -> a -> s :*: a
:*: a
x) (s :*: a) -> (s :*: b) -> (s :*: a) :*: (s :*: b)
forall s a. s -> a -> s :*: a
:*: (s
s s -> b -> s :*: b
forall s a. s -> a -> s :*: a
:*: b
y)

instance Monoidal (<--) (-->) (:*:) (:*:) ((:*:) s) where
	unit :: Proxy (:*:) -> (Unit (:*:) --> a) <-- (s :*: a)
unit Proxy (:*:)
_ = ((s :*: a) -> One --> a) -> Flip (->) (One --> a) (s :*: a)
forall (v :: * -> * -> *) a e. v e a -> Flip v a e
Flip (((s :*: a) -> One --> a) -> Flip (->) (One --> a) (s :*: a))
-> ((s :*: a) -> One --> a) -> Flip (->) (One --> a) (s :*: a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! \(s
_ :*: a
x) -> (One -> a) -> One --> a
forall (v :: * -> * -> *) a e. v a e -> Straight v a e
Straight (\One
_ -> a
x)

instance Comonad (->) ((:*:) s) where

instance Semimonoidal (<--) (:*:) (:*:) (Flip (:*:) a) where
	mult :: (Flip (:*:) a a :*: Flip (:*:) a b) <-- Flip (:*:) a (a :*: b)
mult = (Flip (:*:) a (a :*: b) -> Flip (:*:) a a :*: Flip (:*:) a b)
-> (Flip (:*:) a a :*: Flip (:*:) a b) <-- Flip (:*:) a (a :*: b)
forall (v :: * -> * -> *) a e. v e a -> Flip v a e
Flip ((Flip (:*:) a (a :*: b) -> Flip (:*:) a a :*: Flip (:*:) a b)
 -> (Flip (:*:) a a :*: Flip (:*:) a b) <-- Flip (:*:) a (a :*: b))
-> (Flip (:*:) a (a :*: b) -> Flip (:*:) a a :*: Flip (:*:) a b)
-> (Flip (:*:) a a :*: Flip (:*:) a b) <-- Flip (:*:) a (a :*: b)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! \(Flip ((a
sx :*: b
sy) :*: a
r)) -> (a :*: a) -> Flip (:*:) a a
forall (v :: * -> * -> *) a e. v e a -> Flip v a e
Flip (a
sx a -> a -> a :*: a
forall s a. s -> a -> s :*: a
:*: a
r) Flip (:*:) a a
-> Flip (:*:) a b -> Flip (:*:) a a :*: Flip (:*:) a b
forall s a. s -> a -> s :*: a
:*: (b :*: a) -> Flip (:*:) a b
forall (v :: * -> * -> *) a e. v e a -> Flip v a e
Flip (b
sy b -> a -> b :*: a
forall s a. s -> a -> s :*: a
:*: a
r)

instance Monoidal (<--) (-->) (:*:) (:*:) (Flip (:*:) a) where
	unit :: Proxy (:*:) -> (Unit (:*:) --> a) <-- Flip (:*:) a a
unit Proxy (:*:)
_ = (Flip (:*:) a a -> One --> a)
-> Flip (->) (One --> a) (Flip (:*:) a a)
forall (v :: * -> * -> *) a e. v e a -> Flip v a e
Flip ((Flip (:*:) a a -> One --> a)
 -> Flip (->) (One --> a) (Flip (:*:) a a))
-> (Flip (:*:) a a -> One --> a)
-> Flip (->) (One --> a) (Flip (:*:) a a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! \(Flip (a
s :*: a
_)) -> (One -> a) -> One --> a
forall (v :: * -> * -> *) a e. v a e -> Straight v a e
Straight (\One
_ -> a
s)

--instance Semimonoidal (-->) (:*:) (:*:) (Flip (:*:) a) where
--mult = Straight ! \(Flip ((sx :*: sy) :*: r)) -> Flip (sx :*: r) :*: Flip (sy :*: r)

type Applicative t = (Covariant (->) (->) t, Semimonoidal (-->) (:*:) (:*:) t, Monoidal (-->) (-->) (:*:) (:*:) t)
type Alternative t = (Covariant (->) (->) t, Semimonoidal (-->) (:*:) (:+:) t, Monoidal (-->) (-->) (:*:) (:+:) t)
type Divisible t = (Covariant (->) (->) t, Semimonoidal (<--) (:*:) (:*:) t, Monoidal (-->) (<--) (:*:) (:*:) t)
type Decidable t = (Covariant (->) (->) t, Semimonoidal (<--) (:*:) (:+:) t, Monoidal (-->) (<--) (:*:) (:+:) t)

(<-*-) :: (Covariant (->) (->) t, Semimonoidal (-->) (:*:) (:*:) 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 (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) (u :: * -> *) a b.
Adjoint source target t u =>
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 (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|- (forall k (p :: * -> * -> *) (source :: * -> * -> *)
       (target :: k -> k -> k) (t :: k -> *) (a :: k) (b :: k).
Semimonoidal p source target t =>
p (source (t a) (t b)) (t (target a b))
forall (t :: * -> *) a b.
Semimonoidal (Straight (->)) (:*:) (:*:) t =>
(t a :*: t b) --> t (a :*: b)
mult @(-->) @_ @(:*:) ((t (a -> b) :*: t a) --> t ((a -> b) :*: a))
-> (t (a -> b) :*: t a) -> t ((a -> b) :*: a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! (t (a -> b)
f t (a -> b) -> t a -> t (a -> b) :*: t a
forall s a. s -> a -> s :*: a
:*: t a
x))

(<-*-*-) :: (Covariant (->) (->) t, Covariant (->) (->) u, Semimonoidal (-->) (:*:) (:*:) t, Semimonoidal (-->) (:*:) (:*:) u) => t (u (a -> b)) -> t (u a) -> t (u b)
t (u (a -> b))
f <-*-*- :: t (u (a -> b)) -> t (u a) -> t (u b)
<-*-*- t (u a)
x = u (a -> b) -> u a -> u b
forall (t :: * -> *) a b.
(Covariant (->) (->) t,
 Semimonoidal (Straight (->)) (:*:) (:*:) t) =>
t (a -> b) -> t a -> t b
(<-*-) (u (a -> b) -> u a -> u b) -> t (u (a -> b)) -> t (u a -> u b)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|- t (u (a -> b))
f t (u a -> u b) -> t (u a) -> t (u b)
forall (t :: * -> *) a b.
(Covariant (->) (->) t,
 Semimonoidal (Straight (->)) (:*:) (:*:) t) =>
t (a -> b) -> t a -> t b
<-*- t (u a)
x

(.-*-) :: (Covariant (->) (->) t, Semimonoidal (-->) (:*:) (:*:) t) => t b -> t a -> t b
t b
y .-*- :: t b -> t a -> t b
.-*- t a
x = (\a
_ b
y' -> b
y') (a -> b -> b) -> t a -> t (b -> b)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|- t a
x t (b -> b) -> t b -> t b
forall (t :: * -> *) a b.
(Covariant (->) (->) t,
 Semimonoidal (Straight (->)) (:*:) (:*:) t) =>
t (a -> b) -> t a -> t b
<-*- t b
y

(.-*-*-) :: (Covariant (->) (->) t, Covariant (->) (->) u, Semimonoidal (-->) (:*:) (:*:) t, Semimonoidal (-->) (:*:) (:*:) u) => t (u b) -> t (u a) -> t (u b)
t (u b)
y .-*-*- :: t (u b) -> t (u a) -> t (u b)
.-*-*- t (u a)
x = (\a
_ b
y' -> b
y') (a -> b -> b) -> t (u a) -> t (u (b -> b))
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) (u :: * -> *) a b.
(Covariant source target t,
 Covariant source (Betwixt source target) u,
 Covariant (Betwixt source target) target t) =>
source a b -> target (t (u a)) (t (u b))
<-|-|- t (u a)
x t (u (b -> b)) -> t (u b) -> t (u b)
forall (t :: * -> *) (u :: * -> *) a b.
(Covariant (->) (->) t, Covariant (->) (->) u,
 Semimonoidal (Straight (->)) (:*:) (:*:) t,
 Semimonoidal (Straight (->)) (:*:) (:*:) u) =>
t (u (a -> b)) -> t (u a) -> t (u b)
<-*-*- t (u b)
y

forever_ :: (Covariant (->) (->) t, Semimonoidal (-->) (:*:) (:*:) t) => t a -> t b
forever_ :: t a -> t b
forever_ t a
x = let r :: t b
r = t b
r t b -> t a -> t b
forall (t :: * -> *) b a.
(Covariant (->) (->) t,
 Semimonoidal (Straight (->)) (:*:) (:*:) t) =>
t b -> t a -> t b
.-*- t a
x in t b
r

(<-+-) :: (Covariant (->) (->) t, Semimonoidal (-->) (:*:) (:+:) t) => t b -> t a -> (a :+: b -> r) -> t r
t b
y <-+- :: t b -> t a -> ((a :+: b) -> r) -> t r
<-+- t a
x = \(a :+: b) -> r
f -> (a :+: b) -> r
f ((a :+: b) -> r) -> t (a :+: b) -> t r
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|- (forall k (p :: * -> * -> *) (source :: * -> * -> *)
       (target :: k -> k -> k) (t :: k -> *) (a :: k) (b :: k).
Semimonoidal p source target t =>
p (source (t a) (t b)) (t (target a b))
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Semimonoidal (Straight (->)) source target t =>
source (t a) (t b) --> t (target a b)
mult @(-->) ((t a :*: t b) --> t (a :+: b)) -> (t a :*: t b) -> t (a :+: b)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! (t a
x t a -> t b -> t a :*: t b
forall s a. s -> a -> s :*: a
:*: t b
y))

(.-+-) :: (Covariant (->) (->) t, Semimonoidal (-->) (:*:) (:+:) t) => t a -> t a -> t a
t a
y .-+- :: t a -> t a -> t a
.-+- t a
x = (\a :+: a
r -> case a :+: a
r of Option a
rx -> a
rx; Adoption a
ry -> a
ry) ((a :+: a) -> a) -> t (a :+: a) -> t a
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|- (forall k (p :: * -> * -> *) (source :: * -> * -> *)
       (target :: k -> k -> k) (t :: k -> *) (a :: k) (b :: k).
Semimonoidal p source target t =>
p (source (t a) (t b)) (t (target a b))
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Semimonoidal (Straight (->)) source target t =>
source (t a) (t b) --> t (target a b)
mult @(-->) ((t a :*: t a) --> t (a :+: a)) -> (t a :*: t a) -> t (a :+: a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! (t a
x t a -> t a -> t a :*: t a
forall s a. s -> a -> s :*: a
:*: t a
y))

type Extractable t = Monoidal (<--) (-->) (:*:) (:*:) t
type Pointable t = Monoidal (-->) (-->) (:*:) (:*:) t
type Emptiable t = Monoidal (-->) (-->) (:*:) (:+:) t

extract :: Extractable t => t a -> a
extract :: t a -> a
extract t a
j = Proxy (:*:) -> (Unit (:*:) --> a) <-- t a
forall (p :: * -> * -> *) (q :: * -> * -> *)
       (source :: * -> * -> *) (target :: * -> * -> *) (t :: * -> *) a.
Monoidal p q source target t =>
Proxy source -> p (q (Unit target) a) (t a)
unit @(<--) @(-->) Proxy (:*:)
forall k (a :: k). Proxy a
Proxy Flip (->) (Straight (->) One a) (t a) -> t a -> Straight (->) One a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! t a
j Straight (->) One a -> One -> a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! One
One

point :: Pointable t => a -> t a
point :: a -> t a
point a
x = Proxy (:*:) -> Straight (->) (Unit (:*:)) a --> t a
forall (p :: * -> * -> *) (q :: * -> * -> *)
       (source :: * -> * -> *) (target :: * -> * -> *) (t :: * -> *) a.
Monoidal p q source target t =>
Proxy source -> p (q (Unit target) a) (t a)
unit @(-->) Proxy (:*:)
forall k (a :: k). Proxy a
Proxy Straight (->) (Straight (->) One a) (t a)
-> Straight (->) One a -> t a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! ((One -> a) -> Straight (->) One a
forall (v :: * -> * -> *) a e. v a e -> Straight v a e
Straight ((One -> a) -> Straight (->) One a)
-> (One -> a) -> Straight (->) One a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! \One
One -> a
x)

pass :: Pointable t => t ()
pass :: t ()
pass = () -> t ()
forall (t :: * -> *) a. Pointable t => a -> t a
point ()

empty :: Emptiable t => t a
empty :: t a
empty = Proxy (:*:) -> Straight (->) (Unit (:+:)) a --> t a
forall (p :: * -> * -> *) (q :: * -> * -> *)
       (source :: * -> * -> *) (target :: * -> * -> *) (t :: * -> *) a.
Monoidal p q source target t =>
Proxy source -> p (q (Unit target) a) (t a)
unit @(-->) Proxy (:*:)
forall k (a :: k). Proxy a
Proxy Straight (->) (Straight (->) Zero a) (t a)
-> Straight (->) Zero a -> t a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! (Zero -> a) -> Straight (->) Zero a
forall (v :: * -> * -> *) a e. v a e -> Straight v a e
Straight Zero -> a
forall a. Zero -> a
absurd

--instance Appliable (->) b c (->) e d => Appliable (->) a (b -> c) (->) (a :*: e) d where
--	f ! (x :*: y) = f x ! y

(<-|-<-|-) :: forall (m :: * -> * -> *) (p :: * -> * -> *) a b c d .
	(Covariant m m (p a), Covariant m m (Flip p d), Interpreted m (Flip p d))
	=> m a b :*: m c d -> m (p a c) (p b d)
<-|-<-|- :: (m a b :*: m c d) -> m (p a c) (p b d)
(<-|-<-|-) (m a b
f :*: m c d
g) = m (Flip p d a) (Flip p d b)
-> m (Primary (Flip p d) a) (Primary (Flip p d) b)
forall (m :: * -> * -> *) (t :: * -> *) (u :: * -> *) a b.
(Interpreted m t, Semigroupoid m, Interpreted m u) =>
m (t a) (u b) -> m (Primary t a) (Primary u b)
(=||) @m @(Flip p d) (m a b -> m (Flip p d a) (Flip p d b)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
(<-|-) m a b
f) m (p a d) (p b d) -> m (p a c) (p a d) -> m (p a c) (p b d)
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (m c d -> m (p a c) (p a d)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
(<-|-) m c d
g)

(<-|->-|-) :: forall (m :: * -> * -> *) (p :: * -> * -> *) a b c d .
	(Covariant m m (Flip p c), Contravariant m m (p a), Interpreted m (Flip p c))
	=> m a b :*: m c d -> m (p a d) (p b c)
<-|->-|- :: (m a b :*: m c d) -> m (p a d) (p b c)
(<-|->-|-) (m a b
f :*: m c d
g) = m (Flip p c a) (Flip p c b)
-> m (Primary (Flip p c) a) (Primary (Flip p c) b)
forall (m :: * -> * -> *) (t :: * -> *) (u :: * -> *) a b.
(Interpreted m t, Semigroupoid m, Interpreted m u) =>
m (t a) (u b) -> m (Primary t a) (Primary u b)
(=||) @m @(Flip p c) (m a b -> m (Flip p c a) (Flip p c b)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
(<-|-) m a b
f) m (p a c) (p b c) -> m (p a d) (p a c) -> m (p a d) (p b c)
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (m c d -> m (p a d) (p a c)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Contravariant source target t =>
source a b -> target (t b) (t a)
(>-|-) m c d
g)

(>-|-<-|-) :: forall (m :: * -> * -> *) (p :: * -> * -> *) a b c d .
	(Contravariant m m (Flip p d), Covariant m m (p b), Interpreted m (Flip p d))
	=> m a b :*: m c d -> m (p b c) (p a d)
>-|-<-|- :: (m a b :*: m c d) -> m (p b c) (p a d)
(>-|-<-|-) (m a b
f :*: m c d
g) = m (Flip p d b) (Flip p d a)
-> m (Primary (Flip p d) b) (Primary (Flip p d) a)
forall (m :: * -> * -> *) (t :: * -> *) (u :: * -> *) a b.
(Interpreted m t, Semigroupoid m, Interpreted m u) =>
m (t a) (u b) -> m (Primary t a) (Primary u b)
(=||) @m @(Flip p d) (m a b -> m (Flip p d b) (Flip p d a)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Contravariant source target t =>
source a b -> target (t b) (t a)
(>-|-) m a b
f) m (p b d) (p a d) -> m (p b c) (p b d) -> m (p b c) (p a d)
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (m c d -> m (p b c) (p b d)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
(<-|-) m c d
g)

(>-|->-|-) :: forall (m :: * -> * -> *) (p :: * -> * -> *) a b c d .
	(Contravariant m m (p b), Contravariant m m (Flip p c), Interpreted m (Flip p c))
	=> m a b :*: m c d -> m (p b d) (p a c)
>-|->-|- :: (m a b :*: m c d) -> m (p b d) (p a c)
(>-|->-|-) (m a b
f :*: m c d
g) = m (Flip p c b) (Flip p c a)
-> m (Primary (Flip p c) b) (Primary (Flip p c) a)
forall (m :: * -> * -> *) (t :: * -> *) (u :: * -> *) a b.
(Interpreted m t, Semigroupoid m, Interpreted m u) =>
m (t a) (u b) -> m (Primary t a) (Primary u b)
(=||) @m @(Flip p c) (m a b -> m (Flip p c b) (Flip p c a)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Contravariant source target t =>
source a b -> target (t b) (t a)
(>-|-) m a b
f) m (p b c) (p a c) -> m (p b d) (p b c) -> m (p b d) (p a c)
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (m c d -> m (p b d) (p b c)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Contravariant source target t =>
source a b -> target (t b) (t a)
(>-|-) m c d
g)