{-# OPTIONS_GHC -fno-warn-orphans #-} module Pandora.Paradigm.Inventory.State where import Pandora.Core.Functor (type (:.), type (:=)) import Pandora.Pattern.Category (identity, (.), ($)) import Pandora.Pattern.Functor.Covariant (Covariant ((<$>), (<$$>))) import Pandora.Pattern.Functor.Avoidable (Avoidable (empty)) import Pandora.Pattern.Functor.Pointable (Pointable (point)) import Pandora.Pattern.Functor.Applicative (Applicative ((<*>), (*>))) import Pandora.Pattern.Functor.Alternative (Alternative ((<+>))) import Pandora.Pattern.Functor.Traversable (Traversable ((->>))) import Pandora.Pattern.Functor.Bindable (Bindable ((>>=), (>=>))) import Pandora.Pattern.Functor.Monad (Monad) import Pandora.Pattern.Functor.Adjoint ((-|), (|-)) import Pandora.Pattern.Functor.Bivariant ((<->)) import Pandora.Pattern.Functor ((<*+>)) import Pandora.Paradigm.Controlflow.Effect.Adaptable (Adaptable (adapt)) import Pandora.Paradigm.Controlflow.Effect.Interpreted (Interpreted (Primary, run), Schematic) import Pandora.Paradigm.Controlflow.Effect.Transformer.Monadic (Monadic (wrap), (:>) (TM)) import Pandora.Paradigm.Schemes.TUT (TUT (TUT), type (<:<.>:>)) import Pandora.Paradigm.Primary.Functor (Product ((:*:)), type (:*:), delta) newtype State s a = State ((->) s :. (:*:) s := a) instance Covariant (State s) where a -> b f <$> :: (a -> b) -> State s a -> State s b <$> State s 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 a b -> m a b $ (a -> b) -> Product s a -> Product s b forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b (<$>) a -> b f (Product s a -> Product s b) -> (s -> Product s a) -> ((->) s :. (:*:) s) := b forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . State s a -> Primary (State s) a forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run State s a x instance Applicative (State s) where State s (a -> b) f <*> :: State s (a -> b) -> State s a -> State s b <*> State s 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 a b -> m a b $ (Product (s :*: a) (a -> b) -> ((a -> b) -> (s :*: a) -> s :*: b) -> s :*: b forall (t :: * -> *) (u :: * -> *) a b. Adjoint t u => t a -> (a -> u b) -> b |- (a -> b) -> (s :*: a) -> s :*: b forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b (<$>)) (Product (s :*: a) (a -> b) -> s :*: b) -> (s -> Product (s :*: a) (a -> b)) -> ((->) s :. (:*:) s) := b forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . (State s a -> Primary (State s) a forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run State s a x (((->) s :. (:*:) s) := a) -> ((a -> b) -> a -> b) -> Product s (a -> b) -> Product (s :*: a) (a -> b) forall (v :: * -> * -> *) a b c d. Bivariant v => (a -> b) -> (c -> d) -> v a c -> v b d <-> (a -> b) -> a -> b forall (m :: * -> * -> *) a. Category m => m a a identity) (Product s (a -> b) -> Product (s :*: a) (a -> b)) -> (s -> Product s (a -> b)) -> s -> Product (s :*: a) (a -> b) forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . State s (a -> b) -> Primary (State s) (a -> b) forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run State s (a -> b) f instance Pointable (State s) where point :: a |-> State s point = (((->) s :. (:*:) s) := a) -> State s a forall s a. (((->) s :. (:*:) s) := a) -> State s a State ((((->) s :. (:*:) s) := a) -> State s a) -> (a -> ((->) s :. (:*:) s) := a) -> a |-> State s forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . (a -> (Product s a -> Product s a) -> ((->) s :. (:*:) s) := a forall (t :: * -> *) (u :: * -> *) a b. Adjoint t u => a -> (t a -> b) -> u b -| Product s a -> Product s a forall (m :: * -> * -> *) a. Category m => m a a identity) instance Bindable (State s) where State s a x >>= :: State s a -> (a -> State s b) -> State s b >>= a -> State s b f = (((->) 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 a b -> m a b $ (Product s (State s b) -> (State s b -> ((->) s :. (:*:) s) := b) -> s :*: b forall (t :: * -> *) (u :: * -> *) a b. Adjoint t u => t a -> (a -> u b) -> b |- State s b -> ((->) s :. (:*:) s) := b forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run) (Product s (State s b) -> s :*: b) -> (s -> Product s (State s b)) -> ((->) s :. (:*:) s) := b forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . (a -> State s b) -> Product s a -> Product s (State s b) forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b (<$>) a -> State s b f (Product s a -> Product s (State s b)) -> (s -> Product s a) -> s -> Product s (State s b) forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . State s a -> Primary (State s) a forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run State s a x instance Monad (State s) where instance Interpreted (State s) where type Primary (State s) a = (->) s :. (:*:) s := a run :: State s a -> Primary (State s) a run ~(State ((->) s :. (:*:) s) := a x) = Primary (State s) a ((->) s :. (:*:) s) := a x type instance Schematic Monad (State s) = (->) s <:<.>:> (:*:) s instance Monadic (State s) where wrap :: State s ~> (State s :> u) wrap State s a x = (<:<.>:>) ((->) s) ((:*:) s) u a -> (:>) (State s) u a forall (t :: * -> *) (u :: * -> *) a. Schematic Monad t u a -> (:>) t u a TM ((<:<.>:>) ((->) s) ((:*:) s) u a -> (:>) (State s) u a) -> ((((->) s :. (u :. (:*:) s)) := a) -> (<:<.>:>) ((->) s) ((:*:) s) u a) -> (((->) s :. (u :. (:*:) s)) := a) -> (:>) (State s) u a forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . (((->) s :. (u :. (:*:) s)) := a) -> (<:<.>:>) ((->) s) ((:*:) s) u a forall k k k k k k (ct :: k) (ct' :: k) (cu :: k) (t :: k -> *) (t' :: k -> k) (u :: k -> k) (a :: k). ((t :. (u :. t')) := a) -> TUT ct ct' cu t t' u a TUT ((((->) s :. (u :. (:*:) s)) := a) -> (:>) (State s) u a) -> (((->) s :. (u :. (:*:) s)) := a) -> (:>) (State s) u a forall (m :: * -> * -> *) a b. Category m => m a b -> m a b $ (s :*: a) |-> u forall (t :: * -> *) a. Pointable t => a |-> t point ((s :*: a) |-> u) -> (s -> s :*: a) -> ((->) s :. (u :. (:*:) s)) := a forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b <$> State s a -> Primary (State s) a forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run State s a x type Stateful s = Adaptable (State s) instance Covariant u => Covariant ((->) s <:<.>:> (:*:) s := u) where a -> b f <$> :: (a -> b) -> (:=) ((->) s <:<.>:> (:*:) s) u a -> (:=) ((->) s <:<.>:> (:*:) s) u b <$> (:=) ((->) s <:<.>:> (:*:) s) u a x = (((->) s :. (u :. (:*:) s)) := b) -> (:=) ((->) s <:<.>:> (:*:) s) u b forall k k k k k k (ct :: k) (ct' :: k) (cu :: k) (t :: k -> *) (t' :: k -> k) (u :: k -> k) (a :: k). ((t :. (u :. t')) := a) -> TUT ct ct' cu t t' u a TUT ((((->) s :. (u :. (:*:) s)) := b) -> (:=) ((->) s <:<.>:> (:*:) s) u b) -> (((->) s :. (u :. (:*:) s)) := b) -> (:=) ((->) s <:<.>:> (:*:) s) u b forall (m :: * -> * -> *) a b. Category m => m a b -> m a b $ (a -> b) -> ((u :. (:*:) s) := a) -> (u :. (:*:) s) := b forall (t :: * -> *) (u :: * -> *) a b. (Covariant t, Covariant u) => (a -> b) -> ((t :. u) := a) -> (t :. u) := b (<$$>) a -> b f (((u :. (:*:) s) := a) -> (u :. (:*:) s) := b) -> (s -> (u :. (:*:) s) := a) -> ((->) s :. (u :. (:*:) s)) := b forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . (:=) ((->) s <:<.>:> (:*:) s) u a -> Primary (((->) s <:<.>:> (:*:) s) := u) a forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run (:=) ((->) s <:<.>:> (:*:) s) u a x instance Bindable u => Applicative ((->) s <:<.>:> (:*:) s := u) where (:=) ((->) s <:<.>:> (:*:) s) u (a -> b) f <*> :: (:=) ((->) s <:<.>:> (:*:) s) u (a -> b) -> (:=) ((->) s <:<.>:> (:*:) s) u a -> (:=) ((->) s <:<.>:> (:*:) s) u b <*> (:=) ((->) s <:<.>:> (:*:) s) u a x = (((->) s :. (u :. (:*:) s)) := b) -> (:=) ((->) s <:<.>:> (:*:) s) u b forall k k k k k k (ct :: k) (ct' :: k) (cu :: k) (t :: k -> *) (t' :: k -> k) (u :: k -> k) (a :: k). ((t :. (u :. t')) := a) -> TUT ct ct' cu t t' u a TUT ((((->) s :. (u :. (:*:) s)) := b) -> (:=) ((->) s <:<.>:> (:*:) s) u b) -> (((->) s :. (u :. (:*:) s)) := b) -> (:=) ((->) s <:<.>:> (:*:) s) u b forall (m :: * -> * -> *) a b. Category m => m a b -> m a b $ (:=) ((->) s <:<.>:> (:*:) s) u (a -> b) -> Primary (((->) s <:<.>:> (:*:) s) := u) (a -> b) forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run (:=) ((->) s <:<.>:> (:*:) s) u (a -> b) f (((->) s :. (u :. (:*:) s)) := (a -> b)) -> (Product s (a -> b) -> u (Product s b)) -> ((->) s :. (u :. (:*:) s)) := b forall (t :: * -> *) a b c. Bindable t => (a -> t b) -> (b -> t c) -> a -> t c >=> \ ~(s new :*: a -> b g) -> a -> b g (a -> b) -> ((u :. (:*:) s) := a) -> u (Product s b) forall (t :: * -> *) (u :: * -> *) a b. (Covariant t, Covariant u) => (a -> b) -> ((t :. u) := a) -> (t :. u) := b <$$> (:=) ((->) s <:<.>:> (:*:) s) u a -> ((->) s :. (u :. (:*:) s)) := a forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run (:=) ((->) s <:<.>:> (:*:) s) u a x s new instance Pointable u => Pointable ((->) s <:<.>:> (:*:) s := u) where point :: a |-> (((->) s <:<.>:> (:*:) s) := u) point = (((->) s :. (u :. (:*:) s)) := a) -> TUT Covariant Covariant Covariant ((->) s) ((:*:) s) u a forall k k k k k k (ct :: k) (ct' :: k) (cu :: k) (t :: k -> *) (t' :: k -> k) (u :: k -> k) (a :: k). ((t :. (u :. t')) := a) -> TUT ct ct' cu t t' u a TUT ((((->) s :. (u :. (:*:) s)) := a) -> TUT Covariant Covariant Covariant ((->) s) ((:*:) s) u a) -> (a -> ((->) s :. (u :. (:*:) s)) := a) -> a |-> (((->) s <:<.>:> (:*:) s) := u) forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . (a -> ((s :*: a) -> u (s :*: a)) -> ((->) s :. (u :. (:*:) s)) := a forall (t :: * -> *) (u :: * -> *) a b. Adjoint t u => a -> (t a -> b) -> u b -| (s :*: a) -> u (s :*: a) forall (t :: * -> *) a. Pointable t => a |-> t point) instance Bindable u => Bindable ((->) s <:<.>:> (:*:) s := u) where (:=) ((->) s <:<.>:> (:*:) s) u a x >>= :: (:=) ((->) s <:<.>:> (:*:) s) u a -> (a -> (:=) ((->) s <:<.>:> (:*:) s) u b) -> (:=) ((->) s <:<.>:> (:*:) s) u b >>= a -> (:=) ((->) s <:<.>:> (:*:) s) u b f = (((->) s :. (u :. (:*:) s)) := b) -> (:=) ((->) s <:<.>:> (:*:) s) u b forall k k k k k k (ct :: k) (ct' :: k) (cu :: k) (t :: k -> *) (t' :: k -> k) (u :: k -> k) (a :: k). ((t :. (u :. t')) := a) -> TUT ct ct' cu t t' u a TUT ((((->) s :. (u :. (:*:) s)) := b) -> (:=) ((->) s <:<.>:> (:*:) s) u b) -> (((->) s :. (u :. (:*:) s)) := b) -> (:=) ((->) s <:<.>:> (:*:) s) u b forall (m :: * -> * -> *) a b. Category m => m a b -> m a b $ (:=) ((->) s <:<.>:> (:*:) s) u a -> Primary (((->) s <:<.>:> (:*:) s) := u) a forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run (:=) ((->) s <:<.>:> (:*:) s) u a x (((->) s :. (u :. (:*:) s)) := a) -> (Product s a -> u (s :*: b)) -> ((->) s :. (u :. (:*:) s)) := b forall (t :: * -> *) a b c. Bindable t => (a -> t b) -> (b -> t c) -> a -> t c >=> \ ~(s new :*: a y) -> ((((->) s :. (u :. (:*:) s)) := b) -> ((->) s :. (u :. (:*:) s)) := b forall (m :: * -> * -> *) a b. Category m => m a b -> m a b $ s new) ((((->) s :. (u :. (:*:) s)) := b) -> u (s :*: b)) -> (a -> ((->) s :. (u :. (:*:) s)) := b) -> a -> u (s :*: b) forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . (:=) ((->) s <:<.>:> (:*:) s) u b -> ((->) s :. (u :. (:*:) s)) := b forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run ((:=) ((->) s <:<.>:> (:*:) s) u b -> ((->) s :. (u :. (:*:) s)) := b) -> (a -> (:=) ((->) s <:<.>:> (:*:) s) u b) -> a -> ((->) s :. (u :. (:*:) s)) := b forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . a -> (:=) ((->) s <:<.>:> (:*:) s) u b f (a -> u (s :*: b)) -> a -> u (s :*: b) forall (m :: * -> * -> *) a b. Category m => m a b -> m a b $ a y instance Monad u => Monad ((->) s <:<.>:> (:*:) s := u) where instance Alternative u => Alternative ((->) s <:<.>:> (:*:) s := u) where (:=) ((->) s <:<.>:> (:*:) s) u a x <+> :: (:=) ((->) s <:<.>:> (:*:) s) u a -> (:=) ((->) s <:<.>:> (:*:) s) u a -> (:=) ((->) s <:<.>:> (:*:) s) u a <+> (:=) ((->) s <:<.>:> (:*:) s) u a y = (((->) s :. (u :. (:*:) s)) := a) -> (:=) ((->) s <:<.>:> (:*:) s) u a forall k k k k k k (ct :: k) (ct' :: k) (cu :: k) (t :: k -> *) (t' :: k -> k) (u :: k -> k) (a :: k). ((t :. (u :. t')) := a) -> TUT ct ct' cu t t' u a TUT ((((->) s :. (u :. (:*:) s)) := a) -> (:=) ((->) s <:<.>:> (:*:) s) u a) -> (((->) s :. (u :. (:*:) s)) := a) -> (:=) ((->) s <:<.>:> (:*:) s) u a forall (m :: * -> * -> *) a b. Category m => m a b -> m a b $ (:=) ((->) s <:<.>:> (:*:) s) u a -> Primary (((->) s <:<.>:> (:*:) s) := u) a forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run (:=) ((->) s <:<.>:> (:*:) s) u a x (((->) s :. (u :. (:*:) s)) := a) -> (((->) s :. (u :. (:*:) s)) := a) -> ((->) s :. (u :. (:*:) s)) := a forall (t :: * -> *) (u :: * -> *) a. (Applicative t, Alternative u) => ((t :. u) := a) -> ((t :. u) := a) -> (t :. u) := a <*+> (:=) ((->) s <:<.>:> (:*:) s) u a -> Primary (((->) s <:<.>:> (:*:) s) := u) a forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run (:=) ((->) s <:<.>:> (:*:) s) u a y instance Avoidable u => Avoidable ((->) s <:<.>:> (:*:) s := u) where empty :: (:=) ((->) s <:<.>:> (:*:) s) u a empty = (((->) s :. (u :. (:*:) s)) := a) -> (:=) ((->) s <:<.>:> (:*:) s) u a forall k k k k k k (ct :: k) (ct' :: k) (cu :: k) (t :: k -> *) (t' :: k -> k) (u :: k -> k) (a :: k). ((t :. (u :. t')) := a) -> TUT ct ct' cu t t' u a TUT ((((->) s :. (u :. (:*:) s)) := a) -> (:=) ((->) s <:<.>:> (:*:) s) u a) -> (((->) s :. (u :. (:*:) s)) := a) -> (:=) ((->) s <:<.>:> (:*:) s) u a forall (m :: * -> * -> *) a b. Category m => m a b -> m a b $ \s _ -> u (s :*: a) forall (t :: * -> *) a. Avoidable t => t a empty current :: Stateful s t => t s current :: t s current = State s s -> t s forall k (t :: k -> *) (u :: k -> *). Adaptable t u => t ~> u adapt (State s s -> t s) -> State s s -> t s forall (m :: * -> * -> *) a b. Category m => m a b -> m a b $ (((->) s :. (:*:) s) := s) -> State s s forall s a. (((->) s :. (:*:) s) := a) -> State s a State ((->) s :. (:*:) s) := s forall a. a -> a :*: a delta modify :: Stateful s t => (s -> s) -> t () modify :: (s -> s) -> t () modify s -> s f = State s () -> t () forall k (t :: k -> *) (u :: k -> *). Adaptable t u => t ~> u adapt (State s () -> t ()) -> ((((->) s :. (:*:) s) := ()) -> State s ()) -> (((->) s :. (:*:) s) := ()) -> t () forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . (((->) s :. (:*:) s) := ()) -> State s () forall s a. (((->) s :. (:*:) s) := a) -> State s a State ((((->) s :. (:*:) s) := ()) -> t ()) -> (((->) s :. (:*:) s) := ()) -> t () forall (m :: * -> * -> *) a b. Category m => m a b -> m a b $ (s -> () -> Product s () forall s a. s -> a -> Product s a :*: ()) (((->) s :. (:*:) s) := ()) -> (s -> s) -> ((->) s :. (:*:) s) := () forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . s -> s f replace :: Stateful s t => s -> t () replace :: s -> t () replace s s = State s () -> t () forall k (t :: k -> *) (u :: k -> *). Adaptable t u => t ~> u adapt (State s () -> t ()) -> ((((->) s :. (:*:) s) := ()) -> State s ()) -> (((->) s :. (:*:) s) := ()) -> t () forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . (((->) s :. (:*:) s) := ()) -> State s () forall s a. (((->) s :. (:*:) s) := a) -> State s a State ((((->) s :. (:*:) s) := ()) -> t ()) -> (((->) s :. (:*:) s) := ()) -> t () forall (m :: * -> * -> *) a b. Category m => m a b -> m a b $ \s _ -> s s s -> () -> Product s () forall s a. s -> a -> Product s a :*: () type Memorable s t = (Pointable t, Applicative t, Stateful s t) fold :: (Traversable t, Memorable s u) => (a -> s -> s) -> t a -> u s fold :: (a -> s -> s) -> t a -> u s fold a -> s -> s op t a struct = t a struct t a -> (a -> u ()) -> (u :. t) := () forall (t :: * -> *) (u :: * -> *) a b. (Traversable t, Pointable u, Applicative u) => t a -> (a -> u b) -> (u :. t) := b ->> (s -> s) -> u () forall s (t :: * -> *). Stateful s t => (s -> s) -> t () modify ((s -> s) -> u ()) -> (a -> s -> s) -> a -> u () forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . a -> s -> s op ((u :. t) := ()) -> u s -> u s forall (t :: * -> *) a b. Applicative t => t a -> t b -> t b *> u s forall s (t :: * -> *). Stateful s t => t s current type Decisive t = (Pointable t, Avoidable t, Alternative t, Applicative t)