Kind equalities update

Wed Oct 14 02:27:02 UTC 2015

This feedback is very helpful. And no direction here is more work than any other -- I haven't implemented this piece yet.

I'm not tied, at all, to `type`. I just personally think it's the best option. But it's completely a stylistic choice, and I'm quite happy to go with the majority on this point. As a counter-argument to the "hard to parse for humans" point: any syntax-highlighter for Haskell will color `type` differently, significantly easing this problem. And I'll also say that * is very confusing to beginners, in my experience: lots of people (myself included at one point) think that * is somehow a wildcard.

If we do adopt Type, there's no reason we have to reserve it. It could be exported from, say, Data.Kind (along with Constraint). Once (which may be never) we remove *, users who want kind annotations will just have to import a module. So, using Type would be just as backward-compatible as any other decision. Because we'll have kind synonyms, a large codebase could even type `type TYPE = Data.Kind.Type` or something to avoid name clashes. (This trick would work with any solution... even just leaving * alone!) 

To be very clear: I'm *not* proposing removing * anytime soon! Following the decision to aim for a 3-year window of warning-free code, we couldn't remove * until there have been 2 years of having an alternative. And even then, it's not clear to me that it's worth the trouble. Maybe we'll just deprecate it with no intent to remove. But we can wait to have that debate later.

Again, thanks for the feedback!
Richard

On Oct 13, 2015, at 9:09 PM, Christopher Allen <cma at www.bitemyapp.com> wrote:

> My opinion may not count for a lot from a compiler engineering perspective, but I can say with a fair bit of confidence that violating the "capitalized -> concrete constructor, lowercase -> variable" convention for types would be _very_ surprising to learners and users. I don't think it's a petty issue at all. This isn't a mistake we have to live with, even if it's regrettable that it's more work for Richard.
> 
> >(Wadler's Law strikes again!)
> 
> Apologies for my contributions on this front, didn't disagree with anything else and wanted to bolster Austin's concerns here.
> 
> On Tue, Oct 13, 2015 at 7:37 PM, Austin Seipp <austin at well-typed.com> wrote:
> Hey Richard,
> 
> Thanks a lot. I'm very eager to see this land ASAP! It's exciting. But...
> 
> Looking at the page, I really, really am still not a fan of using
> 'type' in place of *, and I still think (as I mentioned on Reddit I
> believe) that 'Type' is the best choice for this. I mentioned this to
> Simon earlier, and I kind of hate to make even more work for you, but
> my basic reasoning is:
> 
>   - '*' is not a good choice because it's a lexical wart. But in terms
> of 'theory', the statement '* :: *' is completely OK, or 'type ::
> type' or or 'U :: U' or 'Type :: Type'. That is, the reason star is
> bad is because it's a lexical problem that leads to weird ambiguous
> parsing, not that it's necessarily confusing or using any particular
> word I think.
> 
>   - 'type' is not a good choice, because while in theory any name is
> kind of arbitrary, it's very confusing for Haskell IMO - we have
> _chosen_ the distinction between type variables and type constructors
> through the use of capitalization. I think it's a bit strange to say
> '*' or what have you has type 'type' yet 'type' is not an actual
> variable, nor a keyword in a meaningful sense, but an actual type on
> its own. Yet 0-arity type constructors of all sorts (like Int or Bool)
> have this lexical capitalization! That is, 'type' isn't confusing
> because it's a lexical wart, or has bad parsing - but because it
> violates how we syntactically distinguish type variables from
> constructors of types.
> 
>   - (Correct if I'm wrong) As far as I understand, 'Type' doesn't need
> to be reserved unless -XTypeInType is enabled, correct? I think it is
> fairly reasonable to say that extensions may take up parts of your
> namespace should you enable them - for example, -XStaticPointers
> steals the term 'static' for itself, which I think is OK!
> 
>   - As far as code breakage goes, I think the prior point makes the
> outright breakage minimal-to-none if true, which is great. Even GHC
> uses the name `Type`, but we wouldn't even be able to use -XTypeInType
> for another few years at best! So we have plenty of time to address
> that when we want to use it...
> 
> I suppose #2 is a little 'feels-y', since 'violating' how we expect to
> read Haskell is maybe subjective. But I figure I might as well make a
> last ditch effort at the cost of a little stirring.
> 
> I think that mostly sums it up. I'm still reading over the full page,
> I just got to this point and decided to shout. (Wadler's Law strikes
> again!)
> 
> 
> On Tue, Oct 13, 2015 at 12:32 PM, Richard Eisenberg <eir at cis.upenn.edu> wrote:
> > Hi devs,
> >
> > In a chat with Simon this morning about kind equalities, he expressed that you all might want to know about the plans for kind equalities in 8.0.
> >
> > The wiki page both for user-facing changes and for implementation notes is here: https://ghc.haskell.org/trac/ghc/wiki/DependentHaskell/Phase1
> > It is my intent that all user-facing changes mentioned there will be available in 8.0. I am hard at work getting my branch ready to merge, and hope to do so mid-November.
> >
> > Note: this is almost fully backward-compatible. Here are some areas where there are known incompatibilities:
> > - Template Haskell will have to be updated. But there's a raft of changes there, anyway.
> > - GHC will do a more careful job of checking for termination of instances regarding the use of kind variables. This may require new UndecidableInstances declarations. But the fact that these definitions (like `instance (C a, C b) => C (a b)` for a polykinded C) were accepted previously could be called a bug.
> >
> > That's actually all I know of so far.
> >
> > You can take kind equalities for a spin at github.com/goldfirere/ghc, on the "nokinds" branch. Note that this hasn't been merged with `master` since December of last year, so expect a little strange behavior compared with 7.10. These wrinkles will get smoothed out, of course.
> >
> > Richard
> > _______________________________________________
> > ghc-devs mailing list
> > ghc-devs at haskell.org
> > http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
> >
> 
> 
> 
> --
> Regards,
> 
> Austin Seipp, Haskell Consultant
> Well-Typed LLP, http://www.well-typed.com/
> _______________________________________________
> ghc-devs mailing list
> ghc-devs at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
> 
> 
> 
> -- 
> Chris Allen
> Currently working on http://haskellbook.com

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20151013/dc3ce53a/attachment-0001.html>