Kind equalities update

Wed Oct 14 01:09:07 UTC 2015

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/d85eb684/attachment.html>