Safe Haskell | None |
---|---|

Language | Haskell2010 |

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

and `FreeAlgebra1`

, but
for types of kind `FreeAlgebra`

`k -> k -> Type`

.

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

Lift a graph `f`

satsifying the constraint

to a free
its object `AlgebraType0`

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

.

## 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 DNonEmpty (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

is implied by the `AlgebraType0`

m f

constraint. This guarantees that there exists a forgetful functor from
the category of types of kind `AlgebraType`

m f`* -> *`

which satisfy

constrain to the category of types of kind `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 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 #

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

, which defined functor
instance for `fmapFree`

instances) and it satisfies the functor laws:`FreeAlgebra`

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 #