{-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE UndecidableInstances #-} module Pandora.Paradigm.Structure.Ability.Substructure where import Pandora.Core.Functor (type (:=)) import Pandora.Pattern.Functor.Covariant (Covariant ((<$>))) import Pandora.Pattern.Functor.Divariant ((>->)) import Pandora.Pattern.Transformer.Liftable (lift) import Pandora.Pattern.Transformer.Lowerable (lower) import Pandora.Paradigm.Controlflow.Effect.Interpreted ((||=)) import Pandora.Paradigm.Inventory.Optics (type (#=@)) import Pandora.Paradigm.Primary.Functor.Tagged (Tagged) import Pandora.Paradigm.Schemes.TU (type (<:.>)) 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 = forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *) a. (Liftable cat t, Covariant cat cat u) => cat (u a) (t u a) forall (t :: (* -> *) -> * -> *) (u :: * -> *) a. (Liftable (->) t, Covariant (->) (->) u) => 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)) -> (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 (left :: * -> * -> *) (right :: * -> * -> *) (target :: * -> * -> *) (v :: * -> * -> *) a b c d. Divariant left right target v => left a b -> right c d -> target (v b c) (v a d) >-> (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) <$>) (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