= Defining kinds without an associated datatype = This page tracks feature requests for declaring closed data kinds without associated data types (#6024) and declaring open data kinds that can be freely extended after they are declared (#11080). What comes below is a design proposal that is not yet implemented (as of Jan 2015). Main person responsible for working on the implementation is Jan Stolarek (JS). == Motivation for closed data kinds (#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: {{{#!hs data Universe star = Sum (Universe star) (Universe star) | Prod (Universe star) (Universe star) | K star }}} This universe comes with an associated interpretation: {{{#!hs 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`). '''Note''': this is no longer the case - see below. 2. We lose constructor name space, because the datatype constructor names will be taken, even though we will never use them to construct terms. So `Prod` and `K` cannot be used as constructors of `Interpretation` as above, because those are also constructors of `Universe`. == Motivation for open data kinds (#11080) == Users might want to create type-level symbols for the purpose of indexing types. In the past one way of doing this was by using `-XEmptyDataDecls`. But symbols created in this way were always placed in `*` and that does not allow to use kinds to limit what types are admitted as indices. `-XDataKinds` allows to create symbols that are assigned a kind other than `*` but these kinds are closed and adding new symbols is not possible. Thus: 3. We want a way of defining open kinds that can be later extended with new inhabitants. = Solution = I (JS) propose that the mechanism for declaring closed and open data kinds becomes part of `-XDataKinds`. The proposal is backwards compatible. == Closed kinds == Starting with GHC 8.0 users can use `-XTypeInType` extension to write: {{{#!hs data Universe = Sum Universe Universe | Prod Universe Universe | K (*) }}} This addresses disadvantage (1) but still leaves us with disadvantage (2). So the idea behind #6024 is to let users define things like: {{{#!hs -- closed kind using H98 syntax data kind Universe = Sum Universe Universe | Prod Universe Universe | K (*) -- closed kind using GADTs syntax data kind Universe where Sum :: Universe -> Universe -> Universe Prod :: Universe -> Universe -> Universe K :: * -> Universe }}} 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 valid only in types only, and not in terms. == Open kinds == Open data kinds would be declared using following syntax: {{{#!hs -- open kind data kind open Universe data kind member Sum :: Universe -> Universe -> Universe data kind member Prod :: Universe -> Universe -> Universe data kind member K :: * -> Universe }}} Note that open kinds can be parametrized just like closed kinds: {{{#!hs data kind open Dimension :: * data kind member Length :: Dimension data kind open Unit :: Dimension -> * data kind member Meter :: Unit 'Length data kind member Foot :: Unit 'Length }}} = Caveats = == Kind and Type Namespaces == Currently GHC has separate namespaces for types and data constructors. We have a simple rule: all data constructors go into data namespace. With `-XDataKinds` promoted data constructors still live in data constructor namespace and there is a hack in the renamer: when renaming types it first looks for a symbol in type namespace and if that fails then it searches for the symbol in the data namespace. Assume we have: {{{#!hs data kind Foo = MkFoo }}} In order to resolve disadvantage (2), ie. not pollute data constructor namespace with `MkFoo`, we would have to put `MkFoo` in the type namespace. This means that our simple rule "data constructors go into data namespace" would have to be broken. [https://mail.haskell.org/pipermail/ghc-devs/2015-December/010812.html Richard Eisenberg argues] that this is bad and in the case of above declaration `MkFoo` should go into data namespace. But that does not solve disadvantage (2) and thus misses the point of #6024 (given that disadvantage (1) is already solved by `-XTypeInType`). Richard also argues that members of an open data kind should also be placed in data namespace. Putting `MkFoo` into data namespace will also allow us to have quite good error messages from the typechecker, rather than cryptic error messages from the renamer about things being out of scope. == Non-promotable data types? == Let's assume for a moment that we decide to place kind-only constructors in the type namespace (ie. not follow Richard's proposal). Consider again the example of `Universe` kind and `Interpretation` data type. Enabling `-XTypeInType` makes GADTs promotable. This means that data constructors `K` and `Prod` if `Interpretation` data type could be validly used in types. But this would lead to name collission with `K` and `Prod` constructors of `Universe` kind. There would be no way of disambiguating whether `K` refers to constructor of `Universe` or promoted constructor of `Interpretation`. We don't want to end up in a situation where some of the data constructors can be promoted (`L`, `R`) and some can't (`K`, `Prod`). So we would need to make `Interpretation` data type unpromotable. But detecting that seems Real Hard. == Recursive Groups == We need to be careful about recursive groups. For example, this is valid: {{{#!hs data S = S T data T = T S }}} but this is not: {{{#!hs data kind S = S T data T = T S }}} == Future-proofing the design == GHC is growing more and more type level symbols. These symbols vary in their properties like generativity, injectivity, matchability or being open/closed - see [ticket:9840#comment:6] for an overview. Here we propose adding yet another way of defining symbols. Can we introduce more order into world of type-level symbols? Can we have some unifying syntax? Can we anticipate what kind of symbols we might want to have in the future? = Alternative Notations = * Use `data only` instead of `data type`. * Use `'data` instead of `data kind` * Use `type data` instead of `data kind` * Use `data constructor` instead of `data kind member` * Use `data extension Unit where { Meter :: Unit; Foot :: Unit }` instead of `data kind member`