Copyright | (C) 2011-2013 Edward Kmett |
---|---|
License | BSD-style (see the file LICENSE) |
Maintainer | Edward Kmett <ekmett@gmail.com> |
Stability | provisional |
Portability | MPTCs, fundeps |
Safe Haskell | Trustworthy |
Language | Haskell98 |
The covariant form of the Yoneda lemma states that f
is naturally
isomorphic to Yoneda f
.
This is described in a rather intuitive fashion by Dan Piponi in
- newtype Yoneda f a = Yoneda {
- runYoneda :: forall b. (a -> b) -> f b
- liftYoneda :: Functor f => f a -> Yoneda f a
- lowerYoneda :: Yoneda f a -> f a
- maxF :: (Functor f, Ord (f a)) => Yoneda f a -> Yoneda f a -> Yoneda f a
- minF :: (Functor f, Ord (f a)) => Yoneda f a -> Yoneda f a -> Yoneda f a
- maxM :: (Monad m, Ord (m a)) => Yoneda m a -> Yoneda m a -> Yoneda m a
- minM :: (Monad m, Ord (m a)) => Yoneda m a -> Yoneda m a -> Yoneda m a
- yonedaToRan :: Yoneda f a -> Ran Identity f a
- ranToYoneda :: Ran Identity f a -> Yoneda f a
- yonedaToRift :: Yoneda f a -> Rift Identity f a
- riftToYoneda :: Rift Identity f a -> Yoneda f a
Documentation
Yoneda f a
can be viewed as the partial application of fmap
to its second argument.
liftYoneda :: Functor f => f a -> Yoneda f a Source
The natural isomorphism between f
and
given by the Yoneda lemma
is witnessed by Yoneda
fliftYoneda
and lowerYoneda
liftYoneda
.lowerYoneda
≡id
lowerYoneda
.liftYoneda
≡id
lowerYoneda (liftYoneda fa) = -- definition lowerYoneda (Yoneda (f -> fmap f a)) -- definition (f -> fmap f fa) id -- beta reduction fmap id fa -- functor law fa
lift
=liftYoneda
lowerYoneda :: Yoneda f a -> f a Source
as a right Kan extension
yonedaToRan :: Yoneda f a -> Ran Identity f a Source
Yoneda f
can be viewed as the right Kan extension of f
along the Identity
functor.
yonedaToRan
.ranToYoneda
≡id
ranToYoneda
.yonedaToRan
≡id
ranToYoneda :: Ran Identity f a -> Yoneda f a Source
as a right Kan lift
yonedaToRift :: Yoneda f a -> Rift Identity f a Source
Yoneda f
can be viewed as the right Kan lift of f
along the Identity
functor.
yonedaToRift
.riftToYoneda
≡id
riftToYoneda
.yonedaToRift
≡id
riftToYoneda :: Rift Identity f a -> Yoneda f a Source