kan-extensions-4.2: Kan extensions, Kan lifts, various forms of the Yoneda lemma, and (co)density (co)monads

Copyright(C) 2011-2013 Edward Kmett
LicenseBSD-style (see the file LICENSE)
MaintainerEdward Kmett <ekmett@gmail.com>
Stabilityprovisional
PortabilityGADTs, MPTCs, fundeps
Safe HaskellTrustworthy
LanguageHaskell98

Data.Functor.Coyoneda

Contents

Description

The co-Yoneda lemma for a covariant Functor f states that Coyoneda f is naturally isomorphic to f.

Synopsis

Documentation

data Coyoneda f a where Source

A covariant Functor suitable for Yoneda reduction

Constructors

Coyoneda :: (b -> a) -> f b -> Coyoneda f a 

liftCoyoneda :: f a -> Coyoneda f a Source

Yoneda "expansion"

liftCoyoneda . lowerCoyonedaid
lowerCoyoneda . liftCoyonedaid
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

lowerM :: Monad f => Coyoneda f a -> f a Source

Yoneda reduction given a Monad lets us walk under the existential and apply liftM.

You can view Coyoneda as just the arguments to liftM tupled up.

lower = lowerM = lowerCoyoneda

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.

coyonedaToLan . lanToCoyonedaid
lanToCoyoneda . coyonedaToLanid

as a Left Kan lift

coyonedaToLift :: Coyoneda f a -> Lift Identity f a Source

Coyoneda f is the left Kan lift of f along the Identity functor.

coyonedaToLift . liftToCoyonedaid
liftToCoyoneda . coyonedaToLiftid