|Version 15 (modified by elliottt, 2 years ago) (diff)|
Defining kinds without an associated datatype
This ticket to track this request is #6024.
When using -XDataKinds GHC automatically promotes every datatype to a kind, and its constructors to types. This forces us to declare a datatype for every kind. However, sometimes we are not interested in the datatype at all, only on the kind. Consider the following data kind that defines a small universe for generic programming:
data Universe star = Sum Universe Universe | Prod Universe Universe | K star
This universe comes with an associated interpretation:
data Interpretation :: Universe * -> * where L :: Interpretation a -> Interpretation (Sum a b) R :: Interpretation b -> Interpretation (Sum a b) Prod :: Interpretation a -> Interpretation b -> Interpretation (Prod a b) K :: a -> Interpretation (K a)
In this case, having to declare a datatype for Universe has two disadvantages:
- We cannot use kinds (such as *) while defining a datatype, so we are forced to make Universe a parametrised datatype, and later always instantiate this parameter to * (like in the kind of Interpretation).
- We lose constructor name space, because the datatype constructor names will be taken, even though we will never use them. So Prod and K cannot be used as constructors of Interpretation as above, because those are also constructors of Universe.
Solution: let users define things like
data kind Universe = Sum Universe Universe | Prod Universe Universe | K *
By using data kind, we tell GHC that we are only interested in the Universe kind, and not the datatype. Consequently, Sum, Prod, and K will be types only, and not constructors.
data type D = C
defines a datatype D which is not promoted to a kind, and its constructor C is not promoted to a type.
Star in Star
If, in the future, we make * :: *, we will no longer have separation of types and kinds, so we won't be able to make such fine distinctions.
Kind and Type Namespaces
As kinds and types currently share a namespace, data kind and data type declarations in the same module can still conflict. However, if they are in separate modules, this can be controlled by use of the module system.
in GHC.Exts such that the promotion of datatype Star is the kind *. As a datatype, Star is just an empty datatype.
Advantages: very easy, backwards compatible
Disadvantages: somewhat verbose, doesn't fix (2)
- Use data only instead of data type.
- Use 'data instead of data kind, suggested by Gabor Greif.
In both cases, we felt that using type and kind as the modifiers to the data declaration better reflect what's being defined.