Questions on the "free functor" functor

Question

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?

Answer 1

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.