{-# LANGUAGE UndecidableInstances #-}
module Pandora.Paradigm.Primary.Transformer.Construction where

import Pandora.Core.Functor (type (:.), type (>>>), type (:=>), type (~>))
import Pandora.Core.Interpreted (Interpreted (Primary, run, unite, (<~), (<~~~), (<~~~~)))
import Pandora.Pattern.Morphism.Flip (Flip (Flip))
import Pandora.Pattern.Morphism.Straight (Straight (Straight))
import Pandora.Pattern.Semigroupoid ((.))
import Pandora.Pattern.Category ((<--), (<---), (<----), (<-----), (<------))
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.Extendable (Extendable ((<<=)))
import Pandora.Pattern.Functor.Comonad (Comonad)
import Pandora.Pattern.Transformer.Lowerable (Lowerable (lower))
import Pandora.Pattern.Transformer.Hoistable (Hoistable ((/|\)))
import Pandora.Pattern.Object.Setoid (Setoid ((==)))
import Pandora.Pattern.Object.Semigroup (Semigroup ((+)))
import Pandora.Pattern.Object.Ringoid ((*))
import Pandora.Pattern.Object.Monoid (Monoid (zero))
import Pandora.Paradigm.Algebraic ((<-*------), extract)
import Pandora.Paradigm.Algebraic.Exponential (type (<--), type (-->))
import Pandora.Paradigm.Algebraic.Product ((:*:) ((:*:)), type (<:*:>), (<:*:>))
import Pandora.Paradigm.Algebraic.Sum ((:+:))
import Pandora.Paradigm.Algebraic.One (One (One))
import Pandora.Paradigm.Algebraic (empty, (<-||-))
import Pandora.Paradigm.Primary.Functor.Exactly (Exactly (Exactly))
import Pandora.Paradigm.Schemes (TT (TT), T_U (T_U), type (<::>))

data Construction t a = Construct a (t :. Construction t >>> a)

instance Covariant (->) (->) t => Covariant (->) (->) (Construction t) where
	a -> b
f <-|- :: (a -> b) -> Construction t a -> Construction t b
<-|- ~(Construct a
x (t :. Construction t) >>> a
xs) = b -> ((t :. Construction t) >>> b) -> Construction t b
forall (t :: * -> *) a.
a -> ((t :. Construction t) >>> a) -> Construction t a
Construct (b -> ((t :. Construction t) >>> b) -> Construction t b)
-> b -> ((t :. Construction t) >>> b) -> Construction t b
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<------ a -> b
f a
x (((t :. Construction t) >>> b) -> Construction t b)
-> ((t :. Construction t) >>> b) -> Construction t b
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<------ a -> b
f (a -> b)
-> ((t :. Construction t) >>> a) -> (t :. Construction t) >>> 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 :. Construction t) >>> a
xs

instance (Covariant (->) (->) t, Semimonoidal (-->) (:*:) (:*:) t) => Semimonoidal (-->) (:*:) (:*:) (Construction t) where
	mult :: (Construction t a :*: Construction t b)
--> Construction t (a :*: b)
mult = ((Construction t a :*: Construction t b)
 -> Construction t (a :*: b))
-> (Construction t a :*: Construction t b)
   --> Construction t (a :*: b)
forall (v :: * -> * -> *) a e. v a e -> Straight v a e
Straight (((Construction t a :*: Construction t b)
  -> Construction t (a :*: b))
 -> (Construction t a :*: Construction t b)
    --> Construction t (a :*: b))
-> ((Construction t a :*: Construction t b)
    -> Construction t (a :*: b))
-> (Construction t a :*: Construction t b)
   --> Construction t (a :*: b)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- \(Construct a
x (t :. Construction t) >>> a
xs :*: Construct b
y (t :. Construction t) >>> b
ys) -> (a :*: b)
-> ((t :. Construction t) >>> (a :*: b))
-> Construction t (a :*: b)
forall (t :: * -> *) a.
a -> ((t :. Construction t) >>> a) -> Construction t a
Construct ((a :*: b)
 -> ((t :. Construction t) >>> (a :*: b))
 -> Construction t (a :*: b))
-> (a :*: b)
-> ((t :. Construction t) >>> (a :*: b))
-> Construction t (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
		(((t :. Construction t) >>> (a :*: b)) -> Construction t (a :*: b))
-> ((t :. Construction t) >>> (a :*: b))
-> Construction t (a :*: b)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a 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 (-->) source target t =>
source (t a) (t b) --> t (target a b)
mult @(-->) ((Construction t a :*: Construction t b)
 --> Construction t (a :*: b))
-> (Construction t a :*: Construction t b)
-> Construction t (a :*: b)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
<~) ((Construction t a :*: Construction t b)
 -> Construction t (a :*: b))
-> t (Construction t a :*: Construction t b)
-> (t :. Construction t) >>> (a :*: 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 (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Semimonoidal (-->) source target t =>
source (t a) (t b) --> t (target a b)
mult @(-->) ((((t :. Construction t) >>> a) :*: ((t :. Construction t) >>> b))
 --> t (Construction t a :*: Construction t b))
-> (((t :. Construction t) >>> a)
    :*: ((t :. Construction t) >>> b))
-> t (Construction t a :*: Construction t b)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
<~~~ (t :. Construction t) >>> a
xs ((t :. Construction t) >>> a)
-> ((t :. Construction t) >>> b)
-> ((t :. Construction t) >>> a) :*: ((t :. Construction t) >>> b)
forall s a. s -> a -> s :*: a
:*: (t :. Construction t) >>> b
ys

instance (Covariant (->) (->) t, Semimonoidal (<--) (:*:) (:*:) t) => Semimonoidal (<--) (:*:) (:*:) (Construction t) where
	mult :: (Construction t a :*: Construction t b)
<-- Construction t (a :*: b)
mult = (Construction t (a :*: b) -> Construction t a :*: Construction t b)
-> (Construction t a :*: Construction t b)
   <-- Construction t (a :*: b)
forall (v :: * -> * -> *) a e. v e a -> Flip v a e
Flip ((Construction t (a :*: b)
  -> Construction t a :*: Construction t b)
 -> (Construction t a :*: Construction t b)
    <-- Construction t (a :*: b))
-> (Construction t (a :*: b)
    -> Construction t a :*: Construction t b)
-> (Construction t a :*: Construction t b)
   <-- Construction t (a :*: b)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- \(Construct (a
x :*: b
y) (t :. Construction t) >>> (a :*: b)
xys) -> (a -> ((t :. Construction t) >>> a) -> Construction t a
forall (t :: * -> *) a.
a -> ((t :. Construction t) >>> a) -> Construction t a
Construct a
x (((t :. Construction t) >>> a) -> Construction t a)
-> (((t :. Construction t) >>> a) :*: Construction t b)
-> Construction t a :*: Construction t b
forall (m :: * -> * -> *) (p :: * -> * -> *) a b c.
(Covariant m m (Flip p c), Interpreted m (Flip p c)) =>
m a b -> m (p a c) (p b c)
<-||-) ((((t :. Construction t) >>> a) :*: Construction t b)
 -> Construction t a :*: Construction t b)
-> ((((t :. Construction t) >>> a)
     :*: ((t :. Construction t) >>> b))
    -> ((t :. Construction t) >>> a) :*: Construction t b)
-> (((t :. Construction t) >>> a)
    :*: ((t :. Construction t) >>> b))
-> Construction t a :*: Construction t b
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (b -> ((t :. Construction t) >>> b) -> Construction t b
forall (t :: * -> *) a.
a -> ((t :. Construction t) >>> a) -> Construction t a
Construct b
y (((t :. Construction t) >>> b) -> Construction t b)
-> (((t :. Construction t) >>> a)
    :*: ((t :. Construction t) >>> b))
-> ((t :. Construction t) >>> a) :*: Construction t b
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|-)
		((((t :. Construction t) >>> a) :*: ((t :. Construction t) >>> b))
 -> Construction t a :*: Construction t b)
-> (((t :. Construction t) >>> a)
    :*: ((t :. Construction t) >>> b))
-> Construction t a :*: Construction t b
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a 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 (<--) source target t =>
source (t a) (t b) <-- t (target a b)
mult @(<--) ((((t :. Construction t) >>> a) :*: ((t :. Construction t) >>> b))
 <-- t (Construction t a :*: Construction t b))
-> t (Construction t a :*: Construction t b)
-> ((t :. Construction t) >>> a) :*: ((t :. Construction t) >>> b)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t 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 @(<--) ((Construction t a :*: Construction t b)
 <-- Construction t (a :*: b))
-> Construction t (a :*: b)
-> Construction t a :*: Construction t b
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
<~) (Construction t (a :*: b) -> Construction t a :*: Construction t b)
-> ((t :. Construction t) >>> (a :*: b))
-> t (Construction t a :*: Construction t b)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|- (t :. Construction t) >>> (a :*: b)
xys

instance (Covariant (->) (->) t, Semimonoidal (<--) (:*:) (:*:) t) => Monoidal (<--) (-->) (:*:) (:*:) (Construction t) where
	unit :: Proxy (:*:) -> (Unit (:*:) --> a) <-- Construction t a
unit Proxy (:*:)
_ = (Construction t a -> Straight (->) One a)
-> Flip (->) (Straight (->) One a) (Construction t a)
forall (v :: * -> * -> *) a e. v e a -> Flip v a e
Flip ((Construction t a -> Straight (->) One a)
 -> Flip (->) (Straight (->) One a) (Construction t a))
-> (Construction t a -> Straight (->) One a)
-> Flip (->) (Straight (->) One a) (Construction t a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- \(Construct a
x (t :. Construction t) >>> a
_) -> (One -> a) -> Straight (->) One a
forall (v :: * -> * -> *) a e. v a e -> Straight v a e
Straight (\One
_ -> a
x)

instance (Covariant (->) (->) t, Semimonoidal (-->) (:*:) (:*:) t, Monoidal (-->) (-->) (:*:) (:+:) t) => Monoidal (-->) (-->) (:*:) (:*:) (Construction t) where
	unit :: Proxy (:*:) -> (Unit (:*:) --> a) --> Construction t a
unit Proxy (:*:)
_ = (Straight (->) One a -> Construction t a)
-> Straight (->) (Straight (->) One a) (Construction t a)
forall (v :: * -> * -> *) a e. v a e -> Straight v a e
Straight ((Straight (->) One a -> Construction t a)
 -> Straight (->) (Straight (->) One a) (Construction t a))
-> (Straight (->) One a -> Construction t a)
-> Straight (->) (Straight (->) One a) (Construction t a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- \Straight (->) One a
f -> a -> ((t :. Construction t) >>> a) -> Construction t a
forall (t :: * -> *) a.
a -> ((t :. Construction t) >>> a) -> Construction t a
Construct (a -> ((t :. Construction t) >>> a) -> Construction t a)
-> a -> ((t :. Construction t) >>> a) -> Construction t a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- Straight (->) One a -> One -> a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run Straight (->) One a
f One
One (((t :. Construction t) >>> a) -> Construction t a)
-> ((t :. Construction t) >>> a) -> Construction t a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- (t :. Construction t) >>> a
forall (t :: * -> *) a. Emptiable t => t a
empty

instance Traversable (->) (->) t => Traversable (->) (->) (Construction t) where
	a -> u b
f <-/- :: (a -> u b) -> Construction t a -> u (Construction t b)
<-/- ~(Construct a
x (t :. Construction t) >>> a
xs) = b -> ((t :. Construction t) >>> b) -> Construction t b
forall (t :: * -> *) a.
a -> ((t :. Construction t) >>> a) -> Construction t a
Construct (b -> ((t :. Construction t) >>> b) -> Construction t b)
-> u b -> u (((t :. Construction t) >>> b) -> Construction t 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 u (((t :. Construction t) >>> b) -> Construction t b)
-> u ((t :. Construction t) >>> b) -> u (Construction t b)
forall (t :: * -> *) a b.
(Covariant (->) (->) t, Semimonoidal (-->) (:*:) (:*:) t) =>
t (a -> b) -> t a -> t b
<-*------ a -> u b
f (a -> u b)
-> ((t :. Construction t) >>> a) -> u ((t :. Construction t) >>> b)
forall (t :: * -> *) (u :: * -> *) (v :: * -> *)
       (category :: * -> * -> *) a b.
(Traversable category category t, Covariant category category u,
 Monoidal (Straight category) (Straight category) (:*:) (:*:) u,
 Traversable category category v) =>
category a (u b) -> category (v (t a)) (u (v (t b)))
<-/-/- (t :. Construction t) >>> a
xs

instance Covariant (->) (->) t => Extendable (->) (Construction t) where
	Construction t a -> b
f <<= :: (Construction t a -> b) -> Construction t a -> Construction t b
<<= Construction t a
x = b -> ((t :. Construction t) >>> b) -> Construction t b
forall (t :: * -> *) a.
a -> ((t :. Construction t) >>> a) -> Construction t a
Construct (b -> ((t :. Construction t) >>> b) -> Construction t b)
-> b -> ((t :. Construction t) >>> b) -> Construction t b
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<---- Construction t a -> b
f Construction t a
x (((t :. Construction t) >>> b) -> Construction t b)
-> ((t :. Construction t) >>> b) -> Construction t b
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<---- (Construction t a -> b
f (Construction t a -> b) -> Construction t a -> Construction t b
forall (source :: * -> * -> *) (t :: * -> *) a b.
Extendable source t =>
source (t a) b -> source (t a) (t b)
<<=) (Construction t a -> Construction t b)
-> t (Construction t a) -> (t :. Construction t) >>> b
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|- Construction t a -> t (Construction t a)
forall (t :: * -> *) a.
Construction t a -> (t :. Construction t) >>> a
deconstruct Construction t a
x

instance (Covariant (->) (->) t, Semimonoidal (<--) (:*:) (:*:) t) => Comonad (->) (Construction t) where

instance (forall u . Semimonoidal (<--) (:*:) (:*:) u) => Lowerable (->) Construction where
	lower :: Construction u a -> u a
lower Construction u a
x = Construction u a -> a
forall (t :: * -> *) a. Extractable t => t a -> a
extract (Construction u a -> a) -> u (Construction u a) -> u a
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|- Construction u a -> u (Construction u a)
forall (t :: * -> *) a.
Construction t a -> (t :. Construction t) >>> a
deconstruct Construction u a
x

instance (forall u . Semimonoidal (<--) (:*:) (:*:) u, forall u . Covariant (->) (->) u) => Hoistable (->) Construction where
	forall a. u a -> v a
f /|\ :: (forall a. u a -> v a)
-> forall a. Construction u a -> Construction v a
/|\ Construction u a
x = a -> ((v :. Construction v) >>> a) -> Construction v a
forall (t :: * -> *) a.
a -> ((t :. Construction t) >>> a) -> Construction t a
Construct (a -> ((v :. Construction v) >>> a) -> Construction v a)
-> a -> ((v :. Construction v) >>> a) -> Construction v a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<---- Construction u a -> a
forall (t :: * -> *) a. Extractable t => t a -> a
extract Construction u a
x (((v :. Construction v) >>> a) -> Construction v a)
-> ((v :. Construction v) >>> a) -> Construction v a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<---- (forall a. u a -> v a)
-> forall a. Construction u a -> Construction v a
forall k (m :: * -> * -> *) (t :: (* -> *) -> k -> *) (u :: * -> *)
       (v :: * -> *).
(Hoistable m t, Covariant m m u) =>
(forall a. m (u a) (v a)) -> forall (a :: k). m (t u a) (t v a)
(/|\) @(->) forall a. u a -> v a
f (Construction u a -> Construction v a)
-> v (Construction u a) -> (v :. Construction v) >>> a
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|- u (Construction u a) -> v (Construction u a)
forall a. u a -> v a
f (Construction u a -> u (Construction u a)
forall (t :: * -> *) a.
Construction t a -> (t :. Construction t) >>> a
deconstruct Construction u a
x)

instance (Setoid a, forall b . Setoid b => Setoid (t b), Covariant (->) (->) t, Semimonoidal (<--) (:*:) (:*:) t) => Setoid (Construction t a) where
	Construction t a
x == :: Construction t a -> Construction t a -> Boolean
== Construction t a
y = (Construction t a -> a
forall (t :: * -> *) a. Extractable t => t a -> a
extract Construction t a
x a -> a -> Boolean
forall a. Setoid a => a -> a -> Boolean
== Construction t a -> a
forall (t :: * -> *) a. Extractable t => t a -> a
extract Construction t a
y) Boolean -> Boolean -> Boolean
forall a. Ringoid a => a -> a -> a
* (Construction t a -> (t :. Construction t) >>> a
forall (t :: * -> *) a.
Construction t a -> (t :. Construction t) >>> a
deconstruct Construction t a
x ((t :. Construction t) >>> a)
-> ((t :. Construction t) >>> a) -> Boolean
forall a. Setoid a => a -> a -> Boolean
== Construction t a -> (t :. Construction t) >>> a
forall (t :: * -> *) a.
Construction t a -> (t :. Construction t) >>> a
deconstruct Construction t a
y)

instance (Semigroup a, forall b . Semigroup b => Semigroup (t b), Covariant (->) (->) t, Semimonoidal (<--) (:*:) (:*:) t) => Semigroup (Construction t a) where
	Construction t a
x + :: Construction t a -> Construction t a -> Construction t a
+ Construction t a
y = a -> ((t :. Construction t) >>> a) -> Construction t a
forall (t :: * -> *) a.
a -> ((t :. Construction t) >>> a) -> Construction t a
Construct (a -> ((t :. Construction t) >>> a) -> Construction t a)
-> a -> ((t :. Construction t) >>> a) -> Construction t a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- Construction t a -> a
forall (t :: * -> *) a. Extractable t => t a -> a
extract Construction t a
x a -> a -> a
forall a. Semigroup a => a -> a -> a
+ Construction t a -> a
forall (t :: * -> *) a. Extractable t => t a -> a
extract Construction t a
y (((t :. Construction t) >>> a) -> Construction t a)
-> ((t :. Construction t) >>> a) -> Construction t a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- Construction t a -> (t :. Construction t) >>> a
forall (t :: * -> *) a.
Construction t a -> (t :. Construction t) >>> a
deconstruct Construction t a
x ((t :. Construction t) >>> a)
-> ((t :. Construction t) >>> a) -> (t :. Construction t) >>> a
forall a. Semigroup a => a -> a -> a
+ Construction t a -> (t :. Construction t) >>> a
forall (t :: * -> *) a.
Construction t a -> (t :. Construction t) >>> a
deconstruct Construction t a
y

instance (Monoid a, forall b . Semigroup b => Monoid (t b), Covariant (->) (->) t, Semimonoidal (<--) (:*:) (:*:) t) => Monoid (Construction t a) where
	zero :: Construction t a
zero = a -> ((t :. Construction t) >>> a) -> Construction t a
forall (t :: * -> *) a.
a -> ((t :. Construction t) >>> a) -> Construction t a
Construct a
forall a. Monoid a => a
zero (t :. Construction t) >>> a
forall a. Monoid a => a
zero

instance Interpreted (->) (Construction t) where
	type Primary (Construction t) a = (Exactly <:*:> t <::> Construction t) a
	run :: ((->) < Construction t a) < Primary (Construction t) a
run (Construct a
x (t :. Construction t) >>> a
xs) = a -> Exactly a
forall a. a -> Exactly a
Exactly a
x Exactly a
-> (<::>) t (Construction t) a
-> (Exactly <:*:> (t <::> Construction t)) >>>>>> a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (t <:*:> u) >>>>>> a
<:*:> ((t :. Construction t) >>> a) -> (<::>) t (Construction t) a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < Primary t a) < t a
unite (t :. Construction t) >>> a
xs
	unite :: ((->) < Primary (Construction t) a) < Construction t a
unite (T_U (Exactly x :*: TT xs)) = a -> ((t :. Construction t) >>> a) -> Construction t a
forall (t :: * -> *) a.
a -> ((t :. Construction t) >>> a) -> Construction t a
Construct a
x (t :. Construction t) >>> a
xs

-- instance Monotonic a (t :. Construction t > a) => Monotonic a (Construction t a) where
-- 	reduce f r ~(Construct x xs) = f x <-- reduce f r xs
--
-- instance Monotonic a (t :. Construction t > a) => Monotonic a (t <::> Construction t > a) where
-- 	reduce f r = reduce f r . run

deconstruct :: Construction t a -> t :. Construction t >>> a
deconstruct :: Construction t a -> (t :. Construction t) >>> a
deconstruct ~(Construct a
_ (t :. Construction t) >>> a
xs) = (t :. Construction t) >>> a
xs

-- Generate a construction from seed using effectful computation
constitute :: Covariant (->) (->) t => (a -> t a) -> a -> Construction t a
constitute :: (a -> t a) -> a -> Construction t a
constitute a -> t a
f a
x = a -> ((t :. Construction t) >>> a) -> Construction t a
forall (t :: * -> *) a.
a -> ((t :. Construction t) >>> a) -> Construction t a
Construct a
x (((t :. Construction t) >>> a) -> Construction t a)
-> ((t :. Construction t) >>> a) -> Construction t a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<---- (a -> t a) -> a -> Construction t a
forall (t :: * -> *) a.
Covariant (->) (->) t =>
(a -> t a) -> a -> Construction t a
constitute a -> t a
f (a -> Construction t a) -> t a -> (t :. Construction t) >>> a
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|- a -> t a
f a
x

section :: (Comonad (->) t, Monoidal (<--) (-->) (:*:) (:*:) t) => t ~> Construction t
section :: t ~> Construction t
section t a
xs = a -> ((t :. Construction t) >>> a) -> Construction t a
forall (t :: * -> *) a.
a -> ((t :. Construction t) >>> a) -> Construction t a
Construct (a -> ((t :. Construction t) >>> a) -> Construction t a)
-> a -> ((t :. Construction t) >>> a) -> Construction t a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- t a -> a
forall (t :: * -> *) a. Extractable t => t a -> a
extract t a
xs (((t :. Construction t) >>> a) -> Construction t a)
-> ((t :. Construction t) >>> a) -> Construction t a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- t a -> Construction t a
forall (t :: * -> *).
(Comonad (->) t, Monoidal (<--) (-->) (:*:) (:*:) t) =>
t ~> Construction t
section (t a -> Construction t a) -> t a -> (t :. Construction t) >>> a
forall (source :: * -> * -> *) (t :: * -> *) a b.
Extendable source t =>
source (t a) b -> source (t a) (t b)
<<= t a
xs