I find the distinction between the two concepts a bit confusing, and it seems unnecessary. I understand that kinds are to types what types are to values, but I don’t understand why you can’t have types fulfilling that role. Langs like Lean don’t seem to need this extra concept. Or maybe I’m missing something?
PureScript now only has Types, where the types of Types are just other Types. PureScript’s type-language is technically dependently typed, while retaining a separate expression language. Lean is a fully dependently typed language, where it’s a single unified language all the way down.
Theorem provers also generally have universes of types. If everything is the “same” language, to retain logical consistency in a prover, you need some way of distinguishing the levels things refer to. So terms in level 2 express the types of terms in level 1, etc. Purescript has two languages now, where before it technically had 3 and stopped there. A unified term language with universes generalizes this.
1 Like
I see!
I don’t quite understand how these two expressions can be composed to keep climbing universes, and “program at the kind level”, for example.
Thank you for your reply! I’ll make better questions once I grok and apply this. 