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: theory: category theory

Topic: Set^Set and lamba calculus

Stelios Tsampas (Apr 02 2020 at 15:12):

It's been quite a few months that I've been having this idea popping up in my head at random: The functor category $Set^{Set}$ being conceptually very close to some sort of polymorphic $\lambda$-calculus, in that polymorphic (well-behaved) $\lambda$-terms are morphisms and parametric types are objects. Non-parametric stuff are just plain-old terms between "const" functors.

This has the advantage that polymorphic terms are now "internalized" (I'm hoping I'm using the word properly) as morphisms. Thoughts?

Dan Doel (Apr 02 2020 at 15:31):

It's similar to schematic types from e.g. Hindley-Milner. But I think there are some issues. One is that there's only one variable, and it's covariant only. Also, that category might not be (Cartesian) closed, due to size issues (not sure).

Stelios Tsampas (Apr 02 2020 at 15:34):

Yeah, I was thinking about Hindley-Milner as well. As for the CCC structure, according to this entry in nlab, sec. 3, 1st subsec., 2nd paragraph, it is indeed a CCC.

Dan Doel (Apr 02 2020 at 15:36):

$Set$ isn't small.

Stelios Tsampas (Apr 02 2020 at 15:37):

Is that a hard no? Is it not possible to restrict to small sets?

Stelios Tsampas (Apr 02 2020 at 15:37):

Ah, look at "Size" section in the previous nlab link, this can be easily done.

Stelios Tsampas (Apr 02 2020 at 15:39):

Sorry, for the post right above I meant this link.

Dan Doel (Apr 02 2020 at 15:39):

Restrict what? The category of small sets isn't small itself.

Stelios Tsampas (Apr 02 2020 at 15:40):

Hmmmmm :/.

Dan Doel (Apr 02 2020 at 15:42):

You could have $SET^{Set}$ where the capital one is the category of large sets, and non-capital one is itself large, but then it's not exactly the same situation.

Stelios Tsampas (Apr 02 2020 at 15:45):

Whatever works really. I struggle to figure out where things might go wrong. Which brings my to why I have an interest in this. I dabble in Turi's mathematical operational semantics, where semantics are represented by distributive laws of various complexity.

Stelios Tsampas (Apr 02 2020 at 15:46):

If said distributive laws (or semantics) correspond to $\lambda$-terms themselves (as they are morhpisms in the functor category we are working in), or any terms of the model of computation of choice, maybe there's some room for experimentation.

Stelios Tsampas (Apr 02 2020 at 15:49):

Like, in the spirit of classic fixpoint results, attempt to (show that it is not possible to) make a distributive law that is "equivalent" to the computational model one is working in. That would be fun.

Morgan Rogers (he/him) (Apr 02 2020 at 15:54):

Stelios Tsampas said:

Ah, look at "Size" section in the previous nlab link, this can be easily done.

The problem that one encounters when doing category theory formally is that one wants to work with precisely-defined categories, and that means dealing with size issues. In this instance the problem is that while we can choose a category (or "universe") of sets to be closed under typical operations like products, powersets/exponentials, subsets... when we try to build a category like $Set^{Set}$, we would like to argue that these operations are still possible in a point-wise way, but what we find is that even if we know how to "construct" them, the resulting functors may be "too big", in that they no longer take values in our original universe.

Cody Roux (Apr 02 2020 at 15:55):

Yea $Set^{Set}$ is definitely not a CCC.

Morgan Rogers (he/him) (Apr 02 2020 at 15:56):

In this case a solution might be to work in $Set^{FinSet}$ until you desperately need to have uncountably many objects to work with :wink:

Stelios Tsampas (Apr 02 2020 at 15:56):

An important lesson learned :).

Cody Roux (Apr 02 2020 at 15:56):

But I like my identity function to be polymorphic...

Cody Roux (Apr 02 2020 at 15:57):

I think there are pretty strong constraints about what things can be models of System F. In particular, a boolean topos cannot fit the bill...

Stelios Tsampas (Apr 02 2020 at 15:57):

Morgan Rogers said:

In this case a solution might be to work in $Set^{FinSet}$ until you desperately need to have uncountably many objects to work with :wink:

Thank you for the idea. Maybe there's another (full) subcategory that's CCC?

Stelios Tsampas (Apr 02 2020 at 15:58):

It doesn't have to be System F by the way. But it looked like some flavor of polymorphic lambda calculus.

Morgan Rogers (he/him) (Apr 02 2020 at 16:02):

Cody Roux said:

I think there are pretty strong constraints about what things can be models of System F. In particular, a boolean topos cannot fit the bill...

@Stelios Tsampas you should look into whether/why this^ is the case, since it likely precludes many otherwise plausible categories, given that the Yoneda embedding preserves any limits and exponentials that exist. Even if you don't need it to be System F, it might be enlightening to see what goes wrong, and you'll learn some topos theory along the way :heart_eyes: Do you have references, @Cody Roux?

Stelios Tsampas (Apr 02 2020 at 16:05):

@Morgan Rogers What?! You mean to tell me that there isn't a quick and dirty way to git things done? That I can't just cut the Gordian knot??

Just kidding, foundational stuff usually deserve doing them the hard way. This should be worthwhile.

Dan Doel (Apr 02 2020 at 16:16):

For System F, the classic is "Polymorphism Is Not Set Theoretic". That it can be done in a non-boolean topos, there's "Polymorphism is Set Theoretic, Constructively". However, System F may not be relevant, because the question was about schematic types a la Hindley-Milner, which can be predicative, and (the sort of) impredicativity of System F is the real issue.

Stelios Tsampas (Apr 02 2020 at 16:22):

Yes, that makes perfect sense.

Stelios Tsampas (Apr 02 2020 at 16:27):

So maybe I could take a look in the paper you mention and make sure I stay within the boundaries of Set Theory when dealing with polymorphism. And then figure out the best fit for the functor category I'm looking for.

John Baez (Apr 02 2020 at 17:22):

Morgan Rogers said:

In this case a solution might be to work in $\mathsf{Set}^{\mathsf{FinSet}}$ until you desperately need to have uncountably many objects to work with :wink:

Note that $\mathsf{FinSet}$ is a large category. But it's essentially small - equivalent to a small one - so you can replace it with a equivalent small category before taking presheaves on it.

You could do the same replacing finite sets by sets with cardinality bounded by whatever you want. All these give essentially small categories. So, take an inaccessible cardinal...

Stelios Tsampas (Apr 02 2020 at 17:32):

So a large category being equivalent to a small one :thinking:. This sounds crazy, and evil. Or is it I that's evil?

Dan Doel (Apr 02 2020 at 17:32):

But don't you run into equivalent problems if you just do the original thing? Like $κ-Set^{κ-Set}$ is probably not a CCC because it's not κ-complete?

Dan Doel (Apr 02 2020 at 17:33):

The problem with $Set^{FinSet}$ is that it doesn't function in the way the original question was posed, because it is type schemas whose variables are finite types, not arbitrary types.

Reid Barton (Apr 02 2020 at 17:35):

For strong limit cardinals $\kappa$ (those for which $\lambda < \kappa \implies 2^\lambda < \kappa$) it might be okay?

Stelios Tsampas (Apr 02 2020 at 17:36):

I think @John Baez implies that one cat take the category of sets bounded by something like $ℵ_{0}$, not necessarily finite.

Reid Barton (Apr 02 2020 at 17:39):

Oh never mind, the problem is again $\kappa-Set$ itself is not $\kappa$-small

Dan Doel (Apr 02 2020 at 17:39):

Oh right. It probably would be κ-complete.

John Baez (Apr 02 2020 at 17:40):

It's not crazy at all. Every small category is equivalent to a large one: just throw in a proper class of objects isomorphic to objects you already have. (You have to do this correctly to maintain equivalence.) So when someone hands you a large category you should query whether it's equivalent to a small one. The easiest way is to find a skeleton and see if that's small.

John Baez (Apr 02 2020 at 17:47):

Dan Doel said:

But don't you run into equivalent problems if you just do the original thing? Like $κ-Set^{κ-Set}$ is probably not a CCC because it's not κ-complete?

First of all, there's no requirement that a cartesian closed category have any limits other than finite products.

Second, I'm not sure what you mean by $\kappa-\mathsf{Set}$ - the category of sets of cardinality $\lt \kappa$, or some equivalent small category. I prefer working with $\mathsf{Set}^\mathsf{C}$ when the category $\mathsf{C}$ is small, because then a bunch more theorems apply. For example: whenever $\mathsf{C}$ is small, $\mathsf{Set}^{\mathsf{C}}$ is complete and cocomplete. That is, it has all small limits and colimits.

So, if $\kappa-\mathsf{Set}$ means some small category equivalent to the category of sets of cardinality $\lt \kappa$ (or maybe $\le \kappa$) then $\mathsf{Set}^{\kappa-\mathsf{Set}}$ is complete and cocomplete. And yes, it's a cartesian closed category.

Stelios Tsampas (Apr 02 2020 at 17:47):

John Baez said:

It's not crazy at all. Every small category is equivalent to a large one: just throw in a proper class of objects isomorphic to objects you already have. (You have to do this correctly to maintain equivalence.) So when someone hands you a large category you should query whether it's equivalent to a small one. The easiest way is to find a skeleton and see if that's small.

I see! Thank you, I hadn't thought of that :).

Dan Doel (Apr 02 2020 at 17:47):

It's possible that the suggestion of $\mathsf{Set}^{\mathsf{FinSet}}$ was for something else, because it is like extending sets with variables. But it's not obvious to me how that would help.

Nathanael Arkor (Apr 02 2020 at 17:50):

@Stelios Tsampas: you might be interested in Fiore–Hamana's Multiversal Polymorphic Algebraic Theories (https://www.cl.cam.ac.uk/~mpf23/papers/Algebra/mpat.pdf), which describes a framework for polymorphic type theories (including System F) using presheaf categories

Dan Doel (Apr 02 2020 at 17:54):

@John Baez $\mathsf{Set}^{κ-\mathsf{Set}}$ is not like 'types schemas in variables that range over all types', assuming that the 'types' are sets (which is why the base is $\mathsf{Set}$). It has just expanded what the variables range over to κ-sized sets, but that is still the same restriction as using $\mathsf{FinSet}$. I would presume we are looking for $C$ such that $C^C$ is Cartesian closed.

Dan Doel (Apr 02 2020 at 17:55):

$C$ is the types, and $C^C$ are the schemas in one variable.

John Baez (Apr 02 2020 at 17:58):

I don't know anything about "type schemas in variables that range over all types", so I'm not attempting to join this part of the conversation. I just know which categories are complete, cartesian closed, etc., so I was correcting some apparent mistakes I saw.

Dan Doel (Apr 02 2020 at 17:58):

The completeness criterion is that I'm assuming that the nlab's sufficient condition for $D^C$ to be a CCC generalizes to $D$ being $C$-complete.

sarahzrf (Apr 02 2020 at 18:20):

$D$ needs to be complete for things indexed by certain constructions related to $C$, but im not sure that $C$-completeness is sufficient

sarahzrf (Apr 02 2020 at 18:20):

at the very least, in a constructive setting i think it may not be—in a classical setting i don't know

sarahzrf (Apr 02 2020 at 18:21):

consider presheaves on some preordered set; the exponential is basically kripke semantics, so you're using Set's completeness over a down-set (er, maybe an up-set), not just the base category itself

sarahzrf (Apr 02 2020 at 18:23):

and constructively speaking, it's totally possible to have completeness for some shape but not for arbitrary subshapes or similar things—just consider that any category has all limits of shape 1, but few have all limits of every subsingleton shape!

sarahzrf (Apr 02 2020 at 18:24):

it's possible i'm missing something that resolves the issue, but in any case i think this shows that it's not cut-and-dry

Dan Doel (Apr 02 2020 at 18:31):

Yeah, you probably need small copowers as well or something.

Dan Doel (Apr 02 2020 at 18:32):

For the well-known construction.

Joe Moeller (Apr 03 2020 at 03:34):

John Baez said:

It's not crazy at all. Every small category is equivalent to a large one: just throw in a proper class of objects isomorphic to objects you already have. (You have to do this correctly to maintain equivalence.) So when someone hands you a large category you should query whether it's equivalent to a small one. The easiest way is to find a skeleton and see if that's small.

except for the empty category :smirk_cat:

John Baez (Apr 03 2020 at 03:44):

Wow, true. It's so damned small it's not equivalent to any large category!

Matteo Capucci (he/him) (Apr 03 2020 at 07:34):

The empty sets strikes again

Morgan Rogers (he/him) (Apr 03 2020 at 09:52):

Dan Doel said:

The problem with $Set^{FinSet}$ is that it doesn't function in the way the original question was posed, because it is type schemas whose variables are finite types, not arbitrary types.

If you're trying to tackle "arbitrary types" you'll never escape these size issues! Surely there must be some upper bound on the size of type constructions you reeeeally need?

Morgan Rogers (he/him) (Apr 03 2020 at 09:59):

Alternatively put, is there a reason why you need $C^C$ and can't use $D^C$ for some larger category $D$? The only one actually mentioned so far is "I want the identity to be in there", but there is a natural embedding of eg. FinSet into Set which tastes just like the identity. I remember reading some work a long time ago about Relative Pseudomonads (Highland et al, I believe) that was built to overcome size issues a lot like this (eg I want to think of the Yoneda embedding as a kind of monad but I can't because it makes things Big)

Paolo Capriotti (Apr 03 2020 at 11:15):

This is (I think) the original reference about relative 1-monads: https://arxiv.org/abs/1412.7148. This is the paper about relative pseudomonads: https://arxiv.org/abs/1612.03678.

Dan Doel (Apr 03 2020 at 14:58):

@Morgan Rogers Types can have infinite numbers of values in them, like the natural numbers. Type schemas look like a -> a (that's the one for the identity function), and a can be instantiated to any concrete type (or schema, if you're using it to produce another schema). My understanding is that the original question was about fixing a category $C$ that represents all the concrete types, and then representing these schemas as functors $C^C$. I'm not surprised that it doesn't work, because I was trying to explain ways why it wouldn't, initially.

Dan Doel (Apr 03 2020 at 15:00):

Or, I'm not surprised it doesn't work with $C = \mathsf{Set}$.

Dan Doel (Apr 03 2020 at 15:07):

Unless I'm not understanding the alternate suggestion, then $D^C$ is going to be a situation where 1) $C$ does not allow being schematic in all concrete types or 2) $D$ contains things that aren't concrete types, so it isn't a precise correspondence like the initial question wants.

Morgan Rogers (he/him) (Apr 03 2020 at 15:25):

From the preceding discussion, your option 2 sounds like a concession which might ultimately be necessary to avoid size issues if you want both your category of concrete types and your category of schemas to have moderately strong closure properties. :shrug:

Cody Roux (Apr 04 2020 at 01:59):

I actually studied Fiore and Hamana's work on algebras with binders a long time ago, and I'd be happy to see discussion on the subject. It's clear there is a stark distinction between viewing polymorphism as a function between universes and as a schema which involves syntax, which is what Dan is getting at. Obviously syntax allows for anything, including inconsistent theories, so one usually wants some semantics at some point, but it's interesting to start with the syntax.

Dan Doel (Apr 04 2020 at 02:25):

I can kind of understand the hope, because being a functor rather than a function requires you to be coherent in a way that might only allow things we'd understand as parametric. But there are at least technical issues.

Mike Stay (Apr 13 2020 at 22:23):

You could take the category CESet of computably enumerable sets and partial computable functions and do category theory internal to it. Then CESet is "internal to itself" [1] and CESet^CESet is countable, because only computable functors are allowed.

[1] That's a link to a page quoting a thread on the category theory mailing list; I can't find the thread online anywhere else.

Stelios Tsampas (Apr 15 2020 at 00:34):

Mike Stay said:

You could take the category CESet of computably enumerable sets and partial computable functions and do category theory internal to it. Then CESet is "internal to itself" [1] and CESet^CESet is countable, because only computable functors are allowed.

[1] That's a link to a page quoting a thread on the category theory mailing list; I can't find the thread online anywhere else.

That indeed sounds very, very promising. Thanks!