Version 14 (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.

Also,

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.

## Other Extensions

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.

## Alternative Solutions

Add

data Star

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)

## Alternative Notations

- 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.