It's just standard dependent types. Types don't (necessarily) get erased, but all the type checking itself is done at compile time.
I don't think it makes sense to think of it as specifically "statically kinded", since kinds (which are just types higher on the universe hierarchy) can also be present at runtime.
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
It's just standard dependent types. Types don't (necessarily) get erased, but all the type checking itself is done at compile time.
I don't think it makes sense to think of it as specifically "statically kinded", since kinds (which are just types higher on the universe hierarchy) can also be present at runtime.
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)