Data.Functor.Kan.Ran

• Right Kan Extensions

Documentation

newtype Ran g h a

The right Kan extension of a Functor h along a Functor g.

We can define a right Kan extension in several ways. The definition here is obtained by reading off the definition in of a right Kan extension in terms of an End, but we can derive an equivalent definition from the universal property.

Given a Functor h : C -> D and a Functor g : C -> C', we want to find extend h back along g to give Ran g h : C' -> C, such that the natural transformation gran :: Ran g h (g a) -> h a exists.

In some sense this is trying to approximate the inverse of g by using one of its adjoints, because if the adjoint and the inverse both exist, they match!

 Hask -h-> Hask
   |       +
   g      /
   |    Ran g h
   v    /
 Hask -'

The Right Kan extension is unique (up to isomorphism) by taking this as its universal property.

That is to say given any K : C' -> C such that we have a natural transformation from k.g to h (forall x. k (g x) -> h x) there exists a canonical natural transformation from k to Ran g h. (forall x. k x -> Ran g h x).

We could literally read this off as a valid Rank-3 definition for Ran:

 data Ran' g h a = forall z. Functor z => Ran' (forall x. z (g x) -> h x) (z a)

This definition is isomorphic the simpler Rank-2 definition we use below as witnessed by the

 ranIso1 :: Ran g f x -> Ran' g f x
 ranIso1 (Ran e) = Ran' e id

ranIso2 :: Ran' g f x -> Ran g f x
 ranIso2 (Ran' h z) = Ran $ k -> h (k $ z)

 ranIso2 (ranIso1 (Ran e)) ≡ -- by definition
 ranIso2 (Ran' e id) ≡       -- by definition
 Ran $ k -> e (k $ id)    -- by definition
 Ran $ k -> e (k . id)      -- f . id = f
 Ran $ k -> e k             -- eta reduction
 Ran e

The other direction is left as an exercise for the reader.

Constructors

Ran

Fields

runRan :: forall b. (a -> g b) -> h b

Instances

Functor (Ran g h)

toRan :: Functor k => (forall a. k (g a) -> h a) -> k b -> Ran g h b

The universal property of a right Kan extension.

fromRan :: (forall a. k a -> Ran g h a) -> k (g b) -> h b

toRan and fromRan witness a higher kinded adjunction. from (`'Compose'` g) to Ran g

 toRan . fromRan ≡ id
 fromRan . toRan ≡ id

gran :: Ran g h (g a) -> h a

This is the natural transformation that defines a Right Kan extension.

composeRan :: Composition compose => Ran f (Ran g h) a -> Ran (compose f g) h a

 composeRan . decomposeRan ≡ id
 decomposeRan . composeRan ≡ id

decomposeRan :: (Composition compose, Functor f) => Ran (compose f g) h a -> Ran f (Ran g h) a

adjointToRan :: Adjunction f g => f a -> Ran g Identity a

 adjointToRan . ranToAdjoint ≡ id
 ranToAdjoint . adjointToRan ≡ id

ranToAdjoint :: Adjunction f g => Ran g Identity a -> f a

composedAdjointToRan :: (Adjunction f g, Functor h) => h (f a) -> Ran g h a

ranToComposedAdjoint :: Adjunction f g => Ran g h a -> h (f a)

 composedAdjointToRan . ranToComposedAdjoint ≡ id
 ranToComposedAdjoint . composedAdjointToRan ≡ id

repToRan :: Representable u => Key u -> a -> Ran u Identity a

ranToRep :: Representable u => Ran u Identity a -> (Key u, a)

composedRepToRan :: (Representable u, Functor h) => h (Key u, a) -> Ran u h a

ranToComposedRep :: Representable u => Ran u h a -> h (Key u, a)