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.

  • $\begingroup$ 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? $\endgroup$ – Dan Oneață Oct 16 '18 at 12:27
  • 1
    $\begingroup$ 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$. $\endgroup$ – M. Learner Oct 16 '18 at 13:39
  • $\begingroup$ Thanks again! I've only heard about (co)ends, but I plan to study them more closely. Do you have any recommendations on this topic? I couldn't find anything in my go-to books on category theory (Awodey, Leinster, Riehl). $\endgroup$ – Dan Oneață Oct 16 '18 at 14:03
  • 2
    $\begingroup$ Try Fosco Loregian's "This is the (co) end, my only (co)friend", or else head to the classic "Basic Concepts of Enriched Category Theory" by Kelly. $\endgroup$ – Kevin Carlson Oct 16 '18 at 15:55

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.