packages feed

free-algebras 0.0.7.1 → 0.0.7.2

raw patch · 5 files changed

+134/−15 lines, 5 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

ChangeLog.md view
@@ -1,9 +1,12 @@ # Changelog for free-algebras +## Version 0.0.7.2+- Enhanced documentation, and properly attributed fix in ChangeLog.+ ## Version 0.0.7.1 - `Data.Group.Free.normalize` and `Data.Group.Free.normalizeL` are not both   `O(n)`, but the former is implemented using the latter (e.g. transforms-  `DList` to a list).+  `DList` to a list), by Justin Le (https://github.com/mstsg)  ## Version 0.0.7.0 - Poly kinded `Control.Algebra.Free.FreeAlgebra` and
free-algebras.cabal view
@@ -1,5 +1,5 @@ name:           free-algebras-version:        0.0.7.1+version:        0.0.7.2 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, Control, Monads
src/Control/Algebra/Free.hs view
@@ -15,7 +15,7 @@       -- ** Type level witnesses     , Proof (..)     , proof-      -- ** Higher algebra type+      -- ** Higher algebra type \/ constraints     , AlgebraType0     , AlgebraType       -- * Combinators@@ -163,7 +163,7 @@ -- -- * @'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@+-- * @'Control.Monad.Free.retract' :: 'Monad' f => 'Free' f a -> f a@ foldFree1 :: forall m f a .              ( FreeAlgebra1 m              , AlgebraType  m f@@ -177,6 +177,8 @@ -- | -- @'unFoldNatFree'@ is an inverse of @'foldNatFree'@ --+-- It is uniquelly determined by its universal property (by Yonneda lemma):+-- -- prop> unFoldNatFree id = ruturnFree1 -- -- Note that @'unFoldNatFree' id@ is the@@ -192,8 +194,12 @@  -- | -- This is a functor instance for @m@ when considered as an endofuctor of some--- subcategory of @Type -> Type@ (e.g. endofunctors of _Hask_).+-- subcategory of @Type -> Type@ (e.g. endofunctors of /Hask/) and it satisfies+-- the functor laws: --+-- prop> hoistFree1 id = id+-- prop> hoistFree1 f . hoistFree1 g = hoistFree1 (f . g)+-- -- It can be specialized to: -- -- * @'Control.Applicative.Free.hoistAp' :: (forall a. f a -> g a) -> 'Ap' f b -> 'Ap' g b @@@ -289,6 +295,7 @@ -- | -- @'Fix' (m f)@ is the initial /algebra/ of type @'AlgebraType' m@ and -- @'AlgebraType0' f@.+-- cataFree1 :: forall m f a .              ( FreeAlgebra1 m              , AlgebraType  m f
src/Control/Algebra/Free2.hs view
@@ -2,12 +2,24 @@ {-# LANGUAGE PolyKinds           #-} {-# LANGUAGE RankNTypes          #-} +-- |+-- A type class for free objects of kind @k -> k -> Type@, i.e. /graphs/ (we+-- will use this name for types of this kind in this documentation).  Examples+-- include various flavors of /free categories/ and /arrows/ which+-- are not included in this package, see+-- __[free-category](https://hackage.haskell.org/package/free-category)__ on+-- /Hackage/).+-- module Control.Algebra.Free2-    ( FreeAlgebra2 (..)+    ( -- * Free algebra class+      FreeAlgebra2 (..)+      -- ** Type level witnesses     , Proof (..)     , proof+      -- ** Algebra types \/ constraints     , AlgebraType0     , AlgebraType+      -- * Combinators     , wrapFree2     , foldFree2     , unFoldNatFree2@@ -25,22 +37,69 @@ import           Data.Algebra.Free (AlgebraType, AlgebraType0, Proof (..), proof)  -- |--- Free algebra similar to @'FreeAlgebra1'@ and @'FreeAlgebra'@, but for types--- of kind @Type -> Type -> Type@.  Examples include free categories, free--- arrows, etc (see 'free-category' package).+-- Free algebra class similar to @'FreeAlgebra1'@ and @'FreeAlgebra'@, but for+-- types of kind @k -> k -> Type@.+-- class FreeAlgebra2 (m :: (k -> k -> Type) -> k -> k -> Type) where-    liftFree2    :: AlgebraType0 m f => f a b -> m f a b-    foldNatFree2 :: forall (d :: k -> k -> Type) (f :: k -> k -> Type) a b .++    -- |+    -- Lift a graph @f@ satsifying the constraint @'AlgebraType0'@ to+    -- a free its object @m f@.+    --+    liftFree2    :: AlgebraType0 m f+                 => f a b+                 -> m f a b++    -- |+    -- This represents the theorem that @m f@ is indeed free object (as+    -- in propositions as types).  The types of kind @k -> k -> Type@ form+    -- a category, where an arrow from @f :: k -> k -> Type@ to @d :: k ->+    -- k -> Type@ is represented by type @forall x y. f x y -> d x y@.+    -- @foldNatFree2@ states that whenever we have such a morphism and @d@+    -- satisfies the constraint @AlgebraType m d@ then we can construct+    -- a morphism from @m f@ to @d@.+    --+    foldNatFree2 :: forall (d :: k -> k -> Type)+                           (f :: k -> k -> Type) a b .                     ( AlgebraType  m d                     , AlgebraType0 m f                     )                  => (forall x y. f x y -> d x y)                  -> (m f a b -> d a b) -    codom2  :: forall (f :: k -> k -> Type). AlgebraType0 m f => Proof (AlgebraType m (m f)) (m f)-    forget2 :: forall (f :: k -> k -> Type). AlgebraType  m f => Proof (AlgebraType0 m f) (m f)+    -- |+    -- A proof that for each @f@ satisfying @AlgebraType0 m f@, @m f@+    -- satisfies @AlgebraType m (m f)@ constrant.  This means that @m@ is+    -- a well defined /functor/ from the full sub-category of types of+    -- kind @k -> k -> Type@ which satisfy the @AlgebraType0 m@ constraint+    -- to the full subcategory of types of the same kind which satifsfy+    -- the constraint @AlgebraType m@.+    --+    codom2  :: forall (f :: k -> k -> Type).+               AlgebraType0 m f+            => Proof (AlgebraType m (m f)) (m f) -wrapFree2 :: forall (m :: (Type -> Type -> Type) -> Type -> Type -> Type) (f :: Type -> Type -> Type) a b .+    -- | +    -- A proof that each type @f :: k -> k -> Type@ satisfying the+    -- @Algebra m f@ constraint also satisfies @AlgebraType0 m f@.  This+    -- states that there is a well defined /forgetful functor/ from the+    -- category of types of kind @k -> k -> Type@ which satisfy the+    -- @AlgebraType m@ to the category of types of the same kind which+    -- satisfy the @AlgebraType0 m@ constraint.+    --+    forget2 :: forall (f :: k -> k -> Type).+               AlgebraType  m f+            => Proof (AlgebraType0 m f) (m f)++--+-- Combinaators+--++-- | A version of @wrap@ from __free__ package but for graphs.+--+wrapFree2 :: forall (m :: (Type -> Type -> Type) -> Type -> Type -> Type)+                    (f :: Type -> Type -> Type)+                    a b .              ( AlgebraType0 m f              , FreeAlgebra2 m              , Monad (m f a)@@ -50,6 +109,17 @@ wrapFree2 = join . liftFree2 {-# INLINE wrapFree2 #-} +-- | Like @'foldFree'@ or @'foldFree1'@ but for graphs.+-- +-- A lawful instance will satisfy:+--+-- @+--  'foldFree2' . 'liftFree2' == 'id' :: f a b -> f a b+-- @+--+-- It is the [unit](https://ncatlab.org/nlab/show/unit+of+an+adjunction) of+-- adjuction defined by @'FreeAlgebra1'@ class.+-- foldFree2 :: forall (m :: (k -> k -> Type) -> k -> k -> Type)                     (f :: k -> k -> Type)                     a b .@@ -62,6 +132,13 @@     Proof Dict -> foldNatFree2 id {-# INLINE foldFree2 #-} +-- | +-- Inverse of @'foldNatFree2'@.+--+-- It is uniquelly determined by its universal property (by Yonneda lemma):+--+-- prop> unFoldNatFree id = liftFree2+-- unFoldNatFree2     :: forall (m :: (k -> k -> Type) -> k -> k -> Type)               (f :: k -> k -> Type)@@ -74,6 +151,15 @@ unFoldNatFree2 nat = nat . liftFree2 {-# INLINE unFoldNatFree2 #-} +-- |+-- Hoist the underlying graph in the free structure.+-- This is a higher version of a functor (analogous to @'fmapFree'@, which+-- defined functor instance for @'FreeAlgebra'@ instances) and it satisfies the+-- functor laws:+--+-- prop> hoistFree2 id = id+-- prop> hoistFree2 f . hoistFree2 g = hoistFree2 (f . g)+-- hoistFree2 :: forall (m :: (k -> k -> Type) -> k -> k -> Type)                      (f :: k -> k -> Type)                      g a b .@@ -88,6 +174,9 @@     Proof Dict -> foldNatFree2 (liftFree2 . nat) {-# INLINE hoistFree2 #-} +-- |+-- Hoist the top level free structure.+-- hoistFreeH2 :: forall m n f a b .            ( FreeAlgebra2 m            , FreeAlgebra2 n@@ -100,6 +189,10 @@ hoistFreeH2 = foldNatFree2 liftFree2 {-# INLINE hoistFreeH2 #-} +-- |+-- @'FreeAlgebra2' m@ is a monad on some subcategory of graphs (types of kind+-- @k -> k -> Type@), @'joinFree'@ it is the @join@ of this monad.+-- joinFree2 :: forall (m :: (k -> k -> Type) -> k -> k -> Type)                     (f :: k -> k -> Type)                     a b .@@ -113,6 +206,10 @@         Proof Dict -> foldFree2 {-# INLINE joinFree2 #-} +-- |+-- @bind@ of the monad defined by @m@ on the subcategory of graphs (typed of+-- kind @k -> k -> Type@).+-- bindFree2 :: forall m f g a b .              ( FreeAlgebra2 m              , AlgebraType0 m g
src/Data/Algebra/Free.hs view
@@ -15,7 +15,7 @@       -- ** Type level witnesses     , Proof (..)     , proof-    , -- ** Algebra type+    , -- ** Algebra types \/ constraints       AlgebraType     , AlgebraType0       -- * Combinators@@ -139,11 +139,23 @@ -- | -- All types which satisfy @'FreeAlgebra'@ constraint are foldable. --+-- It is uniquelly determined by its universal property (by Yonneda lemma):+-- -- prop> foldFree . returnFree == id -- -- @foldFree@ is the -- [unit](https://ncatlab.org/nlab/show/unit+of+an+adjunction) of the -- adjunction imposed by @FreeAlgebra@ constraint.+--+-- Examples:+--+-- > foldFree @[] = foldMap id+-- >              = foldr (<>) mempty+-- > foldFree @NonEmpty+-- >              = foldr1 (<>)+--+-- Note that @foldFree@ replaces the abstract \/ free algebraic operation in+-- @m a@ to concrete one in @a@. foldFree     :: forall m a .        ( FreeAlgebra  m