Safe Haskell  None 

Language  Haskell2010 
Synopsis
 class FreeAlgebra1 (m :: (Type > Type) > Type > Type) where
 newtype Proof (c :: Constraint) (a :: l) = Proof (Dict c)
 proof :: c => Proof (c :: Constraint) (a :: l)
 type family AlgebraType0 (f :: k) (a :: l) :: Constraint
 type family AlgebraType (f :: k) (a :: l) :: Constraint
 wrapFree :: (FreeAlgebra1 m, AlgebraType0 m f, Monad (m f)) => f (m f a) > m f a
 foldFree1 :: forall m f a. (FreeAlgebra1 m, AlgebraType m f) => m f a > f a
 unFoldNatFree :: (FreeAlgebra1 m, AlgebraType0 m f) => (forall x. m f x > d x) > f a > d a
 hoistFree1 :: forall m f g a. (FreeAlgebra1 m, AlgebraType0 m g, AlgebraType0 m f) => (forall x. f x > g x) > m f a > m g a
 hoistFreeH :: forall m n f a. (FreeAlgebra1 m, FreeAlgebra1 n, AlgebraType0 m f, AlgebraType0 n f, AlgebraType m (n f)) => m f a > n f a
 joinFree1 :: forall m f a. (FreeAlgebra1 m, AlgebraType0 m f) => m (m f) a > m f a
 bindFree1 :: forall m f g a. (FreeAlgebra1 m, AlgebraType0 m g, AlgebraType0 m f) => m f a > (forall x. f x > m g x) > m g a
 assocFree1 :: forall m f a. (FreeAlgebra1 m, AlgebraType m f, Functor (m (m f))) => m f (m f a) > m (m f) (f a)
 iterFree1 :: forall m f a. (FreeAlgebra1 m, AlgebraType0 m f, AlgebraType m Identity) => (forall x. f x > x) > m f a > a
 cataFree1 :: forall m f a. (FreeAlgebra1 m, AlgebraType m f, Monad f, Traversable (m f)) => Fix (m f) > f a
 newtype DayF f a = DayF {}
 dayToAp :: Applicative f => Day f f a > Ap f a
 apToDay :: Applicative f => Ap f a > Day f f a
 class Monad m => MonadList m where
 class MonadMaybe m where
Documentation
class FreeAlgebra1 (m :: (Type > Type) > Type > Type) where Source #
Higher kinded version of
. Instances includes free functors,
free applicative functors, free monads, state monads etc.FreeAlgebra
A lawful instance should guarantee that
is an isomorphism
with inverses foldNatFree
.unFoldNatFree
This guaranties that m
is a left adjoint functor from the category of
types of kind Type > Type
which satisfy
constraint, to the
category of types of kind AlgebraType0
mType > Type
which satisfy the
constraint. This functor is left adjoin to the forgetful functor (which is
well defined if the laws on AlgebraType
m
family are satisfied. This in
turn guarantees that AlgebraType0
m
composed with this forgetful functor is a monad.
In result we get monadic operations:
For m
such that
subsumes AlgebraType0
this class implies:Monad
MFunctor
viahoist = hoistFree1
MMonad
viaembed = flip bindFree1
MonadTrans
vialift = liftFree
liftFree :: AlgebraType0 m f => f a > m f a Source #
Natural transformation that embeds generators into m
.
:: forall (d :: Type > Type). (AlgebraType m d, AlgebraType0 m f)  
=> (forall x. f x > d x)  a natural transformation which embeds generators of 
> m f a > d a  a morphism from 
The freeness property.
codom1 :: forall f. AlgebraType0 m f => Proof (AlgebraType m (m f)) (m f) Source #
A proof that
holds for all AlgebraType
m (m f)AlgebraType0 f => f
.
Together with
this proves that hoistFree1
FreeAlgebra m => m
is
a functor from the full subcategory of types of kind Type > Type
which satisfy
to ones that satisfy AlgebraType0
m f
.AlgebraType
m f
forget1 :: forall f. AlgebraType m f => Proof (AlgebraType0 m f) (m f) Source #
A proof that the forgetful functor from the full subcategory of types of
kind Type > Type
satisfying
constraint to types
satisfying AlgebraType
m f
is well defined.AlgebraType0
m f
Instances
Type level witnesses
newtype Proof (c :: Constraint) (a :: l) Source #
A proof that constraint c
holds for type a
.
Higher algebra type
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 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
Combinators
wrapFree :: (FreeAlgebra1 m, AlgebraType0 m f, Monad (m f)) => f (m f a) > m f a Source #
Anything that carries
constraint is also an instance of
FreeAlgebra1
, but not vice versa. You can use
MonadFree
to define a wrap
instance.
MonadFree
is an example of a monad which does have an ContT
instance, but has an FreeAlgebra1
instance.MonadFree
The
constrain will be satisfied for many monads through the
Monad
'AlgebraType m'
constraint.
foldFree1 :: forall m f a. (FreeAlgebra1 m, AlgebraType m f) => m f a > f a Source #
implies that FreeAlgebra1
mm f
is a foldable.
foldFree1
.liftFree
==id
:: f a > f a
foldFree1
is the
unit of the
adjunction imposed by FreeAlgebra1
constraint.
It can be specialized to:
lowerCoyoneda
::Functor
f =>Coyoneda
f a > f aretractAp
::Applicative
f =>Ap
f a > f afoldFree
::Monad
m => (forall x. f x > m x) >Free
f a > m a
unFoldNatFree :: (FreeAlgebra1 m, AlgebraType0 m f) => (forall x. m f x > d x) > f a > d a Source #
is an inverse of unFoldNatFree
foldNatFree
unFoldNatFree id = ruturnFree1
Note that
is the
unit of the
adjunction imposed by the unFoldNatFree
id
constraint.FreeAlgebra1
:: (FreeAlgebra1 m, AlgebraType0 m g, AlgebraType0 m f)  
=> (forall x. f x > g x)  a natural transformation 
> m f a  
> m g a 
This is a functor instance for m
when considered as an endofuctor of some
subcategory of Type > Type
(e.g. endofunctors of _Hask_).
It can be specialized to:
hoistFreeH :: forall m n f a. (FreeAlgebra1 m, FreeAlgebra1 n, AlgebraType0 m f, AlgebraType0 n f, AlgebraType m (n f)) => m f a > n f a Source #
joinFree1 :: forall m f a. (FreeAlgebra1 m, AlgebraType0 m f) => m (m f) a > m f a Source #
:: (FreeAlgebra1 m, AlgebraType0 m g, AlgebraType0 m f)  
=> m f a  
> (forall x. f x > m g x)  natural transformation 
> m g a 
Bind operator for the
monad, this is just joinFree1
in
disguise.foldNatFree
For
,
StateT
or
WriterT
(or any ReaderT
such
that FreeAlgebra1
m => m
subsumes AlgebraType0
m
), this is the Monad
m>>=
version of
Control.Monad.Morph.embed
.
assocFree1 :: forall m f a. (FreeAlgebra1 m, AlgebraType m f, Functor (m (m f))) => m f (m f a) > m (m f) (f a) Source #
iterFree1 :: forall m f a. (FreeAlgebra1 m, AlgebraType0 m f, AlgebraType m Identity) => (forall x. f x > x) > m f a > a Source #
Specialization of
; it will further specialize to:foldNatFree
@_ @Identity
\_ >
runIdentity
.lowerCoyoneda
iterAp
::Functor
g => (g a > a) >Ap
g a > aiter
::Functor
f => (f a > a) >Free
f a > a
cataFree1 :: forall m f a. (FreeAlgebra1 m, AlgebraType m f, Monad f, Traversable (m f)) => Fix (m f) > f a Source #
is the initial algebra of type Fix
(m f)
and
AlgebraType
m
.AlgebraType0
f
Day convolution
newtype wrapper. It is isomorphic with Day
f f
for applicative
functors Ap
ff
via
(and dayToAp
).apToDay
Instances
FreeAlgebra1 DayF Source # 

Defined in Control.Algebra.Free liftFree :: AlgebraType0 DayF f => f a > DayF f a Source # foldNatFree :: (AlgebraType DayF d, AlgebraType0 DayF f) => (forall x. f x > d x) > DayF f a > d a Source # codom1 :: AlgebraType0 DayF f => Proof (AlgebraType DayF (DayF f)) (DayF f) Source # forget1 :: AlgebraType DayF f => Proof (AlgebraType0 DayF f) (DayF f) Source #  
Functor (DayF f) Source #  
Applicative f => Applicative (DayF f) Source #  
type AlgebraType0 DayF (g :: * > *) Source #  
Defined in Control.Algebra.Free  
type AlgebraType DayF (g :: * > *) Source #  
Defined in Control.Algebra.Free 