{-# LANGUAGE AllowAmbiguousTypes #-} {-# OPTIONS_GHC -fno-warn-orphans #-} module Pandora.Paradigm.Inventory (module Exports, Zoomable (zoom), overlook, (=<>), (~<>)) where import Pandora.Paradigm.Inventory.Ability as Exports import Pandora.Paradigm.Inventory.Some as Exports import Pandora.Core.Functor (type (~>)) 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), Simplification) import Pandora.Paradigm.Primary.Functor.Maybe (Maybe) import Pandora.Paradigm.Primary.Algebraic.Product ((:*:) ((:*:))) import Pandora.Paradigm.Primary.Algebraic.Exponential ((%), type (<--)) import Pandora.Paradigm.Primary.Algebraic (Pointable, extract) import Pandora.Paradigm.Controlflow.Effect.Interpreted (run, (!)) 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 :: * -> * -> *) (t :: * -> *) a. Interpreted m t => m (t a) (Primary t a) ! \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 :: * -> * -> *) (t :: * -> *) a. Interpreted m t => m (t a) (Primary t a) ! 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 :: * -> * -> *) (t :: * -> *) a. Interpreted m t => m (t a) (Primary t a) ! 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 :: * -> * -> *) (t :: * -> *) a. Interpreted m t => m (t a) (Primary t a) ! 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 :: * -> * -> *) (t :: * -> *) a. Interpreted m t => m (t a) (Primary t a) ! 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 class Zoomable (tool :: * -> * -> *) (available :: * -> *) where zoom :: forall bg ls t . Adaptable t (->) (tool bg) => Lens available bg ls -> tool (Simplification available ls) ~> t instance Zoomable State Exactly where zoom :: forall bg ls t result . Stateful bg t => Convex Lens bg ls -> State ls result -> t result zoom :: Convex Lens bg ls -> State ls result -> t result zoom Convex Lens bg ls lens State ls result less = State bg result -> t result 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 (State bg result -> t result) -> ((((->) bg :. (:*:) bg) := result) -> State bg result) -> (((->) bg :. (:*:) bg) := result) -> t result forall (m :: * -> * -> *) b c a. Semigroupoid m => m b c -> m a b -> m a c . (((->) bg :. (:*:) bg) := result) -> State bg result forall s a. (((->) s :. (:*:) s) := a) -> State s a State ((((->) bg :. (:*:) bg) := result) -> t result) -> (((->) bg :. (:*:) bg) := result) -> t result forall (m :: * -> * -> *) (t :: * -> *) a. Interpreted m t => m (t a) (Primary t a) ! \bg source -> (Exactly ls -> bg) -> Exactly ls -> bg :*: result restruct ((Exactly ls -> bg) -> Exactly ls -> bg :*: result) -> (Exactly ls :*: (Exactly 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 (Exactly ls) bg -> Exactly ls :*: (Exactly ls -> bg) forall (m :: * -> * -> *) (t :: * -> *) a. Interpreted m t => m (t a) (Primary t a) run (Lens Exactly bg ls Convex Lens bg ls lens Lens Exactly bg ls -> bg -> Store (Exactly ls) bg forall (m :: * -> * -> *) (t :: * -> *) a. Interpreted m t => m (t a) (Primary t a) ! bg source) where restruct :: (Exactly ls -> bg) -> Exactly ls -> bg :*: result restruct :: (Exactly ls -> bg) -> Exactly ls -> bg :*: result restruct Exactly ls -> bg to (Exactly ls target) = Flip (:*:) result bg -> bg :*: result 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) # Exactly ls -> bg to (Exactly ls -> bg) -> (ls -> Exactly ls) -> ls -> bg forall (m :: * -> * -> *) b c a. Semigroupoid m => m b c -> m a b -> m a c . ls -> Exactly ls forall a. a -> Exactly a Exactly (ls -> bg) -> Flip (:*:) result ls -> Flip (:*:) result bg forall (source :: * -> * -> *) (target :: * -> * -> *) (t :: * -> *) a b. Covariant source target t => source a b -> target (t a) (t b) <-|- (ls :*: result) -> Flip (:*:) result ls forall (v :: * -> * -> *) a e. v e a -> Flip v a e Flip (State ls result less State ls result -> ((->) ls :. (:*:) ls) := result forall (m :: * -> * -> *) (t :: * -> *) a. Interpreted m t => m (t a) (Primary t a) ! ls target) instance Zoomable State Maybe where zoom :: forall bg ls t result . Stateful bg t => Obscure Lens bg ls -> State (Maybe ls) result -> t result zoom :: Obscure Lens bg ls -> State (Maybe ls) result -> t result zoom Obscure Lens bg ls lens State (Maybe ls) result less = State bg result -> t result 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 (State bg result -> t result) -> ((((->) bg :. (:*:) bg) := result) -> State bg result) -> (((->) bg :. (:*:) bg) := result) -> t result forall (m :: * -> * -> *) b c a. Semigroupoid m => m b c -> m a b -> m a c . (((->) bg :. (:*:) bg) := result) -> State bg result forall s a. (((->) s :. (:*:) s) := a) -> State s a State ((((->) bg :. (:*:) bg) := result) -> t result) -> (((->) bg :. (:*:) bg) := result) -> t result forall (m :: * -> * -> *) (t :: * -> *) a. Interpreted m t => m (t a) (Primary t a) ! \bg source -> (Maybe ls -> bg) -> Maybe ls -> bg :*: result restruct ((Maybe ls -> bg) -> Maybe ls -> bg :*: result) -> (Maybe ls :*: (Maybe 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 (Maybe ls) bg -> Maybe ls :*: (Maybe ls -> bg) forall (m :: * -> * -> *) (t :: * -> *) a. Interpreted m t => m (t a) (Primary t a) run (Lens Maybe bg ls Obscure Lens bg ls lens Lens Maybe bg ls -> bg -> Store (Maybe ls) bg forall (m :: * -> * -> *) (t :: * -> *) a. Interpreted m t => m (t a) (Primary t a) ! bg source) where restruct :: (Maybe ls -> bg) -> Maybe ls -> bg :*: result restruct :: (Maybe ls -> bg) -> Maybe ls -> bg :*: result restruct Maybe ls -> bg to Maybe ls target = Flip (:*:) result bg -> bg :*: result forall (m :: * -> * -> *) (t :: * -> *) a. Interpreted m t => m (t a) (Primary t a) run (Maybe ls -> bg to (Maybe ls -> bg) -> Flip (:*:) result (Maybe ls) -> Flip (:*:) result bg forall (source :: * -> * -> *) (target :: * -> * -> *) (t :: * -> *) a b. Covariant source target t => source a b -> target (t a) (t b) <-|-- (Maybe ls :*: result) -> Flip (:*:) result (Maybe ls) forall (v :: * -> * -> *) a e. v e a -> Flip v a e Flip ((Maybe ls :*: result) -> Flip (:*:) result (Maybe ls)) -> (Maybe ls :*: result) -> Flip (:*:) result (Maybe ls) forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b) <-- State (Maybe ls) result -> ((->) (Maybe ls) :. (:*:) (Maybe ls)) := result forall (m :: * -> * -> *) (t :: * -> *) a. Interpreted m t => m (t a) (Primary t a) run State (Maybe ls) result less Maybe 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 :: * -> * -> *) (t :: * -> *) a. Interpreted m t => m (t a) (Primary t a) ! \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 :: * -> * -> *) (t :: * -> *) a. Interpreted m t => m (t a) (Primary t a) ! 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 :: * -> * -> *) (t :: * -> *) a. Interpreted m t => m (t a) (Primary t a) ! (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)