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

[Richard Eisenberg]

> On Aug 20, 2018, at 3:00 AM, Iavor Diatchki <iavor.diatchki at gmail.com> wrote:
> 
> Hello,
> 
> These are significant changes to the current terminology and I really don't think that this is the right place to discuss them---I think that they are significant enough that they deserve their own proposal, with motivation, and discussion by the community.

Perhaps you're right that this should go out to the community. Nevertheless, I'm finding the discussion here to be very helpful, as it's refining my own understanding of this all. If the general consensus here is that we need more community feedback on these points, I'm happy to seek it out.

> 
> Here are some things to think about, if such a proposal is ever written:
>   * in this new terminology `4` is not a type, but it also does not fall in any of the other categories, so what is it?

It's type-level data.

>   * how about `Eq`?

It's a "constraint constructor", a generalization of a type class.

>   * how about a type variable `f`?

It's a type variable. But this is a great question: should it be something else, perhaps a quantified variable (if `f`'s kind isn't Type)? After all, if we have (f :: Nat), then f wouldn't range over types. Indeed, I think calling an f of non-Type kind something other than a type variable would be an improvement. I don't have a great suggestion of what we should call it, though.

>   * are type functions really type constructors?

I'm not sure what this means. Right now, if we have `type family F a`, then F isn't really a type constructor, as we can't ever write a plain F in a Haskell program.

>   * are we really suggesting that we should start supporting things like `'True` at the value level?

No. I'm suggesting that `'True` and `True` are just two different ways of referring to the same thing. The former is accepted only in a type-level context.

> 
> Anyway, it seems to me that we have gone a little off-course, and these changes are not really about making #106 easier to understand.

But I think they are, for the reasons I've articulated above. The GitHub trail contains several comments to the effect of "this proposal is simply a change in data constructors' namespace" but the proposal describes the new feature as a change to promotion.

Richard