Hacker News Reader

Comment by daxfohl | Hacker News Reader

Is set theory more useful than category theory for dynamic types? Seems like set theory is less constrained, like a set can be part of itself by nature, whereas category theory generally doesn't allow mixing containers and elements like that out of the box IIUC. Seems like category theory best suits Haskell and such where types are more precisely defined (something that could be an int or a bool needs an ADT wrapper), whereas set theory might make sense for completely dynamic types, where something could be an int or a bool or whatever else by nature.

But I'm entirely unsure. Maybe it is completely unrelated to why set theory is used as a basis here. Just wondering.

View on HN

https://www.irif.fr/~gc/papers/set-theoretic-types-2022.pdf

This research paper by Giuseppe Castagna presents an in-depth exploration of programming with set-theoretic types, which include union, intersection, and negation type connectives. The author argues that these types are not just useful, but necessary for typing some common programming patterns, and they play a crucial role in precisely typing various language constructs, from branching and pattern matching to function overloading and type-cases.

What sets this work apart is the extension of the theory of types known as semantic subtyping to include polymorphic types. This is a significant step forward as it allows for a more expressive and precise type system. The paper also discusses the design of languages that use these types and presents a theoretical framework that covers all the examples given in the presentation.

one of the key takeaways from this paper is that current programming languages are unable to infer intersection types for functions without explicit annotations. This is a limitation that could impact the development and efficiency of certain programs. The author presents three effective restrictions of this system, each with its own trade-offs, which could potentially guide the design of future programming languages.

The paper concludes with an overview of other aspects of these languages, such as pattern matching, gradual typing, and denotational semantics. These insights could have far-reaching implications for the development of more expressive and precise programming languages.

this paper pushes the boundaries of what we understand about type systems in programming languages, Elixir is going to be the first general purpose language to implement such a type system.

A set being a member if itself (or not) is the source of the famous paradox that destroyed the naive set theory %)

In practice, you usually need either a definite sum.type (int | str | null), or the all-encompassing type, like Any. I think both cases should be adequately representable in a categorial language — am I wrong?

You may need to represent a sum type that includes Any (or a similar type) if you.allow type-based signature overloads for functions. I wonder if this may represent any obstacle to a caregorial approach.

I thought the principle of the excluded middle was the ultimate source of that paradox, not set theory itself?

No, Russel's paradox and the Law of the Excluded Middle have not much to do with each other. (It is not easy to prove such a negative statement, but I googled them together, and found absolutely nothing.)

Both the Russell's paradox and the Curry's paradox (yes, by Haskell Curry) are built on referencing a rule from itself, on breaking the contextual nesting. In a sense, it's like using `goto` to jump inside a loop, thus breaking the loop invariant.

Practically all other paradoxes can be reduced to one of these two.

That would be Russell’s paradox

https://en.m.wikipedia.org/wiki/Russell%27s_paradox

> A set has the least structure. It's a discrete category, with no morphisms other than identities. Conversely, the category of sets has the most structure, since its morphisms don't have to preserve any structure.

https://twitter.com/BartoszMilewski/status/16743572724981104...

This is incorrect. The number of morphisms is not what makes mathematical objects more or less structured. What is correct is that the category of sets does not have constraints for morphisms between its objects. Bartosz is equating morphisms and "structure" which is not how most mathematicians think of what it means for a category or an object to be structured.

It seems incorrect to state that his perspective is categorically incorrect. The term “structure” lacks a precise definition and his interpretation isn’t completely invalid.

He prefaces the statement with "my intuition tells me", so perhaps he is much less categorical (pun intended) about the claim than you interpret it.

It is correct, in the best possible way.

Having least structure is a soft/aesthetical statement, and the explanation is right after it (a correct definition).

I wish all the math looked like this, first a soft/aesthetical statement, then right after the correct math.

Better thread on Mastodon [1]

[1] https://mathstodon.xyz/@johncarlosbaez/110631013611448277

Interesting definition of most structure

"Set-theoretic type theory" is working with the lattice of all subsets of possible values, where a "type" is one of these subsets. This lattice has plenty of structure, but sure individual subsets do not.

The category of sets is different from this lattice, since it allows arbitrary functions between sets for its morphisms rather than just inclusions.

"Set-theoretic types" have a meaningful notion of overlap. Usually types in other type system tend to be practically disjoint, like objects in a concrete category might be sets but the category itself doesn't give language to check whether the objects are disjoint sets.

> a set can be part of itself

A set cannot be part of itself in an axiomatic formulation of set theory. Naïve set theory, one that allows an unrestricted general comprehension, has been thoroughly rejected.

> A set cannot be part of itself in an axiomatic formulation of set theory.

This isn't quite true. In practice, you're correct: "set theory", generally referring to ZF (or some closely related derivative thereof) with the Von Neumann Universe, doesn't allow sets to contain themselves. But it is possible to axiomatize set theory where sets can contain themselves [0].

This replaces the axiom of foundation with the axiom of anti-foundation [1], so it's not naive set theory but it is an axiomatized non-well-founded set theory.

[0]: https://plato.stanford.edu/entries/nonwellfounded-set-theory...

[1]: https://en.wikipedia.org/wiki/Aczel%27s_anti-foundation_axio...

My understanding was that you just had to get rid of the law of the excluded middle. Then things like Russell's Paradox can be stated, but evaluate to neither true nor false, and be fine. Is that not correct?

It's more to do with unrestricted circular self-reference than excluded middle but what you're saying makes sense. Without excluded middle there is no contradiction. There is something called Curry's paradox which is similar. Excluded middle is not involved in Curry's paradox but circular self-refernece is still the culprit for the paradoxical conclusion.

Sorry, but could anyone share some background (reading, links, etc.) on set vs. category theory as applied type systems?

Mostly about proof assistants, but type systems are fundamentally related https://mathoverflow.net/questions/376839/what-makes-depende...

Reply on news.ycombinator.com