It feels like this is unsurprising, given we already have Goedel's theorems and halting theorems. Any system of self-describing complexity ends up in this territory.
This sounds close to Russell's "class of all classes" paradox. Is it?
Yes the type theoretic analog to Russel's (set theoretic) paradox is Girard's (as mentioned in the abstract) paradox.
This is incorrect. The set paradox it’s analogous to is the inability to make the set of all ordinals. Russel’s paradox is the inability to make the set of all sets.
Since we're being pedantic, Russel's paradox involves the set of all sets that don't contain themselves.
Technically speaking, because it's not a set, we should say it involves the collection of all sets that don't contain themselves. But then, who's asking...
I'm asking. What prevents that collection from being a set?
This is the easiest of the paradoxes mentioned in this thread to explain. I want to emphasize that this proof uses the technique of "Assume P, derive contradiction, therefore not P". This kind of proof relies on knowing what the running assumptions are at the time that the contradiction is derived, so I'm going to try to make that explicit.
Here's our first assumption: suppose that there's a set X with the property that for any set Y, Y is a member of X if and only if Y doesn't contain itself as a member. In other words, suppose that the collection of sets that don't contain themselves is a set and call it X.
Here's another assumption: Suppose X contains itself. Then by the premise, X doesn't contain itself, which is contradictory. Since the innermost assumption is that X contains itself, this proves that X doesn't contain itself (under the other assumption).
But if X doesn't contain itself, then by the premise again, X is in X, which is again contradictory. Now the only remaining assumption is that X exists, and so this proves that there cannot be a set with the stated property. In other words, the collection of all sets that don't contain themselves is not a set.
Not getting it. Why would you want to do this? And why is no distinction made between `typeof(type)` and `type`? And doesn't the entire problem go away if you distinguish between `typeof(type)`, which is a value whose type is `type`?
Type systems aren't magic. They do stop all incorrect programs from running, but also the majority of correct programs too.
... for some spectactularly inconsistent and arbitrary definition of "correct program".
Luckily most everyday programs are typeable.
And still this type system could be the base for a very interesting and powerfull programming language imo.
Yeah we don't throw programming languages away because they are undecidable.
So why would we throw type systems away if they are undecidable?
Decidability isn't even that useful. If typechecking takes a million years, that's also bad. What you want is guarantees that correct programs typecheck quickly. Without this, you end up in swift land, where you can write correct code that can't be typechecked quickly and the compiler has to choose between being slow or rejecting your code
> What you want is guarantees that correct programs typecheck quickly.
In practice there's wealth of lemmas provided to you within the inference environment in a way standard library functions are provided in conventional languages. Those act like a memoization cache for the purpose of proving your program's propositions. A compiler can also offer a flag to either proceed with ("trust me, it will infer in time") or reject the immediately undecidable stuff.
Presumably with the rather unpleasant side-effect of compiles that may never finish. :-P
This really isn't a big deal as it resolved via type universes.
Similar to the difficulty in finding Title Search companies on Indeed.
Hum... I'm getting 403, forbiden. Is it down?
Working for me, but very very slow to load (which I assume is most of the way to 403).
It feels like this is unsurprising, given we already have Goedel's theorems and halting theorems. Any system of self-describing complexity ends up in this territory.
This sounds close to Russell's "class of all classes" paradox. Is it?
Yes the type theoretic analog to Russel's (set theoretic) paradox is Girard's (as mentioned in the abstract) paradox.
This is incorrect. The set paradox it’s analogous to is the inability to make the set of all ordinals. Russel’s paradox is the inability to make the set of all sets.
Since we're being pedantic, Russel's paradox involves the set of all sets that don't contain themselves.
Technically speaking, because it's not a set, we should say it involves the collection of all sets that don't contain themselves. But then, who's asking...
I'm asking. What prevents that collection from being a set?
This is the easiest of the paradoxes mentioned in this thread to explain. I want to emphasize that this proof uses the technique of "Assume P, derive contradiction, therefore not P". This kind of proof relies on knowing what the running assumptions are at the time that the contradiction is derived, so I'm going to try to make that explicit.
Here's our first assumption: suppose that there's a set X with the property that for any set Y, Y is a member of X if and only if Y doesn't contain itself as a member. In other words, suppose that the collection of sets that don't contain themselves is a set and call it X.
Here's another assumption: Suppose X contains itself. Then by the premise, X doesn't contain itself, which is contradictory. Since the innermost assumption is that X contains itself, this proves that X doesn't contain itself (under the other assumption).
But if X doesn't contain itself, then by the premise again, X is in X, which is again contradictory. Now the only remaining assumption is that X exists, and so this proves that there cannot be a set with the stated property. In other words, the collection of all sets that don't contain themselves is not a set.
Not getting it. Why would you want to do this? And why is no distinction made between `typeof(type)` and `type`? And doesn't the entire problem go away if you distinguish between `typeof(type)`, which is a value whose type is `type`?
Type systems aren't magic. They do stop all incorrect programs from running, but also the majority of correct programs too.
... for some spectactularly inconsistent and arbitrary definition of "correct program".
Luckily most everyday programs are typeable.
And still this type system could be the base for a very interesting and powerfull programming language imo.
Yeah we don't throw programming languages away because they are undecidable.
So why would we throw type systems away if they are undecidable?
Decidability isn't even that useful. If typechecking takes a million years, that's also bad. What you want is guarantees that correct programs typecheck quickly. Without this, you end up in swift land, where you can write correct code that can't be typechecked quickly and the compiler has to choose between being slow or rejecting your code
> What you want is guarantees that correct programs typecheck quickly.
In practice there's wealth of lemmas provided to you within the inference environment in a way standard library functions are provided in conventional languages. Those act like a memoization cache for the purpose of proving your program's propositions. A compiler can also offer a flag to either proceed with ("trust me, it will infer in time") or reject the immediately undecidable stuff.
Presumably with the rather unpleasant side-effect of compiles that may never finish. :-P
This really isn't a big deal as it resolved via type universes.
Similar to the difficulty in finding Title Search companies on Indeed.
Hum... I'm getting 403, forbiden. Is it down?
Working for me, but very very slow to load (which I assume is most of the way to 403).
still working for me