Module

Data.Coyoneda

#Coyoneda

newtype Coyoneda :: (Type -> Type) -> Type -> Typenewtype Coyoneda f a

The Coyoneda Functor.

Coyoneda f is a Functor for any type constructor f. In fact, it is the free Functor for f, i.e. any natural transformation nat :: f ~> g, can be factor through liftCoyoneda. The natural transformation from Coyoneda f ~> g is given by lowerCoyoneda <<< hoistCoyoneda nat:

lowerCoyoneda <<< hoistCoyoneda nat <<< liftCoyoneda $ fi
= lowerCoyoneda (hoistCoyoneda nat (Coyoneda $ mkExists $ CoyonedaF identity fi))    (by definition of liftCoyoneda)
= lowerCoyoneda (coyoneda identity (nat fi))                                         (by definition of hoistCoyoneda)
= unCoyoneda map (coyoneda identity (nat fi))                                        (by definition of lowerCoyoneda)
= unCoyoneda map (Coyoneda $ mkExists $ CoyonedaF  identity (nat fi))                (by definition of coyoneda)
= map identity (nat fi)                                                              (by definition of unCoyoneda)
= nat fi                                                                       (since g is a Functor)

Constructors

Instances

#CoyonedaF

data CoyonedaF :: (Type -> Type) -> Type -> Type -> Typedata CoyonedaF f a i

Coyoneda is encoded as an existential type using Data.Exists.

This type constructor encodes the contents of the existential package.

#coyoneda

coyoneda :: forall f a b. (a -> b) -> f a -> Coyoneda f b

Construct a value of type Coyoneda f b from a mapping function and a value of type f a.

#unCoyoneda

unCoyoneda :: forall f a r. (forall b. (b -> a) -> f b -> r) -> Coyoneda f a -> r

Deconstruct a value of Coyoneda a to retrieve the mapping function and original value.

#liftCoyoneda

liftCoyoneda :: forall f. f ~> (Coyoneda f)

Lift a value described by the type constructor f to Coyoneda f.

Note that for any functor f liftCoyoneda has a right inverse lowerCoyoneda:

liftCoyoneda <<< lowerCoyoneda $ (Coyoneda e)
= liftCoyoneda <<< unCoyoneda map $ (Coyoneda e)
= liftCoyonead (runExists (\(CoyonedaF k fi) -> map k fi) e)
= liftCoyonead (Coyoneda e)
= coyoneda identity (Coyoneda e)
= Coyoneda e

Moreover if f is a Functor then liftCoyoneda is an isomorphism of functors with inverse lowerCoyoneda: we already showed that lowerCoyoneda <<< hoistCoyoneda identity = lowerCoyoneda is its left inverse whenever f is a functor.

#lowerCoyoneda

lowerCoyoneda :: forall f. Functor f => (Coyoneda f) ~> f

Lower a value of type Coyoneda f a to the Functor f.

#hoistCoyoneda

hoistCoyoneda :: forall f g. (f ~> g) -> (Coyoneda f) ~> (Coyoneda g)

Use a natural transformation to change the generating type constructor of a Coyoneda.

Modules