Indeed - the Type/Kind hierarchy is unified when you write a dependently typed system. In simply typed lambda calculus, you have a system of values, types, and kinds, which are required to make sense of the structure. In dependent types, you have values, and types, which are also values.
Type/Kind hierarchy is unified when you write a dependently typed system
i'm being pedantic, but i don't think that's always the case. afaik
Type : Type
leads to "inconsistency" (sounds like Russell's paradox, but my knowledge of the theory gets flaky here). so e.g. in Coq there's actually a hierarchy of "universes":
"[The type of Int is Set, ] the type of Set is Type(0), the type of Type(0) is Type(1), the type of Type(1) is Type(2), and so on."
Comments
Indeed - the Type/Kind hierarchy is unified when you write a dependently typed system. In simply typed lambda calculus, you have a system of values, types, and kinds, which are required to make sense of the structure. In dependent types, you have values, and types, which are also values.
i'm being pedantic, but i don't think that's always the case. afaik
leads to "inconsistency" (sounds like Russell's paradox, but my knowledge of the theory gets flaky here). so e.g. in Coq there's actually a hierarchy of "universes":http://adam.chlipala.net/cpdt/html/Universes.html
(though a dependently-typed system may hide universes from the user by default and offer "universe polymorphism" to allow them to gloss over it)