Control.Algebra.Free2

Synopsis

Documentation

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

Free algebra similar to FreeAlgebra1 and FreeAlgebra, but for types of kind Type -> Type -> Type. Examples include free categories, free arrows, etc (see 'free-category' package).

Methods

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

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 #

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

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

newtype Proof (c :: Constraint) (a :: l) Source #

A proof that constraint c holds for type a.

Constructors

 Proof (Dict c)

proof :: c => Proof (c :: Constraint) (a :: l) Source #

Proof smart constructor.

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

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 #

foldFree2 :: forall (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 #

unFoldNatFree2 :: forall (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 #

hoistFree2 :: forall (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 #

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 #

joinFree2 :: forall (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 #

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 #

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 #