4 ms·

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

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.

pizza 3y ago
> 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/1674357272498110467 https://twitter.com/BartoszMilewski/status/16743572724981104...
- climatologist 3y ago
  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.
  - klysm 3y ago
    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.
  - js8 3y ago
    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.
  - bmacho 3y ago
    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.
- louthy 3y ago
  Better thread on Mastodon [1] [1] https://mathstodon.xyz/@johncarlosbaez/110631013611448277 https://mathstodon.xyz/@johncarlosbaez/110631013611448277
- klysm 3y ago
  Interesting definition of most structure
- kmill 3y ago
  "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.
kccqzy 3y ago
> 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.
- dkbrk 3y ago
  > 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/ https://plato.stanford.edu/entries/nonwellfounded-set-theory... [1]: https://en.wikipedia.org/wiki/Aczel%27s_anti-foundation_axiom https://en.wikipedia.org/wiki/Aczel%27s_anti-foundation_axio...
  - daxfohl 3y ago
    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?
    - climatologist 3y ago
      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.
nine_k 3y ago
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.
- daxfohl 3y ago
  I thought the principle of the excluded middle was the ultimate source of that paradox, not set theory itself?
  - bmacho 3y ago
    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.)
  - nine_k 3y ago
    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.
- eric-hu 3y ago
  That would be Russell’s paradox https://en.m.wikipedia.org/wiki/Russell%27s_paradox https://en.m.wikipedia.org/wiki/Russell%27s_paradox
ughitsaaron 3y ago
Sorry, but could anyone share some background (reading, links, etc.) on set vs. category theory as applied type systems?
- daxfohl 3y ago
  Mostly about proof assistants, but type systems are fundamentally related https://mathoverflow.net/questions/376839/what-makes-dependent-type-theory-more-suitable-than-set-theory-for-proof-assista https://mathoverflow.net/questions/376839/what-makes-depende...
weatherlight 3y ago
https://www.irif.fr/~gc/papers/set-theoretic-types-2022.pdf 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.

pizza 3y ago

> 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/1674357272498110467 https://twitter.com/BartoszMilewski/status/16743572724981104...

climatologist 3y ago
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.
- klysm 3y ago
  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.
- js8 3y ago
  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.
- bmacho 3y ago
  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.
louthy 3y ago
Better thread on Mastodon [1] [1] https://mathstodon.xyz/@johncarlosbaez/110631013611448277 https://mathstodon.xyz/@johncarlosbaez/110631013611448277
klysm 3y ago
Interesting definition of most structure
kmill 3y ago
"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.

kccqzy 3y ago

> 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.

dkbrk 3y ago
> 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/ https://plato.stanford.edu/entries/nonwellfounded-set-theory... [1]: https://en.wikipedia.org/wiki/Aczel%27s_anti-foundation_axiom https://en.wikipedia.org/wiki/Aczel%27s_anti-foundation_axio...
- daxfohl 3y ago
  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?
  - climatologist 3y ago
    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.

nine_k 3y ago

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.

daxfohl 3y ago
I thought the principle of the excluded middle was the ultimate source of that paradox, not set theory itself?
- bmacho 3y ago
  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.)
- nine_k 3y ago
  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.
eric-hu 3y ago
That would be Russell’s paradox https://en.m.wikipedia.org/wiki/Russell%27s_paradox https://en.m.wikipedia.org/wiki/Russell%27s_paradox

ughitsaaron 3y ago

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

daxfohl 3y ago
Mostly about proof assistants, but type systems are fundamentally related https://mathoverflow.net/questions/376839/what-makes-dependent-type-theory-more-suitable-than-set-theory-for-proof-assista https://mathoverflow.net/questions/376839/what-makes-depende...

weatherlight 3y ago

https://www.irif.fr/~gc/papers/set-theoretic-types-2022.pdf 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.