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

Language | Haskell2010 |

## Synopsis

- class FreeAlgebra (m :: Type -> Type) where
- newtype Proof (c :: Constraint) (a :: l) = Proof (Dict c)
- proof :: c => Proof (c :: Constraint) (a :: l)
- type family AlgebraType (f :: k) (a :: l) :: Constraint
- type family AlgebraType0 (f :: k) (a :: l) :: Constraint
- unFoldMapFree :: FreeAlgebra m => (m a -> d) -> a -> d
- foldFree :: forall m a. (FreeAlgebra m, AlgebraType m a) => m a -> a
- natFree :: forall m n a. (FreeAlgebra m, FreeAlgebra n, AlgebraType0 m a, AlgebraType m (n a)) => m a -> n a
- fmapFree :: forall m a b. (FreeAlgebra m, AlgebraType0 m a, AlgebraType0 m b) => (a -> b) -> m a -> m b
- joinFree :: forall m a. (FreeAlgebra m, AlgebraType0 m a) => m (m a) -> m a
- bindFree :: forall m a b. (FreeAlgebra m, AlgebraType0 m a, AlgebraType0 m b) => m a -> (a -> m b) -> m b
- cataFree :: (FreeAlgebra m, AlgebraType m a, Functor m) => Fix m -> a
- foldrFree :: forall m a b. (FreeAlgebra m, AlgebraType m (Endo b), AlgebraType0 m a) => (a -> b -> b) -> b -> m a -> b
- foldrFree' :: forall m a b. (FreeAlgebra m, AlgebraType m (Dual (Endo (b -> b))), AlgebraType0 m a) => (a -> b -> b) -> m a -> b -> b
- foldlFree :: forall m a b. (FreeAlgebra m, AlgebraType m (Dual (Endo b)), AlgebraType0 m a) => (b -> a -> b) -> b -> m a -> b
- foldlFree' :: forall m a b. (FreeAlgebra m, AlgebraType m (Endo (b -> b)), AlgebraType0 m a) => (b -> a -> b) -> b -> m a -> b
- newtype Free c a = Free {
- runFree :: forall r. c r => (a -> r) -> r

# Free algebra class

class FreeAlgebra (m :: Type -> Type) where Source #

A lawful instance has to guarantee that

is an inverse of
`unFoldFree`

(in the category of algebras of type `foldMapFree`

).`AlgebraType`

m

This in turn guaranties that `m`

is a left adjoint functor from full
subcategory of Hask (of types constrained by `AlgebraType0`

m) to algebras
of type `AlgebraType`

m```
. The right adjoint is the forgetful functor. The
composition of left adjoin and the right one is always a monad, this is why
we will be able to build monad instance for
```

m@.

returnFree :: a -> m a Source #

Injective map that embeds generators `a`

into `m`

.

:: (AlgebraType m d, AlgebraType0 m a) | |

=> (a -> d) | a mappping of generators of |

-> m a -> d | a homomorphism from |

The freeness property.

codom :: forall a. AlgebraType0 m a => Proof (AlgebraType m (m a)) (m a) Source #

Proof that `AlgebraType0 m a => m a`

is an algebra of type `AlgebraType m`

.
This proves that `m`

is a mapping from the full subcategory of `Hask`

of
types satisfying `AlgebraType0 m a`

constraint to the full subcategory
satisfying `AlgebraType m a`

,

below proves that it's a functor.
(`fmapFree`

from codomain)`codom`

forget :: forall a. AlgebraType m a => Proof (AlgebraType0 m a) (m a) Source #

Proof that the forgetful functor from types `a`

satisfying ```
AgelbraType
m a
```

to `AlgebraType0 m a`

is well defined.

## Instances

## Type level witnesses

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

A proof that constraint `c`

holds for type `a`

.

## Algebra type

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

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

# Combinators

unFoldMapFree :: FreeAlgebra m => (m a -> d) -> a -> d Source #

Inverse of `foldMapFree`

unFoldMapFree id = returnFree

Note that

is the unit of the
unit of the
adjunction imposed by the `unFoldMapFree`

id

constraint.`FreeAlgebra`

foldFree :: forall m a. (FreeAlgebra m, AlgebraType m a) => m a -> a Source #

All types which satisfy

constraint are foldable.`FreeAlgebra`

foldFree . returnFree == id

`foldFree`

is the
unit of the
adjunction imposed by `FreeAlgebra`

constraint.

natFree :: forall m n a. (FreeAlgebra m, FreeAlgebra n, AlgebraType0 m a, AlgebraType m (n a)) => m a -> n a Source #

The canonical quotient map from a free algebra of a wider class to a free algebra of a narrower class, e.g. from a free semigroup to free monoid, or from a free monoid to free commutative monoid, etc.

natFree . natFree == natFree

fmapFree f . natFree == hoistFree . fmapFree f

the constraints:
* the algebra `n a`

is of the same type as algebra `m`

(this is
always true, just GHC cannot prove it here)
* `m`

is a free algebra generated by `a`

* `n`

is a free algebra generated by `a`

fmapFree :: forall m a b. (FreeAlgebra m, AlgebraType0 m a, AlgebraType0 m b) => (a -> b) -> m a -> m b Source #

All types which satisfy

constraint are functors.
The constraint `FreeAlgebra`

is always satisfied.`AlgebraType`

m (m b)

joinFree :: forall m a. (FreeAlgebra m, AlgebraType0 m a) => m (m a) -> m a Source #

constraint implies `FreeAlgebra`

`Monad`

constrain.

bindFree :: forall m a b. (FreeAlgebra m, AlgebraType0 m a, AlgebraType0 m b) => m a -> (a -> m b) -> m b Source #

The monadic

operator. `bind`

is the corresponding
`returnFree`

for this monad. This just `return`

in disguise.`foldMapFree`

cataFree :: (FreeAlgebra m, AlgebraType m a, Functor m) => Fix m -> a Source #

is the initial algebra in the category of algebras of type
`Fix`

m

, whenever it `AlgebraType`

m*exists*.

Another way of putting this is observing that

is isomorphic to `Fix`

m```
m
Void
```

where `m`

is the *free algebra*. This isomorphisms is given by
```
fixToFree :: (FreeAlgebra m, AlgebraType m (m Void), Functor m) => Fix m -> m Void
fixToFree = cataFree
```

For monoids the inverse is given by

.`ana`

(_ -> [])

foldrFree :: forall m a b. (FreeAlgebra m, AlgebraType m (Endo b), AlgebraType0 m a) => (a -> b -> b) -> b -> m a -> b Source #

foldrFree' :: forall m a b. (FreeAlgebra m, AlgebraType m (Dual (Endo (b -> b))), AlgebraType0 m a) => (a -> b -> b) -> m a -> b -> b Source #

Like

but strict.`foldrFree`

foldlFree :: forall m a b. (FreeAlgebra m, AlgebraType m (Dual (Endo b)), AlgebraType0 m a) => (b -> a -> b) -> b -> m a -> b Source #

foldlFree' :: forall m a b. (FreeAlgebra m, AlgebraType m (Endo (b -> b)), AlgebraType0 m a) => (b -> a -> b) -> b -> m a -> b Source #

Like

but strict.`foldlFree`

# General free type

represents free algebra for a constraint `Free`

c a`c`

generated by
type `a`

.