I (the proposer) also want to clarify that the proposal leaves some wiggle room about the deprecation of *: - We could continue to support *-as-Type into perpetuity, as long as -XTypeOperators is not on. - We could continue to print * in error messages, perhaps depending on various extensions. Or perhaps we have a -fprint-star-for-type or some such, which would perhaps be used by instructors of courses that use materials mentioning *. - We could continue to support Unicode \bigstar (as we do today) as Type. This doesn't conflict with *-the-multiplication-operator. I would love some guidance from the committee on the above points. Lastly, the proposal does not include any plans for full removal of *, as it will leave GHC in a state where supporting *-as-type (with -XStarIsType) is not burdensome. One final alternative (just added to the proposal, as I had forgotten about it previously) that may be appealing is to use "type" to mean "Type". Because "type" is a keyword, there are no scoping issues, and so it can be always in scope, making the transition from * easier. I'm sorry if adding this alternative late in the game is disruptive, but I thought it worthy of consideration. Thanks, Richard

On Jan 25, 2018, at 5:11 PM, Simon Peyton Jones wrote:

Thanks Iavor I strongly support collapsing TypeInType and PolyKinds. I can never remember the precise differences. Having the distinction carries no user benefit; it is grounded in history not user benefit …but maintaining the distinction has very significant costs in the compiler.

I also support using Type instead of *. Think of it like this: if were designing Haskell today, would we really pick a binary operator and use it as a nullary type constructor? Surely not. It’s a huge wart. E.g. If you write (a :: *->*) GHC gets confused because it thinks *->* is one lexeme. And * is a jolly useful infix binary type constructor!! (Or in type-level arithmetic.)

Yes, * is familiar to us old guys. But you just get used to things. If you want brevity, say type T = Type. I think you’d adjust quickly.

I think we should just bit the bullet on this one.

Simon

  <> From: ghc-steering-committee [mailto:ghc-steering-committee-bounces@haskell.org] On Behalf Of Iavor Diatchki Sent: 25 January 2018 21:45 To: ghc-steering-committee@haskell.org Subject: [ghc-steering-committee] Proposal: Embrace Type in Type

Hello,

I am the shepherd for pull request #83 "Embrace Type in Type" ( https://github.com/ghc-proposals/ghc-proposals/pull/83 https://na01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fghc-proposals%2Fghc-proposals%2Fpull%2F83&data=02%7C01%7Csimonpj%40microsoft.com%7C1f034b5d72644d8d209008d5643cf50c%7Cee3303d7fb734b0c8589bcd847f1c277%7C1%7C0%7C636525135336888213&sdata=wwC%2BmVnVzPRX0luaGkC5g6deSb3qEd4jEWC%2BBg8TnNE%3D&reserved=0), and so I'd like to hear your thoughts about the proposal.

In short, the proposal has two parts:

1. Deprecate the use of `*` for the kind of inhabited Haskell types, and replace it with `Type`.

2. Deprecate extension `TypeInType`, and move its functionality to extension `PolyKinds`.

At first I was quite skeptical about both of these, but after some thought I've realized that most of my concerns are not so much about Type in Type, but rather about the data promotion mechanism, and so I won't discuss them in this e-mail.

As such, I think I would be OK with part 2. In particular, I like that when using TypeInType, one is explicit about kind parameters, as the implicit parameters of `PolyKinds` can be quite confusing. Technically, being explicit about kind parameters is an orthogonal issue to mixing up types and kinds, but this is where we are at the moment, and I think `PolyKinds` is probably more useful with `TypeInType`.

Part 1 of the proposal is obviously just a syntactic thing, but I am a bit concerned about it. In part because I actually tried for a while to use `Type` instead of `*`, and I found that the resulting kind signatures looked much more complicated. Quite possibly this is because I am very used to using `*` and eventually I would adjust, but things just ended up being much longer. It also seems unfortunate that this would break quite a lot of code, and obsolete a bunch of documentation and tutorials online.

So while I understand the reason for the proposal (the confusion between `*` the type function, and `*` the kind), I am not very keen on making this change. The proposal also suggests another extension, `StarIsType`, and when enabled `*` will always refer to the kind, and never to the type function. I am even less keen about this option, as I think it is better to pick a single notation and stick with it.

I'd love to hear what others think!

-Iavor

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

Someone pointed out on the git-hub discussion that `Type` is just a type synonym for `TYPE LiftedRep` and it is odd to use a keyword for a non-primitive. I agree. Also, if we are going to have a special case, I'd much rather have the special case be for * or ★, rather than for `type`. On Thu, Feb 1, 2018 at 5:58 PM Joachim Breitner wrote:

Hi,

Am Freitag, den 02.02.2018, 12:40 +1100 schrieb Manuel M T Chakravarty:

...

However, I have to say, I am very intrigued with the alternative to the proposal that Richard mentioned in this thread, namely to use ”type”, not ”Type”. The more I think about it, the more I like this idea.

This is somewhat analogous to (->). We could treat that as a normal binary operator that his exported by the Prelude, one that could be hidden or shadowed… but we don’t. “type” would be another thing that “Could be a normal name but isn’t”.

But I am not convinced yet.

In particular in light of our use of “type” as a explicit namespace token – so far in export and import lists and fixity declarations – I worry that we will prevent ourselves from using more such explicit namespace things in the future.

Also, the last point:

Finally, it means that

type T = Bool

adds another equality to ”type”, which is really nice.

doesn’t really work for me. If “type” is now just another (albeit) special object, then this looks rather like a functoin definition for this thing called “type”.

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

Hello, I didn't see any discussion about the third part of this proposal, namely the addition of a new extension called `StarIsKind`. The idea is that when this is on, `*` will still be treated as a special alpha-numeric name, and it will *always* refer to the kind of inhabited types (i.e., same as know). The difference is that it cannot be used as another type-level operator (e.g., for multiplication). Presumably, when this extension is on, there would be no deprecation warning emitted for `*`? We should clarify this in the proposal. I am not certain if this is a good idea. It makes the use of `*` sort of "half" deprecated, and leaves us with multiple "standard" ways to refer to the same thing (e.g., in type errors). Also, if we want people to update their code to use `Type` instead of `*`, then we are just delaying the pain point to whenever `StarIsKind` ends up being not on by default. OTOH, if we don't have a standard short-hand way to refer to the kind of inhabited types, I imagine GHC will report some very ugly errors. For example: • Expecting one more argument to ‘Maybe’ Expected a type, but ‘Maybe’ has kind ‘Data.Kind.Type -> Data.Kind.Type’ And this is for a fairly simple kind error, they get much longer if, say, monad transformers are involved. What do others think? -Iavor On Sat, Feb 3, 2018 at 8:24 PM Richard Eisenberg wrote:

...

On Feb 1, 2018, at 8:58 PM, Joachim Breitner wrote:

In particular in light of our use of “type” as a explicit namespace token – so far in export and import lists and fixity declarations – I worry that we will prevent ourselves from using more such explicit namespace things in the future.

This is a really good point. In private musings, I've often wondered about using the keyword `type` in expressions to denote a namespace change. More concretely, I'm worried about the Dreaded Namespace Problem (DNP): that is, a dependently typed language does not want to have separate type-level and term-level namespaces. Of course, Haskell has this.

The best solution I have so far to the DNP is to introduce a *new* namespace, distinct from the two namespaces we have so far. Let's call it the "default" namespace. When -XDependentTypes is on, the default namespace is in effect. Name lookup looks first in the default namespace. If that fails the namespace consulted next depends on context: the "data" namespace in terms and the "type" namespace in type signatures. (This last bit needs to be specified more concretely, but you get the idea.) Or, perhaps, a failed lookup in the default namespace will look up in both the type and data namespaces, erroring if a name appears in both.

If a user wants to specify a namespace directly, they have a very easy way to do so: `type Foo` will look in the type namespace, `data Foo` will look in the data namespace, and `default Foo` will look in the default namespace. :) Because these keywords make sense currently only at the beginning of a line, this Just Works. I also imagined these constructs could scope over a subexpression: `type (T S)`.

All of this deserves a proper proposal and it's too early for that proposal. Nevertheless, I'm grateful that Joachim said something here, given that adding `type` as a spelling of `Type` would invalidate this approach. I also am swayed by the fact that `Type` isn't fully primitive, and making a keyword mean something that's not primitive is a bit awkward. I thus retract this proposed alternative and will update the proposal accordingly.

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

Thanks, Iavor, for bringing this up. To clarify the proposal: -XStarIsType is orthogonal to deprecation. The extension is necessary in order to continue to parse existing programs, but if we choose to deprecate *, then we would deprecate even with -XStarIsType is enabled (precisely to avoid the half-deprecation scenario Iavor is worried about). I envisioned always printing Type unqualified in error messages, even if it's not imported. If a user writes Type and it's out of scope, we could always have a special-case check suggesting they import Data.Kind. I won't argue this is a principled design, though, and is likely a poor choice if some other Type is in scope. The truth is that I don't have a great way forward here (and haven't for years) and am very hopeful someone on this list can come up with one! :) The proposal has my best idea, but I'm still not thrilled with it. Thanks, Richard

On Feb 8, 2018, at 1:46 PM, Iavor Diatchki wrote:

Hello,

I didn't see any discussion about the third part of this proposal, namely the addition of a new extension called `StarIsKind`. The idea is that when this is on, `*` will still be treated as a special alpha-numeric name, and it will *always* refer to the kind of inhabited types (i.e., same as know). The difference is that it cannot be used as another type-level operator (e.g., for multiplication).

Presumably, when this extension is on, there would be no deprecation warning emitted for `*`? We should clarify this in the proposal.

I am not certain if this is a good idea. It makes the use of `*` sort of "half" deprecated, and leaves us with multiple "standard" ways to refer to the same thing (e.g., in type errors). Also, if we want people to update their code to use `Type` instead of `*`, then we are just delaying the pain point to whenever `StarIsKind` ends up being not on by default.

OTOH, if we don't have a standard short-hand way to refer to the kind of inhabited types, I imagine GHC will report some very ugly errors. For example:

• Expecting one more argument to ‘Maybe’ Expected a type, but ‘Maybe’ has kind ‘Data.Kind.Type -> Data.Kind.Type’

And this is for a fairly simple kind error, they get much longer if, say, monad transformers are involved.

What do others think?

-Iavor

On Sat, Feb 3, 2018 at 8:24 PM Richard Eisenberg mailto:rae@cs.brynmawr.edu> wrote:

...

On Feb 1, 2018, at 8:58 PM, Joachim Breitner mailto:mail@joachim-breitner.de> wrote:

In particular in light of our use of “type” as a explicit namespace token – so far in export and import lists and fixity declarations – I worry that we will prevent ourselves from using more such explicit namespace things in the future.

This is a really good point. In private musings, I've often wondered about using the keyword `type` in expressions to denote a namespace change. More concretely, I'm worried about the Dreaded Namespace Problem (DNP): that is, a dependently typed language does not want to have separate type-level and term-level namespaces. Of course, Haskell has this.

The best solution I have so far to the DNP is to introduce a *new* namespace, distinct from the two namespaces we have so far. Let's call it the "default" namespace. When -XDependentTypes is on, the default namespace is in effect. Name lookup looks first in the default namespace. If that fails the namespace consulted next depends on context: the "data" namespace in terms and the "type" namespace in type signatures. (This last bit needs to be specified more concretely, but you get the idea.) Or, perhaps, a failed lookup in the default namespace will look up in both the type and data namespaces, erroring if a name appears in both.

If a user wants to specify a namespace directly, they have a very easy way to do so: `type Foo` will look in the type namespace, `data Foo` will look in the data namespace, and `default Foo` will look in the default namespace. :) Because these keywords make sense currently only at the beginning of a line, this Just Works. I also imagined these constructs could scope over a subexpression: `type (T S)`.

All of this deserves a proper proposal and it's too early for that proposal. Nevertheless, I'm grateful that Joachim said something here, given that adding `type` as a spelling of `Type` would invalidate this approach. I also am swayed by the fact that `Type` isn't fully primitive, and making a keyword mean something that's not primitive is a bit awkward. I thus retract this proposed alternative and will update the proposal accordingly.

Richard _______________________________________________ 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

A chat with some colleagues this morning about all this led to a few thoughts I'd like to contribute: 1. We, as a committee, should decide now on the future of * (and its unicode variant). If we decide to deprecate it, we should start adding warnings and support for a long transition away from *. I don't think it's healthy to have two commonly used name for this concept into perpetuity. 2. We *could* put Type into the Prelude (after suitable waiting periods / warnings / etc). It would be painful to do so, but perhaps it's worth enduring the short-lived pain. 3. An alternative that hasn't yet been discussed is to come up with a wholly new name for this concept and use that. Our math colleagues do this all the time (viz. monoid, monad, group, ring, field, category, etc.). Even among dependently typed languages, there is some wiggle room between Set and Type (and Prop). So maybe we just invent a new name that's not as common as Type, and then put it in the Prelude. Just some food for thought... Thanks, Richard

On Feb 9, 2018, at 5:41 AM, Simon Peyton Jones wrote:

I’m not sure I see the problem here. If ‘Int’ is not in scope then f :: Int -> Int won’t work. What’s different about ‘Type’

Simon

From: ghc-steering-committee [mailto:ghc-steering-committee-bounces@haskell.org] On Behalf Of Richard Eisenberg Sent: 09 February 2018 04:26 To: Iavor Diatchki Cc: ghc-steering-committee@haskell.org; Joachim Breitner Subject: Re: [ghc-steering-committee] Proposal: Embrace Type in Type

Thanks, Iavor, for bringing this up.

To clarify the proposal: -XStarIsType is orthogonal to deprecation. The extension is necessary in order to continue to parse existing programs, but if we choose to deprecate *, then we would deprecate even with -XStarIsType is enabled (precisely to avoid the half-deprecation scenario Iavor is worried about).

I envisioned always printing Type unqualified in error messages, even if it's not imported. If a user writes Type and it's out of scope, we could always have a special-case check suggesting they import Data.Kind. I won't argue this is a principled design, though, and is likely a poor choice if some other Type is in scope.

The truth is that I don't have a great way forward here (and haven't for years) and am very hopeful someone on this list can come up with one! :) The proposal has my best idea, but I'm still not thrilled with it.

Thanks, Richard

On Feb 8, 2018, at 1:46 PM, Iavor Diatchki mailto:iavor.diatchki@gmail.com> wrote:

Hello,

I didn't see any discussion about the third part of this proposal, namely the addition of a new extension called `StarIsKind`. The idea is that when this is on, `*` will still be treated as a special alpha-numeric name, and it will *always* refer to the kind of inhabited types (i.e., same as know). The difference is that it cannot be used as another type-level operator (e.g., for multiplication).

Presumably, when this extension is on, there would be no deprecation warning emitted for `*`? We should clarify this in the proposal.

I am not certain if this is a good idea. It makes the use of `*` sort of "half" deprecated, and leaves us with multiple "standard" ways to refer to the same thing (e.g., in type errors). Also, if we want people to update their code to use `Type` instead of `*`, then we are just delaying the pain point to whenever `StarIsKind` ends up being not on by default.

OTOH, if we don't have a standard short-hand way to refer to the kind of inhabited types, I imagine GHC will report some very ugly errors. For example:

• Expecting one more argument to ‘Maybe’ Expected a type, but ‘Maybe’ has kind ‘Data.Kind.Type -> Data.Kind.Type’

And this is for a fairly simple kind error, they get much longer if, say, monad transformers are involved.

What do others think?

-Iavor

On Sat, Feb 3, 2018 at 8:24 PM Richard Eisenberg mailto:rae@cs.brynmawr.edu> wrote:

...

On Feb 1, 2018, at 8:58 PM, Joachim Breitner mailto:mail@joachim-breitner.de> wrote:

In particular in light of our use of “type” as a explicit namespace token – so far in export and import lists and fixity declarations – I worry that we will prevent ourselves from using more such explicit namespace things in the future.

This is a really good point. In private musings, I've often wondered about using the keyword `type` in expressions to denote a namespace change. More concretely, I'm worried about the Dreaded Namespace Problem (DNP): that is, a dependently typed language does not want to have separate type-level and term-level namespaces. Of course, Haskell has this.

The best solution I have so far to the DNP is to introduce a *new* namespace, distinct from the two namespaces we have so far. Let's call it the "default" namespace. When -XDependentTypes is on, the default namespace is in effect. Name lookup looks first in the default namespace. If that fails the namespace consulted next depends on context: the "data" namespace in terms and the "type" namespace in type signatures. (This last bit needs to be specified more concretely, but you get the idea.) Or, perhaps, a failed lookup in the default namespace will look up in both the type and data namespaces, erroring if a name appears in both.

If a user wants to specify a namespace directly, they have a very easy way to do so: `type Foo` will look in the type namespace, `data Foo` will look in the data namespace, and `default Foo` will look in the default namespace. :) Because these keywords make sense currently only at the beginning of a line, this Just Works. I also imagined these constructs could scope over a subexpression: `type (T S)`.

All of this deserves a proper proposal and it's too early for that proposal. Nevertheless, I'm grateful that Joachim said something here, given that adding `type` as a spelling of `Type` would invalidate this approach. I also am swayed by the fact that `Type` isn't fully primitive, and making a keyword mean something that's not primitive is a bit awkward. I thus retract this proposed alternative and will update the proposal accordingly.

Richard _______________________________________________ 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

Yes, that’s why I think, we cannot deprecate it until we have an alternative that is not the fully qualified name. Manuel

Am 10.02.2018 um 04:46 schrieb Iavor Diatchki :

The issue I see is that it is quite common to get a kind error without doing any fancy type level programming---in particular without writing kind signatures or anything like that. So you'd have no reason to import `Data.Kind(Type)`. The result would be that GHC would give quite a verbose error message, using the fully qualified name of `Type`. Unless we did something special.

-Iavor

On Fri, Feb 9, 2018 at 2:41 AM Simon Peyton Jones mailto:simonpj@microsoft.com> wrote: I’m not sure I see the problem here. If ‘Int’ is not in scope then

f :: Int -> Int

won’t work. What’s different about ‘Type’

Simon

From: ghc-steering-committee [mailto:ghc-steering-committee-bounces@haskell.org mailto:ghc-steering-committee-bounces@haskell.org] On Behalf Of Richard Eisenberg Sent: 09 February 2018 04:26 To: Iavor Diatchki mailto:iavor.diatchki@gmail.com> Cc: ghc-steering-committee@haskell.org mailto:ghc-steering-committee@haskell.org; Joachim Breitner mailto:mail@joachim-breitner.de> Subject: Re: [ghc-steering-committee] Proposal: Embrace Type in Type

Thanks, Iavor, for bringing this up.

To clarify the proposal: -XStarIsType is orthogonal to deprecation. The extension is necessary in order to continue to parse existing programs, but if we choose to deprecate *, then we would deprecate even with -XStarIsType is enabled (precisely to avoid the half-deprecation scenario Iavor is worried about).

I envisioned always printing Type unqualified in error messages, even if it's not imported. If a user writes Type and it's out of scope, we could always have a special-case check suggesting they import Data.Kind. I won't argue this is a principled design, though, and is likely a poor choice if some other Type is in scope.

The truth is that I don't have a great way forward here (and haven't for years) and am very hopeful someone on this list can come up with one! :) The proposal has my best idea, but I'm still not thrilled with it.

Thanks,

Richard

On Feb 8, 2018, at 1:46 PM, Iavor Diatchki mailto:iavor.diatchki@gmail.com> wrote:

Hello,

I didn't see any discussion about the third part of this proposal, namely the addition of a new extension called `StarIsKind`. The idea is that when this is on, `*` will still be treated as a special alpha-numeric name, and it will *always* refer to the kind of inhabited types (i.e., same as know). The difference is that it cannot be used as another type-level operator (e.g., for multiplication).

Presumably, when this extension is on, there would be no deprecation warning emitted for `*`? We should clarify this in the proposal.

I am not certain if this is a good idea. It makes the use of `*` sort of "half" deprecated, and leaves us with multiple "standard" ways to refer to the same thing (e.g., in type errors). Also, if we want people to update their code to use `Type` instead of `*`, then we are just delaying the pain point to whenever `StarIsKind` ends up being not on by default.

OTOH, if we don't have a standard short-hand way to refer to the kind of inhabited types, I imagine GHC will report some very ugly errors. For example:

• Expecting one more argument to ‘Maybe’

Expected a type, but ‘Maybe’ has kind ‘Data.Kind.Type -> Data.Kind.Type’

And this is for a fairly simple kind error, they get much longer if, say, monad transformers are involved.

What do others think?

-Iavor

On Sat, Feb 3, 2018 at 8:24 PM Richard Eisenberg mailto:rae@cs.brynmawr.edu> wrote:

...

On Feb 1, 2018, at 8:58 PM, Joachim Breitner mailto:mail@joachim-breitner.de> wrote:

In particular in light of our use of “type” as a explicit namespace token – so far in export and import lists and fixity declarations – I worry that we will prevent ourselves from using more such explicit namespace things in the future.

This is a really good point. In private musings, I've often wondered about using the keyword `type` in expressions to denote a namespace change. More concretely, I'm worried about the Dreaded Namespace Problem (DNP): that is, a dependently typed language does not want to have separate type-level and term-level namespaces. Of course, Haskell has this.

The best solution I have so far to the DNP is to introduce a *new* namespace, distinct from the two namespaces we have so far. Let's call it the "default" namespace. When -XDependentTypes is on, the default namespace is in effect. Name lookup looks first in the default namespace. If that fails the namespace consulted next depends on context: the "data" namespace in terms and the "type" namespace in type signatures. (This last bit needs to be specified more concretely, but you get the idea.) Or, perhaps, a failed lookup in the default namespace will look up in both the type and data namespaces, erroring if a name appears in both.

If a user wants to specify a namespace directly, they have a very easy way to do so: `type Foo` will look in the type namespace, `data Foo` will look in the data namespace, and `default Foo` will look in the default namespace. :) Because these keywords make sense currently only at the beginning of a line, this Just Works. I also imagined these constructs could scope over a subexpression: `type (T S)`.

All of this deserves a proper proposal and it's too early for that proposal. Nevertheless, I'm grateful that Joachim said something here, given that adding `type` as a spelling of `Type` would invalidate this approach. I also am swayed by the fact that `Type` isn't fully primitive, and making a keyword mean something that's not primitive is a bit awkward. I thus retract this proposed alternative and will update the proposal accordingly.

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

Kind signatures may not be the first thing students see, but they pop up pretty quickly, basically when you explain the difference between a manifest type and a type constructor. They also often are part of error messages, even if you don’t do fancy type-level programming and probably don’t import ’Type’ explicitly. I also think, Haskell is beyond the point where our only worry wrt to textbooks is 101 type material. So, I think, we need a convenient and concise notation that doesn’t require extra imports. Manuel

11.02.2018 15:05 Ryan Newton :

@Manuel, for you would it be sufficient for *-deprecation to have an eventual plan to put Type prelude?

I just can't see how, if Haskell were designed today, the "*" convention would come to be. Personally, I worry more about legacy/textbook issues for topics that are a bit closer to CS101 than I believe kind signatures are.

-Ryan

On Sat, Feb 10, 2018 at 12:42 AM, Manuel M T Chakravarty mailto:chak@justtesting.org> wrote: Yes, that’s why I think, we cannot deprecate it until we have an alternative that is not the fully qualified name.

Manuel

...

Am 10.02.2018 um 04:46 schrieb Iavor Diatchki mailto:iavor.diatchki@gmail.com>:

The issue I see is that it is quite common to get a kind error without doing any fancy type level programming---in particular without writing kind signatures or anything like that. So you'd have no reason to import `Data.Kind(Type)`. The result would be that GHC would give quite a verbose error message, using the fully qualified name of `Type`. Unless we did something special.

-Iavor

On Fri, Feb 9, 2018 at 2:41 AM Simon Peyton Jones mailto:simonpj@microsoft.com> wrote: I’m not sure I see the problem here. If ‘Int’ is not in scope then

f :: Int -> Int

won’t work. What’s different about ‘Type’

Simon

From: ghc-steering-committee [mailto:ghc-steering-committee-bounces@haskell.org mailto:ghc-steering-committee-bounces@haskell.org] On Behalf Of Richard Eisenberg Sent: 09 February 2018 04:26 To: Iavor Diatchki mailto:iavor.diatchki@gmail.com> Cc: ghc-steering-committee@haskell.org mailto:ghc-steering-committee@haskell.org; Joachim Breitner mailto:mail@joachim-breitner.de> Subject: Re: [ghc-steering-committee] Proposal: Embrace Type in Type

Thanks, Iavor, for bringing this up.

To clarify the proposal: -XStarIsType is orthogonal to deprecation. The extension is necessary in order to continue to parse existing programs, but if we choose to deprecate *, then we would deprecate even with -XStarIsType is enabled (precisely to avoid the half-deprecation scenario Iavor is worried about).

I envisioned always printing Type unqualified in error messages, even if it's not imported. If a user writes Type and it's out of scope, we could always have a special-case check suggesting they import Data.Kind. I won't argue this is a principled design, though, and is likely a poor choice if some other Type is in scope.

The truth is that I don't have a great way forward here (and haven't for years) and am very hopeful someone on this list can come up with one! :) The proposal has my best idea, but I'm still not thrilled with it.

Thanks,

Richard

On Feb 8, 2018, at 1:46 PM, Iavor Diatchki mailto:iavor.diatchki@gmail.com> wrote:

Hello,

I didn't see any discussion about the third part of this proposal, namely the addition of a new extension called `StarIsKind`. The idea is that when this is on, `*` will still be treated as a special alpha-numeric name, and it will *always* refer to the kind of inhabited types (i.e., same as know). The difference is that it cannot be used as another type-level operator (e.g., for multiplication).

Presumably, when this extension is on, there would be no deprecation warning emitted for `*`? We should clarify this in the proposal.

I am not certain if this is a good idea. It makes the use of `*` sort of "half" deprecated, and leaves us with multiple "standard" ways to refer to the same thing (e.g., in type errors). Also, if we want people to update their code to use `Type` instead of `*`, then we are just delaying the pain point to whenever `StarIsKind` ends up being not on by default.

OTOH, if we don't have a standard short-hand way to refer to the kind of inhabited types, I imagine GHC will report some very ugly errors. For example:

• Expecting one more argument to ‘Maybe’

Expected a type, but ‘Maybe’ has kind ‘Data.Kind.Type -> Data.Kind.Type’

And this is for a fairly simple kind error, they get much longer if, say, monad transformers are involved.

What do others think?

-Iavor

On Sat, Feb 3, 2018 at 8:24 PM Richard Eisenberg mailto:rae@cs.brynmawr.edu> wrote:

...

On Feb 1, 2018, at 8:58 PM, Joachim Breitner mailto:mail@joachim-breitner.de> wrote:

In particular in light of our use of “type” as a explicit namespace token – so far in export and import lists and fixity declarations – I worry that we will prevent ourselves from using more such explicit namespace things in the future.

This is a really good point. In private musings, I've often wondered about using the keyword `type` in expressions to denote a namespace change. More concretely, I'm worried about the Dreaded Namespace Problem (DNP): that is, a dependently typed language does not want to have separate type-level and term-level namespaces. Of course, Haskell has this.

The best solution I have so far to the DNP is to introduce a *new* namespace, distinct from the two namespaces we have so far. Let's call it the "default" namespace. When -XDependentTypes is on, the default namespace is in effect. Name lookup looks first in the default namespace. If that fails the namespace consulted next depends on context: the "data" namespace in terms and the "type" namespace in type signatures. (This last bit needs to be specified more concretely, but you get the idea.) Or, perhaps, a failed lookup in the default namespace will look up in both the type and data namespaces, erroring if a name appears in both.

If a user wants to specify a namespace directly, they have a very easy way to do so: `type Foo` will look in the type namespace, `data Foo` will look in the data namespace, and `default Foo` will look in the default namespace. :) Because these keywords make sense currently only at the beginning of a line, this Just Works. I also imagined these constructs could scope over a subexpression: `type (T S)`.

All of this deserves a proper proposal and it's too early for that proposal. Nevertheless, I'm grateful that Joachim said something here, given that adding `type` as a spelling of `Type` would invalidate this approach. I also am swayed by the fact that `Type` isn't fully primitive, and making a keyword mean something that's not primitive is a bit awkward. I thus retract this proposed alternative and will update the proposal accordingly.

Richard _______________________________________________ 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

Maybe if we can find a uncommonly used, short, descriptive name then making that available without imports is viable? Do we have any good ideas?

My only idea (it's bad) is Sort. This is inspired by Pure Type Systems, where a type system is parametrized by a set of sorts, and (ignoring levity polymorphism and unlifted types), Haskell has one sort, which could be called Sort. This is a bad idea for two reasons: - The motivation behind the name requires a reference to PTSs, which are advanced and esoteric. - It has nothing to do with, e.g., bubble sort, as everyone will be asking us into perpetuity. I've been told that brainstorming works best when even bad ideas are brought up, and so I've done so. :) Richard

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

Personally I'm not convinced by the motivation for deprecating '*': "GHC's ability to parse * has a significant cost.". There are two kinds of cost here: 1. implementation complexity 2. potential for users to be confused for (1), Haskell historically has not made concessions in the name of implementation simplicity, other concerns have tended to rate more highly: familiarity, conciseness, consistency, ease of use and so forth. (for an example of this tradeoff in action just look at the layout rule). for (2), I think even though we strive for consistency in language design, humans actually cope with exceptions very well - a few quirks here and there actually help us remember things. So the current situation isn't terrible, in my view. Furthermore in this case we're also fighting inertia: there's a lot of code, documentation and other materials using the existing syntax. Perhaps '*' wouldn't be what we would choose if we had a clean slate, but at this point I think changing it is likely worse than not changing it. Cheers Simon On 12 February 2018 at 03:54, Manuel M T Chakravarty wrote:

Yes, existing code uses ’Type’, but it also uses ’*’ (GHC included) — i.e., this change is going to be a pain for some devs anyway. A pragma that couples the removal of ’*’ as a synonym for ’Type’ with the implicit importing of ’Type’ could encourage people to just apply both changes in one go.

Manuel

...

Am 12.02.2018 um 02:04 schrieb Joachim Breitner < mail@joachim-breitner.de>:

Hi,

Am 11. Februar 2018 01:43:03 EST schrieb Manuel M T Chakravarty < chak@justtesting.org>:

...

So, I think, we need a convenient and concise notation that doesn’t require extra imports.

we have precedence for that: (->) could just as well be a name exported from Data.Function and the Prelude, with all the usual rules around it (qualifications, exports). But it is not, and rather parses as it's own thing. So far, nobody seems to bother about this exception from the rule.

But doing this to `Type` is annoying because existing code out there already used `Type`, in particular GHC.

Maybe if we can find a uncommonly used, short, descriptive name then making that available without imports is viable? Do we have any good ideas?

Joachim _______________________________________________ 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

My impression is that the committee overall supports the part of the proposal where we merge `TypeInType` with `PolyKinds`. Based on the discussion so far, opinions differ on the notation for the kind of inhabited types (currently `*`). -Iavor On Wed, Feb 21, 2018 at 6:23 AM Simon Peyton Jones wrote:

Is it true that we are supporting this proposal – except perhaps for the fate of “*”? If so, let’s agree that much at least!

Simon

*From:* Iavor Diatchki [mailto:iavor.diatchki@gmail.com] *Sent:* 09 February 2018 17:47 *To:* Simon Peyton Jones *Cc:* Richard Eisenberg ; ghc-steering-committee@haskell.org; Joachim Breitner < mail@joachim-breitner.de>

*Subject:* Re: [ghc-steering-committee] Proposal: Embrace Type in Type

The issue I see is that it is quite common to get a kind error without doing any fancy type level programming---in particular without writing kind signatures or anything like that. So you'd have no reason to import `Data.Kind(Type)`. The result would be that GHC would give quite a verbose error message, using the fully qualified name of `Type`. Unless we did something special.

-Iavor

On Fri, Feb 9, 2018 at 2:41 AM Simon Peyton Jones wrote:

I’m not sure I see the problem here. If ‘Int’ is not in scope then

f :: Int -> Int

won’t work. What’s different about ‘Type’

Simon

*From:* ghc-steering-committee [mailto: ghc-steering-committee-bounces@haskell.org] *On Behalf Of *Richard Eisenberg *Sent:* 09 February 2018 04:26 *To:* Iavor Diatchki *Cc:* ghc-steering-committee@haskell.org; Joachim Breitner < mail@joachim-breitner.de> *Subject:* Re: [ghc-steering-committee] Proposal: Embrace Type in Type

Thanks, Iavor, for bringing this up.

To clarify the proposal: -XStarIsType is orthogonal to deprecation. The extension is necessary in order to continue to parse existing programs, but if we choose to deprecate *, then we would deprecate even with -XStarIsType is enabled (precisely to avoid the half-deprecation scenario Iavor is worried about).

I envisioned always printing Type unqualified in error messages, even if it's not imported. If a user writes Type and it's out of scope, we could always have a special-case check suggesting they import Data.Kind. I won't argue this is a principled design, though, and is likely a poor choice if some other Type is in scope.

The truth is that I don't have a great way forward here (and haven't for years) and am very hopeful someone on this list can come up with one! :) The proposal has my best idea, but I'm still not thrilled with it.

Thanks,

Richard

On Feb 8, 2018, at 1:46 PM, Iavor Diatchki wrote:

Hello,

I didn't see any discussion about the third part of this proposal, namely the addition of a new extension called `StarIsKind`. The idea is that when this is on, `*` will still be treated as a special alpha-numeric name, and it will *always* refer to the kind of inhabited types (i.e., same as know). The difference is that it cannot be used as another type-level operator (e.g., for multiplication).

Presumably, when this extension is on, there would be no deprecation warning emitted for `*`? We should clarify this in the proposal.

I am not certain if this is a good idea. It makes the use of `*` sort of "half" deprecated, and leaves us with multiple "standard" ways to refer to the same thing (e.g., in type errors). Also, if we want people to update their code to use `Type` instead of `*`, then we are just delaying the pain point to whenever `StarIsKind` ends up being not on by default.

OTOH, if we don't have a standard short-hand way to refer to the kind of inhabited types, I imagine GHC will report some very ugly errors. For example:

• Expecting one more argument to ‘Maybe’

Expected a type, but ‘Maybe’ has kind ‘Data.Kind.Type -> Data.Kind.Type’

And this is for a fairly simple kind error, they get much longer if, say, monad transformers are involved.

What do others think?

-Iavor

On Sat, Feb 3, 2018 at 8:24 PM Richard Eisenberg wrote:

...

On Feb 1, 2018, at 8:58 PM, Joachim Breitner wrote:

In particular in light of our use of “type” as a explicit namespace token – so far in export and import lists and fixity declarations – I worry that we will prevent ourselves from using more such explicit namespace things in the future.

This is a really good point. In private musings, I've often wondered about using the keyword `type` in expressions to denote a namespace change. More concretely, I'm worried about the Dreaded Namespace Problem (DNP): that is, a dependently typed language does not want to have separate type-level and term-level namespaces. Of course, Haskell has this.

The best solution I have so far to the DNP is to introduce a *new* namespace, distinct from the two namespaces we have so far. Let's call it the "default" namespace. When -XDependentTypes is on, the default namespace is in effect. Name lookup looks first in the default namespace. If that fails the namespace consulted next depends on context: the "data" namespace in terms and the "type" namespace in type signatures. (This last bit needs to be specified more concretely, but you get the idea.) Or, perhaps, a failed lookup in the default namespace will look up in both the type and data namespaces, erroring if a name appears in both.

If a user wants to specify a namespace directly, they have a very easy way to do so: `type Foo` will look in the type namespace, `data Foo` will look in the data namespace, and `default Foo` will look in the default namespace. :) Because these keywords make sense currently only at the beginning of a line, this Just Works. I also imagined these constructs could scope over a subexpression: `type (T S)`.

All of this deserves a proper proposal and it's too early for that proposal. Nevertheless, I'm grateful that Joachim said something here, given that adding `type` as a spelling of `Type` would invalidate this approach. I also am swayed by the fact that `Type` isn't fully primitive, and making a keyword mean something that's not primitive is a bit awkward. I thus retract this proposed alternative and will update the proposal accordingly.

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

From the GitHub discussions and the e-mails, I've seen a couple of other options being proposed/discussed:

* Use a unicode star operator. - Pros: short, looks like the current star, much less likely to clash with stuff. - Cons: typing a unicode symbol in some editors could be a pain. * Continue using `*` (or another infix operator), but require that it be written in prefix notation, i.e. write `(*)` instead of `*`. - Pros: less of a wart, follows normal language rules - Cons: it is odd to use an infix operator that is not binary (i.e., can't be written infix); still uses up the `*` name * Continue using `*` but---at the type level---have it always refer to the kind, when used unqualified. This is what is called `StartIsKind` in the proposal. On Wed, Feb 21, 2018 at 7:59 AM Simon Peyton Jones wrote:

The issue about ‘*’ seems to be this

- We need a way to write down the kind of types. E.g. Int :: ???

What is the “???”

· There are several possibilities

1. Continue to use * as *built in syntax. *It’s a massive wart; you can’t write (*->*) because GHC thinks that’s a single lexeme; and * is a terrifically useful infix operator, so stealing it is horrible. I’m sure we would never do this today.

2. Import a module Data.Type to bring Type into scope using the *normal module scoping mechanism*.

- Advantage: no new special things - Disadvantage: an extra import; and error messages might say Data.Type.Type fully qualified if you didn’t have the import.

3. Same, but export Type from Prelude.

- Advantage: no need for that special import - Disadvantage: would break existing programs that define Type, and import Prelude, regardless of flags.

I suppose we could say that you only get Type from Prelude if -XTypeInType is also on, but that IS new (and ad hoc) mechanism.

4. Define Type as a new *keyword* (with TypeInType). It does not need to be imported; it cannot be overridden or redefined. (Just like (->).)

- A variant of this (which I quite like) is to use the existing keyword *type* (lowercase). - Advantage: simple clear story - Note: won’t break existing code; only code that says TypeInType

Is that a fair summary of the design space?

Simon

*From:* Iavor Diatchki [mailto:iavor.diatchki@gmail.com]

*Sent:* 09 February 2018 17:47 *To:* Simon Peyton Jones

*Cc:* Richard Eisenberg ; ghc-steering-committee@haskell.org; Joachim Breitner < mail@joachim-breitner.de>

*Subject:* Re: [ghc-steering-committee] Proposal: Embrace Type in Type

The issue I see is that it is quite common to get a kind error without doing any fancy type level programming---in particular without writing kind signatures or anything like that. So you'd have no reason to import `Data.Kind(Type)`. The result would be that GHC would give quite a verbose error message, using the fully qualified name of `Type`. Unless we did something special.

-Iavor

On Fri, Feb 9, 2018 at 2:41 AM Simon Peyton Jones wrote:

I’m not sure I see the problem here. If ‘Int’ is not in scope then

f :: Int -> Int

won’t work. What’s different about ‘Type’

Simon

*From:* ghc-steering-committee [mailto: ghc-steering-committee-bounces@haskell.org] *On Behalf Of *Richard Eisenberg *Sent:* 09 February 2018 04:26 *To:* Iavor Diatchki *Cc:* ghc-steering-committee@haskell.org; Joachim Breitner < mail@joachim-breitner.de> *Subject:* Re: [ghc-steering-committee] Proposal: Embrace Type in Type

Thanks, Iavor, for bringing this up.

To clarify the proposal: -XStarIsType is orthogonal to deprecation. The extension is necessary in order to continue to parse existing programs, but if we choose to deprecate *, then we would deprecate even with -XStarIsType is enabled (precisely to avoid the half-deprecation scenario Iavor is worried about).

I envisioned always printing Type unqualified in error messages, even if it's not imported. If a user writes Type and it's out of scope, we could always have a special-case check suggesting they import Data.Kind. I won't argue this is a principled design, though, and is likely a poor choice if some other Type is in scope.

The truth is that I don't have a great way forward here (and haven't for years) and am very hopeful someone on this list can come up with one! :) The proposal has my best idea, but I'm still not thrilled with it.

Thanks,

Richard

On Feb 8, 2018, at 1:46 PM, Iavor Diatchki wrote:

Hello,

I didn't see any discussion about the third part of this proposal, namely the addition of a new extension called `StarIsKind`. The idea is that when this is on, `*` will still be treated as a special alpha-numeric name, and it will *always* refer to the kind of inhabited types (i.e., same as know). The difference is that it cannot be used as another type-level operator (e.g., for multiplication).

Presumably, when this extension is on, there would be no deprecation warning emitted for `*`? We should clarify this in the proposal.

I am not certain if this is a good idea. It makes the use of `*` sort of "half" deprecated, and leaves us with multiple "standard" ways to refer to the same thing (e.g., in type errors). Also, if we want people to update their code to use `Type` instead of `*`, then we are just delaying the pain point to whenever `StarIsKind` ends up being not on by default.

OTOH, if we don't have a standard short-hand way to refer to the kind of inhabited types, I imagine GHC will report some very ugly errors. For example:

• Expecting one more argument to ‘Maybe’

Expected a type, but ‘Maybe’ has kind ‘Data.Kind.Type -> Data.Kind.Type’

And this is for a fairly simple kind error, they get much longer if, say, monad transformers are involved.

What do others think?

-Iavor

On Sat, Feb 3, 2018 at 8:24 PM Richard Eisenberg wrote:

...

On Feb 1, 2018, at 8:58 PM, Joachim Breitner wrote:

In particular in light of our use of “type” as a explicit namespace token – so far in export and import lists and fixity declarations – I worry that we will prevent ourselves from using more such explicit namespace things in the future.

This is a really good point. In private musings, I've often wondered about using the keyword `type` in expressions to denote a namespace change. More concretely, I'm worried about the Dreaded Namespace Problem (DNP): that is, a dependently typed language does not want to have separate type-level and term-level namespaces. Of course, Haskell has this.

The best solution I have so far to the DNP is to introduce a *new* namespace, distinct from the two namespaces we have so far. Let's call it the "default" namespace. When -XDependentTypes is on, the default namespace is in effect. Name lookup looks first in the default namespace. If that fails the namespace consulted next depends on context: the "data" namespace in terms and the "type" namespace in type signatures. (This last bit needs to be specified more concretely, but you get the idea.) Or, perhaps, a failed lookup in the default namespace will look up in both the type and data namespaces, erroring if a name appears in both.

If a user wants to specify a namespace directly, they have a very easy way to do so: `type Foo` will look in the type namespace, `data Foo` will look in the data namespace, and `default Foo` will look in the default namespace. :) Because these keywords make sense currently only at the beginning of a line, this Just Works. I also imagined these constructs could scope over a subexpression: `type (T S)`.

All of this deserves a proper proposal and it's too early for that proposal. Nevertheless, I'm grateful that Joachim said something here, given that adding `type` as a spelling of `Type` would invalidate this approach. I also am swayed by the fact that `Type` isn't fully primitive, and making a keyword mean something that's not primitive is a bit awkward. I thus retract this proposed alternative and will update the proposal accordingly.

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

I'd like to get this conversation going again so that we can have some closure here. To remind everyone: this is about proposal #83, where -XTypeInType is folded into -XPolyKinds and -XDataKinds. The only point of contention (both on GitHub and here in committee) is what to do about *. The proposal currently describes a mechanism, -XStarIsType, for how to deal with this. Briefly, when the extension is on (as it is by default), * means Type. When it's off, * is parsed as a normal binary infix operator. That mechanism has not gotten rave reviews in this thread, but no alternative has, either. One slightly separate question is what to print. The proposal currently suggests to print Type. There was concern in this thread that it would be printed fully-qualified, but I like Joachim's suggestion in the last known email in this thread to special-case printing of Type; even if it's not imported, it would print as Type, not Data.Kind.Type. (Unless some other Type were in scope.) It is also easy to teach GHC to print a bespoke warning when a user writes Type when it is out of scope, telling them to import Data.Kind. An alternative that hasn't been suggested so far is to have -XStarIsType control the pretty-printer as well as the parser. Simon PJ and I discussed this this morning, thinking it was a good idea. Upon further consideration, my preference would be to bite the bullet and just switch to printing Type always, but I'm not really against the print-*-with-XStarIsType idea. Regardless, it would be nice to have this settled so we can get on with implementing. Thanks! Richard

On Feb 21, 2018, at 12:52 PM, Joachim Breitner wrote:

Hi,

here is another variant of 2

2a. Import a module Data.Type to bring Type into scope using the normal module scoping mechanism. But: In error messages, unless some other Type is in scope, write “Type”

Advantage: good error messages for most Disadvantage: an extra import; a small special-casing in error messages.

Cheers, Joachim

Am Mittwoch, den 21.02.2018, 17:28 +0000 schrieb Iavor Diatchki:

...

From the GitHub discussions and the e-mails, I've seen a couple of other options being proposed/discussed:

* Use a unicode star operator. - Pros: short, looks like the current star, much less likely to clash with stuff. - Cons: typing a unicode symbol in some editors could be a pain.

* Continue using `*` (or another infix operator), but require that it be written in prefix notation, i.e. write `(*)` instead of `*`. - Pros: less of a wart, follows normal language rules - Cons: it is odd to use an infix operator that is not binary (i.e., can't be written infix); still uses up the `*` name

* Continue using `*` but---at the type level---have it always refer to the kind, when used unqualified. This is what is called `StartIsKind` in the proposal.

On Wed, Feb 21, 2018 at 7:59 AM Simon Peyton Jones wrote:

...

The issue about ‘*’ seems to be this

We need a way to write down the kind of types. E.g. Int :: ??? What is the “???”

· There are several possibilities 1. Continue to use * as built in syntax. It’s a massive wart; you can’t write (*->*) because GHC thinks that’s a single lexeme; and * is a terrifically useful infix operator, so stealing it is horrible. I’m sure we would never do this today. 2. Import a module Data.Type to bring Type into scope using the normal module scoping mechanism. Advantage: no new special things Disadvantage: an extra import; and error messages might say Data.Type.Type fully qualified if you didn’t have the import. 3. Same, but export Type from Prelude. Advantage: no need for that special import Disadvantage: would break existing programs that define Type, and import Prelude, regardless of flags. I suppose we could say that you only get Type from Prelude if -XTypeInType is also on, but that IS new (and ad hoc) mechanism. 4. Define Type as a new keyword (with TypeInType). It does not need to be imported; it cannot be overridden or redefined. (Just like (->).) A variant of this (which I quite like) is to use the existing keyword type (lowercase). Advantage: simple clear story Note: won’t break existing code; only code that says TypeInType Is that a fair summary of the design space? Simon

From: Iavor Diatchki [mailto:iavor.diatchki@gmail.com] Sent: 09 February 2018 17:47 To: Simon Peyton Jones Cc: Richard Eisenberg ; ghc-steering-committee@haskell.org; Joachim Breitner

Subject: Re: [ghc-steering-committee] Proposal: Embrace Type in Type

The issue I see is that it is quite common to get a kind error without doing any fancy type level programming---in particular without writing kind signatures or anything like that. So you'd have no reason to import `Data.Kind(Type)`. The result would be that GHC would give quite a verbose error message, using the fully qualified name of `Type`. Unless we did something special.

-Iavor

On Fri, Feb 9, 2018 at 2:41 AM Simon Peyton Jones wrote:

...

I’m not sure I see the problem here. If ‘Int’ is not in scope then f :: Int -> Int won’t work. What’s different about ‘Type’

Simon

From: ghc-steering-committee [mailto:ghc-steering-committee-bounces@haskell.org] On Behalf Of Richard Eisenberg Sent: 09 February 2018 04:26 To: Iavor Diatchki Cc: ghc-steering-committee@haskell.org; Joachim Breitner Subject: Re: [ghc-steering-committee] Proposal: Embrace Type in Type

Thanks, Iavor, for bringing this up.

To clarify the proposal: -XStarIsType is orthogonal to deprecation. The extension is necessary in order to continue to parse existing programs, but if we choose to deprecate *, then we would deprecate even with -XStarIsType is enabled (precisely to avoid the half-deprecation scenario Iavor is worried about).

I envisioned always printing Type unqualified in error messages, even if it's not imported. If a user writes Type and it's out of scope, we could always have a special-case check suggesting they import Data.Kind. I won't argue this is a principled design, though, and is likely a poor choice if some other Type is in scope.

The truth is that I don't have a great way forward here (and haven't for years) and am very hopeful someone on this list can come up with one! :) The proposal has my best idea, but I'm still not thrilled with it.

Thanks, Richard

...

On Feb 8, 2018, at 1:46 PM, Iavor Diatchki wrote:

Hello,

I didn't see any discussion about the third part of this proposal, namely the addition of a new extension called `StarIsKind`. The idea is that when this is on, `*` will still be treated as a special alpha-numeric name, and it will *always* refer to the kind of inhabited types (i.e., same as know). The difference is that it cannot be used as another type-level operator (e.g., for multiplication).

Presumably, when this extension is on, there would be no deprecation warning emitted for `*`? We should clarify this in the proposal.

I am not certain if this is a good idea. It makes the use of `*` sort of "half" deprecated, and leaves us with multiple "standard" ways to refer to the same thing (e.g., in type errors). Also, if we want people to update their code to use `Type` instead of `*`, then we are just delaying the pain point to whenever `StarIsKind` ends up being not on by default.

OTOH, if we don't have a standard short-hand way to refer to the kind of inhabited types, I imagine GHC will report some very ugly errors. For example:

• Expecting one more argument to ‘Maybe’ Expected a type, but ‘Maybe’ has kind ‘Data.Kind.Type -> Data.Kind.Type’

And this is for a fairly simple kind error, they get much longer if, say, monad transformers are involved.

What do others think?

-Iavor

On Sat, Feb 3, 2018 at 8:24 PM Richard Eisenberg wrote:

...

> On Feb 1, 2018, at 8:58 PM, Joachim Breitner wrote: > > In particular in light of our use of “type” as a explicit namespace > token – so far in export and import lists and fixity declarations – I > worry that we will prevent ourselves from using more such explicit > namespace things in the future.

This is a really good point. In private musings, I've often wondered about using the keyword `type` in expressions to denote a namespace change. More concretely, I'm worried about the Dreaded Namespace Problem (DNP): that is, a dependently typed language does not want to have separate type-level and term-level namespaces. Of course, Haskell has this.

The best solution I have so far to the DNP is to introduce a *new* namespace, distinct from the two namespaces we have so far. Let's call it the "default" namespace. When -XDependentTypes is on, the default namespace is in effect. Name lookup looks first in the default namespace. If that fails the namespace consulted next depends on context: the "data" namespace in terms and the "type" namespace in type signatures. (This last bit needs to be specified more concretely, but you get the idea.) Or, perhaps, a failed lookup in the default namespace will look up in both the type and data namespaces, erroring if a name appears in both.

If a user wants to specify a namespace directly, they have a very easy way to do so: `type Foo` will look in the type namespace, `data Foo` will look in the data namespace, and `default Foo` will look in the default namespace. :) Because these keywords make sense currently only at the beginning of a line, this Just Works. I also imagined these constructs could scope over a subexpression: `type (T S)`.

All of this deserves a proper proposal and it's too early for that proposal. Nevertheless, I'm grateful that Joachim said something here, given that adding `type` as a spelling of `Type` would invalidate this approach. I also am swayed by the fact that `Type` isn't fully primitive, and making a keyword mean something that's not primitive is a bit awkward. I thus retract this proposed alternative and will update the proposal accordingly.

Richard _______________________________________________ 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 -- 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

Hello, I have a couple of pragmatic questions: 1. To "fix" my code so that it is compatible with this change I need to do the following: 1. Whenever I have kind signatures mentioning `*`, replace `*` with `Type` 2. Import `Data.Kind(Type)` 3. Resolve conflicts involving existing datatypes named `Type`. 2. If my code has all of the properties below, then it will break as soon as this change is adopted, so I have to fix it in some way straight away: 1. uses `*` is a binary type operator, and 2. uses `*` in kind signatures, and 3. uses the `PolyKinds` language extension. 3. If my code does not have the properties in (2) but uses `*` in kind signatures, it will continue to work for 2 GHC releases, but then it will break, so I should do (1) sometime before. Is my understanding correct? -Iavor On Mon, Apr 16, 2018 at 10:46 AM Joachim Breitner wrote:

Hi,

Am Montag, den 16.04.2018, 11:55 -0400 schrieb Richard Eisenberg:

...

An alternative that hasn't been suggested so far is to have -XStarIsType control the pretty-printer as well as the parser. Simon PJ and I discussed this this morning, thinking it was a good idea. Upon further consideration, my preference would be to bite the bullet and just switch to printing Type always, but I'm not really against the print-*-with-XStarIsType idea.

I’m with Simon here. We have, I believe, precedence where error messages are affected by the language extension in scope, so this might satisfy the principle of least surprise, and also cause the least contention among our users.

We can still apply this rule when `-XNoStarIsType`:

...

One slightly separate question is what to print. The proposal currently suggests to print Type. There was concern in this thread that it would be printed fully-qualified, but I like Joachim's suggestion in the last known email in this thread to special-case printing of Type; even if it's not imported, it would print as Type, not Data.Kind.Type. (Unless some other Type were in scope.) It is also easy to teach GHC to print a bespoke warning when a user writes Type when it is out of scope, telling them to import Data.Kind.

The proposal currently does not state which modules export Type. I can infer from the text that it is Data.Kind, but this could be made explicit. Also, the proposal should state whether it is re-exported from Prelude or not (I assume it is not).

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

Would it be worth revising the proposal to incorporate the thinking in this thread, including the answers to Iavor’s questions? Simon From: ghc-steering-committee On Behalf Of Richard Eisenberg Sent: 17 April 2018 20:22 To: Iavor Diatchki Cc: ghc-steering-committee@haskell.org; Joachim Breitner Subject: Re: [ghc-steering-committee] Proposal: Embrace Type in Type Hi Iavor, See my answers below. On Apr 17, 2018, at 2:23 PM, Iavor Diatchki mailto:iavor.diatchki@gmail.com> wrote: Hello, I have a couple of pragmatic questions: 1. To "fix" my code so that it is compatible with this change I need to do the following: 1. Whenever I have kind signatures mentioning `*`, replace `*` with `Type` 2. Import `Data.Kind(Type)` 3. Resolve conflicts involving existing datatypes named `Type`. 2. If my code has all of the properties below, then it will break as soon as this change is adopted, so I have to fix it in some way straight away: 1. uses `*` is a binary type operator, and 2. uses `*` in kind signatures, and 3. uses the `PolyKinds` language extension. 3. If my code does not have the properties in (2) but uses `*` in kind signatures, it will continue to work for 2 GHC releases, but then it will break, so I should do (1) sometime before. Is my understanding correct? Not quite. First off, this proposal *does not* propose deprecating *. Earlier versions may have, but that's no longer the case. There is no concrete plan to remove * at any point in the future. Any movement to do so would be years in the future, I imagine. In point (1), "compatible" is unclear. I think you mean "compatible forever" as opposed to "compatible today". The changes you suggest in (1) are what you would have to do if we ever decide to deprecate *. For point (2), the conditions are slightly different than what you write. They should be a. enables -XTypeOperators b. uses `*` in kind signatures Modules that have these features will have to make an immediate change. They could either do the changes under your point (1) or enable -XStarIsType. The only part of this proposal that mentions something that will happen in 2 releases is that -XTypeOperators will stop implying -XNoStarIsType in two releases. That particular aspect of this is up for debate, of course. Richard -Iavor On Mon, Apr 16, 2018 at 10:46 AM Joachim Breitner mailto:mail@joachim-breitner.de> wrote: Hi, Am Montag, den 16.04.2018, 11:55 -0400 schrieb Richard Eisenberg:

An alternative that hasn't been suggested so far is to have -XStarIsType control the pretty-printer as well as the parser. Simon PJ and I discussed this this morning, thinking it was a good idea. Upon further consideration, my preference would be to bite the bullet and just switch to printing Type always, but I'm not really against the print-*-with-XStarIsType idea.

I’m with Simon here. We have, I believe, precedence where error messages are affected by the language extension in scope, so this might satisfy the principle of least surprise, and also cause the least contention among our users. We can still apply this rule when `-XNoStarIsType`:

One slightly separate question is what to print. The proposal currently suggests to print Type. There was concern in this thread that it would be printed fully-qualified, but I like Joachim's suggestion in the last known email in this thread to special-case printing of Type; even if it's not imported, it would print as Type, not Data.Kind.Type. (Unless some other Type were in scope.) It is also easy to teach GHC to print a bespoke warning when a user writes Type when it is out of scope, telling them to import Data.Kind.

The proposal currently does not state which modules export Type. I can infer from the text that it is Data.Kind, but this could be made explicit. Also, the proposal should state whether it is re-exported from Prelude or not (I assume it is not). Cheers, Joachim -- Joachim Breitner mail@joachim-breitner.demailto:mail@joachim-breitner.de http://www.joachim-breitner.de/ _______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.orgmailto: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.orgmailto:ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee

OK, I guess we should just accept this. On Tue, Apr 17, 2018 at 6:57 PM Richard Eisenberg wrote:

Done.

On Apr 17, 2018, at 7:09 PM, Simon Peyton Jones wrote:

Would it be worth revising the proposal to incorporate the thinking in this thread, including the answers to Iavor’s questions?

Simon

*From:* ghc-steering-committee

...

*On Behalf Of *Richard Eisenberg *Sent:* 17 April 2018 20:22 *To:* Iavor Diatchki *Cc:* ghc-steering-committee@haskell.org; Joachim Breitner < mail@joachim-breitner.de> *Subject:* Re: [ghc-steering-committee] Proposal: Embrace Type in Type

Hi Iavor,

See my answers below.

On Apr 17, 2018, at 2:23 PM, Iavor Diatchki wrote:

Hello,

I have a couple of pragmatic questions:

1. To "fix" my code so that it is compatible with this change I need to do the following: 1. Whenever I have kind signatures mentioning `*`, replace `*` with `Type` 2. Import `Data.Kind(Type)` 3. Resolve conflicts involving existing datatypes named `Type`.

2. If my code has all of the properties below, then it will break as soon as this change is adopted, so I have to fix it in some way straight away: 1. uses `*` is a binary type operator, and 2. uses `*` in kind signatures, and 3. uses the `PolyKinds` language extension.

3. If my code does not have the properties in (2) but uses `*` in kind signatures, it will continue to work for 2 GHC releases, but then it will break, so I should do (1) sometime before.

Is my understanding correct?

Not quite.

First off, this proposal *does not* propose deprecating *. Earlier versions may have, but that's no longer the case. There is no concrete plan to remove * at any point in the future. Any movement to do so would be years in the future, I imagine.

In point (1), "compatible" is unclear. I think you mean "compatible forever" as opposed to "compatible today". The changes you suggest in (1) are what you would have to do if we ever decide to deprecate *.

For point (2), the conditions are slightly different than what you write. They should be a. enables -XTypeOperators b. uses `*` in kind signatures Modules that have these features will have to make an immediate change. They could either do the changes under your point (1) or enable -XStarIsType.

The only part of this proposal that mentions something that will happen in 2 releases is that -XTypeOperators will stop implying -XNoStarIsType in two releases. That particular aspect of this is up for debate, of course.

Richard

-Iavor

On Mon, Apr 16, 2018 at 10:46 AM Joachim Breitner < mail@joachim-breitner.de> wrote:

Hi,

Am Montag, den 16.04.2018, 11:55 -0400 schrieb Richard Eisenberg:

...

An alternative that hasn't been suggested so far is to have -XStarIsType control the pretty-printer as well as the parser. Simon PJ and I discussed this this morning, thinking it was a good idea. Upon further consideration, my preference would be to bite the bullet and just switch to printing Type always, but I'm not really against the print-*-with-XStarIsType idea.

I’m with Simon here. We have, I believe, precedence where error messages are affected by the language extension in scope, so this might satisfy the principle of least surprise, and also cause the least contention among our users.

We can still apply this rule when `-XNoStarIsType`:

...

One slightly separate question is what to print. The proposal currently suggests to print Type. There was concern in this thread that it would be printed fully-qualified, but I like Joachim's suggestion in the last known email in this thread to special-case printing of Type; even if it's not imported, it would print as Type, not Data.Kind.Type. (Unless some other Type were in scope.) It is also easy to teach GHC to print a bespoke warning when a user writes Type when it is out of scope, telling them to import Data.Kind.

The proposal currently does not state which modules export Type. I can infer from the text that it is Data.Kind, but this could be made explicit. Also, the proposal should state whether it is re-exported from Prelude or not (I assume it is not).

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

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

You sound reluctant, Iavor. ? The point of the process is to get broad consensus for changes, and to debug them. It is not to allow vocal people like Richard and me to push through changes that others think are misguided. Or maybe I’m over-interpreting your short utterance 😊. Simon From: Iavor Diatchki Sent: 25 April 2018 01:21 To: Richard Eisenberg Cc: Simon Peyton Jones ; ghc-steering-committee@haskell.org; Joachim Breitner Subject: Re: [ghc-steering-committee] Proposal: Embrace Type in Type OK, I guess we should just accept this. On Tue, Apr 17, 2018 at 6:57 PM Richard Eisenberg mailto:rae@cs.brynmawr.edu> wrote: Done. On Apr 17, 2018, at 7:09 PM, Simon Peyton Jones mailto:simonpj@microsoft.com> wrote: Would it be worth revising the proposal to incorporate the thinking in this thread, including the answers to Iavor’s questions? Simon From: ghc-steering-committee mailto:ghc-steering-committee-bounces@haskell.org> On Behalf Of Richard Eisenberg Sent: 17 April 2018 20:22 To: Iavor Diatchki mailto:iavor.diatchki@gmail.com> Cc: ghc-steering-committee@haskell.orgmailto:ghc-steering-committee@haskell.org; Joachim Breitner mailto:mail@joachim-breitner.de> Subject: Re: [ghc-steering-committee] Proposal: Embrace Type in Type Hi Iavor, See my answers below. On Apr 17, 2018, at 2:23 PM, Iavor Diatchki mailto:iavor.diatchki@gmail.com> wrote: Hello, I have a couple of pragmatic questions: 1. To "fix" my code so that it is compatible with this change I need to do the following: 1. Whenever I have kind signatures mentioning `*`, replace `*` with `Type` 2. Import `Data.Kind(Type)` 3. Resolve conflicts involving existing datatypes named `Type`. 2. If my code has all of the properties below, then it will break as soon as this change is adopted, so I have to fix it in some way straight away: 1. uses `*` is a binary type operator, and 2. uses `*` in kind signatures, and 3. uses the `PolyKinds` language extension. 3. If my code does not have the properties in (2) but uses `*` in kind signatures, it will continue to work for 2 GHC releases, but then it will break, so I should do (1) sometime before. Is my understanding correct? Not quite. First off, this proposal *does not* propose deprecating *. Earlier versions may have, but that's no longer the case. There is no concrete plan to remove * at any point in the future. Any movement to do so would be years in the future, I imagine. In point (1), "compatible" is unclear. I think you mean "compatible forever" as opposed to "compatible today". The changes you suggest in (1) are what you would have to do if we ever decide to deprecate *. For point (2), the conditions are slightly different than what you write. They should be a. enables -XTypeOperators b. uses `*` in kind signatures Modules that have these features will have to make an immediate change. They could either do the changes under your point (1) or enable -XStarIsType. The only part of this proposal that mentions something that will happen in 2 releases is that -XTypeOperators will stop implying -XNoStarIsType in two releases. That particular aspect of this is up for debate, of course. Richard -Iavor On Mon, Apr 16, 2018 at 10:46 AM Joachim Breitner mailto:mail@joachim-breitner.de> wrote: Hi, Am Montag, den 16.04.2018, 11:55 -0400 schrieb Richard Eisenberg:

An alternative that hasn't been suggested so far is to have -XStarIsType control the pretty-printer as well as the parser. Simon PJ and I discussed this this morning, thinking it was a good idea. Upon further consideration, my preference would be to bite the bullet and just switch to printing Type always, but I'm not really against the print-*-with-XStarIsType idea.

I’m with Simon here. We have, I believe, precedence where error messages are affected by the language extension in scope, so this might satisfy the principle of least surprise, and also cause the least contention among our users. We can still apply this rule when `-XNoStarIsType`:

One slightly separate question is what to print. The proposal currently suggests to print Type. There was concern in this thread that it would be printed fully-qualified, but I like Joachim's suggestion in the last known email in this thread to special-case printing of Type; even if it's not imported, it would print as Type, not Data.Kind.Type. (Unless some other Type were in scope.) It is also easy to teach GHC to print a bespoke warning when a user writes Type when it is out of scope, telling them to import Data.Kind.

The proposal currently does not state which modules export Type. I can infer from the text that it is Data.Kind, but this could be made explicit. Also, the proposal should state whether it is re-exported from Prelude or not (I assume it is not). Cheers, Joachim -- Joachim Breitner mail@joachim-breitner.demailto:mail@joachim-breitner.de http://www.joachim-breitner.de/https://na01.safelinks.protection.outlook.com/?url=http%3A%2F%2Fwww.joachim-breitner.de%2F&data=02%7C01%7Csimonpj%40microsoft.com%7Cc3fbc3ccb9a34e49a2d808d5aa42671e%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636602124533998677&sdata=jHw8yU8qzlu2KphFVYPy%2BabkbsbYmYwfzj529S8SIrI%3D&reserved=0 _______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.orgmailto: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.orgmailto:ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee