# Questions on the "free functor" functor

I have recently found out that in Haskell we can to turn a type constructor into a functor, using the "free functor" construction [1, 2, 3]. I would like to understand this construction – the free object of the $$\mathbf{Functor}$$ category – in a categorical setting.

I assume that we have two functors going in opposite directions (the free-forgetful pair) between two categories: one modeling type constructors, of kind * → *; the other modeling functors – type constructors that have more structure (they preserve the functor identity and composition laws). In particular, the "free functor" functor should take a type constructor and turn it into a functor.

Here are some questions that I have:

• What are the categories in question? I assume that $$\mathbf{Functor}$$ can be modeled by $$\left[\mathbf{Set}, \mathbf{Set}\right]$$, but how is the category of type constructors defined and what are its morphisms?
• The "free functor" construction is given by the following definition data CoYoneda f a = forall b. CoYo (f b) (b -> a). How can I understand this definition in categorical terms?
• The "free functor" is missing from the list of free objects on Wikipedia and I was not able to find out much information on it outside the programming languages community. Is this notion limited to type theory? If so, why?

You could interpret a type constructor as a functor $$\left[|\mathbf{Set}|, \mathbf{Set}\right]$$, where $$|\mathbf{Set}|$$ denotes the category consiting of sets as objects and only identity functions as morphisms.
There is a "forgetful" functor from $$\left[\mathbf{Set}, \mathbf{Set}\right]$$ to $$\left[|\mathbf{Set}|, \mathbf{Set}\right]$$ which given a functor $$F : \mathbf{Set} \to \mathbf{Set}$$ it turns it into a functor $$F \circ i : |\mathbf{Set}| \to \mathbf{Set}$$ by precomposing with the inclusion functor $$i : |\mathbf{Set}| \to \mathbf{Set}$$. It forgets how it acts on morphisms.
The free functor you're referring to is an attempt to express the left adjoint of this functor just as for other "free-forgetful pairs". Such left adjoints to a precomposition are known as left Kan extensions. In this case, this would be the left Kan extension of $$F$$ along $$i$$. Using the formula for left Kan extensions in Wikipedia, we would obtain: $$(\mathrm{Lan}_i F)c=\int^m\mathbf{Set}(i~m,c)\cdot F(m)$$ When you translate the coend (i.e. the integral sign) into an existential type, $$\mathbf{Set}(i~m, c)$$ into a function i -> c and $$\cdot$$ into tuples, you obtain a formula similar to Coyoneda. In the set theoretic counterpart there are size issues that affect the existential type, as you are taking the coend on a category which is not small.
• Thanks a lot! I've got a couple of further questions: (i) How should I translate the definition of the "free functor" object in mathematical notation? Given a functor $F : |\mathbf{Set}| \to \mathbf{Set}$ the "free functor" object is $(\mathsf{Free} \; F)(-) = F B \times \mathbf{Set}(B, -)$ – but what is $B$? (As you can tell, I'm not really familiar with existential types) (ii) Could you please give a bit more details on the connection with Kan extensions: the free functor is the left Kan extension of which functor along which functor? Oct 16, 2018 at 12:27
• I have edited the answer. i) The $B$ is existentially quantified by a coend (in the answer, this is $m$); ii) it is the left Kan extension of $F$ along $i$. Oct 16, 2018 at 13:39