{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE DeriveFunctor #-}
module FMonad.State.Ran
  (StateT(..),
  toInner, fromInner,
  
  State, state, state_, get, put,
  runState
  ) where

import Control.Monad.Trans.Identity
import Data.Functor.Kan.Ran
import Data.Functor.Precompose
import Data.Coerce (coerce)
import Control.Comonad (Comonad(..))
import Data.Functor.Identity
import FMonad
import FMonad.Adjoint
import Control.Monad.Trans.Writer (WriterT(..))
import Control.Comonad.Traced (TracedT(..))

import qualified FMonad.State.Simple.Inner as Simple.Inner

-- type StateT s = AdjointT (Precompose s) (Ran s)
newtype StateT s mm x a = StateT { forall (s :: * -> *) (mm :: (* -> *) -> * -> *) (x :: * -> *) a.
StateT s mm x a -> forall r. (a -> s r) -> mm (Precompose s x) r
runStateT :: forall r. (a -> s r) -> mm (Precompose s x) r }
  deriving ((forall (g :: * -> *). Functor g => Functor (StateT s mm g)) =>
(forall (g :: * -> *) (h :: * -> *) x.
 (Functor g, Functor h) =>
 (g ~> h) -> StateT s mm g x -> StateT s mm h x)
-> FFunctor (StateT s mm)
forall (g :: * -> *). Functor g => Functor (StateT s mm g)
forall (g :: * -> *) (h :: * -> *) x.
(Functor g, Functor h) =>
(g ~> h) -> StateT s mm g x -> StateT s mm h x
forall (s :: * -> *) (mm :: (* -> *) -> * -> *) (g :: * -> *).
(FFunctor mm, Functor s, Functor g) =>
Functor (StateT s mm g)
forall (s :: * -> *) (mm :: (* -> *) -> * -> *) (g :: * -> *)
       (h :: * -> *) x.
(FFunctor mm, Functor s, Functor g, Functor h) =>
(g ~> h) -> StateT s mm g x -> StateT s 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 (s :: * -> *) (mm :: (* -> *) -> * -> *) (g :: * -> *)
       (h :: * -> *) x.
(FFunctor mm, Functor s, Functor g, Functor h) =>
(g ~> h) -> StateT s mm g x -> StateT s mm h x
ffmap :: forall (g :: * -> *) (h :: * -> *) x.
(Functor g, Functor h) =>
(g ~> h) -> StateT s mm g x -> StateT s mm h x
FFunctor, FFunctor (StateT s mm)
FFunctor (StateT s mm) =>
(forall (g :: * -> *). Functor g => g ~> StateT s mm g)
-> (forall (g :: * -> *) (h :: * -> *) a.
    (Functor g, Functor h) =>
    (g ~> StateT s mm h) -> StateT s mm g a -> StateT s mm h a)
-> FMonad (StateT s mm)
forall (g :: * -> *). Functor g => g ~> StateT s mm g
forall (g :: * -> *) (h :: * -> *) a.
(Functor g, Functor h) =>
(g ~> StateT s mm h) -> StateT s mm g a -> StateT s mm h a
forall (s :: * -> *) (mm :: (* -> *) -> * -> *).
(Functor s, FMonad mm) =>
FFunctor (StateT s mm)
forall (s :: * -> *) (mm :: (* -> *) -> * -> *) (g :: * -> *).
(Functor s, FMonad mm, Functor g) =>
g ~> StateT s mm g
forall (s :: * -> *) (mm :: (* -> *) -> * -> *) (g :: * -> *)
       (h :: * -> *) a.
(Functor s, FMonad mm, Functor g, Functor h) =>
(g ~> StateT s mm h) -> StateT s mm g a -> StateT s 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 (s :: * -> *) (mm :: (* -> *) -> * -> *) (g :: * -> *).
(Functor s, FMonad mm, Functor g) =>
g ~> StateT s mm g
fpure :: forall (g :: * -> *). Functor g => g ~> StateT s mm g
$cfbind :: forall (s :: * -> *) (mm :: (* -> *) -> * -> *) (g :: * -> *)
       (h :: * -> *) a.
(Functor s, FMonad mm, Functor g, Functor h) =>
(g ~> StateT s mm h) -> StateT s mm g a -> StateT s mm h a
fbind :: forall (g :: * -> *) (h :: * -> *) a.
(Functor g, Functor h) =>
(g ~> StateT s mm h) -> StateT s mm g a -> StateT s mm h a
FMonad) via (AdjointT (Precompose s) (Ran s) mm)

deriving
  stock instance (FFunctor mm, Functor s) => Functor (StateT s mm x)

fromAdjointT :: AdjointT (Precompose s) (Ran s) mm x ~> StateT s mm x
fromAdjointT :: forall (s :: * -> *) (mm :: (* -> *) -> * -> *) (x :: * -> *) x.
AdjointT (Precompose s) (Ran s) mm x x -> StateT s mm x x
fromAdjointT = AdjointT (Precompose s) (Ran s) mm x x -> StateT s mm x x
forall a b. Coercible a b => a -> b
coerce

toAdjointT :: StateT s mm x ~> AdjointT (Precompose s) (Ran s) mm x
toAdjointT :: forall (s :: * -> *) (mm :: (* -> *) -> * -> *) (x :: * -> *) x.
StateT s mm x x -> AdjointT (Precompose s) (Ran s) mm x x
toAdjointT = StateT s mm x x -> AdjointT (Precompose s) (Ran s) mm x x
forall a b. Coercible a b => a -> b
coerce

toInner :: (Functor x, FFunctor mm) => StateT ((->) s1) mm x ~> Simple.Inner.StateT s1 mm x
toInner :: forall (x :: * -> *) (mm :: (* -> *) -> * -> *) s1.
(Functor x, FFunctor mm) =>
StateT ((->) s1) mm x ~> StateT s1 mm x
toInner = AdjointT (TracedT s1) (WriterT s1) mm x x -> StateT s1 mm x x
forall s1 (mm :: (* -> *) -> * -> *) (x1 :: * -> *) x2.
AdjointT (TracedT s1) (WriterT s1) mm x1 x2 -> StateT s1 mm x1 x2
Simple.Inner.fromAdjointT (AdjointT (TracedT s1) (WriterT s1) mm x x -> StateT s1 mm x x)
-> (StateT ((->) s1) mm x x
    -> AdjointT (TracedT s1) (WriterT s1) mm x x)
-> StateT ((->) s1) mm x x
-> StateT s1 mm x x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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)
-> (StateT ((->) s1) mm x x -> WriterT s1 (mm (TracedT s1 x)) x)
-> StateT ((->) s1) mm x x
-> AdjointT (TracedT s1) (WriterT s1) mm x x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (mm (Precompose ((->) s1) x) ~> mm (TracedT s1 x))
-> WriterT s1 (mm (Precompose ((->) s1) x)) x
-> WriterT s1 (mm (TracedT s1 x)) x
forall (g :: * -> *) (h :: * -> *) x.
(Functor g, Functor h) =>
(g ~> h) -> WriterT s1 g x -> WriterT s1 h x
forall (ff :: (* -> *) -> * -> *) (g :: * -> *) (h :: * -> *) x.
(FFunctor ff, Functor g, Functor h) =>
(g ~> h) -> ff g x -> ff h x
ffmap ((Precompose ((->) s1) x ~> TracedT s1 x)
-> mm (Precompose ((->) s1) x) x -> mm (TracedT s1 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 (x (s1 -> x) -> TracedT s1 x x
forall m (w :: * -> *) a. w (m -> a) -> TracedT m w a
TracedT (x (s1 -> x) -> TracedT s1 x x)
-> (Precompose ((->) s1) x x -> x (s1 -> x))
-> Precompose ((->) s1) x x
-> TracedT s1 x x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Precompose ((->) s1) x x -> x (s1 -> x)
forall j k (f :: j -> k) (g :: k -> *) (a :: j).
Precompose f g a -> g (f a)
getPrecompose)) (WriterT s1 (mm (Precompose ((->) s1) x)) x
 -> WriterT s1 (mm (TracedT s1 x)) x)
-> (StateT ((->) s1) mm x x
    -> WriterT s1 (mm (Precompose ((->) s1) x)) x)
-> StateT ((->) s1) mm x x
-> WriterT s1 (mm (TracedT s1 x)) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ran ((->) s1) (mm (Precompose ((->) s1) x)) x
-> WriterT s1 (mm (Precompose ((->) s1) x)) x
Ran ((->) s1) (mm (Precompose ((->) s1) x))
~> WriterT s1 (mm (Precompose ((->) s1) x))
forall (f :: * -> *) s1.
Functor f =>
Ran ((->) s1) f ~> WriterT s1 f
ranToWriter (Ran ((->) s1) (mm (Precompose ((->) s1) x)) x
 -> WriterT s1 (mm (Precompose ((->) s1) x)) x)
-> (StateT ((->) s1) mm x x
    -> Ran ((->) s1) (mm (Precompose ((->) s1) x)) x)
-> StateT ((->) s1) mm x x
-> WriterT s1 (mm (Precompose ((->) s1) x)) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AdjointT (Precompose ((->) s1)) (Ran ((->) s1)) mm x x
-> Ran ((->) s1) (mm (Precompose ((->) s1) x)) x
forall {k1} {k2} {k3} {k4} (ff :: k1 -> k2) (uu :: k3 -> k4 -> *)
       (mm :: k2 -> k3) (g :: k1) (x :: k4).
AdjointT ff uu mm g x -> uu (mm (ff g)) x
runAdjointT (AdjointT (Precompose ((->) s1)) (Ran ((->) s1)) mm x x
 -> Ran ((->) s1) (mm (Precompose ((->) s1) x)) x)
-> (StateT ((->) s1) mm x x
    -> AdjointT (Precompose ((->) s1)) (Ran ((->) s1)) mm x x)
-> StateT ((->) s1) mm x x
-> Ran ((->) s1) (mm (Precompose ((->) s1) x)) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StateT ((->) s1) mm x x
-> AdjointT (Precompose ((->) s1)) (Ran ((->) s1)) mm x x
forall (s :: * -> *) (mm :: (* -> *) -> * -> *) (x :: * -> *) x.
StateT s mm x x -> AdjointT (Precompose s) (Ran s) mm x x
toAdjointT

fromInner :: (Functor x, FFunctor mm) => Simple.Inner.StateT s1 mm x ~> StateT ((->) s1) mm x
fromInner :: forall (x :: * -> *) (mm :: (* -> *) -> * -> *) s1.
(Functor x, FFunctor mm) =>
StateT s1 mm x ~> StateT ((->) s1) mm x
fromInner = AdjointT (Precompose ((->) s1)) (Ran ((->) s1)) mm x x
-> StateT ((->) s1) mm x x
forall (s :: * -> *) (mm :: (* -> *) -> * -> *) (x :: * -> *) x.
AdjointT (Precompose s) (Ran s) mm x x -> StateT s mm x x
fromAdjointT (AdjointT (Precompose ((->) s1)) (Ran ((->) s1)) mm x x
 -> StateT ((->) s1) mm x x)
-> (StateT s1 mm x x
    -> AdjointT (Precompose ((->) s1)) (Ran ((->) s1)) mm x x)
-> StateT s1 mm x x
-> StateT ((->) s1) mm x x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ran ((->) s1) (mm (Precompose ((->) s1) x)) x
-> AdjointT (Precompose ((->) s1)) (Ran ((->) 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 (Ran ((->) s1) (mm (Precompose ((->) s1) x)) x
 -> AdjointT (Precompose ((->) s1)) (Ran ((->) s1)) mm x x)
-> (StateT s1 mm x x
    -> Ran ((->) s1) (mm (Precompose ((->) s1) x)) x)
-> StateT s1 mm x x
-> AdjointT (Precompose ((->) s1)) (Ran ((->) s1)) mm x x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (mm (TracedT s1 x) ~> mm (Precompose ((->) s1) x))
-> Ran ((->) s1) (mm (TracedT s1 x)) x
-> Ran ((->) s1) (mm (Precompose ((->) s1) x)) x
forall (g :: * -> *) (h :: * -> *) x.
(Functor g, Functor h) =>
(g ~> h) -> Ran ((->) s1) g x -> Ran ((->) s1) h x
forall (ff :: (* -> *) -> * -> *) (g :: * -> *) (h :: * -> *) x.
(FFunctor ff, Functor g, Functor h) =>
(g ~> h) -> ff g x -> ff h x
ffmap ((TracedT s1 x ~> Precompose ((->) s1) x)
-> mm (TracedT s1 x) x -> mm (Precompose ((->) s1) 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 (x (s1 -> x) -> Precompose ((->) s1) x x
forall j k (f :: j -> k) (g :: k -> *) (a :: j).
g (f a) -> Precompose f g a
Precompose (x (s1 -> x) -> Precompose ((->) s1) x x)
-> (TracedT s1 x x -> x (s1 -> x))
-> TracedT s1 x x
-> Precompose ((->) s1) x x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TracedT s1 x x -> x (s1 -> x)
forall m (w :: * -> *) a. TracedT m w a -> w (m -> a)
runTracedT)) (Ran ((->) s1) (mm (TracedT s1 x)) x
 -> Ran ((->) s1) (mm (Precompose ((->) s1) x)) x)
-> (StateT s1 mm x x -> Ran ((->) s1) (mm (TracedT s1 x)) x)
-> StateT s1 mm x x
-> Ran ((->) s1) (mm (Precompose ((->) s1) x)) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. WriterT s1 (mm (TracedT s1 x)) x
-> Ran ((->) s1) (mm (TracedT s1 x)) x
WriterT s1 (mm (TracedT s1 x)) ~> Ran ((->) s1) (mm (TracedT s1 x))
forall (f :: * -> *) s1.
Functor f =>
WriterT s1 f ~> Ran ((->) s1) f
writerToRan (WriterT s1 (mm (TracedT s1 x)) x
 -> Ran ((->) s1) (mm (TracedT s1 x)) x)
-> (StateT s1 mm x x -> WriterT s1 (mm (TracedT s1 x)) x)
-> StateT s1 mm x x
-> Ran ((->) s1) (mm (TracedT s1 x)) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AdjointT (TracedT s1) (WriterT s1) mm x x
-> WriterT s1 (mm (TracedT s1 x)) x
forall {k1} {k2} {k3} {k4} (ff :: k1 -> k2) (uu :: k3 -> k4 -> *)
       (mm :: k2 -> k3) (g :: k1) (x :: k4).
AdjointT ff uu mm g x -> uu (mm (ff g)) x
runAdjointT (AdjointT (TracedT s1) (WriterT s1) mm x x
 -> WriterT s1 (mm (TracedT s1 x)) x)
-> (StateT s1 mm x x -> AdjointT (TracedT s1) (WriterT s1) mm x x)
-> StateT s1 mm x x
-> WriterT s1 (mm (TracedT s1 x)) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StateT s1 mm x x -> AdjointT (TracedT s1) (WriterT s1) mm x x
forall s1 (mm :: (* -> *) -> * -> *) (x1 :: * -> *) x2.
StateT s1 mm x1 x2 -> AdjointT (TracedT s1) (WriterT s1) mm x1 x2
Simple.Inner.toAdjointT

ranToWriter :: Functor f => Ran ((->) s1) f ~> WriterT s1 f
ranToWriter :: forall (f :: * -> *) s1.
Functor f =>
Ran ((->) s1) f ~> WriterT s1 f
ranToWriter (Ran forall b. (x -> s1 -> b) -> f b
ran) = f (x, s1) -> WriterT s1 f x
forall w (m :: * -> *) a. m (a, w) -> WriterT w m a
WriterT (f (x, s1) -> WriterT s1 f x) -> f (x, s1) -> WriterT s1 f x
forall a b. (a -> b) -> a -> b
$ (x -> s1 -> (x, s1)) -> f (x, s1)
forall b. (x -> s1 -> b) -> f b
ran (,)

writerToRan :: Functor f => WriterT s1 f ~> Ran ((->) s1) f
writerToRan :: forall (f :: * -> *) s1.
Functor f =>
WriterT s1 f ~> Ran ((->) s1) f
writerToRan (WriterT f (x, s1)
f_as) = (forall b. (x -> s1 -> b) -> f b) -> Ran ((->) s1) f x
forall {k} (g :: k -> *) (h :: k -> *) a.
(forall (b :: k). (a -> g b) -> h b) -> Ran g h a
Ran ((forall b. (x -> s1 -> b) -> f b) -> Ran ((->) s1) f x)
-> (forall b. (x -> s1 -> b) -> f b) -> Ran ((->) s1) f x
forall a b. (a -> b) -> a -> b
$ \x -> s1 -> b
k -> ((x, s1) -> b) -> f (x, s1) -> f b
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((x -> s1 -> b) -> (x, s1) -> b
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry x -> s1 -> b
k) f (x, s1)
f_as

-- * Pure state

type State s = StateT s IdentityT

state :: (Functor s, Functor x, FMonad mm)
  => (forall r. (a -> s r) -> x (s r))
  -> StateT s mm x a
state :: forall (s :: * -> *) (x :: * -> *) (mm :: (* -> *) -> * -> *) a.
(Functor s, Functor x, FMonad mm) =>
(forall r. (a -> s r) -> x (s r)) -> StateT s mm x a
state forall r. (a -> s r) -> x (s r)
f = (forall r. (a -> s r) -> mm (Precompose s x) r) -> StateT s mm x a
forall (s :: * -> *) (mm :: (* -> *) -> * -> *) (x :: * -> *) a.
(forall r. (a -> s r) -> mm (Precompose s x) r) -> StateT s mm x a
StateT ((forall r. (a -> s r) -> mm (Precompose s x) r)
 -> StateT s mm x a)
-> (forall r. (a -> s r) -> mm (Precompose s x) r)
-> StateT s mm x a
forall a b. (a -> b) -> a -> b
$ \a -> s r
k -> Precompose s x r -> mm (Precompose s x) r
Precompose s x ~> mm (Precompose s x)
forall (g :: * -> *). Functor g => g ~> mm g
forall (ff :: (* -> *) -> * -> *) (g :: * -> *).
(FMonad ff, Functor g) =>
g ~> ff g
fpure (x (s r) -> Precompose s x r
forall j k (f :: j -> k) (g :: k -> *) (a :: j).
g (f a) -> Precompose f g a
Precompose ((a -> s r) -> x (s r)
forall r. (a -> s r) -> x (s r)
f a -> s r
k))

state_ :: (Functor s, Functor x, FMonad mm)
  => (forall r. s r -> x (s r))
  -> StateT s mm x ()
state_ :: forall (s :: * -> *) (x :: * -> *) (mm :: (* -> *) -> * -> *).
(Functor s, Functor x, FMonad mm) =>
(forall r. s r -> x (s r)) -> StateT s mm x ()
state_ forall r. s r -> x (s r)
f = (forall r. (() -> s r) -> x (s r)) -> StateT s mm x ()
forall (s :: * -> *) (x :: * -> *) (mm :: (* -> *) -> * -> *) a.
(Functor s, Functor x, FMonad mm) =>
(forall r. (a -> s r) -> x (s r)) -> StateT s mm x a
state (\() -> s r
k -> s r -> x (s r)
forall r. s r -> x (s r)
f (() -> s r
k ()))

get :: (Comonad s, FMonad mm) => StateT s mm s ()
get :: forall (s :: * -> *) (mm :: (* -> *) -> * -> *).
(Comonad s, FMonad mm) =>
StateT s mm s ()
get = (forall r. s r -> s (s r)) -> StateT s mm s ()
forall (s :: * -> *) (x :: * -> *) (mm :: (* -> *) -> * -> *).
(Functor s, Functor x, FMonad mm) =>
(forall r. s r -> x (s r)) -> StateT s mm x ()
state_ s r -> s (s r)
forall r. s r -> s (s r)
forall (w :: * -> *) a. Comonad w => w a -> w (w a)
duplicate

put :: (Comonad s, FMonad mm) => s a -> StateT s mm Identity a
put :: forall (s :: * -> *) (mm :: (* -> *) -> * -> *) a.
(Comonad s, FMonad mm) =>
s a -> StateT s mm Identity a
put s a
sa = (forall r. (a -> s r) -> Identity (s r)) -> StateT s mm Identity a
forall (s :: * -> *) (x :: * -> *) (mm :: (* -> *) -> * -> *) a.
(Functor s, Functor x, FMonad mm) =>
(forall r. (a -> s r) -> x (s r)) -> StateT s mm x a
state (\a -> s r
k -> s r -> Identity (s r)
forall a. a -> Identity a
Identity (s r -> r
forall a. s a -> a
forall (w :: * -> *) a. Comonad w => w a -> a
extract (s r -> r) -> (a -> s r) -> a -> r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> s r
k (a -> r) -> s a -> s r
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> s a
sa))

runState :: State s x a -> (a -> s r) -> x (s r)
runState :: forall (s :: * -> *) (x :: * -> *) a r.
State s x a -> (a -> s r) -> x (s r)
runState State s x a
sm a -> s r
k = Precompose s x r -> x (s r)
forall j k (f :: j -> k) (g :: k -> *) (a :: j).
Precompose f g a -> g (f a)
getPrecompose (Precompose s x r -> x (s r)) -> Precompose s x r -> x (s r)
forall a b. (a -> b) -> a -> b
$ IdentityT (Precompose s x) r -> Precompose s x r
forall {k} (f :: k -> *) (a :: k). IdentityT f a -> f a
runIdentityT (IdentityT (Precompose s x) r -> Precompose s x r)
-> IdentityT (Precompose s x) r -> Precompose s x r
forall a b. (a -> b) -> a -> b
$ State s x a -> forall r. (a -> s r) -> IdentityT (Precompose s x) r
forall (s :: * -> *) (mm :: (* -> *) -> * -> *) (x :: * -> *) a.
StateT s mm x a -> forall r. (a -> s r) -> mm (Precompose s x) r
runStateT State s x a
sm a -> s r
k