|Version 12 (modified by heisenbug, 2 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
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.
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)
- 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.)