packages feed

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 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-        ]