Data.Algebra.Free

Synopsis

# Free algebra class

class FreeAlgebra (m :: Type -> Type) where Source #

A lawful instance has to guarantee that unFoldFree is an inverse of foldMapFree (in the category of algebras of type AlgebraType m).

This in turn guaranties that m is a left adjoint functor from full subcategory of Hask (of types constrained by AlgebraType0 m) 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@.

Minimal complete definition

Methods

returnFree :: a -> m a Source #

Injective map that embeds generators a into m.

Arguments

 :: (AlgebraType m d, AlgebraType0 m a) => (a -> d) a mappping of generators of m into d -> m a -> d a homomorphism from m a to d

The freeness property.

codom :: forall a. AlgebraType0 m a => Proof (AlgebraType m (m a)) (m a) Source #

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. (codom from codomain)

forget :: forall a. AlgebraType m a => Proof (AlgebraType0 m a) (m a) Source #

Proof that the forgetful functor from types a satisfying AgelbraType m a to AlgebraType0 m a is well defined.

Instances
 Source # Note that '[]' is a free monoid only for monoids which multiplication is strict in the left argument ref. Note that being strict adds additional equation to the monoid laws:undefined <> a = undefinedThus, expectedly we get an equational theory for left right two-sided strict monoids.Snoc lists are free monoids in the class of monoids which are strict in the right argument, Free Monoid and @DList are free in the class of all Haskell monoids. Instance detailsDefined in Data.Algebra.Free MethodsreturnFree :: a -> [a] Source #foldMapFree :: (AlgebraType [] d, AlgebraType0 [] a) => (a -> d) -> [a] -> d Source #codom :: AlgebraType0 [] a => Proof (AlgebraType [] [a]) [a] Source #forget :: AlgebraType [] a => Proof (AlgebraType0 [] a) [a] Source # Source # Instance detailsDefined in Data.Algebra.Free MethodsreturnFree :: a -> Maybe a Source #foldMapFree :: (AlgebraType Maybe d, AlgebraType0 Maybe a) => (a -> d) -> Maybe a -> d Source #codom :: AlgebraType0 Maybe a => Proof (AlgebraType Maybe (Maybe a)) (Maybe a) Source # Source # Instance detailsDefined in Data.Algebra.Free MethodsreturnFree :: a -> Identity a Source #foldMapFree :: (AlgebraType Identity d, AlgebraType0 Identity a) => (a -> d) -> Identity a -> d Source # Source # NonEmpty is the free semigroup in the class of semigroup which are strict in the left argument. Instance detailsDefined in Data.Algebra.Free MethodsreturnFree :: a -> NonEmpty a Source #foldMapFree :: (AlgebraType NonEmpty d, AlgebraType0 NonEmpty a) => (a -> d) -> NonEmpty a -> d Source # Source # DList is isomorphic to Free Monoid; it is free in the class of all monoids. Instance detailsDefined in Data.Algebra.Free MethodsreturnFree :: a -> DList a Source #foldMapFree :: (AlgebraType DList d, AlgebraType0 DList a) => (a -> d) -> DList a -> d Source #codom :: AlgebraType0 DList a => Proof (AlgebraType DList (DList a)) (DList a) Source # Source # Instance detailsDefined in Data.Group.Free MethodsreturnFree :: a -> FreeGroupL a Source #foldMapFree :: (AlgebraType FreeGroupL d, AlgebraType0 FreeGroupL a) => (a -> d) -> FreeGroupL a -> d Source # Source # Instance detailsDefined in Data.Group.Free MethodsreturnFree :: a -> FreeGroup a Source #foldMapFree :: (AlgebraType FreeGroup d, AlgebraType0 FreeGroup a) => (a -> d) -> FreeGroup a -> d Source # Source # Instance detailsDefined in Data.Semigroup.Abelian MethodsfoldMapFree :: (AlgebraType FreeAbelianSemigroup d, AlgebraType0 FreeAbelianSemigroup a) => (a -> d) -> FreeAbelianSemigroup a -> d Source # Source # Instance detailsDefined in Data.Monoid.Abelian MethodsfoldMapFree :: (AlgebraType FreeAbelianMonoid d, AlgebraType0 FreeAbelianMonoid a) => (a -> d) -> FreeAbelianMonoid a -> d Source # Source # Instance detailsDefined in Data.Semigroup.SemiLattice MethodsreturnFree :: a -> FreeSemiLattice a Source #foldMapFree :: (AlgebraType FreeSemiLattice d, AlgebraType0 FreeSemiLattice a) => (a -> d) -> FreeSemiLattice a -> d Source # Source # Instance detailsDefined in Data.Algebra.Free MethodsreturnFree :: a -> Free Semigroup a Source #foldMapFree :: (AlgebraType (Free Semigroup) d, AlgebraType0 (Free Semigroup) a) => (a -> d) -> Free Semigroup a -> d Source # Source # Instance detailsDefined in Data.Algebra.Free MethodsreturnFree :: a -> Free Monoid a Source #foldMapFree :: (AlgebraType (Free Monoid) d, AlgebraType0 (Free Monoid) a) => (a -> d) -> Free Monoid a -> d Source #codom :: AlgebraType0 (Free Monoid) a => Proof (AlgebraType (Free Monoid) (Free Monoid a)) (Free Monoid a) Source #forget :: AlgebraType (Free Monoid) a => Proof (AlgebraType0 (Free Monoid) a) (Free Monoid a) Source # Source # Instance detailsDefined in Data.Algebra.Free MethodsreturnFree :: a -> Free Group a Source #foldMapFree :: (AlgebraType (Free Group) d, AlgebraType0 (Free Group) a) => (a -> d) -> Free Group a -> d Source #codom :: AlgebraType0 (Free Group) a => Proof (AlgebraType (Free Group) (Free Group a)) (Free Group a) Source #forget :: AlgebraType (Free Group) a => Proof (AlgebraType0 (Free Group) a) (Free Group a) Source # Monoid m => FreeAlgebra (FreeMSet m) Source # Instance detailsDefined in Data.Monoid.MSet MethodsreturnFree :: a -> FreeMSet m a Source #foldMapFree :: (AlgebraType (FreeMSet m) d, AlgebraType0 (FreeMSet m) a) => (a -> d) -> FreeMSet m a -> d Source #codom :: AlgebraType0 (FreeMSet m) a => Proof (AlgebraType (FreeMSet m) (FreeMSet m a)) (FreeMSet m a) Source #forget :: AlgebraType (FreeMSet m) a => Proof (AlgebraType0 (FreeMSet m) a) (FreeMSet m a) Source #

## Type level witnesses

newtype Proof (c :: Constraint) (a :: l) Source #

A proof that constraint c holds for type a.

Constructors

 Proof (Dict c)

proof :: c => Proof (c :: Constraint) (a :: l) Source #

Proof smart constructor.

## Algebra type

type family AlgebraType (f :: k) (a :: l) :: Constraint Source #

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

Instances

type family AlgebraType0 (f :: k) (a :: l) :: Constraint Source #

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.

Instances

# Combinators

unFoldMapFree :: FreeAlgebra m => (m a -> d) -> a -> d Source #

Inverse of foldMapFree

unFoldMapFree id = returnFree

Note that unFoldMapFree id is the unit of the unit of the adjunction imposed by the FreeAlgebra constraint.

foldFree :: forall m a. (FreeAlgebra m, AlgebraType m a) => m a -> a Source #

All types which satisfy FreeAlgebra constraint are foldable.

foldFree . returnFree == id

foldFree is the unit of the adjunction imposed by FreeAlgebra constraint.

natFree :: forall m n a. (FreeAlgebra m, FreeAlgebra n, AlgebraType0 m a, AlgebraType m (n a)) => m a -> n a Source #

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.

natFree . natFree == natFree
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

fmapFree :: forall m a b. (FreeAlgebra m, AlgebraType0 m a, AlgebraType0 m b) => (a -> b) -> m a -> m b Source #

All types which satisfy FreeAlgebra constraint are functors. The constraint AlgebraType m (m b) is always satisfied.

joinFree :: forall m a. (FreeAlgebra m, AlgebraType0 m a) => m (m a) -> m a Source #

FreeAlgebra constraint implies Monad constrain.

bindFree :: forall m a b. (FreeAlgebra m, AlgebraType0 m a, AlgebraType0 m b) => m a -> (a -> m b) -> m b Source #

The monadic bind operator. returnFree is the corresponding return for this monad. This just foldMapFree in disguise.

cataFree :: (FreeAlgebra m, AlgebraType m a, Functor m) => Fix m -> a Source #

Fix m is the initial algebra in the category of algebras of type AlgebraType m, whenever it exists.

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 fixToFree = cataFree  For monoids the inverse is given by ana (_ -> []).

foldrFree :: forall m a b. (FreeAlgebra m, AlgebraType m (Endo b), AlgebraType0 m a) => (a -> b -> b) -> b -> m a -> b Source #

A version of foldr, e.g. it can specialize to

• foldrFree @[] :: (a -> b -> b) -> [a] -> b -> b
• foldrFree @NonEmpty :: (a -> b -> b) -> NonEmpty a -> b -> b

foldrFree' :: forall m a b. (FreeAlgebra m, AlgebraType m (Dual (Endo (b -> b))), AlgebraType0 m a) => (a -> b -> b) -> m a -> b -> b Source #

Like foldrFree but strict.

foldlFree :: forall m a b. (FreeAlgebra m, AlgebraType m (Dual (Endo b)), AlgebraType0 m a) => (b -> a -> b) -> b -> m a -> b Source #

Generalizes foldl, e.g. it can specialize to

• foldlFree @[] :: (b -> a -> b) -> b -> [a] -> b
• foldlFree @NonEmpty :: (b -> a -> b) -> b -> NonEmpty a -> b

foldlFree' :: forall m a b. (FreeAlgebra m, AlgebraType m (Endo (b -> b)), AlgebraType0 m a) => (b -> a -> b) -> b -> m a -> b Source #

Like foldlFree but strict.

# General free type

newtype Free c a Source #

Free c a represents free algebra for a constraint c generated by type a.

Constructors

 Free FieldsrunFree :: forall r. c r => (a -> r) -> r
Instances
 Source # Instance detailsDefined in Data.Algebra.Free MethodsreturnFree :: a -> Free Semigroup a Source #foldMapFree :: (AlgebraType (Free Semigroup) d, AlgebraType0 (Free Semigroup) a) => (a -> d) -> Free Semigroup a -> d Source # Source # Instance detailsDefined in Data.Algebra.Free MethodsreturnFree :: a -> Free Monoid a Source #foldMapFree :: (AlgebraType (Free Monoid) d, AlgebraType0 (Free Monoid) a) => (a -> d) -> Free Monoid a -> d Source #codom :: AlgebraType0 (Free Monoid) a => Proof (AlgebraType (Free Monoid) (Free Monoid a)) (Free Monoid a) Source #forget :: AlgebraType (Free Monoid) a => Proof (AlgebraType0 (Free Monoid) a) (Free Monoid a) Source # Source # Instance detailsDefined in Data.Algebra.Free MethodsreturnFree :: a -> Free Group a Source #foldMapFree :: (AlgebraType (Free Group) d, AlgebraType0 (Free Group) a) => (a -> d) -> Free Group a -> d Source #codom :: AlgebraType0 (Free Group) a => Proof (AlgebraType (Free Group) (Free Group a)) (Free Group a) Source #forget :: AlgebraType (Free Group) a => Proof (AlgebraType0 (Free Group) a) (Free Group a) Source # Source # Instance detailsDefined in Data.Algebra.Free Methods(<>) :: Free Semigroup a -> Free Semigroup a -> Free Semigroup a #stimes :: Integral b => b -> Free Semigroup a -> Free Semigroup a # Source # Instance detailsDefined in Data.Algebra.Free Methods(<>) :: Free Monoid a -> Free Monoid a -> Free Monoid a #sconcat :: NonEmpty (Free Monoid a) -> Free Monoid a #stimes :: Integral b => b -> Free Monoid a -> Free Monoid a # Source # Instance detailsDefined in Data.Algebra.Free Methods(<>) :: Free Group a -> Free Group a -> Free Group a #sconcat :: NonEmpty (Free Group a) -> Free Group a #stimes :: Integral b => b -> Free Group a -> Free Group a # Source # Instance detailsDefined in Data.Algebra.Free Methodsmappend :: Free Monoid a -> Free Monoid a -> Free Monoid a #mconcat :: [Free Monoid a] -> Free Monoid a # Source # Instance detailsDefined in Data.Algebra.Free Methodsmappend :: Free Group a -> Free Group a -> Free Group a #mconcat :: [Free Group a] -> Free Group a # Source # Instance detailsDefined in Data.Algebra.Free Methodsinvert :: Free Group a -> Free Group a #pow :: Integral x => Free Group a -> x -> Free Group a # type AlgebraType0 (Free Group) (a :: l) Source # Instance detailsDefined in Data.Algebra.Free type AlgebraType0 (Free Group) (a :: l) = () type AlgebraType0 (Free Monoid) (a :: l) Source # Instance detailsDefined in Data.Algebra.Free type AlgebraType0 (Free Monoid) (a :: l) = () type AlgebraType0 (Free Semigroup) (a :: l) Source # Instance detailsDefined in Data.Algebra.Free type AlgebraType0 (Free Semigroup) (a :: l) = () type AlgebraType (Free Semigroup) (a :: *) Source # Instance detailsDefined in Data.Algebra.Free type AlgebraType (Free Semigroup) (a :: *) = Semigroup a type AlgebraType (Free Monoid) (a :: *) Source # Instance detailsDefined in Data.Algebra.Free type AlgebraType (Free Monoid) (a :: *) = Monoid a type AlgebraType (Free Group) (a :: *) Source # Instance detailsDefined in Data.Algebra.Free type AlgebraType (Free Group) (a :: *) = Group a