{-# LANGUAGE UndecidableInstances #-}

module Pandora.Paradigm.Primary.Transformer.Construction where

import Pandora.Core.Functor (type (:.), type (:=), type (:=>), type (~>))
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.Functor.Bivariant ((<->))
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.Primary.Algebraic ((<-*-), extract)
import Pandora.Paradigm.Primary.Algebraic.Exponential (type (<--), type (-->))
import Pandora.Paradigm.Primary.Algebraic.Product ((:*:) ((:*:)))
import Pandora.Paradigm.Primary.Algebraic.Sum ((:+:))
import Pandora.Paradigm.Primary.Algebraic.One (One (One))
import Pandora.Paradigm.Primary.Algebraic (empty)
import Pandora.Pattern.Morphism.Flip (Flip (Flip))
import Pandora.Pattern.Morphism.Straight (Straight (Straight))
import Pandora.Paradigm.Controlflow.Effect.Interpreted (run, (!))
import Pandora.Paradigm.Structure.Ability.Monotonic (Monotonic (reduce))
import Pandora.Paradigm.Schemes (type (<::>))

infixr 7 .-+

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 :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! \(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 :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! \(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) := b) -> Construction t b)
-> (((t :. Construction t) := a) :*: ((t :. Construction t) := b))
-> Construction t a :*: Construction t b
forall (left :: * -> * -> *) (right :: * -> * -> *)
       (target :: * -> * -> *) (v :: * -> * -> *) a b c d.
Bivariant left right target v =>
left a b -> right c d -> target (v a c) (v b d)
<-> 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) := a) :*: ((t :. Construction t) := b))
 -> Construction t a :*: 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)
-> Construction t a :*: Construction t b
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (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)
!) (t (Construction t a :*: Construction t b)
 -> Construction t a :*: Construction t b)
-> t (Construction t a :*: Construction t b)
-> Construction t a :*: 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 -> One --> a)
-> Flip (->) (One --> a) (Construction t a)
forall (v :: * -> * -> *) a e. v e a -> Flip v a e
Flip ((Construction t a -> One --> a)
 -> Flip (->) (One --> a) (Construction t a))
-> (Construction t a -> One --> a)
-> Flip (->) (One --> a) (Construction t a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! \(Construct a
x (t :. Construction t) := a
_) -> (One -> a) -> One --> a
forall (v :: * -> * -> *) a e. v a e -> Straight v a e
Straight (\One
_ -> a
x)

--instance (Covariant (->) (->) t, Semimonoidal (-->) (:*:) (:+:) t) => Semimonoidal (-->) (:*:) (:+:) (Construction t) where
	--mult = Straight ! \(Construct x xs :*: Construct y ys) ->

instance (Covariant (->) (->) t, Semimonoidal (-->) (:*:) (:*:) t, Monoidal (-->) (-->) (:*:) (:+:) t) => Monoidal (-->) (-->) (:*:) (:*:) (Construction t) where
	unit :: Proxy (:*:) -> (Unit (:*:) --> a) --> Construction t a
unit Proxy (:*:)
_ = ((One --> a) -> Construction t a)
-> Straight (->) (One --> a) (Construction t a)
forall (v :: * -> * -> *) a e. v a e -> Straight v a e
Straight (((One --> a) -> Construction t a)
 -> Straight (->) (One --> a) (Construction t a))
-> ((One --> a) -> Construction t a)
-> Straight (->) (One --> a) (Construction t a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! \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)
# (One --> a) -> One -> a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run 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 :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! (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 Monotonic a (t :. Construction t := a) => Monotonic a (Construction t a) where
	reduce :: (a -> r -> r) -> r -> Construction t a -> r
reduce a -> r -> r
f r
r ~(Construct a
x (t :. Construction t) := a
xs) = a -> r -> r
f a
x (r -> r) -> r -> r
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! (a -> r -> r) -> r -> ((t :. Construction t) := a) -> r
forall a e r. Monotonic a e => (a -> r -> r) -> r -> e -> r
reduce a -> r -> r
f r
r (t :. Construction t) := a
xs

instance Monotonic a (t :. Construction t := a) => Monotonic a (t <::> Construction t := a) where
	reduce :: (a -> r -> r) -> r -> ((t <::> Construction t) := a) -> r
reduce a -> r -> r
f r
r = (a -> r -> r) -> r -> ((t :. Construction t) := a) -> r
forall a e r. Monotonic a e => (a -> r -> r) -> r -> e -> r
reduce a -> r -> r
f r
r (((t :. Construction t) := a) -> r)
-> (((t <::> Construction t) := a) -> (t :. Construction t) := a)
-> ((t <::> Construction t) := a)
-> r
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. ((t <::> Construction t) := a) -> (t :. Construction t) := a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
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
(.-+) :: Covariant (->) (->) t => a :=> t -> a :=> Construction t
a :=> t
f .-+ :: (a :=> t) -> a :=> Construction t
.-+ 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 :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! (a :=> t
f (a :=> t) -> a :=> Construction t
forall (t :: * -> *) a.
Covariant (->) (->) t =>
(a :=> t) -> a :=> Construction t
.-+) (a :=> Construction t) -> 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
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 :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! 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