From ca62da969634717d7d34deaf44c3f5dc7d52d66c Mon Sep 17 00:00:00 2001
From: Eitan Chatav <eitan.chatav@gmail.com>
Date: Mon, 17 Nov 2025 11:13:52 -0800
Subject: [PATCH 01/19] indexed right Kan extension

optimization via Cayley representation of indexed monad transformers
---
 indexed-transformers.cabal                   |  4 +-
 src/Control/Monad/Trans/Indexed/Codensity.hs | 60 ++++++++++++++++++++
 src/Control/Monad/Trans/Indexed/Free/Wrap.hs |  5 ++
 src/Control/Monad/Trans/Indexed/State/Kan.hs | 18 ++++++
 4 files changed, 86 insertions(+), 1 deletion(-)
 create mode 100644 src/Control/Monad/Trans/Indexed/Codensity.hs
 create mode 100644 src/Control/Monad/Trans/Indexed/State/Kan.hs

diff --git a/indexed-transformers.cabal b/indexed-transformers.cabal
index 0bd88b1..6cc6480 100644
--- a/indexed-transformers.cabal
+++ b/indexed-transformers.cabal
@@ -1,6 +1,6 @@
 cabal-version: 2.2
 
--- This file has been generated from package.yaml by hpack version 0.36.0.
+-- This file has been generated from package.yaml by hpack version 0.38.1.
 --
 -- see: https://github.com/sol/hpack
 
@@ -28,12 +28,14 @@ source-repository head
 library
   exposed-modules:
       Control.Monad.Trans.Indexed
+      Control.Monad.Trans.Indexed.Codensity
       Control.Monad.Trans.Indexed.Cont
       Control.Monad.Trans.Indexed.Do
       Control.Monad.Trans.Indexed.Free
       Control.Monad.Trans.Indexed.Free.Fold
       Control.Monad.Trans.Indexed.Free.Wrap
       Control.Monad.Trans.Indexed.State
+      Control.Monad.Trans.Indexed.State.Kan
       Control.Monad.Trans.Indexed.Writer
   other-modules:
       Paths_indexed_transformers
diff --git a/src/Control/Monad/Trans/Indexed/Codensity.hs b/src/Control/Monad/Trans/Indexed/Codensity.hs
new file mode 100644
index 0000000..3b0a1c0
--- /dev/null
+++ b/src/Control/Monad/Trans/Indexed/Codensity.hs
@@ -0,0 +1,60 @@
+{-# LANGUAGE
+DerivingStrategies
+, GeneralizedNewtypeDeriving
+, StandaloneDeriving
+, TypeApplications
+#-}
+
+module Control.Monad.Trans.Indexed.Codensity
+  ( CodensityIx (..)
+  , lowerCodensityIx
+  , liftCodensityIx
+  ) where
+
+import Control.Applicative
+import Control.Monad
+import Control.Monad.Reader
+import Control.Monad.State
+import Control.Monad.Trans.Indexed
+
+newtype CodensityIx t i j m a = CodensityIx
+  { runCodensityIx :: forall b k. (a -> t j k m b) -> t i k m b }
+  deriving Functor
+
+lowerCodensityIx
+  :: (IxMonadTrans t, Monad m)
+  => CodensityIx t i j m a -> t i j m a
+lowerCodensityIx (CodensityIx f) = f $ \a -> return a
+
+liftCodensityIx
+  :: (IxMonadTrans t, Monad m)
+  => t i j m a -> CodensityIx t i j m a
+liftCodensityIx m = CodensityIx $ \h -> bindIx h m
+
+instance IxMonadTrans t => IxMonadTrans (CodensityIx t) where
+  joinIx (CodensityIx k) =
+    CodensityIx $ \f -> k $ \(CodensityIx g) -> g f
+instance i ~ j => Applicative (CodensityIx t i j m) where
+  pure x = CodensityIx $ \k -> k x
+  CodensityIx cf <*> CodensityIx cx =
+    CodensityIx $ \ k -> cf $ \ f -> cx (k . f)
+instance i ~ j => Monad (CodensityIx t i j m) where
+  return = pure
+  CodensityIx cx >>= k =
+    CodensityIx $ \ c -> cx (\ x -> runCodensityIx (k x) c)
+instance (IxMonadTrans t, i ~ j) => MonadTrans (CodensityIx t i j) where
+  lift m = CodensityIx (\k -> bindIx k (lift m))
+instance (i ~ j, Alternative (t i j m), IxMonadTrans t, Monad m)
+  => Alternative (CodensityIx t i j m) where
+    empty = liftCodensityIx empty
+    x <|> y = liftCodensityIx (lowerCodensityIx x <|> lowerCodensityIx y)
+instance (i ~ j, Alternative (t i j m), IxMonadTrans t, Monad m)
+  => MonadPlus (CodensityIx t i j m)
+instance (i ~ j, MonadReader i (t i j m), IxMonadTrans t, Monad m)
+  => MonadReader i (CodensityIx t i j m) where
+  ask = liftCodensityIx ask
+  local f m = liftCodensityIx (local f (lowerCodensityIx m))
+instance (i ~ j, MonadReader i (t i j m), IxMonadTrans t, Monad m)
+  => MonadState i (CodensityIx t i j m) where
+  get = ask
+  put s = liftCodensityIx (local (const s) (pure ()))
diff --git a/src/Control/Monad/Trans/Indexed/Free/Wrap.hs b/src/Control/Monad/Trans/Indexed/Free/Wrap.hs
index 7a4f61f..9c08486 100644
--- a/src/Control/Monad/Trans/Indexed/Free/Wrap.hs
+++ b/src/Control/Monad/Trans/Indexed/Free/Wrap.hs
@@ -12,6 +12,7 @@ module Control.Monad.Trans.Indexed.Free.Wrap
   , WrapIx (..)
   ) where
 
+import Control.Applicative
 import Control.Monad.Free
 import Control.Monad.Trans
 import Control.Monad.Trans.Indexed
@@ -34,6 +35,10 @@ instance (IxFunctor f, i ~ j, Monad m)
   => Applicative (FreeIx f i j m) where
     pure = FreeIx . pure . Unwrap
     (<*>) = apIx
+instance (IxFunctor f, i ~ j, Monad m, Alternative m)
+  => Alternative (FreeIx f i j m) where
+    empty = FreeIx empty
+    FreeIx x <|> FreeIx y = FreeIx (x <|> y)
 instance (IxFunctor f, i ~ j, Monad m)
   => Monad (FreeIx f i j m) where
     return = pure
diff --git a/src/Control/Monad/Trans/Indexed/State/Kan.hs b/src/Control/Monad/Trans/Indexed/State/Kan.hs
new file mode 100644
index 0000000..5f90dd4
--- /dev/null
+++ b/src/Control/Monad/Trans/Indexed/State/Kan.hs
@@ -0,0 +1,18 @@
+module Control.Monad.Trans.Indexed.State.Kan
+  ( StateIx
+  , ReadStx (..)
+  ) where
+
+import Control.Monad.Trans.Indexed.Codensity
+import Control.Monad.Trans.Indexed.Free.Wrap
+
+type StateIx = CodensityIx (FreeIx ReadStx)
+
+data ReadStx s t x where
+  NoOpStx :: ReadStx s s ()
+  AskStx :: ReadStx s s s
+  LocalStx
+    :: (u -> s) -> (x -> y)
+    -> ReadStx s t x -> ReadStx u t y
+instance Functor (ReadStx s t) where
+  fmap = LocalStx id

From ebf8ba3ae85c8d62b28ae6e3642ce65822057936 Mon Sep 17 00:00:00 2001
From: Eitan Chatav <eitan.chatav@gmail.com>
Date: Mon, 17 Nov 2025 12:00:17 -0800
Subject: [PATCH 02/19] Update Kan.hs

---
 src/Control/Monad/Trans/Indexed/State/Kan.hs | 13 +++++++++++++
 1 file changed, 13 insertions(+)

diff --git a/src/Control/Monad/Trans/Indexed/State/Kan.hs b/src/Control/Monad/Trans/Indexed/State/Kan.hs
index 5f90dd4..2231ad8 100644
--- a/src/Control/Monad/Trans/Indexed/State/Kan.hs
+++ b/src/Control/Monad/Trans/Indexed/State/Kan.hs
@@ -3,7 +3,10 @@ module Control.Monad.Trans.Indexed.State.Kan
   , ReadStx (..)
   ) where
 
+import Control.Monad.Reader
+import Control.Monad.State
 import Control.Monad.Trans.Indexed.Codensity
+import Control.Monad.Trans.Indexed.Free
 import Control.Monad.Trans.Indexed.Free.Wrap
 
 type StateIx = CodensityIx (FreeIx ReadStx)
@@ -16,3 +19,13 @@ data ReadStx s t x where
     -> ReadStx s t x -> ReadStx u t y
 instance Functor (ReadStx s t) where
   fmap = LocalStx id
+
+instance (s ~ t, Monad m, IxMonadTransFree freeIx)
+  => MonadReader s (freeIx ReadStx s t m) where
+    ask = liftFreeIx AskStx
+    local f m = lowerCodensityIx $ do
+      s <- ask
+      put (f s)
+      x <- liftCodensityIx m
+      put s
+      return x

From 02c173fc5a6f21c195c32726de93de0d75e3a910 Mon Sep 17 00:00:00 2001
From: Eitan Chatav <eitan.chatav@gmail.com>
Date: Mon, 17 Nov 2025 13:05:56 -0800
Subject: [PATCH 03/19] Ixer

---
 src/Control/Monad/Trans/Indexed/Free.hs      | 36 ++++++++++----------
 src/Control/Monad/Trans/Indexed/State/Kan.hs | 26 ++++++--------
 2 files changed, 29 insertions(+), 33 deletions(-)

diff --git a/src/Control/Monad/Trans/Indexed/Free.hs b/src/Control/Monad/Trans/Indexed/Free.hs
index 2d9a011..f8d9c9d 100644
--- a/src/Control/Monad/Trans/Indexed/Free.hs
+++ b/src/Control/Monad/Trans/Indexed/Free.hs
@@ -12,7 +12,7 @@ The free indexed monad transformer.
 
 module Control.Monad.Trans.Indexed.Free
   ( IxMonadTransFree (liftFreeIx, hoistFreeIx, foldFreeIx), coerceFreeIx
-  , IxFunctor, IxMap (IxMap), liftFreerIx, hoistFreerIx, foldFreerIx
+  , IxFunctor, Ixer (Ixer), liftFreerIx, hoistFreerIx, foldFreerIx
   ) where
 
 import Control.Monad.Free
@@ -24,7 +24,7 @@ The free `IxMonadTrans` generated by an `IxFunctor`
 is characterized by the `IxMonadTransFree` class
 up to the isomorphism `coerceFreeIx`.
 
-`IxMonadTransFree` and `IxMap`, the free `IxMonadTrans` and
+`IxMonadTransFree` and `Ixer`, the free `IxMonadTrans` and
 the free `IxFunctor`, can be combined as a "freer" `IxMonadTrans`
 and used as a DSL generated by primitive commands like this
 [Conor McBride example]
@@ -46,14 +46,14 @@ data DVDCommand
 >>> :{
 insert
   :: (IxMonadTransFree freeIx, Monad m)
-  => DVD -> freeIx (IxMap DVDCommand) 'False 'True m ()
+  => DVD -> freeIx (Ixer DVDCommand) 'False 'True m ()
 insert dvd = liftFreerIx (Insert dvd)
 :}
 
 >>> :{
 eject
   :: (IxMonadTransFree freeIx, Monad m)
-  => freeIx (IxMap DVDCommand) 'True 'False m DVD
+  => freeIx (Ixer DVDCommand) 'True 'False m DVD
 eject = liftFreerIx Eject
 :}
 
@@ -62,7 +62,7 @@ eject = liftFreerIx Eject
 >>> :{
 swap
   :: (IxMonadTransFree freeIx, Monad m)
-  => DVD -> freeIx (IxMap DVDCommand) 'True 'True m DVD
+  => DVD -> freeIx (Ixer DVDCommand) 'True 'True m DVD
 swap dvd = Indexed.do
   dvd' <- eject
   insert dvd
@@ -71,7 +71,7 @@ swap dvd = Indexed.do
 
 >>> import Control.Monad.Trans
 >>> :{
-printDVD :: IxMonadTransFree freeIx => freeIx (IxMap DVDCommand) 'True 'True IO ()
+printDVD :: IxMonadTransFree freeIx => freeIx (Ixer DVDCommand) 'True 'True IO ()
 printDVD = Indexed.do
   dvd <- eject
   insert dvd
@@ -112,30 +112,30 @@ type IxFunctor
 type IxFunctor f = forall i j. Functor (f i j)
 
 {- |
-`IxMap` is the free `IxFunctor`. It's a left Kan extension.
-Combining `IxMonadTransFree` with `IxMap` as demonstrated in the above example,
+`Ixer` is the free `IxFunctor`. It's a left Kan extension.
+Combining `IxMonadTransFree` with `Ixer` as demonstrated in the above example,
 gives the "freer" `IxMonadTrans`, modeled on this
 [Oleg Kiselyov explanation]
 (https://okmij.org/ftp/Computation/free-monad.html#freer).
 -}
-data IxMap f i j x where
-  IxMap :: (x -> y) -> f i j x -> IxMap f i j y
-instance Functor (IxMap f i j) where
-  fmap g (IxMap f x) = IxMap (g . f) x
+data Ixer f i j x where
+  Ixer :: (x -> y) -> f i j x -> Ixer f i j y
+instance Functor (Ixer f i j) where
+  fmap g (Ixer f x) = Ixer (g . f) x
 
 liftFreerIx
   :: (IxMonadTransFree freeIx, Monad m)
-  => f i j x -> freeIx (IxMap f) i j m x
-liftFreerIx x = liftFreeIx (IxMap id x)
+  => f i j x -> freeIx (Ixer f) i j m x
+liftFreerIx x = liftFreeIx (Ixer id x)
 
 hoistFreerIx
   :: (IxMonadTransFree freeIx, Monad m)
   => (forall i j x. f i j x -> g i j x)
-  -> freeIx (IxMap f) i j m x -> freeIx (IxMap g) i j m x
-hoistFreerIx f = hoistFreeIx (\(IxMap g x) -> IxMap g (f x))
+  -> freeIx (Ixer f) i j m x -> freeIx (Ixer g) i j m x
+hoistFreerIx f = hoistFreeIx (\(Ixer g x) -> Ixer g (f x))
 
 foldFreerIx
   :: (IxMonadTransFree freeIx, IxMonadTrans t, Monad m)
   => (forall i j x. f i j x -> t i j m x)
-  -> freeIx (IxMap f) i j m x -> t i j m x
-foldFreerIx f x = foldFreeIx (\(IxMap g y) -> g <$> f y) x
+  -> freeIx (Ixer f) i j m x -> t i j m x
+foldFreerIx f x = foldFreeIx (\(Ixer g y) -> g <$> f y) x
diff --git a/src/Control/Monad/Trans/Indexed/State/Kan.hs b/src/Control/Monad/Trans/Indexed/State/Kan.hs
index 2231ad8..d57bf81 100644
--- a/src/Control/Monad/Trans/Indexed/State/Kan.hs
+++ b/src/Control/Monad/Trans/Indexed/State/Kan.hs
@@ -3,29 +3,25 @@ module Control.Monad.Trans.Indexed.State.Kan
   , ReadStx (..)
   ) where
 
+import Control.Monad
 import Control.Monad.Reader
 import Control.Monad.State
 import Control.Monad.Trans.Indexed.Codensity
 import Control.Monad.Trans.Indexed.Free
 import Control.Monad.Trans.Indexed.Free.Wrap
 
-type StateIx = CodensityIx (FreeIx ReadStx)
+type StateIx = CodensityIx (FreeIx (Ixer ReadStx))
 
 data ReadStx s t x where
-  NoOpStx :: ReadStx s s ()
   AskStx :: ReadStx s s s
-  LocalStx
-    :: (u -> s) -> (x -> y)
-    -> ReadStx s t x -> ReadStx u t y
-instance Functor (ReadStx s t) where
-  fmap = LocalStx id
 
-instance (s ~ t, Monad m, IxMonadTransFree freeIx)
-  => MonadReader s (freeIx ReadStx s t m) where
-    ask = liftFreeIx AskStx
-    local f m = lowerCodensityIx $ do
+instance (s ~ t, Monad m)
+  => MonadReader s (FreeIx (Ixer ReadStx) s t m) where
+    ask = liftFreerIx AskStx
+    local f m = do
       s <- ask
-      put (f s)
-      x <- liftCodensityIx m
-      put s
-      return x
+      lowerCodensityIx $ do
+        put (f s)
+        x <- liftCodensityIx m
+        put s
+        return x

From 9af959fe7cd4832ea213e9cd0536aeec7ab208ee Mon Sep 17 00:00:00 2001
From: Eitan Chatav <eitan.chatav@gmail.com>
Date: Mon, 17 Nov 2025 13:08:26 -0800
Subject: [PATCH 04/19] Update Kan.hs

---
 src/Control/Monad/Trans/Indexed/State/Kan.hs | 8 +++-----
 1 file changed, 3 insertions(+), 5 deletions(-)

diff --git a/src/Control/Monad/Trans/Indexed/State/Kan.hs b/src/Control/Monad/Trans/Indexed/State/Kan.hs
index d57bf81..412eda9 100644
--- a/src/Control/Monad/Trans/Indexed/State/Kan.hs
+++ b/src/Control/Monad/Trans/Indexed/State/Kan.hs
@@ -3,7 +3,6 @@ module Control.Monad.Trans.Indexed.State.Kan
   , ReadStx (..)
   ) where
 
-import Control.Monad
 import Control.Monad.Reader
 import Control.Monad.State
 import Control.Monad.Trans.Indexed.Codensity
@@ -12,11 +11,10 @@ import Control.Monad.Trans.Indexed.Free.Wrap
 
 type StateIx = CodensityIx (FreeIx (Ixer ReadStx))
 
-data ReadStx s t x where
-  AskStx :: ReadStx s s s
+data ReadStx s t x where AskStx :: ReadStx s s s
 
-instance (s ~ t, Monad m)
-  => MonadReader s (FreeIx (Ixer ReadStx) s t m) where
+instance (s ~ t, Monad m, IxMonadTransFree freeIx)
+  => MonadReader s (freeIx (Ixer ReadStx) s t m) where
     ask = liftFreerIx AskStx
     local f m = do
       s <- ask

From 78795114be8a0d9dd4916a37c3a799098356662a Mon Sep 17 00:00:00 2001
From: Eitan Chatav <eitan.chatav@gmail.com>
Date: Mon, 17 Nov 2025 14:35:41 -0800
Subject: [PATCH 05/19] Codense

---
 indexed-transformers.cabal                   |  1 -
 src/Control/Monad/Trans/Indexed/Codensity.hs | 34 +++++++++++++++++---
 src/Control/Monad/Trans/Indexed/State.hs     | 21 ++++++++++--
 src/Control/Monad/Trans/Indexed/State/Kan.hs | 25 --------------
 4 files changed, 48 insertions(+), 33 deletions(-)
 delete mode 100644 src/Control/Monad/Trans/Indexed/State/Kan.hs

diff --git a/indexed-transformers.cabal b/indexed-transformers.cabal
index 6cc6480..53261b5 100644
--- a/indexed-transformers.cabal
+++ b/indexed-transformers.cabal
@@ -35,7 +35,6 @@ library
       Control.Monad.Trans.Indexed.Free.Fold
       Control.Monad.Trans.Indexed.Free.Wrap
       Control.Monad.Trans.Indexed.State
-      Control.Monad.Trans.Indexed.State.Kan
       Control.Monad.Trans.Indexed.Writer
   other-modules:
       Paths_indexed_transformers
diff --git a/src/Control/Monad/Trans/Indexed/Codensity.hs b/src/Control/Monad/Trans/Indexed/Codensity.hs
index 3b0a1c0..7cf4c4f 100644
--- a/src/Control/Monad/Trans/Indexed/Codensity.hs
+++ b/src/Control/Monad/Trans/Indexed/Codensity.hs
@@ -9,6 +9,9 @@ module Control.Monad.Trans.Indexed.Codensity
   ( CodensityIx (..)
   , lowerCodensityIx
   , liftCodensityIx
+  , ReaderIx
+  , StateIx
+  , ReadStx (..)
   ) where
 
 import Control.Applicative
@@ -16,6 +19,9 @@ import Control.Monad
 import Control.Monad.Reader
 import Control.Monad.State
 import Control.Monad.Trans.Indexed
+import Control.Monad.Trans.Indexed.Free
+import Control.Monad.Trans.Indexed.Free.Fold
+import Control.Monad.Trans.Indexed.State hiding (StateIx (..))
 
 newtype CodensityIx t i j m a = CodensityIx
   { runCodensityIx :: forall b k. (a -> t j k m b) -> t i k m b }
@@ -24,7 +30,7 @@ newtype CodensityIx t i j m a = CodensityIx
 lowerCodensityIx
   :: (IxMonadTrans t, Monad m)
   => CodensityIx t i j m a -> t i j m a
-lowerCodensityIx (CodensityIx f) = f $ \a -> return a
+lowerCodensityIx (CodensityIx f) = f return
 
 liftCodensityIx
   :: (IxMonadTrans t, Monad m)
@@ -50,11 +56,29 @@ instance (i ~ j, Alternative (t i j m), IxMonadTrans t, Monad m)
     x <|> y = liftCodensityIx (lowerCodensityIx x <|> lowerCodensityIx y)
 instance (i ~ j, Alternative (t i j m), IxMonadTrans t, Monad m)
   => MonadPlus (CodensityIx t i j m)
-instance (i ~ j, MonadReader i (t i j m), IxMonadTrans t, Monad m)
+instance (i ~ j, IxMonadTransReader t, Monad m)
   => MonadReader i (CodensityIx t i j m) where
   ask = liftCodensityIx ask
-  local f m = liftCodensityIx (local f (lowerCodensityIx m))
-instance (i ~ j, MonadReader i (t i j m), IxMonadTrans t, Monad m)
+  local = localIx
+instance IxMonadTransReader t => IxMonadTransReader (CodensityIx t) where
+  localIx f m = bindIx (thenIx m . putIx . f) ask
+instance (i ~ j, IxMonadTransReader t, Monad m)
   => MonadState i (CodensityIx t i j m) where
   get = ask
-  put s = liftCodensityIx (local (const s) (pure ()))
+  put = putIx
+instance IxMonadTransReader t => IxMonadTransState (CodensityIx t) where
+  putIx s = CodensityIx (\k -> localIx (const s) (k ()))
+
+type ReaderIx = FreeIx (Ixer ReadStx)
+
+type StateIx = CodensityIx ReaderIx
+
+data ReadStx s t x where AskStx :: ReadStx s s s
+
+instance (s ~ t, Monad m, IxMonadTransFree freeIx)
+  => MonadReader s (freeIx (Ixer ReadStx) s t m) where
+    ask = liftFreerIx AskStx
+    local = localIx
+instance IxMonadTransFree freeIx
+  => IxMonadTransReader (freeIx (Ixer ReadStx)) where
+    localIx f = lowerCodensityIx . localIx f . liftCodensityIx
diff --git a/src/Control/Monad/Trans/Indexed/State.hs b/src/Control/Monad/Trans/Indexed/State.hs
index c2af5ea..1d23587 100644
--- a/src/Control/Monad/Trans/Indexed/State.hs
+++ b/src/Control/Monad/Trans/Indexed/State.hs
@@ -15,8 +15,11 @@ module Control.Monad.Trans.Indexed.State
   , putIx
   , toStateT
   , fromStateT
+  , IxMonadTransReader (..)
+  , IxMonadTransState (..)
   ) where
 
+import Control.Monad.Reader
 import Control.Monad.State
 import Control.Monad.Trans.Indexed
 
@@ -46,11 +49,25 @@ execStateIx m i = snd <$> runStateIx m i
 modifyIx :: Applicative m => (i -> j) -> StateIx i j m ()
 modifyIx f = StateIx $ \i -> pure ((), f i)
 
-putIx :: Applicative m => j -> StateIx i j m ()
-putIx j = modifyIx (\ _ -> j)
+-- putIx :: Applicative m => j -> StateIx i j m ()
+-- putIx j = modifyIx (\ _ -> j)
 
 toStateT :: StateIx i i m x -> StateT i m x
 toStateT (StateIx f) = StateT f
 
 fromStateT :: StateT i m x -> StateIx i i m x
 fromStateT (StateT f) = StateIx f
+
+class
+  ( IxMonadTrans t
+  , forall m i j r. (Monad m, i ~ j, j ~ r) => MonadReader r (t i j m)
+  ) => IxMonadTransReader t where
+  localIx :: Monad m => (i -> h) -> t h j m a -> t i j m a
+
+class
+  ( IxMonadTrans t
+  , forall m i j s. (Monad m, i ~ j, j ~ s) => MonadState s (t i j m)
+  ) => IxMonadTransState t where
+  putIx :: Monad m => j -> t i j m ()
+instance IxMonadTransState StateIx where
+  putIx j = modifyIx (\ _ -> j)
diff --git a/src/Control/Monad/Trans/Indexed/State/Kan.hs b/src/Control/Monad/Trans/Indexed/State/Kan.hs
deleted file mode 100644
index 412eda9..0000000
--- a/src/Control/Monad/Trans/Indexed/State/Kan.hs
+++ /dev/null
@@ -1,25 +0,0 @@
-module Control.Monad.Trans.Indexed.State.Kan
-  ( StateIx
-  , ReadStx (..)
-  ) where
-
-import Control.Monad.Reader
-import Control.Monad.State
-import Control.Monad.Trans.Indexed.Codensity
-import Control.Monad.Trans.Indexed.Free
-import Control.Monad.Trans.Indexed.Free.Wrap
-
-type StateIx = CodensityIx (FreeIx (Ixer ReadStx))
-
-data ReadStx s t x where AskStx :: ReadStx s s s
-
-instance (s ~ t, Monad m, IxMonadTransFree freeIx)
-  => MonadReader s (freeIx (Ixer ReadStx) s t m) where
-    ask = liftFreerIx AskStx
-    local f m = do
-      s <- ask
-      lowerCodensityIx $ do
-        put (f s)
-        x <- liftCodensityIx m
-        put s
-        return x

From 75a3ab2d992c464175afec73742292ee448c6d7d Mon Sep 17 00:00:00 2001
From: Eitan Chatav <eitan.chatav@gmail.com>
Date: Mon, 17 Nov 2025 15:28:44 -0800
Subject: [PATCH 06/19] Update State.hs

---
 src/Control/Monad/Trans/Indexed/State.hs | 27 ++++++++++--------------
 1 file changed, 11 insertions(+), 16 deletions(-)

diff --git a/src/Control/Monad/Trans/Indexed/State.hs b/src/Control/Monad/Trans/Indexed/State.hs
index 1d23587..3fdcb29 100644
--- a/src/Control/Monad/Trans/Indexed/State.hs
+++ b/src/Control/Monad/Trans/Indexed/State.hs
@@ -11,8 +11,6 @@ module Control.Monad.Trans.Indexed.State
   ( StateIx (..)
   , evalStateIx
   , execStateIx
-  , modifyIx
-  , putIx
   , toStateT
   , fromStateT
   , IxMonadTransReader (..)
@@ -23,7 +21,7 @@ import Control.Monad.Reader
 import Control.Monad.State
 import Control.Monad.Trans.Indexed
 
-newtype StateIx i j m x = StateIx { runStateIx :: i -> m (x, j)}
+newtype StateIx i j m x = StateIx {runStateIx :: i -> m (x, j)}
   deriving Functor
 instance IxMonadTrans StateIx where
   joinIx (StateIx f) = StateIx $ \i -> do
@@ -39,6 +37,9 @@ instance i ~ j => MonadTrans (StateIx i j) where
   lift m = StateIx $ \i -> (, i) <$> m
 instance (i ~ j, Monad m) => MonadState i (StateIx i j m) where
   state f = StateIx (return . f)
+instance (i ~ j, Monad m) => MonadReader i (StateIx i j m) where
+  ask = get
+  local = undefined
 
 evalStateIx :: Monad m => StateIx i j m x -> i -> m x
 evalStateIx m i = fst <$> runStateIx m i
@@ -46,28 +47,22 @@ evalStateIx m i = fst <$> runStateIx m i
 execStateIx :: Monad m => StateIx i j m x -> i -> m j
 execStateIx m i = snd <$> runStateIx m i
 
-modifyIx :: Applicative m => (i -> j) -> StateIx i j m ()
-modifyIx f = StateIx $ \i -> pure ((), f i)
-
--- putIx :: Applicative m => j -> StateIx i j m ()
--- putIx j = modifyIx (\ _ -> j)
-
 toStateT :: StateIx i i m x -> StateT i m x
 toStateT (StateIx f) = StateT f
 
 fromStateT :: StateT i m x -> StateIx i i m x
 fromStateT (StateT f) = StateIx f
 
-class
-  ( IxMonadTrans t
-  , forall m i j r. (Monad m, i ~ j, j ~ r) => MonadReader r (t i j m)
-  ) => IxMonadTransReader t where
-  localIx :: Monad m => (i -> h) -> t h j m a -> t i j m a
-
 class
   ( IxMonadTrans t
   , forall m i j s. (Monad m, i ~ j, j ~ s) => MonadState s (t i j m)
   ) => IxMonadTransState t where
   putIx :: Monad m => j -> t i j m ()
+  putIx s = stateIx (\_ -> ((), s))
+  modifyIx :: Monad m => (i -> j) -> t i j m ()
+  modifyIx f = stateIx (\i -> ((), f i))
+  stateIx :: Monad m => (i -> (a,j)) -> t i j m a
+  stateIx f =
+    bindIx (\s -> let ~(a, s') = f s in thenIx (return a) (putIx s')) get
 instance IxMonadTransState StateIx where
-  putIx j = modifyIx (\ _ -> j)
+  stateIx f = StateIx (return . f)

From 076068aabe14637f5dff7e9625a71bd224874529 Mon Sep 17 00:00:00 2001
From: Eitan Chatav <eitan.chatav@gmail.com>
Date: Mon, 17 Nov 2025 15:28:49 -0800
Subject: [PATCH 07/19] Update Codensity.hs

---
 src/Control/Monad/Trans/Indexed/Codensity.hs | 22 ++++++++++----------
 1 file changed, 11 insertions(+), 11 deletions(-)

diff --git a/src/Control/Monad/Trans/Indexed/Codensity.hs b/src/Control/Monad/Trans/Indexed/Codensity.hs
index 7cf4c4f..d524658 100644
--- a/src/Control/Monad/Trans/Indexed/Codensity.hs
+++ b/src/Control/Monad/Trans/Indexed/Codensity.hs
@@ -10,7 +10,7 @@ module Control.Monad.Trans.Indexed.Codensity
   , lowerCodensityIx
   , liftCodensityIx
   , ReaderIx
-  , StateIx
+  , KanStateIx
   , ReadStx (..)
   ) where
 
@@ -56,22 +56,22 @@ instance (i ~ j, Alternative (t i j m), IxMonadTrans t, Monad m)
     x <|> y = liftCodensityIx (lowerCodensityIx x <|> lowerCodensityIx y)
 instance (i ~ j, Alternative (t i j m), IxMonadTrans t, Monad m)
   => MonadPlus (CodensityIx t i j m)
-instance (i ~ j, IxMonadTransReader t, Monad m)
-  => MonadReader i (CodensityIx t i j m) where
-  ask = liftCodensityIx ask
-  local = localIx
-instance IxMonadTransReader t => IxMonadTransReader (CodensityIx t) where
-  localIx f m = bindIx (thenIx m . putIx . f) ask
 instance (i ~ j, IxMonadTransReader t, Monad m)
   => MonadState i (CodensityIx t i j m) where
-  get = ask
+  get = liftCodensityIx ask
   put = putIx
 instance IxMonadTransReader t => IxMonadTransState (CodensityIx t) where
-  putIx s = CodensityIx (\k -> localIx (const s) (k ()))
+  putIx s = CodensityIx (localIx (const s) . ($ ()))
+
+class
+  ( IxMonadTrans t
+  , forall m i j r. (Monad m, i ~ j, j ~ r) => MonadReader r (t i j m)
+  ) => IxMonadTransReader t where
+  localIx :: Monad m => (i -> h) -> t h j m a -> t i j m a
 
 type ReaderIx = FreeIx (Ixer ReadStx)
 
-type StateIx = CodensityIx ReaderIx
+type KanStateIx = CodensityIx ReaderIx
 
 data ReadStx s t x where AskStx :: ReadStx s s s
 
@@ -81,4 +81,4 @@ instance (s ~ t, Monad m, IxMonadTransFree freeIx)
     local = localIx
 instance IxMonadTransFree freeIx
   => IxMonadTransReader (freeIx (Ixer ReadStx)) where
-    localIx f = lowerCodensityIx . localIx f . liftCodensityIx
+    localIx f = lowerCodensityIx . (\m -> bindIx (thenIx m . putIx . f) get) . liftCodensityIx

From bcb78b54006ed11df1691fc0b8e7e33bfa3687be Mon Sep 17 00:00:00 2001
From: Eitan Chatav <eitan.chatav@gmail.com>
Date: Mon, 17 Nov 2025 15:38:23 -0800
Subject: [PATCH 08/19] move to State

---
 indexed-transformers.cabal                   |  1 -
 src/Control/Monad/Trans/Indexed/Codensity.hs | 84 --------------------
 src/Control/Monad/Trans/Indexed/State.hs     | 70 +++++++++++++++-
 3 files changed, 68 insertions(+), 87 deletions(-)
 delete mode 100644 src/Control/Monad/Trans/Indexed/Codensity.hs

diff --git a/indexed-transformers.cabal b/indexed-transformers.cabal
index 53261b5..263865a 100644
--- a/indexed-transformers.cabal
+++ b/indexed-transformers.cabal
@@ -28,7 +28,6 @@ source-repository head
 library
   exposed-modules:
       Control.Monad.Trans.Indexed
-      Control.Monad.Trans.Indexed.Codensity
       Control.Monad.Trans.Indexed.Cont
       Control.Monad.Trans.Indexed.Do
       Control.Monad.Trans.Indexed.Free
diff --git a/src/Control/Monad/Trans/Indexed/Codensity.hs b/src/Control/Monad/Trans/Indexed/Codensity.hs
deleted file mode 100644
index d524658..0000000
--- a/src/Control/Monad/Trans/Indexed/Codensity.hs
+++ /dev/null
@@ -1,84 +0,0 @@
-{-# LANGUAGE
-DerivingStrategies
-, GeneralizedNewtypeDeriving
-, StandaloneDeriving
-, TypeApplications
-#-}
-
-module Control.Monad.Trans.Indexed.Codensity
-  ( CodensityIx (..)
-  , lowerCodensityIx
-  , liftCodensityIx
-  , ReaderIx
-  , KanStateIx
-  , ReadStx (..)
-  ) where
-
-import Control.Applicative
-import Control.Monad
-import Control.Monad.Reader
-import Control.Monad.State
-import Control.Monad.Trans.Indexed
-import Control.Monad.Trans.Indexed.Free
-import Control.Monad.Trans.Indexed.Free.Fold
-import Control.Monad.Trans.Indexed.State hiding (StateIx (..))
-
-newtype CodensityIx t i j m a = CodensityIx
-  { runCodensityIx :: forall b k. (a -> t j k m b) -> t i k m b }
-  deriving Functor
-
-lowerCodensityIx
-  :: (IxMonadTrans t, Monad m)
-  => CodensityIx t i j m a -> t i j m a
-lowerCodensityIx (CodensityIx f) = f return
-
-liftCodensityIx
-  :: (IxMonadTrans t, Monad m)
-  => t i j m a -> CodensityIx t i j m a
-liftCodensityIx m = CodensityIx $ \h -> bindIx h m
-
-instance IxMonadTrans t => IxMonadTrans (CodensityIx t) where
-  joinIx (CodensityIx k) =
-    CodensityIx $ \f -> k $ \(CodensityIx g) -> g f
-instance i ~ j => Applicative (CodensityIx t i j m) where
-  pure x = CodensityIx $ \k -> k x
-  CodensityIx cf <*> CodensityIx cx =
-    CodensityIx $ \ k -> cf $ \ f -> cx (k . f)
-instance i ~ j => Monad (CodensityIx t i j m) where
-  return = pure
-  CodensityIx cx >>= k =
-    CodensityIx $ \ c -> cx (\ x -> runCodensityIx (k x) c)
-instance (IxMonadTrans t, i ~ j) => MonadTrans (CodensityIx t i j) where
-  lift m = CodensityIx (\k -> bindIx k (lift m))
-instance (i ~ j, Alternative (t i j m), IxMonadTrans t, Monad m)
-  => Alternative (CodensityIx t i j m) where
-    empty = liftCodensityIx empty
-    x <|> y = liftCodensityIx (lowerCodensityIx x <|> lowerCodensityIx y)
-instance (i ~ j, Alternative (t i j m), IxMonadTrans t, Monad m)
-  => MonadPlus (CodensityIx t i j m)
-instance (i ~ j, IxMonadTransReader t, Monad m)
-  => MonadState i (CodensityIx t i j m) where
-  get = liftCodensityIx ask
-  put = putIx
-instance IxMonadTransReader t => IxMonadTransState (CodensityIx t) where
-  putIx s = CodensityIx (localIx (const s) . ($ ()))
-
-class
-  ( IxMonadTrans t
-  , forall m i j r. (Monad m, i ~ j, j ~ r) => MonadReader r (t i j m)
-  ) => IxMonadTransReader t where
-  localIx :: Monad m => (i -> h) -> t h j m a -> t i j m a
-
-type ReaderIx = FreeIx (Ixer ReadStx)
-
-type KanStateIx = CodensityIx ReaderIx
-
-data ReadStx s t x where AskStx :: ReadStx s s s
-
-instance (s ~ t, Monad m, IxMonadTransFree freeIx)
-  => MonadReader s (freeIx (Ixer ReadStx) s t m) where
-    ask = liftFreerIx AskStx
-    local = localIx
-instance IxMonadTransFree freeIx
-  => IxMonadTransReader (freeIx (Ixer ReadStx)) where
-    localIx f = lowerCodensityIx . (\m -> bindIx (thenIx m . putIx . f) get) . liftCodensityIx
diff --git a/src/Control/Monad/Trans/Indexed/State.hs b/src/Control/Monad/Trans/Indexed/State.hs
index 3fdcb29..798b58d 100644
--- a/src/Control/Monad/Trans/Indexed/State.hs
+++ b/src/Control/Monad/Trans/Indexed/State.hs
@@ -8,18 +8,28 @@ The state indexed monad transformer.
 -}
 
 module Control.Monad.Trans.Indexed.State
-  ( StateIx (..)
+  ( -- * State
+    IxMonadTransState (..)
+  , StateIx (..)
   , evalStateIx
   , execStateIx
   , toStateT
   , fromStateT
+    -- * Reader
   , IxMonadTransReader (..)
-  , IxMonadTransState (..)
+  , ReadStx (..)
+    -- * Codensity
+  , CodensityIx (..)
+  , liftCodensityIx
+  , lowerCodensityIx
   ) where
 
+import Control.Applicative
+import Control.Monad
 import Control.Monad.Reader
 import Control.Monad.State
 import Control.Monad.Trans.Indexed
+import Control.Monad.Trans.Indexed.Free
 
 newtype StateIx i j m x = StateIx {runStateIx :: i -> m (x, j)}
   deriving Functor
@@ -66,3 +76,59 @@ class
     bindIx (\s -> let ~(a, s') = f s in thenIx (return a) (putIx s')) get
 instance IxMonadTransState StateIx where
   stateIx f = StateIx (return . f)
+
+newtype CodensityIx t i j m a = CodensityIx
+  { runCodensityIx :: forall b k. (a -> t j k m b) -> t i k m b }
+  deriving Functor
+
+lowerCodensityIx
+  :: (IxMonadTrans t, Monad m)
+  => CodensityIx t i j m a -> t i j m a
+lowerCodensityIx (CodensityIx f) = f return
+
+liftCodensityIx
+  :: (IxMonadTrans t, Monad m)
+  => t i j m a -> CodensityIx t i j m a
+liftCodensityIx m = CodensityIx $ \h -> bindIx h m
+
+class
+  ( IxMonadTrans t
+  , forall m i j r. (Monad m, i ~ j, j ~ r) => MonadReader r (t i j m)
+  ) => IxMonadTransReader t where
+  localIx :: Monad m => (i -> h) -> t h j m a -> t i j m a
+
+data ReadStx s t x where AskStx :: ReadStx s s s
+
+instance IxMonadTrans t => IxMonadTrans (CodensityIx t) where
+  joinIx (CodensityIx k) =
+    CodensityIx $ \f -> k $ \(CodensityIx g) -> g f
+instance i ~ j => Applicative (CodensityIx t i j m) where
+  pure x = CodensityIx $ \k -> k x
+  CodensityIx cf <*> CodensityIx cx =
+    CodensityIx $ \ k -> cf $ \ f -> cx (k . f)
+instance i ~ j => Monad (CodensityIx t i j m) where
+  return = pure
+  CodensityIx cx >>= k =
+    CodensityIx $ \ c -> cx (\ x -> runCodensityIx (k x) c)
+instance (IxMonadTrans t, i ~ j) => MonadTrans (CodensityIx t i j) where
+  lift m = CodensityIx (\k -> bindIx k (lift m))
+instance (i ~ j, Alternative (t i j m), IxMonadTrans t, Monad m)
+  => Alternative (CodensityIx t i j m) where
+    empty = liftCodensityIx empty
+    x <|> y = liftCodensityIx (lowerCodensityIx x <|> lowerCodensityIx y)
+instance (i ~ j, Alternative (t i j m), IxMonadTrans t, Monad m)
+  => MonadPlus (CodensityIx t i j m)
+instance (i ~ j, IxMonadTransReader t, Monad m)
+  => MonadState i (CodensityIx t i j m) where
+  get = liftCodensityIx ask
+  put = putIx
+instance IxMonadTransReader t => IxMonadTransState (CodensityIx t) where
+  putIx s = CodensityIx (localIx (const s) . ($ ()))
+
+instance (s ~ t, Monad m, IxMonadTransFree freeIx)
+  => MonadReader s (freeIx (Ixer ReadStx) s t m) where
+    ask = liftFreerIx AskStx
+    local = localIx
+instance IxMonadTransFree freeIx
+  => IxMonadTransReader (freeIx (Ixer ReadStx)) where
+    localIx f = lowerCodensityIx . (\m -> bindIx (thenIx m . putIx . f) get) . liftCodensityIx

From 41d7c24ca6cb4aa344f0770510c745f806a398b8 Mon Sep 17 00:00:00 2001
From: Eitan Chatav <eitan.chatav@gmail.com>
Date: Mon, 17 Nov 2025 15:40:10 -0800
Subject: [PATCH 09/19] Update State.hs

---
 src/Control/Monad/Trans/Indexed/State.hs | 3 ---
 1 file changed, 3 deletions(-)

diff --git a/src/Control/Monad/Trans/Indexed/State.hs b/src/Control/Monad/Trans/Indexed/State.hs
index 798b58d..11b80ab 100644
--- a/src/Control/Monad/Trans/Indexed/State.hs
+++ b/src/Control/Monad/Trans/Indexed/State.hs
@@ -47,9 +47,6 @@ instance i ~ j => MonadTrans (StateIx i j) where
   lift m = StateIx $ \i -> (, i) <$> m
 instance (i ~ j, Monad m) => MonadState i (StateIx i j m) where
   state f = StateIx (return . f)
-instance (i ~ j, Monad m) => MonadReader i (StateIx i j m) where
-  ask = get
-  local = undefined
 
 evalStateIx :: Monad m => StateIx i j m x -> i -> m x
 evalStateIx m i = fst <$> runStateIx m i

From 42b14322e1dfb2aeb68251025bb60f7aa5ace0f6 Mon Sep 17 00:00:00 2001
From: Eitan Chatav <eitan.chatav@gmail.com>
Date: Mon, 17 Nov 2025 17:19:48 -0800
Subject: [PATCH 10/19] Update State.hs

---
 src/Control/Monad/Trans/Indexed/State.hs | 14 +++++++++++++-
 1 file changed, 13 insertions(+), 1 deletion(-)

diff --git a/src/Control/Monad/Trans/Indexed/State.hs b/src/Control/Monad/Trans/Indexed/State.hs
index 11b80ab..79ff3e5 100644
--- a/src/Control/Monad/Trans/Indexed/State.hs
+++ b/src/Control/Monad/Trans/Indexed/State.hs
@@ -17,11 +17,13 @@ module Control.Monad.Trans.Indexed.State
   , fromStateT
     -- * Reader
   , IxMonadTransReader (..)
+  , ReaderIx
   , ReadStx (..)
     -- * Codensity
   , CodensityIx (..)
   , liftCodensityIx
   , lowerCodensityIx
+  , fromStateIx
   ) where
 
 import Control.Applicative
@@ -30,6 +32,7 @@ import Control.Monad.Reader
 import Control.Monad.State
 import Control.Monad.Trans.Indexed
 import Control.Monad.Trans.Indexed.Free
+import Control.Monad.Trans.Indexed.Free.Wrap
 
 newtype StateIx i j m x = StateIx {runStateIx :: i -> m (x, j)}
   deriving Functor
@@ -88,12 +91,18 @@ liftCodensityIx
   => t i j m a -> CodensityIx t i j m a
 liftCodensityIx m = CodensityIx $ \h -> bindIx h m
 
+fromStateIx :: Monad m => StateIx i j m x -> CodensityIx ReaderIx i j m x
+fromStateIx (StateIx f) = get & bindIx
+  (bindIx (\(x,j) -> putIx j & thenIx (return x)) . lift . f)
+
 class
   ( IxMonadTrans t
   , forall m i j r. (Monad m, i ~ j, j ~ r) => MonadReader r (t i j m)
   ) => IxMonadTransReader t where
   localIx :: Monad m => (i -> h) -> t h j m a -> t i j m a
 
+type ReaderIx = FreeIx (Ixer ReadStx)
+
 data ReadStx s t x where AskStx :: ReadStx s s s
 
 instance IxMonadTrans t => IxMonadTrans (CodensityIx t) where
@@ -128,4 +137,7 @@ instance (s ~ t, Monad m, IxMonadTransFree freeIx)
     local = localIx
 instance IxMonadTransFree freeIx
   => IxMonadTransReader (freeIx (Ixer ReadStx)) where
-    localIx f = lowerCodensityIx . (\m -> bindIx (thenIx m . putIx . f) get) . liftCodensityIx
+    localIx f
+      = lowerCodensityIx
+      . (\m -> bindIx (thenIx m . putIx . f) get)
+      . liftCodensityIx

From e622d859046388e5e3908fec2b760a75d764b5f5 Mon Sep 17 00:00:00 2001
From: Eitan Chatav <eitan.chatav@gmail.com>
Date: Mon, 17 Nov 2025 17:25:49 -0800
Subject: [PATCH 11/19] Update State.hs

---
 src/Control/Monad/Trans/Indexed/State.hs | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/Control/Monad/Trans/Indexed/State.hs b/src/Control/Monad/Trans/Indexed/State.hs
index 79ff3e5..c2c844d 100644
--- a/src/Control/Monad/Trans/Indexed/State.hs
+++ b/src/Control/Monad/Trans/Indexed/State.hs
@@ -67,6 +67,7 @@ class
   ( IxMonadTrans t
   , forall m i j s. (Monad m, i ~ j, j ~ s) => MonadState s (t i j m)
   ) => IxMonadTransState t where
+  {-# MINIMAL putIx | stateIx #-}
   putIx :: Monad m => j -> t i j m ()
   putIx s = stateIx (\_ -> ((), s))
   modifyIx :: Monad m => (i -> j) -> t i j m ()

From b7a3e969a26bb4291f1269469d5bce8b10911a19 Mon Sep 17 00:00:00 2001
From: Eitan Chatav <eitan.chatav@gmail.com>
Date: Mon, 17 Nov 2025 18:06:30 -0800
Subject: [PATCH 12/19] Update State.hs

---
 src/Control/Monad/Trans/Indexed/State.hs | 26 +++++++++++++++++++++---
 1 file changed, 23 insertions(+), 3 deletions(-)

diff --git a/src/Control/Monad/Trans/Indexed/State.hs b/src/Control/Monad/Trans/Indexed/State.hs
index c2c844d..2788569 100644
--- a/src/Control/Monad/Trans/Indexed/State.hs
+++ b/src/Control/Monad/Trans/Indexed/State.hs
@@ -18,12 +18,16 @@ module Control.Monad.Trans.Indexed.State
     -- * Reader
   , IxMonadTransReader (..)
   , ReaderIx
+  , runReaderIx
+  , evalReaderIx
+  , execReaderIx
   , ReadStx (..)
     -- * Codensity
   , CodensityIx (..)
   , liftCodensityIx
   , lowerCodensityIx
   , fromStateIx
+  , toStateIx
   ) where
 
 import Control.Applicative
@@ -65,7 +69,7 @@ fromStateT (StateT f) = StateIx f
 
 class
   ( IxMonadTrans t
-  , forall m i j s. (Monad m, i ~ j, j ~ s) => MonadState s (t i j m)
+  , forall m s i j. (Monad m, s ~ i, i ~ j) => MonadState s (t i j m)
   ) => IxMonadTransState t where
   {-# MINIMAL putIx | stateIx #-}
   putIx :: Monad m => j -> t i j m ()
@@ -96,11 +100,27 @@ fromStateIx :: Monad m => StateIx i j m x -> CodensityIx ReaderIx i j m x
 fromStateIx (StateIx f) = get & bindIx
   (bindIx (\(x,j) -> putIx j & thenIx (return x)) . lift . f)
 
+toStateIx :: Monad m => CodensityIx ReaderIx i j m x -> StateIx i j m x
+toStateIx = StateIx . runReaderIx . lowerCodensityIx
+
+runReaderIx :: Monad m => ReaderIx i j m x -> i -> m (x, j)
+runReaderIx (FreeIx m) i = do
+  wrapped <- m
+  case wrapped of
+    Unwrap x -> return (x,i)
+    Wrap (Ixer f AskStx) -> runReaderIx (f i) i
+
+evalReaderIx :: Monad m => ReaderIx i j m x -> i -> m x
+evalReaderIx m i = fst <$> runReaderIx m i
+
+execReaderIx :: Monad m => ReaderIx i j m x -> i -> m j
+execReaderIx m i = snd <$> runReaderIx m i
+
 class
   ( IxMonadTrans t
-  , forall m i j r. (Monad m, i ~ j, j ~ r) => MonadReader r (t i j m)
+  , forall m r i j. (Monad m, r ~ i, i ~ j) => MonadReader r (t i j m)
   ) => IxMonadTransReader t where
-  localIx :: Monad m => (i -> h) -> t h j m a -> t i j m a
+  localIx :: Monad m => (i -> r) -> t r j m a -> t i j m a
 
 type ReaderIx = FreeIx (Ixer ReadStx)
 

From 2773e67d6ee63f042d979a19515e46c3f2bb1911 Mon Sep 17 00:00:00 2001
From: Eitan Chatav <eitan.chatav@gmail.com>
Date: Mon, 17 Nov 2025 18:14:09 -0800
Subject: [PATCH 13/19] Update State.hs

---
 src/Control/Monad/Trans/Indexed/State.hs | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/src/Control/Monad/Trans/Indexed/State.hs b/src/Control/Monad/Trans/Indexed/State.hs
index 2788569..9298d14 100644
--- a/src/Control/Monad/Trans/Indexed/State.hs
+++ b/src/Control/Monad/Trans/Indexed/State.hs
@@ -21,6 +21,8 @@ module Control.Monad.Trans.Indexed.State
   , runReaderIx
   , evalReaderIx
   , execReaderIx
+  , toReaderT
+  , fromReaderT
   , ReadStx (..)
     -- * Codensity
   , CodensityIx (..)
@@ -116,6 +118,14 @@ evalReaderIx m i = fst <$> runReaderIx m i
 execReaderIx :: Monad m => ReaderIx i j m x -> i -> m j
 execReaderIx m i = snd <$> runReaderIx m i
 
+toReaderT :: Monad m => ReaderIx i i m x -> ReaderT i m x
+toReaderT = ReaderT . evalReaderIx
+
+fromReaderT :: Monad m => ReaderT i m x -> ReaderIx i i m x
+fromReaderT (ReaderT f) = do
+  i <- ask
+  lift (f i)
+
 class
   ( IxMonadTrans t
   , forall m r i j. (Monad m, r ~ i, i ~ j) => MonadReader r (t i j m)

From 99e3550970344dbbac1273b8871a1f2b8e9de5de Mon Sep 17 00:00:00 2001
From: Eitan Chatav <eitan.chatav@gmail.com>
Date: Mon, 17 Nov 2025 18:23:29 -0800
Subject: [PATCH 14/19] Update State.hs

---
 src/Control/Monad/Trans/Indexed/State.hs | 1 -
 1 file changed, 1 deletion(-)

diff --git a/src/Control/Monad/Trans/Indexed/State.hs b/src/Control/Monad/Trans/Indexed/State.hs
index 9298d14..b0c6f06 100644
--- a/src/Control/Monad/Trans/Indexed/State.hs
+++ b/src/Control/Monad/Trans/Indexed/State.hs
@@ -161,7 +161,6 @@ instance (i ~ j, IxMonadTransReader t, Monad m)
   put = putIx
 instance IxMonadTransReader t => IxMonadTransState (CodensityIx t) where
   putIx s = CodensityIx (localIx (const s) . ($ ()))
-
 instance (s ~ t, Monad m, IxMonadTransFree freeIx)
   => MonadReader s (freeIx (Ixer ReadStx) s t m) where
     ask = liftFreerIx AskStx

From aab452e887bf469aaae793e98a9ab4019be152db Mon Sep 17 00:00:00 2001
From: Eitan Chatav <eitan.chatav@gmail.com>
Date: Mon, 17 Nov 2025 18:24:45 -0800
Subject: [PATCH 15/19] Update Free.hs

---
 src/Control/Monad/Trans/Indexed/Free.hs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Control/Monad/Trans/Indexed/Free.hs b/src/Control/Monad/Trans/Indexed/Free.hs
index f8d9c9d..c2907c4 100644
--- a/src/Control/Monad/Trans/Indexed/Free.hs
+++ b/src/Control/Monad/Trans/Indexed/Free.hs
@@ -112,7 +112,7 @@ type IxFunctor
 type IxFunctor f = forall i j. Functor (f i j)
 
 {- |
-`Ixer` is the free `IxFunctor`. It's a left Kan extension.
+`Ixer` is the free `IxFunctor`.
 Combining `IxMonadTransFree` with `Ixer` as demonstrated in the above example,
 gives the "freer" `IxMonadTrans`, modeled on this
 [Oleg Kiselyov explanation]

From 24df74d1b43508f7c13ac0f20bbc983a3f5eb9d0 Mon Sep 17 00:00:00 2001
From: Eitan Chatav <eitan.chatav@gmail.com>
Date: Mon, 17 Nov 2025 18:33:35 -0800
Subject: [PATCH 16/19] Update State.hs

---
 src/Control/Monad/Trans/Indexed/State.hs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Control/Monad/Trans/Indexed/State.hs b/src/Control/Monad/Trans/Indexed/State.hs
index b0c6f06..78e43b9 100644
--- a/src/Control/Monad/Trans/Indexed/State.hs
+++ b/src/Control/Monad/Trans/Indexed/State.hs
@@ -118,7 +118,7 @@ evalReaderIx m i = fst <$> runReaderIx m i
 execReaderIx :: Monad m => ReaderIx i j m x -> i -> m j
 execReaderIx m i = snd <$> runReaderIx m i
 
-toReaderT :: Monad m => ReaderIx i i m x -> ReaderT i m x
+toReaderT :: Monad m => ReaderIx i j m x -> ReaderT i m x
 toReaderT = ReaderT . evalReaderIx
 
 fromReaderT :: Monad m => ReaderT i m x -> ReaderIx i i m x

From eca0297728d25defb403090702d0b577b1e1d572 Mon Sep 17 00:00:00 2001
From: Eitan Chatav <eitan.chatav@gmail.com>
Date: Mon, 17 Nov 2025 18:45:14 -0800
Subject: [PATCH 17/19] indexed-do

---
 indexed-transformers.cabal               |  1 +
 package.yaml                             |  1 +
 src/Control/Monad/Trans/Indexed/State.hs | 17 ++++++++++++-----
 3 files changed, 14 insertions(+), 5 deletions(-)

diff --git a/indexed-transformers.cabal b/indexed-transformers.cabal
index 263865a..b673bf1 100644
--- a/indexed-transformers.cabal
+++ b/indexed-transformers.cabal
@@ -49,6 +49,7 @@ library
       LambdaCase
       MultiParamTypeClasses
       PolyKinds
+      QualifiedDo
       QuantifiedConstraints
       RankNTypes
       StandaloneKindSignatures
diff --git a/package.yaml b/package.yaml
index e78950d..09a5a70 100644
--- a/package.yaml
+++ b/package.yaml
@@ -39,6 +39,7 @@ default-extensions:
 - LambdaCase
 - MultiParamTypeClasses
 - PolyKinds
+- QualifiedDo
 - QuantifiedConstraints
 - RankNTypes
 - StandaloneKindSignatures
diff --git a/src/Control/Monad/Trans/Indexed/State.hs b/src/Control/Monad/Trans/Indexed/State.hs
index 78e43b9..101f02e 100644
--- a/src/Control/Monad/Trans/Indexed/State.hs
+++ b/src/Control/Monad/Trans/Indexed/State.hs
@@ -37,6 +37,7 @@ import Control.Monad
 import Control.Monad.Reader
 import Control.Monad.State
 import Control.Monad.Trans.Indexed
+import qualified Control.Monad.Trans.Indexed.Do as Ix
 import Control.Monad.Trans.Indexed.Free
 import Control.Monad.Trans.Indexed.Free.Wrap
 
@@ -79,8 +80,11 @@ class
   modifyIx :: Monad m => (i -> j) -> t i j m ()
   modifyIx f = stateIx (\i -> ((), f i))
   stateIx :: Monad m => (i -> (a,j)) -> t i j m a
-  stateIx f =
-    bindIx (\s -> let ~(a, s') = f s in thenIx (return a) (putIx s')) get
+  stateIx f = Ix.do
+    s <- get
+    let ~(a, s') = f s
+    putIx s'
+    return a
 instance IxMonadTransState StateIx where
   stateIx f = StateIx (return . f)
 
@@ -99,8 +103,11 @@ liftCodensityIx
 liftCodensityIx m = CodensityIx $ \h -> bindIx h m
 
 fromStateIx :: Monad m => StateIx i j m x -> CodensityIx ReaderIx i j m x
-fromStateIx (StateIx f) = get & bindIx
-  (bindIx (\(x,j) -> putIx j & thenIx (return x)) . lift . f)
+fromStateIx (StateIx f) = Ix.do
+  i <- get
+  (x,j) <- lift (f i)
+  putIx j
+  return x
 
 toStateIx :: Monad m => CodensityIx ReaderIx i j m x -> StateIx i j m x
 toStateIx = StateIx . runReaderIx . lowerCodensityIx
@@ -169,5 +176,5 @@ instance IxMonadTransFree freeIx
   => IxMonadTransReader (freeIx (Ixer ReadStx)) where
     localIx f
       = lowerCodensityIx
-      . (\m -> bindIx (thenIx m . putIx . f) get)
+      . (\m -> Ix.do {i <- get; putIx (f i); m})
       . liftCodensityIx

From 784f4e22c97daebd1a24eaa1ae81ee4e1141dc68 Mon Sep 17 00:00:00 2001
From: Eitan Chatav <eitan.chatav@gmail.com>
Date: Mon, 17 Nov 2025 19:03:58 -0800
Subject: [PATCH 18/19] Update State.hs

---
 src/Control/Monad/Trans/Indexed/State.hs | 20 ++++++++++----------
 1 file changed, 10 insertions(+), 10 deletions(-)

diff --git a/src/Control/Monad/Trans/Indexed/State.hs b/src/Control/Monad/Trans/Indexed/State.hs
index 101f02e..bd502e8 100644
--- a/src/Control/Monad/Trans/Indexed/State.hs
+++ b/src/Control/Monad/Trans/Indexed/State.hs
@@ -112,6 +112,16 @@ fromStateIx (StateIx f) = Ix.do
 toStateIx :: Monad m => CodensityIx ReaderIx i j m x -> StateIx i j m x
 toStateIx = StateIx . runReaderIx . lowerCodensityIx
 
+class
+  ( IxMonadTrans t
+  , forall m r i j. (Monad m, r ~ i, i ~ j) => MonadReader r (t i j m)
+  ) => IxMonadTransReader t where
+  localIx :: Monad m => (i -> r) -> t r j m a -> t i j m a
+
+type ReaderIx = FreeIx (Ixer ReadStx)
+
+data ReadStx s t x where AskStx :: ReadStx s s s
+
 runReaderIx :: Monad m => ReaderIx i j m x -> i -> m (x, j)
 runReaderIx (FreeIx m) i = do
   wrapped <- m
@@ -133,16 +143,6 @@ fromReaderT (ReaderT f) = do
   i <- ask
   lift (f i)
 
-class
-  ( IxMonadTrans t
-  , forall m r i j. (Monad m, r ~ i, i ~ j) => MonadReader r (t i j m)
-  ) => IxMonadTransReader t where
-  localIx :: Monad m => (i -> r) -> t r j m a -> t i j m a
-
-type ReaderIx = FreeIx (Ixer ReadStx)
-
-data ReadStx s t x where AskStx :: ReadStx s s s
-
 instance IxMonadTrans t => IxMonadTrans (CodensityIx t) where
   joinIx (CodensityIx k) =
     CodensityIx $ \f -> k $ \(CodensityIx g) -> g f

From 4c5d389f1adfd5cd0ae236f7d21bde6e4161869e Mon Sep 17 00:00:00 2001
From: Eitan Chatav <eitan.chatav@gmail.com>
Date: Mon, 17 Nov 2025 20:34:23 -0800
Subject: [PATCH 19/19] Update State.hs

---
 src/Control/Monad/Trans/Indexed/State.hs | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

diff --git a/src/Control/Monad/Trans/Indexed/State.hs b/src/Control/Monad/Trans/Indexed/State.hs
index bd502e8..d973fd0 100644
--- a/src/Control/Monad/Trans/Indexed/State.hs
+++ b/src/Control/Monad/Trans/Indexed/State.hs
@@ -23,7 +23,7 @@ module Control.Monad.Trans.Indexed.State
   , execReaderIx
   , toReaderT
   , fromReaderT
-  , ReadStx (..)
+  , AskIx (..)
     -- * Codensity
   , CodensityIx (..)
   , liftCodensityIx
@@ -118,16 +118,16 @@ class
   ) => IxMonadTransReader t where
   localIx :: Monad m => (i -> r) -> t r j m a -> t i j m a
 
-type ReaderIx = FreeIx (Ixer ReadStx)
+type ReaderIx = FreeIx (Ixer AskIx)
 
-data ReadStx s t x where AskStx :: ReadStx s s s
+data AskIx i j x where AskIx :: AskIx x x x
 
 runReaderIx :: Monad m => ReaderIx i j m x -> i -> m (x, j)
 runReaderIx (FreeIx m) i = do
   wrapped <- m
   case wrapped of
     Unwrap x -> return (x,i)
-    Wrap (Ixer f AskStx) -> runReaderIx (f i) i
+    Wrap (Ixer f AskIx) -> runReaderIx (f i) i
 
 evalReaderIx :: Monad m => ReaderIx i j m x -> i -> m x
 evalReaderIx m i = fst <$> runReaderIx m i
@@ -169,11 +169,11 @@ instance (i ~ j, IxMonadTransReader t, Monad m)
 instance IxMonadTransReader t => IxMonadTransState (CodensityIx t) where
   putIx s = CodensityIx (localIx (const s) . ($ ()))
 instance (s ~ t, Monad m, IxMonadTransFree freeIx)
-  => MonadReader s (freeIx (Ixer ReadStx) s t m) where
-    ask = liftFreerIx AskStx
+  => MonadReader s (freeIx (Ixer AskIx) s t m) where
+    ask = liftFreerIx AskIx
     local = localIx
 instance IxMonadTransFree freeIx
-  => IxMonadTransReader (freeIx (Ixer ReadStx)) where
+  => IxMonadTransReader (freeIx (Ixer AskIx)) where
     localIx f
       = lowerCodensityIx
       . (\m -> Ix.do {i <- get; putIx (f i); m})