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

Wed Aug 29 13:27:16 UTC 2018

Thanks Richard!

Iavor, Adam Gundry has raised a good question on the public discussion.

> This proposal doesn't seem to mention record fields. What happens if I write this?
>   type data T = MkT { foo :: Bool }
> Is this an error, or does it simply not bring foo into scope at all (at least until some hypothetical future where we can talk about record field selectors in type-level expressions)?

My inclination is that this should be an error, since there's no way to refer to the `foo` selector, but it would be good to specify the answer in the proposal.

Apart from that, I think we've reached a consensus on accepting the proposal. 

What's the next step, Joachim? Do I just mark the proposal as accepted?

On Tue, Aug 28, 2018, at 16:41, Richard Eisenberg wrote:
> OK. I'm convinced now that I should seek further and wider community 
> feedback before pushing through this terminology change. A proposal may 
> be the right way to do that, though it doesn't quite fit within the 
> proposal-process remit.
> 
> Given this, I withdraw my objections and support the current proposal.
> 
> Richard
> 
> > On Aug 21, 2018, at 9:18 AM, Eric Seidel <eric at seidel.io> wrote:
> > 
> > Thanks Iavor and Richard for your comments. This whole discussion has been quite illuminating to me as well. (The more I sleep on it, the more I feel swayed by Richard's perspective.)
> > 
> > That being said, I don't think this proposal is the right place to settle the issue. I think my recommendation at this point would be to:
> > 
> > 1. Accept the proposal as is. It uses standard terminology, and within that framework I think it is quite clear.
> > 2. Encourage Richard to write up another proposal to discuss the broader terminology issue. It seems like ghc-proposals would actually be a natural place to discuss this further. It doesn't really affect the implementation, but it would have a big impact on the Manual.
> > 
> > On Tue, Aug 21, 2018, at 01:47, Iavor Diatchki wrote:
> >> 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
> >> _______________________________________________
> >> ghc-steering-committee mailing list
> >> ghc-steering-committee at haskell.org
> >> https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee
> > _______________________________________________
> > ghc-steering-committee mailing list
> > ghc-steering-committee at haskell.org
> > https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee
> 