diff --git a/CHANGELOG.md b/CHANGELOG.md new file mode 100644 --- /dev/null +++ b/CHANGELOG.md @@ -0,0 +1,5 @@ +# Revision history for monad-actions + +## 0.1.0.0 -- 2026-01-22 + +* First version. Released on an unsuspecting world. diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,165 @@ + GNU LESSER GENERAL PUBLIC LICENSE + Version 3, 29 June 2007 + + Copyright (C) 2007 Free Software Foundation, Inc. + Everyone is permitted to copy and distribute verbatim copies + of this license document, but changing it is not allowed. + + + This version of the GNU Lesser General Public License incorporates +the terms and conditions of version 3 of the GNU General Public +License, supplemented by the additional permissions listed below. + + 0. Additional Definitions. + + As used herein, "this License" refers to version 3 of the GNU Lesser +General Public License, and the "GNU GPL" refers to version 3 of the GNU +General Public License. + + "The Library" refers to a covered work governed by this License, +other than an Application or a Combined Work as defined below. + + An "Application" is any work that makes use of an interface provided +by the Library, but which is not otherwise based on the Library. +Defining a subclass of a class defined by the Library is deemed a mode +of using an interface provided by the Library. + + A "Combined Work" is a work produced by combining or linking an +Application with the Library. The particular version of the Library +with which the Combined Work was made is also called the "Linked +Version". + + The "Minimal Corresponding Source" for a Combined Work means the +Corresponding Source for the Combined Work, excluding any source code +for portions of the Combined Work that, considered in isolation, are +based on the Application, and not on the Linked Version. + + The "Corresponding Application Code" for a Combined Work means the +object code and/or source code for the Application, including any data +and utility programs needed for reproducing the Combined Work from the +Application, but excluding the System Libraries of the Combined Work. + + 1. Exception to Section 3 of the GNU GPL. + + You may convey a covered work under sections 3 and 4 of this License +without being bound by section 3 of the GNU GPL. + + 2. Conveying Modified Versions. + + If you modify a copy of the Library, and, in your modifications, a +facility refers to a function or data to be supplied by an Application +that uses the facility (other than as an argument passed when the +facility is invoked), then you may convey a copy of the modified +version: + + a) under this License, provided that you make a good faith effort to + ensure that, in the event an Application does not supply the + function or data, the facility still operates, and performs + whatever part of its purpose remains meaningful, or + + b) under the GNU GPL, with none of the additional permissions of + this License applicable to that copy. + + 3. Object Code Incorporating Material from Library Header Files. + + The object code form of an Application may incorporate material from +a header file that is part of the Library. You may convey such object +code under terms of your choice, provided that, if the incorporated +material is not limited to numerical parameters, data structure +layouts and accessors, or small macros, inline functions and templates +(ten or fewer lines in length), you do both of the following: + + a) Give prominent notice with each copy of the object code that the + Library is used in it and that the Library and its use are + covered by this License. + + b) Accompany the object code with a copy of the GNU GPL and this license + document. + + 4. Combined Works. + + You may convey a Combined Work under terms of your choice that, +taken together, effectively do not restrict modification of the +portions of the Library contained in the Combined Work and reverse +engineering for debugging such modifications, if you also do each of +the following: + + a) Give prominent notice with each copy of the Combined Work that + the Library is used in it and that the Library and its use are + covered by this License. + + b) Accompany the Combined Work with a copy of the GNU GPL and this license + document. + + c) For a Combined Work that displays copyright notices during + execution, include the copyright notice for the Library among + these notices, as well as a reference directing the user to the + copies of the GNU GPL and this license document. + + d) Do one of the following: + + 0) Convey the Minimal Corresponding Source under the terms of this + License, and the Corresponding Application Code in a form + suitable for, and under terms that permit, the user to + recombine or relink the Application with a modified version of + the Linked Version to produce a modified Combined Work, in the + manner specified by section 6 of the GNU GPL for conveying + Corresponding Source. + + 1) Use a suitable shared library mechanism for linking with the + Library. A suitable mechanism is one that (a) uses at run time + a copy of the Library already present on the user's computer + system, and (b) will operate properly with a modified version + of the Library that is interface-compatible with the Linked + Version. + + e) Provide Installation Information, but only if you would otherwise + be required to provide such information under section 6 of the + GNU GPL, and only to the extent that such information is + necessary to install and execute a modified version of the + Combined Work produced by recombining or relinking the + Application with a modified version of the Linked Version. (If + you use option 4d0, the Installation Information must accompany + the Minimal Corresponding Source and Corresponding Application + Code. If you use option 4d1, you must provide the Installation + Information in the manner specified by section 6 of the GNU GPL + for conveying Corresponding Source.) + + 5. Combined Libraries. + + You may place library facilities that are a work based on the +Library side by side in a single library together with other library +facilities that are not Applications and are not covered by this +License, and convey such a combined library under terms of your +choice, if you do both of the following: + + a) Accompany the combined library with a copy of the same work based + on the Library, uncombined with any other library facilities, + conveyed under the terms of this License. + + b) Give prominent notice with the combined library that part of it + is a work based on the Library, and explaining where to find the + accompanying uncombined form of the same work. + + 6. Revised Versions of the GNU Lesser General Public License. + + The Free Software Foundation may publish revised and/or new versions +of the GNU Lesser General Public License from time to time. Such new +versions will be similar in spirit to the present version, but may +differ in detail to address new problems or concerns. + + Each version is given a distinguishing version number. If the +Library as you received it specifies that a certain numbered version +of the GNU Lesser General Public License "or any later version" +applies to it, you have the option of following the terms and +conditions either of that published version or of any later version +published by the Free Software Foundation. If the Library as you +received it does not specify a version number of the GNU Lesser +General Public License, you may choose any version of the GNU Lesser +General Public License ever published by the Free Software Foundation. + + If the Library as you received it specifies that a proxy can decide +whether future versions of the GNU Lesser General Public License shall +apply, that proxy's public statement of acceptance of any version is +permanent authorization for you to choose that version for the +Library. diff --git a/monad-actions.cabal b/monad-actions.cabal new file mode 100644 --- /dev/null +++ b/monad-actions.cabal @@ -0,0 +1,76 @@ +cabal-version: 3.4 +name: monad-actions +-- The package version. +-- See the Haskell package versioning policy (PVP) for standards +-- guiding when and how versions should be incremented. +-- https://pvp.haskell.org +-- PVP summary: +-- +-+------- breaking API changes +-- | | +----- non-breaking API additions +-- | | | +--- code changes with no API change +version: 0.1.0.0 +synopsis: Left or right actions of a monad on a functor +description: + This package defines classes for left and rght actions of + monads on functors. It also includes modules for using + monad actions with qualified do notation. + +license: LGPL-2.0-or-later +license-file: LICENSE +author: noiioiu +maintainer: noiioiu@cocaine.ninja +category: + Control, + Monads + +homepage: https://codeberg.org/noiioiu/monad-actions +build-type: Simple +extra-doc-files: CHANGELOG.md + +common warnings + ghc-options: -Wall + +source-repository head + type: git + location: ssh://git@codeberg.org/noiioiu/monad-actions.git + +library + import: warnings + exposed-modules: + Control.Monad.Action + Control.Monad.Action.Left + Control.Monad.Action.Right + + other-modules: Control.Monad.Action.TH + build-depends: + base >= 4.20.2 && < 4.21, + free >= 5.2 && < 5.3, + kan-extensions >= 5.2.8 && < 5.3, + mmorph >= 1.2.2 && < 1.3, + mtl >= 2.3.1 && < 2.4, + template-haskell >= 2.22.0 && < 2.23, + transformers >= 0.6.1 && < 0.7, + + + + hs-source-dirs: src + default-language: GHC2021 + +test-suite monad-actions-test + import: warnings + default-language: GHC2021 + type: exitcode-stdio-1.0 + hs-source-dirs: test + main-is: Main.hs + build-depends: + QuickCheck, + base, + checkers, + free, + kan-extensions, + mmorph, + monad-actions, + mtl, + tasty, + tasty-quickcheck, + transformers, diff --git a/src/Control/Monad/Action.hs b/src/Control/Monad/Action.hs new file mode 100644 --- /dev/null +++ b/src/Control/Monad/Action.hs @@ -0,0 +1,359 @@ +{-# LANGUAGE TemplateHaskell #-} + +-- | 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\) 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)\) +-- +-- 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 +-- 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. +-- +-- 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. +module Control.Monad.Action + ( LeftModule (..), + RightModule (..), + BiModule (..), + monadTransLScale, + monadTransRScale, + monadTransBiScale, + ) +where + +import Control.Monad (join) +import Control.Monad.Action.TH +import Control.Monad.Co () +import Control.Monad.Codensity (Codensity (..)) +import Control.Monad.IO.Class +import Control.Monad.Identity (Identity (..)) +import Control.Monad.Morph +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 () +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.CPS qualified as C () +import Control.Monad.Trans.Writer.Lazy qualified as L () +import Control.Monad.Trans.Writer.Strict qualified as S () +import Data.Functor.Compose (Compose (..)) +import Data.List.NonEmpty qualified as NE (NonEmpty, toList) +import Data.Maybe (catMaybes, mapMaybe) + +-- | Instances must satisfy the following laws: +-- +-- * @'ljoin' '.' 'join' = 'ljoin' '.' 'fmap' 'ljoin'@ +-- +-- * @'ljoin' '.' 'pure' = 'id'@ +class (Monad m, Functor f) => LeftModule m f where + ljoin :: + m (f a) -> + -- | left monad action + f a + ljoin = (`lbind` id) + lbind :: m a -> (a -> f b) -> f b + lbind = (ljoin .) . flip fmap + {-# MINIMAL ljoin | lbind #-} + +-- | Instances must satisfy the following laws: +-- +-- * @'rjoin' '.' 'fmap' 'join' = 'rjoin' '.' 'rjoin'@ +-- +-- * @'rjoin' '.' 'fmap' 'pure' = 'id'@ +class (Monad m, Functor f) => RightModule m f where + rjoin :: + f (m a) -> + -- | right monad action + f a + rjoin = (`rbind` id) + rbind :: f a -> (a -> m b) -> f b + rbind = (rjoin .) . flip fmap + {-# MINIMAL rjoin | rbind #-} + +-- | Given two monads r and s, an (r, s) bimodule is a functor that is a left module over r and a right module over s, where the two actions are compatible. +-- Instances must satisfy the following law in addition to the laws for @'LeftModule'@ and @'RightModule'@: +-- +-- * @'rjoin' '.' 'ljoin' = 'ljoin' '.' 'fmap' 'rjoin' = 'bijoin'@ +class (LeftModule r f, RightModule s f) => BiModule r s f where + bijoin :: + r (f (s a)) -> + -- | two-sided monad action + f a + bijoin = rjoin . ljoin + +-- | Default left scalar multiplication for monad transformers. +-- +-- @'MonadTrans'@ instances are required to satisfy these laws, which state that @'lift'@ is a monad homomorphism: +-- +-- * @'lift' '.' 'pure' = 'pure'@ +-- +-- * @'lift' (m '>>=' f) = 'lift' m '>>=' ('lift' '.' f)@ +-- +-- Restating the second law in terms of @'join'@: +-- +-- * @'lift' '.' 'join' = 'join' '.' 'fmap' 'lift' '.' 'lift'@ +-- +-- 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 @'lift'@. +-- The @'MonadTrans'@ laws as string diagrams are: +-- +-- > ├┈┈┈►─── = ├────── +-- +-- > ┈┈┈┐ ┈┈┈►───┐ +-- > ├┈┈┈►─── = ├─── +-- > ┈┈┈┘ ┈┈┈►───┘ +-- +-- and the diagram for @'ljoin'@ is: +-- +-- > ┈┈►──┐ +-- > ├─── +-- > ─────┘ +-- +-- To prove the identity law: +-- +-- > ├┈┈►──┐ ├─────┐ +-- > ├─── = ├─── = ────── +-- > ────────┘ ────────┘ +-- +-- In other words, +-- +-- @ 'ljoin' '.' 'pure' +-- = 'join' '.' 'lift' '.' 'pure' +-- = 'join' '.' 'pure' +-- = 'id'@ +-- +-- To prove associativity: +-- +-- > ┈┈┈┐ ┈┈►──┐ +-- > ├┈┈►─┐ ├──┐ ┈┈┈┈┈┈┈►─┐ +-- > ┈┈┈┘ ├──── = ┈┈►──┘ ├──── = ┈┈►──┐ ├──── +-- > ────────┘ ────────┘ ├───┘ +-- > ─────┘ +-- +-- In other words, +-- +-- @ 'ljoin' '.' 'join' +-- = 'join' '.' 'lift' '.' 'join' +-- = 'join' '.' 'join' '.' 'fmap' 'lift' '.' 'lift' +-- = 'join' '.' 'fmap' 'join' '.' 'fmap' 'lift' '.' 'lift' +-- = 'join' '.' 'fmap' ('join' '.' 'lift') '.' 'lift' +-- = 'join' '.' 'lift' '.' 'fmap' ('join' '.' 'lift') +-- = 'ljoin' '.' 'fmap' 'ljoin'@ +monadTransLScale :: (Monad m, MonadTrans t, Monad (t m)) => m (t m a) -> t m a +monadTransLScale = join . lift + +-- | Default right scalar multiplication for monad transformers. +-- +-- We prove the right module laws using string diagrams, just as in the case +-- of the left module laws. +-- +-- The diagram for @'rjoin'@ is: +-- +-- > ─────┐ +-- > ├─── +-- > ┈┈►──┘ +-- +-- To prove the identity law: +-- +-- > ────────┐ ────────┐ +-- > ├─── = ├─── = ────── +-- > ├┈┈►──┘ ├─────┘ +-- +-- In other words, +-- +-- @ 'rjoin' '.' 'fmap' 'pure' +-- = 'join' '.' 'fmap' 'lift' , 'pure' +-- = 'join' '.' 'fmap' 'lift' , 'fmap' 'pure' +-- = 'join' '.' 'fmap' ('lift' , 'pure') +-- = 'join' '.' 'fmap' 'pure' +-- = 'id'@ +-- +-- To prove associativity: +-- +-- > ─────┐ +-- > ────────┐ ─────────┐ ├───┐ +-- > ┈┈┈┐ ├──── = ┈┈►──┐ ├──── = ┈┈►──┘ ├──── +-- > ├┈┈►─┘ ├───┘ ┈┈┈┈┈┈┈►─┘ +-- > ┈┈┈┘ ┈┈►──┘ +-- +-- In other words, +-- +-- @ 'rjoin' '.' 'fmap' 'join' +-- = 'join' '.' 'fmap' 'lift' '.' 'fmap' 'join' +-- = 'join' '.' 'fmap' ('lift' '.' 'join') +-- = 'join' '.' 'fmap' ('join' '.' 'fmap' 'lift' '.' 'lift') +-- = 'join' '.' 'fmap' 'join' '.' 'fmap' ('fmap' 'lift' '.' 'lift') +-- = 'join' '.' 'join' '.' 'fmap' ('fmap' 'lift') '.' 'fmap' ('lift') +-- = 'join' '.' 'fmap' 'lift' '.' 'join' '.' 'fmap' 'lift' +-- = 'rjoin' '.' 'rjoin'@ +monadTransRScale :: (Monad m, MonadTrans t, Monad (t m)) => t m (m a) -> t m a +monadTransRScale = (lift =<<) + +-- | Default two-sided scalar multiplication for monad transformers. +-- +-- We prove the bimodule law using string diagrams, just as in the case +-- of the left and right module laws: +-- +-- > ┈┈┈►─┐ ┈┈►─┐ +-- > ├───┐ ├───┐ ┈┈┈┈┈┈►─┐ +-- > ─────┘ ├──── = ────┘ ├──── = ────┐ ├──── +-- > ┈►───────┘ ┈┈┈┈┈┈►─┘ ├───┘ +-- > ┈┈►─┘ +-- +-- In other words, +-- +-- @ 'bijoin' +-- = 'join' '.' 'join' '.' 'lift' '.' 'fmap' ('fmap' 'lift') +-- = 'join' '.' 'fmap' 'lift' '.' 'join' '.' 'lift' +-- = 'rjoin' '.' 'ljoin' +-- = 'join' '.' 'fmap' 'lift' '.' 'join' '.' 'lift' +-- = 'join' '.' 'fmap' 'join' '.' 'fmap' ('fmap' 'lift') '.' 'lift' +-- = 'join' '.' 'fmap' ('join' '.' 'fmap' 'lift') '.' 'lift' +-- = 'join' '.' 'fmap' 'rjoin' '.' 'lift' +-- = 'join' '.' 'lift' '.' 'fmap' 'rjoin' +-- = 'ljoin' '.' 'fmap' 'rjoin'@ +monadTransBiScale :: (Monad m, MonadTrans t, Monad (t m)) => m (t m (m a)) -> t m a +monadTransBiScale = join . join . lift . fmap (fmap lift) + +$mkMonadTransModuleInstances + +instance {-# OVERLAPPING #-} (Monad m) => LeftModule m m where ljoin = join; lbind = (>>=) + +instance {-# OVERLAPPING #-} (Monad m) => RightModule m m where rjoin = join; rbind = (>>=) + +instance {-# OVERLAPPING #-} (Monad m) => BiModule m m m + +instance {-# INCOHERENT #-} (Functor f) => LeftModule Identity f where ljoin = runIdentity + +instance {-# INCOHERENT #-} (Functor f) => RightModule Identity f where rjoin = fmap runIdentity + +instance {-# INCOHERENT #-} (Functor f) => BiModule Identity Identity f + +instance RightModule Maybe [] where rjoin = catMaybes; rbind = flip mapMaybe + +instance LeftModule Maybe [] where ljoin = concat; lbind = flip concatMap + +instance LeftModule NE.NonEmpty [] where ljoin = concat; lbind = flip concatMap + +instance RightModule NE.NonEmpty [] where rjoin = (>>= NE.toList) + +instance BiModule Maybe Maybe [] + +instance BiModule Maybe [] [] + +instance BiModule [] Maybe [] + +instance BiModule NE.NonEmpty NE.NonEmpty [] + +instance BiModule [] NE.NonEmpty [] + +instance BiModule NE.NonEmpty [] [] + +instance BiModule Maybe NE.NonEmpty [] + +instance BiModule NE.NonEmpty Maybe [] + +instance RightModule (Either e) Maybe where + rjoin (Just (Right x)) = Just x + rjoin _ = Nothing + +instance LeftModule (Either e) Maybe where + ljoin (Right (Just x)) = Just x + ljoin _ = Nothing + +instance BiModule (Either e) (Either f) Maybe + +instance BiModule (Either e) Maybe Maybe + +instance BiModule Maybe (Either f) Maybe + +instance {-# INCOHERENT #-} (Monad m, Functor f, LeftModule m n) => LeftModule m (Compose n f) where + ljoin = Compose . ljoin . fmap getCompose + a `lbind` f = Compose $ a `lbind` (getCompose . f) + +instance {-# INCOHERENT #-} (Monad m, Functor f, RightModule m n) => RightModule m (Compose f n) where + rjoin = Compose . fmap rjoin . getCompose + a `rbind` f = Compose . fmap (`rbind` f) $ getCompose a + +instance {-# INCOHERENT #-} (Monad s, Monad t, Functor f, LeftModule s u, RightModule t v) => BiModule s t (Compose u (Compose f v)) + +instance {-# INCOHERENT #-} (Monad m) => LeftModule Maybe (MaybeT m) where + ljoin = join . MaybeT . pure + +instance {-# INCOHERENT #-} (Monad m) => RightModule Maybe (MaybeT m) where + rjoin = MaybeT . fmap join . runMaybeT + +instance {-# INCOHERENT #-} (Monad m) => LeftModule (Either e) (MaybeT m) where + ljoin = join . MaybeT . fmap (either (const Nothing) Just) . pure @m + +instance {-# INCOHERENT #-} (Monad m) => RightModule (Either e) (MaybeT m) where + rjoin = MaybeT . fmap (either (const Nothing) Just =<<) . runMaybeT + +instance {-# INCOHERENT #-} (Monoid e, Monad m) => LeftModule Maybe (ExceptT e m) where + ljoin = join . ExceptT . pure . maybe (Left mempty) Right + +instance {-# INCOHERENT #-} (Monoid e, Monad m) => RightModule Maybe (ExceptT e m) where + rjoin = ExceptT . fmap (maybe (Left mempty) Right =<<) . runExceptT + +instance {-# INCOHERENT #-} (Monad m) => LeftModule (Either e) (ExceptT e m) where + ljoin = join . ExceptT . pure + +instance {-# INCOHERENT #-} (Monoid e, Monad m) => RightModule (Either e) (ExceptT e m) where + rjoin = ExceptT . fmap join . runExceptT + +instance {-# INCOHERENT #-} (Monad m) => BiModule Maybe Maybe (MaybeT m) + +instance {-# INCOHERENT #-} (Monad m) => BiModule (Either e) Maybe (MaybeT m) + +instance {-# INCOHERENT #-} (Monad m) => BiModule Maybe (Either e) (MaybeT m) + +instance {-# INCOHERENT #-} (Monad m) => BiModule (Either e) (Either f) (MaybeT m) + +instance {-# INCOHERENT #-} (Monoid e, Monad m) => BiModule Maybe Maybe (ExceptT e m) + +instance {-# INCOHERENT #-} (Monoid e, Monad m) => BiModule (Either e) Maybe (ExceptT e m) + +instance {-# INCOHERENT #-} (Monoid e, Monad m) => BiModule Maybe (Either e) (ExceptT e m) + +instance {-# INCOHERENT #-} (Monoid e, Monad m) => BiModule (Either e) (Either e) (ExceptT e m) + +-- | @'liftIO'@ is a monad homomorphism, so the proof that every monad with a lawful @'MonadIO'@ +-- instance is a {left,right,bi} module over @'IO'@ is the same as the proof for monad transformers. +instance {-# INCOHERENT #-} (MonadIO m) => LeftModule IO m where + ljoin = join . liftIO + +instance {-# INCOHERENT #-} (MonadIO m) => RightModule IO m where + rjoin = (>>= liftIO) + +instance {-# INCOHERENT #-} (MonadIO m) => BiModule IO IO m + +-- | Proof that @f@ is always a left module over @'Codensity' f@: +-- - @ 'ljoin' ('join' m) +-- = 'ljoin' ('Codensity' (\c -> 'runCodensity' m (\a -> 'runCodensity' a c))) +-- = (\c -> 'runCodensity' m (\a -> 'runCodensity' a c)) id +-- = 'runCodensity' m (\a -> 'runCodensity' a 'id') +-- = 'runCodensity' m 'ljoin' 'runCodensity' m (\x -> 'ljoin' x) +-- = (\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 + a `lbind` f = runCodensity (f <$> a) id diff --git a/src/Control/Monad/Action/Left.hs b/src/Control/Monad/Action/Left.hs new file mode 100644 --- /dev/null +++ b/src/Control/Monad/Action/Left.hs @@ -0,0 +1,48 @@ +-- | This module should be imported qualified, and can be used with the @QualifiedDo@ extension. +module Control.Monad.Action.Left ((>>=), (>>), (=<<), (>=>), (<=<), (<*>), fmap, pure, return, fail, join) where + +import Control.Monad.Action +import Prelude hiding (fmap, pure, return, (<*>), (=<<), (>>), (>>=)) +import Prelude qualified as P + +infixl 1 >>= + +(>>=) :: (LeftModule m f) => m a -> (a -> f b) -> f b +(>>=) = lbind + +infixr 1 =<< + +(=<<) :: (LeftModule m f) => (a -> f b) -> m a -> f b +(=<<) = flip lbind + +infixl 1 >> + +(>>) :: (LeftModule m f) => m a -> f b -> f b +(>>) = (. const) . lbind + +infixr 1 >=> + +(>=>) :: (LeftModule m f) => (a -> m b) -> (b -> f c) -> a -> f c +(>=>) = flip $ (.) . (=<<) + +infixr 1 <=< + +(<=<) :: (LeftModule m f) => (b -> f c) -> (a -> m b) -> a -> f c +(<=<) = (.) . (=<<) + +fmap :: (Functor f) => (a -> b) -> f a -> f b +fmap = P.fmap + +pure :: (Applicative f) => a -> f a +pure = P.pure + +return :: (Applicative f) => a -> f a +return = pure + +join :: (LeftModule m f) => m (f a) -> f a +join = ljoin + +infixl 4 <*> + +(<*>) :: (LeftModule m f) => m (a -> b) -> f a -> f b +fs <*> xs = fs >>= flip fmap xs diff --git a/src/Control/Monad/Action/Right.hs b/src/Control/Monad/Action/Right.hs new file mode 100644 --- /dev/null +++ b/src/Control/Monad/Action/Right.hs @@ -0,0 +1,48 @@ +-- | This module should be imported qualified, and can be used with the @QualifiedDo@ extension. +module Control.Monad.Action.Right ((>>=), (>>), (=<<), (>=>), (<=<), (<*>), fmap, pure, return, fail, join) where + +import Control.Monad.Action +import Prelude hiding (fmap, pure, return, (<*>), (=<<), (>>), (>>=)) +import Prelude qualified as P + +infixl 1 >>= + +(>>=) :: (RightModule m f) => f a -> (a -> m b) -> f b +(>>=) = rbind + +infixr 1 =<< + +(=<<) :: (RightModule m f) => (a -> m b) -> f a -> f b +(=<<) = flip rbind + +infixl 1 >> + +(>>) :: (RightModule m f) => f a -> m b -> f b +(>>) = (. const) . rbind + +infixr 1 >=> + +(>=>) :: (RightModule m f) => (a -> f b) -> (b -> m c) -> a -> f c +(>=>) = flip $ (.) . (=<<) + +infixr 1 <=< + +(<=<) :: (RightModule m f) => (b -> m c) -> (a -> f b) -> a -> f c +(<=<) = (.) . (=<<) + +fmap :: (Functor f) => (a -> b) -> f a -> f b +fmap = P.fmap + +pure :: (Applicative f) => a -> f a +pure = P.pure + +return :: (Applicative f) => a -> f a +return = pure + +join :: (RightModule m f) => f (m a) -> f a +join = rjoin + +infixl 4 <*> + +(<*>) :: (RightModule m f) => f (a -> b) -> m a -> f b +fs <*> xs = fs >>= flip fmap xs diff --git a/src/Control/Monad/Action/TH.hs b/src/Control/Monad/Action/TH.hs new file mode 100644 --- /dev/null +++ b/src/Control/Monad/Action/TH.hs @@ -0,0 +1,61 @@ +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE TemplateHaskellQuotes #-} + +module Control.Monad.Action.TH (mkMonadTransModuleInstances) where + +import Control.Monad +import Control.Monad.Trans +import Language.Haskell.TH + +uncurry3 :: (a -> b -> c -> d) -> (a, b, c) -> d +uncurry3 f (a, b, c) = f a b c + +mkMonadTransModuleInstances :: Q [Dec] +mkMonadTransModuleInstances = + reify ''MonadTrans + >>= \case + ClassI _ instances -> + fmap join . forM instances $ \case + InstanceD _ ct (AppT (ConT _) ty) _ -> + do + m <- VarT <$> newName "m" + let ct' = ct ++ [AppT (ConT ''Monad) m] + let ctB = + ct + ++ [ AppT (ConT ''Monad) m, + AppT (AppT (ConT $ mkName "LeftModule") m) (AppT ty m), + AppT (AppT (ConT $ mkName "RightModule") m) (AppT ty m) + ] + let tyL = AppT (AppT (ConT $ mkName "LeftModule") m) (AppT ty m) + let tyR = AppT (AppT (ConT $ mkName "RightModule") m) (AppT ty m) + let tyB = AppT (AppT (AppT (ConT $ mkName "BiModule") m) m) (AppT ty m) + pure $ + fmap + (uncurry3 $ InstanceD (Just Overlaps)) + [ ( ct', + tyL, + [ ValD + (VarP $ mkName "ljoin") + (NormalB (VarE $ mkName "monadTransLScale")) + [] + ] + ), + ( ct', + tyR, + [ ValD + (VarP $ mkName "rjoin") + (NormalB (VarE $ mkName "monadTransRScale")) + [] + ] + ), + ( ctB, + tyB, + [ ValD + (VarP $ mkName "bijoin") + (NormalB (VarE $ mkName "monadTransBiScale")) + [] + ] + ) + ] + _ -> fail "Not an instance" + _ -> pure [] diff --git a/test/Main.hs b/test/Main.hs new file mode 100644 --- /dev/null +++ b/test/Main.hs @@ -0,0 +1,321 @@ +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE QualifiedDo #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE UndecidableInstances #-} +{-# OPTIONS_GHC -Wno-orphans #-} +{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-} +{-# OPTIONS_GHC -Wno-unused-top-binds #-} + +module Main (main) where + +import Control.Applicative +import Control.Monad +import Control.Monad.Action +import Control.Monad.Action.Left qualified as L +import Control.Monad.Action.Right qualified as R +import Control.Monad.Except +import Control.Monad.Identity +import Control.Monad.Reader +import Control.Monad.State +import Control.Monad.Trans.Compose +import Control.Monad.Trans.Free (FreeF (..), FreeT (..)) +import Control.Monad.Trans.Maybe +import Control.Monad.Writer +import Data.Functor.Classes (Eq1) +import Data.Functor.Compose +import Data.Monoid +import Test.QuickCheck +import Test.QuickCheck.Checkers +import Test.Tasty +import Test.Tasty.QuickCheck + +leftmodule :: + forall m f a. + ( LeftModule m f, + Arbitrary (f a), + Arbitrary (m (m (f a))), + Show (f a), + Show (m (m (f a))), + EqProp (f a) + ) => + TestBatch +leftmodule = + ( "left module laws", + [ ("left identity", property leftP), + ("associativity", property assocP) + ] + ) + where + leftP :: f a -> Property + assocP :: m (m (f a)) -> Property + + leftP a = ljoin (pure @m a) =-= a + assocP a = ljoin (join a) =-= ljoin (fmap ljoin a) + +rightmodule :: + forall m f a. + ( RightModule m f, + Arbitrary (f a), + Arbitrary (f (m (m a))), + Show (f a), + Show (f (m (m a))), + EqProp (f a) + ) => + TestBatch +rightmodule = + ( "right module laws", + [ ("right identity", property rightP), + ("associativity", property assocP) + ] + ) + where + rightP :: f a -> Property + assocP :: f (m (m a)) -> Property + + rightP a = rjoin (fmap (pure @m) a) =-= a + assocP a = rjoin (fmap join a) =-= rjoin (rjoin a) + +bimodule :: + forall s t f a. + ( BiModule s t f, + Arbitrary (f a), + Arbitrary (s (f (t a))), + Show (f a), + Show (s (f (t a))), + EqProp (f a) + ) => + TestBatch +bimodule = + ( "bimodule laws", + [ ("associativity 1", property assoc1P), + ("associativity 2", property assoc2P) + ] + ) + where + assoc1P :: s (f (t a)) -> Property + assoc2P :: s (f (t a)) -> Property + + assoc1P a = bijoin a =-= rjoin (ljoin a) + assoc2P a = bijoin a =-= ljoin (fmap rjoin a) + +instance (CoArbitrary s, Arbitrary (m (a, s)), Function s) => Arbitrary (StateT s m a) where + arbitrary = StateT . applyFun <$> arbitrary + +deriving instance (Show s, Arbitrary s, EqProp (m (a, s))) => EqProp (StateT s m a) + +deriving instance (Arbitrary (m (Maybe a))) => Arbitrary (MaybeT m a) + +deriving instance (EqProp (m (Maybe a))) => EqProp (MaybeT m a) + +deriving instance (Arbitrary (m (Either e a))) => Arbitrary (ExceptT e m a) + +deriving instance (EqProp (m (Either e a))) => EqProp (ExceptT e m a) + +deriving instance (Arbitrary ((s (t (m))) a)) => Arbitrary (ComposeT s t m a) + +deriving instance (EqProp ((s (t (m))) a)) => EqProp (ComposeT s t m a) + +rightmodulestate :: + forall m s a. + ( Monad m, + Arbitrary a, + Function s, + CoArbitrary s, + Arbitrary (m (a, s)), + Show s, + Show (m (a, s)), + Arbitrary (m (m a, s)), + Show (m (m a, s)), + Arbitrary s, + EqProp (m (a, s)), + Arbitrary (m (m (m a), s)), + Show (m (m (m a), s)) + ) => + TestBatch +rightmodulestate = + ( "right module laws", + [ ("right identity", property rightP), + ("associativity", property assocP) + ] + ) + where + rightP :: Fun s (m (a, s)) -> Property + assocP :: Fun s (m (m (m a), s)) -> Property + + rightP a = rjoin (fmap (pure @m) (StateT $ applyFun a)) =-= StateT (applyFun a) + assocP a = rjoin (fmap join (StateT $ applyFun a)) =-= rjoin (rjoin (StateT $ applyFun a)) + +leftmodulestate :: + forall m s a. + ( Monad m, + Arbitrary a, + Function s, + CoArbitrary s, + Arbitrary (m (Fun s (m (a, s)))), + Show (m (Fun s (m (a, s)))), + Arbitrary (m (m (Fun s (m (a, s))))), + Show (m (m (Fun s (m (a, s))))), + EqProp (m (StateT s m a)), + Show s, + Arbitrary s, + EqProp (m (a, s)) + ) => + TestBatch +leftmodulestate = + ( "left module laws", + [ ("left identity", property leftP), + ("associativity", property assocP) + ] + ) + where + leftP :: m (Fun s (m (a, s))) -> Property + assocP :: m (m (Fun s (m (a, s)))) -> Property + + leftP a = ljoin (pure @m (StateT . applyFun <$> a)) =-= (StateT . applyFun <$> a) + assocP a = ljoin (join (fmap (StateT . applyFun) <$> a)) =-= ljoin (fmap ljoin (fmap (StateT . applyFun) <$> a)) + +bimodulestate :: + forall m s a. + ( Monad m, + Arbitrary a, + Arbitrary (m (Fun s (m (m a), s))), + Show (m (Fun s (m (m a), s))), + Arbitrary (m (Fun s (m (m a, s)))), + Show (m (Fun s (m (m a, s)))), + Show s, + Arbitrary s, + EqProp (m (a, s)) + ) => + TestBatch +bimodulestate = + ( "bimodule laws", + [ ("associativity 1", property assoc1P), + ("associativity 2", property assoc2P) + ] + ) + where + assoc1P :: m (Fun s (m (m a, s))) -> Property + assoc2P :: m (Fun s (m (m a, s))) -> Property + + assoc1P a = bijoin (StateT . applyFun <$> a) =-= rjoin (ljoin (StateT . applyFun <$> a)) + assoc2P a = bijoin (StateT . applyFun <$> a) =-= ljoin (fmap rjoin (StateT . applyFun <$> a)) + +instance (Show s, Arbitrary s, EqProp (m a)) => EqProp (ReaderT s m a) where + a =-= b = runReaderT a =-= runReaderT b + +rightmodulereader :: + forall m s a. + ( Monad m, + Arbitrary a, + Function s, + CoArbitrary s, + Arbitrary (m a), + Arbitrary (m (m (m a))), + Show (m a), + Show (m (m (m a))), + Show s, + Arbitrary s, + EqProp (m a) + ) => + TestBatch +rightmodulereader = + ( "right module laws", + [ ("right identity", property rightP), + ("associativity", property assocP) + ] + ) + where + rightP :: Fun s (m a) -> Property + assocP :: Fun s (m (m (m a))) -> Property + + rightP a = rjoin (fmap (pure @m) (ReaderT $ applyFun a)) =-= ReaderT (applyFun a) + assocP a = rjoin (fmap join (ReaderT $ applyFun a)) =-= rjoin (rjoin (ReaderT $ applyFun a)) + +instance (Arbitrary (m (a, w))) => Arbitrary (WriterT w m a) where + arbitrary = WriterT <$> arbitrary + +instance (EqProp (m (a, w))) => EqProp (WriterT w m a) where + a =-= b = runWriterT a =-= runWriterT b + +ldotest :: StateT Char [] Int +ldotest = L.do + x <- [1, 2, 3, 4, 5] + g <- get @_ @(StateT Char []) + put @_ @(StateT Char []) $ succ g + pure $ x * x + +rdotest :: Compose ZipList [] Int +rdotest = R.do + x <- Compose $ ZipList [[1, 2, 3], [4, 5, 6], [7, 8, 9]] + [x * x, x] + +instance (Arbitrary1 f) => Arbitrary2 (FreeF f) where liftArbitrary2 a b = oneof [Pure <$> a, Free <$> liftArbitrary b] + +instance (Functor f, Functor m, Arbitrary1 m, Arbitrary1 f) => Arbitrary1 (FreeT f m) where + liftArbitrary a = FreeT <$> liftArbitrary (liftArbitrary2 a $ liftArbitrary a) + +instance (Functor f, Functor m, Arbitrary1 m, Arbitrary1 f, Arbitrary a) => Arbitrary (FreeT f m a) where + arbitrary = liftArbitrary arbitrary + +instance (EqProp a, EqProp (f b)) => EqProp (FreeF f a b) + +instance (Eq1 f, Eq1 m, Eq a) => EqProp (FreeT f m a) where + (=-=) = eq + +main :: IO () +main = + L.do + print (getCompose rdotest) + print (runStateT ldotest 'a') + defaultMain + ( testGroup "monad action laws" $ + uncurry testProperties + <$> [ leftmodule @Maybe @[] @Int, + rightmodule @Maybe @[] @Int, + rightmodule @(Either Int) @Maybe @Int, + leftmodule @(Either Char) @Maybe @Int, + bimodule @(Either Char) @(Either Bool) @Maybe @Int, + bimodule @(Either Char) @(Either Int) @Maybe @Int, + bimodule @Maybe @(Either Int) @Maybe @Int, + bimodule @(Either Char) @Maybe @Maybe @Int, + rightmodule @(Either Int) @(MaybeT []) @Int, + leftmodule @(Either Int) @(MaybeT []) @Int, + bimodule @(Either Int) @(Either [Bool]) @(MaybeT []) @Int, + rightmodule @(Either (Sum Int)) @(ExceptT (Sum Int) []) @Int, + leftmodule @(Either (Sum Int)) @(ExceptT (Sum Int) []) @Int, + bimodule @(Either (Sum Int)) @(Either (Sum Int)) @(ExceptT (Sum Int) []) @Int, + rightmodule @Maybe @(ExceptT (Sum Int) []) @Int, + leftmodule @Maybe @(ExceptT (Sum Int) []) @Int, + bimodule @(Either (Sum Int)) @Maybe @(ExceptT (Sum Int) []) @Int, + rightmodule @[] @(ComposeT MaybeT (ExceptT Bool) []) @Int, + leftmodule @[] @(ComposeT MaybeT (ExceptT Bool) []) @Int, + rightmodule @Maybe @(MaybeT []) @Int, + leftmodule @Maybe @(MaybeT []) @Int, + bimodule @Maybe @Maybe @(MaybeT []) @Int, + -- , bimodule @Maybe @Maybe @[] @Int + -- , leftmodule @[] @(Compose [] ((,) Bool)) @Bool + -- , rightmodule @Maybe @(Compose ((,) Bool) []) @Bool + -- , bimodule @Maybe @Maybe @(Compose [] (Compose (Either Bool) Maybe)) @Bool + -- , leftmodule @Maybe @[] @Int + -- , rightmodule @Maybe @[] @Int + -- , bimodule @Maybe @Maybe @[] @Int + -- , bimodule @Maybe @[] @[] @Int + -- , bimodule @[] @Maybe @[] @Int + -- , bimodule @[] @[] @[] @Int + leftmodule @Maybe @(MaybeT Maybe) @Int, + -- leftmodule @[] @(MaybeT (MaybeT [])) @Int, -- this would require undecidable instances + leftmodule @(Either String) @(MaybeT (ExceptT String [])) @Int, + leftmodule @Identity @Identity @Int, + leftmodule @Maybe @(FreeT Maybe Maybe) @Int, + rightmodulestate @(WriterT (Product Int) (Either Double)) @Int @Char + -- , rightmodulereader @(WriterT (Product Int) (Either Double)) @Int @Char + -- , rightmodulereader @(Either Bool) @Char @Int + + -- , leftmodulestate @(Writer (Sum Int)) @Int @Bool + -- , rightmodulestate @(Writer (Sum Int)) @Int @Bool + -- , rightmodulestate @(Either Bool) @Int @Bool + -- , bimodulestate @(WriterT (Sum Int) Maybe) @Int @Bool + -- , rightmodule @(Writer (Sum Float)) @(Writer (Sum Float)) @Int -- this should fail because Sum Float is not a monoid + -- , leftmodule @(Writer (Sum Float)) @(Writer (Sum Float)) @Int -- this should fail because Sum Float is not a monoid + ] + )