4 ms·
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 sens
by ImprobableTruth 6y ago
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.
- icen 6y agoIndeed - 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.
- uryga 6y ago> 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." http://adam.chlipala.net/cpdt/html/Universes.html 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)