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

A proof that constraint c holds for type a.

Proof smart constructor.

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.

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 (the initial algebra is a free algebra generated by empty set of generators, e.g. the Viod type).

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 (_ -> []).

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

Like foldrFree but strict.

Generalizes foldl, e.g. it can specialize to

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

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

Like foldlFree but strict.

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