Safe Haskell | Safe |
---|---|
Language | Haskell2010 |
Synopsis
- type family AlgebraType (f :: k) (a :: l) :: Constraint
- type family AlgebraType0 (f :: k) (a :: l) :: Constraint
- class FreeAlgebra (m :: Type -> Type) where
- data Proof (c :: Constraint) (f :: k) (a :: l) where
- unFoldMapFree :: FreeAlgebra m => (m a -> d) -> a -> d
- foldFree :: (FreeAlgebra m, AlgebraType0 m a, AlgebraType m a) => m a -> a
- natFree :: forall m n a. (AlgebraType m (n a), AlgebraType0 m a, FreeAlgebra m, FreeAlgebra n) => 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, AlgebraType0 m (m a)) => m (m a) -> m a
- bindFree :: (FreeAlgebra m, AlgebraType0 m a, AlgebraType0 m b, AlgebraType0 m (m b)) => m a -> (a -> m b) -> m b
- cataFree :: (FreeAlgebra m, AlgebraType0 m a, AlgebraType m a, Functor m) => Fix m -> 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 guaranees 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
FreeAlgebra class
class FreeAlgebra (m :: Type -> Type) where Source #
A lawful instance has to guarantee that
is an inverse of
unFoldFree
.foldMapFree
This in turn guaranties that m
is a left adjoint functor from Hask 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) | map generators of |
-> m a -> d | returns a homomorphism from |
The freeness property.
proof :: forall a. AlgebraType0 m a => Proof (AlgebraType m (m a)) m a Source #
Proof that
holds, e.g. if AlgebraType
m (m a)m ~ []
then [a]
is a monoid for all a
.
Instances
data Proof (c :: Constraint) (f :: k) (a :: l) where Source #
Proof that a
is an algebra of type
.AlgebraType
m a
Combinators
unFoldMapFree :: FreeAlgebra m => (m a -> d) -> a -> d Source #
Inverse of foldMapFree
foldFree :: (FreeAlgebra m, AlgebraType0 m a, AlgebraType m a) => m a -> a Source #
All types which satisfy
constraint are foldable. You can
use this map to build a FreeAlgebra
instance.Foldable
foldFree . returnFree == id
natFree :: forall m n a. (AlgebraType m (n a), AlgebraType0 m a, FreeAlgebra m, FreeAlgebra n) => 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, AlgebraType0 m (m a)) => m (m a) -> m a Source #
constraint implies FreeAlgebra
Monad
constrain.
bindFree :: (FreeAlgebra m, AlgebraType0 m a, AlgebraType0 m b, AlgebraType0 m (m b)) => m a -> (a -> m b) -> m b Source #
The monadic
operator. bind
is the corresponding
returnFree
for this monad.return
cataFree :: (FreeAlgebra m, AlgebraType0 m a, AlgebraType m a, Functor m) => Fix m -> a Source #
is the initial algebra in the category of algebras of type
Fix
m
, whenever it exists.AlgebraType
m
Another way of puting this is observing that
is isomorphic to 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
. The
category of semigroups, however, does not have the initial object.ana
(_ -> [])