Data.Functor.Coyoneda

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

Documentation

data Coyoneda f a where

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)

Comonad w => Comonad (Coyoneda w)

Alternative f => Alternative (Coyoneda f)

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 a

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

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

Mnemonically, "Yoneda reduction" sounds like and works a bit like

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

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

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

 coyonedaToLan . lanToCoyoneda ≡ id
 lanToCoyoneda . coyonedaToLan ≡ id

lanToCoyoneda :: Lan Identity f a -> Coyoneda f a

as a Left Kan lift

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

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

 coyonedaToLift . liftToCoyoneda ≡ id
 liftToCoyoneda . coyonedaToLift ≡ id

liftToCoyoneda :: Functor f => Lift Identity f a -> Coyoneda f a