free-algebras-0.0.8.2: Free algebras

Safe HaskellNone
LanguageHaskell2010

Control.Algebra.Free2

Contents

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

liftFree2, foldNatFree2

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.

codom2 :: forall a. AlgebraType m (m a) => Proof (AlgebraType m (m a)) (m a) 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.

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.

forget2 :: forall a. AlgebraType0 m a => Proof (AlgebraType0 m a) (m a) 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.

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
type AlgebraType0 Coyoneda (g :: l) Source #

Algebras of the same type as Coyoneda are all functors.

Instance details

Defined in Control.Algebra.Free

type AlgebraType0 Coyoneda (g :: l) = ()
type AlgebraType0 DList (a :: l) Source # 
Instance details

Defined in Data.Algebra.Free

type AlgebraType0 DList (a :: l) = ()
type AlgebraType0 Maybe (a :: l) Source # 
Instance details

Defined in Data.Algebra.Free

type AlgebraType0 Maybe (a :: l) = ()
type AlgebraType0 [] (a :: l) Source # 
Instance details

Defined in Data.Algebra.Free

type AlgebraType0 [] (a :: l) = ()
type AlgebraType0 NonEmpty (a :: l) Source # 
Instance details

Defined in Data.Algebra.Free

type AlgebraType0 NonEmpty (a :: l) = ()
type AlgebraType0 Identity (a :: l) Source # 
Instance details

Defined in Data.Algebra.Free

type AlgebraType0 Identity (a :: l) = ()
type AlgebraType0 (Free1 c :: (Type -> Type) -> Type -> Type) (f :: l) Source # 
Instance details

Defined in Control.Algebra.Free

type AlgebraType0 (Free1 c :: (Type -> Type) -> Type -> Type) (f :: l) = ()
type AlgebraType0 (Free Group) (a :: l) Source # 
Instance details

Defined in Data.Algebra.Free

type AlgebraType0 (Free Group) (a :: l) = ()
type AlgebraType0 (Free Monoid) (a :: l) Source # 
Instance details

Defined in Data.Algebra.Free

type AlgebraType0 (Free Monoid) (a :: l) = ()
type AlgebraType0 (Free Semigroup) (a :: l) Source # 
Instance details

Defined in Data.Algebra.Free

type AlgebraType0 (Free Semigroup) (a :: l) = ()
type AlgebraType0 FreeGroupL (a :: Type) Source # 
Instance details

Defined in Data.Group.Free

type AlgebraType0 FreeGroupL (a :: Type) = Eq a
type AlgebraType0 FreeGroup (a :: Type) Source # 
Instance details

Defined in Data.Group.Free

type AlgebraType0 FreeGroup (a :: Type) = Eq a
type AlgebraType0 FreeAbelianSemigroup (a :: Type) Source # 
Instance details

Defined in Data.Semigroup.Abelian

type AlgebraType0 FreeAbelianMonoid (a :: Type) Source # 
Instance details

Defined in Data.Monoid.Abelian

type AlgebraType0 FreeSemilattice (a :: Type) Source # 
Instance details

Defined in Data.Semigroup.Semilattice

type AlgebraType0 MaybeT (m :: Type -> Type) Source # 
Instance details

Defined in Control.Algebra.Free

type AlgebraType0 MaybeT (m :: Type -> Type) = Monad m
type AlgebraType0 F (f :: Type -> Type) Source # 
Instance details

Defined 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 details

Defined in Control.Algebra.Free

type AlgebraType0 Free (f :: Type -> Type) = Functor f
type AlgebraType0 Ap (g :: Type -> Type) Source # 
Instance details

Defined in Control.Algebra.Free

type AlgebraType0 Ap (g :: Type -> Type) = Functor g
type AlgebraType0 Ap (g :: Type -> Type) Source # 
Instance details

Defined 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 details

Defined in Control.Algebra.Free

type AlgebraType0 Ap (g :: Type -> Type) = Functor g
type AlgebraType0 Alt (f :: Type -> Type) Source # 
Instance details

Defined in Control.Algebra.Free

type AlgebraType0 Alt (f :: Type -> Type) = Functor f
type AlgebraType0 ListT (f :: Type -> Type) Source # 
Instance details

Defined 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 details

Defined in Control.Algebra.Free

type AlgebraType0 (FreeMAction m :: (Type -> Type) -> Type -> Type) (f :: Type -> Type) Source # 
Instance details

Defined 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 details

Defined in Control.Algebra.Free

type AlgebraType0 (ExceptT e :: (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 details

Defined 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 details

Defined 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 details

Defined 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 details

Defined in Control.Algebra.Free

type AlgebraType0 (WriterT w :: (Type -> Type) -> Type -> Type) (m :: Type -> Type) = (Monad m, Monoid w)
type AlgebraType0 (ReaderT r :: (k -> Type) -> k -> 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 details

Defined in Control.Algebra.Free

type AlgebraType0 (ReaderT r :: (k -> Type) -> k -> Type) (m :: Type -> Type) = Monad m
type AlgebraType0 (RWST r w s :: (Type -> Type) -> Type -> Type) (m :: Type -> Type) Source # 
Instance details

Defined 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 details

Defined 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
type AlgebraType Identity (a :: l) Source # 
Instance details

Defined in Data.Algebra.Free

type AlgebraType Identity (a :: l) = ()
type AlgebraType [] (m :: Type) Source # 
Instance details

Defined in Data.Algebra.Free

type AlgebraType [] (m :: Type) = Monoid m
type AlgebraType Maybe (m :: Type) Source # 
Instance details

Defined in Data.Algebra.Free

type AlgebraType Maybe (m :: Type) = Pointed m
type AlgebraType NonEmpty (m :: Type) Source # 
Instance details

Defined in Data.Algebra.Free

type AlgebraType DList (a :: Type) Source # 
Instance details

Defined in Data.Algebra.Free

type AlgebraType DList (a :: Type) = Monoid a
type AlgebraType FreeGroupL (g :: Type) Source # 
Instance details

Defined in Data.Group.Free

type AlgebraType FreeGroupL (g :: Type) = (Eq g, Group g)
type AlgebraType FreeGroup (g :: Type) Source # 
Instance details

Defined in Data.Group.Free

type AlgebraType FreeGroup (g :: Type) = (Eq g, Group g)
type AlgebraType FreeAbelianSemigroup (a :: Type) Source # 
Instance details

Defined in Data.Semigroup.Abelian

type AlgebraType FreeAbelianMonoid (m :: Type) Source # 
Instance details

Defined in Data.Monoid.Abelian

type AlgebraType FreeSemilattice (a :: Type) Source # 
Instance details

Defined in Data.Semigroup.Semilattice

type AlgebraType (Free Semigroup) (a :: Type) Source # 
Instance details

Defined in Data.Algebra.Free

type AlgebraType (Free Monoid) (a :: Type) Source # 
Instance details

Defined in Data.Algebra.Free

type AlgebraType (Free Monoid) (a :: Type) = Monoid a
type AlgebraType (Free Group) (a :: Type) Source # 
Instance details

Defined in Data.Algebra.Free

type AlgebraType (Free Group) (a :: Type) = Group a
type AlgebraType MaybeT (m :: Type -> Type) Source # 
Instance details

Defined in Control.Algebra.Free

type AlgebraType MaybeT (m :: Type -> Type) = (Monad m, MonadMaybe m)
type AlgebraType F (m :: Type -> Type) Source # 
Instance details

Defined in Control.Algebra.Free

type AlgebraType F (m :: Type -> Type) = Monad m
type AlgebraType Free (m :: Type -> Type) Source # 
Instance details

Defined in Control.Algebra.Free

type AlgebraType Free (m :: Type -> Type) = Monad m
type AlgebraType Ap (g :: Type -> Type) Source # 
Instance details

Defined in Control.Algebra.Free

type AlgebraType Ap (g :: Type -> Type) = Applicative g
type AlgebraType Ap (g :: Type -> Type) Source # 
Instance details

Defined in Control.Algebra.Free

type AlgebraType Ap (g :: Type -> Type) = Applicative g
type AlgebraType Ap (g :: Type -> Type) Source # 
Instance details

Defined in Control.Algebra.Free

type AlgebraType Ap (g :: Type -> Type) = Applicative g
type AlgebraType Alt (m :: Type -> Type) Source # 
Instance details

Defined in Control.Algebra.Free

type AlgebraType Alt (m :: Type -> Type) = Alternative m
type AlgebraType Coyoneda (g :: Type -> Type) Source # 
Instance details

Defined in Control.Algebra.Free

type AlgebraType Coyoneda (g :: Type -> Type) = Functor g
type AlgebraType ListT (m :: Type -> Type) Source # 
Instance details

Defined in Control.Algebra.Free

type AlgebraType ListT (m :: Type -> Type) = MonadList m
type AlgebraType DayF (g :: Type -> Type) Source # 
Instance details

Defined in Control.Algebra.Free

type AlgebraType DayF (g :: Type -> Type) = Applicative g
type AlgebraType (Free1 c :: (Type -> Type) -> Type -> Type) (f :: Type -> Type) Source # 
Instance details

Defined in Control.Algebra.Free

type AlgebraType (Free1 c :: (Type -> Type) -> Type -> Type) (f :: Type -> Type) = c f
type AlgebraType (FreeMAction m :: (Type -> Type) -> Type -> Type) (f :: Type -> Type) Source # 
Instance details

Defined in Control.Monad.Action

type AlgebraType (FreeMAction m :: (Type -> Type) -> Type -> Type) (f :: Type -> Type) = MAction m f
type AlgebraType (ExceptT e :: (Type -> Type) -> Type -> Type) (m :: Type -> Type) Source # 
Instance details

Defined in Control.Algebra.Free

type AlgebraType (ExceptT e :: (Type -> Type) -> Type -> Type) (m :: Type -> Type) = MonadError e m
type AlgebraType (StateT s :: (Type -> Type) -> Type -> Type) (m :: Type -> Type) Source # 
Instance details

Defined in Control.Algebra.Free

type AlgebraType (StateT s :: (Type -> Type) -> Type -> Type) (m :: Type -> Type) = MonadState s m
type AlgebraType (StateT s :: (Type -> Type) -> Type -> Type) (m :: Type -> Type) Source # 
Instance details

Defined in Control.Algebra.Free

type AlgebraType (StateT s :: (Type -> Type) -> Type -> Type) (m :: Type -> Type) = MonadState s m
type AlgebraType (WriterT w :: (Type -> Type) -> Type -> Type) (m :: Type -> Type) Source # 
Instance details

Defined in Control.Algebra.Free

type AlgebraType (WriterT w :: (Type -> Type) -> Type -> Type) (m :: Type -> Type) = MonadWriter w m
type AlgebraType (WriterT w :: (Type -> Type) -> Type -> Type) (m :: Type -> Type) Source # 
Instance details

Defined in Control.Algebra.Free

type AlgebraType (WriterT w :: (Type -> Type) -> Type -> Type) (m :: Type -> Type) = MonadWriter w m
type AlgebraType (ReaderT r :: (k -> Type) -> k -> Type) (m :: Type -> Type) Source # 
Instance details

Defined in Control.Algebra.Free

type AlgebraType (ReaderT r :: (k -> Type) -> k -> Type) (m :: Type -> Type) = MonadReader r m
type AlgebraType (RWST r w s :: (Type -> Type) -> Type -> Type) (m :: Type -> Type) Source # 
Instance details

Defined in Control.Algebra.Free

type AlgebraType (RWST r w s :: (Type -> Type) -> Type -> Type) (m :: Type -> Type) = MonadRWS r w s m
type AlgebraType (RWST r w s :: (Type -> Type) -> Type -> Type) (m :: Type -> Type) Source # 
Instance details

Defined in Control.Algebra.Free

type AlgebraType (RWST r w s :: (Type -> Type) -> Type -> Type) (m :: Type -> Type) = MonadRWS r w s m

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 #