Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: learning: questions

Topic: Can't type Y: but y?

fosco (Sep 08 2020 at 22:06):

-> This question has an elementary nature (an exercise on the impossibility to type the $Y$ combinator, precisely Exercise 90 here); it becomes a purely category-theoretic problem. I would like to know more from connoisseurs of $\lambda$-calculus.

To my eye, "the" reason why one can't type the $Y$ combinator $\lambda f.(\lambda f.f(xx))\lambda f.f(xx)$ is that if $xx$ had a type, this would be an infinite tower of $B$'s for some type $B$: $x : B^{B^{B^{B^\dots}}}$. (More formally: whatever the type $X$ of $x$ is, it must solve the equation $X=B^X$ for some function type.) Nowhere in the syntax the existence of such type is granted. And in the end, $\lambda$-calculus was invented exactly to prevent these illegal self-applications.

Nice and clear. But.

This means that something should go wrong when instead of "$\lambda$-calculus" I say "[language of a] cartesian closed category"; what, exactly?

I agree that in principle there is no reason for the "infinite internal hom" $[[[[\dots,B],B],B],B]$ to exist. Yet, if the ambient category is sufficiently co/complete, say it is $\sf Set$, I can consider infinite products $((\dots\times B)\times B)\times B$: why shouldn't I consider also infinite iterations of the right adjoints of $-\times B$?

What, exactly, prevents me from building a type/set $X$ that is a solution of the equation $X\cong B^X$?

Stop me when this argument isn't legitimate any more: consider the functor $[-,B]:{\cal C} \to {\cal C}$ of your favourite cartesian closed category. Consider the diagram

${\cal C} \xrightarrow{[-,B]} {\cal C} \xrightarrow{[-,B]} {\cal C} \xrightarrow{[-,B]} {\cal C} \xrightarrow{[-,B]} \dots$

and its transfinite composition ${\cal C} \xrightarrow{F_B} {\cal C}$ (I think said colimit is an object of the category of functors ${\cal C} \to {\cal C}$, am I wrong?). Now, the image of $B$ under the functor $F_B$ "can't be", because it should exactly be the infamous $[[[[\dots,B],B],B],B]$. What's wrong, then?

Dan Doel (Sep 08 2020 at 22:24):

Nothing prevents you from having CCCs with solutions to $X \cong B^X$ in general. And $X \cong X^X$ are used as models for the untyped lambda calculus.

fosco (Sep 08 2020 at 22:27):

Thanks! So, what is the precise sense in which "I can't type $\mathbb Y$"?

Dan Doel (Sep 08 2020 at 22:27):

For sets these are generally shown not to exist by some variation on Cantor's diagonal argument.

Dan Doel (Sep 08 2020 at 22:29):

http://emis.matem.unam.mx/journals/TAC/reprints/articles/15/tr15.pdf

Here's a fancy Lawvere paper on the subject.

Dan Doel (Sep 08 2020 at 22:33):

Anyhow, in many cases the point of types is to rule out this sort of thing. You can add it back in, though. Types like that sometimes use a notation like $μ A. B^A$ for the fixed point of $B^-$.

fosco (Sep 08 2020 at 22:33):

aha! So I wasn't imagining the connection with Lawvere FPT (I remember some statements from that paper, if there's a remark on this very question, thanks double)

Dan Doel (Sep 08 2020 at 22:37):

Constructive mathematics can be even more subtle here, too. There are examples of fixed points $X \cong 2^{2^X}$. But that is anti-classical, and I think it is different than $X \cong 2^X$.

Dan Doel (Sep 08 2020 at 22:40):

But e.g. there are CCCs ancillary to domain theory that have examples of the latter, I believe.

fosco (Sep 08 2020 at 22:47):

I must admit I'm still a bit confused (mainly by the fact that I can't judge the correctness of my argument: what prevents me from typing Y? But in my timezone it's 2am, I think I'll call it a day :smile: )

Dan Doel (Sep 08 2020 at 22:52):

In systems where you can't, it's because there's no type $X = B^X$. And for $B$ in general, this is necessary to have models in $\mathsf{Set}$, say, because the only assignments that satisfy $X \cong B^X$ are $X = B = 1$.

Dan Doel (Sep 08 2020 at 22:54):

And this is the case for $\mathsf{Set}$ because for other choices of $B$ there are endomorphisms $B → B$ without fixed points.

Dan Doel (Sep 08 2020 at 23:00):

I think the 'obvious' connection is probably that Y is notation for the fixed point that exists in Lawvere's argument.

Dan Doel (Sep 08 2020 at 23:03):

Perhaps if you stare at his argument hard enough, he wrote Y in very cumbersome category notation. :)

Reid Barton (Sep 08 2020 at 23:09):

In the diagram near the end of your original posts, you have the variable in the wrong slot in $[B, -]$.

Reid Barton (Sep 08 2020 at 23:11):

Also, the colimit of the diagram categories isn't likely to be $\mathcal{C}$--this is the construction for inverting a functor

Reid Barton (Sep 08 2020 at 23:13):

If you write down the construction for an initial fixed point of a functor, which involves a colimit inside $\mathcal{C}$, then one problem will be that $[-, B]$ is contravariant, but a more serious issue is that it doesn't commute with colimits of any degree of filteredness, which is what you need to conclude that the construction produces a fixed point.

fosco (Sep 09 2020 at 08:25):

Both comments are quite explanatory, thank you. :smile: