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 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.
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...
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. The compiler can also offer a flag to either proceed with ("trust me, it will infer in time") or reject the immediately undecidable stuff.
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.
Type systems aren't magic. They do stop all incorrect programs from running, but also the majority of correct programs too.
Luckily most everyday programs are typeable.
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...
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. The compiler can also offer a flag to either proceed with ("trust me, it will infer in time") or reject the immediately undecidable stuff.
Similar to the difficulty in finding Title Search companies on Indeed.
Hum... I'm getting 403, forbiden. Is it down?
still working for me