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.

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.

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.

A proof that constraint c holds for type a.

Inverse of foldMapFree

unFoldMapFree id = returnFree

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

All types which satisfy FreeAlgebra constraint are foldable.

foldFree . returnFree == id

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

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

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

FreeAlgebra constraint implies Monad constrain.

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

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 (_ -> []). The category of semigroups, however, does not have the initial object.