alt Hacker NewsTypechecking is undecidable when 'type' is a type (1989) [pdf]
Comments
Does Rice's theorem cover this?
> [ all non-trivial semantic properties of programs are undecidable ]
https://en.wikipedia.org/wiki/Rice's_theorem
Found here:
From Sumatra to Panama, from Babylon to Valhalla
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?
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.
And still this type system could be the base for a very interesting and powerfull programming language imo.
Similar to the difficulty in finding Title Search companies on Indeed.
[dead]
This stack exchange answer talks about the importance of decidability in type checking
https://langdev.stackexchange.com/a/2072
My interpretation
Decidability is of academic interest, and might be a hint if something is feasible.
But there are (1) ways of sidestepping undecidability, e.g. A valid C++/Rust program is one for which the typechecker terminates in x steps without overflowing the stack
And (2) things which are decidable, but physically impossible to calculate, e.g the last digit of the 10^10^10 th prime
What matters is being able to reject all incorrect programs, and accept most human written valid programs