| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
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
- 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
- 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 (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 (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 (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 (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 FreeAlgebra1FreeAlgebrak -> 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 AlgebraType0m 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.
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 |
Defined in Control.Algebra.Free | |
| type AlgebraType0 DList (a :: l) Source # | |
Defined in Data.Algebra.Free | |
| type AlgebraType0 Maybe (a :: l) Source # | |
Defined in Data.Algebra.Free | |
| type AlgebraType0 [] (a :: l) Source # | |
Defined in Data.Algebra.Free type AlgebraType0 [] (a :: l) = () | |
| type AlgebraType0 NonEmpty (a :: l) Source # | |
Defined in Data.Algebra.Free | |
| type AlgebraType0 Identity (a :: l) Source # | |
Defined in Data.Algebra.Free | |
| type AlgebraType0 (Free1 c :: (Type -> Type) -> Type -> Type) (f :: l) Source # | |
Defined in Control.Algebra.Free | |
| type AlgebraType0 (Free Group) (a :: l) Source # | |
Defined in Data.Algebra.Free | |
| type AlgebraType0 (Free Monoid) (a :: l) Source # | |
Defined in Data.Algebra.Free | |
| type AlgebraType0 (Free Semigroup) (a :: l) Source # | |
Defined in Data.Algebra.Free | |
| type AlgebraType0 FreeGroupL (a :: Type) Source # | |
Defined in Data.Group.Free | |
| type AlgebraType0 FreeGroup (a :: Type) Source # | |
Defined in Data.Group.Free | |
| type AlgebraType0 FreeAbelianSemigroup (a :: Type) Source # | |
Defined in Data.Semigroup.Abelian | |
| type AlgebraType0 FreeAbelianMonoid (a :: Type) Source # | |
Defined in Data.Monoid.Abelian | |
| type AlgebraType0 FreeSemilattice (a :: Type) Source # | |
Defined in Data.Semigroup.Semilattice | |
| type AlgebraType0 MaybeT (m :: Type -> Type) Source # | |
Defined in Control.Algebra.Free | |
| type AlgebraType0 F (f :: Type -> Type) Source # | |
Defined in Control.Algebra.Free | |
| type AlgebraType0 Free (f :: Type -> Type) Source # | Algebras of the same type as |
Defined in Control.Algebra.Free | |
| type AlgebraType0 Ap (g :: Type -> Type) Source # | |
Defined in Control.Algebra.Free | |
| type AlgebraType0 Ap (g :: Type -> Type) Source # | |
Defined in Control.Algebra.Free | |
| type AlgebraType0 Ap (g :: Type -> Type) Source # | Algebras of the same type as |
Defined in Control.Algebra.Free | |
| type AlgebraType0 Alt (f :: Type -> Type) Source # | |
Defined in Control.Algebra.Free | |
| type AlgebraType0 ListT (f :: Type -> Type) Source # | |
Defined in Control.Algebra.Free | |
| type AlgebraType0 DayF (g :: Type -> Type) Source # | Algebras of the same type as |
Defined in Control.Algebra.Free | |
| type AlgebraType0 (FreeMAction m :: (Type -> Type) -> Type -> Type) (f :: Type -> Type) Source # | |
Defined in Control.Monad.Action | |
| type AlgebraType0 (ExceptT e :: (Type -> Type) -> Type -> Type) (m :: Type -> Type) Source # | Algebras of the same type as |
Defined in Control.Algebra.Free | |
| type AlgebraType0 (StateT s :: (Type -> Type) -> Type -> Type) (m :: Type -> Type) Source # | Algebras of the same type as |
Defined in Control.Algebra.Free | |
| type AlgebraType0 (StateT s :: (Type -> Type) -> Type -> Type) (m :: Type -> Type) Source # | Algebras of the same type as |
Defined in Control.Algebra.Free | |
| type AlgebraType0 (WriterT w :: (Type -> Type) -> Type -> Type) (m :: Type -> Type) Source # | Algebras of the same type as |
| type AlgebraType0 (WriterT w :: (Type -> Type) -> Type -> Type) (m :: Type -> Type) Source # | Algebras of the same type as |
| type AlgebraType0 (ReaderT r :: (k -> Type) -> k -> Type) (m :: Type -> Type) Source # | Algebras of the same type as TODO: take advantage of poly-kinded |
Defined in Control.Algebra.Free | |
| type AlgebraType0 (RWST r w s :: (Type -> Type) -> Type -> Type) (m :: Type -> Type) Source # | |
| type AlgebraType0 (RWST r w s :: (Type -> Type) -> Type -> Type) (m :: Type -> Type) Source # | |
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 fAlgebraType
m f* -> * which satisfy AlgebraType m* -> * which satisfy the
'AlgebraType0 m constraint.
Instances
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 (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 #
Inverse of foldNatFree2
It is uniquelly determined by its universal property (by Yonneda lemma):
unFoldNatFree id = liftFree2
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 #
Hoist the underlying graph in the free structure.
This is a higher version of a functor (analogous to fmapFreeFreeAlgebra
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 (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 #