{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE DerivingVia #-}
module FMonad.State.Lan
  (StateT(..),
   fromAdjointT,
   toAdjointT,
   toInner, fromInner,
   
   State,
   state, runState
  ) where

import Control.Monad.Trans.Identity
import Data.Functor.Kan.Lan
import Data.Functor.Precompose
import qualified FMonad.State.Simple.Inner as Simple.Inner

import FMonad
import FMonad.Adjoint
import Data.Tuple (swap)
import Control.Monad.Trans.Writer (WriterT(..))
import Control.Comonad.Traced (TracedT(..))
import Data.Coerce (coerce)

-- type StateT s = AdjointT (Lan s) (Precompose s)
newtype StateT s mm x a = StateT { forall (s :: * -> *) (mm :: (* -> *) -> * -> *) (x :: * -> *) a.
StateT s mm x a -> mm (Lan s x) (s a)
runStateT :: mm (Lan s x) (s a) }
  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 (Lan s) (Precompose s) mm)

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

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

fromAdjointT :: AdjointT (Lan s) (Precompose s) mm x ~> StateT s mm x
fromAdjointT :: forall (s :: * -> *) (mm :: (* -> *) -> * -> *) (x :: * -> *) x.
AdjointT (Lan s) (Precompose s) mm x x -> StateT s mm x x
fromAdjointT = AdjointT (Lan s) (Precompose s) mm x x -> StateT 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 (Lan ((,) s1) x) ~> mm (TracedT s1 x))
-> WriterT s1 (mm (Lan ((,) 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 ((Lan ((,) s1) x ~> TracedT s1 x)
-> mm (Lan ((,) 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 Lan ((,) s1) x x -> TracedT s1 x x
Lan ((,) s1) x ~> TracedT s1 x
forall (f :: * -> *) s1.
Functor f =>
Lan ((,) s1) f ~> TracedT s1 f
lanToTraced) (WriterT s1 (mm (Lan ((,) s1) x)) x
 -> WriterT s1 (mm (TracedT s1 x)) x)
-> (StateT ((,) s1) mm x x -> WriterT s1 (mm (Lan ((,) 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
. (mm (Lan ((,) s1) x) (x, s1) -> WriterT s1 (mm (Lan ((,) s1) x)) x
forall w (m :: * -> *) a. m (a, w) -> WriterT w m a
WriterT (mm (Lan ((,) s1) x) (x, s1) -> WriterT s1 (mm (Lan ((,) s1) x)) x)
-> (Precompose ((,) s1) (mm (Lan ((,) s1) x)) x
    -> mm (Lan ((,) s1) x) (x, s1))
-> Precompose ((,) s1) (mm (Lan ((,) s1) x)) x
-> WriterT s1 (mm (Lan ((,) s1) x)) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((s1, x) -> (x, s1))
-> mm (Lan ((,) s1) x) (s1, x) -> mm (Lan ((,) s1) x) (x, s1)
forall a b.
(a -> b) -> mm (Lan ((,) s1) x) a -> mm (Lan ((,) s1) x) b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (s1, x) -> (x, s1)
forall a b. (a, b) -> (b, a)
swap (mm (Lan ((,) s1) x) (s1, x) -> mm (Lan ((,) s1) x) (x, s1))
-> (Precompose ((,) s1) (mm (Lan ((,) s1) x)) x
    -> mm (Lan ((,) s1) x) (s1, x))
-> Precompose ((,) s1) (mm (Lan ((,) s1) x)) x
-> mm (Lan ((,) s1) x) (x, s1)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Precompose ((,) s1) (mm (Lan ((,) s1) x)) x
-> mm (Lan ((,) s1) x) (s1, x)
forall j k (f :: j -> k) (g :: k -> *) (a :: j).
Precompose f g a -> g (f a)
getPrecompose) (Precompose ((,) s1) (mm (Lan ((,) s1) x)) x
 -> WriterT s1 (mm (Lan ((,) s1) x)) x)
-> (StateT ((,) s1) mm x x
    -> Precompose ((,) s1) (mm (Lan ((,) s1) x)) x)
-> StateT ((,) s1) mm x x
-> WriterT s1 (mm (Lan ((,) s1) x)) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AdjointT (Lan ((,) s1)) (Precompose ((,) s1)) mm x x
-> Precompose ((,) s1) (mm (Lan ((,) 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 (Lan ((,) s1)) (Precompose ((,) s1)) mm x x
 -> Precompose ((,) s1) (mm (Lan ((,) s1) x)) x)
-> (StateT ((,) s1) mm x x
    -> AdjointT (Lan ((,) s1)) (Precompose ((,) s1)) mm x x)
-> StateT ((,) s1) mm x x
-> Precompose ((,) s1) (mm (Lan ((,) s1) x)) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StateT ((,) s1) mm x x
-> AdjointT (Lan ((,) s1)) (Precompose ((,) s1)) mm x x
forall (s :: * -> *) (mm :: (* -> *) -> * -> *) (x :: * -> *) x.
StateT s mm x x -> AdjointT (Lan s) (Precompose 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 (Lan ((,) s1)) (Precompose ((,) s1)) mm x x
-> StateT ((,) s1) mm x x
forall (s :: * -> *) (mm :: (* -> *) -> * -> *) (x :: * -> *) x.
AdjointT (Lan s) (Precompose s) mm x x -> StateT s mm x x
fromAdjointT (AdjointT (Lan ((,) s1)) (Precompose ((,) s1)) mm x x
 -> StateT ((,) s1) mm x x)
-> (StateT s1 mm x x
    -> AdjointT (Lan ((,) s1)) (Precompose ((,) s1)) mm x x)
-> StateT s1 mm x x
-> StateT ((,) s1) mm x x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Precompose ((,) s1) (mm (Lan ((,) s1) x)) x
-> AdjointT (Lan ((,) s1)) (Precompose ((,) 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 (Precompose ((,) s1) (mm (Lan ((,) s1) x)) x
 -> AdjointT (Lan ((,) s1)) (Precompose ((,) s1)) mm x x)
-> (StateT s1 mm x x
    -> Precompose ((,) s1) (mm (Lan ((,) s1) x)) x)
-> StateT s1 mm x x
-> AdjointT (Lan ((,) s1)) (Precompose ((,) s1)) mm x x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (mm (TracedT s1 x) ~> mm (Lan ((,) s1) x))
-> Precompose ((,) s1) (mm (TracedT s1 x)) x
-> Precompose ((,) s1) (mm (Lan ((,) s1) x)) x
forall (g :: * -> *) (h :: * -> *) x.
(Functor g, Functor h) =>
(g ~> h) -> Precompose ((,) s1) g x -> Precompose ((,) 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 ~> Lan ((,) s1) x)
-> mm (TracedT s1 x) x -> mm (Lan ((,) 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 TracedT s1 x x -> Lan ((,) s1) x x
TracedT s1 x ~> Lan ((,) s1) x
forall s1 (f :: * -> *) x. TracedT s1 f x -> Lan ((,) s1) f x
tracedToLan) (Precompose ((,) s1) (mm (TracedT s1 x)) x
 -> Precompose ((,) s1) (mm (Lan ((,) s1) x)) x)
-> (StateT s1 mm x x -> Precompose ((,) s1) (mm (TracedT s1 x)) x)
-> StateT s1 mm x x
-> Precompose ((,) s1) (mm (Lan ((,) s1) x)) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (mm (TracedT s1 x) (s1, x)
-> Precompose ((,) s1) (mm (TracedT s1 x)) x
forall j k (f :: j -> k) (g :: k -> *) (a :: j).
g (f a) -> Precompose f g a
Precompose (mm (TracedT s1 x) (s1, x)
 -> Precompose ((,) s1) (mm (TracedT s1 x)) x)
-> (WriterT s1 (mm (TracedT s1 x)) x -> mm (TracedT s1 x) (s1, x))
-> WriterT s1 (mm (TracedT s1 x)) x
-> Precompose ((,) s1) (mm (TracedT s1 x)) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((x, s1) -> (s1, x))
-> mm (TracedT s1 x) (x, s1) -> mm (TracedT s1 x) (s1, x)
forall a b. (a -> b) -> mm (TracedT s1 x) a -> mm (TracedT s1 x) b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (x, s1) -> (s1, x)
forall a b. (a, b) -> (b, a)
swap (mm (TracedT s1 x) (x, s1) -> mm (TracedT s1 x) (s1, x))
-> (WriterT s1 (mm (TracedT s1 x)) x -> mm (TracedT s1 x) (x, s1))
-> WriterT s1 (mm (TracedT s1 x)) x
-> mm (TracedT s1 x) (s1, x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. WriterT s1 (mm (TracedT s1 x)) x -> mm (TracedT s1 x) (x, s1)
forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
runWriterT) (WriterT s1 (mm (TracedT s1 x)) x
 -> Precompose ((,) s1) (mm (TracedT s1 x)) x)
-> (StateT s1 mm x x -> WriterT s1 (mm (TracedT s1 x)) x)
-> StateT s1 mm x x
-> Precompose ((,) 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

lanToTraced :: Functor f => Lan ((,) s1) f ~> TracedT s1 f
lanToTraced :: forall (f :: * -> *) s1.
Functor f =>
Lan ((,) s1) f ~> TracedT s1 f
lanToTraced (Lan (s1, b) -> x
sr_a f b
fr) = f (s1 -> x) -> TracedT s1 f x
forall m (w :: * -> *) a. w (m -> a) -> TracedT m w a
TracedT (f (s1 -> x) -> TracedT s1 f x) -> f (s1 -> x) -> TracedT s1 f x
forall a b. (a -> b) -> a -> b
$ (b -> s1 -> x) -> f b -> f (s1 -> x)
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\b
r s1
s -> (s1, b) -> x
sr_a (s1
s,b
r)) f b
fr

tracedToLan :: TracedT s1 f ~> Lan ((,) s1) f
tracedToLan :: forall s1 (f :: * -> *) x. TracedT s1 f x -> Lan ((,) s1) f x
tracedToLan (TracedT f (s1 -> x)
fsa) = ((s1, s1 -> x) -> x) -> f (s1 -> x) -> Lan ((,) s1) f x
forall {k} (g :: k -> *) (b :: k) a (h :: k -> *).
(g b -> a) -> h b -> Lan g h a
Lan (\(s1
s1,s1 -> x
sa) -> s1 -> x
sa s1
s1) f (s1 -> x)
fsa

-- * Pure state

type State s = StateT s IdentityT

state :: (Functor s, FMonad mm, Functor x)
  => (s b -> s a) -> x b -> StateT s mm x a
state :: forall (s :: * -> *) (mm :: (* -> *) -> * -> *) (x :: * -> *) b a.
(Functor s, FMonad mm, Functor x) =>
(s b -> s a) -> x b -> StateT s mm x a
state s b -> s a
f x b
xb = mm (Lan s x) (s a) -> StateT s mm x a
forall (s :: * -> *) (mm :: (* -> *) -> * -> *) (x :: * -> *) a.
mm (Lan s x) (s a) -> StateT s mm x a
StateT (mm (Lan s x) (s a) -> StateT s mm x a)
-> mm (Lan s x) (s a) -> StateT s mm x a
forall a b. (a -> b) -> a -> b
$ Lan s x (s a) -> mm (Lan s x) (s a)
Lan s x ~> mm (Lan s x)
forall (g :: * -> *). Functor g => g ~> mm g
forall (ff :: (* -> *) -> * -> *) (g :: * -> *).
(FMonad ff, Functor g) =>
g ~> ff g
fpure ((s b -> s a) -> x b -> Lan s x (s a)
forall {k} (g :: k -> *) (b :: k) a (h :: k -> *).
(g b -> a) -> h b -> Lan g h a
Lan s b -> s a
f x b
xb)

runState :: State s x a -> Lan s x (s a)
runState :: forall (s :: * -> *) (x :: * -> *) a. State s x a -> Lan s x (s a)
runState = IdentityT (Lan s x) (s a) -> Lan s x (s a)
forall {k} (f :: k -> *) (a :: k). IdentityT f a -> f a
runIdentityT (IdentityT (Lan s x) (s a) -> Lan s x (s a))
-> (State s x a -> IdentityT (Lan s x) (s a))
-> State s x a
-> Lan s x (s a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. State s x a -> IdentityT (Lan s x) (s a)
forall (s :: * -> *) (mm :: (* -> *) -> * -> *) (x :: * -> *) a.
StateT s mm x a -> mm (Lan s x) (s a)
runStateT