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.
> Why would you want to do this?
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.