Safe Haskell	Safe-Inferred
Language	Haskell2010

Control.Algebra.Free2

Contents

Free algebra class
- Type level witnesses
- Algebra types / constraints
Combinators

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

class FreeAlgebra2 (m :: (k -> k -> Type) -> k -> k -> Type) where
- liftFree2 :: AlgebraType0 m f => f a b -> m f a b
- 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
- codom2 :: forall (f :: k -> k -> Type). AlgebraType0 m f => Proof (AlgebraType m (m f)) (m f)
- forget2 :: forall (f :: k -> k -> Type). AlgebraType m f => Proof (AlgebraType0 m f) (m f)
data Proof (c :: Constraint) (a :: l) where
- Proof :: c => Proof c a
type family AlgebraType0 (f :: k) (a :: l) :: Constraint
type family AlgebraType (f :: k) (a :: l) :: Constraint
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
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
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
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
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
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
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
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)

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 satisfying 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) constraint. 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 satisfy 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 details Defined in Control.Algebra.Free type AlgebraType0 Coyoneda (g :: l) = ()
type AlgebraType0 FreeGroup (a :: Type) Source #
Instance details Defined in Data.Group.Free type AlgebraType0 FreeGroup (a :: Type) = Eq a
type AlgebraType0 FreeGroupL (a :: Type) Source #
Instance details Defined in Data.Group.Free type AlgebraType0 FreeGroupL (a :: Type) = Eq a
type AlgebraType0 FreeAbelianMonoid (a :: Type) Source #
Instance details Defined in Data.Monoid.Abelian type AlgebraType0 FreeAbelianMonoid (a :: Type) = Ord a
type AlgebraType0 FreeAbelianSemigroup (a :: Type) Source #
Instance details Defined in Data.Semigroup.Abelian type AlgebraType0 FreeAbelianSemigroup (a :: Type) = Ord a
type AlgebraType0 FreeSemilattice (a :: Type) Source #
Instance details Defined in Data.Semigroup.Semilattice type AlgebraType0 FreeSemilattice (a :: Type) = Ord a
type AlgebraType0 Identity (a :: l) Source #
Instance details Defined in Data.Algebra.Free type AlgebraType0 Identity (a :: l) = ()
type AlgebraType0 DList (a :: l) Source #
Instance details Defined in Data.Algebra.Free type AlgebraType0 DList (a :: l) = ()
type AlgebraType0 DNonEmpty (a :: l) Source #
Instance details Defined in Data.Algebra.Free type AlgebraType0 DNonEmpty (a :: l) = ()
type AlgebraType0 NonEmpty (a :: l) Source #
Instance details Defined in Data.Algebra.Free type AlgebraType0 NonEmpty (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 (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 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 (Free Group) (a :: l) Source #
Instance details Defined in Data.Algebra.Free type AlgebraType0 (Free Group) (a :: l) = ()
type AlgebraType0 Alt (f :: Type -> Type) Source #
Instance details Defined in Control.Algebra.Free type AlgebraType0 Alt (f :: Type -> Type) = Functor f
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 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 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 F (f :: Type -> Type) Source #
Instance details Defined in Control.Algebra.Free type AlgebraType0 F (f :: Type -> Type) = Functor 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 DayF (g :: Type -> Type) = Applicative g
type AlgebraType0 ListT (f :: Type -> Type) Source #
Instance details Defined in Control.Algebra.Free type AlgebraType0 ListT (f :: Type -> Type) = Monad f
type AlgebraType0 MaybeT (m :: Type -> Type) Source #
Instance details Defined in Control.Algebra.Free type AlgebraType0 MaybeT (m :: Type -> Type) = Monad m
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 (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 details Defined 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 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 (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

Instances details

type AlgebraType DList (a :: Type) Source #
Instance details Defined in Data.Algebra.Free type AlgebraType DList (a :: Type) = Monoid a
type AlgebraType DNonEmpty (m :: Type) Source #
Instance details Defined in Data.Algebra.Free type AlgebraType DNonEmpty (m :: Type) = Semigroup m
type AlgebraType FreeGroup (g :: Type) Source #
Instance details Defined in Data.Group.Free type AlgebraType FreeGroup (g :: Type) = (Eq g, Group g)
type AlgebraType FreeGroupL (g :: Type) Source #
Instance details Defined in Data.Group.Free type AlgebraType FreeGroupL (g :: Type) = (Eq g, Group g)
type AlgebraType FreeAbelianMonoid (m :: Type) Source #
Instance details Defined in Data.Monoid.Abelian type AlgebraType FreeAbelianMonoid (m :: Type) = (Ord m, Monoid m, AbelianSemigroup m)
type AlgebraType FreeAbelianSemigroup (a :: Type) Source #
Instance details Defined in Data.Semigroup.Abelian type AlgebraType FreeAbelianSemigroup (a :: Type) = (Ord a, AbelianSemigroup a)
type AlgebraType FreeSemilattice (a :: Type) Source #
Instance details Defined in Data.Semigroup.Semilattice type AlgebraType FreeSemilattice (a :: Type)
type AlgebraType NonEmpty (m :: Type) Source #
Instance details Defined in Data.Algebra.Free type AlgebraType NonEmpty (m :: Type) = Semigroup m
type AlgebraType Maybe (m :: Type) Source #
Instance details Defined in Data.Algebra.Free type AlgebraType Maybe (m :: Type) = Pointed m
type AlgebraType [] (m :: Type) Source #
Instance details Defined in Data.Algebra.Free type AlgebraType [] (m :: Type) = Monoid m
type AlgebraType Identity (a :: l) Source #
Instance details Defined in Data.Algebra.Free type AlgebraType Identity (a :: l) = ()
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 Semigroup) (a :: Type) Source #
Instance details Defined in Data.Algebra.Free type AlgebraType (Free Semigroup) (a :: Type) = Semigroup 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 Alt (m :: Type -> Type) Source #
Instance details Defined in Control.Algebra.Free type AlgebraType Alt (m :: Type -> Type) = Alternative 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 Free (m :: Type -> Type) Source #
Instance details Defined in Control.Algebra.Free type AlgebraType Free (m :: Type -> Type) = Monad 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 DayF (g :: Type -> Type) Source #
Instance details Defined in Control.Algebra.Free type AlgebraType DayF (g :: Type -> Type) = Applicative g
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 MaybeT (m :: Type -> Type) Source #
Instance details Defined in Control.Algebra.Free type AlgebraType MaybeT (m :: Type -> Type) = (Monad m, MonadMaybe m)
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 (ReaderT r :: (Type -> Type) -> Type -> Type) (m :: Type -> Type) Source #
Instance details Defined in Control.Algebra.Free type AlgebraType (ReaderT r :: (Type -> Type) -> Type -> Type) (m :: Type -> Type) = MonadReader r 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 (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 adjunction 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 uniquely determined by its universal property (by Yoneda 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 mis a monad on some subcategory of graphs (types of kindk -> 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 #