{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE UndecidableInstances #-}
module Pandora.Paradigm.Structure.Ability.Substructure where
import Pandora.Core.Functor (type (:=))
import Pandora.Pattern.Semigroupoid (Semigroupoid ((.)))
import Pandora.Pattern.Category (identity)
import Pandora.Pattern.Functor.Covariant (Covariant ((<-|-)))
import Pandora.Pattern.Transformer.Liftable (lift)
import Pandora.Pattern.Transformer.Lowerable (lower)
import Pandora.Paradigm.Controlflow.Effect.Interpreted ((||=))
import Pandora.Paradigm.Inventory.Some.Store (Store (Store))
import Pandora.Paradigm.Inventory.Some.Optics (Lens, Convex, type (#=@))
import Pandora.Paradigm.Primary.Algebraic.Product ((:*:) ((:*:)))
import Pandora.Paradigm.Primary.Algebraic ((>-|-<-|-))
import Pandora.Paradigm.Primary.Functor.Identity (Identity)
import Pandora.Paradigm.Primary.Functor.Tagged (Tagged)
import Pandora.Paradigm.Schemes.TU (type (<:.>))
import Pandora.Paradigm.Schemes.P_Q_T (P_Q_T (P_Q_T))
import Pandora.Paradigm.Controlflow.Effect.Interpreted ((!))
data Segment a = Root a | Tail a
type Substructured segment source available target = (Substructure segment source,
Substance segment source ~ target, Available segment source ~ available)
class Substructure segment (structure :: * -> *) where
type Available segment structure :: * -> *
type Substance segment structure :: * -> *
substructure :: (Tagged segment <:.> structure) #=@ Substance segment structure := Available segment structure
sub :: (Covariant (->) (->) structure) => structure #=@ Substance segment structure := Available segment structure
sub = (structure a -> TU Covariant Covariant (Tagged segment) structure a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (structure a
-> TU Covariant Covariant (Tagged segment) structure a)
-> (Store
(Available segment structure (Substance segment structure a))
(TU Covariant Covariant (Tagged segment) structure a)
-> Store
(Available segment structure (Substance segment structure a))
(structure a))
-> (structure a
-> TU Covariant Covariant (Tagged segment) structure a)
:*: (Store
(Available segment structure (Substance segment structure a))
(TU Covariant Covariant (Tagged segment) structure a)
-> Store
(Available segment structure (Substance segment structure a))
(structure a))
forall s a. s -> a -> s :*: a
:*: (forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
a.
(Lowerable cat t, Covariant cat cat u) =>
cat (t u a) (u a)
forall (t :: (* -> *) -> * -> *) (u :: * -> *) a.
(Lowerable (->) t, Covariant (->) (->) u) =>
t u a -> u a
lower @(->) (TU Covariant Covariant (Tagged segment) structure a
-> structure a)
-> Store
(Available segment structure (Substance segment structure a))
(TU Covariant Covariant (Tagged segment) structure a)
-> Store
(Available segment structure (Substance segment structure a))
(structure a)
forall (source :: * -> * -> *) (target :: * -> * -> *)
(t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|-) ((structure a
-> TU Covariant Covariant (Tagged segment) structure a)
:*: (Store
(Available segment structure (Substance segment structure a))
(TU Covariant Covariant (Tagged segment) structure a)
-> Store
(Available segment structure (Substance segment structure a))
(structure a)))
-> (TU Covariant Covariant (Tagged segment) structure a
-> Store
(Available segment structure (Substance segment structure a))
(TU Covariant Covariant (Tagged segment) structure a))
-> structure a
-> Store
(Available segment structure (Substance segment structure a))
(structure a)
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)
>-|-<-|-) (Primary
(P_Q_T
(->)
Store
(Available segment structure)
(TU Covariant Covariant (Tagged segment) structure a))
(Substance segment structure a)
-> Primary
(P_Q_T (->) Store (Available segment structure) (structure a))
(Substance segment structure a))
-> P_Q_T
(->)
Store
(Available segment structure)
(TU Covariant Covariant (Tagged segment) structure a)
(Substance segment structure a)
-> P_Q_T
(->)
Store
(Available segment structure)
(structure a)
(Substance segment structure a)
forall (m :: * -> * -> *) (t :: * -> *) (u :: * -> *) a b.
(Interpreted m t, Semigroupoid m, Interpreted m u) =>
m (Primary t a) (Primary u b) -> m (t a) (u b)
||= Substructure segment structure =>
((Tagged segment <:.> structure) #=@ Substance segment structure)
:= Available segment structure
forall k (segment :: k) (structure :: * -> *).
Substructure segment structure =>
((Tagged segment <:.> structure) #=@ Substance segment structure)
:= Available segment structure
substructure @segment @structure
only :: forall segment structure element . (Covariant (->) (->) structure, Substructured segment structure Identity Identity) => Convex Lens (structure element) element
only :: Convex Lens (structure element) element
only = Lens Identity (Identity element) element
Convex Lens (Identity element) element
inner Lens Identity (Identity element) element
-> P_Q_T (->) Store Identity (structure element) (Identity element)
-> P_Q_T (->) Store Identity (structure element) element
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. ((forall k (segment :: k) (structure :: * -> *).
(Substructure segment structure, Covariant (->) (->) structure) =>
(structure #=@ Substance segment structure)
:= Available segment structure
forall (structure :: * -> *).
(Substructure segment structure, Covariant (->) (->) structure) =>
(structure #=@ Substance segment structure)
:= Available segment structure
sub @segment) :: Convex Lens (structure element) (Identity element)) where
inner :: Convex Lens (Identity element) element
inner :: Convex Lens (Identity element) element
inner = (Identity element -> Store (Identity element) (Identity element))
-> Lens Identity (Identity element) element
forall (p :: * -> * -> *) (q :: * -> * -> *) (t :: * -> *) a b.
p a (q (t b) a) -> P_Q_T p q t a b
P_Q_T ((Identity element -> Store (Identity element) (Identity element))
-> Lens Identity (Identity element) element)
-> (Identity element
-> Store (Identity element) (Identity element))
-> Lens Identity (Identity element) element
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! \Identity element
x -> (((:*:) (Identity element) :. (->) (Identity element))
:= Identity element)
-> Store (Identity element) (Identity element)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Identity element) :. (->) (Identity element))
:= Identity element)
-> Store (Identity element) (Identity element))
-> (((:*:) (Identity element) :. (->) (Identity element))
:= Identity element)
-> Store (Identity element) (Identity element)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! Identity element
x Identity element
-> (Identity element -> Identity element)
-> ((:*:) (Identity element) :. (->) (Identity element))
:= Identity element
forall s a. s -> a -> s :*: a
:*: Identity element -> Identity element
forall (m :: * -> * -> *) a. Category m => m a a
identity