diff --git a/ChangeLog.md b/ChangeLog.md new file mode 100644 --- /dev/null +++ b/ChangeLog.md @@ -0,0 +1,3 @@ +# Changelog for free-algebras + +## Unreleased changes diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,373 @@ +Mozilla Public License Version 2.0 +================================== + +1. Definitions +-------------- + +1.1. "Contributor" + means each individual or legal entity that creates, contributes to + the creation of, or owns Covered Software. + +1.2. "Contributor Version" + means the combination of the Contributions of others (if any) used + by a Contributor and that particular Contributor's Contribution. + +1.3. "Contribution" + means Covered Software of a particular Contributor. + +1.4. "Covered Software" + means Source Code Form to which the initial Contributor has attached + the notice in Exhibit A, the Executable Form of such Source Code + Form, and Modifications of such Source Code Form, in each case + including portions thereof. + +1.5. "Incompatible With Secondary Licenses" + means + + (a) that the initial Contributor has attached the notice described + in Exhibit B to the Covered Software; or + + (b) that the Covered Software was made available under the terms of + version 1.1 or earlier of the License, but not also under the + terms of a Secondary License. + +1.6. "Executable Form" + means any form of the work other than Source Code Form. + +1.7. "Larger Work" + means a work that combines Covered Software with other material, in + a separate file or files, that is not Covered Software. + +1.8. "License" + means this document. + +1.9. "Licensable" + means having the right to grant, to the maximum extent possible, + whether at the time of the initial grant or subsequently, any and + all of the rights conveyed by this License. + +1.10. "Modifications" + means any of the following: + + (a) any file in Source Code Form that results from an addition to, + deletion from, or modification of the contents of Covered + Software; or + + (b) any new file in Source Code Form that contains any Covered + Software. + +1.11. "Patent Claims" of a Contributor + means any patent claim(s), including without limitation, method, + process, and apparatus claims, in any patent Licensable by such + Contributor that would be infringed, but for the grant of the + License, by the making, using, selling, offering for sale, having + made, import, or transfer of either its Contributions or its + Contributor Version. + +1.12. "Secondary License" + means either the GNU General Public License, Version 2.0, the GNU + Lesser General Public License, Version 2.1, the GNU Affero General + Public License, Version 3.0, or any later versions of those + licenses. + +1.13. "Source Code Form" + means the form of the work preferred for making modifications. + +1.14. "You" (or "Your") + means an individual or a legal entity exercising rights under this + License. For legal entities, "You" includes any entity that + controls, is controlled by, or is under common control with You. For + purposes of this definition, "control" means (a) the power, direct + or indirect, to cause the direction or management of such entity, + whether by contract or otherwise, or (b) ownership of more than + fifty percent (50%) of the outstanding shares or beneficial + ownership of such entity. + +2. License Grants and Conditions +-------------------------------- + +2.1. Grants + +Each Contributor hereby grants You a world-wide, royalty-free, +non-exclusive license: + +(a) under intellectual property rights (other than patent or trademark) + Licensable by such Contributor to use, reproduce, make available, + modify, display, perform, distribute, and otherwise exploit its + Contributions, either on an unmodified basis, with Modifications, or + as part of a Larger Work; and + +(b) under Patent Claims of such Contributor to make, use, sell, offer + for sale, have made, import, and otherwise transfer either its + Contributions or its Contributor Version. + +2.2. Effective Date + +The licenses granted in Section 2.1 with respect to any Contribution +become effective for each Contribution on the date the Contributor first +distributes such Contribution. + +2.3. Limitations on Grant Scope + +The licenses granted in this Section 2 are the only rights granted under +this License. No additional rights or licenses will be implied from the +distribution or licensing of Covered Software under this License. +Notwithstanding Section 2.1(b) above, no patent license is granted by a +Contributor: + +(a) for any code that a Contributor has removed from Covered Software; + or + +(b) for infringements caused by: (i) Your and any other third party's + modifications of Covered Software, or (ii) the combination of its + Contributions with other software (except as part of its Contributor + Version); or + +(c) under Patent Claims infringed by Covered Software in the absence of + its Contributions. + +This License does not grant any rights in the trademarks, service marks, +or logos of any Contributor (except as may be necessary to comply with +the notice requirements in Section 3.4). + +2.4. Subsequent Licenses + +No Contributor makes additional grants as a result of Your choice to +distribute the Covered Software under a subsequent version of this +License (see Section 10.2) or under the terms of a Secondary License (if +permitted under the terms of Section 3.3). + +2.5. Representation + +Each Contributor represents that the Contributor believes its +Contributions are its original creation(s) or it has sufficient rights +to grant the rights to its Contributions conveyed by this License. + +2.6. Fair Use + +This License is not intended to limit any rights You have under +applicable copyright doctrines of fair use, fair dealing, or other +equivalents. + +2.7. Conditions + +Sections 3.1, 3.2, 3.3, and 3.4 are conditions of the licenses granted +in Section 2.1. + +3. Responsibilities +------------------- + +3.1. Distribution of Source Form + +All distribution of Covered Software in Source Code Form, including any +Modifications that You create or to which You contribute, must be under +the terms of this License. You must inform recipients that the Source +Code Form of the Covered Software is governed by the terms of this +License, and how they can obtain a copy of this License. You may not +attempt to alter or restrict the recipients' rights in the Source Code +Form. + +3.2. Distribution of Executable Form + +If You distribute Covered Software in Executable Form then: + +(a) such Covered Software must also be made available in Source Code + Form, as described in Section 3.1, and You must inform recipients of + the Executable Form how they can obtain a copy of such Source Code + Form by reasonable means in a timely manner, at a charge no more + than the cost of distribution to the recipient; and + +(b) You may distribute such Executable Form under the terms of this + License, or sublicense it under different terms, provided that the + license for the Executable Form does not attempt to limit or alter + the recipients' rights in the Source Code Form under this License. + +3.3. Distribution of a Larger Work + +You may create and distribute a Larger Work under terms of Your choice, +provided that You also comply with the requirements of this License for +the Covered Software. If the Larger Work is a combination of Covered +Software with a work governed by one or more Secondary Licenses, and the +Covered Software is not Incompatible With Secondary Licenses, this +License permits You to additionally distribute such Covered Software +under the terms of such Secondary License(s), so that the recipient of +the Larger Work may, at their option, further distribute the Covered +Software under the terms of either this License or such Secondary +License(s). + +3.4. Notices + +You may not remove or alter the substance of any license notices +(including copyright notices, patent notices, disclaimers of warranty, +or limitations of liability) contained within the Source Code Form of +the Covered Software, except that You may alter any license notices to +the extent required to remedy known factual inaccuracies. + +3.5. Application of Additional Terms + +You may choose to offer, and to charge a fee for, warranty, support, +indemnity or liability obligations to one or more recipients of Covered +Software. However, You may do so only on Your own behalf, and not on +behalf of any Contributor. You must make it absolutely clear that any +such warranty, support, indemnity, or liability obligation is offered by +You alone, and You hereby agree to indemnify every Contributor for any +liability incurred by such Contributor as a result of warranty, support, +indemnity or liability terms You offer. You may include additional +disclaimers of warranty and limitations of liability specific to any +jurisdiction. + +4. Inability to Comply Due to Statute or Regulation +--------------------------------------------------- + +If it is impossible for You to comply with any of the terms of this +License with respect to some or all of the Covered Software due to +statute, judicial order, or regulation then You must: (a) comply with +the terms of this License to the maximum extent possible; and (b) +describe the limitations and the code they affect. Such description must +be placed in a text file included with all distributions of the Covered +Software under this License. Except to the extent prohibited by statute +or regulation, such description must be sufficiently detailed for a +recipient of ordinary skill to be able to understand it. + +5. Termination +-------------- + +5.1. The rights granted under this License will terminate automatically +if You fail to comply with any of its terms. However, if You become +compliant, then the rights granted under this License from a particular +Contributor are reinstated (a) provisionally, unless and until such +Contributor explicitly and finally terminates Your grants, and (b) on an +ongoing basis, if such Contributor fails to notify You of the +non-compliance by some reasonable means prior to 60 days after You have +come back into compliance. Moreover, Your grants from a particular +Contributor are reinstated on an ongoing basis if such Contributor +notifies You of the non-compliance by some reasonable means, this is the +first time You have received notice of non-compliance with this License +from such Contributor, and You become compliant prior to 30 days after +Your receipt of the notice. + +5.2. If You initiate litigation against any entity by asserting a patent +infringement claim (excluding declaratory judgment actions, +counter-claims, and cross-claims) alleging that a Contributor Version +directly or indirectly infringes any patent, then the rights granted to +You by any and all Contributors for the Covered Software under Section +2.1 of this License shall terminate. + +5.3. In the event of termination under Sections 5.1 or 5.2 above, all +end user license agreements (excluding distributors and resellers) which +have been validly granted by You or Your distributors under this License +prior to termination shall survive termination. + +************************************************************************ +* * +* 6. Disclaimer of Warranty * +* ------------------------- * +* * +* Covered Software is provided under this License on an "as is" * +* basis, without warranty of any kind, either expressed, implied, or * +* statutory, including, without limitation, warranties that the * +* Covered Software is free of defects, merchantable, fit for a * +* particular purpose or non-infringing. The entire risk as to the * +* quality and performance of the Covered Software is with You. * +* Should any Covered Software prove defective in any respect, You * +* (not any Contributor) assume the cost of any necessary servicing, * +* repair, or correction. This disclaimer of warranty constitutes an * +* essential part of this License. No use of any Covered Software is * +* authorized under this License except under this disclaimer. * +* * +************************************************************************ + +************************************************************************ +* * +* 7. Limitation of Liability * +* -------------------------- * +* * +* Under no circumstances and under no legal theory, whether tort * +* (including negligence), contract, or otherwise, shall any * +* Contributor, or anyone who distributes Covered Software as * +* permitted above, be liable to You for any direct, indirect, * +* special, incidental, or consequential damages of any character * +* including, without limitation, damages for lost profits, loss of * +* goodwill, work stoppage, computer failure or malfunction, or any * +* and all other commercial damages or losses, even if such party * +* shall have been informed of the possibility of such damages. This * +* limitation of liability shall not apply to liability for death or * +* personal injury resulting from such party's negligence to the * +* extent applicable law prohibits such limitation. Some * +* jurisdictions do not allow the exclusion or limitation of * +* incidental or consequential damages, so this exclusion and * +* limitation may not apply to You. * +* * +************************************************************************ + +8. Litigation +------------- + +Any litigation relating to this License may be brought only in the +courts of a jurisdiction where the defendant maintains its principal +place of business and such litigation shall be governed by laws of that +jurisdiction, without reference to its conflict-of-law provisions. +Nothing in this Section shall prevent a party's ability to bring +cross-claims or counter-claims. + +9. Miscellaneous +---------------- + +This License represents the complete agreement concerning the subject +matter hereof. If any provision of this License is held to be +unenforceable, such provision shall be reformed only to the extent +necessary to make it enforceable. Any law or regulation which provides +that the language of a contract shall be construed against the drafter +shall not be used to construe this License against a Contributor. + +10. Versions of the License +--------------------------- + +10.1. New Versions + +Mozilla Foundation is the license steward. Except as provided in Section +10.3, no one other than the license steward has the right to modify or +publish new versions of this License. Each version will be given a +distinguishing version number. + +10.2. Effect of New Versions + +You may distribute the Covered Software under the terms of the version +of the License under which You originally received the Covered Software, +or under the terms of any subsequent version published by the license +steward. + +10.3. Modified Versions + +If you create software not governed by this License, and you want to +create a new license for such software, you may create and use a +modified version of this License if you rename the license and remove +any references to the name of the license steward (except to note that +such modified license differs from this License). + +10.4. Distributing Source Code Form that is Incompatible With Secondary +Licenses + +If You choose to distribute Source Code Form that is Incompatible With +Secondary Licenses under the terms of this version of the License, the +notice described in Exhibit B of this License must be attached. + +Exhibit A - Source Code Form License Notice +------------------------------------------- + + This Source Code Form is subject to the terms of the Mozilla Public + License, v. 2.0. If a copy of the MPL was not distributed with this + file, You can obtain one at http://mozilla.org/MPL/2.0/. + +If it is not possible or desirable to put the notice in a particular +file, then You may include the notice in a location (such as a LICENSE +file in a relevant directory) where a recipient would be likely to look +for such a notice. + +You may add additional accurate notices of copyright ownership. + +Exhibit B - "Incompatible With Secondary Licenses" Notice +--------------------------------------------------------- + + This Source Code Form is "Incompatible With Secondary Licenses", as + defined by the Mozilla Public License, v. 2.0. diff --git a/README.md b/README.md new file mode 100644 --- /dev/null +++ b/README.md @@ -0,0 +1,8 @@ +# Free Algebras + +Universal algebra approach to free algebras (including higher order structures +like functors, applicative functors or monads). Mathematical introduction +alongside with some Haskell ideas can be found +[here](https://marcinszamotulski.me/posts/free-monads.html). + +For an example check out [this](https://github.com/coot/free-algebras/blob/master/example/src/Network/TCP.hs). diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/free-algebras.cabal b/free-algebras.cabal new file mode 100644 --- /dev/null +++ b/free-algebras.cabal @@ -0,0 +1,88 @@ +-- This file has been generated from package.yaml by hpack version 0.28.2. +-- +-- see: https://github.com/sol/hpack +-- +-- hash: 8252360922bbd229818e963e538ab0a45e583719ce19477848aa674083eb9377 + +name: free-algebras +version: 0.0.1.0 +description: Please see the README on GitHub at +homepage: https://github.com/coot/free-algebras#readme +bug-reports: https://github.com/git@github.com:coot/free-algebras/issues +author: Marcin Szamotulski +maintainer: profunctor@pm.me +copyright: (c) 2018 Marcin Szamotulski +license: MPL-2.0 +license-file: LICENSE +build-type: Simple +cabal-version: >= 1.10 +extra-source-files: + ChangeLog.md + README.md + +source-repository head + type: git + location: https://github.com/git@github.com:coot/free-algebras + +flag develop + description: Set -Werror flag + manual: True + default: False + +library + exposed-modules: + Control.Algebra.Free + Control.Monad.Action + Data.Algebra.Free + Data.Algebra.Pointed + Data.Group.Free + Data.Monoid.Abelian + Data.Monoid.MSet + Data.Semigroup.Abelian + Data.Semigroup.SemiLattice + Data.Semigroup.SSet + other-modules: + Paths_free_algebras + hs-source-dirs: + src + default-extensions: ConstraintKinds DataKinds DeriveFunctor EmptyDataDecls FlexibleInstances FlexibleContexts KindSignatures InstanceSigs MultiParamTypeClasses OverloadedStrings PolyKinds RankNTypes ScopedTypeVariables TupleSections TypeApplications TypeFamilies + build-depends: + base >=4.11 && <5 + , containers + , data-fix + , free + , groups + , kan-extensions + , mtl + , natural-numbers + , transformers + if flag(develop) + ghc-options: -Werror -Wall -Wincomplete-record-updates -Wincomplete-uni-patterns -Wredundant-constraints -Wno-deprecations + else + ghc-options: -Wall -Wincomplete-record-updates -Wincomplete-uni-patterns -Wredundant-constraints -Wno-deprecations + default-language: Haskell2010 + +test-suite free-algebras-test + type: exitcode-stdio-1.0 + main-is: Spec.hs + other-modules: + Test.Control.Algebra.Free + Test.Data.Algebra.Free + Paths_free_algebras + hs-source-dirs: + test + default-extensions: ConstraintKinds DataKinds DeriveFunctor EmptyDataDecls FlexibleInstances FlexibleContexts KindSignatures InstanceSigs MultiParamTypeClasses OverloadedStrings PolyKinds RankNTypes ScopedTypeVariables TupleSections TypeApplications TypeFamilies + ghc-options: -threaded -rtsopts -with-rtsopts=-N -main-is Spec + build-depends: + base >=4.11 && <5 + , containers + , data-fix + , free + , free-algebras + , groups + , hedgehog + , kan-extensions + , mtl + , natural-numbers + , transformers + default-language: Haskell2010 diff --git a/src/Control/Algebra/Free.hs b/src/Control/Algebra/Free.hs new file mode 100644 --- /dev/null +++ b/src/Control/Algebra/Free.hs @@ -0,0 +1,569 @@ +{-# LANGUAGE GADTs #-} +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +module Control.Algebra.Free + ( + -- * Classes + AlgebraType0 + , AlgebraType + , Proof (..) + , FreeAlgebra1 (..) + -- * Combinators + , wrapFree + , foldFree1 + , unFoldNatFree + , hoistFree1 + , hoistFreeH + , joinFree1 + , bindFree1 + , assocFree1 + , iterFree1 + , cataFree1 + -- * Day convolution + , DayF (..) + , dayToAp + , apToDay + -- * Various classes (higher algebra types) + , MonadList (..) + , MonadMaybe (..) + ) where + +import Control.Applicative (Alternative) +import Control.Applicative.Free (Ap) +import qualified Control.Applicative.Free as Ap +import qualified Control.Applicative.Free.Fast as Fast +import qualified Control.Applicative.Free.Final as Final +import Control.Alternative.Free (Alt (..)) +import qualified Control.Alternative.Free as Alt +import Control.Monad (foldM, join) +import Control.Monad.Except (ExceptT (..), MonadError (..)) +import Control.Monad.Free (Free) +import qualified Control.Monad.Free as Free +import qualified Control.Monad.Free.Church as Church +import Control.Monad.List (ListT (..)) +import Control.Monad.Reader (MonadReader (..), ReaderT (..)) +import Control.Monad.RWS.Class (MonadRWS) +import Control.Monad.RWS.Lazy as L (RWST (..)) +import Control.Monad.RWS.Strict as S (RWST (..)) +import Control.Monad.State.Class (MonadState (..)) +import qualified Control.Monad.State.Lazy as L (StateT (..)) +import qualified Control.Monad.State.Strict as S (StateT (..)) +import Control.Monad.Trans (lift) +import Control.Monad.Trans.Maybe (MaybeT (..)) +import Control.Monad.Writer.Class (MonadWriter (..)) +import qualified Control.Monad.Writer.Lazy as L (WriterT (..)) +import qualified Control.Monad.Writer.Strict as S (WriterT (..)) +import Data.Kind (Type) +import Data.Fix (Fix, cataM) +import Data.Functor.Coyoneda (Coyoneda (..), liftCoyoneda) +import Data.Functor.Day (Day (..)) +import qualified Data.Functor.Day as Day +import Data.Functor.Identity (Identity (..)) + +import Data.Algebra.Free (AlgebraType, AlgebraType0, Proof (..)) + +-- | +-- Higher kinded version of @'FreeAlgebra'@. Instances includes free functors, +-- free applicative functors, free monads, state monads etc. +-- +-- A lawful instance should guarantee that @'foldNatFree'@ is an isomorphism +-- with inversese @'unFoldNatFree'@. +-- +-- This guaranties that @m@ is a left adjoint functor from the category of +-- types of kind @Type -> Type@ which satisfy @'AlgebraType0' m@ constraint, to the +-- category of types of kind @Type -> Type@ which satisfy the @'AlgebraType' m@ +-- constraint. This functor is left afjoin to the forgetful functor (which is +-- well defined if the laws on @'AlgebraType0'@ family are satisfied. This in +-- turn guarantess that @m@ componsed with this forgetful functor is a monad. +-- In result we get the monadic combinators: @'liftFree'@ (@'return'@ of +-- this monad) and @'bindFree1'@ (its @'bind'@) and @'joinFree1'@ - its +-- @'join'@ operator. +class FreeAlgebra1 (m :: (Type -> Type) -> Type -> Type) where + -- | Natural transformation that embeds generators into @m@. + liftFree :: AlgebraType0 m f => f a -> m f a + + -- | The freeness property. + foldNatFree + :: forall (d :: Type -> Type) f a . + ( AlgebraType m d + , AlgebraType0 m f + ) + => (forall x. f x -> d x) + -- ^ natural transformation which embeds generators of @m@ into @d@ + -> (m f a -> d a) + -- ^ a homomorphism from @m f@ to @d@ + + -- | + -- A proof that @'AlgebraType0' m (m f)@ holds. + proof0 :: forall f. AlgebraType0 m f => Proof (AlgebraType0 m (m f)) m f + -- | + -- A proof that @'AlgebraType' m (m f)@ holds. + proof1 :: forall f. AlgebraType0 m f => Proof (AlgebraType m (m f)) m f + +-- | +-- Anything that carries @'FreeAlgebra1'@ constraint is also an instance of +-- @'Control.Monad.Free.Class.MonadFree'@, but not vice versa. You can use +-- @'wrap'@ to define the a @'Contorl.Monad.Free.Class.MonadFree'@ instance. +-- @'ContT'@ is an example of a monad which does have an @'FreeAlgebra1'@ +-- instance, but has an @'MonadFree'@ instance. +-- +-- The @'Monad'@ constrain will be satisfied for many monads through the +-- @'AlgebraType m'@ constraint. +wrapFree + :: ( FreeAlgebra1 m + , AlgebraType0 m f + , Monad (m f) + ) + => f (m f a) + -> m f a +wrapFree = join . liftFree + +-- | +-- @'unFoldNatFree'@ is an inverse of @'foldNatFree'@ +unFoldNatFree + :: ( FreeAlgebra1 m + , AlgebraType0 m f + ) + => (forall x . m f x -> d x) + -> f a -> d a +unFoldNatFree nat = nat . liftFree + +-- | +-- @'FreeAlgebra1' m@ implies that @m f@ is a foldable. +-- +-- @ +-- 'foldFree1' . 'liftFree' == 'id' :: f a -> f a +-- @ +-- +-- It can be specialized to: +-- +-- * @'Data.Functor.Coyoneda.lowerCoyoneda' :: 'Functor' f => 'Coyoneda' f a -> f a@ +-- * @'Control.Applicative.Free.retractAp' :: 'Applicative' f => 'Ap' f a -> f a@ +-- * @'Control.Monad.Free.foldFree' :: 'Monad' m => (forall x. f x -> m x) -> 'Free' f a -> m a@ +foldFree1 :: ( FreeAlgebra1 m + , AlgebraType0 m f + , AlgebraType m f + ) + => m f a + -> f a +foldFree1 = foldNatFree id + +-- | +-- This is a functor instance for @m@ when considered as an endofuctor of some +-- subcategory of @Type -> Type@ (e.g. endofunctors of _Hask_). +-- +-- It can be specialized to: +-- +-- * @'Control.Applicative.Free.hoistAp' :: (forall a. f a -> g a) -> 'Ap' f b -> 'Ap' g b @ +-- * @'Control.Monad.Free.hoistFree' :: 'Functor' g => (forall a. f a -> g a) -> 'Free' f b -> 'Free' g b@ +hoistFree1 :: forall m f g a . + ( FreeAlgebra1 m + , AlgebraType0 m g + , AlgebraType0 m f + ) + => (forall x. f x -> g x) -- ^ a natural transformation @f ~> g@ + -> m f a + -> m g a +hoistFree1 = go (proof1 :: Proof (AlgebraType m (m g)) m g) where + go :: Proof (AlgebraType m (m g)) m g -> (forall x. f x -> g x) -> m f a -> m g a + go Proof nat = foldNatFree (liftFree . nat) + {-# INLINE go #-} + +-- | +-- @ +-- 'hoistFreeH' . 'hoistFreeH' = 'hoistFreeH' +-- @ +-- +-- and when @'FreeAlgebra1' m ~ 'FreeAlgebra1' n@: +-- +-- @ +-- 'hoistFreeH' = 'id' +-- @ +hoistFreeH :: forall m n f a . + ( FreeAlgebra1 m + , FreeAlgebra1 n + , AlgebraType0 m f + , AlgebraType0 n f + , AlgebraType m (n f) + ) + => m f a + -> n f a +hoistFreeH = foldNatFree liftFree + +-- | +-- @'joinFree1'@ makes @m@ a monad in some subcatgory of types of kind @Type -> Type@ +-- (usually the end-functor category of @Hask@). It is just a specialization +-- of @'foldFree1'@. +joinFree1 :: forall m f a . + ( FreeAlgebra1 m + , AlgebraType0 m f + ) + => m (m f) a + -> m f a +joinFree1 = go (proof0 :: Proof (AlgebraType0 m (m f)) m f) (proof1 :: Proof (AlgebraType m (m f)) m f) + where + go :: Proof (AlgebraType0 m (m f)) m f -> Proof (AlgebraType m (m f)) m f -> m (m f) a -> m f a + go Proof Proof = foldFree1 + {-# INLINE go #-} + +-- | +-- Bind operator for the @'joinFree1'@ monad +bindFree1 :: forall m f g a . + ( FreeAlgebra1 m + , AlgebraType0 m g + , AlgebraType0 m f + ) + => m f a + -> (forall x . f x -> m g x) -- ^ natural transformation @f ~> m g@ + -> m g a +bindFree1 = go (proof0 :: Proof (AlgebraType0 m (m g)) m g) (proof1 :: Proof (AlgebraType m (m g)) m g) + where + go :: Proof (AlgebraType0 m (m g)) m g -> Proof (AlgebraType m (m g)) m g -> m f a -> (forall x . f x -> m g x) -> m g a + go Proof Proof mfa nat = joinFree1 $ hoistFree1 nat mfa + {-# INLINE go #-} + +assocFree1 :: forall m f a . + ( FreeAlgebra1 m + , AlgebraType m f + , AlgebraType0 m f + , Functor (m (m f)) + ) + => m f (m f a) + -> m (m f) (f a) +assocFree1 = outer (proof0 :: Proof (AlgebraType0 m (m f)) m f) + where + -- `Proof0` is needed to prove `Proof1` + {-# INLINE outer #-} + outer :: Proof (AlgebraType0 m (m f)) m f -> m f (m f a) -> m (m f) (f a) + outer Proof = inner (proof1 :: Proof (AlgebraType m (m (m f))) m (m f)) + where + {-# INLINE inner #-} + inner :: Proof (AlgebraType m (m (m f))) m (m f) -> m f (m f a) -> m (m f) (f a) + inner Proof = fmap g <$> foldNatFree f + + f :: forall x. f x -> m (m f) x + f = hoistFree1 liftFree . liftFree + + g :: m f a -> f a + g = foldFree1 + +-- | +-- @'Fix' (m f)@ is the initial /algebra/ of type @'AlgebraType' m@ and +-- @'AlgebraType0' f@ (whenever it /exists/). +cataFree1 :: forall m f a . + ( FreeAlgebra1 m + , AlgebraType m f + , AlgebraType0 m f + , Monad f + , Traversable (m f) + ) + => Fix (m f) + -> f a +cataFree1 = cataM foldFree1 + +-- | +-- Specialization of @'foldNatFree' \@_ \@'Identity'@; it will further specialize to: +-- +-- * @\\_ -> 'runIdentity' . 'Data.Functor.Coyoneda.lowerCoyoneda'@ +-- * @'Control.Applicative.Free.iterAp' :: 'Functor' g => (g a -> a) -> 'Ap' g a -> a@ +-- * @'Control.Monad.Free.iter' :: 'Functor' f => (f a -> a) -> 'Free' f a -> a@ +iterFree1 :: forall m f a . + ( FreeAlgebra1 m + , AlgebraType0 m f + , AlgebraType m Identity + ) + => (forall x . f x -> x) + -> m f a + -> a +iterFree1 f = runIdentity . foldNatFree @_ @Identity (Identity . f) + +-- Instances + +-- | +-- Algebras of the same type as @'Coyoneda'@ are all functors. +type instance AlgebraType0 Coyoneda g = () +type instance AlgebraType Coyoneda g = Functor g +instance FreeAlgebra1 Coyoneda where + liftFree = liftCoyoneda + foldNatFree nat (Coyoneda ba fx) = ba <$> nat fx + + proof0 = Proof + proof1 = Proof + +-- | +-- Algebras of the same type as @'Ap'@ are the applicative functors. +type instance AlgebraType0 Ap g = Functor g +type instance AlgebraType Ap g = Applicative g +-- | +-- @'Ap'@ is a free in the class of applicative functors, over any functor +-- (@'Ap' f@ is applicative whenever @f@ is a functor) +instance FreeAlgebra1 Ap where + liftFree = Ap.liftAp + foldNatFree = Ap.runAp + + proof0 = Proof + proof1 = Proof + +type instance AlgebraType0 Fast.Ap g = Functor g +type instance AlgebraType Fast.Ap g = Applicative g +instance FreeAlgebra1 Fast.Ap where + liftFree = Fast.liftAp + foldNatFree = Fast.runAp + + proof0 = Proof + proof1 = Proof + +type instance AlgebraType0 Final.Ap g = Functor g +type instance AlgebraType Final.Ap g = Applicative g +instance FreeAlgebra1 Final.Ap where + liftFree = Final.liftAp + foldNatFree = Final.runAp + + proof0 = Proof + proof1 = Proof + +-- | +-- @'Day' f f@ newtype wrapper. It is isomorphic with @'Ap' f@ for applicative +-- functors @f@ via @'dayToAp'@ (and @'apToDay'@). +newtype DayF f a = DayF { runDayF :: Day f f a} + deriving (Functor, Applicative) + +dayToAp :: Applicative f => Day f f a -> Ap f a +dayToAp = hoistFreeH . DayF + +apToDay :: Applicative f => Ap f a -> Day f f a +apToDay = runDayF . hoistFreeH + +-- | +-- Algebras of the same type as @'DayF'@ are all the applicative functors. +type instance AlgebraType0 DayF g = Applicative g +type instance AlgebraType DayF g = Applicative g +-- | +-- @'DayF'@, as @'Ap'@ is a free applicative functor, but over applicative functors +-- (@'DayF' f@ is applicative if @f@ is an applicative functor). +instance FreeAlgebra1 DayF where + liftFree fa = DayF $ Day fa fa const + foldNatFree nat (DayF day) + = Day.dap . Day.trans2 nat . Day.trans1 nat $ day + + proof0 = Proof + proof1 = Proof + +-- | +-- Algebras of the same type as @'Free'@ monad is the class of all monads. +type instance AlgebraType0 Free f = Functor f +type instance AlgebraType Free m = Monad m +-- | +-- @'Free'@ monad is free in the class of monad over the class of functors. +instance FreeAlgebra1 Free where + liftFree = Free.liftF + foldNatFree = Free.foldFree + + proof0 = Proof + proof1 = Proof + +type instance AlgebraType0 Church.F f = Functor f +type instance AlgebraType Church.F m = Monad m +instance FreeAlgebra1 Church.F where + liftFree = Church.liftF + foldNatFree = Church.foldF + + proof0 = Proof + proof1 = Proof + +type instance AlgebraType0 Alt f = Functor f +type instance AlgebraType Alt m = Alternative m +instance FreeAlgebra1 Alt where + liftFree = Alt.liftAlt + foldNatFree = Alt.runAlt + + proof0 = Proof + proof1 = Proof + +-- | +-- Algebras of the same type as @'L.StateT'@ monad is the class of all state +-- monads. +type instance AlgebraType0 (L.StateT s) m = Monad m +type instance AlgebraType (L.StateT s) m = ( MonadState s m ) +-- | +-- Lazy @'L.StateT'@ monad transformer is a free algebra in the class of monads +-- which satisfy the @'MonadState'@ constraint. Note that this instance +-- captures that @'L.StateT' s@ is a monad transformer: +-- +-- @ +-- 'liftFree' = 'lift' +-- @ +-- +-- This is also true for all the other monad transformers. +instance FreeAlgebra1 (L.StateT s) where + liftFree = lift + foldNatFree nat ma = do + (a, s) <- get >>= nat . L.runStateT ma + put s + return a + + proof0 = Proof + proof1 = Proof + +-- | +-- Algebras of the same type as @'S.StateT'@ monad is the class of all state +-- monads. +type instance AlgebraType0 (S.StateT s) m = Monad m +type instance AlgebraType (S.StateT s) m = ( MonadState s m ) +-- | +-- Strict @'S.StateT'@ monad transformer is also a free algebra, thus @'hoistFreeH'@ +-- is an isomorphism between the strict and lazy versions. +instance FreeAlgebra1 (S.StateT s) where + liftFree :: Monad m => m a -> S.StateT s m a + liftFree = lift + foldNatFree nat ma = do + (a, s) <- get >>= nat . S.runStateT ma + put s + return a + + proof0 = Proof + proof1 = Proof + +-- | +-- Algebras of the same type as @'L.WriterT'@ monad is the class of all writer +-- monads. +type instance AlgebraType0 (L.WriterT w) m = ( Monad m, Monoid w ) +type instance AlgebraType (L.WriterT w) m = ( MonadWriter w m ) +-- | +-- Lazy @'L.WriterT'@ is free for algebras of type @'MonadWriter'@. +instance FreeAlgebra1 (L.WriterT w) where + liftFree = lift + foldNatFree nat (L.WriterT m) = fst <$> nat m + + proof0 = Proof + proof1 = Proof + +-- | +-- Algebras of the same type as @'S.WriterT'@ monad is the class of all writer +-- monads. +type instance AlgebraType0 (S.WriterT w) m = ( Monad m, Monoid w ) +type instance AlgebraType (S.WriterT w) m = ( MonadWriter w m ) +-- | +-- Strict @'S.WriterT'@ monad transformer is a free algebra among all +-- @'MonadWriter'@s. +instance FreeAlgebra1 (S.WriterT w) where + liftFree = lift + foldNatFree nat (S.WriterT m) = fst <$> nat m + + proof0 = Proof + proof1 = Proof + +-- | +-- Algebras of the same type as @'L.ReaderT'@ monad is the class of all reader +-- monads. +type instance AlgebraType0 (ReaderT r) m = ( Monad m ) +type instance AlgebraType (ReaderT r) m = ( MonadReader r m ) +-- | +-- @'ReaderT'@ is a free monad in the class of all @'MonadReader'@ monads. +instance FreeAlgebra1 (ReaderT r) where + liftFree = lift + foldNatFree nat (ReaderT g) = + ask >>= nat . g + + proof0 = Proof + proof1 = Proof + +-- | +-- Algebras of the same type as @'S.ReaderT'@ monad is the class of all reader +-- monads. +type instance AlgebraType0 (ExceptT e) m = ( Monad m ) +type instance AlgebraType (ExceptT e) m = ( MonadError e m ) +-- | +-- @'ExceptT' e@ is a free algebra among all @'MonadError' e@ monads. +instance FreeAlgebra1 (ExceptT e) where + liftFree = lift + foldNatFree nat (ExceptT m) = do + ea <- nat m + case ea of + Left e -> throwError e + Right a -> return a + + proof0 = Proof + proof1 = Proof + +type instance AlgebraType0 (L.RWST r w s) m = ( Monad m, Monoid w ) +type instance AlgebraType (L.RWST r w s) m = MonadRWS r w s m +instance FreeAlgebra1 (L.RWST r w s) where + liftFree = lift + foldNatFree nat (L.RWST fn) = do + r <- ask + s <- get + (a, s', w) <- nat $ fn r s + put s' + tell w + return a + + proof0 = Proof + proof1 = Proof + +type instance AlgebraType0 (S.RWST r w s) m = ( Monad m, Monoid w ) +type instance AlgebraType (S.RWST r w s) m = MonadRWS r w s m +instance FreeAlgebra1 (S.RWST r w s) where + liftFree = lift + foldNatFree nat (S.RWST fn) = do + r <- ask + s <- get + (a, s', w) <- nat $ fn r s + put s' + tell w + return a + + proof0 = Proof + proof1 = Proof + +-- | +-- Algebra type for @'ListT'@ monad transformer. +class Monad m => MonadList m where + mempty1 :: m a + mappend1 :: m a -> m a -> m a + +mappend1_ :: MonadList m => a -> a -> m a +mappend1_ a b = return a `mappend1` return b + +instance Monad m => MonadList (ListT m) where + mempty1 = ListT (return []) + mappend1 (ListT ma) (ListT mb) = ListT $ mappend <$> ma <*> mb + +type instance AlgebraType0 ListT f = ( Monad f ) +type instance AlgebraType ListT m = ( MonadList m ) +instance FreeAlgebra1 ListT where + liftFree = lift + foldNatFree nat (ListT mas) = do + as <- nat mas + empty <- mempty1 + a <- foldM (\x y -> x `mappend1_` y) empty as + return a + + proof0 = Proof + proof1 = Proof + +-- $monadContT +-- +-- @'ContT' r m@ is not functorial in @m@, so there is no chance it can admit +-- an instance of @'FreeAlgebra1'@ + +-- | +-- A higher version @'Data.Algebra.Pointed'@ class. +-- +-- With @'QuantifiedConstraints'@ this class will be redundant. +class MonadMaybe m where + point :: forall a. m a + +instance Monad m => MonadMaybe (MaybeT m) where + point = MaybeT (return Nothing) + +type instance AlgebraType0 MaybeT m = ( Monad m ) +type instance AlgebraType MaybeT m = ( Monad m, MonadMaybe m ) +instance FreeAlgebra1 MaybeT where + liftFree = lift + foldNatFree nat (MaybeT mma) = + nat mma >>= \ma -> case ma of + Nothing -> point + Just a -> return a + + proof0 = Proof + proof1 = Proof 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,66 @@ +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE UndecidableInstances #-} +module Control.Monad.Action where + +import Control.Monad (join) +import Data.Functor.Const (Const (..)) + +import Control.Algebra.Free + ( AlgebraType0 + , AlgebraType + , FreeAlgebra1 (..) + , Proof (..) + ) +import Data.Algebra.Pointed (Pointed (point)) +import Data.Algebra.Free (FreeAlgebra, foldFree) + +-- | +-- A /monad action/ is an `m`-algebra parametrized over a functor `f`. +-- This is direct translation of a /monoid action/ in the monoidal category of +-- endofunctors with monoidal product: functor composition. +-- +-- @'mact'@ should be /associative/: +-- prop> 'mact' . 'mact' = 'mact' . 'join' +-- and /unital/: +-- prop> mact . return = id +-- +-- There are monads which do not have any (safe) instances, like @'IO'@. +class (Monad m, Functor f) => MAction m f where + mact :: m (f a) -> f a + +instance Monad m => MAction m m where + mact = join + +-- | +-- You can use @'PointedMonoid'@ newtype wrapper if you want to laverage +-- @'Pointed'@ instance for a @'Monoid'@. +instance (Pointed r, Functor f) => MAction ((->) r) f where + mact f = f point + +-- | +-- Every algebra @d@ which satisfies the constraint @'AlgebraType' m d@ lifts +-- to an action on the constant functor @'Const' d@. This is the same as to +-- say that @d@ is an @m@-algebra (as of /f-algebras/ in category theory). +instance ( Monad m + , FreeAlgebra m + , AlgebraType m d + , AlgebraType0 m d + ) + => MAction m (Const d) where + mact mca = Const $ foldFree $ getConst <$> mca + +-- | +-- Free algebra associated with the @'MAction' constraint. +newtype FreeMAction m f a = FreeMAction { runFreeMAction :: m (f a) } + deriving (Show, Eq, Ord, Functor) + +instance (Monad m, Functor f) => MAction m (FreeMAction m f) where + mact mfa = FreeMAction $ join $ runFreeMAction <$> mfa + +type instance AlgebraType (FreeMAction m) f = MAction m f +type instance AlgebraType0 (FreeMAction m) f = Functor f +instance Monad m => FreeAlgebra1 (FreeMAction m) where + liftFree = FreeMAction . return + foldNatFree nat (FreeMAction mfa) = mact $ nat <$> mfa + proof0 = Proof + proof1 = Proof diff --git a/src/Data/Algebra/Free.hs b/src/Data/Algebra/Free.hs new file mode 100644 --- /dev/null +++ b/src/Data/Algebra/Free.hs @@ -0,0 +1,215 @@ +{-# LANGUAGE GADTs #-} +module Data.Algebra.Free + ( -- * Algebra type + AlgebraType + , AlgebraType0 + -- * FreeAlgebra class + , FreeAlgebra (..) + , Proof (..) + -- * Combinators + , unFoldMapFree + , foldFree + , natFree + , fmapFree + , joinFree + , bindFree + , cataFree + ) + where + +import Prelude + +import Data.Fix (Fix, cata) +import Data.Kind (Constraint, Type) +import Data.List.NonEmpty (NonEmpty (..)) +import Data.Monoid (Monoid (..)) +import Data.Semigroup (Semigroup, (<>)) + +import Data.Algebra.Pointed (Pointed (..)) + +-- | +-- Type family which for each free algebra @m@ returns a type level lambda from +-- types to constraints. It is describe the class of algebras for which this +-- free algebra is free. +-- +-- A lawful instance for this type family must guarantee +-- that the constraint @'AlgebraType0' m f@ is implied by the @'AlgebraType' +-- m f@ constraint. This guaranees that there exists a forgetful functor from +-- the category of types of kind @* -> *@ which satisfy @'AlgebraType' m@ +-- constrain to the category of types of kind @* -> *@ which satisfy the +-- @'AlgebraType0 m@ constraint. +type family AlgebraType (f :: k) (a :: l) :: Constraint + +-- | +-- Type family which limits Hask to its full subcategory which satisfies +-- a given constraints. Some free algebras, like free groups, or free abelian +-- semigroups have additional constraints on on generators, like @Eq@ or @Ord@. +type family AlgebraType0 (f :: k) (a :: l) :: Constraint + +-- | +-- Proof that @a@ is an algebra of type @'AlgebraType' m a@. +data Proof (c :: Constraint) (f :: k) (a :: l) where + Proof :: c => Proof c f a + +-- | +-- A lawful instance has to guarantee that @'unFoldFree'@ is an inverse of +-- @'foldMapFree'@. +-- +-- This in turn guaranties that @m@ is a left adjoint functor from Hask to +-- algebras of type @'AlgebraType m'@. The right adjoint is the forgetful +-- functor. The composition of left adjoin and the right one is always +-- a monad, this is why we will be able to build monad instance for @m@. +class FreeAlgebra (m :: Type -> Type) where + -- | Injective map that embeds generators @a@ into @m@. + returnFree :: a -> m a + -- | The freeness property. + foldMapFree + :: forall d a + . ( AlgebraType m d + , AlgebraType0 m a + ) + => (a -> d) -- ^ map generators of @m@ into @d@ + -> (m a -> d) -- ^ returns a homomorphism from @m a@ to @d@ + + -- | Proof that @'AlgebraType' m (m a)@ holds, e.g. if @m ~ []@ + -- then @[a]@ is a monoid for all @a@. + proof :: forall a. AlgebraType0 m a => Proof (AlgebraType m (m a)) m a + +-- | +-- Inverse of @'foldMapFree'@ +unFoldMapFree + :: FreeAlgebra m + => (m a -> d) + -> (a -> d) +unFoldMapFree f = f . returnFree + +-- | +-- All types which satisfy @'FreeAlgebra'@ constraint are foldable. You can +-- use this map to build a @'Foldable'@ instance. +-- +-- prop> foldFree . returnFree == id +foldFree + :: ( FreeAlgebra m + , AlgebraType0 m a + , AlgebraType m a + ) + => m a + -> a +foldFree = foldMapFree id + +-- | +-- The canonical quotient map from a free algebra of a wider class to a free +-- algebra of a narrower class, e.g. from a free semigroup to +-- free monoid, or from a free monoid to free commutative monoid, +-- etc. +-- +-- prop> natFree . natFree == natFree +-- prop> fmapFree f . natFree == hoistFree . fmapFree f +-- +-- the constraints: +-- * the algebra @n a@ is of the same type as algebra @m@ (this is +-- always true, just ghc cannot prove it here) +-- * @m@ is a free algebra generated by @a@ +-- * @n@ is a free algebra generated by @a@ +natFree :: forall m n a . + ( AlgebraType m (n a) + , AlgebraType0 m a + , FreeAlgebra m + , FreeAlgebra n + ) + => m a + -> n a +natFree = foldMapFree returnFree + +-- | +-- All types which satisfy @'FreeAlgebra'@ constraint are functors. +-- The constraint @'AlgebraType' m (m b)@ is always satisfied. +fmapFree :: forall m a b . + ( FreeAlgebra m + , AlgebraType0 m a + , AlgebraType0 m b + ) + => (a -> b) + -> m a + -> m b +fmapFree = go (proof :: Proof (AlgebraType m (m b)) m b) + where + go :: Proof (AlgebraType m (m b)) m b -> (a -> b) -> m a -> m b + go p f ma = case p of Proof -> foldMapFree (returnFree . f) ma + {-# INLINE go #-} + +-- | +-- @'FreeAlgebra'@ constraint implies @Monad@ constrain. +joinFree :: forall m a . + ( FreeAlgebra m + , AlgebraType0 m a + , AlgebraType0 m (m a) + ) + => m (m a) + -> m a +joinFree = go (proof :: Proof (AlgebraType m (m a)) m a) + where + go :: Proof (AlgebraType m (m a)) m a -> m (m a) -> m a + go p mma = case p of Proof -> foldFree mma + {-# INLINE go #-} + +-- | +-- The monadic @'bind'@ operator. @'returnFree'@ is the corresponding +-- @'return'@ for this monad. +bindFree :: ( FreeAlgebra m + , AlgebraType0 m a + , AlgebraType0 m b + , AlgebraType0 m (m b) + ) + => m a + -> (a -> m b) + -> m b +bindFree ma f = joinFree $ fmapFree f ma + +-- | +-- @'Fix' m@ is the initial algebra in the category of algebras of type +-- @'AlgebraType' m@, whenever it /exists/. +-- +-- Another way of puting this is observing that @'Fix' m@ is isomorphic to @m +-- Void@ where @m@ is the /free algebra/. This isomorphisms is given by +-- @ +-- fixToFree :: (FreeAlgebra m, AlgebraType m (m Void), Functor m) => Fix m -> m Void +-- fixToFree = cataFree +-- @ +-- For monoids the inverse is given by @'Data.Fix.ana' (\_ -> [])@. The +-- category of semigroups, however, does not have the initial object. +cataFree :: ( FreeAlgebra m + , AlgebraType0 m a + , AlgebraType m a + , Functor m + ) + => Fix m + -> a +cataFree = cata foldFree + +type instance AlgebraType0 NonEmpty a = () +type instance AlgebraType NonEmpty m = Semigroup m +instance FreeAlgebra NonEmpty where + returnFree a = a :| [] + -- @'foldMap'@ requires @'Monoid' d@ constraint which we don't need to + -- satisfy here + foldMapFree f (a :| []) = f a + foldMapFree f (a :| (b : bs)) = f a <> foldMapFree f (b :| bs) + + proof = Proof + +type instance AlgebraType0 [] a = () +type instance AlgebraType [] m = Monoid m +instance FreeAlgebra [] where + returnFree a = [a] + foldMapFree = foldMap + proof = Proof + +type instance AlgebraType0 Maybe a = () +type instance AlgebraType Maybe m = Pointed m +instance FreeAlgebra Maybe where + returnFree = Just + foldMapFree _ Nothing = point + foldMapFree f (Just a) = f a + + proof = Proof diff --git a/src/Data/Algebra/Pointed.hs b/src/Data/Algebra/Pointed.hs new file mode 100644 --- /dev/null +++ b/src/Data/Algebra/Pointed.hs @@ -0,0 +1,28 @@ +{-# LANGUAGE UndecidableInstances #-} +module Data.Algebra.Pointed + ( Pointed (..) + , PointedMonoid (..) + ) where + + +-- | +-- Class of pointed sets +class Pointed p where + point :: p + +instance Pointed (Maybe a) where + point = Nothing + +-- | +-- @Monoid@ should be a subclass of @Pointed@. +newtype PointedMonoid m = PointedMonoid { runPointedMonoid :: m } + deriving (Show, Eq, Ord, Functor) + +instance Semigroup m => Semigroup (PointedMonoid m) where + (PointedMonoid m) <> (PointedMonoid n) = PointedMonoid (m <> n) + +instance Monoid m => Monoid (PointedMonoid m) where + mempty = PointedMonoid mempty + +instance Monoid m => Pointed (PointedMonoid m) where + point = mempty diff --git a/src/Data/Group/Free.hs b/src/Data/Group/Free.hs new file mode 100644 --- /dev/null +++ b/src/Data/Group/Free.hs @@ -0,0 +1,110 @@ +{- | + Free groups + * https://en.wikipedia.org/wiki/Free_group + * https://ncatlab.org/nlab/show/Nielsen-Schreier+theorem + -} +module Data.Group.Free + ( FreeGroup + , fromList + , toList + , normalize + ) where + +import Control.Monad (ap) +import Data.Group (Group (..)) +import Data.Semigroup (Semigroup (..)) + +import Data.Algebra.Free + ( AlgebraType + , AlgebraType0 + , FreeAlgebra (..) + , Proof (..) + ) + +-- | +-- Free group generated by a type @a@. Internally it's represented by a list +-- @[Either a a]@ where inverse is given by: +-- +-- @ +-- inverse (FreeGroup [a]) = FreeGroup [either Right Left a] +-- @ +-- +-- It is a monad on a full subcategory of @Hask@ which constists of types which +-- satisfy the @'Eq'@ constraint. +newtype FreeGroup a = FreeGroup { runFreeGroup :: [Either a a] } + deriving (Show, Eq, Ord) + +instance Functor FreeGroup where + fmap f (FreeGroup as) = FreeGroup $ map (either (Left . f) (Right . f)) as + +instance Applicative FreeGroup where + pure = returnFree + (<*>) = ap + +instance Monad FreeGroup where + return a = FreeGroup [Right a] + FreeGroup as >>= f = FreeGroup $ concatMap (runFreeGroup . either f f) as + +-- | +-- Normalize a list, i.e. remove adjusten inverses from a word, i.e. +-- @ab⁻¹ba⁻¹c = c@ +-- +-- Complexity: @O(n)@ +normalize + :: Eq a + => [Either a a] + -> [Either a a] + +normalize (Left a : Right b : bs) + | a == b = normalize bs + | otherwise = case normalize (Right b : bs) of + Right b' : bs' | a == b' + -> bs' + | otherwise + -> Left a : Right b' : bs' + bs' -> Left a : bs' + +normalize (Right a : Left b : bs) + | a == b = normalize bs + | otherwise = case normalize (Left b : bs) of + Left b' : bs' | a == b' + -> bs' + | otherwise + -> Right a : Left b' : bs' + bs' -> Right a : bs' + +normalize (a : as) = case normalize as of + a' : as' | either Right Left a == a' + -> as' + | otherwise + -> a : a' : as' + [] -> [a] + +normalize [] = [] + +-- | +-- Smart constructor which normalizes a list. +fromList :: Eq a => [Either a a] -> FreeGroup a +fromList = FreeGroup . normalize + +toList :: FreeGroup a -> [Either a a] +toList = runFreeGroup + + +instance Eq a => Semigroup (FreeGroup a) where + FreeGroup as <> FreeGroup bs = FreeGroup $ normalize (as ++ bs) + +instance Eq a => Monoid (FreeGroup a) where + mempty = FreeGroup [] + +instance Eq a => Group (FreeGroup a) where + invert (FreeGroup as) = FreeGroup $ foldl (\acu a -> either Right Left a : acu) [] as + +type instance AlgebraType0 FreeGroup a = Eq a +type instance AlgebraType FreeGroup g = Group g +instance FreeAlgebra FreeGroup where + returnFree a = FreeGroup [Right a] + foldMapFree _ (FreeGroup []) = mempty + foldMapFree f (FreeGroup (a : as)) = either (invert . f) f a <> foldMapFree f (FreeGroup as) + + proof = Proof diff --git a/src/Data/Monoid/Abelian.hs b/src/Data/Monoid/Abelian.hs new file mode 100644 --- /dev/null +++ b/src/Data/Monoid/Abelian.hs @@ -0,0 +1,33 @@ +module Data.Monoid.Abelian + ( FreeAbelianMonoid (..) + ) where + +import Data.Map.Strict (Map) +import qualified Data.Map.Strict as Map +import Data.Semigroup (stimes) +import Data.Natural (Natural) + +import Data.Algebra.Free (AlgebraType, AlgebraType0, FreeAlgebra (..), Proof (..)) +import Data.Semigroup.Abelian (AbelianSemigroup) + +-- | +-- Free abelian monoid. Note that `FreeAbelianMonoid () ≅ Natural` as +-- expected. +newtype FreeAbelianMonoid a = FreeAbelianMonoid (Map a Natural) + deriving (Eq, Ord, Show) + +instance Ord a => Semigroup (FreeAbelianMonoid a) where + (FreeAbelianMonoid a) <> (FreeAbelianMonoid b) = FreeAbelianMonoid $ Map.unionWith (+) a b + +instance Ord a => AbelianSemigroup (FreeAbelianMonoid a) + +instance Ord a => Monoid (FreeAbelianMonoid a) where + mempty = FreeAbelianMonoid (Map.empty) + +type instance AlgebraType0 FreeAbelianMonoid a = Ord a +type instance AlgebraType FreeAbelianMonoid m = (Monoid m, AbelianSemigroup m) +instance FreeAlgebra FreeAbelianMonoid where + returnFree a = FreeAbelianMonoid (Map.singleton a 1) + foldMapFree g (FreeAbelianMonoid as) = Map.foldMapWithKey (\a n -> stimes n $ g a) as + + proof = Proof diff --git a/src/Data/Monoid/MSet.hs b/src/Data/Monoid/MSet.hs new file mode 100644 --- /dev/null +++ b/src/Data/Monoid/MSet.hs @@ -0,0 +1,121 @@ +{-# LANGUAGE DeriveFunctor #-} +{- | + Monoid and [group actions](https://en.wikipedia.org/wiki/Group_action) (M-Sets and G-Sets). + The category of @MSet@s (and @GSet@s) is monadic (unlike the category of @SSet@s). + -} +module Data.Monoid.MSet + ( MSet + , Endo (..) + , rep + , fact + , FreeMSet (..) + , hoistFreeMSet + ) where + +import Control.Monad (ap) +import Data.Monoid (Monoid, Endo (..), Sum (..)) +import Data.List.NonEmpty (NonEmpty) +import Data.Functor.Const (Const (..)) +import Data.Functor.Identity (Identity (..)) +import qualified Data.Functor.Product as Functor (Product) +import qualified Data.Functor.Sum as Functor (Sum) +import Data.Natural (Natural) +import Data.Ord (Down) +import Data.Set (Set) + +import Data.Semigroup.SSet (SSet (..), fact, rep) +import Data.Algebra.Free (AlgebraType, AlgebraType0, FreeAlgebra (..), Proof (..), bindFree) + +-- | +-- Lawful instance should satisfy: +-- +-- prop> act mempty = id +-- prop> g `act` h `act` a = g <> h `act` a +-- +-- This is the same as to say that `act` is a monoid homomorphism from @m@ to +-- the monoid of endomorphisms of @a@ (i.e. maps from @a@ to @a@). +-- +-- Note that if @g@ is a @'Group'@ then an @MSet@ is simply a @GSet@, this +-- is because monoids and groups share the same morphisms (a monoid homomorphis +-- between groups necessarily preserves inverses). +class (Monoid m, SSet m a) => MSet m a + +instance Monoid m => MSet m m + +instance (MSet m a, MSet m b) => MSet m (a, b) + +instance (MSet m a, MSet m b, MSet m c) => MSet m (a, b, c) + +instance (MSet m a, MSet m b, MSet m c, MSet m d) => MSet m (a, b, c, d) + +instance (MSet m a, MSet m b, MSet m c, MSet m d, MSet m e) => MSet m (a, b, c, d, e) + +instance (MSet m a, MSet m b, MSet m c, MSet m d, MSet m e, MSet m f) => MSet m (a, b, c, d, e, f) + +instance (MSet m a, MSet m b, MSet m c, MSet m d, MSet m e, MSet m f, MSet m h) => MSet m (a, b, c, d, e, f, h) + +instance (MSet m a, MSet m b, MSet m c, MSet m d, MSet m e, MSet m f, MSet m h, MSet m i) => MSet m (a, b, c, d, e, f, h, i) + +instance MSet m a => MSet m [a] + +instance MSet m a => MSet m (NonEmpty a) + +instance (MSet m a, Ord a) => MSet m (Set a) + +{-- + - instance {-# OVERLAPPABLE #-} (Functor f, MSet m a) => MSet m (f a) where + - act m fa = fmap (act m) fa + --} + +instance MSet m a => MSet m (Identity a) + +instance MSet m a => MSet (Identity m) a + +instance MSet m a => MSet m (Maybe a) + +instance MSet m b => MSet m (Either a b) + +instance MSet m a => MSet m (Down a) + +instance MSet m a => MSet m (IO a) + +instance MSet m b => MSet m (a -> b) + +instance MSet (Endo a) a + +instance Monoid m => MSet (Sum Natural) m + +instance MSet m a => MSet m (Const a b) + +instance (Functor f, Functor h, MSet m a) => MSet m (Functor.Product f h a) + +instance (Functor f, Functor h, MSet m a) => MSet m (Functor.Sum f h a) + +newtype FreeMSet m a = FreeMSet { runFreeMSet :: (m, a) } + deriving (Show, Ord, Eq, Functor) + +hoistFreeMSet + :: (m -> n) -- ^ monoid homomorphism + -> FreeMSet m a + -> FreeMSet n a +hoistFreeMSet f (FreeMSet (m, a)) = FreeMSet (f m, a) + +instance Monoid m => Applicative (FreeMSet m) where + pure = returnFree + (<*>) = ap + +instance Monoid m => Monad (FreeMSet m) where + return = returnFree + (>>=) = bindFree + +instance Semigroup m => SSet m (FreeMSet m a) where + act m (FreeMSet (h, a)) = FreeMSet $ (m <> h, a) + +instance Monoid m => MSet m (FreeMSet m a) + +type instance AlgebraType0 (FreeMSet m) a = () +type instance AlgebraType (FreeMSet m) a = MSet m a +instance Monoid m => FreeAlgebra (FreeMSet m) where + returnFree a = FreeMSet (mempty, a) + foldMapFree f (FreeMSet (m, a)) = act m (f a) + proof = Proof diff --git a/src/Data/Semigroup/Abelian.hs b/src/Data/Semigroup/Abelian.hs new file mode 100644 --- /dev/null +++ b/src/Data/Semigroup/Abelian.hs @@ -0,0 +1,103 @@ +module Data.Semigroup.Abelian + ( AbelianSemigroup + , FreeAbelianSemigroup + , toNonEmpty + , fromNonEmpty + ) where + +import Data.IntSet (IntSet) +import Data.List.NonEmpty (NonEmpty) +import qualified Data.List.NonEmpty as NE +import Data.Map (Map) +import qualified Data.Map as Map +import Data.Set (Set) +import Data.Semigroup + ( Semigroup + , All + , Any + , Dual + , Max + , Min + , Option + , Product + , Sum + ) +import Data.Void (Void) + +import Data.Algebra.Free + ( AlgebraType + , AlgebraType0 + , FreeAlgebra (..) + , Proof (..) + ) + +-- | +-- Class of commutative monoids, e.g. with additional law: +-- @ +-- a <> b = b <> a +-- @ +class Semigroup m => AbelianSemigroup m + +instance AbelianSemigroup Void + +instance AbelianSemigroup () + +instance AbelianSemigroup All + +instance AbelianSemigroup Any + +instance AbelianSemigroup a => AbelianSemigroup (Dual a) + +instance Ord a => AbelianSemigroup (Max a) + +instance Ord a => AbelianSemigroup (Min a) + +instance AbelianSemigroup a => AbelianSemigroup (Option a) + +instance Num a => AbelianSemigroup (Product a) + +instance Num a => AbelianSemigroup (Sum a) + +instance Ord a => AbelianSemigroup (Set a) + +instance AbelianSemigroup IntSet + +-- | +-- Free abelian semigroup is isomorphic to a non empty map with keys @a@ and +-- values positive natural numbers. +newtype FreeAbelianSemigroup a = FreeAbelianSemigroup { runFreeAbelianSemigroup :: Map a Integer } + deriving (Ord, Eq, Show) + +toNonEmpty :: FreeAbelianSemigroup a -> NonEmpty (a, Integer) +toNonEmpty (FreeAbelianSemigroup as) = NE.fromList . Map.toList $ as + +-- | +-- Smart constructor which creates `FreeAbelianSemigroup` from a non empty list +-- of pairs @(a, n) :: (a, Integer)@ where @n > 0@. +fromNonEmpty :: Ord a => NonEmpty (a, Integer) -> Maybe (FreeAbelianSemigroup a) +fromNonEmpty = fmap (FreeAbelianSemigroup . Map.fromList) . go . NE.toList + where + go [] = Just [] + go ((a, n) : as) | n < 0 = Nothing + | otherwise = ((a, n) :) <$> go as + +instance Ord a => Semigroup (FreeAbelianSemigroup a) where + (FreeAbelianSemigroup a) <> (FreeAbelianSemigroup b) = FreeAbelianSemigroup $ Map.unionWith (+) a b + +instance Ord a => AbelianSemigroup (FreeAbelianSemigroup a) + +type instance AlgebraType0 FreeAbelianSemigroup a = Ord a +type instance AlgebraType FreeAbelianSemigroup a = AbelianSemigroup a +instance FreeAlgebra FreeAbelianSemigroup where + returnFree a = FreeAbelianSemigroup $ Map.singleton a 1 + foldMapFree f (FreeAbelianSemigroup as) = foldMapFree f (toNonEmpty_ as) + where + replicate_ :: a -> Integer -> [a] + replicate_ _ n | n <= 0 = error "foldMapFree @FreeAbelianSemigroup: impossible" + replicate_ a 1 = [a] + replicate_ a n = a : replicate_ a (n - 1) + + toNonEmpty_ :: Map a Integer -> NonEmpty a + toNonEmpty_ = NE.fromList . concat . map (uncurry replicate_) . Map.toList + + proof = Proof diff --git a/src/Data/Semigroup/SSet.hs b/src/Data/Semigroup/SSet.hs new file mode 100644 --- /dev/null +++ b/src/Data/Semigroup/SSet.hs @@ -0,0 +1,117 @@ +{- | + Actions of [semigroup](https://en.wikipedia.org/wiki/Semigroup_action) (SSet). + -} +module Data.Semigroup.SSet + ( SSet (..) + , rep + , fact + ) where + +import Data.Semigroup (Endo (..), Sum (..)) +import Data.Functor.Const (Const (..)) +import Data.Functor.Identity (Identity (..)) +import qualified Data.Functor.Product as Functor (Product) +import qualified Data.Functor.Sum as Functor (Sum) +import Data.Group (Group (..)) +import Data.List.NonEmpty (NonEmpty) +import qualified Data.List.NonEmpty as NE +import Data.Natural (Natural) +import Data.Ord (Down) +import Data.Set (Set) +import qualified Data.Set as Set + +-- | +-- A lawful instance should satisfy: +-- +-- prop> g `act` h `act` a = g <> h `act` a +-- +-- This is the same as to say that `act` is a semigroup homomorphism from @s@ to +-- the monoid of endomorphisms of @a@ (i.e. maps from @a@ to @a@). +-- +-- Note that if @g@ is a @'Group'@ then @'MAct' g@ is simply a @GSet@, this +-- is because monoids and groups share the same morphisms (a monoid homomorphis +-- between groups necessarily preserves inverses). +class Semigroup s => SSet s a where + act :: s -> a -> a + +rep :: SSet s a => s -> Endo a +rep s = Endo (act s) + +instance Semigroup s => SSet s s where + act = (<>) + +instance (SSet s a, SSet s b) => SSet s (a, b) where + act s (a, b) = (act s a, act s b) + +instance (SSet s a, SSet s b, SSet s c) => SSet s (a, b, c) where + act s (a, b, c) = (act s a, act s b, act s c) + +instance (SSet s a, SSet s b, SSet s c, SSet s d) => SSet s (a, b, c, d) where + act s (a, b, c, d) = (act s a, act s b, act s c, act s d) + +instance (SSet s a, SSet s b, SSet s c, SSet s d, SSet s e) => SSet s (a, b, c, d, e) where + act s (a, b, c, d, e) = (act s a, act s b, act s c, act s d, act s e) + +instance (SSet s a, SSet s b, SSet s c, SSet s d, SSet s e, SSet s f) => SSet s (a, b, c, d, e, f) where + act s (a, b, c, d, e, f) = (act s a, act s b, act s c, act s d, act s e, act s f) + +instance (SSet s a, SSet s b, SSet s c, SSet s d, SSet s e, SSet s f, SSet s h) => SSet s (a, b, c, d, e, f, h) where + act s (a, b, c, d, e, f, h) = (act s a, act s b, act s c, act s d, act s e, act s f, act s h) + +instance (SSet s a, SSet s b, SSet s c, SSet s d, SSet s e, SSet s f, SSet s h, SSet s i) => SSet s (a, b, c, d, e, f, h, i) where + act s (a, b, c, d, e, f, h, i) = (act s a, act s b, act s c, act s d, act s e, act s f, act s h, act s i) + +instance SSet s a => SSet s [a] where + act s = map (act s) + +instance SSet s a => SSet s (NonEmpty a) where + act s as = NE.map (act s) as + +instance (SSet s a, Ord a) => SSet s (Set a) where + act s as = Set.map (act s) as + +-- | +-- Any @'SSet'@ wrapped in a functor is a valid @'SSet'@. +fact :: (Functor f, SSet s a) => s -> f a -> f a +fact s = fmap (act s) + +instance SSet s a => SSet s (Identity a) where + act = fact + +instance SSet s a => SSet (Identity s) a where + act (Identity f) a = f `act` a + +instance SSet s a => SSet s (Maybe a) where + act = fact + +instance SSet s b => SSet s (Either a b) where + act = fact + +instance SSet s a => SSet s (Down a) where + act = fact +instance SSet s a => SSet s (IO a) where + act = fact + +instance SSet s b => SSet s (a -> b) where + act = fact + +instance SSet (Endo a) a where + act (Endo f) a = f a + +instance Monoid s => SSet (Sum Natural) s where + act (Sum 0) _ = mempty + act (Sum n) s = s <> act (Sum (n - 1)) s + +instance Group g => SSet (Sum Integer) g where + act (Sum n) g | n < 0 = invert g <> act (Sum (n + 1)) g + | n > 0 = g <> act (Sum (n - 1)) g + | otherwise = mempty + +instance SSet s a => SSet s (Const a b) where + act s (Const a) = Const $ s `act` a + +instance (Functor f, Functor h, SSet s a) => SSet s (Functor.Product f h a) where + act = fact + +instance (Functor f, Functor h, SSet s a) => SSet s (Functor.Sum f h a) where + act = fact diff --git a/src/Data/Semigroup/SemiLattice.hs b/src/Data/Semigroup/SemiLattice.hs new file mode 100644 --- /dev/null +++ b/src/Data/Semigroup/SemiLattice.hs @@ -0,0 +1,57 @@ +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +module Data.Semigroup.SemiLattice + ( FreeSemiLattice + , fromNonEmpty + , toNonEmpty + ) where + +import Data.List.NonEmpty (NonEmpty (..)) +import qualified Data.List.NonEmpty as NE +import Data.IntSet (IntSet) +import Data.Semigroup (All, Any, sconcat) +import Data.Set (Set) +import qualified Data.Set as Set +import Data.Void (Void) + +import Data.Algebra.Free + ( AlgebraType + , AlgebraType0 + , FreeAlgebra (..) + , Proof (..) + ) +import Data.Semigroup.Abelian (AbelianSemigroup) + +-- | +-- Class of abelian semigroups in which every element is idempontent, i.e. +-- @a <> a = a@. +class AbelianSemigroup m => SemiLattice m + +instance SemiLattice Void +instance SemiLattice () +instance SemiLattice All +instance SemiLattice Any +instance Ord a => SemiLattice (Set a) +instance SemiLattice IntSet + +-- | +-- @'FreeSemiLattice'@ is a non empty set. +newtype FreeSemiLattice a = FreeSemiLattice { runFreeSemiLattice :: Set a } + deriving (Ord, Eq, Show, Semigroup) + +instance Ord a => AbelianSemigroup (FreeSemiLattice a) + +instance Ord a => SemiLattice (FreeSemiLattice a) + +fromNonEmpty :: Ord a => NonEmpty a -> FreeSemiLattice a +fromNonEmpty = FreeSemiLattice . Set.fromList . NE.toList + +toNonEmpty :: FreeSemiLattice a -> NonEmpty a +toNonEmpty (FreeSemiLattice as) = NE.fromList $ Set.toList as + +type instance AlgebraType0 FreeSemiLattice a = Ord a +type instance AlgebraType FreeSemiLattice a = SemiLattice a +instance FreeAlgebra FreeSemiLattice where + returnFree a = FreeSemiLattice $ Set.singleton a + foldMapFree f (FreeSemiLattice as) = sconcat $ fmap f $ NE.fromList $ Set.toList as + + proof = Proof diff --git a/test/Spec.hs b/test/Spec.hs new file mode 100644 --- /dev/null +++ b/test/Spec.hs @@ -0,0 +1,22 @@ +module Spec + ( main + ) where + +import Control.Monad (unless) +import System.Exit (exitFailure) + +import qualified Test.Data.Algebra.Free (tests) +import qualified Test.Control.Algebra.Free (tests) + +runTests :: [IO Bool] -> IO () +runTests tests = do + res <- and <$> sequence tests + unless res + exitFailure + +main :: IO () +main = do + runTests + [ Test.Data.Algebra.Free.tests + , Test.Control.Algebra.Free.tests + ] diff --git a/test/Test/Control/Algebra/Free.hs b/test/Test/Control/Algebra/Free.hs new file mode 100644 --- /dev/null +++ b/test/Test/Control/Algebra/Free.hs @@ -0,0 +1,287 @@ +{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE LambdaCase #-} +module Test.Control.Algebra.Free + ( tests + ) where + +import Control.Applicative.Free (Ap) +import qualified Control.Applicative.Free as Ap +import Control.Monad.Free (Free) +import qualified Control.Monad.Free as Free +import Control.Monad (join) +import Data.List.NonEmpty (NonEmpty (..)) +import Data.Foldable (fold) +import Data.Functor.Identity (Identity (..)) +import Data.Functor.Coyoneda (Coyoneda (..), lowerCoyoneda) +import Data.Monoid (Sum (..)) +import Data.Proxy (Proxy (..)) +import Hedgehog (Property, PropertyT, Gen, property, (===)) +import qualified Hedgehog as H +import qualified Hedgehog.Gen as Gen +import qualified Hedgehog.Range as Range + +import Data.Algebra.Free ( AlgebraType ) +import Control.Algebra.Free + ( AlgebraType0 + , FreeAlgebra1 (..) + , unFoldNatFree + , foldFree1 + , hoistFree1 + , iterFree1 + ) + +genIntToInt :: Integral n => Gen (n -> n) +genIntToInt = do + x <- Gen.integral $ Range.linear (-100) 100 + return (+x) + +showIntToInt :: (Integral n, Show n) => (n -> n) -> String +showIntToInt f = "(+"++ show (f 0) ++ ")" + +-- | +-- Generate a @Coyoneda f@ given a constructor of @f@. +genCoyoneda + :: (Int -> f Int) + -> Gen (Coyoneda f Int) +genCoyoneda f = do + a <- Gen.int $ Range.linear 0 100 + Gen.bool_ >>= \case + True -> return $ Coyoneda id (f a) + False -> do + x <- Gen.int $ Range.linear 0 100 + return $ Coyoneda (\x -> x + a) (f x) + +toOdd :: Integral n => n -> Maybe n +toOdd x = if x `mod` 2 == 0 + then Nothing + else Just x + +-- | +-- Generated `Ap Maybe` with arbitrary depth. +genAp :: forall f x . Show x + => Gen x + -> Gen (x -> x) + -> Gen (Ap Maybe x) +genAp gen genf = Gen.sized $ \s -> go s + where + go (Range.Size 0) = Gen.maybe gen >>= \case + Just x -> return $ Ap.Pure x + Nothing -> return $ Ap.Ap Nothing (Ap.Pure id) + go s = do + ap <- go (s - 1) + f <- genf + return $ Ap.Pure f <*> ap + +genApIdentity + :: forall f x . Show x + => Gen x + -> Gen (x -> x) + -> Gen (Ap Identity x) +genApIdentity gen genf = Gen.sized $ \s -> go s + where + go (Range.Size 0) = do + x <- gen + return $ Ap.Ap (Identity x) (Ap.Pure id) + go s = do + ap <- go (s - 1) + f <- genf + return $ Ap.Pure f <*> ap + +-- | +-- Generate @Free Maybe@ of arbitrary depth. +genFree :: Gen x + -> Gen (Free Maybe x) +genFree gen = Gen.sized go + where + go (Range.Size 0) = Free.Pure <$> gen + go s = Free.Free <$> Gen.maybe (go (s - 1)) + +genFreeIdentity + :: Gen x + -> Gen (Free Identity x) +genFreeIdentity gen = Gen.sized go + where + go (Range.Size 0) = Free.Pure <$> gen + go s = Free.Free . Identity <$> go (s - 1) + +foldMapFree1_property + :: forall m f d a + . ( FreeAlgebra1 m + , AlgebraType m d + , AlgebraType m f + , AlgebraType0 m f + , Show a + , Show (f a) + , Eq (d a) + , Show (d a) + ) + => Gen (m f a) + -> Gen (f a) + -> (forall x. f x -> d x) + -> (forall x. m f x -> d x) + -> Property +foldMapFree1_property gen_mfa gen_fa fd mfd + = property $ do + mfa <- H.forAllWith (show . foldFree1) gen_mfa + fa <- H.forAll gen_fa + H.assert $ fd_id (Proxy :: Proxy m) fd fa == fd fa + H.assert $ mfd_id mfd mfa == mfd mfa + where + fd_id :: forall a + . Proxy m + -> (forall x. f x -> d x) + -> (forall x. f x -> d x) + fd_id _ nat = + let nat' :: forall a . m f a -> d a + nat' = foldNatFree nat + in unFoldNatFree nat' + + mfd_id :: forall a + . (forall x. m f x -> d x) + -> (forall x. m f x -> d x) + mfd_id nat = + let nat' :: forall a . f a -> d a + nat' = unFoldNatFree nat + in foldNatFree nat' + +prop_foldMapFree1_coyoneda :: Property +prop_foldMapFree1_coyoneda + = foldMapFree1_property + (genCoyoneda toOdd) + (Gen.maybe $ Gen.integral (Range.linear 0 1000)) + id + foldFree1 + +prop_foldMapFree1_ap :: Property + = foldMapFree1_property + (genAp (Gen.word8 (Range.linear 0 254)) genIntToInt) + (Gen.maybe $ Gen.word8 (Range.linear 0 254)) + id + foldFree1 + +prop_foldMapFree1_free :: Property +prop_foldMapFree1_free + = foldMapFree1_property + (genFree $ Gen.word8 (Range.linear 0 254)) + (Gen.maybe $ Gen.word8 (Range.linear 0 254)) + id + foldFree1 + +foldFree1_property + :: forall m f a + . ( FreeAlgebra1 m + , AlgebraType m f + , AlgebraType0 m f + , Eq (f a) + , Show (f a) + ) + => PropertyT IO (m f a) + -> (m f a -> f a) + -- ^ reference fold implentation + -> Property +foldFree1_property gen fold_ = property $ do + mfa <- gen + foldFree1 mfa === fold_ mfa + +prop_foldFree1_coyoneda :: Property +prop_foldFree1_coyoneda = + foldFree1_property (H.forAll $ genCoyoneda toOdd) lowerCoyoneda + +prop_foldFree1_ap :: Property +prop_foldFree1_ap = foldFree1_property + (H.forAllWith (show . Ap.retractAp) $ genAp (Gen.integral $ Range.linear 0 100) genIntToInt) + Ap.retractAp + +prop_foldFree1_free :: Property +prop_foldFree1_free = foldFree1_property + (H.forAll $ genFree (Gen.integral $ Range.linear 0 100)) + (Free.foldFree id) + +hoistFree1_property + :: forall m f g a + . ( FreeAlgebra1 m + , AlgebraType m f + , AlgebraType m (m g) + , AlgebraType0 m f + , AlgebraType m g + , AlgebraType0 m g + ) + => Gen (m f a) + -> (m f a -> String) + -> (m g a -> m g a -> Bool) + -> (forall x. f x -> g x) + -> ((forall x . f x -> g x) -> m f a -> m g a) + -- ^ reference hoist impelentation + -> Property +hoistFree1_property gen show_mfa eq_mga nat refImpl = property $ do + mfa <- H.forAllWith show_mfa gen + H.assert $ hoistFree1 nat mfa `eq_mga` refImpl nat mfa + +prop_hoistFree1_coyoneda :: Property +prop_hoistFree1_coyoneda = hoistFree1_property + (genCoyoneda toOdd) + (show . lowerCoyoneda) + (\a b -> lowerCoyoneda a == lowerCoyoneda b) + (maybe (Left ()) Right) + (\nat (Coyoneda xa fx) -> Coyoneda xa (nat fx)) + +prop_hoistFree1_ap :: Property +prop_hoistFree1_ap = hoistFree1_property + (genAp (Gen.int $ Range.linear 0 1000) genIntToInt) + (show . Ap.retractAp) + (\x y -> Ap.retractAp x == Ap.retractAp y) + (maybe (Left ()) Right) + Ap.hoistAp + +prop_hoistFree1_free :: Property +prop_hoistFree1_free = hoistFree1_property + (genFree (Gen.integral $ Range.linear 0 100)) + show + (==) + (maybe (Left ()) Right) + Free.hoistFree + +iterFree1_property + :: forall m f a + . ( FreeAlgebra1 m + , AlgebraType m f + , AlgebraType0 m f + , AlgebraType m Identity + , AlgebraType0 m Identity + , Eq a + , Show a + ) + => Gen (m f a) + -> (m f a -> String) + -> (forall x. f x -> x) + -> ((forall x . f x -> x) -> m f a -> a) + -- ^ reference implementation + -> Property +iterFree1_property gen show_mfa nat refImpl = property $ do + mfa <- H.forAllWith show_mfa gen + iterFree1 nat mfa === refImpl nat mfa + +prop_iterFree1_coyoneda :: Property +prop_iterFree1_coyoneda = iterFree1_property + (genCoyoneda Identity) + show + runIdentity + (\_ -> runIdentity . lowerCoyoneda) + +prop_iterFree1_free :: Property +prop_iterFree1_free = iterFree1_property + (genFreeIdentity (Gen.int $ Range.linear 0 1000)) + show + runIdentity + Free.iter + +prop_iterFree1_ap :: Property +prop_iterFree1_ap = iterFree1_property + (genApIdentity (Gen.int $ Range.linear 0 1000) genIntToInt) + (show . Ap.retractAp) + runIdentity + Ap.iterAp + where + +tests :: IO Bool +tests = H.checkParallel $$(H.discover) diff --git a/test/Test/Data/Algebra/Free.hs b/test/Test/Data/Algebra/Free.hs new file mode 100644 --- /dev/null +++ b/test/Test/Data/Algebra/Free.hs @@ -0,0 +1,220 @@ +{-# LANGUAGE TemplateHaskell #-} +module Test.Data.Algebra.Free + ( tests + ) where + +import Control.Monad (join) +import Data.List.NonEmpty (NonEmpty (..)) +import Data.Foldable (fold) +import Data.Monoid (Sum (..)) +import Hedgehog (Property, Gen, property, (===)) +import qualified Hedgehog as H +import qualified Hedgehog.Gen as Gen +import qualified Hedgehog.Range as Range + +import Data.Algebra.Free + ( AlgebraType + , AlgebraType0 + , FreeAlgebra (..) + , foldFree + , unFoldMapFree + , natFree + , fmapFree + , joinFree + , bindFree + ) + +natFree_property + :: ( FreeAlgebra f + , AlgebraType0 f a + , AlgebraType f (f a) + , Eq (f a) + , Show (f a) + ) + => Gen (f a) -> Property +natFree_property gen = property $ do + fa <- H.forAll gen + natFree fa === fa + +prop_natFree_list :: Property +prop_natFree_list = natFree_property + $ Gen.list (Range.linear 0 100) Gen.alpha + +prop_nafF_nonempty :: Property +prop_nafF_nonempty = natFree_property + $ Gen.nonEmpty (Range.linear 0 100) Gen.alpha + +-- | +-- Check that @'foldFree' is @'fold'@ for @f@ which are @'Foldable'@ and @a@ which +-- are @'Monoid' a. +foldFree_property + :: ( FreeAlgebra f + , AlgebraType0 f a + , AlgebraType f a + , Monoid a -- fold brings this constraint, @'foldFree'@ is free of it! + , Foldable f + , Eq a + , Eq (f a) + , Show a + , Show (f a) + ) + => Gen (f a) + -> Property +foldFree_property gen = property $ do + fa <- H.forAll gen + foldFree fa === fold fa + +prop_foldFree_list :: Property +prop_foldFree_list = foldFree_property + $ (Gen.list $ Range.linear 0 100) + (Sum <$> Gen.word32 (Range.linear 0 1024)) + +prop_foldFree_nonempty :: Property +prop_foldFree_nonempty = foldFree_property + $ (Gen.nonEmpty $ Range.linear 0 100) + (Sum <$> Gen.word32 (Range.linear 0 1024)) + +-- | +-- @'fmapFoldFree'@ is inverse of @'unFoldMapFree'@ +foldMapFree_property + :: forall f d a . + ( FreeAlgebra f + , AlgebraType0 f d + , AlgebraType0 f a + , AlgebraType f d + , Show (f a) + , Show a + , Show d + , Eq d + ) + => Gen (f a) + -> Gen a + -> (f a -> d) + -> (a -> d) + -> Property +foldMapFree_property gen_fa gen fad ad = property $ do + fa <- H.forAll gen_fa + a <- H.forAll gen + unFoldMapFree (foldMapFree @f ad) a === ad a + foldMapFree (unFoldMapFree @f fad) fa === fad fa + +prop_foldMapFree_list :: Property +prop_foldMapFree_list + = foldMapFree_property @[] @(Sum Int) @Int + ((Gen.list $ Range.linear 0 100) + (Gen.integral $ Range.linear 0 1024)) + (Gen.integral $ Range.linear 0 1024) + (Sum . sum) + Sum + +prop_foldMapFree_nonempty :: Property + = foldMapFree_property @NonEmpty @(Sum Int) @Int + ((Gen.nonEmpty $ Range.linear 0 100) + (Gen.integral $ Range.linear 0 1024)) + (Gen.integral $ Range.linear 0 1024) + (Sum . sum) + Sum + +-- | +-- @'fmapFree'@ should aggree with @'fmap'@ for types which satisfy @'Functor'@ +-- constraint. +fmapFree_property + :: forall f a b . + ( FreeAlgebra f + , AlgebraType0 f a + , AlgebraType0 f b + , Functor f + , Show (f a) + , Eq (f a) + , Show (f b) + , Eq (f b) + ) + => Gen (f a) + -> (a -> b) + -> Property +fmapFree_property gen f = property $ do + fa <- H.forAll gen + fmapFree f fa === fmap f fa + +prop_fmapFree_list :: Property +prop_fmapFree_list = fmapFree_property @[] @Integer @Integer + ((Gen.list $ Range.linear 0 100) + (Gen.integral $ Range.linear 0 1024)) + (\x -> x^2 + 2 * x + 1) + +prop_fmapFree_nonempty :: Property +prop_fmapFree_nonempty = fmapFree_property + ((Gen.nonEmpty $ Range.linear 0 100) + (Gen.integral $ Range.linear 0 1024)) + (\x -> x^2 + 2 * x + 1) + +-- | +-- @'joinFree'@ should be equal to @'join'@ for monads. +joinFree_property + :: ( FreeAlgebra m + , AlgebraType0 m a + , AlgebraType0 m (m a) + , AlgebraType m (m a) + , Monad m + , Show (m (m a)) + , Eq (m (m a)) + , Show (m a) + , Eq (m a) + ) + => Gen (m (m a)) + -> Property +joinFree_property gen = property $ do + mma <- H.forAll gen + joinFree mma === join mma + +prop_joinFree_list :: Property +prop_joinFree_list = + let gen = Gen.list (Range.linear 0 100) + (Gen.list (Range.linear 0 10) Gen.alpha) + in joinFree_property gen + +prop_joinFree_nonempty :: Property +prop_joinFree_nonempty = + let gen = Gen.nonEmpty (Range.linear 0 100) + (Gen.nonEmpty (Range.linear 0 10) Gen.alpha) + in joinFree_property gen + +-- | +-- @'bindFree'@ should be equal to @'>>='@ for monads. +bindFree_property + :: ( FreeAlgebra m + , AlgebraType0 m a + , AlgebraType0 m b + , AlgebraType0 m (m b) + , AlgebraType m (m a) + , AlgebraType m (m b) + , AlgebraType m (m (m b)) + , Monad m + , Show (m a) + , Eq (m a) + , Show (m b) + , Eq (m b) + ) + => Gen (m a) + -> (a -> m b) + -> Property +bindFree_property gen f = property $ do + ma <- H.forAll gen + bindFree ma f === (ma >>= f) + +prop_bindFree_list :: Property +prop_bindFree_list = + let gen = Gen.list + (Range.linear 0 10) + (Gen.integral $ Range.linear 0 1024) + in bindFree_property gen (\x -> [x^2, 2 * x, 1]) + +prop_bindFree_nonempty :: Property +prop_bindFree_nonempty = + let gen = Gen.nonEmpty + (Range.linear 0 10) + (Gen.integral $ Range.linear 0 1024) + in bindFree_property gen (\x -> x^2 :| [2 * x, 1]) + +tests :: IO Bool +tests = H.checkParallel $$(H.discover)