free-algebras 0.0.2.0 → 0.0.3.0
raw patch · 12 files changed
+197/−159 lines, 12 filesPVP: major bump suggested
API removals or changes: PVP suggests a major version bump
API changes (from Hackage documentation)
- Control.Algebra.Free: proof0 :: forall f. (FreeAlgebra1 m, AlgebraType0 m f) => Proof (AlgebraType0 m (m f)) (m f)
- Control.Monad.Action: instance (GHC.Base.Monad m, Data.Algebra.Free.FreeAlgebra m, Data.Algebra.Free.AlgebraType m d, Data.Algebra.Free.AlgebraType0 m d) => Control.Monad.Action.MAction m (Data.Functor.Const.Const d)
+ Control.Algebra.Free: forget1 :: forall f. (FreeAlgebra1 m, AlgebraType m f) => Proof (AlgebraType0 m f) (m f)
+ Control.Monad.Action: instance (GHC.Base.Monad m, Data.Algebra.Free.FreeAlgebra m, Data.Algebra.Free.AlgebraType m d) => Control.Monad.Action.MAction m (Data.Functor.Const.Const d)
+ Data.Algebra.Free: forget :: forall a. (FreeAlgebra m, AlgebraType m a) => Proof (AlgebraType0 m a) (m a)
- Control.Algebra.Free: 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)
+ Control.Algebra.Free: assocFree1 :: forall m f a. (FreeAlgebra1 m, AlgebraType m f, Functor (m (m f))) => m f (m f a) -> m (m f) (f a)
- Control.Algebra.Free: cataFree1 :: forall m f a. (FreeAlgebra1 m, AlgebraType m f, AlgebraType0 m f, Monad f, Traversable (m f)) => Fix (m f) -> f a
+ Control.Algebra.Free: cataFree1 :: forall m f a. (FreeAlgebra1 m, AlgebraType m f, Monad f, Traversable (m f)) => Fix (m f) -> f a
- Control.Algebra.Free: foldFree1 :: (FreeAlgebra1 m, AlgebraType0 m f, AlgebraType m f) => m f a -> f a
+ Control.Algebra.Free: foldFree1 :: forall m f a. (FreeAlgebra1 m, AlgebraType m f) => m f a -> f a
- Data.Algebra.Free: bindFree :: (FreeAlgebra m, AlgebraType0 m a, AlgebraType0 m b, AlgebraType0 m (m b)) => m a -> (a -> m b) -> m b
+ Data.Algebra.Free: bindFree :: forall m a b. (FreeAlgebra m, AlgebraType0 m a, AlgebraType0 m b) => m a -> (a -> m b) -> m b
- Data.Algebra.Free: cataFree :: (FreeAlgebra m, AlgebraType0 m a, AlgebraType m a, Functor m) => Fix m -> a
+ Data.Algebra.Free: cataFree :: (FreeAlgebra m, AlgebraType m a, Functor m) => Fix m -> a
- Data.Algebra.Free: foldFree :: (FreeAlgebra m, AlgebraType0 m a, AlgebraType m a) => m a -> a
+ Data.Algebra.Free: foldFree :: forall m a. (FreeAlgebra m, AlgebraType m a) => m a -> a
- Data.Algebra.Free: joinFree :: forall m a. (FreeAlgebra m, AlgebraType0 m a, AlgebraType0 m (m a)) => m (m a) -> m a
+ Data.Algebra.Free: joinFree :: forall m a. (FreeAlgebra m, AlgebraType0 m a) => m (m a) -> m a
- Data.Algebra.Free: natFree :: forall m n a. (AlgebraType m (n a), AlgebraType0 m a, FreeAlgebra m, FreeAlgebra n) => m a -> n a
+ Data.Algebra.Free: natFree :: forall m n a. (FreeAlgebra m, FreeAlgebra n, AlgebraType0 m a, AlgebraType m (n a)) => m a -> n a
Files
- ChangeLog.md +6/−0
- free-algebras.cabal +4/−4
- src/Control/Algebra/Free.hs +100/−89
- src/Control/Monad/Action.hs +3/−3
- src/Data/Algebra/Free.hs +46/−32
- src/Data/Group/Free.hs +5/−2
- src/Data/Monoid/Abelian.hs +3/−2
- src/Data/Monoid/MSet.hs +2/−1
- src/Data/Semigroup/Abelian.hs +3/−2
- src/Data/Semigroup/SemiLattice.hs +3/−2
- test/Main.hs +22/−0
- test/Spec.hs +0/−22
ChangeLog.md view
@@ -1,5 +1,11 @@ # Changelog for free-algebras +## Version 0.0.3.0++- Breaking change: changed proofs in FreeAlgebra and FreeAlgebra1 class; now+ using `FreeAlgebra` and `FreeAlgebra1` classes let us deduce an adjunction.+- Monadicity example+ ## Version 0.0.2.0 - Simplified `Proof` type.
free-algebras.cabal view
@@ -2,13 +2,13 @@ -- -- see: https://github.com/sol/hpack ----- hash: 01ca145922d0171eb90e9232004a0c588b6403c06f81dcae21bd5416c907bd75+-- hash: 9cf25d016d878667110e6394084d060d946ebb54650a1bb2b8786fd56371dc93 name: free-algebras-version: 0.0.2.0+version: 0.0.3.0 synopsis: Free algebras in Haskell. description: Universal algebra approach to free algebras including higher kinded algebraic structures like functors, applicative functors or monads.-category: Algebra+category: Algebra, Control, Monads homepage: https://github.com/coot/free-algebras#readme bug-reports: https://github.com/coot/free-algebras/issues author: Marcin Szamotulski@@ -67,7 +67,7 @@ test-suite free-algebras-test type: exitcode-stdio-1.0- main-is: Spec.hs+ main-is: Main.hs other-modules: Test.Control.Algebra.Free Test.Data.Algebra.Free
src/Control/Algebra/Free.hs view
@@ -67,14 +67,14 @@ -- free applicative functors, free monads, state monads etc. -- -- A lawful instance should guarantee that @'foldNatFree'@ is an isomorphism--- with inversese @'unFoldNatFree'@.+-- with inverses @'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+-- constraint. This functor is left adjoin 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.+-- turn guarantees that @m@ composed 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.@@ -85,7 +85,7 @@ -- | The freeness property. foldNatFree :: forall (d :: Type -> Type) f a .- ( AlgebraType m d+ ( AlgebraType m d , AlgebraType0 m f ) => (forall x. f x -> d x)@@ -94,16 +94,23 @@ -- ^ a homomorphism from @m f@ to @d@ -- |- -- A proof that @'AlgebraType0' m (m f)@ holds for all @f@.- proof0 :: forall f. AlgebraType0 m f => Proof (AlgebraType0 m (m f)) (m f)+ -- A proof that @'AlgebraType' m (m f)@ holds for all @AlgebraType0 f => f@.+ -- Together with @hoistFree1@ this proves that @FreeAlgebra m => m@ is+ -- a functor from the full subcategory of types of kind @Type -> Type@+ -- which satisfy @'AlgebraType0' m f@ to ones that satisfy @'AlgebraType'+ -- m f@.+ proof1 :: forall f. AlgebraType0 m f => Proof (AlgebraType m (m f)) (m f)+ -- |- -- A proof that @'AlgebraType' m (m f)@ holds for all @f@.- proof1 :: forall f. AlgebraType0 m f => Proof (AlgebraType m (m f)) (m f)+ -- A proof that the forgetful functor from the full subcategory of types of+ -- kind @Type -> Type@ satisfying @'AlgebraType' m f@ constraint to types+ -- satisfying @'AlgebraType0' m f@ is well defined.+ forget1 :: forall f. AlgebraType m f => Proof (AlgebraType0 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.+-- @'wrap'@ to define 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. --@@ -119,36 +126,47 @@ 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 -- @ --+-- @foldFree1@ is the+-- [unit](https://ncatlab.org/nlab/show/unit+of+an+adjunction) of the+-- adjunction imposed by @FreeAlgebra1@ constraint.+-- -- 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+foldFree1 :: forall m f a .+ ( FreeAlgebra1 m , AlgebraType m f ) => m f a -> f a-foldFree1 = foldNatFree id+foldFree1 = case forget1 @m @f of+ Proof Dict -> foldNatFree id -- |+-- @'unFoldNatFree'@ is an inverse of @'foldNatFree'@+--+-- prop> unFoldNatFree id = ruturnFree1+--+-- Note that @'unFoldNatFree' id@ is the+-- [unit](https://ncatlab.org/nlab/show/unit+of+an+adjunction) of the+-- adjunction imposed by the @'FreeAlgebra1'@ constraint.+unFoldNatFree+ :: ( FreeAlgebra1 m+ , AlgebraType0 m f+ )+ => (forall x . m f x -> d x)+ -> f a -> d a+unFoldNatFree nat = nat . liftFree++-- | -- This is a functor instance for @m@ when considered as an endofuctor of some -- subcategory of @Type -> Type@ (e.g. endofunctors of _Hask_). --@@ -164,10 +182,8 @@ => (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 Dict) nat = foldNatFree (liftFree . nat)- {-# INLINE go #-}+hoistFree1 nat = case proof1 @m @g of+ Proof Dict -> foldNatFree (liftFree . nat) -- | -- @@@ -200,14 +216,13 @@ ) => 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 Dict) (Proof Dict) = foldFree1- {-# INLINE go #-}+joinFree1 = case proof1 @m @f of+ Proof Dict -> case forget1 @m @(m f) of+ Proof Dict -> foldFree1 -- |--- Bind operator for the @'joinFree1'@ monad+-- Bind operator for the @'joinFree1'@ monad, this is just @'foldNatFree'@ in+-- disguise. bindFree1 :: forall m f g a . ( FreeAlgebra1 m , AlgebraType0 m g@@ -216,36 +231,33 @@ => 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 Dict) (Proof Dict) mfa nat = joinFree1 $ hoistFree1 nat mfa- {-# INLINE go #-}+bindFree1 mfa nat = case proof1 @m @g of+ Proof Dict -> foldNatFree nat mfa 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))+assocFree1 = case forget1 @m @f of+ Proof Dict -> case proof1 @m @f of+ Proof Dict -> case forget1 @m @(m f) of+ Proof Dict -> case proof1 @m @(m f) of+ Proof Dict -> case forget1 @m @(m (m f)) of+ Proof Dict -> fmap g <$> foldNatFree 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 Dict) = 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 Dict) = fmap g <$> foldNatFree f-- f :: forall x. f x -> m (m f) x- f = hoistFree1 liftFree . liftFree+ f :: forall x .+ ( AlgebraType0 m f+ , AlgebraType0 m (m f)+ )+ => f x+ -> m (m f) x+ f = hoistFree1 liftFree . liftFree - g :: m f a -> f a- g = foldFree1+ g :: m f a -> f a+ g = foldFree1 -- | -- @'Fix' (m f)@ is the initial /algebra/ of type @'AlgebraType' m@ and@@ -253,7 +265,6 @@ cataFree1 :: forall m f a . ( FreeAlgebra1 m , AlgebraType m f- , AlgebraType0 m f , Monad f , Traversable (m f) )@@ -287,8 +298,8 @@ liftFree = liftCoyoneda foldNatFree nat (Coyoneda ba fx) = ba <$> nat fx - proof0 = Proof Dict- proof1 = Proof Dict+ proof1 = Proof Dict+ forget1 = Proof Dict -- | -- Algebras of the same type as @'Ap'@ are the applicative functors.@@ -301,8 +312,8 @@ liftFree = Ap.liftAp foldNatFree = Ap.runAp - proof0 = Proof Dict- proof1 = Proof Dict+ proof1 = Proof Dict+ forget1 = Proof Dict type instance AlgebraType0 Fast.Ap g = Functor g type instance AlgebraType Fast.Ap g = Applicative g@@ -310,8 +321,8 @@ liftFree = Fast.liftAp foldNatFree = Fast.runAp - proof0 = Proof Dict- proof1 = Proof Dict+ proof1 = Proof Dict+ forget1 = Proof Dict type instance AlgebraType0 Final.Ap g = Functor g type instance AlgebraType Final.Ap g = Applicative g@@ -319,8 +330,8 @@ liftFree = Final.liftAp foldNatFree = Final.runAp - proof0 = Proof Dict- proof1 = Proof Dict+ proof1 = Proof Dict+ forget1 = Proof Dict -- | -- @'Day' f f@ newtype wrapper. It is isomorphic with @'Ap' f@ for applicative@@ -346,8 +357,8 @@ foldNatFree nat (DayF day) = Day.dap . Day.trans2 nat . Day.trans1 nat $ day - proof0 = Proof Dict- proof1 = Proof Dict+ proof1 = Proof Dict+ forget1 = Proof Dict -- | -- Algebras of the same type as @'Free'@ monad is the class of all monads.@@ -359,8 +370,8 @@ liftFree = Free.liftF foldNatFree = Free.foldFree - proof0 = Proof Dict- proof1 = Proof Dict+ proof1 = Proof Dict+ forget1 = Proof Dict type instance AlgebraType0 Church.F f = Functor f type instance AlgebraType Church.F m = Monad m@@ -368,8 +379,8 @@ liftFree = Church.liftF foldNatFree = Church.foldF - proof0 = Proof Dict- proof1 = Proof Dict+ proof1 = Proof Dict+ forget1 = Proof Dict type instance AlgebraType0 Alt f = Functor f type instance AlgebraType Alt m = Alternative m@@ -377,8 +388,8 @@ liftFree = Alt.liftAlt foldNatFree = Alt.runAlt - proof0 = Proof Dict- proof1 = Proof Dict+ proof1 = Proof Dict+ forget1 = Proof Dict -- | -- Algebras of the same type as @'L.StateT'@ monad is the class of all state@@ -402,8 +413,8 @@ put s return a - proof0 = Proof Dict- proof1 = Proof Dict+ proof1 = Proof Dict+ forget1 = Proof Dict -- | -- Algebras of the same type as @'S.StateT'@ monad is the class of all state@@ -421,8 +432,8 @@ put s return a - proof0 = Proof Dict- proof1 = Proof Dict+ proof1 = Proof Dict+ forget1 = Proof Dict -- | -- Algebras of the same type as @'L.WriterT'@ monad is the class of all writer@@ -435,8 +446,8 @@ liftFree = lift foldNatFree nat (L.WriterT m) = fst <$> nat m - proof0 = Proof Dict- proof1 = Proof Dict+ proof1 = Proof Dict+ forget1 = Proof Dict -- | -- Algebras of the same type as @'S.WriterT'@ monad is the class of all writer@@ -450,8 +461,8 @@ liftFree = lift foldNatFree nat (S.WriterT m) = fst <$> nat m - proof0 = Proof Dict- proof1 = Proof Dict+ proof1 = Proof Dict+ forget1 = Proof Dict -- | -- Algebras of the same type as @'L.ReaderT'@ monad is the class of all reader@@ -465,8 +476,8 @@ foldNatFree nat (ReaderT g) = ask >>= nat . g - proof0 = Proof Dict- proof1 = Proof Dict+ proof1 = Proof Dict+ forget1 = Proof Dict -- | -- Algebras of the same type as @'S.ReaderT'@ monad is the class of all reader@@ -483,8 +494,8 @@ Left e -> throwError e Right a -> return a - proof0 = Proof Dict- proof1 = Proof Dict+ proof1 = Proof Dict+ forget1 = Proof Dict 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@@ -498,8 +509,8 @@ tell w return a - proof0 = Proof Dict- proof1 = Proof Dict+ proof1 = Proof Dict+ forget1 = Proof Dict 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@@ -513,8 +524,8 @@ tell w return a - proof0 = Proof Dict- proof1 = Proof Dict+ proof1 = Proof Dict+ forget1 = Proof Dict -- | -- Algebra type for @'ListT'@ monad transformer.@@ -539,8 +550,8 @@ a <- foldM (\x y -> x `mappend1_` y) empty as return a - proof0 = Proof Dict- proof1 = Proof Dict+ proof1 = Proof Dict+ forget1 = Proof Dict -- $monadContT --@@ -566,5 +577,5 @@ Nothing -> point Just a -> return a - proof0 = Proof Dict- proof1 = Proof Dict+ proof1 = Proof Dict+ forget1 = Proof Dict
src/Control/Monad/Action.hs view
@@ -45,7 +45,6 @@ instance ( Monad m , FreeAlgebra m , AlgebraType m d- , AlgebraType0 m d ) => MAction m (Const d) where mact mca = Const $ foldFree $ getConst <$> mca@@ -63,5 +62,6 @@ instance Monad m => FreeAlgebra1 (FreeMAction m) where liftFree = FreeMAction . return foldNatFree nat (FreeMAction mfa) = mact $ nat <$> mfa- proof0 = Proof Dict- proof1 = Proof Dict++ proof1 = Proof Dict+ forget1 = Proof Dict
src/Data/Algebra/Free.hs view
@@ -35,7 +35,7 @@ -- -- 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+-- m f@ constraint. This guarantees 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.@@ -71,12 +71,26 @@ => (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 for all @a@, 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)+ -- |+ -- Proof that @AlgebraType0 m a => m a@ is an algebra of type @AlgebraType m@.+ -- This proves that @m@ is a mapping from the full subcategory of @Hask@ of+ -- types satisfying @AlgebraType0 m a@ constraint to the full subcategory+ -- satisfying @AlgebraType m a@, @fmapFree@ below proves that it's a functor.+ proof :: forall a. AlgebraType0 m a => Proof (AlgebraType m (m a)) (m a)+ -- |+ -- Proof that the forgetful functor from types @a@ satisfying @AgelbraType+ -- m a@ to @AlgebraType0 m a@ is well defined.+ forget :: forall a. AlgebraType m a => Proof (AlgebraType0 m a) (m a) + -- | -- Inverse of @'foldMapFree'@+--+-- prop> unFoldMapFree id = returnFree+--+-- Note that @'unFoldMapFree' id@ is the unit of the+-- [unit](https://ncatlab.org/nlab/show/unit+of+an+adjunction) of the+-- adjunction imposed by the @'FreeAlgebra'@ constraint. unFoldMapFree :: FreeAlgebra m => (m a -> d)@@ -84,18 +98,22 @@ unFoldMapFree f = f . returnFree -- |--- All types which satisfy @'FreeAlgebra'@ constraint are foldable. You can--- use this map to build a @'Foldable'@ instance.+-- All types which satisfy @'FreeAlgebra'@ constraint are foldable. -- -- prop> foldFree . returnFree == id+--+-- @foldFree@ is the+-- [unit](https://ncatlab.org/nlab/show/unit+of+an+adjunction) of the+-- adjunction imposed by @FreeAlgebra@ constraint. foldFree- :: ( FreeAlgebra m- , AlgebraType0 m a+ :: forall m a .+ ( FreeAlgebra m , AlgebraType m a ) => m a -> a-foldFree = foldMapFree id+foldFree ma = case forget @m @a of+ Proof Dict -> foldMapFree id ma -- | -- The canonical quotient map from a free algebra of a wider class to a free@@ -112,10 +130,10 @@ -- * @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 m , FreeAlgebra n+ , AlgebraType0 m a+ , AlgebraType m (n a) ) => m a -> n a@@ -132,45 +150,39 @@ => (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 Dict -> foldMapFree (returnFree . f) ma- {-# INLINE go #-}+fmapFree f ma = case proof @m @b of+ Proof Dict -> foldMapFree (returnFree . f) ma -- | -- @'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 Dict -> foldFree mma- {-# INLINE go #-}+joinFree mma = case proof @m @a of+ Proof Dict -> foldFree mma -- | -- The monadic @'bind'@ operator. @'returnFree'@ is the corresponding--- @'return'@ for this monad.-bindFree :: ( FreeAlgebra m+-- @'return'@ for this monad. This just @'foldMapFree'@ in disguise.+bindFree :: forall m a b .+ ( 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+bindFree ma f = case proof @m @b of+ Proof Dict -> foldMapFree 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+-- Another way of putting 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@@ -179,7 +191,6 @@ -- 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 )@@ -196,14 +207,16 @@ foldMapFree f (a :| []) = f a foldMapFree f (a :| (b : bs)) = f a <> foldMapFree f (b :| bs) - proof = Proof Dict+ proof = Proof Dict+ forget = Proof Dict type instance AlgebraType0 [] a = () type instance AlgebraType [] m = Monoid m instance FreeAlgebra [] where returnFree a = [a] foldMapFree = foldMap- proof = Proof Dict+ proof = Proof Dict+ forget = Proof Dict type instance AlgebraType0 Maybe a = () type instance AlgebraType Maybe m = Pointed m@@ -212,4 +225,5 @@ foldMapFree _ Nothing = point foldMapFree f (Just a) = f a - proof = Proof Dict+ proof = Proof Dict+ forget = Proof Dict
src/Data/Group/Free.hs view
@@ -1,7 +1,9 @@ {- | Free groups+ * https://en.wikipedia.org/wiki/Free_group * https://ncatlab.org/nlab/show/Nielsen-Schreier+theorem+ -} module Data.Group.Free ( FreeGroup@@ -102,10 +104,11 @@ 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+type instance AlgebraType FreeGroup g = (Eq 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 Dict+ proof = Proof Dict+ forget = Proof Dict
src/Data/Monoid/Abelian.hs view
@@ -26,8 +26,9 @@ mempty = FreeAbelianMonoid (Map.empty) type instance AlgebraType0 FreeAbelianMonoid a = Ord a-type instance AlgebraType FreeAbelianMonoid m = (Monoid m, AbelianSemigroup m)+type instance AlgebraType FreeAbelianMonoid m = (Ord 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 Dict+ proof = Proof Dict+ forget = Proof Dict
src/Data/Monoid/MSet.hs view
@@ -119,4 +119,5 @@ instance Monoid m => FreeAlgebra (FreeMSet m) where returnFree a = FreeMSet (mempty, a) foldMapFree f (FreeMSet (m, a)) = act m (f a)- proof = Proof Dict+ proof = Proof Dict+ forget = Proof Dict
src/Data/Semigroup/Abelian.hs view
@@ -88,7 +88,7 @@ instance Ord a => AbelianSemigroup (FreeAbelianSemigroup a) type instance AlgebraType0 FreeAbelianSemigroup a = Ord a-type instance AlgebraType FreeAbelianSemigroup a = AbelianSemigroup a+type instance AlgebraType FreeAbelianSemigroup a = (Ord a, AbelianSemigroup a) instance FreeAlgebra FreeAbelianSemigroup where returnFree a = FreeAbelianSemigroup $ Map.singleton a 1 foldMapFree f (FreeAbelianSemigroup as) = foldMapFree f (toNonEmpty_ as)@@ -101,4 +101,5 @@ toNonEmpty_ :: Map a Integer -> NonEmpty a toNonEmpty_ = NE.fromList . concat . map (uncurry replicate_) . Map.toList - proof = Proof Dict+ proof = Proof Dict+ forget = Proof Dict
src/Data/Semigroup/SemiLattice.hs view
@@ -50,9 +50,10 @@ toNonEmpty (FreeSemiLattice as) = NE.fromList $ Set.toList as type instance AlgebraType0 FreeSemiLattice a = Ord a-type instance AlgebraType FreeSemiLattice a = SemiLattice a+type instance AlgebraType FreeSemiLattice a = (Ord 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 Dict+ proof = Proof Dict+ forget = Proof Dict
+ test/Main.hs view
@@ -0,0 +1,22 @@+module Main+ ( 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+ ]
− test/Spec.hs
@@ -1,22 +0,0 @@-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- ]