wiki:GhcKinds/KindsWithoutData

Version 12 (modified by heisenbug, 13 months ago) (diff)

suggest kind only syntax

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:

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

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

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