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.
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`?
It makes life much easier when you want to use fancier types. E.g. if you want to be able to have ListOfLength[4], it's much nicer to be able to use normal 4 which you can use normal arithmetic on (and therefore say that when you append ListOfLength[x] to ListOfLength[y] you get ListOfLength[x + y]), than to have to encode everything in types and make it some kind of ListOfLength[SpecialTypeLevel4] (and then when you append the two lists you get a ListOfLength[TypeLevelAdditionIsCommutative[TypeLevelAdd[x, y]]#Result] or something).
To make that work you have to be able to use values as type parameters, i.e. types, so you have to be able to have e.g. types of type int, as well as types of type type, and it all gets a lot simpler and easier to work with if you just say that types have type type.
> And why is no distinction made between `typeof(type)` and `type`?
Well that's the whole point, to say that type is of type type.
> And doesn't the entire problem go away if you distinguish between `typeof(type)`, which is a value whose type is `type`?
No, because why would you ever use it as a value? The whole point of typeof is that it gives you a type that you can use as a type.
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 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.
14 comments
[ 0.20 ms ] story [ 41.4 ms ] threadIt makes life much easier when you want to use fancier types. E.g. if you want to be able to have ListOfLength[4], it's much nicer to be able to use normal 4 which you can use normal arithmetic on (and therefore say that when you append ListOfLength[x] to ListOfLength[y] you get ListOfLength[x + y]), than to have to encode everything in types and make it some kind of ListOfLength[SpecialTypeLevel4] (and then when you append the two lists you get a ListOfLength[TypeLevelAdditionIsCommutative[TypeLevelAdd[x, y]]#Result] or something).
To make that work you have to be able to use values as type parameters, i.e. types, so you have to be able to have e.g. types of type int, as well as types of type type, and it all gets a lot simpler and easier to work with if you just say that types have type type.
> And why is no distinction made between `typeof(type)` and `type`?
Well that's the whole point, to say that type is of type type.
> And doesn't the entire problem go away if you distinguish between `typeof(type)`, which is a value whose type is `type`?
No, because why would you ever use it as a value? The whole point of typeof is that it gives you a type that you can use as a type.
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
> [ 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
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.