free-algebras-0.1.0.1: Free algebras

Control.Algebra.Free2

Description

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 on Hackage).

Synopsis

# Free algebra class

class FreeAlgebra2 (m :: (k -> k -> Type) -> k -> k -> Type) where Source #

Free algebra class similar to FreeAlgebra1 and FreeAlgebra, but for types of kind k -> k -> Type.

Minimal complete definition

Methods

liftFree2 :: AlgebraType0 m f => f a b -> m f a b Source #

Lift a graph f satsifying the constraint AlgebraType0 to a free its object m f.

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 Source #

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 nat (liftFree2 tr) = nat tr
foldNatFree2 nat . foldNatFree2 nat' = foldNatFree2 (foldNatFree2 nat . nat')

codom2 :: forall (f :: k -> k -> Type). AlgebraType0 m f => Proof (AlgebraType m (m f)) (m f) Source #

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.

default codom2 :: forall a. AlgebraType m (m a) => Proof (AlgebraType m (m a)) (m a) Source #

forget2 :: forall (f :: k -> k -> Type). AlgebraType m f => Proof (AlgebraType0 m f) (m f) Source #

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.

default forget2 :: forall a. AlgebraType0 m a => Proof (AlgebraType0 m a) (m a) Source #

## Type level witnesses

data Proof (c :: Constraint) (a :: l) where Source #

A proof that constraint c holds for type a.

Constructors

 Proof :: c => Proof c a

## Algebra types / constraints

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

Instances details
 type AlgebraType0 Coyoneda (g :: l) Source # Algebras of the same type as Coyoneda are all functors. Instance detailsDefined in Control.Algebra.Free type AlgebraType0 Coyoneda (g :: l) = () type AlgebraType0 DList (a :: l) Source # Instance detailsDefined in Data.Algebra.Free type AlgebraType0 DList (a :: l) = () type AlgebraType0 Maybe (a :: l) Source # Instance detailsDefined in Data.Algebra.Free type AlgebraType0 Maybe (a :: l) = () type AlgebraType0 [] (a :: l) Source # Instance detailsDefined in Data.Algebra.Free type AlgebraType0 [] (a :: l) = () type AlgebraType0 NonEmpty (a :: l) Source # Instance detailsDefined in Data.Algebra.Free type AlgebraType0 NonEmpty (a :: l) = () type AlgebraType0 Identity (a :: l) Source # Instance detailsDefined in Data.Algebra.Free type AlgebraType0 Identity (a :: l) = () type AlgebraType0 DNonEmpty (a :: l) Source # Instance detailsDefined in Data.Algebra.Free type AlgebraType0 DNonEmpty (a :: l) = () type AlgebraType0 (Free1 c :: (Type -> Type) -> Type -> Type) (f :: l) Source # Instance detailsDefined in Control.Algebra.Free type AlgebraType0 (Free1 c :: (Type -> Type) -> Type -> Type) (f :: l) = () 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 AlgebraType0 FreeGroupL (a :: Type) Source # Instance detailsDefined in Data.Group.Free type AlgebraType0 FreeGroupL (a :: Type) = Eq a type AlgebraType0 FreeGroup (a :: Type) Source # Instance detailsDefined in Data.Group.Free type AlgebraType0 FreeGroup (a :: Type) = Eq a type AlgebraType0 FreeAbelianSemigroup (a :: Type) Source # Instance detailsDefined in Data.Semigroup.Abelian type AlgebraType0 FreeAbelianSemigroup (a :: Type) = Ord a type AlgebraType0 FreeAbelianMonoid (a :: Type) Source # Instance detailsDefined in Data.Monoid.Abelian type AlgebraType0 FreeAbelianMonoid (a :: Type) = Ord a type AlgebraType0 FreeSemilattice (a :: Type) Source # Instance detailsDefined in Data.Semigroup.Semilattice type AlgebraType0 FreeSemilattice (a :: Type) = Ord a type AlgebraType0 MaybeT (m :: Type -> Type) Source # Instance detailsDefined in Control.Algebra.Free type AlgebraType0 MaybeT (m :: Type -> Type) = Monad m type AlgebraType0 F (f :: Type -> Type) Source # Instance detailsDefined in Control.Algebra.Free type AlgebraType0 F (f :: Type -> Type) = Functor f type AlgebraType0 Free (f :: Type -> Type) Source # Algebras of the same type as Free monad is the class of all monads. Instance detailsDefined in Control.Algebra.Free type AlgebraType0 Free (f :: Type -> Type) = Functor f type AlgebraType0 Ap (g :: Type -> Type) Source # Instance detailsDefined in Control.Algebra.Free type AlgebraType0 Ap (g :: Type -> Type) = Functor g type AlgebraType0 Ap (g :: Type -> Type) Source # Instance detailsDefined in Control.Algebra.Free type AlgebraType0 Ap (g :: Type -> Type) = Functor g type AlgebraType0 Ap (g :: Type -> Type) Source # Algebras of the same type as Ap are the applicative functors. Instance detailsDefined in Control.Algebra.Free type AlgebraType0 Ap (g :: Type -> Type) = Functor g type AlgebraType0 Alt (f :: Type -> Type) Source # Instance detailsDefined in Control.Algebra.Free type AlgebraType0 Alt (f :: Type -> Type) = Functor f type AlgebraType0 ListT (f :: Type -> Type) Source # Instance detailsDefined in Control.Algebra.Free type AlgebraType0 ListT (f :: Type -> Type) = Monad f type AlgebraType0 DayF (g :: Type -> Type) Source # Algebras of the same type as DayF are all the applicative functors. Instance detailsDefined in Control.Algebra.Free type AlgebraType0 DayF (g :: Type -> Type) = Applicative g type AlgebraType0 (FreeMAction m :: (Type -> Type) -> Type -> Type) (f :: Type -> Type) Source # Instance detailsDefined in Control.Monad.Action type AlgebraType0 (FreeMAction m :: (Type -> Type) -> Type -> Type) (f :: Type -> Type) = Functor f type AlgebraType0 (ExceptT e :: (Type -> Type) -> Type -> Type) (m :: Type -> Type) Source # Algebras of the same type as ReaderT monad is the class of all reader monads. Instance detailsDefined in Control.Algebra.Free type AlgebraType0 (ExceptT e :: (Type -> Type) -> Type -> Type) (m :: Type -> Type) = Monad m type AlgebraType0 (ReaderT r :: (Type -> Type) -> Type -> Type) (m :: Type -> Type) Source # Algebras of the same type as ReaderT monad is the class of all reader monads.TODO: take advantage of poly-kinded ReaderT Instance detailsDefined in Control.Algebra.Free type AlgebraType0 (ReaderT r :: (Type -> Type) -> Type -> Type) (m :: Type -> Type) = Monad m type AlgebraType0 (StateT s :: (Type -> Type) -> Type -> Type) (m :: Type -> Type) Source # Algebras of the same type as StateT monad is the class of all state monads. Instance detailsDefined in Control.Algebra.Free type AlgebraType0 (StateT s :: (Type -> Type) -> Type -> Type) (m :: Type -> Type) = Monad m type AlgebraType0 (StateT s :: (Type -> Type) -> Type -> Type) (m :: Type -> Type) Source # Algebras of the same type as StateT monad is the class of all state monads. Instance detailsDefined in Control.Algebra.Free type AlgebraType0 (StateT s :: (Type -> Type) -> Type -> Type) (m :: Type -> Type) = Monad m type AlgebraType0 (WriterT w :: (Type -> Type) -> Type -> Type) (m :: Type -> Type) Source # Algebras of the same type as WriterT monad is the class of all writer monads. Instance detailsDefined in Control.Algebra.Free type AlgebraType0 (WriterT w :: (Type -> Type) -> Type -> Type) (m :: Type -> Type) = (Monad m, Monoid w) type AlgebraType0 (WriterT w :: (Type -> Type) -> Type -> Type) (m :: Type -> Type) Source # Algebras of the same type as WriterT monad is the class of all writer monads. Instance detailsDefined in Control.Algebra.Free type AlgebraType0 (WriterT w :: (Type -> Type) -> Type -> Type) (m :: Type -> Type) = (Monad m, Monoid w) type AlgebraType0 (RWST r w s :: (Type -> Type) -> Type -> Type) (m :: Type -> Type) Source # Instance detailsDefined in Control.Algebra.Free type AlgebraType0 (RWST r w s :: (Type -> Type) -> Type -> Type) (m :: Type -> Type) = (Monad m, Monoid w) type AlgebraType0 (RWST r w s :: (Type -> Type) -> Type -> Type) (m :: Type -> Type) Source # Instance detailsDefined in Control.Algebra.Free type AlgebraType0 (RWST r w s :: (Type -> Type) -> Type -> Type) (m :: Type -> Type) = (Monad m, Monoid w)

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

Instances details

# Combinators

wrapFree2 :: forall (m :: (Type -> Type -> Type) -> Type -> Type -> Type) (f :: Type -> Type -> Type) a b. (AlgebraType0 m f, FreeAlgebra2 m, Monad (m f a)) => f a (m f a b) -> m f a b Source #

Version of wrap from free package but for graphs.

foldFree2 :: forall k (m :: (k -> k -> Type) -> k -> k -> Type) (f :: k -> k -> Type) a b. (FreeAlgebra2 m, AlgebraType m f) => m f a b -> f a b Source #

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 of adjuction defined by FreeAlgebra1 class.

unFoldNatFree2 :: forall k (m :: (k -> k -> Type) -> k -> k -> Type) (f :: k -> k -> Type) d a b. (FreeAlgebra2 m, AlgebraType0 m f) => (forall x y. m f x y -> d x y) -> f a b -> d a b Source #

Inverse of foldNatFree2.

It is uniquelly determined by its universal property (by Yonneda lemma):

unFoldNatFree id = liftFree2

hoistFree2 :: forall k (m :: (k -> k -> Type) -> k -> k -> Type) (f :: k -> k -> Type) g a b. (FreeAlgebra2 m, AlgebraType0 m g, AlgebraType0 m f) => (forall x y. f x y -> g x y) -> m f a b -> m g a b Source #

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:

hoistFree2 id = id
hoistFree2 f . hoistFree2 g = hoistFree2 (f . g)

hoistFreeH2 :: forall m n f a b. (FreeAlgebra2 m, FreeAlgebra2 n, AlgebraType0 m f, AlgebraType0 n f, AlgebraType m (n f)) => m f a b -> n f a b Source #

Hoist the top level free structure.

joinFree2 :: forall k (m :: (k -> k -> Type) -> k -> k -> Type) (f :: k -> k -> Type) a b. (FreeAlgebra2 m, AlgebraType0 m f) => m (m f) a b -> m f a b Source #

FreeAlgebra2 m is a monad on some subcategory of graphs (types of kind k -> k -> Type@), joinFree it is the join of this monad.

foldNatFree2 nat . joinFree2 = foldNatFree2 (foldNatFree2 nat)

This property is analogous to foldMap f . concat = foldMap (foldMap f),

bindFree2 :: forall m f g a b. (FreeAlgebra2 m, AlgebraType0 m g, AlgebraType0 m f) => m f a b -> (forall x y. f x y -> m g x y) -> m g a b Source #

bind of the monad defined by m on the subcategory of graphs (types of kind k -> k -> Type).

foldNatFree2 nat (bindFree mf nat') = foldNatFree2 (foldNatFree2 nat . nat') mf

assocFree2 :: forall (m :: (Type -> Type -> Type) -> Type -> Type -> Type) (f :: Type -> Type -> Type) a b. (FreeAlgebra2 m, AlgebraType m f, Functor (m (m f) a)) => m f a (m f a b) -> m (m f) a (f a b) Source #