{-# 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 = structure a -> TU Covariant Covariant (Tagged segment) structure a forall (t :: (* -> *) -> * -> *) (u :: * -> *). (Liftable t, Covariant u) => u ~> t u 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 (v :: * -> * -> *) a b c d. Divariant v => (a -> b) -> (c -> d) -> v b c -> v a d >-> (TU Covariant Covariant (Tagged segment) structure a -> structure a forall (t :: (* -> *) -> * -> *) (u :: * -> *). (Lowerable t, Covariant u) => t u ~> u 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 (t :: * -> *) a b. Covariant t => (a -> b) -> 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 (t :: * -> *) (u :: * -> *) a b. (Interpreted t, Interpreted u) => (Primary t a -> Primary u b) -> 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