{-# LANGUAGE QuantifiedConstraints #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE BlockArguments #-} {-# LANGUAGE DerivingVia #-} {-# LANGUAGE DeriveFunctor #-} {-# LANGUAGE StandaloneDeriving #-} module FMonad.State.Simple.Inner (StateT(..), flift, toAdjointT, fromAdjointT, State, state, runState ) where import Control.Monad.Trans.Identity ( IdentityT(..) ) import Control.Comonad.Trans.Traced ( TracedT(..) ) import Control.Monad.Trans.Writer ( WriterT(..) ) import Data.Functor.Day (Day(..), swapped) import Data.Functor.Day.Extra (dayToTraced) import Data.Coerce (coerce) import FMonad import FMonad.Adjoint import FStrong newtype StateT s1 mm x a = StateT { forall s1 (mm :: (* -> *) -> * -> *) (x :: * -> *) a. StateT s1 mm x a -> mm (TracedT s1 x) (a, s1) runStateT :: mm (TracedT s1 x) (a, s1) } deriving ((forall (g :: * -> *). Functor g => Functor (StateT s1 mm g)) => (forall (g :: * -> *) (h :: * -> *) x. (Functor g, Functor h) => (g ~> h) -> StateT s1 mm g x -> StateT s1 mm h x) -> FFunctor (StateT s1 mm) forall s1 (mm :: (* -> *) -> * -> *) (g :: * -> *). (FFunctor mm, Functor g) => Functor (StateT s1 mm g) forall s1 (mm :: (* -> *) -> * -> *) (g :: * -> *) (h :: * -> *) x. (FFunctor mm, Functor g, Functor h) => (g ~> h) -> StateT s1 mm g x -> StateT s1 mm h x forall (g :: * -> *). Functor g => Functor (StateT s1 mm g) forall (g :: * -> *) (h :: * -> *) x. (Functor g, Functor h) => (g ~> h) -> StateT s1 mm g x -> StateT s1 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 s1 (mm :: (* -> *) -> * -> *) (g :: * -> *) (h :: * -> *) x. (FFunctor mm, Functor g, Functor h) => (g ~> h) -> StateT s1 mm g x -> StateT s1 mm h x ffmap :: forall (g :: * -> *) (h :: * -> *) x. (Functor g, Functor h) => (g ~> h) -> StateT s1 mm g x -> StateT s1 mm h x FFunctor, FFunctor (StateT s1 mm) FFunctor (StateT s1 mm) => (forall (g :: * -> *). Functor g => g ~> StateT s1 mm g) -> (forall (g :: * -> *) (h :: * -> *) a. (Functor g, Functor h) => (g ~> StateT s1 mm h) -> StateT s1 mm g a -> StateT s1 mm h a) -> FMonad (StateT s1 mm) forall s1 (mm :: (* -> *) -> * -> *). FMonad mm => FFunctor (StateT s1 mm) forall s1 (mm :: (* -> *) -> * -> *) (g :: * -> *). (FMonad mm, Functor g) => g ~> StateT s1 mm g forall s1 (mm :: (* -> *) -> * -> *) (g :: * -> *) (h :: * -> *) a. (FMonad mm, Functor g, Functor h) => (g ~> StateT s1 mm h) -> StateT s1 mm g a -> StateT s1 mm h a forall (g :: * -> *). Functor g => g ~> StateT s1 mm g forall (g :: * -> *) (h :: * -> *) a. (Functor g, Functor h) => (g ~> StateT s1 mm h) -> StateT s1 mm g a -> StateT s1 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 s1 (mm :: (* -> *) -> * -> *) (g :: * -> *). (FMonad mm, Functor g) => g ~> StateT s1 mm g fpure :: forall (g :: * -> *). Functor g => g ~> StateT s1 mm g $cfbind :: forall s1 (mm :: (* -> *) -> * -> *) (g :: * -> *) (h :: * -> *) a. (FMonad mm, Functor g, Functor h) => (g ~> StateT s1 mm h) -> StateT s1 mm g a -> StateT s1 mm h a fbind :: forall (g :: * -> *) (h :: * -> *) a. (Functor g, Functor h) => (g ~> StateT s1 mm h) -> StateT s1 mm g a -> StateT s1 mm h a FMonad) via (AdjointT (TracedT s1) (WriterT s1) mm) type State s1 = StateT s1 IdentityT deriving stock instance (FFunctor mm, Functor x) => Functor (StateT s1 mm x) toAdjointT :: StateT s1 mm x ~> AdjointT (TracedT s1) (WriterT s1) mm x toAdjointT :: forall s1 (mm :: (* -> *) -> * -> *) (x :: * -> *) x. StateT s1 mm x x -> AdjointT (TracedT s1) (WriterT s1) mm x x toAdjointT = StateT s1 mm x x -> AdjointT (TracedT s1) (WriterT s1) mm x x forall a b. Coercible a b => a -> b coerce fromAdjointT :: AdjointT (TracedT s1) (WriterT s1) mm x ~> StateT s1 mm x fromAdjointT :: forall s1 (mm :: (* -> *) -> * -> *) (x :: * -> *) x. AdjointT (TracedT s1) (WriterT s1) mm x x -> StateT s1 mm x x fromAdjointT = AdjointT (TracedT s1) (WriterT s1) mm x x -> StateT s1 mm x x forall a b. Coercible a b => a -> b coerce flift :: (FStrong mm, Functor x) => mm x ~> StateT s1 mm x flift :: forall (mm :: (* -> *) -> * -> *) (x :: * -> *) s1. (FStrong mm, Functor x) => mm x ~> StateT s1 mm x flift mm x x mm = AdjointT (TracedT s1) (WriterT s1) mm x x -> StateT s1 mm x x forall s1 (mm :: (* -> *) -> * -> *) (x :: * -> *) x. AdjointT (TracedT s1) (WriterT s1) mm x x -> StateT s1 mm x x fromAdjointT (AdjointT (TracedT s1) (WriterT s1) mm x x -> StateT s1 mm x x) -> AdjointT (TracedT s1) (WriterT s1) mm x x -> StateT s1 mm x x forall a b. (a -> b) -> a -> b $ WriterT s1 (mm (TracedT s1 x)) x -> AdjointT (TracedT s1) (WriterT s1) mm x x forall {k} {k1} {k2} {k3} (ff :: k -> k1) (uu :: k2 -> k3 -> *) (mm :: k1 -> k2) (g :: k) (x :: k3). uu (mm (ff g)) x -> AdjointT ff uu mm g x AdjointT (WriterT s1 (mm (TracedT s1 x)) x -> AdjointT (TracedT s1) (WriterT s1) mm x x) -> WriterT s1 (mm (TracedT s1 x)) x -> AdjointT (TracedT s1) (WriterT s1) mm x x forall a b. (a -> b) -> a -> b $ mm (TracedT s1 x) (x, s1) -> WriterT s1 (mm (TracedT s1 x)) x forall w (m :: * -> *) a. m (a, w) -> WriterT w m a WriterT (mm (TracedT s1 x) (x, s1) -> WriterT s1 (mm (TracedT s1 x)) x) -> mm (TracedT s1 x) (x, s1) -> WriterT s1 (mm (TracedT s1 x)) x forall a b. (a -> b) -> a -> b $ (Day x ((->) s1) ~> TracedT s1 x) -> mm (Day x ((->) s1)) (x, s1) -> mm (TracedT s1 x) (x, s1) 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 (Day ((->) s1) x x -> TracedT s1 x x Day ((->) s1) x ~> TracedT s1 x forall (f :: * -> *) s1. Functor f => Day ((->) s1) f ~> TracedT s1 f dayToTraced (Day ((->) s1) x x -> TracedT s1 x x) -> (Day x ((->) s1) x -> Day ((->) s1) x x) -> Day x ((->) s1) x -> TracedT s1 x x forall b c a. (b -> c) -> (a -> b) -> a -> c . Day x ((->) s1) x -> Day ((->) s1) x x forall (f :: * -> *) (g :: * -> *) a. Day f g a -> Day g f a swapped) (Day (mm x) ((->) s1) (x, s1) -> mm (Day x ((->) s1)) (x, s1) Day (mm x) ((->) s1) ~> mm (Day x ((->) s1)) forall (g :: * -> *) (h :: * -> *). Functor g => Day (mm g) h ~> mm (Day g h) forall (ff :: (* -> *) -> * -> *) (g :: * -> *) (h :: * -> *). (FStrong ff, Functor g) => Day (ff g) h ~> ff (Day g h) fstrength (mm x x -> (s1 -> s1) -> (x -> s1 -> (x, s1)) -> Day (mm x) ((->) s1) (x, s1) forall (f :: * -> *) (g :: * -> *) a b c. f b -> g c -> (b -> c -> a) -> Day f g a Day mm x x mm s1 -> s1 forall a. a -> a id (,))) state :: forall s1 x mm a. (Functor x, FMonad mm) => x (s1 -> (a, s1)) -> StateT s1 mm x a state :: forall s1 (x :: * -> *) (mm :: (* -> *) -> * -> *) a. (Functor x, FMonad mm) => x (s1 -> (a, s1)) -> StateT s1 mm x a state = mm (TracedT s1 x) (a, s1) -> StateT s1 mm x a forall s1 (mm :: (* -> *) -> * -> *) (x :: * -> *) a. mm (TracedT s1 x) (a, s1) -> StateT s1 mm x a StateT (mm (TracedT s1 x) (a, s1) -> StateT s1 mm x a) -> (x (s1 -> (a, s1)) -> mm (TracedT s1 x) (a, s1)) -> x (s1 -> (a, s1)) -> StateT s1 mm x a forall b c a. (b -> c) -> (a -> b) -> a -> c . TracedT s1 x (a, s1) -> mm (TracedT s1 x) (a, s1) TracedT s1 x ~> mm (TracedT s1 x) forall (g :: * -> *). Functor g => g ~> mm g forall (ff :: (* -> *) -> * -> *) (g :: * -> *). (FMonad ff, Functor g) => g ~> ff g fpure (TracedT s1 x (a, s1) -> mm (TracedT s1 x) (a, s1)) -> (x (s1 -> (a, s1)) -> TracedT s1 x (a, s1)) -> x (s1 -> (a, s1)) -> mm (TracedT s1 x) (a, s1) forall b c a. (b -> c) -> (a -> b) -> a -> c . x (s1 -> (a, s1)) -> TracedT s1 x (a, s1) forall m (w :: * -> *) a. w (m -> a) -> TracedT m w a TracedT runState :: State s1 x a -> x (s1 -> (a, s1)) runState :: forall s1 (x :: * -> *) a. State s1 x a -> x (s1 -> (a, s1)) runState = State s1 x a -> x (s1 -> (a, s1)) forall a b. Coercible a b => a -> b coerce