Allow defining kinds alone, without a datatype
Sometimes we want to define a kind alone, and we are not interested in the datatype. In principle having an extra datatype around is not a big problem, but the constructor names will be taken, so they cannot be used somewhere else. A contrived example:
data Code = Unit | Prod Code Code data family Interprt (c :: Code) :: * data instance Interprt Unit = Unit1 data instance Interprt (Prod a b) = Prod1 (Interprt a) (Interprt b)
We're only interested in the constructors of the data family
Interprt, but we cannot use the names
Prod because they are constructors of
The suggestion is to allow defining:
data kind Code = Unit | Prod Code Code
Code is a kind, and not a type, and
Prod are types, and not constructors.
Note that using "data kind" instead of just "kind" means the word "kind" does not have to be a reserved keyword.
You could also think you would want to have datatypes that should not be promoted:
data K data type T = K
But I don't see a need for this, as the fact that the
K constructor is promoted to a type does not prevent you from having a datatype named
|Component||Compiler (Type checker)|