Functors #
This module provides additional lemmas, definitions, and instances for Functor
s.
Main definitions #
Functor.Const α
is the functor that sends all types toα
.Functor.AddConst α
isFunctor.Const α
but for whenα
has an additive structure.Functor.Comp F G
for functorsF
andG
is the functor composition ofF
andG
.Liftp
andLiftr
respectively lift predicates and relations on a typeα
toF α
. Terms ofF α
are considered to, in some sense, contain values of typeα
.
Tags #
functor, applicative
Const α
is the constant functor, mapping every type to α
. When
α
has a monoid structure, Const α
has an Applicative
instance.
(If α
has an additive monoid structure, see Functor.AddConst
.)
Instances For
Extract the element of α
from the Const
functor.
Instances For
The map operation of the Const γ
functor.
Instances For
AddConst α
is a synonym for constant functor Const α
, mapping
every type to α
. When α
has an additive monoid structure,
AddConst α
has an Applicative
instance. (If α
has a
multiplicative monoid structure, see Functor.Const
.)
Instances For
AddConst.mk
is the canonical map α → AddConst α β
, which is the identity,
where AddConst α β = Const α β
. It can be used as a pattern to extract this value.
Instances For
Extract the element of α
from the constant functor.
Instances For
Construct a term of Comp F G α
from a term of F (G α)
, which is the same type.
Can be used as a pattern to extract a term of F (G α)
.
Instances For
Extract a term of F (G α)
from a term of Comp F G α
, which is the same type.
Instances For
The map operation for the composition Comp F G
of functors F
and G
.
Instances For
The <*>
operation for the composition of applicative functors.
Instances For
If we consider x : F α
to, in some sense, contain values of type α
, then
Liftr r x y
relates x
and y
iff (1) x
and y
have the same shape and
(2) we can pair values a
from x
and b
from y
so that r a b
holds.
Instances For
If f
is a functor, if fb : f β
and a : α
, then mapConstRev fb a
is the result of
applying f.map
to the constant function β → α
sending everything to a
, and then
evaluating at fb
. In other words it's const a <$> fb
.
Instances For
If f
is a functor, if fb : f β
and a : α
, then mapConstRev fb a
is the result of
applying f.map
to the constant function β → α
sending everything to a
, and then
evaluating at fb
. In other words it's const a <$> fb
.