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

[Iavor Diatchki]

Hello,

On Tue, Aug 21, 2018 at 7:06 AM Richard Eisenberg <rae at cs.brynmawr.edu>
wrote:

>
> >
> > 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.
>
> Why? it is not introduced by a `data` declaration.



> >   * how about `Eq`?
>
> It's a "constraint constructor", a generalization of a type class.
>
> Yes, we could refer to the things that construct types of kind K, as
K-constructors, and indeed sometimes people do.   This is consistent, for
example we could say that `4` is a `Nat` constructor.  However, it is also
convenient to have the concept of a "type constructor", which ranges over
all of these things, independent of what their kind is.   And, the question
of how they were introduced (through a `data` declaration, a class, as a
primitive or in some other way) is often completely irrelevant.


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

I think the current terminology works just fine and we don't need to keep
inventing new names.

>   * 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.
>
> I was referring to the fact that some type functions meet your definition
of a type constructor: when applied to enough arguments they produce
something of kind `Type`.



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

I think that this is the crux of our misunderstanding: if it is really the
same thing, then why does it have different names, and some of them are
only available sometimes.
In what sense does a `type data` declaration introduce a `data`
constructor, if this `data` constructor can never be used at the value
level (e.g., in a case statement)?


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

We may be able to implement this proposal as just a change to a
data-constructor's namespace (I am not sure, last time I tried to do it, it
seemed more complicated than this, but this was a long time ago, and I a
much more familiar with how GHC works now).   Explaining it that way is not
simpler, however, as this discussion has illustrated.

This is a summary:
   * this proposal does NOT change `data` declarations---they work just
like they do at the moment,
   * this proposal does NOT change anything to do with promotion (or
whatever we want to call what `DataKinds` does)
   * this proposal DOES introduce a new language construct, `type data`,
which looks somewhat like a `data` declaration, but it is not the same
(e.g. no records, no strictness, unpacking, constructors can't be the same
as the LHS, etc.)
   * the purpose of `type data` is to declare some new type-level
constants, that's all.

-Iavor
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-steering-committee/attachments/20180821/aae39985/attachment.html>