Deprecate the -XTypeInType extension (as it would be a synonym for -XTypeInType).

Do you mean that it is a synonym for the -XPolyKinds extension?

No. I think -XPolyKinds is the better extension name, as Type :: Type is always true.

There was a typo on this line; fixed now.

If we are going to be removing *-the-kind entirely in favor of Type, perhaps it would make sense to reexport Type from the Prelude?

But Type is a very common datatype name, sadly. Maybe doing so would cause less breakage, though.

Indeed, we are going to be breaking a fair bit of code regardless of which choice we make. I suppose we'd have to weigh the cost of avoiding having to import Data.Kind in lots of code against the cost of hiding Type from Prelude imports in lots of code.

I think tying the question of * to TypeInType was pretty strange to begin with. It's much more clearly related to TypeOperators. Perhaps we should separate these issues and leave * imported by default for now?

Any type can be used in a kind

-XTypeInType, on the other hand, makes no assumption about the kind of a kind variable.

Can you clarify? I would hope we'd allow

forall (n :: Int#)

but what about

forall (b :: 'True)
forall (x :: Maybe)

Here's my suggestion for *:

Step 1

• Decouple * from TypeInType.

• Deprecate the use of * as a kind when TypeOperators is enabled.

• Add an extension, TypeColonOperators, that allows type operators only if they begin with a colon. With DataKinds, promoted infix data constructors (which always begin with a colon) would also be permitted. This extension, unlike TypeOperators, would be completely conservative. But it would be sufficient for the exports from Data.Type.Equality, GHC.Generics, and (as mentioned) promoted constructors.

Step 2

• Forbid the use of the kind * when TypeOperators is enabled.

Once these steps are complete, the parsing of * will be determined by TypeOperators, which is just as easy as doing it with any other extension, but (IMO) more sensible.

Tying * to TypeInType was done because, pre-GHC8, you couldn't use kind operators (precisely because kind operators were unparsable). But if types=kinds, then we would be in a pickle. So I implemented special rules to help parse *, which are kludgy and painful. Of course, looking back, there is no reason that the TypeInType extension has to control this parsing behavior, even though TypeInType and the pain around * are historically linked. I do notice in @treeowl's alternative treatment for *, the symbol is never deprecated in general, only when TypeOperators is on. I would advocate for coming up with some path, however long, to get rid of it entirely. It really causes a good deal of complication in the parser and renamer.

(One alternative to getting rid of * is to move toward mixfix notation in some way, making all the pain have more benefit instead of giving us one symbol.)

As to assumptions around the kind of a type variable: pre-GHC8, if you had foo :: .... (.... :: ... k ...) ..., then GHC would immediately assume k :: BOX, without using any inference. This is no longer the case: GHC makes no assumptions about the kind of k and then uses inference to figure it out. I don't think this will matter because there's no place you could use a kind variable of a kind other than Type (which BOX has become) in pre-TypeInType code.

@goldfirere wrote:

I do notice in @treeowl's alternative treatment for *, the symbol is never deprecated in general, only when TypeOperators is on. I would advocate for coming up with some path, however long, to get rid of it entirely. It really causes a good deal of complication in the parser and renamer.

I'm sure it does! But I conjecture that the vast majority of that pain comes from having to figure out whether * is the one from Data.Kind or not. With my suggested change, it would be determined by TypeOperators with no need to consider imports. The whole thing could be handled in the parser, with no need to bring the renamer into it. I don't see any need to ever get rid of it when TypeOperators is not in play, and breaking a whole bunch of code and a slew of printed resources shouldn't be done without a compelling reason. If you really want to be rid if it, I think my suggestion let's you remove most of its problems with minimal breakage while Type is adopted more widely, new editions of books are printed, etc. If you want to deprecate the * kind soon, planning to remove it in ten or twelve years, then I guess that's okay.

Compelling argument. Yes, I agree that if *'s meaning is determined solely by an extension (and not by imports), then supporting it into perpetuity isn't nearly so irksome.

So, may I understand your proposal this way:

• With -XNoTypeOperators, * works as it always has -- it's always in scope and it parses just like alphanumeric identifiers.
• With -XTypeOperators, it is utterly impossible to refer to * by that name. (Of course, you can still use Type.)

If this is correct, then the difficult migration is incurred only by modules with -XTypeOperators. If I've got it right, confirm this and I'll update the proposal.

breaking a whole bunch of code and a slew of printed resources shouldn't be done without a compelling reason.

Hear, hear.

If you want to deprecate the * kind soon, planning to remove it in ten or twelve years, then I guess that's okay.

More like twenty or thirty years; as in after I've hung up my coding pencil.

For students/people wanting to learn functional programming and practical type systems, what language would you recommend these days? The Haskell by which I learned to love FP seems to be turning into some bloated, barely-recognisable hieroglyphics. "Like a monstrous carbuncle on an old friend."

For students/people wanting to learn functional programming and practical type systems, what language would you recommend these days?

Haskell, of course. Since my time in this playground, the only changes that would affect beginners have been the changes to base in GHC 7.8 (the Applicative-Monad proposal and the Foldable/Traversable change). My opinions on these changes are out of scope in this discussion. The various features I've been peddling of late are specialty features that needn't be taught or learned for a long time in someone's Haskell career -- but could be used by experts to do amazing things. If you're talking about hieroglyphics, I think removing * is a big step in the right direction -- as I say in the proposal, I have yet to observe anyone learn about * without getting thrown off by its spelling. Of course, educational materials are printed and can't be updated, and so I do think (with @treeowl's suggestions) we should keep * around for a long time, but I also think that writing new materials with Type will be an improvement.

(Sidenote: Isn't this proposal process lovely? I can't tell you how many hours I spent agonizing over what to do about * (among other problems) when implementing -XTypeInType. Now that there is a public and appropriate forum for such discussions, we can all work together to build the best language we can. Thanks for everyone's contributions!)

(Sidenote: Isn't this proposal process lovely? I can't tell you how many hours I spent agonizing ...
Now that there is a public and appropriate forum for such discussions, ...

Oh, we always had ways to bikeshed over lexical syntax. ;-)

I well remember when even so great a personage as SPJ proposed a change to one of the symbols that had been in Haskell since forever. ('The power of the dot.') There were long and vehement howls of outrage. (In fact I'm wondering where all those people have gone.)

Arguably using dot for compose should never have happened. (Functional notation uses that ringy thing.) And personally I thought the proposal made a lot of sense; but there was the same riposte as here: breaking code and printed resources. (And for that educational reason, I agree with what you didn't say about the FTP change: it's been cited again this week as a reason against using Haskell in education.)

But * has always been used to represent the arity of functions.

Perhaps it's because my math background is surprisingly absent (now having earned my doctorate and gotten a job, I can admit the first college-level-or-above math class I've been associated with is the one I'm teaching at the moment!), but I've never seen * used in a way to denote a function's arity.

Returning to @treeowl's idea: What would the parser do with -XTypeOperators -XStarIsType? Or would that just be an immediate error? (I think it would have to be.)

The various features I've been peddling of late are specialty features that needn't be taught or learned for a long time in someone's Haskell career ...

Until you import some library that uses them; you don't have that extension switched on in your own code; but you make a small mistake in how you use the library; then you get an avalanche of higher-typed error messages, with type signatures containing things that don't even look like types.

Or even you make a small typo in writing a signature, and rather than GHC helpfully saying it's mal-formed, you get "Perhaps you intended to us PolyKinds or a similar language extension ...." Eek! What's that?

I'm glad to see @treeowl is talking some sense. If * were allowed as a type operator; next, people would be wanting to use . -- because it's a term-level operator. Then good luck parsing

f :: forall a . b . a -> b * Int

I like @treeowl's suggestion to decouple the * vs Type issue from other extensions, by making a new extension like StarIsType. Then it is very simple to determine what * means for a whole module (just check whether the extension is enabled), and we can argue independently at what point (if ever) the extension should be deprecated or its default state changed. In the interests of simplicity, I'd be inclined not to bother about the fully qualified case, and simply say that * cannot be used as a type operator when StarIsType is enabled.

I just typed in type a ★ b = Either a b and it was accepted. Unicode star is built-in syntax in kinds, but not in types, and that's the crux of the issue.

Ah, I was confused by the following GHCi session:

ghci> type ★ = ()
<interactive>:1:1: error: Illegal binding of built-in syntax: ★

Apparently GHC does some sort of disambiguation based on whether ★ is applied to type parameters?

Not sure, to be honest (though I can replicate your experience). It has something to do with the hackery around parsing *. Saying type (★) = () works fine.

I suppose we could teach the lexer to treat it like an alphanumeric (the way * is today). This won't conflict with the use of * as a multiplication operator. It would be backwards-incompatible, if anyone has used ★ as an infix operator in a type, but I'm willing to take my chances there.

I think a better plan is to have no special case rules in the lexer, and instead advocate the use of (*) or (★) for infix symbolical versions of Type.

I think a better plan is to have no special case rules in the lexer, and instead advocate the use of (*) or (★) for infix symbolical versions of Type.

There is reason to treat them differently:

Prelude Data.Char> isPunctuation '★'
False
Prelude Data.Char> isPunctuation '*'
True

I insist that we want a one-character shorthand for Type, and I see no better option than ★.

Despite having submitted this to the committee already, I added one last alternative that just occurred to me: use type for Type. By making it lower-case, we can piggyback on type's status as a keyword, and so it can always be in scope.

@goldfirere

By making it lower-case, we can piggyback on type's status as a keyword, and so it can always be in scope.'

Why not just put Type in the Prelude?

@vagarenko, see the series of comments starting at #83 (comment). Exporting Type from the Prelude is not without its drawbacks.

It seems a little strange to make a keyword for a thing that is not a primitive.
Type is just a type synonym defined as

type Type = TYPE LiftedRep

I've retracted my type suggestion, as now included in the proposal text.

Currently, the proposal states:

This proposal paves the way for future proposals relating to type-level features. Specifically, implementing this will make it possible to treat kind-variable scoping the same way we do type-variable scoping. The proposal is yet to be written, but I will update this paragraph when it's available.

I assume this is referring to #103?

It looks like I'm late to the party but I'd certainly like to be on record and preferring having * continue to have its current meaning. There is a lot of existing code and literature that uses this meaning of *.

The most common kinds are going to continue to be constructed from -> and *, so I'd like to see these kinds look the most succinct (whether or not we get to call these things kinds any more).

The Type constructor could continue to live in Data.Kind

I'm opposed to clever Unicode-based replacements for * and for longer word replacements.

I think we all agree that we should collapse -XPolyKinds and -XTypeInType. The only issue is what to do about *. No solution is perfect: let's get this decided!

The status quo is terrible!

• With -XTypeInType,

  • '' means Type iff '' is imported from Data.Kind
  • '*' has no special meaning otherwise; that is, it's an ordinary infix operator, and is used as such in TypeLits
  • Ambiguity error if it is in scope two ways)

• Without -XTypeInType

  • '*' means Type iff it is used in a context that syntactically means "this is a kind"
  • '*' has no special meaning otherwise

That is, the meaning of '*' depends both on the extension flags -- and moreover on a flag whose primary purpose is quite separate -- AND depends (in some cases) on lexical scope or (in other cases) on syntactic context. This is a ridiculous design.

The simplest thing to do is to say

• The meaning of '*' is controlled by a flag, -XStarIsType, that has no other purpose
• -XStarIsType is on by default. (Perhaps: switched off by -XTypeOperators.)
• 'Type' is exported by Data.Type (or whatever) and is always available as an alternative to '*'.
• When -XStarIsType is on, we print '*' in error messages whenever possible.

That is simple and explicable. Moreover the on-by-default rule means that most existing prams that use PolyKinds will continue to work unchanged. In effect -XStarIsType is roughly the delta between -XPolyKinds and -XTypeInType.

Once that is in place we can think about future policy. For example

• Leave it alone
• Announce that -XStarIsType will move to off-by-default in a specified future GHC XX.YY, and emit deprecation messages for three previous releases

But let's get this done, one way or another.