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.
ww (Feb 03 2026 at 08:58):From a sociologist friend:
This is Ontological Gerrymandering. By using "typed systems" the developers have built a world where only certain types of data are allowed to exist. The social scientist would investigate what is excluded by these rigid technical pipes.
Morgan Rogers (he/him) (Feb 03 2026 at 09:35):An interesting idea, and I appreciate the post-modernist inspiration; it reminds me of the notion of "organisational knowledge/ignorance", which I learned about from PhilosophyTube. It's curious that they use "ontological" rather than "epistemological". Types don't control what data is allowed to exist, only what data a system is able to talk about.
However, I feel that this idea exaggerates the rigidity of typed systems. It's true that types impose fundamental limits in the above sense, and sometimes these limits are an advantage because they enable more powerful results that would not be true of a more expressive system, but for typed systems used in practice any form of data that is excluded or can only be included through a complex encoding that is difficult to reason about within the system is a problem usually addressed by expanding the type system.
The meta version of this question is more substantial: which type constructors are considered admissible or important, either in the abstract or in a given programming language paradigm? How might your friend name that kind of restriction?
Amar Hadzihasanovic (Feb 03 2026 at 13:16):Certainly typing is more akin to the existence of electoral districts themselves, as opposed to allowing everyone to vote in any election and hoping that a person in rural Ohio will simply not bother voting in a local election in Los Angeles. Gerrymandering would be more like the definition of "unnatural" types designed to exclude undesirable values, which certainly is already considered bad practice.
fosco (Feb 03 2026 at 14:18):I say this in the most peaceful tone: what the hell are you talking about?
fosco (Feb 03 2026 at 14:19):I really don't understand what's going on in this thread, is it me?
fosco (Feb 03 2026 at 14:20):is this how a non mathematician feels like when we discuss and we mumble "ah, yeah, of course, it's a filtered colimit, yes yes"?
Vincent R.B. Blazy (Feb 03 2026 at 14:45):fosco said:
is this how a non mathematician feels like when we discuss and we mumble "ah, yeah, of course, it's a filtered colimit, yes yes"?
Yes it might be :stuck_out_tongue: What don’t you get: philosophy, or electoral stuff?
Vincent R.B. Blazy (Feb 03 2026 at 14:47):Amar Hadzihasanovic said:
Certainly typing is more akin to the existence of electoral districts themselves, as opposed to allowing everyone to vote in any election and hoping that a person in rural Ohio will simply not bother voting in a local election in Los Angeles. Gerrymandering would be more like the definition of "unnatural" types designed to exclude undesirable values, which certainly is already considered bad practice.
Indeed, typing is rather the design of the districts, would it be fair, or the worst gerrymandering. Now… Would there be a relevant analogy with voting systems without districts, like proportional representation? :face_with_monocle:
Alex Kreitzberg (Feb 03 2026 at 14:48):It reads to me like the quoted friend is making a metaphor to convey they believe type systems inhibit perfectly good data, just like Gerrymandering inhibits perfectly good voters. Which, to them, implies you should look at what data is excluded to get a complete picture.
This comparison feels forced, that's why folks are spending energy fixing the metaphor
ww (Feb 03 2026 at 15:03):I think it was brought about by an amusing misunderstanding.
ww (Feb 03 2026 at 15:03):But it's an interesting turn of phrase :)
Nathaniel Virgo (Feb 03 2026 at 15:05):I dunno, it kind of makes sense to me. I've spent most of my career thinking about living organisms, but I've no idea what a living organism is, mathematically. I wish I did. But I don't think there's any typed system where living organisms are a term. So maybe they are excluded by ontological gerrymandering. [tone: mostly joking around, but also slightly hoping someone makes sense of this and says something insightful]
Chad Nester (Feb 03 2026 at 15:08):I think it's an interesting way to misunderstand the nature of "data types" in, at least, computer science.
It's true that raw, unstructured information is in some sense more basic than its "typed" counterpart, but I don't think types are actually about filtering this raw information according to some scheme. They are much more about interpreting it according to some scheme. A crucial point is that a given piece of raw, unstructured information can be interpreted in may ways, and so can "have many types".
Alex Kreitzberg (Feb 03 2026 at 15:12):To be clear I think it's worth thinking about whether typing omits interesting systems.
But if someone gave me this metaphor I'd want them to clarify how they were trying to use it.
Matteo Capucci (he/him) (Feb 04 2026 at 11:10):Gerrymandering does not prevent things to exist though, it forces a result by contorting data flow (if you really want to sound like a tech bro). It's a form of statistical torture, if anything. I don't quite see the connection... :thinking: