[ghc-steering-committee] Proposal: Define Kinds Without Promotion (#106)

[Richard Eisenberg]

I'm neutral on this proposal, but I know there are others who are quite keen on it, so that favors acceptance. However, I would request changes to the proposal text: this proposal has nothing at all to do with promotion. Instead, this is all to do with namespaces. I think a lot of clever people misunderstand this point, and so I would want the proposal to be carefully worded around this.

Under this proposal, a the constructors of a datatype introduced with `type data` are added to the type-level namespace instead of the data-level namespace. And that's it!

Specifically:

- Types and kinds are simply the same now. There really is no difference. So the first sentence of this proposal, "This proposal introduces a language construct for defining kinds without having to promote types." is, in my opinion, quite misleading. All `data` declarations introduce kinds (because they introduce types, and types = kinds). And data constructors aren't really promoted either -- they can simply be used in types.

- The proposal talks about referring to types in export lists. But we can already do this, via the normal syntax for listing data constructors with type constructors. So I'm not sure what that point of motivation really means.

- The "normal types win" is true, but it's all about namespace lookup. In a type, when GHC sees a capitalized identifier, it looks in the type namespace for that identifier. If the identifier is bound in the type namespace, that identifier is found. If not, GHC looks in the data-level namespace. According to this algorithm, "normal types win", indeed. But the "normal"cy of the type is that it lives in the type namespace, not because it isn't promoted.

- If something introduced with `type data` can be used without -XDataKinds, then what does -XDataKinds really mean? It would seem to enable solely the extra data-level namespace check. That's fine with me, but we should document it that way. Alternatively, -XDataKinds could mean that some types have kinds that don't end in Type or Constraint, in which case it would need to be enabled to use a `type data` data constructor.

- The RHS of a `type data` does not introduce type constructors. A type constructor constructs a type -- that is, if T is a type constructor, then T applied to appropriate arguments has kind Type (or Constraint). But the data constructors of `type data` really are data constructors. It just so happens that their names live only in the type-level namespace. If we want, we can call these "type-level data constructors", but I think "type constructors" is misleading.

Rereading the GitHub trail, I see that I've voiced support in the recent past. This is still true, but before this proposal text gets locked into perpetuity, I think clarifying the points above would be very helpful.

Thanks,
Richard

> On Aug 14, 2018, at 8:31 PM, Eric Seidel <eric at seidel.io> wrote:
> 
> Hi everyone!
> 
> This proposal would allow the declaration of new kinds and type constructors, without the associated data constructors that would have been generated by -XDataKinds.
> 
> https://github.com/yav/ghc-proposals/blob/data-kind-only/proposals/0000-type-data.rst
> 
> It introduces a new language extension, -XTypeData, which allows declarations like the following:
> 
>  type data Universe = Character | Number | Boolean
> 
> This introduces a new kind, Universe, with three associated type constructors
> 
>  Character :: Universe
>  Number :: Universe
>  Boolean :: Universe
> 
> Notably, no data constructors are introduced.
> 
> The proposal aims to solve several usability issues with -XDataKinds:
> 
> 1. We often don't want the data constructors, which simply pollute the value namespace.
> 2. We cannot easily control the export behavior of promoted types (instead we resort to tricks like the alias `type Character = 'Character`).
> 3. The name resolution rules involving promoted types can be confusing.
> 
> I find these issues (particularly #2) compelling, and the community response seems to be mostly positive, so I recommend accepting the proposal. 
> 
> I'm not particularly fond of the proposed syntax (`type data` makes it sound like we're doing something with data constructors, which is precisely what we're NOT doing), but the proposal has already had a good bit of bikeshedding, and people seem mostly happy with the current syntax, so I think we should probably stick with `type data`.
> 
> Eric
> _______________________________________________
> ghc-steering-committee mailing list
> ghc-steering-committee at haskell.org
> https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee