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

Portability GADTs, MPTCs, fundeps provisional Edward Kmett Trustworthy

Data.Functor.Coyoneda

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 whereSource

A covariant Functor suitable for Yoneda reduction

Constructors

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

Instances

 ComonadTrans Coyoneda MonadTrans Coyoneda Monad m => Monad (Coyoneda m) Functor (Coyoneda f) MonadFix f => MonadFix (Coyoneda f) MonadPlus f => MonadPlus (Coyoneda f) Applicative f => Applicative (Coyoneda f) Foldable f => Foldable (Coyoneda f) Traversable f => Traversable (Coyoneda f) Distributive f => Distributive (Coyoneda f) Representable f => Representable (Coyoneda f) Alternative f => Alternative (Coyoneda f) Comonad w => Comonad (Coyoneda w) Plus f => Plus (Coyoneda f) Alt f => Alt (Coyoneda f) Traversable1 f => Traversable1 (Coyoneda f) Foldable1 f => Foldable1 (Coyoneda f) Apply f => Apply (Coyoneda f) Bind m => Bind (Coyoneda m) Extend w => Extend (Coyoneda w) Adjunction f g => Adjunction (Coyoneda f) (Coyoneda g) (Functor f, Eq (f a)) => Eq (Coyoneda f a) (Functor f, Ord (f a)) => Ord (Coyoneda f a) (Functor f, Read (f a)) => Read (Coyoneda f a) (Functor f, Show (f a)) => Show (Coyoneda f a)

liftCoyoneda :: f a -> Coyoneda f aSource

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 aSource

Yoneda reduction lets us walk under the existential and apply fmap.

Mnemonically, "Yoneda reduction" sounds like and works a bit like β-reduction.

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

lower = lowerM = lowerCoyoneda

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

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 aSource

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 aSource

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

coyonedaToLift . liftToCoyonedaid
liftToCoyoneda . coyonedaToLiftid