1
$\begingroup$

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?
$\endgroup$

1 Answer 1

Reset to default
4
$\begingroup$

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.

$\endgroup$
4
  • $\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, 2018 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, 2018 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, 2018 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 Arlin
    Oct 16, 2018 at 15:55

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .