{-# LANGUAGE QuantifiedConstraints #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE BlockArguments #-} {-# LANGUAGE DerivingVia #-} {-# LANGUAGE DeriveFunctor #-} {-# LANGUAGE StandaloneDeriving #-} module FMonad.State.Simple.Outer (StateT(..), flift, fromAdjointT, toAdjointT, State, state, runState, ) where import Control.Monad.Trans.Identity ( IdentityT(..) ) import Control.Comonad.Trans.Env import Control.Monad.Trans.Reader import Data.Tuple (swap) import Data.Coerce (coerce) import FMonad import FMonad.Adjoint newtype StateT s0 mm x a = StateT { forall s0 (mm :: (* -> *) -> * -> *) (x :: * -> *) a. StateT s0 mm x a -> s0 -> mm (EnvT s0 x) a runStateT :: s0 -> mm (EnvT s0 x) a } deriving ((forall (g :: * -> *). Functor g => Functor (StateT s0 mm g)) => (forall (g :: * -> *) (h :: * -> *) x. (Functor g, Functor h) => (g ~> h) -> StateT s0 mm g x -> StateT s0 mm h x) -> FFunctor (StateT s0 mm) forall s0 (mm :: (* -> *) -> * -> *) (g :: * -> *). (FFunctor mm, Functor g) => Functor (StateT s0 mm g) forall s0 (mm :: (* -> *) -> * -> *) (g :: * -> *) (h :: * -> *) x. (FFunctor mm, Functor g, Functor h) => (g ~> h) -> StateT s0 mm g x -> StateT s0 mm h x forall (g :: * -> *). Functor g => Functor (StateT s0 mm g) forall (g :: * -> *) (h :: * -> *) x. (Functor g, Functor h) => (g ~> h) -> StateT s0 mm g x -> StateT s0 mm h x forall (ff :: (* -> *) -> * -> *). (forall (g :: * -> *). Functor g => Functor (ff g)) => (forall (g :: * -> *) (h :: * -> *) x. (Functor g, Functor h) => (g ~> h) -> ff g x -> ff h x) -> FFunctor ff $cffmap :: forall s0 (mm :: (* -> *) -> * -> *) (g :: * -> *) (h :: * -> *) x. (FFunctor mm, Functor g, Functor h) => (g ~> h) -> StateT s0 mm g x -> StateT s0 mm h x ffmap :: forall (g :: * -> *) (h :: * -> *) x. (Functor g, Functor h) => (g ~> h) -> StateT s0 mm g x -> StateT s0 mm h x FFunctor, FFunctor (StateT s0 mm) FFunctor (StateT s0 mm) => (forall (g :: * -> *). Functor g => g ~> StateT s0 mm g) -> (forall (g :: * -> *) (h :: * -> *) a. (Functor g, Functor h) => (g ~> StateT s0 mm h) -> StateT s0 mm g a -> StateT s0 mm h a) -> FMonad (StateT s0 mm) forall s0 (mm :: (* -> *) -> * -> *). FMonad mm => FFunctor (StateT s0 mm) forall s0 (mm :: (* -> *) -> * -> *) (g :: * -> *). (FMonad mm, Functor g) => g ~> StateT s0 mm g forall s0 (mm :: (* -> *) -> * -> *) (g :: * -> *) (h :: * -> *) a. (FMonad mm, Functor g, Functor h) => (g ~> StateT s0 mm h) -> StateT s0 mm g a -> StateT s0 mm h a forall (g :: * -> *). Functor g => g ~> StateT s0 mm g forall (g :: * -> *) (h :: * -> *) a. (Functor g, Functor h) => (g ~> StateT s0 mm h) -> StateT s0 mm g a -> StateT s0 mm h a forall (ff :: (* -> *) -> * -> *). FFunctor ff => (forall (g :: * -> *). Functor g => g ~> ff g) -> (forall (g :: * -> *) (h :: * -> *) a. (Functor g, Functor h) => (g ~> ff h) -> ff g a -> ff h a) -> FMonad ff $cfpure :: forall s0 (mm :: (* -> *) -> * -> *) (g :: * -> *). (FMonad mm, Functor g) => g ~> StateT s0 mm g fpure :: forall (g :: * -> *). Functor g => g ~> StateT s0 mm g $cfbind :: forall s0 (mm :: (* -> *) -> * -> *) (g :: * -> *) (h :: * -> *) a. (FMonad mm, Functor g, Functor h) => (g ~> StateT s0 mm h) -> StateT s0 mm g a -> StateT s0 mm h a fbind :: forall (g :: * -> *) (h :: * -> *) a. (Functor g, Functor h) => (g ~> StateT s0 mm h) -> StateT s0 mm g a -> StateT s0 mm h a FMonad) via (AdjointT (EnvT s0) (ReaderT s0) mm) type State s0 = StateT s0 IdentityT deriving stock instance (FFunctor mm, Functor x) => Functor (StateT s0 mm x) fromAdjointT :: AdjointT (EnvT s0) (ReaderT s0) mm x ~> StateT s0 mm x fromAdjointT :: forall s0 (mm :: (* -> *) -> * -> *) (x :: * -> *) x. AdjointT (EnvT s0) (ReaderT s0) mm x x -> StateT s0 mm x x fromAdjointT = AdjointT (EnvT s0) (ReaderT s0) mm x x -> StateT s0 mm x x forall a b. Coercible a b => a -> b coerce toAdjointT :: StateT s0 mm x ~> AdjointT (EnvT s0) (ReaderT s0) mm x toAdjointT :: forall s0 (mm :: (* -> *) -> * -> *) (x :: * -> *) x. StateT s0 mm x x -> AdjointT (EnvT s0) (ReaderT s0) mm x x toAdjointT = StateT s0 mm x x -> AdjointT (EnvT s0) (ReaderT s0) mm x x forall a b. Coercible a b => a -> b coerce flift :: (FFunctor mm, Functor x) => mm x ~> StateT s0 mm x flift :: forall (mm :: (* -> *) -> * -> *) (x :: * -> *) s0. (FFunctor mm, Functor x) => mm x ~> StateT s0 mm x flift mm x x mm = (s0 -> mm (EnvT s0 x) x) -> StateT s0 mm x x forall s0 (mm :: (* -> *) -> * -> *) (x :: * -> *) a. (s0 -> mm (EnvT s0 x) a) -> StateT s0 mm x a StateT ((s0 -> mm (EnvT s0 x) x) -> StateT s0 mm x x) -> (s0 -> mm (EnvT s0 x) x) -> StateT s0 mm x x forall a b. (a -> b) -> a -> b $ \s0 s0 -> (x ~> EnvT s0 x) -> mm x x -> mm (EnvT s0 x) x forall (g :: * -> *) (h :: * -> *) x. (Functor g, Functor h) => (g ~> h) -> mm g x -> mm h x forall (ff :: (* -> *) -> * -> *) (g :: * -> *) (h :: * -> *) x. (FFunctor ff, Functor g, Functor h) => (g ~> h) -> ff g x -> ff h x ffmap (s0 -> x x -> EnvT s0 x x forall e (w :: * -> *) a. e -> w a -> EnvT e w a EnvT s0 s0) mm x x mm state :: forall s0 x mm a. (FMonad mm, Functor x) => (s0 -> (x a, s0)) -> StateT s0 mm x a state :: forall s0 (x :: * -> *) (mm :: (* -> *) -> * -> *) a. (FMonad mm, Functor x) => (s0 -> (x a, s0)) -> StateT s0 mm x a state s0 -> (x a, s0) stateX = (s0 -> mm (EnvT s0 x) a) -> StateT s0 mm x a forall s0 (mm :: (* -> *) -> * -> *) (x :: * -> *) a. (s0 -> mm (EnvT s0 x) a) -> StateT s0 mm x a StateT \s0 s0 -> let (x a x, s0 s0') = s0 -> (x a, s0) stateX s0 s0 in EnvT s0 x a -> mm (EnvT s0 x) a EnvT s0 x ~> mm (EnvT s0 x) forall (g :: * -> *). Functor g => g ~> mm g forall (ff :: (* -> *) -> * -> *) (g :: * -> *). (FMonad ff, Functor g) => g ~> ff g fpure (s0 -> x a -> EnvT s0 x a forall e (w :: * -> *) a. e -> w a -> EnvT e w a EnvT s0 s0' x a x) runState :: forall s0 x a. State s0 x a -> s0 -> (x a, s0) runState :: forall s0 (x :: * -> *) a. State s0 x a -> s0 -> (x a, s0) runState State s0 x a stateX = (s0, x a) -> (x a, s0) forall a b. (a, b) -> (b, a) swap ((s0, x a) -> (x a, s0)) -> (s0 -> (s0, x a)) -> s0 -> (x a, s0) forall b c a. (b -> c) -> (a -> b) -> a -> c . EnvT s0 x a -> (s0, x a) forall e (w :: * -> *) a. EnvT e w a -> (e, w a) runEnvT (EnvT s0 x a -> (s0, x a)) -> (s0 -> EnvT s0 x a) -> s0 -> (s0, x a) forall b c a. (b -> c) -> (a -> b) -> a -> c . IdentityT (EnvT s0 x) a -> EnvT s0 x a forall {k} (f :: k -> *) (a :: k). IdentityT f a -> f a runIdentityT (IdentityT (EnvT s0 x) a -> EnvT s0 x a) -> (s0 -> IdentityT (EnvT s0 x) a) -> s0 -> EnvT s0 x a forall b c a. (b -> c) -> (a -> b) -> a -> c . State s0 x a -> s0 -> IdentityT (EnvT s0 x) a forall s0 (mm :: (* -> *) -> * -> *) (x :: * -> *) a. StateT s0 mm x a -> s0 -> mm (EnvT s0 x) a runStateT State s0 x a stateX