{-# LANGUAGE AllowAmbiguousTypes #-} {-# OPTIONS_GHC -fno-warn-orphans #-} module Pandora.Paradigm.Inventory (module Exports, zoom, overlook, (=<>), (~<>)) where import Pandora.Paradigm.Inventory.Ability as Exports import Pandora.Paradigm.Inventory.Some as Exports import Pandora.Core.Functor (type (~>)) import Pandora.Core.Interpreted (run, (<~)) import Pandora.Pattern.Semigroupoid ((.)) import Pandora.Pattern.Category ((<--), (<---), (<----)) import Pandora.Pattern.Kernel (constant) import Pandora.Pattern.Morphism.Flip (Flip (Flip)) import Pandora.Pattern.Functor.Covariant (Covariant ((<-|-), (<-|--))) import Pandora.Pattern.Functor.Semimonoidal (Semimonoidal (mult)) import Pandora.Pattern.Functor.Adjoint (Adjoint ((-|), (--|), (|-), (|--))) import Pandora.Paradigm.Primary.Functor.Exactly (Exactly (Exactly)) import Pandora.Paradigm.Primary.Functor.Maybe (Maybe) import Pandora.Paradigm.Algebraic.Product ((:*:) ((:*:))) import Pandora.Paradigm.Algebraic.Exponential ((%), type (<--)) import Pandora.Paradigm.Algebraic (Pointable, extract) import Pandora.Paradigm.Primary (Simplification) import Pandora.Paradigm.Controlflow.Effect.Adaptable (Adaptable (adapt)) instance Adjoint (->) (->) (Store s) (State s) where (-|) :: (Store s a -> b) -> a -> State s b Store s a -> b f -| :: (Store s a -> b) -> a -> State s b -| a x = (((->) s :. (:*:) s) >>> b) -> State s b forall s a. (((->) s :. (:*:) s) >>> a) -> State s a State ((((->) s :. (:*:) s) >>> b) -> State s b) -> (((->) s :. (:*:) s) >>> b) -> State s b forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b) <-- \s s -> s -> b -> s :*: b forall s a. s -> a -> s :*: a (:*:) s s (b -> s :*: b) -> ((s :*: (s -> a)) -> b) -> (s :*: (s -> a)) -> s :*: b forall (m :: * -> * -> *) b c a. Semigroupoid m => m b c -> m a b -> m a c . Store s a -> b f (Store s a -> b) -> ((s :*: (s -> a)) -> Store s a) -> (s :*: (s -> a)) -> b forall (m :: * -> * -> *) b c a. Semigroupoid m => m b c -> m a b -> m a c . (s :*: (s -> a)) -> Store s a forall s a. (((:*:) s :. (->) s) >>> a) -> Store s a Store ((s :*: (s -> a)) -> s :*: b) -> (s :*: (s -> a)) -> s :*: b forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b) <--- s s s -> (s -> a) -> s :*: (s -> a) forall s a. s -> a -> s :*: a :*: a -> s -> a forall (m :: * -> * -> *) a i. Kernel m => m a (m i a) constant a x (|-) :: (a -> State s b) -> Store s a -> b a -> State s b g |- :: (a -> State s b) -> Store s a -> b |- Store (s s :*: s -> a f) = (s :*: b) -> b forall (t :: * -> *) a. Extractable t => t a -> a extract ((s :*: b) -> b) -> (a -> s :*: b) -> a -> b forall (m :: * -> * -> *) b c a. Semigroupoid m => m b c -> m a b -> m a c . (State s b -> ((->) s :. (:*:) s) >>> b forall (m :: * -> * -> *) (t :: * -> *) a. Interpreted m t => (m < t a) < Primary t a run (State s b -> ((->) s :. (:*:) s) >>> b) -> s -> State s b -> s :*: b forall a b c. (a -> b -> c) -> b -> a -> c % s s) (State s b -> s :*: b) -> (a -> State s b) -> a -> s :*: b forall (m :: * -> * -> *) b c a. Semigroupoid m => m b c -> m a b -> m a c . a -> State s b g (a -> b) -> a -> b forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b) <-- s -> a f s s instance Adjoint (->) (->) (Accumulator e) (Imprint e) where Accumulator e a -> b f -| :: (Accumulator e a -> b) -> a -> Imprint e b -| a x = (e -> b) -> Imprint e b forall e a. (e -> a) -> Imprint e a Imprint ((e -> b) -> Imprint e b) -> (e -> b) -> Imprint e b forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b) <--- Accumulator e a -> b f (Accumulator e a -> b) -> ((e :*: a) -> Accumulator e a) -> (e :*: a) -> b forall (m :: * -> * -> *) b c a. Semigroupoid m => m b c -> m a b -> m a c . (e :*: a) -> Accumulator e a forall e a. (e :*: a) -> Accumulator e a Accumulator ((e :*: a) -> b) -> a -> e -> b forall (source :: * -> * -> *) (target :: * -> * -> *) (t :: * -> *) (u :: * -> *) a b. Adjoint source target t u => source (t a) b -> target a (u b) --| a x a -> Imprint e b g |- :: (a -> Imprint e b) -> Accumulator e a -> b |- Accumulator e a x = Imprint e b -> e -> b forall (m :: * -> * -> *) (t :: * -> *) a. Interpreted m t => (m < t a) < Primary t a run (Imprint e b -> e -> b) -> (a -> Imprint e b) -> a -> e -> b forall (m :: * -> * -> *) b c a. Semigroupoid m => m b c -> m a b -> m a c . a -> Imprint e b g (a -> e -> b) -> (e :*: a) -> b forall (source :: * -> * -> *) (target :: * -> * -> *) (t :: * -> *) (u :: * -> *) a b. Adjoint source target t u => target a (u b) -> source (t a) b |-- Accumulator e a -> e :*: a forall (m :: * -> * -> *) (t :: * -> *) a. Interpreted m t => (m < t a) < Primary t a run Accumulator e a x instance Adjoint (->) (->) (Equipment e) (Provision e) where Equipment e a -> b f -| :: (Equipment e a -> b) -> a -> Provision e b -| a x = (e -> b) -> Provision e b forall e a. (e -> a) -> Provision e a Provision ((e -> b) -> Provision e b) -> (e -> b) -> Provision e b forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b) <--- Equipment e a -> b f (Equipment e a -> b) -> ((e :*: a) -> Equipment e a) -> (e :*: a) -> b forall (m :: * -> * -> *) b c a. Semigroupoid m => m b c -> m a b -> m a c . (e :*: a) -> Equipment e a forall e a. (e :*: a) -> Equipment e a Equipment ((e :*: a) -> b) -> a -> e -> b forall (source :: * -> * -> *) (target :: * -> * -> *) (t :: * -> *) (u :: * -> *) a b. Adjoint source target t u => source (t a) b -> target a (u b) --| a x a -> Provision e b g |- :: (a -> Provision e b) -> Equipment e a -> b |- Equipment e a x = Provision e b -> e -> b forall (m :: * -> * -> *) (t :: * -> *) a. Interpreted m t => (m < t a) < Primary t a run (Provision e b -> e -> b) -> (a -> Provision e b) -> a -> e -> b forall (m :: * -> * -> *) b c a. Semigroupoid m => m b c -> m a b -> m a c . a -> Provision e b g (a -> e -> b) -> (e :*: a) -> b forall (source :: * -> * -> *) (target :: * -> * -> *) (t :: * -> *) (u :: * -> *) a b. Adjoint source target t u => target a (u b) -> source (t a) b |-- Equipment e a -> e :*: a forall (m :: * -> * -> *) (t :: * -> *) a. Interpreted m t => (m < t a) < Primary t a run Equipment e a x zoom :: forall bg ls u result . Lens u bg ls -> State (u ls) result -> State bg result zoom :: Lens u bg ls -> State (u ls) result -> State bg result zoom Lens u bg ls lens State (u ls) result less = (((->) bg :. (:*:) bg) >>> result) -> State bg result forall s a. (((->) s :. (:*:) s) >>> a) -> State s a State ((((->) bg :. (:*:) bg) >>> result) -> State bg result) -> (((->) bg :. (:*:) bg) >>> result) -> State bg result forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b) <-- \bg source -> (u ls -> bg) -> u ls -> bg :*: result restruct ((u ls -> bg) -> u ls -> bg :*: result) -> (u ls :*: (u ls -> bg)) -> bg :*: result forall (source :: * -> * -> *) (target :: * -> * -> *) (t :: * -> *) (u :: * -> *) a b. Adjoint source target t u => target a (u b) -> source (t a) b |- Store (u ls) bg -> u ls :*: (u ls -> bg) forall (m :: * -> * -> *) (t :: * -> *) a. Interpreted m t => (m < t a) < Primary t a run (Lens u bg ls lens Lens u bg ls -> bg -> Store (u ls) bg forall (m :: * -> * -> *) (t :: * -> *) a. Interpreted m t => (m < t a) < Primary t a <~ bg source) where restruct :: (u ls -> bg) -> u ls -> bg :*: result restruct :: (u ls -> bg) -> u ls -> bg :*: result restruct u ls -> bg to u ls target = forall (t :: * -> *) a. Interpreted (->) t => ((->) < t a) < Primary t a forall (m :: * -> * -> *) (t :: * -> *) a. Interpreted m t => (m < t a) < Primary t a run @(->) (Flip (:*:) result bg -> bg :*: result) -> Flip (:*:) result bg -> bg :*: result forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b) <---- u ls -> bg to (u ls -> bg) -> Flip (:*:) result (u ls) -> Flip (:*:) result bg forall (source :: * -> * -> *) (target :: * -> * -> *) (t :: * -> *) a b. Covariant source target t => source a b -> target (t a) (t b) <-|- (u ls :*: result) -> Flip (:*:) result (u ls) forall (v :: * -> * -> *) a e. v e a -> Flip v a e Flip (State (u ls) result less State (u ls) result -> ((->) (u ls) :. (:*:) (u ls)) >>> result forall (m :: * -> * -> *) (t :: * -> *) a. Interpreted m t => (m < t a) < Primary t a <~ u ls target) overlook :: (Covariant (->) (->) t, Semimonoidal (<--) (:*:) (:*:) t) => State s result -> State (t s) (t result) overlook :: State s result -> State (t s) (t result) overlook (State ((->) s :. (:*:) s) >>> result state) = (((->) (t s) :. (:*:) (t s)) >>> t result) -> State (t s) (t result) forall s a. (((->) s :. (:*:) s) >>> a) -> State s a State ((((->) (t s) :. (:*:) (t s)) >>> t result) -> State (t s) (t result)) -> (((->) (t s) :. (:*:) (t s)) >>> t result) -> State (t s) (t result) forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b) <-- \t s ts -> forall k (p :: * -> * -> *) (source :: * -> * -> *) (target :: k -> k -> k) (t :: k -> *) (a :: k) (b :: k). Semimonoidal p source target t => p (source (t a) (t b)) (t (target a b)) forall (t :: * -> *) a b. Semimonoidal (<--) (:*:) (:*:) t => (t a :*: t b) <-- t (a :*: b) mult @(<--) @(:*:) @(:*:) ((t s :*: t result) <-- t (s :*: result)) -> t (s :*: result) -> t s :*: t result forall (m :: * -> * -> *) (t :: * -> *) a. Interpreted m t => (m < t a) < Primary t a <~ (((->) s :. (:*:) s) >>> result state (((->) s :. (:*:) s) >>> result) -> t s -> t (s :*: result) forall (source :: * -> * -> *) (target :: * -> * -> *) (t :: * -> *) a b. Covariant source target t => source a b -> target (t a) (t b) <-|- t s ts) (=<>) :: (Pointable available, Stateful src t) => Lens available src tgt -> tgt -> t src Lens available src tgt lens =<> :: Lens available src tgt -> tgt -> t src =<> tgt new = ((->) < State src src) < t src forall k k k (u :: k -> k) (m :: k -> k -> *) (t :: k -> k) (a :: k). Adaptable u m t => (m < t a) < u a adapt (forall e r. Modifiable State => Modification State e r forall k (i :: k) e r. Modifiable i => Modification i e r modify @State ((src -> src) -> State src src) -> (src -> src) -> State src src forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b) <-- tgt -> Lens available src tgt -> src -> src forall k (i :: k) e r. Settable i => Setting i e r set @(Lens _) tgt new Lens available src tgt lens) (~<>) :: (Pointable available, Covariant (->) (->) available, Gettable (Lens available), Stateful src t) => Lens available src tgt -> (tgt -> tgt) -> t src Lens available src tgt lens ~<> :: Lens available src tgt -> (tgt -> tgt) -> t src ~<> tgt -> tgt f = ((->) < State src src) < t src forall k k k (u :: k -> k) (m :: k -> k -> *) (t :: k -> k) (a :: k). Adaptable u m t => (m < t a) < u a adapt (forall e r. Modifiable State => Modification State e r forall k (i :: k) e r. Modifiable i => Modification i e r modify @State ((src -> src) -> State src src) -> (src -> src) -> State src src forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b) <-- (tgt -> tgt) -> Lens available src tgt -> src -> src forall k (i :: k) e r. Modifiable i => Modification i e r modify @(Lens _) tgt -> tgt f Lens available src tgt lens)