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