monad-actions 1.0.0.0 → 2.0.0.0

raw patch · 8 files changed

+581/−192 lines, 8 filesdep +constraintsPVP ok

version bump matches the API change (PVP)

Dependencies added: constraints

API changes (from Hackage documentation)

Files

• CHANGELOG.md +4/−0
• README.md +10/−0
• monad-actions.cabal +7/−3
• src/Control/Monad/Action.hs +11/−158
• src/Control/Monad/Action/Records.hs +323/−0
• src/Control/Monad/Action/TH.hs +48/−27
• src/Control/Monad/TransformerStack.hs +169/−0
• test/Main.hs +9/−4

@@ -1,5 +1,9 @@ # Revision history for monad-actions +## 2.0.0.0 -- 2026-02-22++* This version adds a new record-based implementation of monad actions, meant to avoid overlapping instances.+ ## 1.0.0.0 -- 2026-01-27  * For any monad m, m acts on every transformer stack whose base is m.

@@ -0,0 +1,10 @@+Left or right actions of a monad on a functor.++See [this blog post](https://stringdiagram.com/2023/04/23/monad-actions/) by Dan Marsden for an introduction to monad actions.++This package provides two implementations of monad actions.+The simpler one uses the `LeftModule`, `RightModule`, and `BiModule` classes defined in `Control.Monad.Action`,+and can be used with the `QualifiedDo` extension by qualifying the `do` blocks with either `Control.Monad.Action.Right` or `Control.Monad.Action.Left`.+However, it uses incoherent instances.+The second implementation, designed to avoid incoherent and overlapping instances, is defined in `Control.Monad.Action.Records`, and uses the `LeftAction`, `RightAtion`, and `BiAction` types.+It is meant to be used with `RecordWildCards` and `RebindableSyntax` and/or `OverloadedRecordDot`.

@@ -8,8 +8,8 @@ --       +-+------- breaking API changes --       | | +----- non-breaking API additions --       | | | +--- code changes with no API change-version: 1.0.0.0-synopsis: Left or right actions of a monad on a functor+version: 2.0.0.0+synopsis: Actions of monads on functors description:   This package defines classes for left and right actions of   monads on functors.  It also includes modules for using@@ -26,6 +26,7 @@ homepage: https://codeberg.org/noiioiu/monad-actions build-type: Simple extra-doc-files: CHANGELOG.md+                 README.md  common warnings   ghc-options: -Wall@@ -38,8 +39,10 @@   import: warnings   exposed-modules:     Control.Monad.Action+    Control.Monad.TransformerStack     Control.Monad.Action.Left     Control.Monad.Action.Right+    Control.Monad.Action.Records    other-modules: Control.Monad.Action.TH   build-depends:@@ -50,8 +53,9 @@    mtl >= 2.3.1 && < 2.4,    template-haskell >= 2.22.0 && < 2.23,    transformers >= 0.6.1 && < 0.7,+   constraints >= 0.14.4 && < 0.15, -    +    hs-source-dirs: src   default-language: GHC2021

@@ -1,12 +1,12 @@+{-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE DataKinds #-}-{-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE UndecidableInstances #-}  -- | Given a monad \(M\) on a category \(\mathcal{D}\) with unit \(\eta\) and --     multiplication \(\mu\) and a functor \(F\) from \(\mathcal{C}\) to \(\mathcal{D}\),---     a left monad action of \(M\) on \(F\) is a natural transformation \(\nu: M \circ F \to F\)---     such that the following two laws hold:+--     a left (or outer) monad action of \(M\) on \(F\) is a natural transformation+--     \(\nu: M \circ F \to F\) such that the following two laws hold: -- --     * \(\nu \cdot (\eta \circ F) = \mathrm{id}_F\) --     * \(\nu \cdot (\mu \circ F) = \nu \cdot (M \circ \nu)\)@@ -14,12 +14,12 @@ --     We also say that \(F\) is a left module over \(M\).  In the case --     \(\mathcal{C} = \mathcal{D}\), a left monad module is a left monoid module --     object in the category of endofunctors on \(\mathcal{C}\).  We may also---     call \(\alpha\) the scalar multiplication of the module by the monad, by analogy+--     call \(\nu\) the scalar multiplication of the module by the monad, by analogy --     with ring modules, which are monoid module objects in the category of abelian groups --     with tensor product as the monoidal product (rings are just monoid objects in this --     category). -----     Right monad actions are defined similarly.+--     Right (or inner) monad actions are defined similarly. -- --     See [this blog post](https://stringdiagram.com/2023/04/23/monad-actions/) by Dan Marsden --     or the paper /Modules over monads and their algebras/ by Piróg, Wu, and Gibbons.@@ -27,13 +27,10 @@   ( LeftModule (..),     RightModule (..),     BiModule (..),-    LiftStack (..),   ) where  import Control.Monad (join)-import Control.Monad.Action.TH-import Control.Monad.Co () import Control.Monad.Codensity (Codensity (..)) import Control.Monad.Error.Class (MonadError (..), liftEither) import Control.Monad.IO.Class@@ -41,21 +38,11 @@ import Control.Monad.Reader.Class (MonadReader (..)) import Control.Monad.State (State, runState) import Control.Monad.State.Class (MonadState (..))-import Control.Monad.Trans ()-import Control.Monad.Trans.Accum ()-import Control.Monad.Trans.Compose () import Control.Monad.Trans.Except (ExceptT (..), runExceptT)-import Control.Monad.Trans.Free ()-import Control.Monad.Trans.Iter () import Control.Monad.Trans.Maybe (MaybeT (..)) import Control.Monad.Trans.Reader (Reader, runReader)-import Control.Monad.Trans.Select ()-import Control.Monad.Trans.State.Lazy qualified as L ()-import Control.Monad.Trans.State.Strict qualified as S () import Control.Monad.Trans.Writer (Writer, runWriter)-import Control.Monad.Trans.Writer.CPS qualified as C ()-import Control.Monad.Trans.Writer.Lazy qualified as L ()-import Control.Monad.Trans.Writer.Strict qualified as S ()+import Control.Monad.TransformerStack import Control.Monad.Writer.Class (MonadWriter (..)) import Data.Functor.Compose (Compose (..)) import Data.List.NonEmpty qualified as NE (NonEmpty, toList)@@ -103,149 +90,15 @@     f a   bijoin = rjoin . ljoin --- | All @'LiftStack'@ instances are defined inductively using @'Control.Monad.Trans.Class.MonadTrans'@.---   @'Control.Monad.Trans.Class.MonadTrans'@ instances are required to satisfy these laws, which state---   that @'Control.Monad.Trans.Class.lift'@ is a monad homomorphism:------   * @'Control.Monad.Trans.Class.lift' '.' 'pure' = 'pure'@------   * @'Control.Monad.Trans.Class.lift' (m '>>=' f) = 'Control.Monad.Trans.Class.lift' m '>>=' ('Control.Monad.Trans.Class.lift' '.' f)@------   Restating the second law in terms of @'join'@:------   * @'Control.Monad.Trans.Class.lift' '.' 'join' = 'join' '.' 'fmap' 'Control.Monad.Trans.Class.lift' '.' 'Control.Monad.Trans.Class.lift'@------   Because the composition of two monad homomorphisms is a monad homomorphism, @'liftStack'@ also satisfies these laws:------   * @'liftStack' '.' 'pure' = 'pure'@------   * @'liftStack' '.' 'join' = 'join' '.' 'fmap' 'liftStack' '.' 'liftStack'@------   The left monad action laws can now be easily proved using string diagrams.---   Functors compose from top to bottom, natural transformations from left to right,---   @───@ represents @t m@, @┈┈┈@ represents @m@, @├@ represents @'pure'@ or---   @'join'@ depending on the number of inputs, and @┈┈┈►───@ represents @'liftStack'@.---   The @'LiftStack'@ laws as string diagrams are:------   > ├┈┈┈►───  = ├──────------   > ┈┈┈┐            ┈┈┈►───┐---   >    ├┈┈┈►───  =         ├───---   > ┈┈┈┘            ┈┈┈►───┘------   and the diagram for @'ljoin'@ is:------   > ┈┈►──┐---   >      ├───---   > ─────┘------   To prove the identity law:------   >   ├┈┈►──┐          ├─────┐---   >         ├───  =          ├───  =  ──────---   > ────────┘        ────────┘------   In other words,------   @   'ljoin' '.' 'pure'---   = 'join' '.' 'liftStack' '.' 'pure'---   = 'join' '.' 'pure'---   = 'id'@------   To prove associativity:------   > ┈┈┈┐              ┈┈►──┐---   >    ├┈┈►─┐              ├──┐         ┈┈┈┈┈┈┈►─┐---   > ┈┈┈┘    ├────  =  ┈┈►──┘  ├────  =  ┈┈►──┐   ├────---   > ────────┘         ────────┘              ├───┘---   >                                     ─────┘------   In other words,------   @  'ljoin' '.' 'join'---   = 'join' '.' 'liftStack' '.' 'join'---   = 'join' '.' 'join' '.' 'fmap' 'liftStack' '.' 'liftStack'---   = 'join' '.' 'fmap' 'join' '.' 'fmap' 'liftStack' '.' 'liftStack'---   = 'join' '.' 'fmap' ('join' '.' 'liftStack') '.' 'liftStack'---   = 'join' '.' 'liftStack' '.' 'fmap' ('join' '.' 'liftStack')---   = 'ljoin' '.' 'fmap' 'ljoin'@------   We can prove the right module laws using string diagrams in the same way.------   The diagram for @'rjoin'@ is:------   > ─────┐---   >      ├───---   > ┈┈►──┘------   To prove the identity law:------   > ────────┐        ────────┐---   >         ├───  =          ├───  =  ──────---   >   ├┈┈►──┘          ├─────┘------   In other words,------   @   'rjoin' '.' 'fmap' 'pure'---   = 'join' '.' 'fmap' 'liftStack' , 'pure'---   = 'join' '.' 'fmap' 'liftStack' , 'fmap' 'pure'---   = 'join' '.' 'fmap' ('liftStack' , 'pure')---   = 'join' '.' 'fmap' 'pure'---   = 'id'@------   To prove associativity:------   >                                      ─────┐---   > ────────┐         ─────────┐              ├───┐---   > ┈┈┈┐    ├────  =  ┈┈►──┐   ├────  =  ┈┈►──┘   ├────---   >    ├┈┈►─┘              ├───┘         ┈┈┈┈┈┈┈►─┘---   > ┈┈┈┘              ┈┈►──┘------   In other words,------   @  'rjoin' '.' 'fmap' 'join'---   = 'join' '.' 'fmap' 'liftStack' '.' 'fmap' 'join'---   = 'join' '.' 'fmap' ('liftStack' '.' 'join')---   = 'join' '.' 'fmap' ('join' '.' 'fmap' 'liftStack' '.' 'liftStack')---   = 'join' '.' 'fmap' 'join' '.' 'fmap' ('fmap' 'liftStack' '.' 'liftStack')---   = 'join' '.' 'join' '.' 'fmap' ('fmap' 'liftStack') '.' 'fmap' ('liftStack')---   = 'join' '.' 'fmap' 'liftStack' '.' 'join' '.' 'fmap' 'liftStack'---   = 'rjoin' '.' 'rjoin'@------   The bimodule law can be proved as follows:------   > ┈┈┈►─┐             ┈┈►─┐---   >      ├───┐             ├───┐          ┈┈┈┈┈┈►─┐---   > ─────┘   ├────  =  ────┘   ├────  =   ────┐   ├────---   > ┈►───────┘         ┈┈┈┈┈┈►─┘              ├───┘---   >                                       ┈┈►─┘------   In other words,------   @  'bijoin'---   = 'join' '.' 'join' '.' 'liftStack' '.' 'fmap' ('fmap' 'liftStack')---   = 'join' '.' 'fmap' 'liftStack' '.' 'join' '.' 'liftStack'---   = 'rjoin' '.' 'ljoin'---   = 'join' '.' 'fmap' 'liftStack' '.' 'join' '.' 'liftStack'---   = 'join' '.' 'fmap' 'join' '.' 'fmap' ('fmap' 'liftStack') '.' 'liftStack'---   = 'join' '.' 'fmap' ('join' '.' 'fmap' 'liftStack') '.' 'liftStack'---   = 'join' '.' 'fmap' 'rjoin' '.' 'liftStack'---   = 'join' '.' 'liftStack' '.' 'fmap' 'rjoin'---   = 'ljoin' '.' 'fmap' 'rjoin'@-class LiftStack m n where-  liftStack :: forall a. m a -> n a--$mkLiftStackInstances--instance {-# OVERLAPS #-} (Monad n, Monad m, LiftStack m n) => LeftModule m n where+instance {-# OVERLAPS #-} (Monad n, Monad m, MonadTransStack m n) => LeftModule m n where   ljoin = join . liftStack   lbind = (>>=) . liftStack -instance {-# OVERLAPS #-} (Monad n, Monad m, LiftStack m n) => RightModule m n where+instance {-# OVERLAPS #-} (Monad n, Monad m, MonadTransStack m n) => RightModule m n where   rjoin = (liftStack =<<)   rbind = flip $ (=<<) . (liftStack .) -instance {-# OVERLAPS #-} (Monad n, Monad m, LiftStack m n) => BiModule m m n+instance {-# OVERLAPS #-} (Monad n, Monad m, MonadTransStack m n) => BiModule m m n  instance {-# INCOHERENT #-} (Functor f) => LeftModule Identity f where ljoin = runIdentity @@ -419,7 +272,7 @@ instance {-# INCOHERENT #-} (MonadState s m) => BiModule (State s) (State s) m  -- | Proof that @f@ is always a left module over @t'Codensity' f@:--- +-- --   * @   'ljoin' ('join' m) --       = 'ljoin' ('Codensity' (\\c -> 'runCodensity' m (\\a -> 'runCodensity' a c))) --       = (\\c -> 'runCodensity' m (\\a -> 'runCodensity' a c)) id@@ -428,7 +281,7 @@ --       = (\\k -> 'runCodensity' m (\\x -> k ('ljoin' x))) 'id' --       = 'ljoin' ('Codensity' (\\k -> 'runCodensity' m (\\x -> k ('ljoin' x)))) --       = 'ljoin' ('fmap' 'ljoin' m)@--- +-- --   * @'ljoin' ('pure' x) = 'ljoin' ('Codensity' (\\x -> k x)) = (\\k -> k x) 'id' = x@ instance (Functor f) => LeftModule (Codensity f) f where   ljoin c = runCodensity c id

@@ -0,0 +1,323 @@+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE DuplicateRecordFields #-}+{-# LANGUAGE MonoLocalBinds #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE RecordWildCards #-}+{-# LANGUAGE NoFieldSelectors #-}++-- | This module should be used with @OverloadedRecordDot@ and/or @RebindableSyntax@ (and @RecordWildCards@).+module Control.Monad.Action.Records where++import Control.Monad qualified as M (Monad (..), join, (=<<))+import Control.Monad.Codensity (Codensity (..))+import Control.Monad.Error.Class (MonadError, liftEither)+import Control.Monad.IO.Class (MonadIO (..))+import Control.Monad.RWS (MonadRWS, RWS, RWST (..), runRWS)+import Control.Monad.Reader (MonadReader (..), Reader, ReaderT (..), runReader)+import Control.Monad.State (MonadState (..), State, StateT (..), runState)+import Control.Monad.Trans.Writer (WriterT (..))+import Control.Monad.TransformerStack+import Control.Monad.Writer (MonadWriter (..), Writer, runWriter)+import Data.Bifunctor (second)+import Data.Constraint (Dict (..))+import Data.Functor.Compose (Compose (..))+import Data.Kind (Constraint, Type)+import Data.List.NonEmpty qualified as NE+import Data.Maybe (maybeToList)+import Prelude hiding ((<*>), (=<<), (>>), (>>=))+import Prelude qualified as P++infixl 1 >>=++infixr 1 =<<++infixl 1 >>++infixr 1 >=>++infixr 1 <=<++infixl 4 <*>++-- | Every @'LeftAction'@ @l@ should satisfy the following laws:+--+-- * @l.'join' '.' 'Control.Monad.join' = l.'join' '.' 'fmap' l.'join'@+--+-- * @l.'join' '.' 'pure' = 'id'@+--+-- All of the operators should match the default implementations in "Control.Monad.Action" and "Control.Monad.Left".+data LeftAction (action :: (Type -> Type) -> (Type -> Type) -> Constraint) where+  LeftAction ::+    { -- | left monad action scalar multiplication+      join :: forall m f a. (action m f) => m (f a) -> f a,+      -- | left monad action bind+      (>>=) :: forall m f a b. (action m f) => m a -> (a -> f b) -> f b,+      -- | left monad action bind with arguments reversed+      (=<<) :: forall m f a b. (action m f) => (a -> f b) -> m a -> f b,+      -- | left to right Kleisli arrow scalar multiplication induced by a left monad action+      (>=>) :: forall m f a b c. (action m f) => (a -> m b) -> (b -> f c) -> a -> f c,+      -- | right to left Kleisli arrow scalar multiplication induced by a left monad action+      (<=<) :: forall m f a b c. (action m f) => (b -> f c) -> (a -> m b) -> a -> f c,+      -- | left monad action sequencing operator+      (>>) :: forall m f a b. (action m f) => m a -> f b -> f b,+      -- | scalar sequential application, used for desugaring applicative do blocks+      (<*>) :: forall m f a b. (action m f) => m (a -> b) -> f a -> f b+    } ->+    LeftAction action++-- | Every @'RightAction'@ @r@ should satisfy the following laws:+--+-- * @r.'join' '.' 'fmap' 'Control.Monad.join' = r.'join' '.' r.'join'@+--+-- * @r.'join' '.' 'fmap' 'pure' = 'id'@+--+-- All of the operators should match the default implementations in "Control.Monad.Action" and "Control.Monad.Right".+data RightAction (action :: (Type -> Type) -> (Type -> Type) -> Constraint) where+  RightAction ::+    { -- | right monad action scalar multiplication+      join :: forall m f a. (action m f) => f (m a) -> f a,+      -- | right monad action bind+      (>>=) :: forall m f a b. (action m f) => f a -> (a -> m b) -> f b,+      -- | right monad action bind with arguments reversed+      (=<<) :: forall m f a b. (action m f) => (a -> m b) -> f a -> f b,+      -- | left to right Kleisli arrow scalar multiplication induced by a right monad action+      (>=>) :: forall m f a b c. (action m f) => (a -> f b) -> (b -> m c) -> a -> f c,+      -- | right to left Kleisli arrow scalar multiplication induced by a right monad action+      (<=<) :: forall m f a b c. (action m f) => (b -> m c) -> (a -> f b) -> a -> f c,+      -- | right monad action sequencing operator+      (>>) :: forall m f a b. (action m f) => f a -> m b -> f b,+      -- | scalar sequential application, used for desugaring applicative do blocks+      (<*>) :: forall m f a b. (action m f) => f (a -> b) -> m a -> f b+    } ->+    RightAction action++-- | Every @'BiAction'@ @b@ should satisfy the following laws, in addition to the laws for left and right actions:+--+-- * @b.'right'.'join' '.' b.'left'.'join' = b.'left'.'join' '.' 'fmap' b.'right'.'join'@+data BiAction (action :: (Type -> Type) -> (Type -> Type) -> Constraint) where+  BiAction ::+    { left :: LeftAction action,+      right :: RightAction action+    } ->+    BiAction action++-- | @'MonadHomomorphism' c@ means that, whenever @c m n@, there is a monad homomorphism @'hom'@ from @m@ to @n@.+class MonadHomomorphism (c :: (Type -> Type) -> (Type -> Type) -> Constraint) where+  hom :: forall m n a. (c m n) => m a -> n a+  mDict :: forall m n. (c m n) => (Dict (Monad m), Dict (Monad n))++-- | Two-sided action induced by a monad homomorphism.+monadMorphAction :: forall action. (MonadHomomorphism action) => BiAction action+monadMorphAction =+  let left =+        let join :: forall m n a. (action m n) => m (n a) -> n a+            join = case mDict @action @m @n of (_, Dict) -> M.join . hom @action+            (>>=) :: forall m n a b. (action m n) => m a -> (a -> n b) -> n b+            (>>=) = case mDict @action @m @n of (_, Dict) -> (P.>>=) . hom @action+            (=<<) :: forall m n a b. (action m n) => (a -> n b) -> m a -> n b+            (=<<) = flip (>>=)+            (>=>) :: forall m n a b c. (action m n) => (a -> m b) -> (b -> n c) -> a -> n c+            f >=> g = \x -> f x >>= g+            (<=<) :: forall m n a b c. (action m n) => (b -> n c) -> (a -> m b) -> a -> n c+            (<=<) = flip (>=>)+            (>>) :: forall m n a b. (action m n) => m a -> n b -> n b+            a >> b = a >>= const b+            (<*>) :: forall m n a b. (action m n) => m (a -> b) -> n a -> n b+            (<*>) = case mDict @action @m @n of (_, Dict) -> (P.<*>) . hom @action+         in LeftAction {..} :: LeftAction action+      right =+        let join :: forall m n a. (action m n) => n (m a) -> n a+            join = case mDict @action @m @n of (_, Dict) -> (hom @action M.=<<)+            (>>=) :: forall m n a b. (action m n) => n a -> (a -> m b) -> n b+            (>>=) = flip (=<<)+            (=<<) :: forall m n a b. (action m n) => (a -> m b) -> n a -> n b+            (=<<) = case mDict @action @m @n of (_, Dict) -> (M.=<<) . (hom @action .)+            (>=>) :: forall m n a b c. (action m n) => (a -> n b) -> (b -> m c) -> a -> n c+            f >=> g = \x -> f x >>= g+            (<=<) :: forall m n a b c. (action m n) => (b -> m c) -> (a -> n b) -> a -> n c+            (<=<) = flip (>=>)+            (>>) :: forall m n a b. (action m n) => n a -> m b -> n b+            a >> b = a >>= const b+            (<*>) :: forall m n a b. (action m n) => n (a -> b) -> m a -> n b+            f <*> x = case mDict @action @m @n of (_, Dict) -> f P.<*> hom @action x+         in RightAction {..} :: RightAction action+   in BiAction {..}++instance MonadHomomorphism MonadTransStack where+  hom = liftStack+  mDict = (Dict, Dict)++transformerStackAction :: BiAction MonadTransStack+transformerStackAction = monadMorphAction++-- | @m ':<:' n@ means that @m@ is a submonad of @n@. @'inject'@ must be a monic monad homomorphism.+class (Monad m, Monad n) => m :<: n where+  inject :: forall a. m a -> n a++instance MonadHomomorphism (:<:) where+  hom = inject+  mDict = (Dict, Dict)++submonadAction :: BiAction (:<:)+submonadAction = monadMorphAction++instance (Monad m) => m :<: m where+  inject = id++-- | A @'Maybe'@ is just a list of length at most 1.+instance Maybe :<: [] where+  inject = maybeToList++-- | A @'Data.List.NonEmpty.NonEmpty'@ is just a list of length at least 1.+instance NE.NonEmpty :<: [] where+  inject = NE.toList++-- | @'ReaderT'@ is just read-only @'StateT'@.+instance (m :<: n) => ReaderT s m :<: StateT s n where+  inject ReaderT {runReaderT} = StateT $ \s -> inject . fmap (,s) $ runReaderT s++-- | @'WriterT'@ is just append-only @'StateT'@.+instance (Monoid s, m :<: n) => WriterT s m :<: StateT s n where+  inject WriterT {runWriterT} = StateT $ \s -> inject @m @n . fmap (second (s <>)) $ runWriterT++-- | @'StateT'@ is just @'RWST'@ that ignores the read-only environment and doesn't append to the output.+instance (Monoid w, m :<: n) => StateT s m :<: RWST r w s n where+  inject StateT {runStateT} = RWST $ \_ s -> inject . fmap (\(a, t) -> (a, t, mempty)) $ runStateT s++-- | @'ReaderT'@ is just @'RWST'@ that ignores the state and doesn't append to the output.+--+--   Note: @'inject' \@('ReaderT' s m) \@('StateT' s n) '.' 'inject' \@('StateT' s n) \@('RWST' s w s k) =/= 'inject' \@('ReaderT' s m) \@('RWST' s w s k)@+instance (Monoid w, m :<: n) => ReaderT r m :<: RWST r w s n where+  inject ReaderT {runReaderT} = RWST $ \r s -> inject . fmap (,s,mempty) $ runReaderT r++-- | @'WriterT'@ is just @'RWST'@ that ignores the environment and state.+--+--   Note: @'inject' \@('WriterT' w m) \@('StateT' w n) '.' 'inject' \@('StateT' w n) \@('RWST' r w w k) =/= 'inject' \@('WriterT' w m) \@('RWST' r w w k)@+instance (Monoid w, m :<: n) => WriterT w m :<: RWST r w s n where+  inject WriterT {runWriterT} = RWST $ \_ s -> inject @m @n . fmap (\(a, w) -> (a, s, w)) $ runWriterT++instance (MonadIO m) => IO :<: m where+  inject = liftIO++instance (MonadState s m) => (State s) :<: m where+  inject = state . runState++instance (MonadReader r m) => (Reader r) :<: m where+  inject = reader . runReader++instance (MonadWriter w m) => (Writer w) :<: m where+  inject = writer . runWriter++instance (MonadRWS r w s m) => (RWS r w s) :<: m where+  inject t =+    ask P.>>= \r ->+      get P.>>= \s ->+        let (a, s', w) = runRWS t r s+         in put s'+              M.>> tell w+              M.>> pure a++instance (MonadError e m) => (Either e) :<: m where+  inject = liftEither++class CodensityAction m f where+  codensityJoin :: forall a. m (f a) -> f a+  codensityBind :: forall a b. m a -> (a -> f b) -> f b+  codensityApply :: forall a b. m (a -> b) -> f a -> f b++codensityAction :: LeftAction CodensityAction+codensityAction =+  let join :: forall m f a. (CodensityAction m f) => m (f a) -> f a+      join = codensityJoin+      (>>=) :: forall m f a b. (CodensityAction m f) => m a -> (a -> f b) -> f b+      (>>=) = codensityBind+      (=<<) :: forall m f a b. (CodensityAction m f) => (a -> f b) -> m a -> f b+      (=<<) = flip codensityBind+      (>=>) :: forall m f a b c. (CodensityAction m f) => (a -> m b) -> (b -> f c) -> a -> f c+      f >=> g = \x -> f x >>= g+      (<=<) :: forall m f a b c. (CodensityAction m f) => (b -> f c) -> (a -> m b) -> a -> f c+      (<=<) = flip (>=>)+      (>>) :: forall m f a b. (CodensityAction m f) => m a -> f b -> f b+      a >> b = a >>= const b+      (<*>) :: forall m f a b. (CodensityAction m f) => m (a -> b) -> f a -> f b+      (<*>) = codensityApply+   in LeftAction {..}++instance (Monad m) => CodensityAction m m where+  codensityJoin = M.join+  codensityBind = (P.>>=)+  codensityApply = (P.<*>)++instance (Functor f) => CodensityAction (Codensity f) f where+  codensityJoin c = runCodensity c id+  a `codensityBind` f = runCodensity (f P.<$> a) id+  fs `codensityApply` xs = fs `codensityBind` flip fmap xs++class (Monad m, Functor f) => LeftCompAction m f where+  leftCompJoin :: forall a. m (f a) -> f a+  leftCompBind :: forall a b. m a -> (a -> f b) -> f b+  leftCompApply :: forall a b. m (a -> b) -> f a -> f b++-- | Left action of any monad @m@ on any composition of functors with @m@ as the outermost component.+leftCompAction :: LeftAction LeftCompAction+leftCompAction =+  let join :: forall m f a. (LeftCompAction m f) => m (f a) -> f a+      join = leftCompJoin+      (>>=) :: forall m f a b. (LeftCompAction m f) => m a -> (a -> f b) -> f b+      (>>=) = leftCompBind+      (=<<) :: forall m f a b. (LeftCompAction m f) => (a -> f b) -> m a -> f b+      (=<<) = flip leftCompBind+      (>=>) :: forall m f a b c. (LeftCompAction m f) => (a -> m b) -> (b -> f c) -> a -> f c+      f >=> g = \x -> f x >>= g+      (<=<) :: forall m f a b c. (LeftCompAction m f) => (b -> f c) -> (a -> m b) -> a -> f c+      (<=<) = flip (>=>)+      (>>) :: forall m f a b. (LeftCompAction m f) => m a -> f b -> f b+      a >> b = a >>= const b+      (<*>) :: forall m f a b. (LeftCompAction m f) => m (a -> b) -> f a -> f b+      (<*>) = leftCompApply+   in LeftAction {..}++instance (Monad m) => LeftCompAction m m where+  leftCompJoin = M.join+  leftCompBind = (P.>>=)+  leftCompApply = (P.<*>)++instance (LeftCompAction m f, Functor g) => LeftCompAction m (Compose f g) where+  leftCompJoin = Compose . leftCompJoin . fmap getCompose+  a `leftCompBind` f = Compose $ a `leftCompBind` (getCompose . f)+  fs `leftCompApply` xs = fs `leftCompBind` flip fmap xs++class (Monad m, Functor f) => RightCompAction m f where+  rightCompJoin :: forall a. f (m a) -> f a+  rightCompBind :: forall a b. f a -> (a -> m b) -> f b+  rightCompApply :: forall a b. f (a -> b) -> m a -> f b++-- | Right action of any monad @m@ on any composition of functors with @m@ as the innermost component.+rightCompAction :: RightAction RightCompAction+rightCompAction =+  let join :: forall m f a. (RightCompAction m f) => f (m a) -> f a+      join = rightCompJoin+      (>>=) :: forall m f a b. (RightCompAction m f) => f a -> (a -> m b) -> f b+      (>>=) = rightCompBind+      (=<<) :: forall m f a b. (RightCompAction m f) => (a -> m b) -> f a -> f b+      (=<<) = flip rightCompBind+      (>=>) :: forall m f a b c. (RightCompAction m f) => (a -> f b) -> (b -> m c) -> a -> f c+      f >=> g = \x -> f x >>= g+      (<=<) :: forall m f a b c. (RightCompAction m f) => (b -> m c) -> (a -> f b) -> a -> f c+      (<=<) = flip (>=>)+      (>>) :: forall m f a b. (RightCompAction m f) => f a -> m b -> f b+      a >> b = a >>= const b+      (<*>) :: forall m f a b. (RightCompAction m f) => f (a -> b) -> m a -> f b+      (<*>) = rightCompApply+   in RightAction {..}++instance (Monad m) => RightCompAction m m where+  rightCompJoin = M.join+  rightCompBind = (P.>>=)+  rightCompApply = (P.<*>)++instance (RightCompAction m f, Functor g) => RightCompAction m (Compose g f) where+  rightCompJoin = Compose . fmap rightCompJoin . getCompose+  a `rightCompBind` f = Compose . fmap (`rightCompBind` f) $ getCompose a+  fs `rightCompApply` xs = fs `rightCompBind` flip fmap xs

@@ -1,9 +1,11 @@ {-# LANGUAGE LambdaCase #-} {-# LANGUAGE TemplateHaskellQuotes #-}+{-# LANGUAGE TypeData #-} -module Control.Monad.Action.TH (mkLiftStackInstances) where+module Control.Monad.Action.TH (mkLiftBy) where  import Control.Monad.Trans+import Data.Kind qualified as K import Language.Haskell.TH  infixl 5 #@@ -11,43 +13,62 @@ (#) :: Type -> Type -> Type (#) = AppT -mkLiftStackInstances :: Q [Dec]-mkLiftStackInstances =+(|->|) :: Type -> Type -> Type+a |->| b = ArrowT # a # b++mkLiftBy :: Q [Dec]+mkLiftBy =   reify ''MonadTrans     >>= \case       ClassI _ instances ->         do+          decs <-+            [d|+              type data Nat = Z | S Nat++              class (Monad m, Monad n) => LiftBy (k :: Nat) (m :: K.Type -> K.Type) (n :: K.Type -> K.Type) | k n -> m where+                liftBy :: m a -> n a++              instance (Monad m) => LiftBy Z m m where+                liftBy = id+              |]+          let famName = mkName "Steps"           m <- newName "m"           n <- newName "n"-          let cName = mkName "LiftStack"-          -- instance LiftStack m m where-          --   liftStack = id-          let baseInstance =-                InstanceD-                  (Just Incoherent)-                  []-                  (ConT cName # VarT m # VarT m)-                  [ValD (VarP $ mkName "liftStack") (NormalB $ VarE 'id) []]-              inductiveInstances =+          k <- newName "k"+          let famDec =+                ClosedTypeFamilyD+                  ( TypeFamilyHead+                      famName+                      [ KindedTV m BndrReq (StarT |->| StarT),+                        KindedTV n BndrReq (StarT |->| StarT)+                      ]+                      (KindSig . ConT $ mkName "Nat")+                      Nothing+                  )+                  $ TySynEqn Nothing (ConT famName # VarT m # VarT m) (ConT $ mkName "Z")+                    : ( instances >>= \case+                          InstanceD _ _ (AppT (ConT _) t) _ ->+                            [ TySynEqn+                                Nothing+                                (ConT famName # VarT m # (t # VarT n))+                                (ConT (mkName "S") # (ConT famName # VarT m # VarT n))+                            ]+                          _ -> []+                      )+          let inductiveInstances =                 instances >>= \case-                  InstanceD _ ct (AppT (ConT _) t) _ ->-                    -- instance (Monad m, Monad n, LiftStack m n) => LiftStack m (t n) where-                    --   liftStack = lift . liftStack+                  InstanceD ov ct (AppT (ConT _) t) _ ->                     pure $                       InstanceD-                        (Just Incoherent)-                        ( [ ConT ''Monad # VarT m,-                            ConT ''Monad # VarT n,-                            ConT cName # VarT m # VarT n-                          ]-                            ++ ct-                        )-                        (ConT cName # VarT m # (t # VarT n))+                        ov+                        (ct ++ [ConT (mkName "LiftBy") # VarT k # VarT m # VarT n, ConT ''Monad # (t # VarT n)])+                        (ConT (mkName "LiftBy") # (ConT (mkName "S") # VarT k) # VarT m # (t # VarT n))                         [ ValD-                            (VarP $ mkName "liftStack")-                            (NormalB $ UInfixE (VarE 'lift) (VarE '(.)) (VarE $ mkName "liftStack"))+                            (VarP $ mkName "liftBy")+                            (NormalB $ UInfixE (VarE 'lift) (VarE '(.)) (AppTypeE (VarE $ mkName "liftBy") (VarT k)))                             []                         ]                   _ -> []-          pure $ baseInstance : inductiveInstances+          pure $ decs ++ famDec : inductiveInstances       _ -> pure []

@@ -0,0 +1,169 @@+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE FunctionalDependencies #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE TypeData #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE UndecidableInstances #-}++module Control.Monad.TransformerStack (MonadTransStack (..)) where++import Control.Monad.Action.TH+import Control.Monad.Co ()+import Control.Monad.Trans ()+import Control.Monad.Trans.Accum ()+import Control.Monad.Trans.Compose ()+import Control.Monad.Trans.Except ()+import Control.Monad.Trans.Free ()+import Control.Monad.Trans.Iter ()+import Control.Monad.Trans.Maybe ()+import Control.Monad.Trans.RWS ()+import Control.Monad.Trans.RWS.CPS ()+import Control.Monad.Trans.RWS.Lazy ()+import Control.Monad.Trans.RWS.Strict ()+import Control.Monad.Trans.Reader ()+import Control.Monad.Trans.Select ()+import Control.Monad.Trans.State.Lazy ()+import Control.Monad.Trans.State.Strict ()+import Control.Monad.Trans.Writer ()+import Control.Monad.Trans.Writer.CPS ()+import Control.Monad.Trans.Writer.Lazy ()+import Control.Monad.Trans.Writer.Strict ()++$mkLiftBy++-- | @'MonadTransStack' m n@ means that @n@ is a stack of monad transformers over @m@.+--+--   All @'MonadTransStack'@ instances are defined inductively using @'Control.Monad.Trans.Class.MonadTrans'@.+--   @'Control.Monad.Trans.Class.MonadTrans'@ instances are required to satisfy these laws, which state+--   that @'Control.Monad.Trans.Class.lift'@ is a monad homomorphism:+--+--   * @'Control.Monad.Trans.Class.lift' '.' 'pure' = 'pure'@+--+--   * @'Control.Monad.Trans.Class.lift' (m '>>=' f) = 'Control.Monad.Trans.Class.lift' m '>>=' ('Control.Monad.Trans.Class.lift' '.' f)@+--+--   Restating the second law in terms of @'Control.Monad.join'@:+--+--   * @'Control.Monad.Trans.Class.lift' '.' 'Control.Monad.join' = 'Control.Monad.join' '.' 'fmap' 'Control.Monad.Trans.Class.lift' '.' 'Control.Monad.Trans.Class.lift'@+--+--   Because the composition of two monad homomorphisms is a monad homomorphism, @'liftStack'@ also satisfies these laws:+--+--   * @'liftStack' '.' 'pure' = 'pure'@+--+--   * @'liftStack' '.' 'Control.Monad.join' = 'Control.Monad.join' '.' 'fmap' 'liftStack' '.' 'liftStack'@+--+--   The left monad action laws can now be easily proved using string diagrams.+--   Functors compose from top to bottom, natural transformations from left to right,+--   @───@ represents @t m@, @┈┈┈@ represents @m@, @├@ represents @'pure'@ or+--   @'Control.Monad.join'@ depending on the number of inputs, and @┈┈┈►───@ represents @'liftStack'@.+--   The @'MonadTransStack'@ laws as string diagrams are:+--+--   > ├┈┈┈►───  = ├──────+--+--   > ┈┈┈┐            ┈┈┈►───┐+--   >    ├┈┈┈►───  =         ├───+--   > ┈┈┈┘            ┈┈┈►───┘+--+--   and the diagram for @'Control.Monad.Action.ljoin'@ is:+--+--   > ┈┈►──┐+--   >      ├───+--   > ─────┘+--+--   To prove the identity law:+--+--   >   ├┈┈►──┐          ├─────┐+--   >         ├───  =          ├───  =  ──────+--   > ────────┘        ────────┘+--+--   In other words,+--+--   @   'Control.Monad.Action.ljoin' '.' 'pure'+--   = 'Control.Monad.join' '.' 'liftStack' '.' 'pure'+--   = 'Control.Monad.join' '.' 'pure'+--   = 'id'@+--+--   To prove associativity:+--+--   > ┈┈┈┐              ┈┈►──┐+--   >    ├┈┈►─┐              ├──┐         ┈┈┈┈┈┈┈►─┐+--   > ┈┈┈┘    ├────  =  ┈┈►──┘  ├────  =  ┈┈►──┐   ├────+--   > ────────┘         ────────┘              ├───┘+--   >                                     ─────┘+--+--   In other words,+--+--   @  'Control.Monad.Action.ljoin' '.' 'Control.Monad.join'+--   = 'Control.Monad.join' '.' 'liftStack' '.' 'Control.Monad.join'+--   = 'Control.Monad.join' '.' 'Control.Monad.join' '.' 'fmap' 'liftStack' '.' 'liftStack'+--   = 'Control.Monad.join' '.' 'fmap' 'Control.Monad.join' '.' 'fmap' 'liftStack' '.' 'liftStack'+--   = 'Control.Monad.join' '.' 'fmap' ('Control.Monad.join' '.' 'liftStack') '.' 'liftStack'+--   = 'Control.Monad.join' '.' 'liftStack' '.' 'fmap' ('Control.Monad.join' '.' 'liftStack')+--   = 'Control.Monad.Action.ljoin' '.' 'fmap' 'Control.Monad.Action.ljoin'@+--+--   We can prove the right module laws using string diagrams in the same way.+--+--   The diagram for @'Control.Monad.Action.rjoin'@ is:+--+--   > ─────┐+--   >      ├───+--   > ┈┈►──┘+--+--   To prove the identity law:+--+--   > ────────┐        ────────┐+--   >         ├───  =          ├───  =  ──────+--   >   ├┈┈►──┘          ├─────┘+--+--   In other words,+--+--   @   'Control.Monad.Action.rjoin' '.' 'fmap' 'pure'+--   = 'Control.Monad.join' '.' 'fmap' 'liftStack' , 'pure'+--   = 'Control.Monad.join' '.' 'fmap' 'liftStack' , 'fmap' 'pure'+--   = 'Control.Monad.join' '.' 'fmap' ('liftStack' , 'pure')+--   = 'Control.Monad.join' '.' 'fmap' 'pure'+--   = 'id'@+--+--   To prove associativity:+--+--   >                                      ─────┐+--   > ────────┐         ─────────┐              ├───┐+--   > ┈┈┈┐    ├────  =  ┈┈►──┐   ├────  =  ┈┈►──┘   ├────+--   >    ├┈┈►─┘              ├───┘         ┈┈┈┈┈┈┈►─┘+--   > ┈┈┈┘              ┈┈►──┘+--+--   In other words,+--+--   @  'Control.Monad.Action.rjoin' '.' 'fmap' 'Control.Monad.join'+--   = 'Control.Monad.join' '.' 'fmap' 'liftStack' '.' 'fmap' 'Control.Monad.join'+--   = 'Control.Monad.join' '.' 'fmap' ('liftStack' '.' 'Control.Monad.join')+--   = 'Control.Monad.join' '.' 'fmap' ('Control.Monad.join' '.' 'fmap' 'liftStack' '.' 'liftStack')+--   = 'Control.Monad.join' '.' 'fmap' 'Control.Monad.join' '.' 'fmap' ('fmap' 'liftStack' '.' 'liftStack')+--   = 'Control.Monad.join' '.' 'Control.Monad.join' '.' 'fmap' ('fmap' 'liftStack') '.' 'fmap' ('liftStack')+--   = 'Control.Monad.join' '.' 'fmap' 'liftStack' '.' 'Control.Monad.join' '.' 'fmap' 'liftStack'+--   = 'Control.Monad.Action.rjoin' '.' 'Control.Monad.Action.rjoin'@+--+--   The bimodule law can be proved as follows:+--+--   > ┈┈┈►─┐             ┈┈►─┐+--   >      ├───┐             ├───┐          ┈┈┈┈┈┈►─┐+--   > ─────┘   ├────  =  ────┘   ├────  =   ────┐   ├────+--   > ┈►───────┘         ┈┈┈┈┈┈►─┘              ├───┘+--   >                                       ┈┈►─┘+--+--   In other words,+--+--   @  'Control.Monad.Action.bijoin'+--   = 'Control.Monad.join' '.' 'Control.Monad.join' '.' 'liftStack' '.' 'fmap' ('fmap' 'liftStack')+--   = 'Control.Monad.join' '.' 'fmap' 'liftStack' '.' 'Control.Monad.join' '.' 'liftStack'+--   = 'Control.Monad.Action.rjoin' '.' 'Control.Monad.Action.ljoin'+--   = 'Control.Monad.join' '.' 'fmap' 'liftStack' '.' 'Control.Monad.join' '.' 'liftStack'+--   = 'Control.Monad.join' '.' 'fmap' 'Control.Monad.join' '.' 'fmap' ('fmap' 'liftStack') '.' 'liftStack'+--   = 'Control.Monad.join' '.' 'fmap' ('Control.Monad.join' '.' 'fmap' 'liftStack') '.' 'liftStack'+--   = 'Control.Monad.join' '.' 'fmap' 'Control.Monad.Action.rjoin' '.' 'liftStack'+--   = 'Control.Monad.join' '.' 'liftStack' '.' 'fmap' 'Control.Monad.Action.rjoin'+--   = 'Control.Monad.Action.ljoin' '.' 'fmap' 'Control.Monad.Action.rjoin'@+class (LiftBy (Steps m n) m n) => MonadTransStack m n where+  liftStack :: forall a. m a -> n a++instance (LiftBy (Steps m n) m n) => MonadTransStack m n where+  liftStack = liftBy @(Steps m n)

@@ -21,6 +21,7 @@ import Control.Monad.Trans.Compose import Control.Monad.Trans.Free (FreeF (..), FreeT (..)) import Control.Monad.Trans.Maybe+import Control.Monad.TransformerStack import Control.Monad.Writer import Data.Functor.Classes (Eq1) import Data.Functor.Compose@@ -130,7 +131,8 @@     Arbitrary s,     EqProp (m (a, s)),     Arbitrary (m (m (m a), s)),-    Show (m (m (m a), s))+    Show (m (m (m a), s)),+    MonadTransStack m (StateT s m)   ) =>   TestBatch rightmodulestate =@@ -159,7 +161,8 @@     EqProp (m (StateT s m a)),     Show s,     Arbitrary s,-    EqProp (m (a, s))+    EqProp (m (a, s)),+    MonadTransStack m (StateT s m)   ) =>   TestBatch leftmodulestate =@@ -185,7 +188,8 @@     Show (m (Fun s (m (m a, s)))),     Show s,     Arbitrary s,-    EqProp (m (a, s))+    EqProp (m (a, s)),+    MonadTransStack m (StateT s m)   ) =>   TestBatch bimodulestate =@@ -216,7 +220,8 @@     Show (m (m (m a))),     Show s,     Arbitrary s,-    EqProp (m a)+    EqProp (m a),+    MonadTransStack m (ReaderT s m)   ) =>   TestBatch rightmodulereader =