5 ms·

You wrote "in theory, there is a type system that describes every system": I would be very surprised if this is true. It would a major turnaround in modern math

by ngrilly 12y ago

You wrote "in theory, there is a type system that describes every system": I would be very surprised if this is true. It would a major turnaround in modern mathematics. What is this theory? Any link?

gizmo686 12y ago
The fact that there exists such a type system, does not mean that we have constructed it. Having said that, the theoretical existence of such a theory seems highly plausible, but without a proof, it would not surprise me to learn that such is impossible. Without a constructivist proof, it would not suprise me to learn that the existence of such a system is irrelevent (to applied computer science).
steveklabnik 12y ago
As I mentioned with my caveat, I'm an amateur type theorist, so I'm still digging into a lot of things. Do you have some relevant literature for me about this being impossible? My claim may have been too strong: I meant more that "it hasn't been disproven that type systems are inherently disjoint." Similar to how physicists believe there's a Grand Unified Theory of physics, but that doesn't mean we actually know it yet.
- poof131 12y ago
  Not entirely sure, but it seems if you had a type system that describes every system you may be on your way to disproving the first incompleteness theorem. http://en.wikipedia.org/wiki/G%C3%B6del's_incompleteness_theorems http://en.wikipedia.org/wiki/G%C3%B6del's_incompleteness_the...
  - steveklabnik 12y ago
    Hmmmmmm yes. I can see that. This is why I need to move from 'amateur type theorist' to 'intermediate type theorist.' :)
  - dllthomas 12y ago
    That certainly tells us that there is no single type system that can describe every correct program, which seems to be the stronger version of Steve's thesis that he was supporting in the immediate parent. A weaker version of his thesis, which could still support his original phrasing in the GGP, would be "for any correct program, there exists a type system in which it can be typed [though we might not be able to find it]." That doesn't seem to be ruled out, and sounds plausible, though I don't know of any specific results on it.

by ngrilly 12y ago

You wrote "in theory, there is a type system that describes every system": I would be very surprised if this is true. It would a major turnaround in modern mathematics. What is this theory? Any link?

gizmo686 12y ago

The fact that there exists such a type system, does not mean that we have constructed it. Having said that, the theoretical existence of such a theory seems highly plausible, but without a proof, it would not surprise me to learn that such is impossible. Without a constructivist proof, it would not suprise me to learn that the existence of such a system is irrelevent (to applied computer science).

steveklabnik 12y ago

As I mentioned with my caveat, I'm an amateur type theorist, so I'm still digging into a lot of things. Do you have some relevant literature for me about this being impossible? My claim may have been too strong: I meant more that "it hasn't been disproven that type systems are inherently disjoint." Similar to how physicists believe there's a Grand Unified Theory of physics, but that doesn't mean we actually know it yet.

poof131 12y ago
Not entirely sure, but it seems if you had a type system that describes every system you may be on your way to disproving the first incompleteness theorem. http://en.wikipedia.org/wiki/G%C3%B6del's_incompleteness_theorems http://en.wikipedia.org/wiki/G%C3%B6del's_incompleteness_the...
- steveklabnik 12y ago
  Hmmmmmm yes. I can see that. This is why I need to move from 'amateur type theorist' to 'intermediate type theorist.' :)
- dllthomas 12y ago
  That certainly tells us that there is no single type system that can describe every correct program, which seems to be the stronger version of Steve's thesis that he was supporting in the immediate parent. A weaker version of his thesis, which could still support his original phrasing in the GGP, would be "for any correct program, there exists a type system in which it can be typed [though we might not be able to find it]." That doesn't seem to be ruled out, and sounds plausible, though I don't know of any specific results on it.