{-# LANGUAGE UndecidableInstances #-} module Pandora.Paradigm.Structure.Modification.Prefixed where import Pandora.Core.Functor (type (:=)) import Pandora.Pattern.Category ((.), ($)) import Pandora.Pattern.Functor.Covariant (Covariant ((<$>))) import Pandora.Pattern.Functor.Contravariant ((>$<)) import Pandora.Pattern.Functor.Pointable (Pointable (point)) import Pandora.Pattern.Functor.Extractable (Extractable (extract)) import Pandora.Pattern.Functor.Traversable (Traversable ((->>))) import Pandora.Pattern.Functor.Bindable (Bindable ((>>=))) import Pandora.Pattern.Transformer.Liftable (lift) import Pandora.Pattern.Object.Monoid (Monoid (zero)) import Pandora.Pattern.Object.Setoid (Setoid) import Pandora.Paradigm.Primary.Functor.Maybe (Maybe (Just)) import Pandora.Paradigm.Primary.Functor.Product (Product ((:*:)), attached) import Pandora.Paradigm.Primary.Functor.Predicate (equate) import Pandora.Paradigm.Controlflow.Effect.Interpreted (Interpreted (Primary, run, unite)) import Pandora.Paradigm.Schemes.TU (TU (TU), type (<:.>)) import Pandora.Paradigm.Structure.Ability.Monotonic (Monotonic, find) import Pandora.Paradigm.Structure.Interface.Dictionary (Dictionary ((?=))) type Keyed k = Product k <:.> Maybe newtype Prefixed t k a = Prefixed (t <:.> Keyed k := a) instance Interpreted (Prefixed t k) where type Primary (Prefixed t k) a = t <:.> Keyed k := a run :: Prefixed t k a -> Primary (Prefixed t k) a run ~(Prefixed (t <:.> Keyed k) := a x) = Primary (Prefixed t k) a (t <:.> Keyed k) := a x unite :: Primary (Prefixed t k) a -> Prefixed t k a unite = Primary (Prefixed t k) a -> Prefixed t k a forall (t :: * -> *) k a. ((t <:.> Keyed k) := a) -> Prefixed t k a Prefixed instance Covariant t => Covariant (Prefixed t k) where a -> b f <$> :: (a -> b) -> Prefixed t k a -> Prefixed t k b <$> Prefixed (t <:.> Keyed k) := a x = ((t <:.> Keyed k) := b) -> Prefixed t k b forall (t :: * -> *) k a. ((t <:.> Keyed k) := a) -> Prefixed t k a Prefixed (((t <:.> Keyed k) := b) -> Prefixed t k b) -> ((t <:.> Keyed k) := b) -> Prefixed t k b forall (m :: * -> * -> *). Category m => m ~~> m $ a -> b f (a -> b) -> ((t <:.> Keyed k) := a) -> (t <:.> Keyed k) := b forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b <$> (t <:.> Keyed k) := a x instance Traversable t => Traversable (Prefixed t k) where Prefixed (t <:.> Keyed k) := a x ->> :: Prefixed t k a -> (a -> u b) -> (u :. Prefixed t k) := b ->> a -> u b f = ((t <:.> Keyed k) := b) -> Prefixed t k b forall (t :: * -> *) k a. ((t <:.> Keyed k) := a) -> Prefixed t k a Prefixed (((t <:.> Keyed k) := b) -> Prefixed t k b) -> u ((t <:.> Keyed k) := b) -> (u :. Prefixed t k) := b forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b <$> (t <:.> Keyed k) := a x ((t <:.> Keyed k) := a) -> (a -> u b) -> u ((t <:.> Keyed k) := b) forall (t :: * -> *) (u :: * -> *) a b. (Traversable t, Pointable u, Applicative u) => t a -> (a -> u b) -> (u :. t) := b ->> a -> u b f instance (Monoid k, Pointable t) => Pointable (Prefixed t k) where point :: a :=> Prefixed t k point = ((t <:.> Keyed k) := a) -> Prefixed t k a forall (t :: * -> *) k a. ((t <:.> Keyed k) := a) -> Prefixed t k a Prefixed (((t <:.> Keyed k) := a) -> Prefixed t k a) -> (a -> (t <:.> Keyed k) := a) -> a :=> Prefixed t k forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . Keyed k a -> (t <:.> Keyed k) := a forall (t :: (* -> *) -> * -> *) (u :: * -> *). (Liftable t, Covariant u) => u ~> t u lift (Keyed k a -> (t <:.> Keyed k) := a) -> (a -> Keyed k a) -> a -> (t <:.> Keyed k) := a forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . ((Product k :. Maybe) := a) -> Keyed k a forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k) (a :: k). ((t :. u) := a) -> TU ct cu t u a TU (((Product k :. Maybe) := a) -> Keyed k a) -> (a -> (Product k :. Maybe) := a) -> a -> Keyed k a forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . k -> Maybe a -> (Product k :. Maybe) := a forall s a. s -> a -> Product s a (:*:) k forall a. Monoid a => a zero (Maybe a -> (Product k :. Maybe) := a) -> (a -> Maybe a) -> a -> (Product k :. Maybe) := a forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . a -> Maybe a forall a. a -> Maybe a Just instance (Monotonic (Keyed k a) (t (Keyed k a)), Setoid k) => Dictionary a k (Prefixed t k) where k k ?= :: k -> Prefixed t k a -> Maybe a ?= Prefixed (t <:.> Keyed k) := a x = Predicate (Keyed k a) -> t (Keyed k a) -> Maybe (Keyed k a) forall a e (t :: * -> *). (Monotonic a e, Pointable t, Avoidable t) => Predicate a -> e -> t a find @(Keyed k a) ((k :*: Maybe a) -> k forall a b. (a :*: b) -> a attached ((k :*: Maybe a) -> k) -> (Keyed k a -> k :*: Maybe a) -> Keyed k a -> k forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . Keyed k a -> k :*: Maybe a forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run (Keyed k a -> k) -> Predicate k -> Predicate (Keyed k a) forall (t :: * -> *) a b. Contravariant t => (a -> b) -> t b -> t a >$< k :=> Predicate forall a. Setoid a => a :=> Predicate equate k k) (((t <:.> Keyed k) := a) -> Primary (t <:.> Keyed k) a forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run (t <:.> Keyed k) := a x) Maybe (Keyed k a) -> (Keyed k a -> Maybe a) -> Maybe a forall (t :: * -> *) a b. Bindable t => t a -> (a -> t b) -> t b >>= Maybe a <:= Product k forall (t :: * -> *) a. Extractable t => a <:= t extract (Maybe a <:= Product k) -> (Keyed k a -> k :*: Maybe a) -> Keyed k a -> Maybe a forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . Keyed k a -> k :*: Maybe a forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run