Control.Algebra.Free2

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

Free algebra class

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

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

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

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)

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)

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)

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)

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

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

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)

Algebras of the same type as Coyoneda are all functors.

Defined in Control.Algebra.Free

type AlgebraType0 Coyoneda (g :: l) = ()

type AlgebraType0 DList (a :: l)

Defined in Data.Algebra.Free

type AlgebraType0 DList (a :: l) = ()

type AlgebraType0 Maybe (a :: l)

Defined in Data.Algebra.Free

type AlgebraType0 Maybe (a :: l) = ()

type AlgebraType0 [] (a :: l)

Defined in Data.Algebra.Free

type AlgebraType0 [] (a :: l) = ()

type AlgebraType0 NonEmpty (a :: l)

Defined in Data.Algebra.Free

type AlgebraType0 NonEmpty (a :: l) = ()

type AlgebraType0 Identity (a :: l)

Defined in Data.Algebra.Free

type AlgebraType0 Identity (a :: l) = ()

type AlgebraType0 (Free1 c :: (Type -> Type) -> Type -> Type) (f :: l)

Defined in Control.Algebra.Free

type AlgebraType0 (Free1 c :: (Type -> Type) -> Type -> Type) (f :: l) = ()

type AlgebraType0 (Free Group) (a :: l)

Defined in Data.Algebra.Free

type AlgebraType0 (Free Group) (a :: l) = ()

type AlgebraType0 (Free Monoid) (a :: l)

Defined in Data.Algebra.Free

type AlgebraType0 (Free Monoid) (a :: l) = ()

type AlgebraType0 (Free Semigroup) (a :: l)

Defined in Data.Algebra.Free

type AlgebraType0 (Free Semigroup) (a :: l) = ()

type AlgebraType0 FreeGroupL (a :: Type)

Defined in Data.Group.Free

type AlgebraType0 FreeGroupL (a :: Type) = Eq a

type AlgebraType0 FreeGroup (a :: Type)

Defined in Data.Group.Free

type AlgebraType0 FreeGroup (a :: Type) = Eq a

type AlgebraType0 FreeAbelianSemigroup (a :: Type)

Defined in Data.Semigroup.Abelian

type AlgebraType0 FreeAbelianSemigroup (a :: Type) = Ord a

type AlgebraType0 FreeAbelianMonoid (a :: Type)

Defined in Data.Monoid.Abelian

type AlgebraType0 FreeAbelianMonoid (a :: Type) = Ord a

type AlgebraType0 FreeSemilattice (a :: Type)

Defined in Data.Semigroup.Semilattice

type AlgebraType0 FreeSemilattice (a :: Type) = Ord a

type AlgebraType0 MaybeT (m :: Type -> Type)

Defined in Control.Algebra.Free

type AlgebraType0 MaybeT (m :: Type -> Type) = Monad m

type AlgebraType0 F (f :: Type -> Type)

Defined in Control.Algebra.Free

type AlgebraType0 F (f :: Type -> Type) = Functor f

type AlgebraType0 Free (f :: Type -> Type)

Algebras of the same type as Free monad is the class of all monads.

Defined in Control.Algebra.Free

type AlgebraType0 Free (f :: Type -> Type) = Functor f

type AlgebraType0 Ap (g :: Type -> Type)

Defined in Control.Algebra.Free

type AlgebraType0 Ap (g :: Type -> Type) = Functor g

type AlgebraType0 Ap (g :: Type -> Type)

Defined in Control.Algebra.Free

type AlgebraType0 Ap (g :: Type -> Type) = Functor g

type AlgebraType0 Ap (g :: Type -> Type)

Algebras of the same type as Ap are the applicative functors.

Defined in Control.Algebra.Free

type AlgebraType0 Ap (g :: Type -> Type) = Functor g

type AlgebraType0 Alt (f :: Type -> Type)

Defined in Control.Algebra.Free

type AlgebraType0 Alt (f :: Type -> Type) = Functor f

type AlgebraType0 ListT (f :: Type -> Type)

Defined in Control.Algebra.Free

type AlgebraType0 ListT (f :: Type -> Type) = Monad f

type AlgebraType0 DayF (g :: Type -> Type)

Algebras of the same type as DayF are all the applicative functors.

Defined in Control.Algebra.Free

type AlgebraType0 DayF (g :: Type -> Type) = Applicative g

type AlgebraType0 (FreeMAction m :: (Type -> Type) -> Type -> Type) (f :: Type -> Type)

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)

Algebras of the same type as ReaderT monad is the class of all reader monads.

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)

Algebras of the same type as StateT monad is the class of all state monads.

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)

Algebras of the same type as StateT monad is the class of all state monads.

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)

Algebras of the same type as WriterT monad is the class of all writer monads.

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)

Algebras of the same type as WriterT monad is the class of all writer monads.

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)

Algebras of the same type as ReaderT monad is the class of all reader monads.

TODO: take advantage of poly-kinded ReaderT

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)

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)

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

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)

Defined in Data.Algebra.Free

type AlgebraType Identity (a :: l) = ()

type AlgebraType [] (m :: Type)

Defined in Data.Algebra.Free

type AlgebraType [] (m :: Type) = Monoid m

type AlgebraType Maybe (m :: Type)

Defined in Data.Algebra.Free

type AlgebraType Maybe (m :: Type) = Pointed m

type AlgebraType NonEmpty (m :: Type)

Defined in Data.Algebra.Free

type AlgebraType NonEmpty (m :: Type) = Semigroup m

type AlgebraType DList (a :: Type)

Defined in Data.Algebra.Free

type AlgebraType DList (a :: Type) = Monoid a

type AlgebraType FreeGroupL (g :: Type)

Defined in Data.Group.Free

type AlgebraType FreeGroupL (g :: Type) = (Eq g, Group g)

type AlgebraType FreeGroup (g :: Type)

Defined in Data.Group.Free

type AlgebraType FreeGroup (g :: Type) = (Eq g, Group g)

type AlgebraType FreeAbelianSemigroup (a :: Type)

Defined in Data.Semigroup.Abelian

type AlgebraType FreeAbelianSemigroup (a :: Type) = (Ord a, AbelianSemigroup a)

type AlgebraType FreeAbelianMonoid (m :: Type)

Defined in Data.Monoid.Abelian

type AlgebraType FreeAbelianMonoid (m :: Type) = (Ord m, Monoid m, AbelianSemigroup m)

type AlgebraType FreeSemilattice (a :: Type)

Defined in Data.Semigroup.Semilattice

type AlgebraType FreeSemilattice (a :: Type)

type AlgebraType (Free Semigroup) (a :: Type)

Defined in Data.Algebra.Free

type AlgebraType (Free Semigroup) (a :: Type) = Semigroup a

type AlgebraType (Free Monoid) (a :: Type)

Defined in Data.Algebra.Free

type AlgebraType (Free Monoid) (a :: Type) = Monoid a

type AlgebraType (Free Group) (a :: Type)

Defined in Data.Algebra.Free

type AlgebraType (Free Group) (a :: Type) = Group a

type AlgebraType MaybeT (m :: Type -> Type)

Defined in Control.Algebra.Free

type AlgebraType MaybeT (m :: Type -> Type) = (Monad m, MonadMaybe m)

type AlgebraType F (m :: Type -> Type)

Defined in Control.Algebra.Free

type AlgebraType F (m :: Type -> Type) = Monad m

type AlgebraType Free (m :: Type -> Type)

Defined in Control.Algebra.Free

type AlgebraType Free (m :: Type -> Type) = Monad m

type AlgebraType Ap (g :: Type -> Type)

Defined in Control.Algebra.Free

type AlgebraType Ap (g :: Type -> Type) = Applicative g

type AlgebraType Ap (g :: Type -> Type)

Defined in Control.Algebra.Free

type AlgebraType Ap (g :: Type -> Type) = Applicative g

type AlgebraType Ap (g :: Type -> Type)

Defined in Control.Algebra.Free

type AlgebraType Ap (g :: Type -> Type) = Applicative g

type AlgebraType Alt (m :: Type -> Type)

Defined in Control.Algebra.Free

type AlgebraType Alt (m :: Type -> Type) = Alternative m

type AlgebraType Coyoneda (g :: Type -> Type)

Defined in Control.Algebra.Free

type AlgebraType Coyoneda (g :: Type -> Type) = Functor g

type AlgebraType ListT (m :: Type -> Type)

Defined in Control.Algebra.Free

type AlgebraType ListT (m :: Type -> Type) = MonadList m

type AlgebraType DayF (g :: Type -> Type)

Defined in Control.Algebra.Free

type AlgebraType DayF (g :: Type -> Type) = Applicative g

type AlgebraType (Free1 c :: (Type -> Type) -> Type -> Type) (f :: Type -> Type)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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

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

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

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

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

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

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

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)