Typechecking is undecidable when 'type' is a type (1989) [pdf]
zem · 82 points · 52 comments · 30 янв. · Open original
Comments
5 preview comments · loading full thread
Log in to use comments
Log in to h4cker, then connect Hacker News to publish comments.
PVpvillano2 февр.
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
ANAnimats1 февр.
This sounds close to Russell's "class of all classes" paradox. Is it?
JEjeberle2 февр.
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
https://www.youtube.com/watch?v=bE1bRbZzQ_k&t=48m27s
RArandomNumber71 февр.
And still this type system could be the base for a very interesting and powerfull programming language imo.
DAda_chicken2 февр.
This seems strange to me, but it's hours past my bed time and I haven't tried reading lambda calculus or lambda-star calculus theory in about 20 years.
Many programming languages have a variant or object type. In C#, any instance of a class will also say that it is of type System.Object. That does nearly make that a type of all types.
There is some nuance and special cases. Like any null is considered a null instance of any nullable object, but you're also not permitted to ask a null value what type it is. It just is a null. Similarly, C# does differentiate between a class and an instance of a class. Both a class and an instance are of a given type, but a class is not an instance of a class.
Presumably the difference is either in one of those nuances, or else in some other axiomatic assertion in the language design that this paper is not making.
Or else I'm very much missing what the author is driving at, which at this time of the morning seems equally possible.
Comments
5 preview comments · loading full threadLog in to h4cker, then connect Hacker News to publish comments.
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
This sounds close to Russell's "class of all classes" paradox. Is it?
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 https://www.youtube.com/watch?v=bE1bRbZzQ_k&t=48m27s
And still this type system could be the base for a very interesting and powerfull programming language imo.
This seems strange to me, but it's hours past my bed time and I haven't tried reading lambda calculus or lambda-star calculus theory in about 20 years. Many programming languages have a variant or object type. In C#, any instance of a class will also say that it is of type System.Object. That does nearly make that a type of all types. There is some nuance and special cases. Like any null is considered a null instance of any nullable object, but you're also not permitted to ask a null value what type it is. It just is a null. Similarly, C# does differentiate between a class and an instance of a class. Both a class and an instance are of a given type, but a class is not an instance of a class. Presumably the difference is either in one of those nuances, or else in some other axiomatic assertion in the language design that this paper is not making. Or else I'm very much missing what the author is driving at, which at this time of the morning seems equally possible.