Copyright | (C) 2011-2016 Edward Kmett |
---|---|
License | BSD-style (see the file LICENSE) |
Maintainer | Edward Kmett <ekmett@gmail.com> |
Stability | provisional |
Portability | MPTCs, fundeps |
Safe Haskell | Trustworthy |
Language | Haskell2010 |
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
Synopsis
- newtype Yoneda (f :: Type -> Type) a = Yoneda {
- runYoneda :: forall b. (a -> b) -> f b
- liftYoneda :: Functor f => f a -> Yoneda f a
- lowerYoneda :: Yoneda f a -> f a
- maxF :: forall (f :: Type -> Type) a. (Functor f, Ord (f a)) => Yoneda f a -> Yoneda f a -> Yoneda f a
- minF :: forall (f :: Type -> Type) a. (Functor f, Ord (f a)) => Yoneda f a -> Yoneda f a -> Yoneda f a
- maxM :: forall (m :: Type -> Type) a. (Monad m, Ord (m a)) => Yoneda m a -> Yoneda m a -> Yoneda m a
- minM :: forall (m :: Type -> Type) a. (Monad m, Ord (m a)) => Yoneda m a -> Yoneda m a -> Yoneda m a
- yonedaToRan :: forall (f :: Type -> Type) a. Yoneda f a -> Ran Identity f a
- ranToYoneda :: forall (f :: Type -> Type) a. Ran Identity f a -> Yoneda f a
Documentation
newtype Yoneda (f :: Type -> Type) a Source #
Yoneda f a
can be viewed as the partial application of fmap
to its second argument.
Instances
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 #
maxF :: forall (f :: Type -> Type) a. (Functor f, Ord (f a)) => Yoneda f a -> Yoneda f a -> Yoneda f a Source #
minF :: forall (f :: Type -> Type) a. (Functor f, Ord (f a)) => Yoneda f a -> Yoneda f a -> Yoneda f a Source #
maxM :: forall (m :: Type -> Type) a. (Monad m, Ord (m a)) => Yoneda m a -> Yoneda m a -> Yoneda m a Source #
minM :: forall (m :: Type -> Type) a. (Monad m, Ord (m a)) => Yoneda m a -> Yoneda m a -> Yoneda m a Source #
as a right Kan extension
yonedaToRan :: forall (f :: Type -> Type) a. 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