| Safe Haskell | Safe |
|---|---|
| Language | Haskell2010 |
Data.Algebra.Free
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 unFoldFreefoldMapFreeAlgebraType 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@.
Minimal complete definition
Methods
returnFree :: a -> m a Source #
Injective map that embeds generators a into m.
Arguments
| :: (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, fmapFreecodom
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 AlgebraType0 m fAlgebraType
m f* -> * which satisfy 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 unFoldMapFree idFreeAlgebra
foldFree :: forall m a. (FreeAlgebra m, AlgebraType m a) => m a -> a Source #
All types which satisfy 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 FreeAlgebraAlgebraType m (m b)
joinFree :: forall m a. (FreeAlgebra m, AlgebraType0 m a) => m (m a) -> m a Source #
FreeAlgebraMonad constrain.
bindFree :: forall m a b. (FreeAlgebra m, AlgebraType0 m a, AlgebraType0 m b) => m a -> (a -> m b) -> m b Source #
The monadic bindreturnFreereturnfoldMapFree
cataFree :: (FreeAlgebra m, AlgebraType m a, Functor m) => Fix m -> a Source #
Fix mAlgebraType m
Another way of putting this is observing that Fix mm
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 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 foldlFree
General free type
Free c ac generated by
type a.