| Copyright | (C) 2011-2016 Edward Kmett |
|---|---|
| License | BSD-style (see the file LICENSE) |
| Maintainer | Edward Kmett <ekmett@gmail.com> |
| Stability | provisional |
| Portability | GADTs, MPTCs, fundeps |
| Safe Haskell | Trustworthy |
| Language | Haskell98 |
Data.Functor.Coyoneda
Contents
Description
- data Coyoneda f a where
- liftCoyoneda :: f a -> Coyoneda f a
- lowerCoyoneda :: Functor f => Coyoneda f a -> f a
- lowerM :: Monad f => Coyoneda f a -> f a
- hoistCoyoneda :: (forall a. f a -> g a) -> Coyoneda f b -> Coyoneda g b
- coyonedaToLan :: Coyoneda f a -> Lan Identity f a
- lanToCoyoneda :: Lan Identity f a -> Coyoneda f a
Documentation
data Coyoneda f a where Source #
A covariant Functor suitable for Yoneda reduction
Instances
liftCoyoneda :: f a -> Coyoneda f a Source #
Yoneda "expansion"
liftCoyoneda.lowerCoyoneda≡idlowerCoyoneda.liftCoyoneda≡id
lowerCoyoneda (liftCoyoneda fa) = -- by definition lowerCoyoneda (Coyoneda id fa) = -- by definition fmap id fa = -- functor law fa
lift=liftCoyoneda
lowerCoyoneda :: Functor f => Coyoneda f a -> f a Source #
Yoneda reduction lets us walk under the existential and apply fmap.
Mnemonically, "Yoneda reduction" sounds like and works a bit like β-reduction.
http://ncatlab.org/nlab/show/Yoneda+reduction
You can view Coyoneda as just the arguments to fmap tupled up.
lower=lowerM=lowerCoyoneda
hoistCoyoneda :: (forall a. f a -> g a) -> Coyoneda f b -> Coyoneda g b Source #
Lift a natural transformation from f to g to a natural transformation
from Coyoneda f to Coyoneda g.
as a Left Kan extension
coyonedaToLan :: Coyoneda f a -> Lan Identity f a Source #
Coyoneda f is the left Kan extension of f along the Identity functor.
Coyoneda f is always a functor, even if f is not. In this case, it
is called the free functor over f. Note the following categorical fine
print: If f is not a functor, Coyoneda f is actually not the left Kan
extension of f along the Identity functor, but along the inclusion
functor from the discrete subcategory of Hask which contains only identity
functions as morphisms to the full category Hask. (This is because f,
not being a proper functor, can only be interpreted as a categorical functor
by restricting the source category to only contain identities.)
coyonedaToLan.lanToCoyoneda≡idlanToCoyoneda.coyonedaToLan≡id