Richard makes good points here. Cheers, Manuel

Am 15.08.2018 um 05:09 schrieb 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 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...

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@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee

_______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee

On Aug 15, 2018, at 9:41 AM, Eric Seidel wrote:

The normal syntax for exporting data constructors would export the constructor in both the value namespace AND the type namespace. But we didn't want the constructor in the value namespace to begin with. I think this is the issue, we have no way to export ONLY the constructor in the type namespace.

I disagree here. The normal syntax exports data constructors only in the data-level namespace, because those constructors don't live at all in the type-level namespace. (The ' syntax doesn't promote anything: it's just a signal to the renamer to look only in the data-level namespace, bypassing the normal type-level lookup.) Right now, the only way to get a data constructor in the type-level namespace is to use a type synonym, and (presumably) the author of this proposal finds that fact annoying (understandably).

I think "type-level data constructors" just makes things more confusing. The way I think about it (and I could certainly be wrong!), data constructors produce objects that can be used at the value level, and type constructors produce objects that can be used at the type level.

This is a common usage of these terms, so you're not alone. But I don't think it's a helpful vocabulary. The dependent types literature diverges from this usage considerably, not distinguishing between runtime data and compile-time data. As GHC inches toward dependent types (even if we get no further in this direction, the "promotion" feature is directly inspired by dependent types), I think updating our usage of these vocabulary words will be helpful.

We still have a value/type level distinction in Haskell, so the term "type-level data constructor" reads like an oxymoron to me.

Is it perhaps more comfortable to think of compile-time data vs. runtime data?

Another way of saying this could just be that "data" constructors live in the value namespace, while "type" constructors live in the type namespace.

I think it all boils down to vocabulary here. We could define the terms this way. But then we need to talk about promoting data constructors to type constructors. We also have the awkwardness of explaining that, say, `'True` is a type (it is used on the type level) but no values have type `'True`. I think it's much clearer to say that `'True` is type-level data. No promotion anymore, just namespaces, and we reserve type to mean things like `Int`.

If you think of type constructors in my sense, then I think it also makes sense to call the constructors introduced by `type data` type constructors.

Agreed about this implication. But since I don't satisfy your premise, I'm not bound to agree with your conclusion. To be clear, I don't think there's a "right" vocabulary and a "wrong" vocabulary here. (And perhaps my email from yesterday is too strongly worded in places around this -- apologies.) I do think the vocabulary I'm advocating for will lead to a simpler formulation of this all and will help Haskellers get a better intuition around these features than the other vocabulary. This change has been slow to formulate in my own head, and is the result of thinking about these issues a lot over the past years -- I, too, have wanted to call data constructors used in types "type constructors". I no longer think it's the best way to describe it, though. I hope this helps! Richard

It sounds like we all agree that the disagreement is mostly over terminology, specifically, over the definition of a type constructor. Richard prefers a definition that limits type constructors to producing objects of type Type (or Constraint), whereas I (and Iavor, I think) prefer a broader definition that encompasses any constructor that produces an object that can be used at the type-level. Richard points out, correctly, that when Dependent Haskell arrives, the value/type level distinction will disappear, and our definition will become (mostly) untenable. (I say mostly because, at least in my limited experience with dependent types, you often still have objects that are used primarily in a type context, and so an informal value/type distinction could still be useful.) The question then is what to do in the meantime. Do we stick with the established terminology and incur a larger change when Dependent Haskell arrives, or do we start making preparations now? I think Richard's perspective makes sense for a dependently-typed language, but Haskell is not dependently-typed, yet. So I'm inclined to say the change of terminology should be deferred to the Dependent Haskell proposal. I know we generally operate on the silence-means-agreement principle, but this disagreement is over a pretty crucial definition, so I'd like to solicit feedback from the rest of the committee. On Thu, Aug 16, 2018, at 06:02, Iavor Diatchki wrote:

Hello,

I'd be happy to make changes to the text of the proposal, but I would like to understand the underlying concerns so that I can address them appropriately. At the moment, I am pretty sure that I am missing something, as might be evident from my comments below. Either way, my comments below are intended to shed some light on my thinking, and emphasize the parts of Richard's comments I don't understand.

On Wed, Aug 15, 2018 at 6:10 AM Richard Eisenberg wrote:

...

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

The proposal uses the same terminology that is used in GHC's manual, and also by the majority of the Haskell community. For example, Section 10.1 of the manual is about "Datatype Promotion", and the summary is "Allow promotion of data types to kind level.". Section 10.10.2 says "With DataKinds, GHC automatically promotes every datatype to be a kind and its (value) constructors to be type constructors.". This proposal introduces a language construct that allows us to declare non-empty kinds without having to promote a datatype in the sense of 10.1. I am talking about the language specification, not the actual implementation, which we can discuss once we agree we'd like to have this new feature.

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.

Of course this is technically correct, but without data type promotion these are empty kinds that are a side-effect of mixing up types and kinds. I say empty "kinds" rather than empty "types" to emphasize the fact that I am referring to the kinding relation, not the typing one.

...

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

Here is a datatype declaration:

data T = A | B

In current GHC how would you export the type `A` of kind `T` without exporting the value `A` of type `T`?

Here is my attempt:

{-# Language DataKinds, ExplicitNamespaces #-}

module M (type A) where

data T = A | B

This results in:

error: Not in scope: type constructor or class ‘A’ | 3 | module M (type A) where | ^^^^^^

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

I think that with this proposal we have a much easier way to explain how things work, without having to refer to the algorithm used by GHC's renamer:

data T = A | B -- T is a type, and A and B are values of this type type data S = X | Y -- S is a kind, and X and Y are types of this kind

Simple.

...

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

This proposal is orthogonal to `DataKinds` and does not change anything about how it works.

Personally, if I had `TypeData`, I think I would very rarely use `DataKinds`, except for type-level nats and symbols, which should probably get a separate extension anyway. The reason is that I rarely need the same constructors at the value and the type level without any link between the two.

...

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

I am sorry but I don't understand this at all---it is going contrary to the terminology used by the Haskell community for decades. I really don't see why we need to invent new terms, and arbitrarily limit the term "type-constructor" to only types of kind `Type` or `Constraint`, especially if we are willing to refer to all "kinds" as "types". The notion of classifying types by kinds and having a rich kind language is completely orthogonal to dependent types, and I think the current terminology works just fine.

If I am reading Richard's comments correctly (and I apologize if I am misunderstanding) his main concern is about terminology, based on his vision and plans about Dependent Haskell. I am supportive of work in this area, but I don't think that this proposal is the right place to start changing the terminology. I would suggest that we stick with the established language, which is widely used by the community, GHC's manual, and GHC's source code. Once there is a design document for Dependent Haskell, we could discuss that and settle on appropriate terminology.

-Iavor

...

Thanks, Richard

...

On Aug 14, 2018, at 8:31 PM, Eric Seidel 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...

...

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

...

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

value namespace. 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@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee

_______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee

_______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee

On Aug 17, 2018, at 3:22 AM, Simon Peyton Jones via ghc-steering-committee wrote:

Can you restate the terminological choice(s) as explicitly as possible, with examples?

Old: type: Something used at the type level. In contrast to "type constructor", generally doesn't take any arguments. Examples: Int, Bool, 4, 'True, '[Int, Bool], '[] type constructor: Something used in a function position in a type. Examples: Maybe, Either, 'Just data constructor: A symbol used to construct a data element of some type at runtime. Examples: True, Nothing, Left. Non-examples: 'True, 'Nothing, 'Left. promotion: 'True is a type that is the promoted form of the data constructor True; 'Just is a type constructor that is the promoted form of the data constructor Just. New: type: Something that can reasonably go to the right of a ::. In other words, an element of the kind * (or Type). Examples: Int, Bool, Maybe Double. Non-examples: 4, 'True, '[Int, Bool], '[] type constructor: Something that, when applied to the right number of well-kinded arguments, becomes a type. Examples: Maybe, Either. Non-example: 'Just data constructor: A symbol used to construct a data element of some type, at either runtime or compile-time. Examples: True, Nothing, Left, 'True, 'Nothing, 'Left. promotion: No longer used. 'True and True are now the same thing: both data constructors, just used in different contexts. NB: This is all about user-facing documentation. I am not proposing any change to GHC datatypes. I hope this helps! Richard

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. 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? * how about `Eq`? * how about a type variable `f`? * are type functions really type constructors? * are we really suggesting that we should start supporting things like `'True` at the value level? 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. -Iavor On Fri, Aug 17, 2018 at 6:46 PM Richard Eisenberg wrote:

On Aug 17, 2018, at 3:22 AM, Simon Peyton Jones via ghc-steering-committee wrote:

Can you restate the terminological choice(s) as explicitly as possible, with examples?

Old:

type: Something used at the type level. In contrast to "type constructor", generally doesn't take any arguments. Examples: Int, Bool, 4, 'True, '[Int, Bool], '[] type constructor: Something used in a function position in a type. Examples: Maybe, Either, 'Just data constructor: A symbol used to construct a data element of some type at runtime. Examples: True, Nothing, Left. Non-examples: 'True, 'Nothing, 'Left. promotion: 'True is a type that is the promoted form of the data constructor True; 'Just is a type constructor that is the promoted form of the data constructor Just.

New:

type: Something that can reasonably go to the right of a ::. In other words, an element of the kind * (or Type). Examples: Int, Bool, Maybe Double. Non-examples: 4, 'True, '[Int, Bool], '[] type constructor: Something that, when applied to the right number of well-kinded arguments, becomes a type. Examples: Maybe, Either. Non-example: 'Just data constructor: A symbol used to construct a data element of some type, at either runtime or compile-time. Examples: True, Nothing, Left, 'True, 'Nothing, 'Left. promotion: No longer used. 'True and True are now the same thing: both data constructors, just used in different contexts.

NB: This is all about user-facing documentation. I am not proposing any change to GHC datatypes.

I hope this helps! Richard _______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee

Hello, On Tue, Aug 21, 2018 at 7:06 AM Richard Eisenberg 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

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 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 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@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee

---

ghc-steering-committee mailing list ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee

Hi, Am Mittwoch, den 29.08.2018, 09:27 -0400 schrieb Eric Seidel:

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

yes. Or you declare it as accepted here on the mailing list, and I mark it as such on GitHub (I have to touch it anyways, to merge it and give it the final proposal number). Cheers, Joachim -- Joachim Breitner mail@joachim-breitner.de http://www.joachim-breitner.de/

Though I'd still like to have it specify what happens with record selectors, as pointed out by Adam. On Wed, Aug 29, 2018, at 13:21, Eric Seidel wrote:

Ok, then I declare it accepted!

On Wed, Aug 29, 2018, at 13:17, Joachim Breitner wrote:

...

Hi,

Am Mittwoch, den 29.08.2018, 09:27 -0400 schrieb Eric Seidel:

...

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

yes. Or you declare it as accepted here on the mailing list, and I mark it as such on GitHub (I have to touch it anyways, to merge it and give it the final proposal number).

Cheers, Joachim

-- Joachim Breitner mail@joachim-breitner.de http://www.joachim-breitner.de/ _______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee Email had 1 attachment: + signature.asc 1k (application/pgp-signature)

Yes, I got a bit excited to exercise my power :) On Wed, Aug 29, 2018, at 15:11, Joachim Breitner wrote:

Hi,

in that case, I suggest you work with the authors to get that fixed, and only then pronounce it accepted :-)

Cheers, Joachim

Am Mittwoch, den 29.08.2018, 13:22 -0400 schrieb Eric Seidel:

...

Though I'd still like to have it specify what happens with record selectors, as pointed out by Adam.

On Wed, Aug 29, 2018, at 13:21, Eric Seidel wrote:

...

Ok, then I declare it accepted!

On Wed, Aug 29, 2018, at 13:17, Joachim Breitner wrote:

...

Hi,

Am Mittwoch, den 29.08.2018, 09:27 -0400 schrieb Eric Seidel:

...

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

yes. Or you declare it as accepted here on the mailing list, and I mark it as such on GitHub (I have to touch it anyways, to merge it and give it the final proposal number).

Cheers, Joachim

-- Joachim Breitner mail@joachim-breitner.de http://www.joachim-breitner.de/ _______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee Email had 1 attachment: + signature.asc 1k (application/pgp-signature)

_______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee -- Joachim Breitner mail@joachim-breitner.de http://www.joachim-breitner.de/

---

ghc-steering-committee mailing list ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee Email had 1 attachment: + signature.asc 1k (application/pgp-signature)

The proposal has been updated to specify that record selectors, quantifiers, and bangs/unpacks are disallowed in `type data`. These restrictions all make sense to me, at least for now, so I think we can properly declare this proposal accepted. On Thu, Aug 30, 2018, at 09:53, Iavor Diatchki wrote:

Indeed, record selectors are not supported in type data, and should result in an error. Same for other special things like strictness annotations, unpack pragmas, and quantifiers.

I am on vacation without a computer at the moment and I am not sure if I can edit the proposal from my phone, but I'll give it a go later.

Iavor

On Wed, Aug 29, 2018, 11:42 PM Eric Seidel wrote:

...

Yes, I got a bit excited to exercise my power :)

On Wed, Aug 29, 2018, at 15:11, Joachim Breitner wrote:

...

Hi,

in that case, I suggest you work with the authors to get that fixed, and only then pronounce it accepted :-)

Cheers, Joachim

Am Mittwoch, den 29.08.2018, 13:22 -0400 schrieb Eric Seidel:

...

Though I'd still like to have it specify what happens with record selectors, as pointed out by Adam.

On Wed, Aug 29, 2018, at 13:21, Eric Seidel wrote:

...

Ok, then I declare it accepted!

On Wed, Aug 29, 2018, at 13:17, Joachim Breitner wrote:

...

Hi,

Am Mittwoch, den 29.08.2018, 09:27 -0400 schrieb Eric Seidel: > What's the next step, Joachim? Do I just mark the proposal as accepted?

yes. Or you declare it as accepted here on the mailing list, and I mark it as such on GitHub (I have to touch it anyways, to merge it and give it the final proposal number).

Cheers, Joachim

-- Joachim Breitner mail@joachim-breitner.de http://www.joachim-breitner.de/ _______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org

https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee

...

Email had 1 attachment: + signature.asc 1k (application/pgp-signature)

_______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org

https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee -- Joachim Breitner mail@joachim-breitner.de http://www.joachim-breitner.de/ _______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee Email had 1 attachment: + signature.asc 1k (application/pgp-signature)

---

ghc-steering-committee mailing list ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee

Iavor brings up some really good points here. He's right that I'm (mostly) arguing about terminology. At their core, I might summarize Iavor's points as follows: * Should we change this terminology at all? * If so, should we do so now? Unsurprisingly, I wish to argue "yes" to both points. First off, I recognize that I'm arguing against the Haskell grain right now, in that the terminology is well established. I had not considered the use of, say, "type constructor" in the manual. (In all this, I'm thinking solely of user-facing features, not at all the GHC implementation.) I did not acknowledge this in my first email in this thread. Why change the terminology? - The current terminology puts us out of step with the dependent types community. The features we're discussing (i.e., the ability to use `'True' as a type argument) exist only in Haskell and in dependently typed languages. It thus seems sensible to be in line with dependently typed languages in our terminology. - Calling `'True` a type leads to confusion, because some people want to find some term whose type is `'True`, but such a thing cannot exist. - Currently, we say that * is the "kind of types with values". But someone could reasonably ask whether Void has kind * -- after all, Void is inhabited by no values. (It is inhabited by `undefined`, but that's not a value.) So "kind of types with values" is a bit wrong. Perhaps better would be "kind of types inhabited by terms", but that's an even wordier mouthful. With the proposed change in terminology, we could just say that * is the kind of types. Simple! (Naturally, this works beautifully with *'s new name, Type.) - It's conceptually simpler (to me), to think of `'True` and `True` as the same thing. In the new terminology, both are data constructors. Indeed, we can refer to them as being the same -- the ' is there because the two appear in different contexts and therefore must be spelled slightly differently (like we understand M.lookup and Map.lookup to be the same thing but with different import statements in scope). By describing the two as the same, we have better intuition around, e.g., export/import lists, where there would no longer be a desire to export/import the "type constructor" independently of the "data constructor". - Right now, datatypes and data families have a restriction that their kinds end in `... -> *`. With the new terminology, we can just say these must be type constructors. - GHC uses this terminology in a limited way in error messages. If you say `x :: 'True`, GHC says that True is expected to be a type. According to the "old" terminology, `'True` *is* a type, so this error message is misleading. Under the new terminology, it works just fine. Reasons to keep the existing terminology: - It's existing. This means that it's familiar to many and has been enshrined in written materials. - Many find the type-leve/term-level distinction to be a convenient proxy for the compile-time/runtime distinction. In today's Haskell, this is accurate, though it would change with dependent types. However, my suggested change in terminology does not change this -- it just means that data constructors can be used at the type level. We should also consider the timing of this change. Why do this now instead of waiting? - The new terminology makes as good sense today as it will in a dependently typed future. Even if the development toward dependent types stops, this change is worthwhile for the reasons above, none of which appeal to any features that do not already exist. - The right time for any change of this sort is "yesterday". But seeing as we can't do that, let's do "today", the next best thing. Essentially, my argument here is that we got this all slightly wrong when -XDataKinds came into being -- not the feature, but the way we describe it. Perhaps this is all just much ado about little, but I do think this small change in how we speak of these features will help Haskellers learn how they work with the right set of intuitions. (I would like to note that my arguments here are borne of experience. I was not part of the initial wave of design of -XDataKinds, but if I had been, I'm sure I would have gone with what I'm calling the "old" terminology.) Thanks, Richard

On Aug 16, 2018, at 6:02 AM, Iavor Diatchki wrote:

Hello,

I'd be happy to make changes to the text of the proposal, but I would like to understand the underlying concerns so that I can address them appropriately. At the moment, I am pretty sure that I am missing something, as might be evident from my comments below. Either way, my comments below are intended to shed some light on my thinking, and emphasize the parts of Richard's comments I don't understand.

On Wed, Aug 15, 2018 at 6:10 AM Richard Eisenberg mailto:rae@cs.brynmawr.edu> wrote:

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

The proposal uses the same terminology that is used in GHC's manual, and also by the majority of the Haskell community. For example, Section 10.1 of the manual is about "Datatype Promotion", and the summary is "Allow promotion of data types to kind level.". Section 10.10.2 says "With DataKinds, GHC automatically promotes every datatype to be a kind and its (value) constructors to be type constructors.". This proposal introduces a language construct that allows us to declare non-empty kinds without having to promote a datatype in the sense of 10.1. I am talking about the language specification, not the actual implementation, which we can discuss once we agree we'd like to have this new feature.

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.

Of course this is technically correct, but without data type promotion these are empty kinds that are a side-effect of mixing up types and kinds. I say empty "kinds" rather than empty "types" to emphasize the fact that I am referring to the kinding relation, not the typing one.

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

Here is a datatype declaration:

data T = A | B

In current GHC how would you export the type `A` of kind `T` without exporting the value `A` of type `T`?

Here is my attempt:

{-# Language DataKinds, ExplicitNamespaces #-}

module M (type A) where

data T = A | B

This results in:

error: Not in scope: type constructor or class ‘A’ | 3 | module M (type A) where | ^^^^^^

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

I think that with this proposal we have a much easier way to explain how things work, without having to refer to the algorithm used by GHC's renamer:

data T = A | B -- T is a type, and A and B are values of this type type data S = X | Y -- S is a kind, and X and Y are types of this kind

Simple.

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

This proposal is orthogonal to `DataKinds` and does not change anything about how it works.

Personally, if I had `TypeData`, I think I would very rarely use `DataKinds`, except for type-level nats and symbols, which should probably get a separate extension anyway. The reason is that I rarely need the same constructors at the value and the type level without any link between the two.

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

I am sorry but I don't understand this at all---it is going contrary to the terminology used by the Haskell community for decades. I really don't see why we need to invent new terms, and arbitrarily limit the term "type-constructor" to only types of kind `Type` or `Constraint`, especially if we are willing to refer to all "kinds" as "types". The notion of classifying types by kinds and having a rich kind language is completely orthogonal to dependent types, and I think the current terminology works just fine.

If I am reading Richard's comments correctly (and I apologize if I am misunderstanding) his main concern is about terminology, based on his vision and plans about Dependent Haskell. I am supportive of work in this area, but I don't think that this proposal is the right place to start changing the terminology. I would suggest that we stick with the established language, which is widely used by the community, GHC's manual, and GHC's source code. Once there is a design document for Dependent Haskell, we could discuss that and settle on appropriate terminology.

-Iavor

Thanks, Richard

...

On Aug 14, 2018, at 8:31 PM, Eric Seidel mailto:eric@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... https://github.com/yav/ghc-proposals/blob/data-kind-only/proposals/0000-type...

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@haskell.org mailto:ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee

_______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org mailto:ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee _______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org mailto:ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee