Nottingham FP Lab Blog

Left Kan extensions of containers

by Thorsten on October 3, 2009.
Tagged as: Lunches.

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 $G \circ J$ is naturally isomorphic to the set of natural transformations $\mathrm{Lan}_J\,F$ to .

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