{-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE UndecidableInstances #-} module Pandora.Paradigm.Structure.Ability.Substructure where import Pandora.Pattern.Category ((.), ($)) import Pandora.Pattern.Functor.Covariant (Covariant ((<$>))) import Pandora.Pattern.Functor.Extractable (extract) import Pandora.Pattern.Functor.Pointable (point) import Pandora.Pattern.Functor.Divariant ((>->)) import Pandora.Pattern.Transformer.Liftable (lift) import Pandora.Paradigm.Controlflow.Effect.Interpreted (run, unite) import Pandora.Paradigm.Inventory.Optics (type (:~.), (|>)) import Pandora.Paradigm.Primary.Functor.Tagged (Tagged) import Pandora.Paradigm.Schemes.TU (type (<:.>)) class Substructure f t where type Substructural (f :: k) (t :: * -> *) :: * -> * substructure :: Tagged f <:.> t :~. Substructural f t sub :: Covariant t => t :~. Substructural f t sub t a x = t a <:= Tagged f forall (t :: * -> *) a. Extractable t => a <:= t extract (t a <:= Tagged f) -> (TU Covariant Covariant (Tagged f) t a -> Tagged f (t a)) -> TU Covariant Covariant (Tagged f) t a -> t a forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . TU Covariant Covariant (Tagged f) t a -> Tagged f (t a) forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run (TU Covariant Covariant (Tagged f) t a -> t a) -> Store (Substructural f t a) (TU Covariant Covariant (Tagged f) t a) -> Store (Substructural f t a) (t a) forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b <$> Lens (TU Covariant Covariant (Tagged f) t a) (Substructural f t a) forall k (f :: k) (t :: * -> *). Substructure f t => (Tagged f <:.> t) :~. Substructural f t substructure @f (t a -> TU Covariant Covariant (Tagged f) t a forall (t :: (* -> *) -> * -> *) (u :: * -> *). (Liftable t, Covariant u) => u ~> t u lift t a x) data Segment a = Tail a data (|>) (i :: * -> k) (j :: * -> k') a instance (Covariant t, Covariant (Substructural i t), Substructure i t, Substructure j (Substructural i t)) => Substructure (i |> j) t where type Substructural (i |> j) t = Substructural j (Substructural i t) substructure :: Lens ((<:.>) (Tagged (i |> j)) t a) (Substructural (i |> j) t a) substructure = t a <:= Tagged (i |> j) forall (t :: * -> *) a. Extractable t => a <:= t extract (t a <:= Tagged (i |> j)) -> ((<:.>) (Tagged (i |> j)) t a -> Tagged (i |> j) (t a)) -> (<:.>) (Tagged (i |> j)) t a -> t a forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . (<:.>) (Tagged (i |> j)) t a -> Tagged (i |> j) (t a) forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run ((<:.>) (Tagged (i |> j)) t a -> t a) -> (Store (Substructural j (Substructural i t) a) (t a) -> Store (Substructural j (Substructural i t) a) ((<:.>) (Tagged (i |> j)) t a)) -> (t a -> Store (Substructural j (Substructural i t) a) (t a)) -> (<:.>) (Tagged (i |> j)) t a -> Store (Substructural j (Substructural i t) a) ((<:.>) (Tagged (i |> j)) t a) forall (v :: * -> * -> *) a b c d. Divariant v => (a -> b) -> (c -> d) -> v b c -> v a d >-> (Tagged (i |> j) (t a) -> (<:.>) (Tagged (i |> j)) t a forall (t :: * -> *) a. Interpreted t => Primary t a -> t a unite (Tagged (i |> j) (t a) -> (<:.>) (Tagged (i |> j)) t a) -> (t a -> Tagged (i |> j) (t a)) -> t a -> (<:.>) (Tagged (i |> j)) t a forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . t a -> Tagged (i |> j) (t a) forall (t :: * -> *) a. Pointable t => a :=> t point (t a -> (<:.>) (Tagged (i |> j)) t a) -> Store (Substructural j (Substructural i t) a) (t a) -> Store (Substructural j (Substructural i t) a) ((<:.>) (Tagged (i |> j)) t a) forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b <$>) ((t a -> Store (Substructural j (Substructural i t) a) (t a)) -> (<:.>) (Tagged (i |> j)) t a -> Store (Substructural j (Substructural i t) a) ((<:.>) (Tagged (i |> j)) t a)) -> (t a -> Store (Substructural j (Substructural i t) a) (t a)) -> (<:.>) (Tagged (i |> j)) t a -> Store (Substructural j (Substructural i t) a) ((<:.>) (Tagged (i |> j)) t a) forall (m :: * -> * -> *). Category m => m ~~> m $ forall k (f :: k) (t :: * -> *). (Substructure f t, Covariant t) => t :~. Substructural f t forall (t :: * -> *). (Substructure i t, Covariant t) => t :~. Substructural i t sub @i (t a -> Store (Substructural i t a) (t a)) -> Lens (Substructural i t a) (Substructural j (Substructural i t) a) -> t a -> Store (Substructural j (Substructural i t) a) (t a) forall src tgt new. Lens src tgt -> Lens tgt new -> Lens src new |> forall k (f :: k) (t :: * -> *). (Substructure f t, Covariant t) => t :~. Substructural f t forall (t :: * -> *). (Substructure j t, Covariant t) => t :~. Substructural j t sub @j type Substructured i source target = (Substructure i source, Substructural i source ~ target)