| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Data.Algebra.Free
Synopsis
- class FreeAlgebra (m :: Type -> Type) where
- returnFree :: a -> m a
- foldMapFree :: forall d a. (AlgebraType m d, AlgebraType0 m a) => (a -> d) -> m a -> d
- codom :: forall a. AlgebraType0 m a => Proof (AlgebraType m (m a)) (m a)
- forget :: forall a. AlgebraType m a => Proof (AlgebraType0 m a) (m a)
- data Proof (c :: Constraint) (a :: l) where
- 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 :: Type -> Constraint) a = Free {
- runFree :: forall r. c r => (a -> r) -> r
- newtype DNonEmpty a = DNonEmpty ([a] -> NonEmpty a)
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@.
Minimal complete definition
Methods
returnFree :: a -> m a Source #
Injective map that embeds generators a into m.
Arguments
| :: forall d a. (AlgebraType m d, AlgebraType0 m a) | |
| => (a -> d) | a mapping 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
default codom :: forall a. AlgebraType m (m a) => Proof (AlgebraType m (m a)) (m a) Source #
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.
default forget :: forall a. AlgebraType0 m a => Proof (AlgebraType0 m a) (m a) Source #
Instances
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 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
| type AlgebraType0 Coyoneda (g :: l) Source # | Algebras of the same type as |
Defined in Control.Algebra.Free | |
| type AlgebraType0 FreeGroup (a :: Type) Source # | |
Defined in Data.Group.Free | |
| type AlgebraType0 FreeGroupL (a :: Type) Source # | |
Defined in Data.Group.Free | |
| type AlgebraType0 FreeAbelianMonoid (a :: Type) Source # | |
Defined in Data.Monoid.Abelian | |
| type AlgebraType0 FreeAbelianSemigroup (a :: Type) Source # | |
Defined in Data.Semigroup.Abelian | |
| type AlgebraType0 FreeSemilattice (a :: Type) Source # | |
Defined in Data.Semigroup.Semilattice | |
| type AlgebraType0 Identity (a :: l) Source # | |
Defined in Data.Algebra.Free | |
| type AlgebraType0 DList (a :: l) Source # | |
Defined in Data.Algebra.Free | |
| type AlgebraType0 DNonEmpty (a :: l) Source # | |
Defined in Data.Algebra.Free | |
| type AlgebraType0 NonEmpty (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 (Free1 c :: (Type -> Type) -> Type -> Type) (f :: l) Source # | |
Defined in Control.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 (Free Group) (a :: l) Source # | |
Defined in Data.Algebra.Free | |
| type AlgebraType0 Alt (f :: 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 Ap (g :: Type -> Type) Source # | |
Defined in Control.Algebra.Free | |
| type AlgebraType0 Ap (g :: 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 F (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 ListT (f :: Type -> Type) Source # | |
Defined in Control.Algebra.Free | |
| type AlgebraType0 MaybeT (m :: Type -> Type) Source # | |
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 (ReaderT r :: (Type -> Type) -> Type -> Type) (m :: Type -> Type) Source # | Algebras of the same type as TODO: take advantage of poly-kinded |
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 (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 # | |
Combinators
unFoldMapFree :: FreeAlgebra m => (m a -> d) -> a -> d Source #
Inverse of foldMapFree
It is uniquely determined by its universal property (by Yoneda lemma):
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.
Examples:
foldFree @[] = foldMap id
= foldr (<>) mempty
foldFree @NonEmpty
= foldr1 (<>)Note that foldFree replaces the abstract / free algebraic operation in
m a to concrete one in a.
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 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 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 (the initial algebra is a free algebra generated by empty
set of generators, e.g. the AlgebraType mVoid type).
Another way of putting 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 .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
newtype Free (c :: Type -> Constraint) a Source #
represents free algebra for a constraint Free c ac generated by
type a.
Instances
DNonEmpty is the free semigroup in the class of all semigroups.
Instances
| FreeAlgebra DNonEmpty Source # | |
Defined in Data.Algebra.Free Methods returnFree :: a -> DNonEmpty a Source # foldMapFree :: (AlgebraType DNonEmpty d, AlgebraType0 DNonEmpty a) => (a -> d) -> DNonEmpty a -> d Source # codom :: AlgebraType0 DNonEmpty a => Proof (AlgebraType DNonEmpty (DNonEmpty a)) (DNonEmpty a) Source # forget :: AlgebraType DNonEmpty a => Proof (AlgebraType0 DNonEmpty a) (DNonEmpty a) Source # | |
| Semigroup (DNonEmpty a) Source # | |
| type AlgebraType DNonEmpty (m :: Type) Source # | |
Defined in Data.Algebra.Free | |
| type AlgebraType0 DNonEmpty (a :: l) Source # | |
Defined in Data.Algebra.Free | |