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 | Haskell2010 |
Synopsis
- data Coyoneda (f :: Type -> Type) 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 :: forall (f :: Type -> Type) a. Coyoneda f a -> Lan Identity f a
- lanToCoyoneda :: forall (f :: Type -> Type) a. Lan Identity f a -> Coyoneda f a
Documentation
data Coyoneda (f :: Type -> Type) a where Source #
A covariant Functor
suitable for Yoneda reduction
Instances
liftCoyoneda :: f a -> Coyoneda f a Source #
Yoneda "expansion"
liftCoyoneda
.lowerCoyoneda
≡id
lowerCoyoneda
.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 :: forall (f :: Type -> Type) a. 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
≡id
lanToCoyoneda
.coyonedaToLan
≡id