Indexed Kan Extension

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
 
@@ -33,6 +33,7 @@ library
       Control.Monad.Trans.Indexed.Free
       Control.Monad.Trans.Indexed.Free.Fold
       Control.Monad.Trans.Indexed.Free.Wrap
+      Control.Monad.Trans.Indexed.Kan
       Control.Monad.Trans.Indexed.State
       Control.Monad.Trans.Indexed.Writer
   other-modules:
@@ -49,6 +50,7 @@ library
       LambdaCase
       MultiParamTypeClasses
       PolyKinds
+      QualifiedDo
       QuantifiedConstraints
       RankNTypes
       StandaloneKindSignatures

package.yaml

@@ -39,6 +39,7 @@ default-extensions:
 - LambdaCase
 - MultiParamTypeClasses
 - PolyKinds
+- QualifiedDo
 - QuantifiedConstraints
 - RankNTypes
 - StandaloneKindSignatures

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`.
+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

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
@@ -27,25 +28,29 @@ instance (IxFunctor f, Monad m)
       Wrap fm -> Wrap $ fmap (fmap f) fm
 
 newtype FreeIx f i j m x = FreeIx {runFreeIx :: m (WrapIx f i j m x)}
+instance IxFunctor f
+  => IxMonadTrans (FreeIx f) where
+    joinIx (FreeIx mm) = FreeIx $ mm >>= \case
+      Unwrap (FreeIx m) -> m
+      Wrap fm -> return $ Wrap $ fmap joinIx fm
 instance (IxFunctor f, Monad m)
   => Functor (FreeIx f i j m) where
     fmap f (FreeIx m) = FreeIx $ fmap (fmap f) m
 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
     (>>=) = flip bindIx
 instance (IxFunctor f, i ~ j)
   => MonadTrans (FreeIx f i j) where
     lift = FreeIx . fmap Unwrap
-instance IxFunctor f
-  => IxMonadTrans (FreeIx f) where
-    joinIx (FreeIx mm) = FreeIx $ mm >>= \case
-      Unwrap (FreeIx m) -> m
-      Wrap fm -> return $ Wrap $ fmap joinIx fm
 instance
   ( IxFunctor f
   , Monad m

src/Control/Monad/Trans/Indexed/Kan.hs

@@ -0,0 +1,51 @@
+{- |
+Module      :  Control.Monad.Trans.Indexed.Kan
+Copyright   :  (C) 2024 Eitan Chatav
+License     :  BSD 3-Clause License (see the file LICENSE)
+Maintainer  :  Eitan Chatav <eitan.chatav@gmail.com>
+
+-}
+
+module Control.Monad.Trans.Indexed.Kan
+  ( CodensityIx (..)
+  ) where
+
+import Control.Applicative
+import Control.Monad
+import Control.Monad.Trans
+import Control.Monad.Trans.Indexed
+import Control.Monad.Trans.Indexed.State
+
+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)

src/Control/Monad/Trans/Indexed/State.hs

@@ -8,19 +8,21 @@ The state indexed monad transformer.
 -}
 
 module Control.Monad.Trans.Indexed.State
-  ( StateIx (..)
+  ( -- * State
+    IxMonadTransState (..)
+  , StateIx (..)
   , evalStateIx
   , execStateIx
-  , modifyIx
-  , putIx
   , toStateT
   , fromStateT
   ) where
 
+import Control.Monad.Reader
 import Control.Monad.State
 import Control.Monad.Trans.Indexed
+import qualified Control.Monad.Trans.Indexed.Do as Ix
 
-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
@@ -43,14 +45,48 @@ 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 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 ()
+  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 = Ix.do
+    s <- get
+    let ~(a, s') = f s
+    putIx s'
+    return a
+instance IxMonadTransState StateIx where
+
+data KanStateIx i j m a where
+  KanStateIx
+    :: {runKanStateIx :: forall x. (a -> (i -> k) -> ReaderT i m x) -> StateIx j k m x}
+    -> KanStateIx i j m a
+instance Functor (KanStateIx i j m) where
+  fmap f (KanStateIx k) = KanStateIx $ \g -> k (g . f)
+instance IxMonadTrans KanStateIx where
+  joinIx (KanStateIx k) =
+    KanStateIx $ \f ->
+      k $ \(KanStateIx g) -> g _
+instance (i ~ j, Monad m) => Applicative (KanStateIx i j m) where
+  pure x = KanStateIx $ \k -> do
+    i <- get
+    lift $ runReaderT (k x id) i
+  (<*>) = apIx
+instance (i ~ j, Monad m) => Monad (KanStateIx i j m) where
+  return = pure
+  (>>=) = flip bindIx
+instance i ~ j => MonadTrans (KanStateIx i j) where
+  lift m = KanStateIx $ _
+-- instance (i ~ j, Monad m) => MonadState i (StateIx i j m) where
+--   state f = StateIx (return . f)