New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Embrace (Type :: Type) #83

Merged
merged 18 commits into from Apr 25, 2018

Conversation

Projects
None yet
@goldfirere
Contributor

goldfirere commented Oct 18, 2017

This proposal expands the meaning of -XPolyKinds to include -XTypeInType, deprecates -XTypeInType, and advocates for using Type in place of *.

Rendered

@Tritlo

This comment has been minimized.

Tritlo commented Oct 18, 2017

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

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

@goldfirere

This comment has been minimized.

Contributor

goldfirere commented Oct 18, 2017

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

There was a typo on this line; fixed now.

@RyanGlScott

This comment has been minimized.

Contributor

RyanGlScott commented Oct 18, 2017

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?

@goldfirere

This comment has been minimized.

Contributor

goldfirere commented Oct 18, 2017

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

@RyanGlScott

This comment has been minimized.

Contributor

RyanGlScott commented Oct 18, 2017

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.

@treeowl

This comment has been minimized.

Contributor

treeowl commented Oct 18, 2017

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?

@treeowl

This comment has been minimized.

Contributor

treeowl commented Oct 18, 2017

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)
@treeowl

This comment has been minimized.

Contributor

treeowl commented Oct 18, 2017

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.

@goldfirere

This comment has been minimized.

Contributor

goldfirere commented Oct 18, 2017

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.

@treeowl

This comment has been minimized.

Contributor

treeowl commented Oct 18, 2017

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

@goldfirere

This comment has been minimized.

Contributor

goldfirere commented Oct 18, 2017

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.

@AntC2

This comment has been minimized.

AntC2 commented Oct 18, 2017

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

@treeowl

This comment has been minimized.

Contributor

treeowl commented Oct 18, 2017

@goldfirere

This comment has been minimized.

Contributor

goldfirere commented Oct 18, 2017

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.

@goldfirere

This comment has been minimized.

Contributor

goldfirere commented Oct 18, 2017

(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!)

@treeowl

This comment has been minimized.

Contributor

treeowl commented Oct 18, 2017

@treeowl

This comment has been minimized.

Contributor

treeowl commented Oct 18, 2017

@AntC2

This comment has been minimized.

AntC2 commented Oct 19, 2017

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

@goldfirere

This comment has been minimized.

Contributor

goldfirere commented Oct 19, 2017

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

@treeowl

This comment has been minimized.

Contributor

treeowl commented Oct 19, 2017

@treeowl

This comment has been minimized.

Contributor

treeowl commented Oct 19, 2017

@AntC2

This comment has been minimized.

AntC2 commented Oct 19, 2017

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
@adamgundry

This comment has been minimized.

Contributor

adamgundry commented Oct 19, 2017

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.

@int-index

This comment has been minimized.

Contributor

int-index commented Jan 6, 2018

I don't believe anyone could have used the Unicode star as an infix operator, it is treated as built-in syntax and cannot be redefined at the moment.

@goldfirere

This comment has been minimized.

Contributor

goldfirere commented Jan 6, 2018

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.

@int-index

This comment has been minimized.

Contributor

int-index commented Jan 6, 2018

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?

@goldfirere

This comment has been minimized.

Contributor

goldfirere commented Jan 6, 2018

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.

@nomeata

This comment has been minimized.

Contributor

nomeata commented Jan 6, 2018

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.

@int-index

This comment has been minimized.

Contributor

int-index commented Jan 26, 2018

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 .

RyanGlScott added a commit to goldfirere/singletons that referenced this pull request Jan 26, 2018

Fully embrace Type over *
In anticipation of
ghc-proposals/ghc-proposals#83
being implemented one day.

@RyanGlScott RyanGlScott referenced this pull request Jan 26, 2018

Closed

Remove DStarT? #69

@goldfirere

This comment has been minimized.

Contributor

goldfirere commented Jan 26, 2018

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.

@vagarenko

This comment has been minimized.

vagarenko commented Jan 29, 2018

@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?

@RyanGlScott

This comment has been minimized.

Contributor

RyanGlScott commented Jan 29, 2018

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

@vagarenko

This comment has been minimized.

vagarenko commented Feb 2, 2018

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
@goldfirere

This comment has been minimized.

Contributor

goldfirere commented Feb 4, 2018

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

@RyanGlScott

This comment has been minimized.

Contributor

RyanGlScott commented Feb 9, 2018

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?

@glguy

This comment has been minimized.

glguy commented Feb 13, 2018

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.

@simonpj

This comment has been minimized.

Contributor

simonpj commented Apr 24, 2018

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.

@nomeata nomeata merged commit a89b187 into ghc-proposals:master Apr 25, 2018

@int-index int-index referenced this pull request Jun 10, 2018

Merged

Remove the * kind syntax #143

@bravit bravit added the Proposal label Nov 11, 2018

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment