## Left Kan extensions of containers

October 3rd, 2009 by ThorstenI 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 to is naturally isomorphic to the set of natural transformations to .

There is a useful explicit representation of Lans using coends:

(for simplicity I assume that the range of the functors is Set).

The coend is actually the quotient of a large -type:

where is the equivalence relation generated by

for any .

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:

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. .

What has this to do with containers? A container is a functor of the form where and . We write . Now given also we can use the coend formula to work out the container representing :

The interesting step isthe 4th equality from the top. I worked it out using the explicit representation of coends as a -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 , where we obtain

which can be further simplified to

Hence, . Indeed, we could have proven this result directly using the Yoneda lemma (which also shows that it doesn’t depend on being a container). Applying this isomorphism to Fin it turns out that there is an isomorphic datatype which isn’t a GADT, namely:

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 always exists (even if G is not a container). However, isn’t necessary a container even if both F and G are.

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

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?

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.

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.