Version 12 (modified by 5 years ago) (diff) | ,
---|

# Defining kinds without an associated datatype

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 1**: 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)

**Solution 2**: 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 only (i :: D) where C :: I ('C Int)

defines a datatype `D`

which is not promoted to a kind, and its constructors
are not promoted to types. We would then also have ‘type only T = Int -> Int`.

*Advantages*: solves (1) and (2)

*Disadvantages*:

- If, in the future, we make
`* :: *`

, we will no longer have separation of

types and kinds, so things like `D`

/`I`

above will become impossible.

- Requires changing the parser

Currently we are planning to implement the second solution. If we do get `* :: *`

other things will break due to name clashes, so that shouldn't prevent us from going ahead now. This ticket to track this request is #6024.

## Thoughts (Gabor Greif)

I'd prefer writing

'data Universe = Sum Universe Universe | Prod Universe Universe | K *

over `data kind`

to only obtain the `Universe`

kind and `Sum`

, `Prod`

and `K`

types. This would extrapolate the `'Universe`

notation for grabbing the kind when a type also exists with the same name.
I am also a bit less enthusiastic with `data only`

. Why not `data data`

? (Still does not feel right.)