In a language with dependent types you can have Type-in-Type which simplifies the language and gives it a lot of power. This makes the language logically inconsistent but this might not be a problem if you are interested in programming only and not theorem proving.
In the Cayenne paper (a dependently typed language for programming) it is mentioned about Type-in-Type that "the unstratified type system would make it impossible during type checking to determine if an expression corresponds to a type or a real value and it would be impossible to remove the types at runtime" (section 2.4).
I have two questions about this:
- In some dependently typed languages (like Agda) you can explicitly say which variables should be erased. In that case does Type-in-Type still cause problems?
- We could extend the hierarchy one extra step with
Kind
whereType : Kind
andKind : Kind
. This is still inconsistent but it seems that now you can know if a term is a type or a value. Is this correct?