Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
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@.
returnFree :: a -> m a Source #
Injective map that embeds generators a
into m
.
:: 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 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 (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 uniquelly determined by its universal property (by Yonneda 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 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
(the initial algebra is a free algebra generated by empty
set of generators, e.g. the AlgebraType
mViod
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 ihn the class of all semigroups.
Instances
FreeAlgebra DNonEmpty Source # | |
Defined in Data.Algebra.Free 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 AlgebraType0 DNonEmpty (a :: l) Source # | |
Defined in Data.Algebra.Free | |
type AlgebraType DNonEmpty (m :: Type) Source # | |
Defined in Data.Algebra.Free |