«
»

Left Kan extensions of containers

October 3rd, 2009 by Thorsten

I find that it is often helpful to look at operations on functors instead of datatypes. An example is the exponential of functors which turns out to be an operation on containers. Recently, I have been looking at left Kan extensions, or short Lans. Left Kan extensions are defined as the left adjoint to composition, i.e. the set of natural transformations from F to G \circ J is naturally isomorphic to the set of natural transformations \mathrm{Lan}_J\,F to G.

There is a useful explicit representation of Lans using coends:
\mathrm{Lan}_J\,F = \int^X(J\,X \to A)\times F\,X
(for simplicity I assume that the range of the functors is Set).
The coend is actually the quotient of a large \Sigma-type:
\dots = (\Sigma X.(J\,X \to A)\times F\,X)/\sim
where \sim is the equivalence relation generated by
(X,g\circ J\,h,x) \sim (Y,g,F\,h\,x)
for any h\in X\to Y.

Neil Ghani found a nice application of Lans to give initial algebra semantics to GADTs. As an example consider an encoding of Fin as a GADT:
\begin{code} data Fin : Set -> Set where fz : Fin (Maybe a) fs : Fin a -> Fin (Maybe a) \end{code}
Can we understand Fin as an initial algebra of an endofunctor on the category of endofunctors. A problem is the occurence of Maybe on the right hand side. Using Lans we can shift this on the right, i.e. Fin = \mu H.\mathrm{Lan}_\mathrm{Maybe}\,(1 + H).

What has this to do with containers? A container is a functor of the form F\,X = \Sigma s\in S.P\,s \to X where S\in\mathrm{Set} and P\in S\to\mathrm{Set}. We write F = S \lhd P. Now given also G = T\lhd Q we can use the coend formula to work out the container representing \mathrm{Lan}_F\,G:
\begin{eqnarray*} \mathrm{Lan}_F\,G\,A & = & \int^X (F\,X \to A) \times G\,X \\ & = & \int^X (\Sigma s\in S.P\,s \to X) \to A) \times \Sigma t\in T.Q\,t \to X \\ & \simeq & \Sigma t\in T.\int^X (\Sigma s\in S.P\,s \to X) \to A) \times Q\,t \to X \\ & \simeq & \Sigma t\in T.(\Sigma s\in S.P\,s \to Q\,t) \to A)\\ & = & t \in T \lhd \Sigma s\in S.P\,s \to Q\,t \end{eqnarray*}
The interesting step isthe 4th equality from the top. I worked it out using the explicit representation of coends as a \Sigma-type, but maybe there is a more abstract way to prove it. I also checked the equations by plugging it into the definition of a Lan as an adjunction using the explicit representation of container morphisms.

Now if we apply the formula to Lan_{\mathrm{Maybe}}\,G, where \mathrm{Maybe} = b\in 2 \lhd b=1 we obtain
Lan_{\mathrm{Maybe}}\,G = t\in T \lhd \Sigma b\in 2.(b=1)\to Q\,t
which can be further simplified to
\dots = \in T \lhd 1 + Q\,t
Hence, Lan_{\mathrm{Maybe}}\,G\,A = A \times G\,A. Indeed, we could have proven this result directly using the Yoneda lemma (which also shows that it doesn’t depend on G being a container). Applying this isomorphism to Fin it turns out that there is an isomorphic datatype which isn’t a GADT, namely:
\begin{code} data Fin' : Set -> Set where fz' : a -> Fin' a fs' : a -> Fin' a -> Fin' a \end{code}
I leave it to the reader to work out the isomorphism between Fin and Fin’.

Btw, what about Right Kan Extensions? I can show that if F is a container then \mathrm{Ran}_F\,G always exists (even if G is not a container). However, \mathrm{Ran}_F\,G isn’t necessary a container even if both F and G are.

This entry was posted on Saturday, October 3rd, 2009 at 6:02 pm and is filed under Lunches. You can follow any responses to this entry through the RSS 2.0 feed. You can leave a response, or trackback from your own site.

4 Responses to “Left Kan extensions of containers”

  1. Derek Elkins Says:
    October 3rd, 2009 at 11:24 pm

    F = S <| P = Lan_P (K_S 1)
    G = T <| Q = Lan_Q (K_T 1)
    K the constant functor
    Lan_H o Lan_K = Lan_(H o K)
    provided everything exists, particularly Lan_K
    So, Lan_F G = (Lan_F o Lan_Q) (K_T 1) = Lan_(F o Q) (K_T 1) = T <| F o Q

  2. Thorsten Says:
    October 4th, 2009 at 5:50 pm

    Looks interesting, but I don’t (yet) get it.
    P : S -> Set, do you view S here as a discrete category?
    Also the 2nd argument should be a functor, but K_S 1 is a Set.
    Why is S <| P a Lan?

  3. Derek Elkins Says:
    October 4th, 2009 at 7:35 pm

    Yes, I’m treating S and T as the discrete categories generated by the sets.

    My notation was somewhat ill-defined. K_S was intended to mean the constant functor over the discrete category generated from S, S is not being passed to it. It is just K1 : S -> Set. I didn’t want S and T to completely disappear. (Also, in Lan_H o Lan_K, I meant arbitrary H and K, I just wasn’t thinking there.)

    The representation of the (semantics of) containers as left Kan extensions comes from “Constructing Polymorphic Programs with Quotient Types.” However, you can also arrive at it by using the explicit representation in terms of coends. Using the names from the explicit representation for Lan_J F, F = K1 and the equivalence ~ is just the identity relation since we are “integrating” over a discrete category. The coend becomes just the dependent sum and the product trivializes to just the left component.

  4. Peter Morris Says:
    October 7th, 2009 at 1:01 pm

    Unfortunately the example above does not work, since your assumption that Fin is an endofunctor is not true. This should have been obvious since the type Fin’ you construct is the type of non-empty lists, which is rather different than Fin.

    It might be an interesting question what this means for GADTs which _are_ functors in the Haskell sense, but I suspect these GADTs are already trivially reducible to plain Haskell data types.

Leave a Reply